avewright/proofwiki-math huggingface dataset:
Theorem: Intersection is Commutative/Family of Sets

Let $\family {S_i}_{i \mathop \in I}$ be an indexed family of sets.
Let $\ds I = \bigcap_{i \mathop \in I} S_i$ denote the intersection of $\family {S_i}_{i \mathop \in I}$.
Let $J \subseteq I$ be a subset of $I$.
Then:
:$\ds \bigcap_{i \mathop \in I} S_i = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k = \bigcap_{k \mathop \in \relcomp I J} S_k \cap \bigcap_{j \mathop \in J} S_j$
where $\relcomp I J$ denotes the complement of $J$ relative to $I$.

Proof:
{{begin-eqn}}
{{eqn | l = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k
      | r = \map \complement {\map \complement {\bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k} }
      | c = Complement of Complement
}}
{{eqn | r = \map \complement {\map \complement {\bigcap_{j \mathop \in J} S_j} \cup \map \complement {\bigcap_{k \mathop \in \relcomp I J} S_k} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection
}}
{{eqn | n = 1
      | r = \map \complement {\bigcup_{j \mathop \in J} \map \complement {S_j} \cup \bigcup_{k \mathop \in \relcomp I J} \map \complement {S_k} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \map \complement {\bigcup_{k \mathop \in \relcomp I J} \map \complement {S_k} \cup \bigcup_{j \mathop \in J} \map \complement {S_j} }
      | c = General Commutativity of Set Union
}}
{{eqn | r = \map \complement {\map \complement {\bigcap_{k \mathop \in \relcomp I J} S_k}\cup \map \complement {\bigcap_{j \mathop \in J} S_j} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \map \complement {\map \complement {\bigcap_{k \mathop \in \relcomp I J} \cap S_k \bigcap_{j \mathop \in J} S_j} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Complement of Intersection
}}
{{eqn | r = \bigcap_{k \mathop \in \relcomp I J} S_k \cap \bigcap_{j \mathop \in J} S_j
      | c = Complement of Complement
}}
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = \bigcap_{i \mathop \in I} S_i
      | r = \map \complement {\map \complement {\bigcap_{i \mathop \in I} S_i} }
      | c = Complement of Complement
}}
{{eqn | r = \map \complement {\bigcup_{i \mathop \in I} \map \complement {S_i} }
      | c = De Morgan's Laws (Set Theory)/Set Complement/Family of Sets/Complement of Intersection
}}
{{eqn | r = \map \complement {\bigcup_{j \mathop \in J} \map \complement {S_j} \cup \bigcup_{k \mathop \in \relcomp I J} \map \complement {S_k} }
      | c = General Commutativity of Set Union
}}
{{eqn | r = \bigcap_{j \mathop \in J} S_j \cap \bigcap_{k \mathop \in \relcomp I J} S_k
      | c = from $(1)$ above
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral to Infinity of Power of x by Logarithm of x over One plus x

:$\ds \int_0^\infty \frac {x^{p - 1} \ln x} {1 + x} \rd x = -\pi^2 \csc p \pi \cot p \pi$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {x^{p - 1} \ln x} {1 + x} \rd x
	| r = \int_0^\infty \frac 1 {1 + x} \map {\frac \partial {\partial p} } {x^{p - 1} } \rd x
	| c = Derivative of Power of Constant
}}
{{eqn	| r = \frac \d {\d p} \int_0^\infty \frac {x^{p - 1} } {1 + x} \rd x
	| c = Definite Integral of Partial Derivative
}}
{{eqn	| r = \map {\frac \d {\d p} } {\pi \csc p \pi}
	| c = Definite Integral to Infinity of $\dfrac {x^{p - 1} } {1 + x}$
}}
{{eqn	| r = -\pi^2 \csc p \pi \cot p \pi
	| c = Chain Rule for Derivatives, Derivative of Cosecant Function
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Logarithm of Sine x

:$\ds \int_0^{\pi/2} \map \ln {\sin x} \rd x = -\frac \pi 2 \ln 2$

Proof:
By Definite Integral from $0$ to $\dfrac \pi 2$ of $\map \ln {\sin x}$: Lemma, we have: 
:$\ds \int_0^\pi \map \ln {\sin x} \rd x = 2 \int_0^{\pi/2} \map \ln {\sin x} \rd x$
We also have: 
{{begin-eqn}}
{{eqn	| l = \int_0^{\pi/2} \map \ln {\sin x} \rd x
	| r = \int_0^{\pi/2} \map \ln {\map \sin {\frac \pi 2 - x} } \rd x
	| c = Integral between Limits is Independent of Direction
}}
{{eqn	| r = \int_0^{\pi/2} \map \ln {\cos x} \rd x
	| c = Sine of Complement equals Cosine
}}
{{end-eqn}}
giving: 
{{begin-eqn}}
{{eqn	| l = 2 \int_0^{\pi/2} \map \ln {\sin x} \rd x
	| r = \int_0^{\pi/2} \map \ln {\sin x \cos x} \rd x
	| c = Sum of Logarithms
}}
{{eqn	| r = \int_0^{\pi/2} \map \ln {\frac 1 2 \sin 2 x} \rd x
	| c = Double Angle Formula for Sine
}}
{{eqn	| r = \frac \pi 2 \map \ln {\frac 1 2} + \int_0^{\pi/2} \map \ln {\sin 2 x} \rd x
	| c = Primitive of Constant, Sum of Logarithms
}}
{{eqn	| r = \frac \pi 2 \map \ln {\frac 1 2} + \frac 1 2 \int_0^\pi \map \ln {\sin u} \rd u
	| c = substituting $u = 2 x$
}}
{{eqn	| r = -\frac \pi 2 \ln 2 + \int_0^{\pi/2} \map \ln {\sin u} \rd u
	| c = Logarithm of Reciprocal
}}
{{end-eqn}}
Therefore: 
:$\ds \int_0^{\pi/2} \map \ln {\sin x} \rd x = -\frac \pi 2 \ln 2$
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Logarithm of Sine x

:$\ds \int_0^{\pi/2} \map \ln {\sin x} \rd x = -\frac \pi 2 \ln 2$

Proof:
By {{Lemma|Definite Integral from 0 to Half Pi of Logarithm of Sine x|disp = Definite Integral from $0$ to $\dfrac \pi 2$ of $\map \ln {\sin x}$}}, we have: 
:$\ds \int_0^\pi \map \ln {\sin x} \rd x = 2 \int_0^{\pi/2} \map \ln {\sin x} \rd x$
By Product of Sines of Fractions of Pi, we have: 
:$\ds \prod_{k \mathop = 1}^{n - 1} \map \sin {\frac {k \pi} n} = \frac n {2^{n - 1} }$
Therefore, we have: 
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = 1}^{n - 1} \map \ln {\map \sin {\frac {k \pi} n} }
      | r = \map \ln {\prod_{k \mathop = 1}^{n - 1} \map \sin {\frac {k \pi} n} }
      | c = Sum of Logarithms: Natural Logarithm
}}
{{eqn | r = \map \ln {\frac n {2^{n - 1} } }
}}
{{eqn | r = \ln n - \paren {n - 1} \ln 2
      | c = Difference of Logarithms
}}
{{end-eqn}}
We have: 
{{begin-eqn}}
{{eqn | l = \int_0^\pi \map \ln {\sin x} \rd x
      | r = \lim_{n \mathop \to \infty} \frac \pi n \sum_{k \mathop = 1}^{n - 1} \map \ln {\map \sin {\frac {\pi k} n} } 
      | c = {{Defof|Riemann Integral}}
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren {\frac \pi n \ln n - \pi \paren {1 - \frac 1 n} \ln 2}
}}
{{end-eqn}}
We can show the first term to vanish: 
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \frac \pi n \ln n
      | r = \pi \lim_{u \mathop \to \infty} u e^{-u}
      | c = letting $n = e^u$
}}
{{eqn | r = 0
      | c = Limit to Infinity of $x^n e^{-a x}$
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \paren {\frac \pi n \ln n - \pi \paren {1 - \frac 1 n} \ln 2}
      | r = -\pi \ln 2 \lim_{n \mathop \to \infty} \paren {1 - \frac 1 n}
      | c = Combined Sum Rule for Limits of Real Functions
}}
{{eqn | r = -\pi \ln 2
}}
{{end-eqn}}
giving:
:$\ds \int_0^{\pi/2} \map \ln {\sin x} \rd x = -\frac \pi 2 \ln 2$
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Logarithm of Cosine x

:$\ds \int_0^{\pi/2} \map \ln {\cos x} \rd x = -\frac \pi 2 \ln 2$

Proof:
By Definite Integral from $0$ to $\dfrac \pi 2$ of $\map \ln {\sin x}$: Proof 1 we have: 
:$\ds \int_0^{\pi/2} \map \ln {\sin x} \rd x = \int_0^{\pi/2} \map \ln {\cos x} \rd x$
and:
:$\ds \int_0^{\pi/2} \map \ln {\sin x} \rd x = -\frac \pi 2 \ln 2$
The result follows.
{{qed}}
Theorem: Non-Null Cauchy Sequence in Non-Archimedean Norm is Eventually Stationary/P-adic Norm

Let $p$ be a prime number.
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers.
Let $\sequence {x_n}$ be a Cauchy sequence such that $\sequence {x_n}$ does not converge to $0$.
Then:
:$\exists N \in \N: \forall n, m \ge N: \norm {x_n}_p = \norm {x_m}_p$

Proof:
From:
:P-adic Numbers form Non-Archimedean Valued Field
:Non-Null Cauchy Sequence in Non-Archimedean Norm is Eventually Stationary 
it follows that:
:$\exists N \in \N: \forall n, m \ge N: \norm {x_n}_p = \norm {x_m}_p$
{{qed}}
Theorem: Definite Integral to Infinity of Logarithm of Exponential of x plus One over Exponential of x minus One

:$\ds \int_0^\infty \map \ln {\frac {e^x + 1} {e^x - 1} } \rd x = \frac {\pi^2} 4$

Proof:
We can write: 
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \map \ln {\frac {e^x + 1} {e^x - 1} } \rd x
	| r = \int_0^\infty \map \ln {\frac {e^{x/2} \paren {e^{x/2} + e^{-x/2} } } {e^{x/2} \paren {e^{x/2} - e^{-x/2} } } } \rd x
}}
{{eqn	| r = \int_0^\infty \map \ln {\coth \frac x 2} \rd x
	| c = {{Defof|Hyperbolic Cotangent}}
}}
{{end-eqn}}
Let: 
:$u = \coth \dfrac x 2$
We have, by Derivative of Hyperbolic Cotangent Function:
:$\dfrac {\d u} {\d x} = -\dfrac 1 2 \csch^2 \dfrac x 2$
From Difference of Squares of Hyperbolic Cotangent and Cosecant, this can be written: 
:$\dfrac {\d u} {\d x} = \dfrac 1 2 \paren {1 - \coth^2 \dfrac x 2} = \dfrac 1 2 \paren {1 - u^2}$
From Limit to Infinity of Hyperbolic Cotangent Function, we have: 
:as $x \to \infty$, $u \to 1$.
We also have: 
:as $x \to 0^+$, $u \to \infty$.
With this, we have: 
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \map \ln {\coth \frac x 2} \rd x
	| r = 2 \int_\infty^1 \frac {\ln u} {1 - u^2} \rd u
	| c = substituting $u = \coth \dfrac x 2$
}}
{{eqn	| r = -2 \int_1^\infty \frac {\ln u} {1 - u^2} \rd u
	| c = Reversal of Limits of Definite Integral
}}
{{eqn	| r = -2 \int_1^0 \paren {-\frac 1 {v^2} } \frac {\map \ln {\frac 1 v} } {1 - \paren {\frac 1 {v^2} }^2} \rd v
	| c = substituting $v = \dfrac 1 v$
}}
{{eqn	| r = -2 \int_0^1 \frac {\ln v} {1 - v^2} \rd v
	| c = Reversal of Limits of Definite Integral
}}
{{eqn	| r = -2 \int_0^1 \ln v \paren {\sum_{n \mathop = 0}^\infty \paren {v^2}^n} \rd v
	| c = Sum of Infinite Geometric Sequence
}}
{{eqn	| r = -2 \sum_{n \mathop = 0}^\infty \int_0^1 v^{2 n} \ln v \rd v
	| c = Fubini's Theorem
}}
{{eqn	| r = 2 \sum_{n \mathop = 0}^\infty \frac {\map \Gamma 2} {\paren {2 n + 1}^2}
	| c = Definite Integral from $0$ to $1$ of $x^m \paren {\ln x}^n$
}}
{{eqn	| r = 2 \times 1! \times \frac {\pi^2} 8
	| c = Gamma Function Extends Factorial, Sum of Reciprocals of Squares of Odd Integers
}}
{{eqn	| r = \frac {\pi^2} 4
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Quarter Pi of Logarithm of One plus Tan x

:$\ds \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x = \frac \pi 8 \ln 2$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x
	| r = \int_0^{\pi/4} \map \ln {1 + \map \tan {\frac \pi 4 - x} } \rd x
	| c = Integral between Limits is Independent of Direction
}}
{{eqn	| r = \int_0^{\pi/4} \map \ln {1 + \frac {\tan \frac \pi 4 - \tan x} {1 + \tan \frac \pi 4 \tan x} } \rd x
	| c = Tangent of Difference
}}
{{eqn	| r = \int_0^{\pi/4} \map \ln {1 + \frac {1 - \tan x} {1 + \tan x} } \rd x
	| c = Tangent of $45 \degrees$
}}
{{eqn	| r = \int_0^{\pi/4} \map \ln {\frac 2 {1 + \tan x} } \rd x
}}
{{eqn	| r = \int_0^{\pi/4} \ln 2 \rd x - \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x
	| c = Difference of Logarithms
}}
{{eqn	| r = \frac \pi 4 \ln 2 - \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x
	| c = Primitive of Constant
}}
{{end-eqn}}
Therefore: 
:$\ds 2 \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x = \frac \pi 4 \ln 2$
giving: 
:$\ds \int_0^{\pi/4} \map \ln {1 + \tan x} \rd x = \frac \pi 8 \ln 2$
{{qed}}
Theorem: Primitive of Sine x by Logarithm of Sine x

:$\ds \int \sin x \map \ln {\sin x} \rd x = \cos x \paren {1 - \map \ln {\sin x} } + \ln \size {\tan \frac x 2} + C$

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \map {\frac \d {\d x} } {\map \ln {\sin x} } 
	| r = \map {\frac \d {\map \d {\sin x} } } {\map \ln {\sin x} } \map {\frac \d {\d x} } {\sin x}
	| c = Chain Rule for Derivatives
}}
{{eqn	| r = \frac {\cos x} {\sin x}
	| c = Derivative of Logarithm Function, Derivative of Sine Function
}}
{{end-eqn}}
We also have, by Primitive of Sine Function:
:$\ds \int \sin x \rd x = -\cos x + C$
So: 
{{begin-eqn}}
{{eqn	| l = \int \sin x \map \ln {\sin x} \rd x
	| r = -\cos x \map \ln {\sin x} + \int \frac {\cos^2 x} {\sin x} \rd x
	| c = Integration by Parts
}}
{{eqn	| r = -\cos x \map \ln {\sin x} + \int \frac {1 - \sin^2 x} {\sin x} \rd x
	| c = Sum of Squares of Sine and Cosine
}}
{{eqn	| r = -\cos x \map \ln {\sin x} + \int \csc x \rd x - \int \sin x \rd x
}}
{{eqn	| r = -\cos x \map \ln {\sin x} + \ln \size {\tan \frac x 2} + \cos x + C
	| c = Primitive of Sine Function, Primitive of $\csc x$: Tangent Form
}}
{{eqn	| r = \cos x \paren {1 - \map \ln {\sin x} } + \ln \size {\tan \frac x 2} + C
}}
{{end-eqn}}
{{qed}}
Category:Primitives involving Sine Function
Category:Primitives involving Logarithm Function
qvetd42p66dfj06kdl355f9xzlg3ah0
Theorem: Euler-Mascheroni Constant as Difference of Integrals involving Cosine

:$\ds \int_0^1 \frac {1 - \cos x} x \rd x - \int_1^\infty \frac {\cos x} x \rd x = \gamma$

Proof:
From Characterization of Cosine Integral Function, we have: 
:$\ds \int_t^\infty \frac {\cos x} x \rd x = -\gamma - \ln t + \int_0^t \frac {1 - \cos x} x \rd x$
for all real $t > 0$.
Rearranging: 
:$\ds \int_0^t \frac {1 - \cos x} x \rd x - \int_t^\infty \frac {\cos x} x \rd x = \gamma + \ln t$
Setting $t = 1$ gives the result, from Natural Logarithm of 1 is 0.
{{qed}}
Theorem: Definite Integral from 0 to 1 of Arcsine of x over x

:$\ds \int_0^1 \frac {\arcsin x} x = \frac \pi 2 \ln 2$

Proof:
Let: 
:$x = \sin \theta$
By Derivative of Sine Function, we have: 
:$\dfrac {\d x} {\d \theta} = \cos \theta$
We have, by Arcsine of Zero is Zero: 
:as $x \to 0$, $\theta \to \arcsin 0 = 0$.
By Arcsine of One is Half Pi, we have: 
:as $x \to 1$, $\theta \to \arcsin 1 = \dfrac \pi 2$.
We have:
{{begin-eqn}}
{{eqn | l = \int_0^1 \frac {\arcsin x} x \rd x
      | r = \int_0^{\pi/2} \frac {\cos \theta \map \arcsin {\sin \theta} } {\sin \theta} \rd \theta
      | c = substituting $x = \sin \theta$ 
}}
{{eqn | r = \int_0^{\pi/2} \theta \cot \theta \rd \theta
      | c = {{Defof|Real Arcsine}}, {{Defof|Real Cotangent Function}}
}}
{{end-eqn}}
By Primitive of Cotangent Function:
:$\ds \int \cot \theta \rd \theta = \map \ln {\sin \theta} + C$
So:
{{begin-eqn}}
{{eqn | l = \int_0^{\pi/2} \theta \cot \theta \rd \theta
      | r = \bigintlimits {\theta \map \ln {\sin \theta} } 0 {\frac \pi 2} - \int_0^{\pi/2} \map \ln {\sin \theta} \rd \theta
      | c = Integration by Parts
}}
{{eqn | r = \frac \pi 2 \map \ln {\sin \frac \pi 2} - \lim_{\theta \to 0^+} \paren {\theta \map \ln {\sin \theta} } + \frac \pi 2 \ln 2
      | c = Definite Integral from 0 to $\dfrac \pi 2$ of $\map \ln {\sin x}$
}}
{{eqn | r = -\lim_{\theta \to 0^+} \paren {\theta \map \ln {\sin \theta} } + \frac \pi 2 \ln 2
      | c = Sine of Right Angle, Natural Logarithm of 1 is 0
}} 
{{end-eqn}}
We have: 
{{begin-eqn}}
{{eqn | l = \lim_{\theta \to 0^+} \paren {\theta \map \ln {\sin \theta} }
      | r = \lim_{\theta \to 0^+} \paren {\theta \map \ln {\frac {\sin \theta} \theta \theta} }
}}
{{eqn | r = \lim_{\theta \to 0^+} \paren {\theta \map \ln {\frac {\sin \theta} \theta} } + \lim_{\theta \to 0^+} \theta \ln \theta
      | c = Sum of Logarithms, Sum Rule for Limits of Real Functions
}}
{{eqn | r = \paren {\lim_{\theta \to 0^+} \theta} \paren {\map \ln {\lim_{\theta \to 0^+} \frac {\sin \theta} \theta} } + \lim_{\theta \to 0^+} \theta \ln \theta
      | c = Product Rule for Limits of Real Functions
}}
{{eqn | r = 0 \ln 1 + 0
      | c = Limit of $\dfrac {\sin x} x$ at Zero, Limit of $x^n \paren {\ln x}^m$
}}
{{eqn | r = 0
}}
{{end-eqn}}
giving: 
:$\ds \int_0^{\pi/2} \theta \cot \theta \rd \theta = \frac \pi 2 \ln 2$
hence the result.
{{qed}}
Theorem: Definite Integral from 0 to 1 of Arctangent of x over x

:$\ds \int_0^1 \frac {\arctan x} x \rd x = G$

Proof:
{{begin-eqn}}
{{eqn | l = \int_0^1 \frac {\arctan x} x \rd x
      | r = \int_0^1 \frac 1 x \paren {\sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {2 n + 1} } \rd x
      | c = Power Series Expansion for Real Arctangent Function
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {2 n + 1} \int_0^1 x^{2 n} \rd x
      | c = Power Series is Termwise Integrable within Radius of Convergence
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {2 n + 1} \intlimits {\frac {x^{2 n + 1} } {2 n + 1} } 0 1 \rd x
      | c = Primitive of Power
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {2 n + 1}^2}
      | c = evaluation of definite integral
}}
{{eqn | r = G
      | c = {{Defof|Catalan's Constant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of x over Sine x

:$\ds \int_0^{\pi/2} \frac x {\sin x} \rd x = 2 G$

Proof:
From Definite Integral from $0$ to $1$ of $\dfrac {\arctan x} x$, we have: 
:$\ds \int_0^1 \frac {\arctan x} x \rd x = G$
Let: 
:$x = \tan \theta$ 
By Derivative of Tangent Function, we have: 
:$\ds \frac {\d x} {\d \theta} = \sec^2 \theta$
We have, by Arctangent of Zero is Zero: 
:as $x \to 0$, $\theta \to 0$.
We also have, by Arctangent of One:
:as $x \to 1$, $\theta \to \dfrac \pi 4$
We therefore have: 
{{begin-eqn}}
{{eqn	| l = \int_0^1 \frac {\arctan x} x \rd x
	| r = \int_0^{\pi/4} \frac {\sec^2 \theta \map \arctan {\tan \theta} } {\tan \theta} \rd \theta
	| c = substituting $x = \tan \theta$
}}
{{eqn	| r = \int_0^{\pi/4} \frac \theta {\cos^2 \theta} \times \frac {\cos \theta} {\sin \theta} \rd \theta
	| c = {{Defof|Real Secant Function}}, {{Defof|Real Tangent Function}}
}}
{{eqn	| r = \int_0^{\pi/4} \frac \theta {\sin \theta \cos \theta} \rd \theta
}}
{{eqn	| r = \int_0^{\pi/4} \frac \theta {\frac 1 2 \sin 2 \theta} \rd \theta
	| c = Double Angle Formula for Sine
}}
{{eqn	| r = \frac 1 2 \int_0^{\pi/2} \frac \phi {\sin \phi} \rd \phi
	| c = substituting $\phi = 2 \theta$
}}
{{end-eqn}}
giving: 
:$\ds \int_0^{\pi/2} \frac \phi {\sin \phi} \rd \phi = 2 G$
{{qed}}
Theorem: Definite Integral to Infinity of Arctangent of p x minus Arctangent of q x over x

:$\ds \int_0^\infty \frac {\arctan p x - \arctan q x} x \rd x = \frac \pi 2 \ln \frac p q$

Proof:
Note that the integrand is of the form: 
:$\ds \int_0^\infty \frac {\map f {p x} - \map f {q x} } x \rd x$
where:
:$\map f x = \arctan x$
We have, by Derivative of Arctangent Function:
:$\map {f'} x = \dfrac 1 {1 + x^2}$
which is continuous on $\R$. 
By Limit to Infinity of Arctangent Function: 
:$\ds \lim_{x \mathop \to \infty} \map f x =  \lim_{x \mathop \to \infty} \arctan x = \frac \pi 2$
As $f$ is continuously differentiable and $\ds \lim_{x \mathop \to \infty} \map f x$ exists and is finite, we may apply Frullani's Integral, giving:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \frac {\arctan p x - \arctan q x} x \rd x
	| r = \paren {\lim_{x \mathop \to \infty} \arctan x - \arctan 0} \ln \frac p q
}}
{{eqn	| r = \frac \pi 2 \ln \frac p q
	| c = Arctangent of Zero is Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Definite Integral from 0 to Half Pi of Sine x by Logarithm of Sine x

:$\ds \int_0^{\pi/2} \sin x \map \ln {\sin x} \rd x = \ln 2 - 1$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^{\pi/2} \sin x \map \ln {\sin x} \rd x
	| r = \intlimits {\cos x \paren {1 - \map \ln {\sin x} } + \map \ln {\tan \frac x 2} } 0 {\pi/2}
	| c = Primitive of $\sin x \map \ln {\sin x}$
}}
{{eqn	| r = \cos \frac \pi 2 \paren {1 - \map \ln {\sin \frac \pi 2} } + \map \ln {\tan \frac \pi 4} - \cos 0 + \lim_{x \mathop \to 0^+} \paren {\map \ln {\sin x} - \map \ln {\tan \frac x 2} }
}}
{{eqn	| r = -1 + \lim_{x \mathop \to 0^+} \paren {\map \ln {\sin x} - \map \ln {\tan \frac x 2} }
	| c = Cosine of Right Angle, Tangent of $45 \degrees$, Natural Logarithm of 1 is 0, Cosine of Zero is One
}}
{{end-eqn}}
It remains to compute: 
:$\ds \lim_{x \mathop \to 0^+} \paren {\map \ln {\sin x} - \map \ln {\tan \frac x 2} }$
We have:
{{begin-eqn}}
{{eqn	| l = \lim_{x \mathop \to 0^+} \paren {\map \ln {\sin x} - \map \ln {\tan \frac x 2} }
	| r = \lim_{x \mathop \to 0^+} \paren {\map \ln {2 \sin \frac x 2 \cos \frac x 2} - \map \ln {\sin \frac x 2} + \map \ln {\cos \frac x 2} }
	| c = Double Angle Formula for Sine, {{Defof|Real Tangent Function}}, Difference of Logarithms
}}
{{eqn	| r = \lim_{x \mathop \to 0^+} \paren {\ln 2 + \map \ln {\sin \frac x 2} + \map \ln {\cos \frac x 2} - \map \ln {\sin \frac x 2} + \map \ln {\cos \frac x 2} }
	| c = Sum of Logarithms
}}
{{eqn	| r = \ln 2 + 2 \lim_{x \mathop \to 0^+} \map \ln {\cos \frac x 2}
	| c = Sum Rule for Limits of Real Functions
}}
{{eqn	| r = \ln 2 + 2 \map \ln {\lim_{x \mathop \to 0^+} \cos \frac x 2}
}}
{{eqn	| r = \ln 2 + 2 \ln 1
	| c = Cosine of Zero is One
}}
{{eqn	| r = \ln 2
	| c = Natural Logarithm of 1 is 0
}}
{{end-eqn}}
giving: 
:$\ds \int_0^{\pi/2} \sin x \map \ln {\sin x} \rd x = \ln 2 - 1$
{{qed}}
Theorem: Definite Integral from 0 to Pi of x by Logarithm of Sine x

:$\ds \int_0^\pi x \map \ln {\sin x} \rd x = -\frac {\pi^2} 2 \ln 2$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\pi x \map \ln {\sin x} \rd x
	| r = \int_0^\pi \paren {\pi - x} \map \ln {\map \sin {\pi - x} } \rd x
	| c = Integral between Limits is Independent of Direction
}}
{{eqn	| r = \pi \int_0^\pi \map \ln {\sin x} - \int_0^\pi x \map \ln {\sin x} \rd x
	| c = Sine of Supplementary Angle, Linear Combination of Definite Integrals
}}
{{end-eqn}}
So: 
{{begin-eqn}}
{{eqn	| l = 2 \int_0^\pi x \map \ln {\sin x} \rd x
	| r = \pi \int_0^\pi \map \ln {\sin x} \rd x
}}
{{eqn	| r = 2 \pi \int_0^{\pi/2} \map \ln {\sin x} \rd x
	| c = Definite Integral from $0$ to $\dfrac \pi 2$ of $\map \ln {\sin x}$: Lemma
}}
{{eqn	| r = -\pi^2 \ln 2
	| c = Definite Integral from $0$ to $\dfrac \pi 2$ of $\map \ln {\sin x}$
}}
{{end-eqn}}
giving: 
:$\ds \int_0^\pi x \map \ln {\sin x} \rd x = -\frac {\pi^2} 2 \ln 2$
{{qed}}
Theorem: Definite Integral to Infinity of Exponential of -(a x^2 plus b x plus c)

:$\ds \int_0^\infty \map \exp {-\paren {a x^2 + b x + c} } \rd x = \frac 1 2 \sqrt {\frac \pi a} \map \exp {\frac {b^2 - 4 a c} {4 a} } \map \erfc {\frac b {2 \sqrt a} }$

Proof:
{{begin-eqn}}
{{eqn	| l = \int_0^\infty \map \exp {-\paren {a x^2 + bx + c} } \rd x
	| r = \int_0^\infty \map \exp {-a \paren {x + \frac b {2 a} }^2 + \frac {b^2} {4 a} - c} \rd x
	| c = Completing the Square
}}
{{eqn	| r = \map \exp {\frac {b^2 - 4 a c} {4 a} } \int_0^\infty \map \exp {-a \paren {x + \frac b {2 a} }^2} \rd x
	| c = Exponential of Sum
}}
{{eqn	| r = \map \exp {\frac {b^2 - 4 a c} {4 a} } \int_0^\infty \map \exp {-\paren {\sqrt a x + \frac b {2 \sqrt a} }^2} \rd x
}}
{{eqn	| r = \frac 1 {\sqrt a} \map \exp {\frac {b^2 - 4 a c} {4 a} } \int_{\frac b {2 \sqrt a} }^\infty \map \exp {-u^2} \rd u
	| c = substituting $u = \sqrt a x + \dfrac b {2 \sqrt a}$
}}
{{eqn	| r = \frac 1 2 \sqrt {\frac \pi a} \map \exp {\frac {b^2 - 4 a c} {4 a} } \paren {\frac 2 {\sqrt \pi} \int_{\frac b {2 \sqrt a} }^\infty \map \exp {-u^2} \rd u}
}}
{{eqn	| r = \frac 1 2 \sqrt {\frac \pi a} \map \exp {\frac {b^2 - 4 a c} {4 a} } \map \erfc {\frac b {2 \sqrt a} }
	| c = {{Defof|Complementary Error Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Set is Subset of Intersection of Supersets

Let $S$, $T_1$ and $T_2$ be sets.
Let $S$ be a subset of both $T_1$ and $T_2$.
Then:
:$S \subseteq T_1 \cap T_2$
That is:
:$\paren {S \subseteq T_1} \land \paren {S \subseteq T_2} \implies S \subseteq \paren {T_1 \cap T_2}$

Proof:
Let $S \subseteq T_1 \land S \subseteq T_2$.
Then:
{{begin-eqn}}
{{eqn | l = x \in S
      | o = \leadsto
      | r = x \in T_1 \land x \in T_2
      | c = {{Defof|Subset}}
}}
{{eqn | o = \leadsto
      | r = x \in T_1 \cap T_2
      | c = {{Defof|Set Intersection}}
}}
{{eqn | o = \leadsto
      | r = S \subseteq T_1 \cap T_2
      | c = {{Defof|Subset}}
}}
{{end-eqn}}
Theorem: Set is Subset of Intersection of Supersets

Let $S$, $T_1$ and $T_2$ be sets.
Let $S$ be a subset of both $T_1$ and $T_2$.
Then:
:$S \subseteq T_1 \cap T_2$
That is:
:$\paren {S \subseteq T_1} \land \paren {S \subseteq T_2} \implies S \subseteq \paren {T_1 \cap T_2}$

Proof:
{{begin-eqn}}
{{eqn | l = S
      | o = \subseteq
      | r = T_1
}}
{{eqn | lo= \land
      | l = S
      | o = \subseteq
      | r = T_2
}}
{{eqn | ll= \leadsto
      | l = S \cap S
      | o = \subseteq
      | r = S \cap T_2
      | c = Set Intersection Preserves Subsets
}}
{{eqn | ll= \leadsto
      | l = S
      | o = \subseteq
      | r = T_1 \cap T_2
      | c = Set Intersection is Idempotent
}}
{{end-eqn}}
{{Qed}}