avewright/proofwiki-math huggingface dataset:
Theorem: Complex Exponential Function is Entire

Let $\exp: \C \to \C$ be the complex exponential function. 
Then $\exp$ is entire.

Proof:
By the definition of the complex exponential function, $\exp$ admits a power series expansion about $0$: 
:$\ds \exp z = \sum_{n \mathop = 0}^\infty \frac {z^n} {n!}$
By Complex Function is Entire iff it has Everywhere Convergent Power Series, to show that $\exp$ is entire it suffices to show that this series is everywhere convergent.
Note that this power series is of the form: 
:$\ds \sum_{n \mathop = 0}^\infty \frac {\paren {z - \xi}^n} {n!}$
with $\xi = 0$. 
Therefore, by Radius of Convergence of Power Series over Factorial: Complex Case, we have that the former power series is everywhere convergent. 
Hence the result.
{{qed}}
Theorem: Complex Cosine Function is Entire

Let $\cos: \C \to \C$ be the complex cosine function. 
Then $\cos$ is entire.

Proof:
By the definition of the complex cosine function, $\cos$ admits a power series expansion about $0$: 
:$\ds \cos z = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {z^{2 n} } {\paren {2 n}!}$
By Complex Function is Entire iff it has Everywhere Convergent Power Series, to show that $\cos$ is entire it suffices to show that this series is everywhere convergent.
From Radius of Convergence from Limit of Sequence: Complex Case, it is sufficient to show that: 
:$\ds \lim_{n \mathop \to \infty} \size {\frac {\paren {-1}^{n + 1} } {\paren {2 n + 2}!} \times \frac {\paren {2 n}!} {\paren {-1}^n} } = 0$
We have: 
{{begin-eqn}}
{{eqn	| l = \lim_{n \mathop \to \infty} \size {\frac {\paren {-1}^{n + 1} } {\paren {2 n + 2}!} \times \frac {\paren {2 n}!} {\paren {-1}^n} }
	| r = \size {-1} \lim_{n \mathop \to \infty} \size {\frac {\paren {2 n}!} {\paren {2 n + 2} \paren {2 n + 1} \paren {2 n}!} }
	| c = {{Defof|Factorial}}
}}
{{eqn	| r = \lim_{n \mathop \to \infty} \paren {\frac 1 {\paren {2 n + 2} \paren {2 n + 1} } }
}}
{{eqn	| r = 0
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Complex Cosine Function is Entire

Let $\cos: \C \to \C$ be the complex cosine function. 
Then $\cos$ is entire.

Proof:
Let: 
{{begin-eqn}}
{{eqn | l = \map f z
      | r = \exp z
}}
{{eqn | l = \map g z
      | r = i z
}}
{{eqn | l = \map h z
      | r = -i z
}}
{{end-eqn}}
for all $z \in \C$. 
By Complex Exponential Function is Entire, we have that $f$ is entire. 
By Polynomial is Entire, we have that $g$ and $h$ are entire. 
Therefore, by Composition of Entire Functions is Entire, we have that both $f \circ g$ and $f \circ h$ are entire.
By Linear Combination of Entire Functions is Entire, we then have that: 
:$\dfrac 1 2 \paren {f \circ g + f \circ h}$
is entire.
Then: 
{{begin-eqn}}
{{eqn | l = \frac 1 2 \paren {\map {\paren {f \circ g} } z + \map {\paren {f \circ h} } z}
      | r = \frac 1 2 \paren {\map \exp {i z} + \map \exp {-i z} }
}}
{{eqn | r = \cos z
      | c = Euler's Cosine Identity
}}
{{end-eqn}}
Therefore $\cos$ is an entire function.
{{qed}}
Theorem: Arccosecant Logarithmic Formulation

Let $x$ be a real number. 
Let $x \in \hointl {-\infty} {-1} \cup \hointr 1 {\infty}$.
Then: 
:$\arccsc x = -i \map \Ln {\sqrt {1 - \dfrac 1 {x^2} } + \dfrac i x}$
where:
:$\arccsc$ is the arccosecant function
:$\Ln$ is the principal branch of the complex logarithm whose imaginary part lies in $\hointl {-\pi} \pi$.

Proof:
{{begin-eqn}}
{{eqn | l = \arccsc x
      | r = \map \arcsin {\frac 1 x}
      | c = Arccosecant of Reciprocal equals Arcsine
}}
{{eqn | r = -i \map \Ln {\sqrt {1 - \paren {\frac 1 x}^2} + i \times \frac 1 x}
      | c = Arcsine Logarithmic Formulation
}}
{{eqn | r = -i \map \Ln {\sqrt {1 - \frac 1 {x^2} } + \frac i x}
}}
{{end-eqn}}
{{qed}}
Theorem: Arcsecant Logarithmic Formulation

Let $x$ be a real number. 
Let $x \in \hointl \gets {-1} \cup \hointr 1 \to$.
Then: 
:$\ds \arcsec x = -i \map \Ln {i \sqrt {1 - \frac 1 {x^2} } + \frac 1 x}$
where:
:$\arcsec$ is the arcsecant function
:$\Ln$ is the principal branch of the complex logarithm whose imaginary part lies in $\hointl {-\pi} \pi$.

Proof:
{{begin-eqn}}
{{eqn	| l = \arcsec x 
	| r = \map \arccos {\frac 1 x}
	| c = Arcsecant of Reciprocal equals Arccosine
}}
{{eqn	| r = -i \map \Ln {i \sqrt {1 - \paren {\frac 1 x}^2} + \frac 1 x}
	| c = Arccosine Logarithmic Formulation
}}
{{eqn	| r = -i \map \Ln {i \sqrt {1 - \frac 1 {x^2} } + \frac 1 x}
}}
{{end-eqn}}
{{qed}}
Theorem: Nontrivial Zeroes of Riemann Zeta Function are Symmetrical with respect to Critical Line

The nontrivial zeroes of the Riemann $\zeta$ function are distributed symmetrically {{WRT}} the  critical line.
That is, suppose $s_1 = \sigma_1 + i t$ is a nontrivial zero of $\map \zeta s$.
Then there exists another nontrivial zero $s_2$ of $\map \zeta s$ such that:
:$s_2 = 1 - s_1$

Proof:
From Functional Equation for Riemann Zeta Function, we have:
:$\ds \pi^{-s/2} \map \Gamma {\dfrac s 2} \map \zeta s = \pi^{\paren {s/2 - 1/2 } } \map \Gamma {\dfrac {1 - s} 2} \map \zeta {1 - s}$
We suppose $s_1 = \sigma_1 + i t$ is a nontrivial zero of $\map \zeta s$.
Then we have:
{{begin-eqn}}
{{eqn | l = \map \zeta {s_1}
      | r = 0
      | c = 
}}
{{eqn | l = \pi^{-s_1/2 } \map \Gamma {\dfrac {s_1} 2} \map \zeta {s_1}
      | r = 0
      | c = {{LHS}}
}}
{{eqn | l = \pi^{\paren {s_1/2 - 1/2 } } \map \Gamma {\dfrac {1 - s_1} 2} \map \zeta {1 - s_1}
      | r = 0
      | c = {{RHS}}
}}
{{end-eqn}}
It remains to be shown that of the three terms on the {{RHS}}, $\map \zeta {1 - s_1}$ MUST equal zero.
We can rewrite the first term in terms of the exponential function
:$\ds \pi^{\paren {s_1 / 2 - 1 / 2} } = \map \exp {\map \ln {\pi^{\paren {s_1 / 2 - 1 / 2} } } }$
From the definition of the exponential function, we know $\map \exp {\map \ln {\pi^{\paren { {s_1}/2 - 1/2 } } }}$ never equals zero.
From Zeroes of Gamma Function, we know $\map \Gamma {\dfrac {1 - s_1} 2}$ never equals zero.
Therefore:
:$\map \zeta {1 - s_1} = 0$
{{qed}}
Theorem: Prime-Counting Function in terms of Eulerian Logarithmic Integral/Riemann Hypothesis Holds

If the Riemann Hypothesis holds, then:
:$\map \pi x = \map \Li x + \map \OO {\sqrt x \ln x}$

Proof:
{{tidy}}
{{MissingLinks}}
{{refactor|level = medium|Usual exercise}}
Let $x$ denote a real number.
Let $n$ denote a natural number.
Let $p$ denote a prime number.
Let $\map \li x$ denote the  logarithmic integral.
{{refactor|level = medium|These definitions are to be removed from here and referenced to their definition pages}}
Theorem: Mertens' Third Theorem

:$\ds \lim_{x \mathop \to \infty} \ln x \prod_{\substack {p \mathop \le x \\ \text {$p$ prime} } } \paren {1 - \dfrac 1 p} = e^{-\gamma}$
where $\gamma$ denotes the Euler-Mascheroni constant.

Proof:
{{ProofWanted}}
{{Namedfor|Franz Mertens|cat = Mertens}}
Theorem: Abi-Khuzam Inequality

Let $\triangle ABC$ be a triangle.
Then:
:$\sin A \cdot \sin B \cdot \sin C \le k A \cdot B \cdot C$
where:
:$A, B, C$ are measured in radians
:$k = \paren {\dfrac {3 \sqrt 3} {2 \pi} }^3 \approx 0 \cdotp 56559 \, 56245 \ldots$

Proof:
{{tidy}}
{{MissingLinks}}
For $0 < \alpha_i < \pi, \alpha_1 + \alpha_2 + \alpha_3 = \pi$ we consider the function:
:$\map F {\alpha_1, \alpha_2, \alpha_3} =  \dfrac {\sin \alpha_1 \sin \alpha_2 \sin \alpha_3} {\alpha_1 \alpha_2 \alpha_3}$
$F$ is defined on the region $G$ in the $\tuple {\alpha_1, \alpha_2, \alpha_3}$-space consisting of the points inside the triangle with the vertices:
{{begin-eqn}}
{{eqn | l = P_1
      | o = :=
      | r = \tuple {\pi, 0, 0}
      | c = 
}}
{{eqn | l = P_2
      | o = :=
      | r = \tuple {0, \pi, 0}
      | c = 
}}
{{eqn | l = P_3
      | o = :=
      | r = \tuple {0, 0, \pi}
      | c = 
}}
{{end-eqn}}
We define $F$ on the boundary of the triangle by:
:$\map F {0, \alpha_2, \alpha_3} = \dfrac {\sin \alpha_2 \sin \alpha_3} {\alpha_2 \alpha_3}, \alpha_2 \neq 0, \alpha_3 \neq 0, \alpha_2 + \alpha_3 = \pi$
and analogously:
:$\map F {\alpha_1, 0, \alpha_3}$ and $\map F{\alpha_1, \alpha_2, 0}$
furthermore:
:$\map F {\pi, 0, 0} = \map F {0, \pi, 0} = \map F {0, 0, \pi} = 0$
$F$ is now defined on a closed region $\bar G$; it is continuous and differentiable on $\bar G$.
Moreover, as $0 \le F < 1$ there is (at least) one point in $\bar G$ where $F$ has its maximum value.
By the usual procedure, in view of $\alpha_1 + \alpha_2 + \alpha_3 = \pi$, a maximum satisfies:
{{begin-eqn}}
{{eqn | n = 6
      | l = \frac {\partial F} {\partial \alpha_1}
      | r = \frac {\partial F} {\partial \alpha_2}
      | rr= = \frac {\partial F} {\partial \alpha_3} \paren {= \lambda}
}}
{{end-eqn}}
In $G$ we have:
:$\ds \frac {\partial F} {\partial \alpha_1} = \frac {\sin \alpha_2 \sin \alpha_3} {\alpha_2 \alpha_3} \cdot \frac {\alpha_1 \cos \alpha_1 - \sin \alpha_1} {\alpha_1^2} = \map F {\cot \alpha_1 - \alpha_1^{-1} }$
and, as $F \ne 0$, $(6)$ implies:
{{begin-eqn}}
{{eqn | n = 7
      | l = \cot \alpha_1 - \alpha_1^{-1}
      | r = \cot \alpha_2 - \alpha_2^{-1}
      | rr= = \cot \alpha_3 - \alpha_3^{-1}
}}
{{end-eqn}}
For $f = \cot \alpha - \alpha^{-1}$ we obtain:
:$f' = -\sin^{-2} \alpha + \alpha^{-2} < 0$
$f$ is therefore a decreasing function of $\alpha$ (we have $0 > f > -\infty$)
hence $(7)$ implies
:$\ds \alpha_1 = \alpha_2 = \alpha_3 (= \pi / 3)$
in this point we have $F = k$.
We must verify whether larger values appear on the boundary of $\bar G$.
Between $P_2$ and $P_3$ yields
:$\ds F = \frac {\sin \alpha_2 \sin \alpha_3} {\alpha_2 \alpha_3}, \alpha_2 + \alpha_3 = \pi$
and by an argument analogous to the former, but now with two factors instead of three, it follows that for the maximum on $P_2 P_3$ we have $\alpha_2 = \alpha_3 = \pi / 2$ and $F = 4 / \pi^2$, that is less than $k$.
Hence $F \le k$ on $\bar G$, which concludes the proof.
{{qed}}
{{Namedfor|Faruk Fuad Abi-Khuzam|cat = Abi-Khuzam}}
Theorem: Yff's Conjecture

Let $\triangle ABC$ be a triangle.
Let $\omega$ be the Brocard angle of $\triangle ABC$.
Then:
:$8 \omega^3 < ABC$
where $A, B, C$ are measured in radians.

Proof:
The Abi-Khuzam Inequality states that
:$\sin A \cdot \sin B \cdot \sin C \le  \paren {\dfrac {3 \sqrt 3} {2 \pi} }^3 A \cdot B \cdot C$
The maximum value of $A B C - 8 \omega^3$ occurs when two of the angles are equal.
So taking $A = B$, and using $A + B + C = \pi$, the maximum occurs at the maximum of:
:$\map f A = A^2 \paren {\pi - 2 A} - 8 \paren {\map \arccot {2 \cot A - \cot 2 A} }^3$ 	
which occurs when:
:$2 A \paren {\pi - 3 A} - \dfrac {48 \paren {\map \arccot {\frac 1 2 \paren {3 \cot A + \tan A} } }^2 \paren {1 + 2 \cos 2 A} } {5 + 4 \cos 2 A} = 0$
{{finish|Needs expanding and completing}}
Theorem: Limit to Infinity of x minus Gamma of Reciprocal of x

thumbright600px
:$\ds \lim_{x \mathop \to \infty} \paren {x - \map \Gamma {\dfrac 1 x} } = \gamma$
where:
:$\Gamma$ denotes the $\Gamma$ (Gamma) function
:$\gamma$ denotes the Euler-Mascheroni constant.

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to \infty} \paren {x - \map \Gamma {\frac 1 x} }
      | r = \lim_{x \mathop \to 0} \paren {\frac 1 x - \map \Gamma x}
}}
{{eqn | r = \lim_{x \mathop \to 0} \paren {\frac 1 x - \frac {\map \Gamma {x + 1} } x}
      | c = Gamma Difference Equation
}}
{{eqn | r = \lim_{x \mathop \to 0} \paren {\frac {\map \Gamma 1 - \map \Gamma {1 + x} } x}
      | c = $\map \Gamma 1 = 1$ as Gamma Function Extends Factorial
}}
{{eqn | r = -\map {\Gamma'} 1
      | c = Definition of Derivative
}}
{{eqn | r = \gamma
      | c = Derivative of Gamma Function at 1
}}
{{end-eqn}}
{{qed}}
Theorem: Jung's Theorem

Let $S \subseteq \R^n$ be a compact subspace of an $n$-dimensional (real) Euclidean space.
Let $d = \ds \max_{x, y \mathop \in S} \map d {x, y}$ be the diameter of $S$.
Then there exists a closed ball ${B_r}^-$ with radius $r$ such that:
:$r = d \sqrt {\dfrac n {2 \paren {n + 1} } }$
such that $S \subseteq {B_r}^-$.

Proof:
{{ProofWanted}}
{{Namedfor|Heinrich Wilhelm Ewald Jung|cat = Jung}}
Theorem: Jung's Theorem in the Plane

Let $S \subseteq \R^2$ be a compact region in a Euclidean plane.
Let $d$ be the diameter of $S$.
Then there exists a circle $C$ with radius $r$ such that:
:$r = d \dfrac {\sqrt 3} 3$
such that $S \subseteq C$.

Proof:
This is an instance of Jung's Theorem, setting $n = 2$.
{{qed}}
{{Namedfor|Heinrich Wilhelm Ewald Jung}}
Theorem: Reciprocal of One minus x in terms of Gaussian Hypergeometric Function

:$\dfrac 1 {1 - x} = \map F {1, p; p; x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map F {1, p; p; x}
      | r = \sum_{n \mathop = 0}^\infty \frac {1^{\bar n} p^{\bar n} } {p^{\bar n} } \frac {x^n} {n!}
      | c = {{Defof|Gaussian Hypergeometric Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty n! \frac {x^n} {n!}
      | c = One to Integer Rising is Integer Factorial
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty x^n
}}
{{eqn | r = \frac 1 {1 - x}
      | c = Sum of Infinite Geometric Sequence, justified as $\size x < 1$
}}
{{end-eqn}}
{{qed}}
Theorem: Arctangent Function in terms of Gaussian Hypergeometric Function

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

Proof:
{{begin-eqn}}
{{eqn | l = x \map F {\frac 1 2, 1; \frac 3 2; -x^2}
      | r = x \sum_{n \mathop = 0}^\infty \frac {\paren {\frac 1 2}^{\bar n} 1^{\bar n} } {\paren {\frac 3 2}^{\bar n} } \frac {\paren {-x^2}^n} {n!}
      | c = {{Defof|Gaussian Hypergeometric Function}}
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2 + n} } {\map \Gamma {\frac 1 2} } \times \frac {\map \Gamma {\frac 3 2} } {\map \Gamma {\frac 3 2 + n} } n! \frac {\paren {-x^2}^n} {n!}
      | c = Rising Factorial as Quotient of Factorials, One to Integer Rising is Integer Factorial
}}
{{eqn | r = x \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2 + n} } {\map \Gamma {\frac 1 2 + n} } \times \frac {\map \Gamma {\frac 1 2} } {\map \Gamma {\frac 1 2} } \times \frac 1 {2 \paren {n + \frac 1 2} } \paren {-1}^n x^{2 n}
      | c = Gamma Difference Equation
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {2 n + 1} 
}}
{{eqn | r = \arctan x
      | c = Power Series Expansion for Real Arctangent Function
}}
{{end-eqn}}
{{qed}}
Theorem: Alternating Sum and Difference of Factorials to Infinity

According to {{AuthorRef|Leonhard Paul Euler}}:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 0}^\infty \paren {-1}^n n!
      | r = \int_0^\infty \dfrac {e^{-u} } {1 + u} \rd u
      | c = 
}}
{{eqn | r = 0! - 1! + 2! - 3! + 4! - 5! + \cdots
      | c = 
}}
{{eqn | r = G
      | c = the Euler-Gompertz constant
}}
{{eqn | o = \approx
      | r = 0 \cdotp 59634 \, 73623 \, 23194 \, 07434 \, 10784 \, 99369 \, 27937 \, 6074 \ldots
      | c = 
}}
{{end-eqn}}
{{explain|Clarify meaning of this equality. We need to add Borel transforms to {{ProofWiki}}. Here, we are doing a Borel transform and then a Laplace transform }}

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 0}^\infty \paren {-1}^n n!
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \map \Gamma {n + 1}
      | c = Gamma Function Extends Factorial
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \int_0^{\to \infty} u^{\paren {n + 1} - 1} e^{-u} \rd u
      | c = {{Defof|Gamma Function/Integral Form}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \int_0^{\to \infty} u^n e^{-u} \rd u
      | c = 
}}
{{eqn | r = \int_0^{\to \infty} \sum_{n \mathop = 0}^\infty \paren {-u}^n e^{-u} \rd u
      | c = interchange of sum and integral is valid by Fubini's Theorem
}}
{{eqn | r = \int_0^\infty \dfrac {e^{-u} } {1 + u} \rd u
      | c = Sum of Infinite Geometric Sequence
}}
{{end-eqn}}
Theorem: Arcsine Function in terms of Gaussian Hypergeometric Function

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

Proof:
{{begin-eqn}}
{{eqn | l = x \map F {\frac 1 2, \frac 1 2; \frac 3 2; x^2}
      | r = x \sum_{n \mathop = 0}^\infty \frac {\paren {\paren {\frac 1 2}^{\bar n} }^2} {\paren {\frac 3 2}^{\bar n} } \frac {x^{2 n} } {n!}
      | c = {{Defof|Gaussian Hypergeometric Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {\map \Gamma {\frac 1 2 + n} }^2 \map \Gamma {\frac 3 2} } {\paren {\map \Gamma {\frac 1 2} }^2 \map \Gamma {\frac 3 2 + n} } \frac {x^{2 n + 1} } {n!}
      | c = Rising Factorial as Quotient of Factorials
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {\map \Gamma {\frac 1 2 + n} }^2 \map \Gamma {\frac 1 2} } {2 \paren {\map \Gamma {\frac 1 2} }^2 \paren {\frac 1 2 + n} \map \Gamma {\frac 1 2 + n} } \frac {x^{2 n + 1} } {n!}
      | c = Gamma Difference Equation
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\map \Gamma {\frac 1 2 + n} } {\paren {2 n + 1} \sqrt \pi} \frac {x^{2 n + 1} } {n!}
      | c = Gamma Function of One Half
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\paren {\frac {\paren {2 n}!} {2^{2 n} n!} \sqrt \pi} \times \frac 1 {\paren {2 n + 1} \sqrt \pi} \times \frac 1 {n!} x^{2 n + 1} }
      | c = Gamma Function of Positive Half-Integer
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {2 n}!} {2^{2 n} \paren {n!}^2} \frac {x^{2 n + 1} } {2 n + 1}
}}
{{eqn | r = \arcsin x
      | c = Power Series Expansion for Real Arcsine Function
}}
{{end-eqn}}
{{qed}}
Theorem: Rational Number Expressible as Sum of Reciprocals of Distinct Squares

Let $x$ be a rational number such that $0 < x < \dfrac {\pi^2} 6 - 1$.
Then $x$ can be expressed as the sum of a finite number of reciprocals of distinct squares.

Proof:
That no rational number such that $x \ge \dfrac {\pi^2} 6 - 1$ can be so expressed follows from Riemann Zeta Function of 2:
:$\ds \sum_{n \mathop = 1}^n \dfrac 1 {n^2} = 1 + \dfrac 1 {2^2} + \dfrac 1 {3^2} + \dotsb = \dfrac {\pi^2} 6$
That is, using ''all'' the  reciprocals of distinct squares, you can never get as high as $\dfrac {\pi^2} 6 - 1$.
It remains to be shown that for all rational numbers $x$ less than $\dfrac {\pi^2} 6 - 1$, you can make $x$ with a subset of them.
{{ProofWanted}}
Theorem: Recursion Property of Elementary Symmetric Function

Let $\set {z_1, z_2, \ldots, z_{n + 1} }$ be a set of $n + 1$ numbers, duplicate values permitted.
Then for $1 \le m \le n$:
:$\map {e_m} {\set {z_1, \ldots, z_n, z_{n + 1} } } = z_{n + 1} \map {e_{m - 1} } {\set {z_1, \ldots, z_n} } + \map {e_m} {\set {z_1, \ldots, z_n} }$

Proof:
Recall the definition of elementary symmetric function:
{{begin-eqn}}
{{eqn | l = \map {e_m} {\set {z_1, z_2, \ldots, z_n} }
      | r = \sum_{1 \mathop \le j_1 \mathop < j_2 \mathop < \mathop \cdots \mathop < j_m \mathop \le n} \paren {\prod_{i \mathop = 1}^m z_{j_i} }
      | c = 
}}
{{eqn | r = \sum_{1 \mathop \le j_1 \mathop < j_2 \mathop < \mathop \cdots \mathop < j_m \mathop \le n} z_{j_1} z_{j_2} \cdots z_{j_m}
      | c = 
}}
{{end-eqn}}
Consider the summands of $\map {e_m} {\set {z_1, z_2, \ldots, z_n, z_{n + 1} } }$:
:$z_{j_1} z_{j_2} \cdots z_{j_m}$
where $1 \le j_1 < j_2 < \cdots j_m \le n + 1$.
They consist of $2$ types:
:Type $(1)$: such that $j_m < n + 1$
:Type $(2)$: such that $j_m = n + 1$.
We have that:
:the summands of Type $(1)$ are exactly the summands of $\map {e_m} {\set {z_1, z_2, \ldots, z_n} }$
:the summands of Type $(2)$ consist of the summands of $\map {e_{m - 1} } {\set {z_1, z_2, \ldots, z_n} }$ multiplied by $z_{n + 1}$.
Hence the result.
{{qed}}
Theorem: Uniform Matroid is Matroid

Let $S$ be a finite set of cardinality $n$.
Let $0 \le k \le n$.
Let $U_{k, n} = \struct{S, \mathscr I}$ be the uniform matroid of rank $k$.
Then $U_{k, n}$ is a matroid.

Proof:
It needs to be shown that $\mathscr I$ satisfies the matroid axioms $(I1)$, $(I2)$ and $(I3)$.
Theorem: Free Matroid is Matroid

Let $S$ be a finite set.
Let $\struct {S, \powerset S}$ be the free matroid of $S$.
Then $\struct {S, \powerset S}$ is a matroid.

Proof:
Let $S$ have cardinality $n$.
Let $\struct {S, \mathscr I_{n, n} }$ be the uniform matroid of rank $n$.
From Cardinality of Proper Subset of Finite Set, every subset of $S$ has cardinality less than or equal to $n$.
It follows that $\mathscr I_{n, n} = \powerset S$.
From Uniform Matroid is Matroid, then $\struct {S, \powerset S}$ Is a matroid.
{{qed}}
Theorem: Matroid Induced by Linear Independence in Vector Space is Matroid

Let $V$ be a vector space.
Let $S$ be a finite subset of $V$.
Let $\struct{S, \mathscr I}$ be the matroid induced on $S$ by linear independence in $V$.
That is, $\mathscr I$ is the set of linearly independent subsets of $S$.
Then $\struct{S, \mathscr I}$ is a matroid.

Proof:
It needs to be shown that $\mathscr I$ satisfies the matroid axioms $(I1)$, $(I2)$ and $(I3)$.
Theorem: Cycle Matroid is Matroid

Let $G = \struct {V, E}$ be a graph.
Let $\struct {E, \mathscr I}$ be the cycle matroid of $G$.
Then $\struct {E, \mathscr I}$ is a matroid.

Proof:
It needs to be shown that $\mathscr I$ satisfies the matroid axioms $(\text I 1)$, $(\text I 2)$ and $(\text I 3)$.
Theorem: Matroid Induced by Algebraic Independence is Matroid

Let $L / K$ be a field extension.
Let $S \subseteq L$ be a finite subset of $L$.
Let $\struct {S, \mathscr I}$ be the matroid induced by algebraic independence over $K$ on $S$.
That is, $\mathscr I$ is the set of algebraically independent subsets of $S$.
Then $\struct {S, \mathscr I}$ is a matroid.

Proof:
It needs to be shown that $\mathscr I$ satisfies the matroid axioms $(\text I 1)$, $(\text I 2)$ and $(\text I 3)$.
Theorem: Matroid Induced by Affine Independence is Matroid

Let $\R^n$ be the $n$-dimensional real Euclidean space.
Let $S = \set {x_1, \dots, x_r}$ be a finite subset of $\R^n$.
Let $\struct {S, \mathscr I}$ be the matroid induced by affine independence on $S$.
That is, $\mathscr I$ is the set of affinely independent subsets of $S$.
Then $\struct{S, \mathscr I}$ is a matroid.

Proof:
It needs to be shown that $\mathscr I$ satisfies the matroid axioms $(I1)$, $(I2)$ and $(I3)$.
Theorem: Matroid Induced by Linear Independence in Abelian Group is Matroid

Let $\struct{G, +}$ be a torsion-free Abelian group.
Let $\struct{G, +, \times}$ be the $\Z$-module associated with $G$.
Let $S$ be a finite subset of $G$.
Let $\struct{S, \mathscr I}$ be the matroid induced by linear independence in $G$ on $S$.
That is, $\mathscr I$ is the set of linearly independent subsets of $S$.
Then $\struct{S, \mathscr I}$ is a matroid.

Proof:
It needs to be shown that $\mathscr I$ satisfies the matroid axioms $(I1)$, $(I2)$ and $(I3)$.
Theorem: Independent Set can be Augmented by Larger Independent Set

Let $M = \struct{S, \mathscr I}$ be a matroid.
Let $X, Y \in \mathscr I$ such that:
:$\size X < \size Y$
Then there exists non-empty $Z \subseteq Y \setminus X$ such that:
:$X \cup Z \in \mathscr I$
:$\size {X \cup Z} = \size Y$

Proof:
Let $\mathscr Z = \set {Z \subseteq Y \setminus X : X \cup Z \in \mathscr I}$
Note that $\O \in \mathscr Z $
So $\mathscr Z \ne \O$
Let $Z_0 \in \mathscr Z : \size {Z_0} = \max \set {\size Z : Z \in \mathscr Z}$
{{AimForCont}}:
:$\size {X \cup Z_0} < \size Y$
By matroid axiom $(\text I 3)$:
:$\exists y \in Y \setminus \paren{X \cup Z_0} : X \cup Z_0 \cup \set y \in \mathscr I$
By choice of $Z_0$ and $y$:
:$Z_0 \cup \set y \subseteq Y \setminus X$
So:
:$Z_0 \cup \set y \in \mathscr Z$
Then:
{{begin-eqn}}
{{eqn | l = \size {Z_0 \cup \set y}
      | r = \size {Z_0} + \size {\set y}
      | c = {{Corollary|Cardinality of Set Union}}
}}
{{eqn | r = \size {Z_0} + 1
      | c = Cardinality of Singleton
}}
{{eqn | o = >
      | r = \size {Z_0}
}}
{{end-eqn}}
This contradicts the choice of $Z_0$.
It follows that:
{{begin-eqn}}
{{eqn | l = \size Y
      | o = \le
      | r = \size {X \cup Z_0}
}}
{{eqn | r = \size X + \size {Z_0}
      | c = {{Corollary|Cardinality of Set Union}}
}}
{{eqn | ll= \leadsto
      | l = \size {Z_0}
      | o = \ge
      | r = \size Y - \size X
}}
{{end-eqn}}
From Finite Set Contains Subset of Smaller Cardinality:
:$\exists Z \subseteq Z_0 : \size Z = \size Y - \size X$
Then:
{{begin-eqn}}
{{eqn | l = \size {X \cup Z}
      | r = \size X + \size Z
      | c = {{Corollary|Cardinality of Set Union}}
}}
{{eqn | r = \size Y
}}
{{end-eqn}}
We have:
{{begin-eqn}}
{{eqn | l = \card Z
      | r = \card Y - \card X
}}
{{eqn | o = >
      | r = 0
      | c = As $\card X < \card Y$
}}
{{eqn | ll = \leadsto
      | l = Z
      | o = \neq
      | r = \O
      | c = Cardinality of Empty Set
}}
{{end-eqn}}
{{qed}}