avewright/proofwiki-math huggingface dataset:
Theorem: Permutation of Indices

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers.
Let the fiber of truth of $R$ be finite.
Let  $\pi$ is a permutation on the fiber of truth of $R$.
Then:

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{\map R {\map \pi j} } a_{\map \pi j}
      | r = \sum_{j \mathop \in \Z} a_{\map \pi j} \sqbrk {\map R {\map \pi j} }
      | c = {{Defof|Summation by Iverson's Convention}}
}}
{{eqn | r = \sum_{j \mathop \in \Z} \sum_{i \mathop \in \Z} a_i \sqbrk {\map R i} \sqbrk {i = \map \pi j}
      | c = 
}}
{{eqn | r = \sum_{i \mathop \in \Z} a_i \sqbrk {\map R i} \sum_{j \mathop \in \Z} \sqbrk {i = \map \pi j}
      | c = 
}}
{{eqn | r = \sum_{i \mathop \in \Z} a_i \sqbrk {\map R i}
      | c = 
}}
{{eqn | r = \sum_{\map R i} a_i
      | c = 
}}
{{eqn | r = \sum_{\map R j} a_j
      | c = Change of Index Variable of Summation
}}
{{end-eqn}}
{{qed}}
Theorem: Change of Index Variable of Product

:$\ds \prod_{\map R i} a_i = \prod_{\map R j} a_j$

Proof:
Let $S = \set {i \in \Z: \map R i}$.
Let $T = \set {j \in \Z: \map R j}$.
Let $i \in S$.
Then $\map R i$.
Let $j = i$.
By Leibniz's Law, $\map R j$.
Thus $i \in T$.
By definition of subset:
:$S \subseteq T$
Similarly, let $j \in T$.
Then $\map R j$.
Let $i = j$.
By Leibniz's Law, $\map R i$.
Thus $j \in S$.
By definition of subset:
:$T \subseteq S$
Thus by definition of set equality:
:$S = T$
Thus:
{{begin-eqn}}
{{eqn | l = \prod_{\map R i} a_i
      | r = \prod a_i \sqbrk {\map R i}
      | c = {{Defof|Iverson's Convention}}
}}
{{eqn | r = \prod a_i \times \chi_S
      | c = {{Defof|Characteristic Function of Set}}
}}
{{eqn | r = \prod a_j \times \chi_T
      | c = as $S = T$
}}
{{eqn | r = \prod a_j \sqbrk {\map R j}
      | c = {{Defof|Iverson's Convention}}
}}
{{eqn | r = \prod_{\map R j} a_j
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Translation of Index Variable of Summation/Corollary

:$\ds \sum_{j \mathop = m}^n a_j = \sum_{j \mathop = m + c}^{n + c} a_{j - c}$
where $c$ is an integer constant which is not dependent upon $j$.

Proof:
{{proof wanted}}
Category:Summations
aracbiz9djucfdwdm6iryfcxhnaoxhg
Theorem: Permutation of Indices of Product

:$\ds \prod_{\map R j} a_j = \prod_{\map R {\map \pi j} } a_{\map \pi j}$

Proof:
{{begin-eqn}}
{{eqn | l = \prod_{\map R {\map \pi j} } a_{\map \pi j}
      | r = \prod_{j \mathop \in \Z} {a_{\map \pi j} }^{\sqbrk {\map R {\map \pi j} } }
      | c = {{Defof|Continued Product by Iverson's Convention}}
}}
{{eqn | r = \prod_{j \mathop \in \Z} \prod_{i \mathop \in \Z} {a_i}^{\sqbrk {\map R i} \sqbrk {i = \map \pi j} }
      | c = 
}}
{{eqn | r = \paren {\prod_{i \mathop \in \Z} {a_i}^{\sqbrk {\map R i} } } \uparrow \paren {\prod_{j \mathop \in \Z} \sqbrk {i = \map \pi j} }
      | c = using Knuth uparrow notation
}}
{{eqn | r = \prod_{i \mathop \in \Z} {a_i}^{\sqbrk {\map R i} }
      | c = 
}}
{{eqn | r = \prod_{\map R i} a_i
      | c = 
}}
{{eqn | r = \prod_{\map R j} a_j
      | c = Change of Index Variable of Product
}}
{{end-eqn}}
{{qed}}
{{Proofread}}
Theorem: Product of Products over Overlapping Domains

:$\ds \prod_{\map R j} a_j \prod_{\map S j} a_j = \paren {\prod_{\map R j \mathop \lor \map S j} a_j} \paren {\prod_{\map R j \mathop \land \map S j} a_j}$
where $\lor$ and $\land$ signify logical disjunction and logical conjunction respectively.

Proof:
{{begin-eqn}}
{{eqn | l = \prod_{\map R j} a_j \times \prod_{\map S j} a_j
      | r = \prod_{j \mathop \in \Z} a_j^{\sqbrk {\map R j} } \times \prod_{j \mathop \in \Z} a_j^{\sqbrk {\map S j} }
      | c = {{Defof|Continued Product by Iverson's Convention}}
}}
{{eqn | r = \prod_{j \mathop \in \Z} a_j^{\paren {\sqbrk {\map R j} + \sqbrk {\map S j} } }
      | c = Product of Powers
}}
{{end-eqn}}
Let:
:$A := \set {j \in \Z: \map R j}$
:$B := \set {j \in \Z: \map S j}$
The result then follows from Cardinality of Set Union.
{{qed}}
Theorem: Topology is Locally Compact iff Ordered Set of Topology is Continuous

Let $T = \struct {S, \tau}$ be a topological space.
Let $L = \struct {\tau, \preceq}$ be the ordered set where $\preceq$ is the subset relation.
Then
:$(1): \quad T$ is locally compact implies $L$ is continuous
:$(2): \quad T$ is $T_3$ space and $L$ is continuous implies $T$ is locally compact

Proof:
=== Condition $(1)$ ===
Let $T$ be locally compact.
By Topology forms Complete Lattice:
:$L$ is complete lattice.
Thus by Way Below Closure is Directed in Bounded Below Join Semilattice:
:$\forall x \in \tau: x^\ll$ is directed
Thus by definition:
:$L$ is up-complete.
Let $x \in \tau$.
We will prove that
:$x \subseteq \map \sup {x^\ll}$
Let $a \in x$.
By definition:
:$x$ is open set in $T$
By definition of locally compact:
:there exists local basis $\BB$ of $a$ such that all elements are compact.
By definition of local basis:
:$\exists y \in \BB: y \subseteq x$
Then
:$y$ is compact.
By Way Below if Between is Compact Set in Ordered Set of Topology:
:$y \ll x$
By definition of way below closure:
:$y \in x^\ll$
By Set is Subset of Union/Set of Sets:
:$\ds y \subseteq \bigcup \paren {x^\ll}$
By definition of subset:
:$\ds a \in \bigcup \paren {x^\ll}$
Thus by proof of Topology forms Complete Lattice:
:$a \in \sup \paren {x^\ll}$
{{qed|lemma}}
According to definition of set equality it remains to prove that:
:$\map \sup {x^\ll} \subseteq x$
Let $a \in \map \sup {x^\ll}$.
By proof of Topology forms Complete Lattice:
:$\ds a \in \bigcup \paren {x^\ll}$
By definition of union:
:$\exists y \in x^\ll: a \in y$
By definition of way below closure:
:$y \ll x$
By Way Below implies Preceding:
:$y \preceq x$
Then
:$y \subseteq x$
Thus by definition of subset:
:$a \in x$
By definition:
:$L$ satisfies the axiom of approximation.
Thus by definition
:$L$ is continuous.
{{qed|lemma}}
Theorem: Sum of Sequence of Power by Index

:$\ds \sum_{j \mathop = 0}^n j x^j = \frac {n x^{n + 2} - \paren {n + 1} x^{n + 1} + x} {\paren {x - 1}^2}$
for $x \ne 1$.

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^n j x^j
      | r = x \sum_{1 \mathop \le j \mathop \le n}^n j x^{j - 1}
      | c = 
}}
{{eqn | r = x \sum_{0 \mathop \le j \mathop \le n - 1} \paren {j + 1} x^j
      | c = 
}}
{{eqn | r = \paren {x \sum_{0 \mathop \le j \mathop \le n - 1} j x^j} + \paren {x \sum_{0 \mathop \le j \mathop \le n - 1} x^j}
      | c = 
}}
{{eqn | r = \paren {x \sum_{0 \mathop \le j \mathop \le n} j x^j} - n x^{n + 1} + \paren {\sum_{0 \mathop \le j \mathop \le n - 1} x^{j + 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \paren {x - 1} \sum_{0 \mathop \le j \mathop \le n} j x^j
      | r = n x^{n + 1} - \paren {\sum_{1 \mathop \le j \mathop \le n} x^j}
      | c = 
}}
{{eqn | r = n x^{n + 1} - \paren {\sum_{0 \mathop \le j \mathop \le n} x^j} + 1
      | c = 
}}
{{eqn | r = n x^{n + 1} - \paren {\frac {x^{n - 1} - 1} {x - 1} } + 1
      | c = Sum of Geometric Sequence
}}
{{eqn | ll= \leadsto
      | l = \sum_{j \mathop = 0}^n j x^j
      | r = \frac {n x^{n + 2} - \paren {n + 1} x^{n + 1} + x} {\paren {x - 1}^2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Power by Index

:$\ds \sum_{j \mathop = 0}^n j x^j = \frac {n x^{n + 2} - \paren {n + 1} x^{n + 1} + x} {\paren {x - 1}^2}$
for $x \ne 1$.

Proof:
From Sum of Arithmetic-Geometric Sequence:
:$\ds \sum_{j \mathop = 0}^n \paren {a + j d} x^j = \frac {a \paren {1 - x^{n + 1} } } {1 - x} + \frac {x d \paren {1 - \paren {n + 1} x^n + n x^{n + 1} } } {\paren {1 - x}^2}$
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^n j x^j
      | r = \frac {0 \paren {1 - x^{n + 1} } } {1 - x} + \frac {x \times 1 \paren {1 - \paren {n + 1} x^n + n x^{n + 1} } } {\paren {1 - x}^2}
      | c = putting $a = 0, d = 1$
}}
{{eqn | r = \frac {x \paren {1 - \paren {n + 1} x^n + n x^{n + 1} } } {\paren {1 - x}^2}
      | c = initial simplification
}}
{{eqn | r = \frac {x - \paren {n + 1} x^{n + 1} + n x^{n + 2} } {\paren {x - 1}^2}
      | c = further simplification
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Reciprocal of Real Exponential

:$\dfrac 1 {\map \exp x} = \map \exp {-x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \exp 0
      | r = 1
      | c = Exponential of Zero
}}
{{eqn | ll= \leadsto
      | l = \map \exp {x - x}
      | r = 1
      | c = as $\forall x \in \R : x - x = 0$
}}
{{eqn | ll= \leadsto
      | l = \map \exp {-x} \, \map \exp x
      | r = 1
      | c = Exponential of Sum of Real Numbers
}}
{{eqn | ll= \leadsto
      | l = \map \exp {-x}
      | r = \dfrac 1 {\exp x}
      | c = dividing both sides by $\exp x$, which is non-zero by Exponential of Real Number is Strictly Positive
}}
{{end-eqn}}
{{qed}}
Theorem: Telescoping Series/Example 2

Let $\sequence {b_n}$ be a sequence in $\R$.
Let $\sequence {a_n}$ be a sequence whose terms are defined as:
:$a_k = b_k - b_{k - 1}$
Then:
:$\ds \sum_{k \mathop = m}^n a_k = b_n - b_{m - 1}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop = m}^n a_k
      | r = \sum_{k \mathop = m}^n \paren {b_k - b_{k - 1} }
      | c = 
}}
{{eqn | r = \sum_{k \mathop = m}^n b_k - \sum_{k \mathop = m}^n b_{k - 1}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = m}^n b_k - \sum_{k \mathop = m - 1}^{n - 1} b_k
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \paren {\sum_{k \mathop = m}^{n - 1} b_k + b_n} - \paren {b_{m - 1} + \sum_{k \mathop = m}^{n - 1} b_k}
      | c = 
}}
{{eqn | r = b_n - b_{m - 1}
      | c = 
}}
{{end-eqn}}
{{Qed}}
Theorem: Repunit Integer as Product of Base - 1 by Increasing Digit Integer

{{begin-eqn}}
{{eqn | l = 9 \times 0 + 1
      | r = 1
}}
{{eqn | l = 9 \times 1 + 2
      | r = 11
}}
{{eqn | l = 9 \times 12 + 3
      | r = 111
}}
{{eqn | l = 9 \times 123 + 4
      | r = 1111
}}
{{eqn | l = 9 \times 1234 + 5
      | r = 11111
}}
{{eqn | l = 9 \times 12345 + 6
      | r = 111111
}}
{{eqn | o = \ldots
}}
{{end-eqn}}
That is:
:$\ds 9 \sum_{j \mathop = 0}^n \paren {n - j} 10^j + n + 1 = \sum_{j \mathop = 0}^n 10^j$

Proof:
A specific instance of the general result:
{{:Repunit Integer as Product of Base - 1 by Increasing Digit Integer/General Result}}
where $b = 10$.
{{qed}}
Theorem: Repunit Integer as Product of Base - 1 by Increasing Digit Integer/General Result

:$\ds \paren {b - 1} \sum_{j \mathop = 0}^n \paren {n - j} b^j + n + 1 = \sum_{j \mathop = 0}^n b^j$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {b - 1} \sum_{j \mathop = 0}^n \paren {n - j} b^j + n + 1
      | c = 
}}
{{eqn | r = n \paren {b - 1} \sum_{j \mathop = 0}^n b^j - \paren {b - 1} \sum_{j \mathop = 0}^n j b^j + n + 1
      | c = 
}}
{{eqn | r = n \paren {b - 1} \frac {b^{n + 1} - 1} {b - 1} - \paren {b - 1} \sum_{j \mathop = 0}^n j b^j + n + 1
      | c = Sum of Geometric Sequence
}}
{{eqn | r = n \paren {b - 1} \frac {b^{n + 1} - 1} {b - 1} - \paren {b - 1} \frac {n b^{n + 2} - \paren {n + 1} b^{n + 1} + b} {\paren {b - 1}^2} + n + 1
      | c = Sum of Sequence of Power by Index
}}
{{eqn | r = \frac {n \paren {b - 1} \paren {b^{n + 1} - 1} - \paren {n b^{n + 2} - \paren {n + 1} b^{n + 1} + b} + \paren {b - 1} n + \paren {b - 1} } {b - 1}
      | c = elementary simplification
}}
{{eqn | r = \frac {n b^{n + 2} - n b^{n - 1} - n b + n - n b^{n + 2} + n b^{n - 1} + b^{n + 1} - b + n b - n + b - 1} {b - 1}
      | c = multiplying out
}}
{{eqn | r = \frac {b^{n + 1} - 1} {b - 1}
      | c = simplification
}}
{{eqn | r = \sum_{j \mathop = 0}^n b^j
      | c = Sum of Geometric Sequence
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Real Number is Strictly Positive/Proof 5/Lemma

:$\forall x \in \R: \exp x \ne 0$

Proof:
This proof assumes the definition of $\exp$ as the solution to an initial value problem.
That is, suppose $\exp$ satisfies:
:$(1): \quad D_x \exp x = \exp x$
:$(2): \quad \map \exp 0 = 1$
on $\R$.
{{AimForCont}} $\exists \alpha \in \R: \exp \alpha = 0$.
Suppose that $\alpha > 0$.
Let $J = \closedint 0 \alpha$.
From Exponential Function is Continuous, $\exp$ is continuous on $J$.
From Max and Min of Function on Closed Real Interval:
:$\exists K \in \R: \forall x \in J: \size {\exp x} < K$
Then, $\forall n \in \N : \exists c_n \in J$ such that:
{{begin-eqn}}
{{eqn | l = 1
      | r = \exp 0
      | c = by $(2)$
}}
{{eqn | r = \sum_{j \mathop = 0}^{n - 1} \frac {\map {\exp^j} \alpha} {j!} \paren {-\alpha}^j + \frac {\exp c_n} {n!} \paren {-\alpha}^n
      | c = Taylor's Theorem for Univariate Functions
}}
{{eqn | r = \sum_{j \mathop = 0}^{n - 1} \frac {\map \exp \alpha} {j!} \paren {-\alpha}^j + \frac {\exp c_n} {n!} \paren {-\alpha}^n
      | c = by $(1)$
}}
{{eqn | r = \sum_{j \mathop = 0}^{n - 1} \frac 0 {j!} \paren {-\alpha}^j + \frac {\exp c_n} {n!} \paren {-\alpha}^n
      | c = from our assumption aiming for a contradiction
}}
{{eqn | r = \frac {\exp c_n} {n!} \paren {-\alpha}^n
}}
{{end-eqn}}
So:
:$\forall n \in \N: 1 \le K \dfrac {\alpha^n} {n!}$
That is, dividing both sides by $K$:
:$\forall n \in \N: \dfrac 1 K \le \dfrac {\alpha^n} {n!}$
But from Power over Factorial, $\dfrac {\alpha^n} {n!} \to 0$.
This contradicts our assumption.
The same argument, {{mutatis}} proves the result for $\alpha < 0$.
By hypothesis $(2)$:
{{begin-eqn}}
{{eqn | l = \alpha
      | r = 0
}}
{{eqn | ll= \leadsto
      | l = \exp \alpha 
      | r = 1
}}
{{eqn | o = \ne
      | r = 0
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Exponential of Real Number is Strictly Positive
phekb8ldcw5xiui8e9elkbh1s9q95v3
Theorem: Product of Products

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers.
Let $\ds \prod_{R \paren i} x_i$ denote a continued product over $R$.
Let the fiber of truth of $R$ be finite.
Then:
:$\ds \prod_{R \paren i} \paren {b_i c_i} = \paren {\prod_{R \paren i} b_i} \paren {\prod_{R \paren i} c_i}$

Proof:
Let $b_i =: a_{i 1}$ and $c_i =: a_{i 2}$.
Then:
{{begin-eqn}}
{{eqn | l = \prod_{R \paren i} \paren {b_i c_i}
      | r = \prod_{R \paren i} \paren {a_{i 1} a_{i 2} }
      | c = by definition
}}
{{eqn | r = \prod_{R \paren i} \paren {\prod_{1 \mathop \le j \mathop \le 2} a_{i j} }
      | c = {{Defof|Continued Product by Propositional Function}}
}}
{{eqn | r = \prod_{1 \mathop \le j \mathop \le 2} \paren {\prod_{R \paren i} a_{i j} }
      | c = Exchange of Order of Product
}}
{{eqn | r = \paren {\prod_{R \paren i} a_{i 1} } \paren {\prod_{R \paren i} a_{i 2} }
      | c = {{Defof|Continued Product by Propositional Function}}
}}
{{eqn | r = \paren {\prod_{R \paren i} b_i} \paren {\prod_{R \paren i} c_i}
      | c = by definition
}}
{{end-eqn}}
{{qed}}
Theorem: Summation of General Logarithms

Let $R: \Z \to \set {\T, \F}$ be a propositional function on the set of integers.
Let $\ds \prod_{\map R i} a_i$ denote a product over $R$.
Let the fiber of truth of $R$ be finite.
Then:
:$\ds \map {\log_b} {\prod_{\map R i} a_i} = \sum_{\map R i} \log_b a_i$

Proof:
The proof proceeds by induction.
First let:
:$S := \set {a_i: \map R i}$
We have that $S$ is finite.
Hence the contents of $S$ can be well-ordered, by Finite Totally Ordered Set is Well-Ordered.
Let $S$ have $m$ elements, identified as:
:$S = \set {s_1, s_2, \ldots, s_m}$
For all $n \in \Z_{\ge 0}$ such that $n \le m$, let $\map P n$ be the proposition:
:$\ds \map {\log_b} {\prod_{i \mathop = 1}^n s_i} = \sum_{i \mathop = 1}^n \log_b s_i$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \map {\log_b} {\prod_{i \mathop = 1}^0 s_i}
      | r = \log_b 1
      | c = {{Defof|Vacuous Product}}
}}
{{eqn | r = 0
      | c = Logarithm of 1 is 0
}}
{{eqn | r = \sum_{i \mathop = 1}^n \log_b s_i
      | c = {{Defof|Vacuous Summation}}
}}
{{end-eqn}}
Theorem: Way Below Closure is Directed in Bounded Below Join Semilattice

Let $\struct {S, \vee, \preceq}$ be a bounded below join semilattice.
Let $x \in S$.
Then
:$x^\ll$ is directed.

Proof:
By Bottom is Way Below Any Element:
:$\bot \ll x$
By definition of way below closure:
:$\bot \in x^\ll$
Thus by definition:
:$x^\ll$ is a non-empty set.
Let $y, z \in x^\ll$
By definition of way below closure:
:$y \ll x$ and $z \ll x$
By Join is Way Below if Operands are Way Below
:$y \vee z \ll x$
By definition of way below closure:
:$y \vee z \in x^\ll$
By Join Succeeds Operands:
:$y \preceq y \vee z$ and $z \preceq y \vee z$
Thus by definition
:$x^\ll$ is directed.
{{qed}}
Theorem: Bottom is Way Below Any Element

Let $\left({S, \preceq}\right)$ be a bounded below ordered set.
Let $x \in S$.
Then
:$\bot \ll x$
where $\bot$ denotes the smallest element in $S$.

Proof:
Let $D$ be directed subset of $S$ such that
:$D$ admits a supremum and $x \preceq \sup D$
Because $D$ is non-empty, therefore
:$\exists a: a \in D$
By definition of smallest element:
:$\bot \preceq a$
Thus by definition of way below relation;
:$\bot \ll x$
{{qed}}
Theorem: Equivalence of Definitions of Real Exponential Function/Proof 2

The following definitions of the exponential function are equivalent.

Proof:
From Derivative of Exponential Function and Exponential of Zero, each definition of $\exp$ satisfies the following:
:$(1): \quad D_x \exp = \exp$
:$(2): \quad \map \exp 0 = 1$
on $\R$.
From Exponential Function is Well-Defined, such a solution is unique.
Thus they all are all equivalent.
{{qed}}
Theorem: Product to n of Product to Index

:$\ds \prod_{i \mathop = 0}^n \prod_{j \mathop = 0}^i a_i a_j = \prod_{i \mathop = 0}^n {a_i}^{n + 2}$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = P_1
      | o = :=
      | r = \prod_{i \mathop = 0}^n \prod_{j \mathop = 0}^i a_i a_j
}}
{{eqn | l = P_2
      | o = :=
      | r = \prod_{i \mathop = 0}^n \prod_{j \mathop = i}^n a_i a_j
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = P_1 P_2
      | r = \paren {\prod_{i \mathop = 0}^n \prod_{j \mathop = 0}^i a_i a_j} \paren {\prod_{i \mathop = 0}^n \prod_{j \mathop = i}^n a_i a_j}
      | c = 
}}
{{eqn | r = \prod_{i \mathop = 0}^n \paren {\paren {\prod_{j \mathop = 0}^i a_i a_j} \paren {\prod_{j \mathop = i}^n a_i a_j} }
      | c = 
}}
{{eqn | r = \prod_{i \mathop = 0}^n \paren {\paren {\prod_{j \mathop = 0}^n a_j a_j} {a_i}^2}
      | c = Product of Products over Overlapping Domains
}}
{{eqn | r = \prod_{i \mathop = 0}^n \paren { {a_i}^{n + 1} \paren {\prod_{j \mathop = 0}^n a_j} {a_i}^2}
      | c = 
}}
{{eqn | r = \paren {\prod_{i \mathop = 0}^n {a_i}^{n + 1} } \paren {\prod_{j \mathop = 0}^n \paren {\prod_{j \mathop = 0}^n a_j} {a_i}^2}
      | c = 
}}
{{eqn | r = \paren {\prod_{i \mathop = 0}^n {a_i}^{n + 1} } \paren {\prod_{j \mathop = 0}^n {a_i}^{n + 1} {a_i}^2}
      | c = 
}}
{{eqn | r = \prod_{i \mathop = 0}^n {a_i}^{2 n + 4}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = P_1
      | r = \prod_{i \mathop = 0}^n {a_i}^{n + 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Bernoulli's Inequality/Corollary/General Result

For all $n \in \Z_{\ge 0}$:
:$\ds \prod_{j \mathop = 1}^n \paren {1 - a_j} \ge 1 - \sum_{j \mathop = 1}^n a^j$
where $0 < a_j < 1$ for all $j$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \prod_{j \mathop = 1}^n \paren {1 - a_j} \ge 1 - \sum_{j \mathop = 1}^n a^j$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \prod_{j \mathop = 1}^0 \paren {1 - a_j}
      | r = 1
      | c = {{Defof|Vacuous Product}}
}}
{{eqn | o = \ge
      | r = 1 - 0
      | c = 
}}
{{eqn | r = 1 - \sum_{j \mathop = 1}^0 a^j
      | c = {{Defof|Vacuous Summation}}
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
Theorem: Product of Sequence of 1 minus Reciprocal of Squares

For all $n \in \Z_{\ge 1}$:
:$\ds \prod_{j \mathop = 2}^n \paren {1 - \dfrac 1 {j^2} } = \dfrac {n + 1} {2 n}$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:$\ds \prod_{j \mathop = 2}^n \paren {1 - \dfrac 1 {j^2} } = \dfrac {n + 1} {2 n}$
It is first noted that $n = 0$ is excluded because in that case $\dfrac {n + 1} {2 n}$ is undefined.
$\map P 1$ is the other edge case:
{{begin-eqn}}
{{eqn | l = \prod_{j \mathop = 2}^1 \paren {1 - \dfrac 1 {j^2} }
      | r = 1
      | c = {{Defof|Vacuous Product}}
}}
{{eqn | r = \dfrac {1 + 1} {2 \times 1}
      | c = 
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
=== Basis for the Induction ===
$\map P 2$ is the case:
{{begin-eqn}}
{{eqn | l = \prod_{j \mathop = 2}^2 \paren {1 - \dfrac 1 {j^2} }
      | r = 1 - \dfrac 1 {2^2}
      | c = {{Defof|Continued Product}}
}}
{{eqn | r = \frac {4 - 1} 4
      | c = 
}}
{{eqn | r = \frac {2 + 1} {2 \times 2}
      | c = 
}}
{{eqn | r = \valueat {\frac {n + 1} {2 n} } {n \mathop = 2}
      | c = 
}}
{{end-eqn}}
Thus $\map P 1$ is seen to hold.
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that, if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:$\ds \prod_{j \mathop = 2}^k \paren {1 - \dfrac 1 {j^2} } = \dfrac {k + 1} {2 k}$
from which it is to be shown that:
:$\ds \prod_{j \mathop = 2}^{k + 1} \paren {1 - \dfrac 1 {j^2} } = \dfrac {k + 2} {2 \paren {k + 1} }$
=== Induction Step ===
This is the induction step:
{{begin-eqn}}
{{eqn | l = \prod_{j \mathop = 2}^{k + 1} \paren {1 - \dfrac 1 {j^2} }
      | r = \prod_{j \mathop = 2}^k \paren {1 - \dfrac 1 {j^2} } \paren {1 - \dfrac 1 {\paren {k + 1}^2} }
      | c = {{Defof|Continued Product}}
}}
{{eqn | r = \dfrac {k + 1} {2 k} \paren {1 - \dfrac 1 {\paren {k + 1}^2} }
      | c = Induction Hypothesis
}}
{{eqn | r = \dfrac {k + 1} {2 k} \times \dfrac {\paren {k + 1}^2 - 1} {\paren {k + 1}^2}
      | c = 
}}
{{eqn | r = \dfrac {k^2 + 2 k + 1 - 1} {2 k \paren {k + 1} }
      | c = simplification
}}
{{eqn | r = \dfrac {k \paren {k + 2} } {2 k \paren {k + 1} }
      | c = further simplification
}}
{{eqn | r = \dfrac {k + 2} {2 \paren {k + 1} }
      | c = further simplification
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\ds \forall n \in \Z_{\ge 1}: \prod_{j \mathop = 2}^n \paren {1 - \dfrac 1 {j^2} } = \dfrac {n + 1} {2 n}$
{{qed}}
Theorem: Product of Sequence of 1 minus Reciprocal of Squares

For all $n \in \Z_{\ge 1}$:
:$\ds \prod_{j \mathop = 2}^n \paren {1 - \dfrac 1 {j^2} } = \dfrac {n + 1} {2 n}$

Proof:
We have: 
{{begin-eqn}}
{{eqn	| l = \prod_{j \mathop = 2}^n \paren {1 - \frac 1 {j^2} }
	| r = \prod_{j \mathop = 2}^n \paren {\frac {\paren {j - 1} \paren {j + 1} } {j^2} }
	| c = Difference of Two Squares
}}
{{eqn	| r = \paren {\prod_{j \mathop = 2}^n \paren {j - 1} } \paren {\prod_{j \mathop = 2}^n \paren {j + 1} } \paren {\prod_{j \mathop = 2}^n \frac 1 j}^2
	| c = Product of Products
}}
{{eqn	| r = \paren {\prod_{j \mathop = 1}^{n - 1} j} \paren {\prod_{j \mathop = 3}^{n + 1} j} \frac 1 {\paren {\prod_{j \mathop = 2}^n j}^2}
}}
{{eqn	| r = \paren {n - 1}! \paren {\frac 1 2 \prod_{j \mathop = 2}^{n + 1} j} \frac 1 {\paren {n!}^2}
	| c = {{Defof|Factorial}}
}}
{{eqn	| r = \frac {\paren {n - 1}! \paren {n + 1}!} {2 \times n! \times n!}
	| c = {{Defof|Factorial}}
}}
{{eqn	| r = \frac {\paren {n - 1}! n! \paren {n + 1} } {2 \paren {n - 1}! \times n \times n!}
	| c = Gamma Difference Equation
}}
{{eqn	| r = \frac {n + 1} {2 n}
}}
{{end-eqn}}
{{qed}}