avewright/proofwiki-math huggingface dataset:
Theorem: Cosine Function in terms of Hypergeometric Function

:$\cos x = \map { {}_0 \operatorname F_1} {\dfrac 1 2; \dfrac {-x^2} 4}$

Proof:
{{begin-eqn}}
{{eqn | l = \map { {}_0 \operatorname F_1} {\frac 1 2; \dfrac {-x^2} 4}
      | r = \sum_{n \mathop = 0}^\infty \frac 1 {\paren {\frac 1 2}^{\bar n} } \frac {\paren {\frac {-x^2} 4 }^n} {n!}
      | c = {{Defof|Generalized Hypergeometric Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {\frac 1 2 + n} } \paren {-1}^n \frac {\paren {\frac {x^2} 4 }^n} {\map \Gamma {n + 1} }
      | c = Rising Factorial as Quotient of Factorials, Gamma Function Extends Factorial
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {n + \frac 1 2} } \frac {\paren {-1}^n x^{2 n} } {2^{2 n} \map \Gamma {n + 1} }
      | c = Gamma Difference Equation, Power of Power
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {n + \frac 1 2} } \frac {\paren {-1}^n x^{2 n} } {2^{2 n - 1} \paren {2 n} \map \Gamma n }
      | c = Gamma Difference Equation
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n x^{2 n} } {\map \Gamma {2 n } \paren {2 n} }
      | c = Legendre's Duplication Formula
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n x^{2 n} } {\paren {2 n}!}
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \cos x
      | c = Power Series Expansion for Cosine Function
}}
{{end-eqn}}
{{qed}}
Theorem: Sine Function in terms of Hypergeometric Function

:$\sin x = x \paren {\map { {}_0 \operatorname F_1} {\dfrac 3 2; \dfrac {-x^2} 4} }$

Proof:
{{begin-eqn}}
{{eqn | l = x \paren {\map { {}_0 \operatorname F_1} {\frac 3 2; \dfrac {-x^2} 4} }
      | r = x \sum_{n \mathop = 0}^\infty \frac 1 {\paren {\frac 3 2}^{\bar n} } \frac {\paren {\frac {-x^2} 4 }^n} {n!}
      | c = {{Defof|Generalized Hypergeometric Function}}
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 3 2} } {\map \Gamma {\frac 3 2 + n} } \frac {\paren {-1}^n \paren {\frac {x^2} 4 }^n} {\map \Gamma {n + 1} }
      | c = Rising Factorial as Quotient of Factorials, Gamma Function Extends Factorial
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\frac 1 2 \map \Gamma {\frac 1 2} } {\map \Gamma {n + 1 + \frac 1 2} } \frac {\paren {-1}^n x^{2 n} } {2^{2 n} \map \Gamma {n + 1} }
      | c = Gamma Difference Equation, Power of Power
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {n + 1 + \frac 1 2} } \frac {\paren {-1}^n x^{2 n} } {2^{2 n + 1} \map \Gamma {n + 1} }
      | c = 
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {n + 1 + \frac 1 2} } \frac {\paren {-1}^n x^{2 n} } {2^{2 \paren {n + 1} - 1} \map \Gamma {n + 1} }
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n x^{2 n + 1} } {\map \Gamma {2 \paren {n + 1} } }
      | c = Legendre's Duplication Formula
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \sin x
      | c = Power Series Expansion for Hyperbolic Sine Function
}}
{{end-eqn}}
{{qed}}
Theorem: Continued Fraction for Tangent Function

:$\tan x = \cfrac x {1 - \cfrac {x^2} {3 - \cfrac {x^2} {5 - \cfrac {x^2} {7 - \cfrac {x^2} {9 - \cfrac {x^2} \ddots} } } } }$

Proof:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \dfrac {\sin x} {\cos x}
      | c = {{Defof|Tangent}}
}}
{{eqn | r = \frac {x \map { {}_0 \operatorname F_1} {\dfrac 3 2; \dfrac {-x^2} 4} } {\map { {}_0 \operatorname F_1} {\dfrac 1 2; \dfrac {-x^2} 4} }
      | c = Sine Function in terms of Hypergeometric Function, Cosine Function in terms of Hypergeometric Function
}}
{{eqn | r = \frac {x \map { {}_0 \operatorname F_1} {\dfrac 1 2 + 1; \dfrac {-x^2} 4} } {\map { {}_0 \operatorname F_1} {\dfrac 1 2; \dfrac {-x^2} 4} }
      | c = 
}}
{{end-eqn}}
From Hypergeometric Continued Fraction Formulation 1, we have:
:$\dfrac {\map { {}_0 \operatorname F_1} {a + 1; x} } {\map { {}_0 \operatorname F_1} {a; x} } = \cfrac a {a + \cfrac x {\paren {a + 1} + \cfrac x {\paren {a + 2} + \cfrac x {\paren {a + 3} + \cfrac x {\ddots + \cfrac \ddots \ddots} } } } }$
Therefore:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \cfrac {\dfrac x 2} {\dfrac 1 2 + \cfrac {\dfrac {-x^2} 4} {\paren {\dfrac 1 2 + 1} + \cfrac {\dfrac {-x^2} 4} {\paren {\dfrac 1 2 + 2} + \cfrac {\dfrac {-x^2} 4} {\paren {\dfrac 1 2 + 3} + \cfrac {\dfrac {-x^2} 4} {\ddots + \cfrac \ddots \ddots} } } } }
      | c = $a = \dfrac 1 2$
}}
{{eqn | r = \cfrac {\dfrac x 2 \times 2} {2 \times \dfrac 1 2 - \cfrac {\dfrac {x^2} 4 \times 2 \times 2} {2 \times \paren {\dfrac 3 2} - \cfrac {\dfrac {x^2} 4 \times 2 \times 2} {2 \times \paren {\dfrac 5 2} - \cfrac {\dfrac {x^2} 4 \times 2 \times 2} {2 \times \paren {\dfrac 7 2} - \cfrac {\dfrac {x^2} 4 \times 2 \times 2} {\ddots - \cfrac \ddots \ddots} } } } }
      | c = multiplying top and bottom by $2$ throughout
}}
{{eqn | r = \cfrac x {1 - \cfrac {x^2} {3 - \cfrac {x^2} {5 - \cfrac {x^2} {7 - \cfrac {x^2} {9 - \cfrac {x^2} \ddots} } } } }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential Function in terms of Hypergeometric Function

:$e^x = \map { {}_1 \operatorname F_1} {p; p; x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map { {}_1 \operatorname F_1} {p; p; x}
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {p}^{\bar n} } {\paren {p}^{\bar n} } \frac {x^n} {n!}
      | c = {{Defof|Generalized Hypergeometric Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}
      | c = 
}}
{{eqn | r = e^x
      | c = Power Series Expansion for Exponential Function
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential Function as Limit of Gaussian Hypergeometric Function

:$\ds e^x = \lim_{p \mathop \to \infty} \map F {1, p; 1; \dfrac x p}$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{p \mathop \to \infty} \map F {1, p; 1; \dfrac x p}
      | r = \sum_{n \mathop = 0}^\infty \lim_{p \mathop \to \infty} \frac {\paren {p}^{\overline n} 1^{\overline n} } {1^{\overline n} } \frac {\paren {\dfrac x p}^n} {n!}
      | c = {{Defof|Gaussian Hypergeometric Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \lim_{p \mathop \to \infty} \paren {p}^{\overline n} \frac {\paren {\dfrac x p}^n} {n!}
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \lim_{p \mathop \to \infty} \dfrac {\map \Gamma {p + n} } {\map \Gamma p \times p^n}  \frac {x^n} {n!}
      | c = Rising Factorial as Quotient of Factorials, Power of Quotient
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \lim_{p \mathop \to \infty} \paren {\frac p p \times \frac {p + 1} p \times \frac {p + 2} p \times \cdots \times \frac {p + n - 1} p } \frac {x^n} {n!}
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \lim_{p \mathop \to \infty} \paren {1 \times \paren {1 + \frac 1 p} \times \paren {1 + \frac 2 p} \times \cdots \times \paren {1 + \frac {n - 1} p} } \frac {x^n} {n!}
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {1 \times \paren 1 \times \paren 1 \times \cdots \times \paren 1 } \frac {x^n} {n!}
      | c = Limit of Reciprocal of x at Infinity
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}
      | c = 
}}
{{eqn | r = e^x
      | c = Power Series Expansion for Exponential Function
}}
{{end-eqn}}
{{qed}}
Theorem: Group of Rationals Modulo One Induces Equivalence Relation

Define a relation $\sim$ on $\Q$ such that:
:$\forall p, q \in \Q: p \sim q \iff p - q \in \Z$
Then $\sim$ is an equivalence relation

Proof:
{{proofread}}
From Integers under Addition form Abelian Group, $\struct {\Z, +}$ forms an abelian group.
Checking in turn each of the criteria for equivalence:
Theorem: Almost-Everywhere Equality Relation for Real-Valued Functions is Equivalence Relation

Let $\struct {X, \Sigma, \mu}$ be a measure space.
<onlyinclude>
Let $\map {\mathcal M} {X, \Sigma, \R}$ be the real-valued $\Sigma$-measurable functions on $X$. 
Let $\sim_\mu$ be the $\mu$-almost-everywhere equality relation on $\map {\mathcal M} {X, \Sigma, \R}$ by: 
:$f \sim_\mu g$ {{iff}} $\map f x = \map g x$ for $\mu$-almost all $x \in X$.
That is: 
:$\map \mu {\set {x \in X : \map f x \ne \map g x} } = 0$
Then $\sim_\mu$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Cosecant Function in terms of Gaussian Hypergeometric Function

:$\csc x = \dfrac 1 x \map F {\dfrac 1 2, \dfrac 1 2; \dfrac 3 2; \sin^2 x}$

Proof:
{{begin-eqn}}
{{eqn | l = \arcsin x
      | r = x \map F {\dfrac 1 2, \dfrac 1 2; \dfrac 3 2; x^2}
      | c = Arcsine Function in terms of Gaussian Hypergeometric Function
}}
{{eqn | ll = \leadsto
      | l = \map \arcsin {\sin x}
      | r = \sin x \map F {\dfrac 1 2, \dfrac 1 2; \dfrac 3 2; \sin^2 x}
      | c = $x \to \sin x$
}}
{{eqn | ll = \leadsto
      | l = x
      | r = \sin x \map F {\dfrac 1 2, \dfrac 1 2; \dfrac 3 2; \sin^2 x}
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \csc x 
      | r = \dfrac 1 x \map F {\dfrac 1 2, \dfrac 1 2; \dfrac 3 2; \sin^2 x}
      | c = Sine is Reciprocal of Cosecant
}}
{{end-eqn}}
{{qed}}
Theorem: Secant Function in terms of Gaussian Hypergeometric Function

:$\sec x = \map F {\dfrac 1 2, 1; 1; \sin^2 x}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {1 + x}^p
      | r = \map F {-p, 1; 1; -x}
      | c = Power of One plus x in terms of Gaussian Hypergeometric Function
}}
{{eqn | ll = \leadsto
      | l = \frac 1 {\sqrt {\paren {1 - \sin^2 x} } }
      | r = \map F {\frac 1 2, 1; 1; \sin^2 x}
      | c = $p \gets -\dfrac 1 2$ and $-x \gets \sin^2 x$
}}
{{eqn | ll = \leadsto
      | l = \frac 1 {\sqrt {\paren {\cos^2 x} } }
      | r = \map F {\frac 1 2, 1; 1; \sin^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll = \leadsto
      | l = \sec x
      | r = \map F {\frac 1 2, 1; 1; \sin^2 x}
      | c = Cosine is Reciprocal of Secant
}}
{{end-eqn}}
{{qed}}
Theorem: Almost-Everywhere Equality Relation for Lebesgue Space is Equivalence Relation

Let $\struct {X, \Sigma, \mu}$ be a measure space, and let $p \in \closedint 1 \infty$.
Let $\map {\mathcal L^p} {X, \Sigma, \mu}$ be the Lebesgue $p$-space of $\struct {X, \Sigma, \mu}$.
We define the $\mu$-almost-everywhere equality relation $\sim_\mu$ on $\map {\mathcal L^p} {X, \Sigma, \mu}$ by: 
:$\forall f, g \in \mathcal L^p: f \sim_\mu g$ {{iff}} $\norm {f - g}_p = 0$
where $\norm {\, \cdot \,}_p$ is the $p$-seminorm.
Then $\sim_\mu$ is an equivalence relation.

Proof:
Let $f, g, h \in \LL^p$.
Checking in turn each of the criteria for equivalence:
=== Reflexivity ===
From P-Seminorm of Function Zero iff A.E. Zero, we have:
:$\norm {f - f}_p = 0$
Therefore:
:$f \sim_\mu f$
Hence $\sim_\mu$ is a reflexive relation.
{{qed|lemma}}
=== Symmetry ===
Suppose:
:$f \sim_\mu g$
Then:
:$\norm {f - g}_p = 0$
Then:
:$\norm {g - f}_p = 0$
Therefore:
:$g \sim_\mu f$
Hence $\sim_\mu$ is a symmetric relation.
{{qed|lemma}}
=== Transitivity ===
Suppose:
:$f \sim_\mu g$
and:
:$g \sim_\mu h$
Then:
:$\norm {f - g}_p = 0$
and:
:$\norm {g - h}_p = 0$
Then:
:$\norm {f - h}_p = 0$
Hence $\sim_\mu$ is a transitive relation.
{{qed|lemma}}
All the criteria are therefore seen to hold for $\sim_\mu$ to be an equivalence relation.
{{qed}}
Theorem: Almost-Everywhere Equality Relation for Lebesgue Space is Equivalence Relation

Let $\struct {X, \Sigma, \mu}$ be a measure space, and let $p \in \closedint 1 \infty$.
Let $\map {\mathcal L^p} {X, \Sigma, \mu}$ be the Lebesgue $p$-space of $\struct {X, \Sigma, \mu}$.
We define the $\mu$-almost-everywhere equality relation $\sim_\mu$ on $\map {\mathcal L^p} {X, \Sigma, \mu}$ by: 
:$\forall f, g \in \mathcal L^p: f \sim_\mu g$ {{iff}} $\norm {f - g}_p = 0$
where $\norm {\, \cdot \,}_p$ is the $p$-seminorm.
Then $\sim_\mu$ is an equivalence relation.

Proof:
Let $f, g, h \in \LL^p$.
Checking in turn each of the criteria for equivalence:
=== Reflexivity ===
By Equality is Reflexive, we have:
:$f \sim_\mu f$ {{iff}} $\map f x = \map f x$ for $\mu$-almost all $x \in X$.
Therefore:
:$f \sim_\mu f$
Hence $\sim_\mu$ is a reflexive relation.
{{qed|lemma}}
=== Symmetry ===
Suppose:
:$f \sim_\mu g$
Then:
:$\map f x = \map g x$ for $\mu$-almost all $x \in X$.
Then by Equality is Symmetric
:$\map g x = \map f x$ for $\mu$-almost all $x \in X$.
Therefore:
:$g \sim_\mu f$
Hence $\sim_\mu$ is a symmetric relation.
{{qed|lemma}}
=== Transitivity ===
Suppose:
:$f \sim_\mu g$
and:
:$g \sim_\mu h$
Then:
:$\map f x = \map g x$ for $\mu$-almost all $x \in X$.
and:
:$\map g x = \map h x$ for $\mu$-almost all $x \in X$.
Then by Equality is Transitive:
:$\map f x = \map h x$ for $\mu$-almost all $x \in X$.
Hence $\sim_\mu$ is a transitive relation.
{{qed|lemma}}
All the criteria are therefore seen to hold for $\sim_\mu$ to be an equivalence relation.
{{qed}}
Theorem: Cosine Function in terms of Gaussian Hypergeometric Function

:$\map \cos x = \map F {\dfrac 1 2, -\dfrac 1 2; \dfrac 1 2; \sin^2 x}$

Proof:
{{begin-eqn}}
{{eqn | l = \paren {1 + x}^p
      | r = \map F {-p, 1; 1; -x}
      | c = Power of One plus x in terms of Gaussian Hypergeometric Function
}}
{{eqn | ll = \leadsto
      | l = \sqrt {\paren {1 - \sin^2 x} }
      | r = \map F {-\frac 1 2, 1; 1; \sin^2 x}
      | c = $p \to \frac 1 2$ and $-x \to \sin^2 x$
}}
{{eqn | ll = \leadsto
      | l = \sqrt {\paren {\cos^2 x} }
      | r = \map F {-\frac 1 2, 1; 1; \sin^2 x}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll = \leadsto
      | l = \cos x
      | r = \map F {-\frac 1 2, 1; 1; \sin^2 x}
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \cos x
      | r = \map F {\frac 1 2, -\frac 1 2; \frac 1 2; \sin^2 x}
      | c = Real Multiplication is Commutative, numerator and denominator will cancel
}}
{{end-eqn}}
{{qed}}
Theorem: Almost-Everywhere Equality Relation for Measurable Sets is Equivalence Relation

Let $\struct {X, \Sigma, \mu}$ be a measure space.
We define the $\mu$-almost-everywhere equality relation $\sim_\mu$ on $\Sigma$ by: 
:$A \sim_\mu B$ {{iff}} $\map \mu {A \symdif B} = 0$
where $\symdif$ denotes set symmetric difference.
Then:
:$\sim_\mu$ is an equivalence relation.

Proof:
Checking in turn each of the criteria for equivalence:
=== Reflexivity ===
By Symmetric Difference with Self is Empty Set, we have:
We have:
:$A \symdif A = \O$
By Measure of Empty Set is Zero:
:$\map \mu \O = 0$
So:
:$\map \mu {A \symdif A} = 0$
Therefore:
:$A \sim_\mu A$
Hence $\sim_\mu$ is a reflexive relation.
{{qed|lemma}}
=== Symmetry ===
Suppose:
:$A \sim_\mu B$
Then:
:$\map \mu {A \symdif B} = 0$
We have:
:$\map \mu {B \symdif A} = 0$
Therefore:
:$B \sim_\mu A$
Hence $\sim_\mu$ is a symmetric relation.
{{qed|lemma}}
=== Transitivity ===
Suppose:
:$A \sim_\mu B$
and:
:$B \sim_\mu C$
Then:
:$\map \mu {A \symdif B} = 0$
And:
:$\map \mu {B \symdif C} = 0$
Therefore:
:$\map \mu {A \symdif C} = 0$
Hence $\sim_\mu$ is a transitive relation.
{{qed|lemma}}
All the criteria are therefore seen to hold for $\sim_\mu$ to be an equivalence relation.
{{qed}}
Theorem: Space of Integrable Functions Under Pointwise Addition forms Abelian Group

Let $\struct {X, \Sigma, \mu}$ be a measure space.
Let $\map {\LL^1} \mu$ be the space of real-valued $\mu$-integrable functions.
Then $\map {\LL^1} \mu$, endowed with pointwise addition, forms an abelian group over $\map {\LL^1} \mu$.

Proof:
Suppose $f, g \in \map {\LL^1} \mu$.
By Pointwise Sum of Integrable Functions is Integrable Function:
:$f + g \in \map {\LL^1} \mu$
So $\map {\LL^1} \mu$ is closed under pointwise addition.
{{finish}}
Hence the result.
{{qed}}
Theorem: Adjacency Matrix for Undirected Graph is Symmetric

Let $G$ be an undirected graph.
The adjacency matrix for $G$ is a symmetric matrix.

Proof:
{{MissingLinks}}
{{tidy}}
Let $G = \struct {V, E}$ be an undirected graph and $M$ its adjacency matrix.
We will show that $M_{ij} = M_{ji}$.
Let $v_i, v_j \in V$ be vertices on $G$.
;Case 1:  $v_i v_j \in E$
It follows from the definition of adjacency matrix that $M_{ij} = 1$.
It follows from the definition of undirected graph that if $v_i v_j \in E$ then $v_j v_i \in E$, then $M_{ji} = 1 = M_{ij}$
;Case 2: $v_i v_j \notin E$
It follows from the definition of adjacency matrix that $M_{ij} = 0$.
Suppose that $v_j v_i \in E$, then by the definition of undirected graph we have that $v_i v_j \in E$, this is a contradiction, then if $v_i v_j \notin E$ then $v_j v_i \notin E$.
It follows from the definition of adjacency matrix that $M_{ji} = 0 = M_{ij}$.
Therefore, $M_{ij} = M_{ji}$ in any situation.
{{qed}}
Theorem: Logarithm of One plus x over One minus x in terms of Gaussian Hypergeometric Function

:$\map \ln {\dfrac {1 + x} {1 - x} } = 2 x \map F {\dfrac 1 2, 1; \dfrac 3 2; x^2}$

Proof:
{{begin-eqn}}
{{eqn | l = 2 x \map F {\dfrac 1 2, 1; \dfrac 3 2; x^2}
      | r = 2 x \sum_{n \mathop = 0}^\infty \frac {\paren {\frac 1 2}^{\bar n} \paren {1}^{\bar n} } {\paren {\frac 3 2}^{\bar n} } \frac {\paren {x^2}^n } {n!}
      | c = {{Defof|Gaussian Hypergeometric Function}}
}}
{{eqn | r = 2 x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2 + n} \map \Gamma {1 + n} \map \Gamma {\frac 3 2} } {\map \Gamma {\frac 1 2} \map \Gamma 1 \map \Gamma {\frac 3 2 + n} } \frac {x^{2 n} } {\map \Gamma {1 + n} }
      | c = Rising Factorial as Quotient of Factorials, One to Integer Rising is Integer Factorial, Gamma Function Extends Factorial
}}
{{eqn | r = 2 x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2 + n} \frac 1 2 \map \Gamma {\frac 1 2} } {\map \Gamma {\frac 1 2} \paren {\frac 1 2 + n} \map \Gamma {\frac 1 2 + n} } x^{2 n}
      | c = Gamma Difference Equation, $\map \Gamma {1 + n}$ cancels
}}
{{eqn | r = 2 \sum_{n \mathop = 0}^\infty \frac {x^{2 n + 1} } {\paren {2 n + 1} }
      | c = Product of Powers
}}
{{eqn | r = \map \ln {\dfrac {1 + x} {1 - x} }
      | c = Power Series Expansion for $\dfrac {\map \ln {1 + x} } {\map \ln {1 - x} }$
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Affine Hull

Let $S$ be a set.
{{TFAE|def = Affine Hull}}

Proof:
=== Definition $(1)$ implies Definition $(2)$ ===
Let $\HH$ be the affine hull of $S$ by definition $1$.
{{Recall|Affine Hull|index = 1}}
{{:Definition:Affine Hull/Definition 1}}
{{finish}}
Thus $\HH$ is the affine hull of $S$ by definition $2$.
{{qed|lemma}}
Theorem: Arccosine Function in terms of Gaussian Hypergeometric Function

:$\arccos x = 2 \sqrt {\dfrac {1 - x} 2} \map F {\dfrac 1 2, \dfrac 1 2; \dfrac 3 2; \dfrac {1 - x} 2}$

Proof:
{{begin-eqn}}
{{eqn | l = u
      | r = \map \arcsin {\sin u}
      | c = 
}}
{{eqn | r = \sin u \map F {\frac 1 2, \frac 1 2; \frac 3 2; \sin^2 u}
      | c = Arcsine Function in terms of Gaussian Hypergeometric Function
}}
{{eqn | r = \sqrt {\dfrac {1 - \map \cos {2 u} } 2} \map F {\frac 1 2, \frac 1 2; \frac 3 2; \dfrac {1 - \map \cos {2 u} } 2}
      | c = Double Angle Formula for Cosine Corollary 5
}}
{{eqn | ll = \leadsto
      | l = \dfrac 1 2 \map \arccos {\map \cos {2 u} }
      | r = \sqrt {\dfrac {1 - x} 2} \map F {\dfrac 1 2, \dfrac 1 2; \dfrac 3 2; \dfrac {1 - x} 2}
      | c = Letting $\map \cos {2 u} = x$, and $u = \dfrac 1 2 \map \arccos {\map \cos {2 u} }$
}}
{{eqn | ll = \leadsto
      | l = \arccos x
      | r = 2 \sqrt {\dfrac {1 - x} 2} \map F {\dfrac 1 2, \dfrac 1 2; \dfrac 3 2; \dfrac {1 - x} 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Area of Right Parabolic Segment

Let $ABC$ be a right parabolic segment where:
:$AB$ is the defining chord $\LL$ of $ABC$
:$C$ is the vertex of the defining parabola $\PP$ of $ABC$.
:480px
The area $\AA$ of $ABC$ is given by:
:$\AA = \dfrac {2 a b} 3$
where:
:$a$ is the length of the line segment $CF$, where $F$ is the point at which the axis of $\PP$ intersects $AB$
:$b$ is the length of the line segment $AB$.

Proof:
Construct the triangle $\triangle ABC$:
:480px
From Quadrature of Parabola:
:$\AA = \dfrac 4 3 \triangle ABC$
From Area of Triangle in Terms of Side and Altitude, the area of $\triangle ABC$ equals $\dfrac {a b} 2$.
The result follows.
{{qed}}
Theorem: Logarithmic Approximation of Error Term of Stirling's Formula for Gamma Function/Lemma 1

:If $\size {\arg z} \le \dfrac \pi 4 $, then $K_z = 1$

Proof:
{{begin-eqn}}
{{eqn | l = K_z
      | r = \map \sup {\size {\dfrac {z^2} {u^2 + z^2} } }
      | c = 
}}
{{eqn | r = \map \sup {\size {\dfrac {\paren {\cmod z e^{i \size {\arg z} } }^2 } {u^2 + \paren {\cmod z e^{i \size {\arg z} } }^2} } }
      | c = 
}}
{{eqn | r = \map \sup {\size {\dfrac {\cmod z^2 e^{i 2 \size {\arg z} } } {u^2 + \cmod z^2 e^{i 2 \size {\arg z} } } } }
      | c = 
}}
{{eqn | r = \map \sup {\size {\dfrac {\cmod z^2 \paren {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } } {u^2 + \cmod z^2 \paren {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } } } }
      | c = $\size {\arg z} \le \dfrac \pi 4 $ implies $\map \cos {2 \size {\arg z} } \ge 0$, (i.e real part $\map \Re {z^2}$ is positive)
}}
{{eqn | r = \size {\dfrac {\cmod z^2 \paren {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } } {0^2 + \cmod z^2 \paren {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } } }
      | c = 
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Logarithmic Approximation of Error Term of Stirling's Formula for Gamma Function
4o00501113ob7o18ua6e10wg9g5h4tx
Theorem: Logarithmic Approximation of Error Term of Stirling's Formula for Gamma Function/Lemma 2

:If $\dfrac \pi 4 < \size {\arg z} < \dfrac \pi 2 $, then $K_z = \map \csc {2 \size {\arg z} }$

Proof:
{{begin-eqn}}
{{eqn | l = K_z
      | r = \map \sup {\size {\dfrac {z^2} {u^2 + z^2} } }
      | c = 
}}
{{eqn | r = \map \sup {\size {\dfrac {\cmod z^2 \paren {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } } {u^2 + \cmod z^2 \paren {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } } } }
      | c = as $\dfrac \pi 4 < \size {\arg z} < \dfrac \pi 2 $ implies $\map \cos {2 \size {\arg z} } < 0$ (that is, real part $\map \Re {z^2}$ is negative)
}}
{{eqn | r = \map \sup {\size {\dfrac {\cmod z^2 \paren {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } } {-\cmod z^2 \map \cos {2 \size {\arg z} } + \cmod z^2 \paren {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } } } }
      | c = setting $u^2 = -\cmod z^2 \map \cos {2 \size {\arg z} }$ to minimize the denominator to maximize the ratio
}}
{{eqn | r = \cmod {\dfrac {\map \cos {2 \size {\arg z} } + i \map \sin {2 \size {\arg z} } } {i \map \sin {2 \size {\arg z} } } }
      | c = 
}}
{{eqn | r = \cmod {1 + \dfrac {\map \cos {2 \size {\arg z} } } {i \map \sin {2 \size {\arg z} } } }
      | c = 
}}
{{eqn | r = \cmod {1 + \dfrac {\map \cos {2 \size {\arg z} } } {i \map \sin {2 \size {\arg z} } } \times \dfrac i i}
      | c = multiplying top and bottom by $i$
}}
{{eqn | r = \cmod {1 - i \dfrac {\map \cos {2 \size {\arg z} } } {\map \sin {2 \size {\arg z} } } }
      | c = $i^2 = -1$
}}
{{eqn | r = \cmod {1 - i \map \cot {2 \size {\arg z} } }
      | c = {{Defof|Complex Cotangent Function}}
}}
{{eqn | r = \sqrt {1^2 + \paren {\map \cot {2 \size {\arg z} } }^2 }
      | c = {{Defof|Complex Modulus}}
}}
{{eqn | r = \sqrt {\paren {\map \csc {2 \size {\arg z} } }^2 }
      | c = {{Corollary|Sum of Squares of Sine and Cosine|2}}
}}
{{eqn | r = \map \csc {2 \size {\arg z} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Logarithmic Approximation of Error Term of Stirling's Formula for Gamma Function
qv48l6ja8oc8y8jivz41zgaf66bj242
Theorem: Volume of Circular Cylinder/Height

Let $\CC$ be a circular cylinder such that:
:the bases of $\CC$ are circles of radius $r$
:the height of $\CC$ is $h$.
The volume $\VV$ of $\CC$ is given by the formula:
:$\VV = \pi r^2 h$

Proof:
From Volume of Cylinder in terms of Height and Base Area:
:$\VV = \AA h$
where $\AA$ is the area of the base of $\CC$.
From Area of Circle:
:$\AA = \pi r^2$
The result follows.
{{qed}}