avewright/proofwiki-math huggingface dataset:
Theorem: Real Semi-Inner Product Space is Complex Semi-Inner Product Space

Let $\struct{V, \innerprod \cdot \cdot}$ be a real semi-inner product space.
Then $\struct{V, \innerprod \cdot \cdot}$ is a complex semi-inner product Space.

Proof:
This follows immediately from:
* {{Defof|Real Semi-Inner Product Space}}
* {{Defof|Complex Semi-Inner Product Space}}
* Real Semi-Inner Product is Complex Semi-Inner Product
{{qed}}
Theorem: Real Inner Product is Complex Inner Product

Let $V$ be a vector space over a real subfield $\GF$.
Let $\innerprod \cdot \cdot: V \times V \to \GF$ be a real inner product.
Then $\innerprod \cdot \cdot$ is a complex inner product

Proof:
This follows immediately from:
* {{Defof|Real Inner Product}}
* {{Defof|Complex Inner Product}}
* Complex Number equals Conjugate iff Wholly Real
{{qed}}
Theorem: Real Inner Product Space is Complex Inner Product Space

Let $\struct{V, \innerprod \cdot \cdot}$ be a real inner product space.
Then $\struct{V, \innerprod \cdot \cdot}$ is a complex inner product Space.

Proof:
This follows immediately from:
* {{Defof|Real Inner Product Space}}
* {{Defof|Complex Inner Product Space}}
* Real Inner Product is Complex Inner Product
{{qed}}
Theorem: Number of Ways of Seating People at Circular Table

Let there be $n$ people to be seated at a round table.
Let $N$ be the number of different ways to seat those $n$ people.
Note that if person $A$ is seated between person $B$ and person $C$, then having $B$ on the left and $C$ on the right is considered different from having $B$ on the right and $C$ on the left.
Then:
:$N = \paren {n - 1}!$

Proof:
From Number of Permutations of All Elements, the number of different ways of arranging $n$ people in line is $n!$.
However, a round table has no beginning and end.
Hence the vital factor is the arrangement relative to an arbitrary given person.
So we fix one person, and arrange the other $n - 1$ people relative to that person.
From Number of Permutations of All Elements, there are $\paren {n - 1}!$ ways to arrange those people. 
{{qed}}
Theorem: Number of Ways of Threading Beads on a Loop of Wire

Let there be $n$ beads to be threaded on a circular loop of wire.
Let $N$ be the number of different ways to thread those $n$ beads.
Then:
:$N = \dfrac {\paren {n - 1}!} 2$

Proof:
This is the same as Number of Ways of Seating People at Circular Table, except that having threaded the beads in one arrangement, you can get another arrangement by flipping the ring of beads over.
From Number of Ways of Seating People at Circular Table, the number of arrangements of $n$ beads on a ring, without flipping it over, is $\paren {n - 1}!$.
But every arrangement can be paired with exactly one other arrangement such that those two arrangements are effectively the same.
Hence the result.
{{qed}}
Theorem: Number of Arrangements of n Objects of m Types

Let $S$ be a collection of $n$ objects.
Let these $n$ objects be of $m$ different types, as follows:
Let there be:
:$k_1$ objects of type $1$
:$k_2$ objects of type $2$
:$\cdots$
:$k_m$ objects of type $m$
such that:
:for each $j \in \set {1, 2, \ldots, m}$, all objects of type $j$ are indistinguishable from each other
:$k_1 + k_2 + \cdots + k_m = n$
Then the total number $N$ of different arrangements of $S$ is given by the multinomial coefficient:
:$N = \dbinom n {k_1, k_2, \ldots, k_m} = \dfrac {n!} {k_1! \, k_2! \cdots k_m!}$

Proof:
Let $N$ be the number of different arrangements of $S$.
First suppose that all $n$ objects are distinct one from another.
Then from Number of Permutations of All Elements:
:$N = n!$
Now suppose that $k_j$ elements of $S$ are indistinguishable from each other.
From Number of Permutations of All Elements, there are $k_j!$ different arrangements of those $k_j$ elements.
Hence the $n!$ arrangements of $S$ can each be grouped into $\dfrac {n!} {k_j!}$ partitions, each with $k_j$ elements, such that all the arrangements in each partition are indistinguishable from each other.
This applies for all $m$ types of objects.
The result follows.
{{qed}}
{{improve|This is intuitive and not at all rigorous. I throw it open for anyone either to improve this informal demonstration or write a further proof along rigorous lines.}}
Theorem: Space of Square Summable Mappings is Vector Space

Let $\GF$ be a subfield of $\C$.
Let $I$ be a set.
Let $\map {\ell^2} I$ be the space of square summable mappings over $I$.
Then $\map {\ell^2} I$ is a vector space.

Proof:
By definition, $\map {\ell^2} I$ is a subset of the vector space $\GF^I$ of all mappings $f: I \to \GF$.
Let us apply the One-Step Vector Subspace Test.
Thus, let $f, g \in \map {\ell^2} I$ and $\lambda \in \GF$.
Then we must show that $f + \lambda g: I \to \GF$ is square summable.
First, note that:
:$\set{ i \in I: \map f i + \lambda \map g i \ne 0 } \subseteq \set{ i \in I: \map f i \ne 0 } \cup \set{ i \in I: \map g i \ne 0 }$
By Finite Union of Countable Sets is Countable and Subset of Countable Set is Countable, it follows that:
:$\set{ i \in I: \map f i + \lambda \map g i \ne 0 }$
is countable.
Next:
{{begin-eqn}}
{{eqn| l = \sum_{i \mathop \in I} \cmod{ \map f i + \lambda \map g i }^2
     | o = \le
     | r = \sum_{i \mathop \in I} \cmod{ \map f i }^2 + \cmod{\lambda}^2 \cmod{ \map g i }^2
}}
{{eqn| r = \sum_{i \mathop \in I} \cmod{ \map f i }^2 + \cmod{\lambda}^2 \sum_{i \mathop \in I} \cmod{ \map g i }^2
}}
{{eqn| o = <
     | r = \infty
}}
{{end-eqn}}
so that $f + \lambda g$ is square summable.
Hence the result by the One-Step Vector Subspace Test.
{{qed}}
Category:Examples of Vector Spaces
Category:Space of Square Summable Mappings
8ais6vsdz9ynt32ouqvofs6pzwxrczd
Theorem: Number of Selections of 1 or More from Set

Let $S$ be a set of $n$ objects.
The total number $N$ of ways that at least $1$ object can be selected from $S$ is:
:$N = 2^n - 1$

Proof:
This is equivalent to counting the number of non-empty subsets of $S$.
From Cardinality of Power Set of Finite Set, the total number of subsets of $S$ is $2^n$.
This includes the empty set.
Excluding the empty set from the count gives the result.
{{qed}}
Theorem: Number of Selections from n Objects of 2 Types

Let $S$ be a collection of $n$ objects, consisting of:
:$p$ objects of one type
:$q$ objects of another type.
The total number $N$ of different non-empty selections from $S$ is given by:
:$N = 2^n \paren {p + 1} \paren {q + 1} - 1$

Proof:
For each object, we have $2$ choices: whether to select or whether not.
From Cardinality of Power Set of Finite Set, this gives us $2^n$ options.
From the $p$ things of the first type, we may take $0, 1, 2, \ldots, p$ objects.
Hence we have $\paren {p + 1}$ choices.
Similarly, from the $q$ things of the second type, we have $\paren {q + 1}$ choices.
Hence we have $\paren {p + 1}$ choices.
Because the non-empty selection is excluded, this gives:
:$N = 2^n \paren {p + 1} \paren {q + 1} - 1$
Hence the result.
{{qed}}
{{questionable|I don't understand this. How can the number of selections be more than Cardinality of Power Set of Finite Set? The above is copied verbatim from the book. More thought needed as to exactly what it means.}}
Theorem: Inner Product on Space of Square Summable Mappings is Complex Inner Product

Let $\GF$ be a subfield of $\C$.
Let $I$ be a set.
Let $\map {\ell^2} I$ be the space of square summable mappings over $I$.
Let $\innerprod \cdot \cdot: \map {\ell^2} I \times \map {\ell^2} I \to \GF$ be the inner product on $\map {\ell^2} I$.
Then $\innerprod \cdot \cdot$ is a complex inner product.

Proof:
By Space of Square Summable Mappings is $L^2$ Space, $\map {\ell^2} I$ is equal to $\map {L^2} {I, \powerset I, \mu}$.
Here, $\mu$ is the counting measure on the subsets of $I$.
By Inner Product/Examples/Lebesgue 2-Space, there is a complex inner product on $\map {\ell^2} I = \map {L^2} {I, \powerset I, \mu}$ defined by:
:$\ds \innerprod f g = \int f ~ \overline g \rd \mu$
By Integral over Counting Measure is Sum over Values, it follows that:
:$\ds \innerprod f g = \int f ~ \overline g \rd \mu = \sum_{i \mathop \in I} \map f i \overline{ \map g i }$
which is exactly the definition of the inner product on $\map {\ell^2} I$.
{{qed}}
Category:Examples of Inner Products
8ya90mqjm8nnz9cwhdft12q2yn7amcz
Theorem: Space of Square Summable Mappings is Hilbert Space

Let $\GF$ be a subfield of $\C$.
Let $I$ be a set.
Let $\map {\ell^2} I$ be the space of square summable mappings over $I$.
Let $\innerprod \cdot \cdot: \map {\ell^2} I \times \map {\ell^2} I \to \GF$ be the inner product on $\map {\ell^2} I$.
Then $\map {\ell^2} I$ endowed with $\innerprod \cdot \cdot$ is a Hilbert space.

Proof:
By Space of Square Summable Mappings is $L^2$ Space, $\map {\ell^2} I$ is equal to $\map {L^2} {I, \powerset I, \mu}$.
The result follows by $L^2$ Space forms Hilbert Space.
{{qed}}
Theorem: Space of Square Summable Mappings is L-2 Space

Let $\GF$ be a subfield of $\C$.
Let $I$ be a set.
Let $\map {\ell^2} I$ be the space of square summable mappings over $I$.
Then $\map {\ell^2} I$ is equal to the $L^2$ space $\map {L^2} {I, \powerset I, \mu}$, where $\mu$ is the counting measure on $I$.

Proof:
First, let us unpack the definition of the Lebesgue space $\map {\LL^2} {I, \powerset I, \mu}$:
:$\ds \map {\LL^2} {I, \powerset I, \mu} = \set{ f: I \to \GF: f \in \map \MM { \powerset I }, \int \size f^2 \rd \mu < \infty}$
By Function Measurable with respect to Power Set, all mappings $f: I \to \GF$ are measurable.
By Integral over Counting Measure is Sum of Values:
:$\ds \int \size f^2 \rd \mu = \sum_{i \mathop \in I} \cmod {\map f i}^2$
Hence:
:$\ds \map {\LL^2} {I, \powerset I, \mu} = \set{ f: I \to \GF: \sum_{i \mathop \in I} \cmod{ \map f i }^2 < \infty}$
which is exactly the definition of $\map {\ell^2} I$.
Next, the definition of $\map {L^2} {I, \powerset I, \mu}$ is:
:$\map {L^2} \mu = \map {\LL^2} {\mu} / \sim_\mu$
where $\sim_\mu$ is the $\mu$-almost-everywhere equality relation.
Now let $f, g \in \map {\ell^2} I$ such that $\map \mu { \set{ f \ne g } } = 0$.
Then since $\mu$ is the counting measure, it follows that $\set {f \ne g} = \O$.
That is, $f = g$.
Therefore, $\sim_\mu$ is the trivial equivalence and $\map {\ell^2} I = \map {L^2} {I, \powerset I, \mu}$.
{{qed}}
Theorem: Equivalence of Definitions of Semiring of Sets/Definition 1 implies Definition 2

Let $\SS$ be a system of sets satisfying the semiring of sets axioms:
{{:Axiom:Semiring of Sets Axioms/Axioms 1}}
Then $\SS$ satisfies the semiring of sets axioms:
{{:Axiom:Semiring of Sets Axioms/Axioms 2}}

Proof:
Let $\SS$ be a system of sets satisfying the axioms:
{{:Axiom:Semiring of Sets Axioms/Axioms 1}}
It remains to be shown that $\SS$ satisfies the axiom 
{{begin-axiom}}
{{axiom | n = 3'
        | q = \forall A, B \in \SS
        | tr = $\exists n \in \N$ and pairwise disjoint sets $A_1, A_2, A_3, \ldots, A_n \in \SS : \ds A \setminus B = \bigcup_{k \mathop = 1}^n A_k$
}}
{{end-axiom}}
Let $A, B \in \SS$. 
Let $A_1 = A \cap B$.
By axiom $(2)$:
:$A_1 \in \SS$
From Intersection is Subset:
:$A_1 \subseteq A$
By axiom $(3)$:
:$\exists$ a finite sequence of pairwise disjoint sets $A_2, A_3, \ldots, A_n \in \SS : \ds A = \bigcup_{k \mathop = 1}^n A_k$
Then:
{{begin-eqn}}
{{eqn | l = A \setminus B
      | r = A \setminus \paren {A \cap B}
      | c = Set Difference with Intersection is Difference
}}
{{eqn | r = A \setminus A_1
}}
{{eqn | r = \paren {\bigcup_{k \mathop = 1}^n A_k} \setminus A_1
}}
{{eqn | r = \bigcup_{k \mathop = 1}^n \paren {A_k \setminus A_1}
      | c = Set Difference is Right Distributive over Union
}}
{{eqn | r = \bigcup_{k \mathop = 2}^n \paren {A_k \setminus A_1}
      | c = Set Difference with Self is Empty Set and Union with Empty Set
}}
{{eqn | r = \bigcup_{k \mathop = 2}^n A_k
      | c = Set Difference with Disjoint Set
}}
{{end-eqn}}
As $A$ and $B$ were arbitrary, then $\SS$ satisfies axiom $(3')$
The result follows
Theorem: Equivalence of Definitions of Semiring of Sets/Definition 2 implies Definition 1

Let $\SS$ be a system of sets satisfying the semiring of sets axioms:
{{:Axiom:Semiring of Sets Axioms/Axioms 2}}
Then $\SS$ satisfies the semiring of sets axioms:
{{:Axiom:Semiring of Sets Axioms/Axioms 1}}

Proof:
Let $\SS$ be a system of sets satisfying the axioms:
{{:Axiom:Semiring of Sets Axioms/Axioms 2}}
It remains to be shown that $\SS$ satisfies the axiom 
{{begin-axiom}}
{{axiom | n = 3
        | q = \forall A, A_1 \in \SS : A_1 \subseteq A
        | tr = $\exists n \in \N$ and pairwise disjoint sets $A_2, A_3, \ldots, A_n \in \SS : \ds A = \bigcup_{k \mathop = 1}^n A_k$
}}
{{end-axiom}}
Let $A, B \in \SS : B \subseteq A$.
By axiom $(3)$:
:$\exists$ a finite sequence of pairwise disjoint sets $A_1, A_2, \ldots, A_n \in \SS : \ds A \setminus B = \bigcup_{k \mathop = 1}^n A_k$.
Then $B$ is disjoint with each of the sets $A_k$.
Then:
{{begin-eqn}}
{{eqn | l = B \cup \bigcup_{k \mathop = 1}^n A_k
      | r = \paren {A \setminus B} \cup B
}}
{{eqn | r = A \cup B
      | c = Set Difference Union Second Set is Union
}}
{{eqn | r = A
      | c = Union with Superset is Superset
}}
{{end-eqn}}
As $A$ and $B$ were arbitrary, then $\SS$ satisfies axiom $(3)$
The result follows
Theorem: Set of Empty Set is Semiring of Sets

Let $\SS = \set{\O}$.
Then $\SS$ is a semiring of sets.

Proof:
Taking the axioms of semiring of sets in turn:
Theorem: Divisor of Integer/Examples/80 divides 9^2n - 1

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then:
:$80 \divides 9^{2 n} - 1$
where $\divides$ denotes divisibility.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the equivalent proposition:
:$80 \divides 9^{2 n} - 1$
where $\divides$ denotes divisbility
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = 9^{2 \times 0} - 1
      | r = 9^0 - 1
      | c = 
}}
{{eqn | r = 1 - 1
      | c = Zeroth Power of Real Number equals One
}}
{{eqn | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 80
      | o = \divides
      | r = 9^{2 \times 0} - 1
      | c = Integer Divides Zero
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = 9^{2 \times 1} - 1
      | r = 9^2 - 1
      | c = 
}}
{{eqn | r = 81 - 1
      | c = 
}}
{{eqn | r = 80
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 80
      | o = \divides
      | r = 9^{2 \times 1} - 1
      | c = Integer Divides Itself
}}
{{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:
:$80 \divides 9^{2 k} - 1$
from which it is to be shown that:
:$80 \divides 9^{2 \paren {k + 1} } - 1$
=== Induction Step ===
This is the induction step:
From the induction hypothesis we have that:
:$80 \divides 9^{2 k} - 1$
Hence by definition of divisibility, we have:
:$\exists r \in \Z: 9^{2 k} - 1 = 80 r$
and so:
:$(1): \quad \exists r \in \Z: 9^{2 k} = 80 r + 1$
{{begin-eqn}}
{{eqn | l = 9^{2 \paren {k + 1} } - 1
      | r = 9^2 \times 9^{2 k} - 1
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists r \in \Z
      | l = 9^{2 \paren {k + 1} } - 1
      | r = 81 \times \paren {80 r + 1} - 1
      | c = from $(1)$
}}
{{eqn | r = 81 \times 80 r + 80
      | c = algebra
}}
{{eqn | r = 80 \paren {81 r + 1}
      | c = algebra
}}
{{end-eqn}}
Hence by definition of divisibility:
:$80 \divides 9^{2 \paren {k + 1} } - 1$
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 0}: 80 \divides 9^{2 n} - 1$
{{qed}}
Theorem: Divisor of Integer/Examples/80 divides 9^2n - 1

Let $n \in \Z_{\ge 0}$ be a non-negative integer.
Then:
:$80 \divides 9^{2 n} - 1$
where $\divides$ denotes divisibility.

Proof:
From Integer Less One divides Power Less One, we have that:
:$\forall m, n \in \Z: \paren {m - 1} \divides \paren {m^n - 1}$
This result is the special case where $m = 9^2$.
{{qed}}
Theorem: Divisor of Integer/Examples/63 divides 8^2n - 1

Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$63 \divides 8^{2 n} - 1$
where $\divides$ denotes divisibility.

Proof:
Proof by induction:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$63 \divides 8^{2 n} - 1$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = 8^{2 \times 0} - 1
      | r = 8^0 - 1
      | c = 
}}
{{eqn | r = 1 - 1
      | c = Zeroth Power of Real Number equals One
}}
{{eqn | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 63
      | o = \divides
      | r = 8^{2 \times 0} - 1
      | c = Integer Divides Zero
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = 8^{2 \times 1} - 1
      | r = 8^2 - 1
      | c = 
}}
{{eqn | r = 64 - 1
      | c = 
}}
{{eqn | r = 63
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 63
      | o = \divides
      | r = 8^{2 \times 1} - 1
      | c = Integer Divides Itself
}}
{{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:
:$63 \divides 8^{2 k} - 1$
from which it is to be shown that:
:$63 \divides 8^{2 \paren {k + 1} } - 1$
=== Induction Step ===
This is the induction step:
From the induction hypothesis we have that:
:$63 \divides 8^{2 k} - 1$
Hence by definition of divisibility, we have:
:$\exists r \in \Z: 8^{2 k} - 1 = 63 r$
and so:
:$(1): \quad \exists r \in \Z: 8^{2 k} = 63 r + 1$
{{begin-eqn}}
{{eqn | l = 8^{2 \paren {k + 1} } - 1
      | r = 8^2 \times 8^{2 k} - 1
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists r \in \Z
      | l = 8^{2 \paren {k + 1} } - 1
      | r = 64 \times \paren {63 r + 1} - 1
      | c = from $(1)$
}}
{{eqn | r = 64 \times 63 r + 63
      | c = algebra
}}
{{eqn | r = 63 \paren {64 r + 1}
      | c = algebra
}}
{{eqn | ll= \leadsto
      | l = 63
      | o = \divides
      | r = 8^{2 \paren {k + 1} } - 1
      | c = {{Defof|Divisor of Integer}}
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 0}: 63 \divides 8^{2 n} - 1$
{{qed}}
Theorem: Divisor of Integer/Examples/63 divides 8^2n - 1

Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$63 \divides 8^{2 n} - 1$
where $\divides$ denotes divisibility.

Proof:
From Integer Less One divides Power Less One, we have that:
:$\forall m, n \in \Z: \paren {m - 1} \divides \paren {m^n - 1}$
This result is the special case where $m = 8^2$.
{{qed}}
Theorem: Divisor of Integer/Examples/6 divides 7^n - 1

Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$6 \divides 7^n - 1$
where $\divides$ denotes divisibility.

Proof:
From Integer Less One divides Power Less One, we have that:
:$\forall m, n \in \Z: \paren {m - 1} \divides \paren {m^n - 1}$
This result is the special case where $m = 7$.
{{qed}}
Theorem: Divisor of Integer/Examples/6 divides n (n+1) (n+2)

Let $n$ be an integer.
Then:
:$6 \divides n \paren {n + 1} \paren {n + 2}$

Proof:
From $3$ divides $n \paren {n + 1} \paren {n + 2}$:
:$3 \divides n \paren {n + 1} \paren {n + 2}$
From $2$ divides $n \paren {n + 1}$:
:$2 \divides n \paren {n + 1}$
and so:
:$2 \divides n \paren {n + 1} \paren {n + 2}$
Hence:
:$2 \times 3 = 6 \divides \paren {n + 1} \paren {n + 2}$
{{qed}}
Theorem: Divisor of Integer/Examples/6 divides n (n+1) (n+2)

Let $n$ be an integer.
Then:
:$6 \divides n \paren {n + 1} \paren {n + 2}$

Proof:
Proof by induction:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$6 \divides n \paren {n + 1} \paren {n + 2}$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = 0 \times 1 \times 2
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 6
      | o = \divides
      | r = 0 \paren {0 + 1} \paren {0 + 2}
      | c = Integer Divides Zero
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = 1 \paren {1 + 1} \paren {1 + 2}
      | r = 1 \times 2 \times 3
      | c = 
}}
{{eqn | r = 6
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 6
      | o = \divides
      | r = 1 \paren {1 + 1} \paren {1 + 2}
      | c = Integer Divides Itself
}}
{{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:
:$6 \divides k \paren {k + 1} \paren {k + 2}$
from which it is to be shown that:
:$6 \divides \paren {k + 1} \paren {k + 2} \paren {k + 3}$
=== Induction Step ===
This is the induction step:
From the induction hypothesis we have that:
:$6 \divides k \paren {k + 1} \paren {k + 2}$
Hence by definition of divisibility, we have:
:$(1): \quad \exists r \in \Z: k \paren {k + 1} \paren {k + 2} = 6 r$
From $2$ divides $n \paren {n + 1}$ we have:
:$(2): \quad \exists s \in \Z: \paren {k + 1} \paren {k + 2} = 2 s$
{{begin-eqn}}
{{eqn | l = \paren {k + 1} \paren {k + 2} \paren {k + 3}
      | r = k \paren {k + 1} \paren {k + 2} + 3 \paren {k + 1} \paren {k + 2}
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists r \in \Z
      | l = \paren {k + 1} \paren {k + 2} \paren {k + 3}
      | r =  6 r + 3 \times 2 s
      | c = from $(1)$ and $(2)$
}}
{{eqn | r = 7 \times 6 r + 6
      | c = algebra
}}
{{eqn | r = 6 \paren {r + s}
      | c = algebra
}}
{{eqn | ll= \leadsto
      | l = 6
      | o = \divides
      | r = \paren {k + 1} \paren {k + 2} \paren {k + 3}
      | c = {{Defof|Divisor of Integer}}
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \Z_{\ge 0}: 6 \divides n \paren {n + 1} \paren {n + 2}$
{{qed}}
Theorem: Unique Point of Minimal Distance to Closed Linear Subspace of Hilbert Space iff Orthogonal

Let $H$ be a Hilbert space, and let $h \in H$.
Let $K \subseteq H$ be a closed linear subspace of $H$.
Then the unique point $k_0 \in K$ from Unique Point of Minimal Distance to Closed Convex Subset of Hilbert Space such that:
:$\norm {h - k_0} = \map d {h, K}$
where $d$ denotes distance to a set, is characterised by:
:$\norm {h - k_0} = \map d {h, K} \iff \paren {h - k_0} \perp K$
where $\perp$ signifies orthogonality.

Proof:
=== Necessary Condition ===
Suppose that:
:$\ds \norm {h - k_0} = \map d {h, K} = \inf_{k \in K} \norm {h - k}$
Let $k \in K$. 
Since $K$ is a linear subspace, we have $k_0 + k \in K$. 
Hence, we have:
:$\norm {h - k_0}^2 \le \norm {h - \paren {k_0 + k} }^2 = \norm {\paren {h - k_0} - k}^2$
From Square of Inner Product Norm of Sum, we have:
:$\norm {\paren {h - k_0} - k}^2 = \norm {h - k_0}^2 - 2 \map \Re {\innerprod {h - k_0} k} + \norm k^2$ 
Hence:
:$\norm {h - k_0}^2 \le \norm {h - k_0}^2 - 2 \map \Re {\innerprod {h - k_0} k} + \norm k^2$
so that:
:$2 \map \Re {\innerprod {h - k_0} k} \le \norm k^2$ 
for each $k \in K$. 
Let:
:$r = \cmod {\innerprod {h - k_0} k}$
and:
:$\theta = \map \arg {\innerprod {h - k_0} k}$
so that:
:$\innerprod {h - k_0} k = r e^{i \theta}$ 
Let $t > 0$. 
Now, we have from Inner Product is Sesquilinear:
:$\innerprod {h - k_0} {t e^{i \theta} k} = t e^{-i \theta} \paren {r e^{i \theta} } = t r$ 
Since $\norm {t e^{i \theta} k }^2 = t^2 \norm k^2$ from {{NormAxiomVector|2}}, we therefore have:
:$t r \le t^2 \norm k^2$ 
Dividing by $t$ we have:
:$r \le t \norm k^2$ 
Taking $t \to 0^+$, we have $r \le 0$. 
Since we also have $r \ge 0$, we have $r = 0$. 
Hence we have $\innerprod {h - k_0} k = 0$ so that $h - k_0 \perp k$. 
Since $k \in K$ was arbitrary, we have $h - k_0 \perp K$. 
{{qed|lemma}}
Theorem: Hyperbolic Sine of Zero is Zero

:$\map \sinh 0 = 0$
where $\sinh$ denotes the hyperbolic sine.

Proof:
{{begin-eqn}}
{{eqn | l = \map \sinh 0
      | r = \dfrac {e^0 - e^{-0} } 2
      | c = {{Defof|Hyperbolic Sine}}
}}
{{eqn | r = \dfrac {1 - 1} 2
      | c = {{Defof|Integer Power}}
}}
{{eqn | r = 0
      | c = 
}}
{{end-eqn}}
{{qed}}