avewright/proofwiki-math huggingface dataset:
Theorem: Sum of Geometric Sequence

Let $x$ be an element of one of the standard number fields: $\Q, \R, \C$ such that $x \ne 1$.
Let $n \in \N_{>0}$.
Then:
:$\ds \sum_{j \mathop = 0}^{n - 1} x^j = \frac {x^n - 1} {x - 1}$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{0 \mathop \le j \mathop < n} a r^j
      | r = a + \sum_{1 \mathop \le j \mathop < n} a r^j
      | c = 
}}
{{eqn | r = a + r \sum_{1 \mathop \le j \mathop < n} a r^{j-1}
      | c = Distributive Property
}}
{{eqn | r = a + r \sum_{0 \mathop \le j \mathop < n - 1} a r^j
      | c = Exchange of Order of Summation
}}
{{eqn | r = a + r \sum_{0 \mathop \le j \mathop < n} a r^j - a r^n
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \paren {1 - r} \sum_{0 \mathop \le j \mathop < n} a r^j
      | r = a - a r^n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sum_{j \mathop = 0}^{n - 1} a r^j
      | r = \frac {a \paren {1 - r^n} } {1 - r}
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Sum of Geometric Sequence

Let $x$ be an element of one of the standard number fields: $\Q, \R, \C$ such that $x \ne 1$.
Let $n \in \N_{>0}$.
Then:
:$\ds \sum_{j \mathop = 0}^{n - 1} x^j = \frac {x^n - 1} {x - 1}$

Proof:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\ds \sum_{j \mathop = 0}^{n - 1} x^j = \frac {x^n - 1} {x - 1}$
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = \dfrac {x^1 - 1} {x - 1}
      | r = 1
      | c = 
}}
{{eqn | r = 2^0
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 0}^{1 - 1} x^j
      | c = 
}}
{{end-eqn}}
so $\map P 1$ holds.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show 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 our induction hypothesis:
:$\ds \sum_{j \mathop = 0}^{k - 1} x^j = \frac {x^k - 1} {x - 1}$
Then we need to show:
:$\ds \sum_{j \mathop = 0}^k x^j = \frac {x^{k + 1} - 1} {x - 1}$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 0}^k x^j
      | r = \sum_{j \mathop = 0}^{k - 1} x^j + x^k
      | c = 
}}
{{eqn | r = \frac {x^k - 1} {x - 1} + x^k
      | c = 
}}
{{eqn | r = \frac {x^k - 1 + \paren {x - 1} x^k} {x - 1}
      | c = 
}}
{{eqn | r = \frac {x^k - 1 + x^{k + 1} - x^k} {x - 1}
      | c = 
}}
{{eqn | r = \frac {x^{k + 1} - 1} {x - 1}
      | c = 
}}
{{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 \N_{>0}: \sum_{j \mathop = 0}^{n - 1} x^j = \frac {x^n - 1} {x - 1}$
{{qed}}
Theorem: Sum of Geometric Sequence

Let $x$ be an element of one of the standard number fields: $\Q, \R, \C$ such that $x \ne 1$.
Let $n \in \N_{>0}$.
Then:
:$\ds \sum_{j \mathop = 0}^{n - 1} x^j = \frac {x^n - 1} {x - 1}$

Proof:
Let $\ds S_n = \sum_{j \mathop = 0}^{n - 1} x^j$.
Then:
{{begin-eqn}}
{{eqn | l = \paren {x - 1} S_n
      | r = x S_n - S_n
      | c = 
}}
{{eqn | r = x \sum_{j \mathop = 0}^{n - 1} x^j - \sum_{j \mathop = 0}^{n - 1} x^j
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 1}^n x^j - \sum_{j \mathop = 0}^{n - 1} x^j
      | c = 
}}
{{eqn | r = x^n + \sum_{j \mathop = 1}^{n - 1} x^j - \paren {x^0 + \sum_{j \mathop = 1}^{n - 1} x^j}
      | c = 
}}
{{eqn | r = x^n - x^0
      | c = 
}}
{{eqn | r = x^n - 1
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
Theorem: Sum of Geometric Sequence

Let $x$ be an element of one of the standard number fields: $\Q, \R, \C$ such that $x \ne 1$.
Let $n \in \N_{>0}$.
Then:
:$\ds \sum_{j \mathop = 0}^{n - 1} x^j = \frac {x^n - 1} {x - 1}$

Proof:
From Difference of Two Powers:
:$\ds a^n - b^n = \paren {a - b} \paren {a^{n - 1} + a^{n - 2} b + a^{n - 3} b^2 + \ldots + a b^{n - 2} + b^{n - 1} } = \paren {a - b} \sum_{j \mathop = 0}^{n - 1} a^{n - j - 1} b^j$
Set $a = x$ and $b = 1$:
:$\ds x^n - 1 = \paren {x - 1} \paren {x^{n - 1} + x^{n - 2} + \cdots + x + 1} = \paren {x - 1} \sum_{j \mathop = 0}^{n - 1} x^j$
from which the result follows directly.
{{qed}}
Theorem: Sum of Geometric Sequence

Let $x$ be an element of one of the standard number fields: $\Q, \R, \C$ such that $x \ne 1$.
Let $n \in \N_{>0}$.
Then:
:$\ds \sum_{j \mathop = 0}^{n - 1} x^j = \frac {x^n - 1} {x - 1}$

Proof:
=== Lemma ===
{{:Sum of Geometric Sequence/Proof 4/Lemma}}{{qed|lemma}}
Then by the lemma:
{{begin-eqn}}
{{eqn | l = \paren {1 - x} \sum_{i \mathop = 0}^{n - 1} x^i
      | r = 1 - x^n
}}
{{eqn | ll= \leadsto
      | l = \sum_{i \mathop = 0}^{n - 1} x^i = \frac {1 - x^n} {1 - x}
      | r = \frac {x^n - 1} {x - 1}
}}
{{end-eqn}}
{{qed}}
Theorem: Congruence of Sum of Digits to Base Less 1

Let $x \in \Z$, and $b \in \N, b > 1$.
Let $x$ be written in base $b$:
:$x = \sqbrk {r_m r_{m - 1} \ldots r_2 r_1 r_0}_b$
Then:
:$\ds \map {s_b} x = \sum_{j \mathop = 0}^m r_j \equiv x \pmod {b - 1}$
where $\map {s_b} x$ is the digit sum of $x$ in base $b$ notation.
That is, the digit sum of any integer $x$ in base $b$ notation is congruent to $x$ modulo $b - 1$.

Proof:
Let $x \in \Z, x > 0$, and $b \in \N, b > 1$.
Then from the Basis Representation Theorem, $x$ can be expressed uniquely as:
:$\ds x = \sum_{j \mathop = 0}^m r_j b^j, r_0, r_1, \ldots, r_m \in \set {0, 1, \ldots, b - 1}$
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition $\ds \sum_{j \mathop = 0}^n r_j \equiv x \pmod {b - 1}$.
Theorem: Euler Phi Function of Integer

Let $n \in \Z_{>0}$, that is, a (strictly) positive integer.
Let $\phi: \Z_{>0} \to \Z_{>0}$ be the Euler $\phi$ function.
Then for any $n \in \Z_{>0}$, we have:
:$\map \phi n = n \paren {1 - \dfrac 1 {p_1} } \paren {1 - \dfrac 1 {p_2} } \cdots \paren {1 - \dfrac 1 {p_r} }$
where $p_1, p_2, \ldots, p_r$ are the distinct primes dividing $n$.
Or, more compactly:
:$\ds \map \phi n = n \prod_{p \mathop \divides n} \paren {1 - \frac 1 p}$
where $p \divides n$ denotes the primes which divide $n$.

Proof:
If $n = 1$ the result holds by inspection.
Let $n \ge 2$.
We express $n$ in its prime decomposition:
:$n = p_1^{k_1} p_2^{k_2} \cdots p_r^{k_r}, p_1 < p_2 < \cdots < p_r$
as it is always possible to do.
By definition, all primes are coprime to each other.
Hence from Euler Phi Function is Multiplicative:
:$\map \phi n = \map \phi {p_1^{k_1} } \map \phi {p_2^{k_2} } \cdots \map \phi {p_r^{k_r} }$
and from Euler Phi Function of Prime Power:
:$\map \phi {p^k} = p^k \paren {1 - \dfrac 1 p}$
So:
:$\map \phi n = p_1^{k_1} \paren {1 - \dfrac 1 {p_1} } p_2^{k_2} \paren {1 - \dfrac 1 {p_2} } \cdots p_r^{k_r} \paren {1 - \dfrac 1 {p_r} }$
and the result follows directly from:
:$n = p_1^{k_1} p_2^{k_2} \cdots p_r^{k_r}$
{{qed}}
Theorem: Euler Phi Function is Multiplicative

The Euler $\phi$ function is a multiplicative function:
:$m \perp n \implies \map \phi {m n} = \map \phi m \map \phi n$
where $m, n \in \Z_{>0}$.

Proof:
From Euler Phi Function of Product, we have:
:$\map \phi {m n} = \map \phi m \map \phi n \paren {\dfrac {\map \gcd {m, n} } {\map \phi {\map \gcd {m, n} } } }$
From hypothesis, we have:
:$\map \gcd {m, n} = 1$
From Euler Phi Function of 1, we have $\map \phi 1 = 1$, giving the result.
{{qed}}
Theorem: Euler Phi Function of Prime Power

Let $p^n$ be a prime power for some prime number $p > 1$.
Then:
:$\map \phi {p^n} = p^n \paren {1 - \dfrac 1 p} = \paren {p - 1} p^{n - 1}$
where $\phi: \Z_{>0} \to \Z_{>0}$ is the Euler $\phi$ function.

Proof:
From Euler Phi Function of Prime:
:$\map \phi p = p - 1$
From Prime not Divisor implies Coprime:
:$k \perp p^n \iff p \nmid k$
There are $p^{n - 1}$ integers $k$ such that $1 \le k \le p^n$ which are divisible by $p$:
:$k \in \set {p, 2 p, 3 p, \ldots, \paren {p^{n - 1} } p}$
Therefore:
:$\map \phi {p^n} = p^n - p^{n - 1} = p^n \paren {1 - \dfrac 1 p} = \paren {p - 1} p^{n - 1}$
{{qed}}
Theorem: Sum of Euler Phi Function over Divisors

Let $n \in \Z_{>0}$ be a strictly positive integer.
Then $\ds \sum_{d \mathop \divides n} \map \phi d = n$
where:
:$\ds \sum_{d \mathop \divides n}$ denotes the sum over all of the divisors of $n$
:$\map \phi d$ is the Euler $\phi$ function, the number of integers less than $d$ that are prime to $d$.
That is, the total of all the totients of all divisors of a number equals that number.

Proof:
Let us define:
:$S_d = \set {m \in \Z: 1 \le m \le n, \gcd \set {m, n} = d}$.
That is, $S_d$ is all the numbers less than or equal to $n$ whose GCD with $n$ is $d$.
Now from Integers Divided by GCD are Coprime we have:
:$\gcd \set {m, n} = d \iff \dfrac m d, \dfrac n d \in \Z: \dfrac m d \perp \dfrac n d$
So the number of integers in $S_d$ equals the number of positive integers no bigger than $\dfrac n d$ which are prime to $\dfrac n d$.
That is, by definition of the Euler phi function:
:$\card {S_d} = \map \phi {\dfrac n d}$
From the definition of the $S_d$, it follows that for all $1 \le m \le n$:
:$\exists d \divides n: m \in S_d$
Therefore:
:$\ds \set {1, \ldots, n} = \bigcup_{d \mathop \divides n} S_d$
Moreover, it follows from the definition of the $S_d$ that they are pairwise disjoint.
Now from {{Corollary|Cardinality of Set Union}}, it follows that:
{{begin-eqn}}
{{eqn | l = n 
      | r = \sum_{d \mathop \divides n} \card {S_d}
}}
{{eqn | r = \sum_{d \mathop \divides n} \map \phi {\dfrac n d}
}}
{{end-eqn}}
But from Sum Over Divisors Equals Sum Over Quotients:
:$\ds \sum_{d \mathop \divides n} \map \phi {\frac n d} = \sum_{d \mathop \divides n} \map \phi d$
and hence the result.
{{qed}}
Theorem: Möbius Function is Multiplicative

The Möbius function $\mu$  is a multiplicative function:
:$m \perp n \implies \map \mu {m n} = \map \mu m \map \mu n$
where $m, n \in \Z_{>0}$.

Proof:
First note that we have $\map \mu 1 = 1$, which agrees with Value of Multiplicative Function at One.
Let $m, n \in \Z_{>0}$ such that $m \perp n$.
First, suppose that either $\map \mu m = 0$ or $\map \mu n = 0$.
Then either $m$ or $n$ has a factor $p^2$ where $p$ is prime.
Thus it will follow that $m n$ will also have a factor $p^2$ and hence $\map \mu {m n} = 0$.
So the result holds when $\map \mu m = 0$ or $\map \mu n = 0$.
Now suppose that $\map \mu m \ne 0$ and $\map \mu n \ne 0$.
Let $m = p_1 p_2 \ldots p_r$, $n = q_1 q_2 \ldots q_s$ where all the $p_i, q_j$ are prime.
Then:
:$m n = p_1 p_2 \ldots p_r q_1 q_2 \ldots q_s$
As $m \perp n$ it follows that:
:$\forall i, j: p_i \ne q_j$
Hence there is no prime in $m n$ whose power is higher than $1$, which means that $\map \mu {m n} \ne 0$.
So:
:$\map \mu {m n} = \paren {-1}^{r + s} = \paren {-1}^r \paren {-1}^s = \map \mu m \map \mu n$
Hence the result.
{{qed}}
Theorem: Euler Phi Function in terms of Möbius Function

Let $n \in \Z_{>0}$ be a strictly positive integer.
Then:
:$\ds \sum_{d \mathop \divides n} \map \mu d \frac n d = \map \phi n$
where:
:$\ds \sum_{d \mathop \divides n}$ denotes the sum over all of the divisors of $n$
:$\map \phi n$ is the Euler $\phi$ function, the number of integers less than $n$ that are prime to $n$
:$\map \mu d$ is the Möbius function.
Equivalently, this says that:
:$\phi = \mu * I_{\Z_{>0} }$
where:
:$*$ denotes Dirichlet convolution
:$I_{\Z_{>0} }$ denotes the identity mapping on $\Z_{>0}$, that is:
::$\forall n \in \Z_{>0}: I_{\Z_{>0} }: n \mapsto n$
{{wtd|Add a link to a page proving this equivalence.}}

Proof:
Sum of Möbius Function over Divisors says:
{{:Sum of Möbius Function over Divisors}}{{qed|lemma}}
Let $\map 1 k = 1$ be the constant mapping.
Then $\phi$ is defined as:
:$\ds \map \phi n = \sum_{\substack {k \mathop \perp n \\ 1 \mathop \le k \mathop \le n}} \map 1 k$
We have that $\floor {\dfrac 1 {\gcd \set {n, k} } }$ is $1$ if $k \perp n$ and $0$ otherwise.
Thus we can rewrite the above summation as:
:$\ds \sum_{k \mathop = 1}^n \floor {\frac 1 {\gcd \set {n, k} } }$
Now we may use Sum of Möbius Function over Divisors, with $\gcd \set {n, k}$ replacing $n$, to get:
{{begin-eqn}}
{{eqn | l = \map \phi n
      | r = \sum_{k \mathop = 1}^n \paren {\sum_{d \mathop \divides \gcd \set {n, k} } \map \mu d}
      | c = 
}}
{{eqn | r = \sum_{k \mathop = 1}^n \sum_{\substack {d \mathop \divides n \\ d \mathop \divides k} } \map \mu d
      | c = 
}}
{{end-eqn}}
For a fixed divisor $d$ of $n$, we must sum over all those $k$ in the range $1 \le k \le n$ which are multiples of $d$.
If we write $k = q d$, then $1 \le k \le n$ {{iff}} $1 \le q \le \dfrac n d$.  
Hence the last sum for $\map \phi n$ can be written as:
{{begin-eqn}}
{{eqn | l = \map \phi n
      | r = \sum_{d \mathop \divides n} \paren {\sum_{q \mathop = 1}^{\tfrac n d} \map \mu d}
      | c = 
}}
{{eqn | r = \sum_{d \mathop \divides n} \map \mu d \sum_{q \mathop = 1}^{\tfrac n d} \map 1 q
      | c = 
}}
{{eqn | r = \sum_{d \mathop \divides n} \map \mu d \frac n d
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Binomial Coefficient of Prime

Let $p$ be a prime number.
Then:
:$\forall k \in \Z: 0 < k < p: \dbinom p k \equiv 0 \pmod p$
where $\dbinom p k$ is defined as a binomial coefficient.

Proof:
Because:
:$\dbinom p k = \dfrac {p \paren {p - 1} \paren {p - 2} \cdots \paren {p - k + 1} } {k!}$
is an integer, we have that:
:$k! \divides p \paren {p - 1} \paren {p - 2} \cdots \paren {p - k + 1}$
But because $k < p$ it follows that:
:$k! \mathrel \perp p$
that is, that:
:$\gcd \set {k!, p} = 1$
So by Euclid's Lemma:
:$k! \divides \paren {p - 1} \paren {p - 2} \cdots \paren {p - k + 1}$
Hence:
:$\dbinom p k = p \dfrac {\paren {p - 1} \paren {p - 2} \cdots \paren {p - k + 1} } {k!}$
Hence the result.
{{qed}}
Theorem: Binomial Coefficient of Prime

Let $p$ be a prime number.
Then:
:$\forall k \in \Z: 0 < k < p: \dbinom p k \equiv 0 \pmod p$
where $\dbinom p k$ is defined as a binomial coefficient.

Proof:
Lucas' Theorem gives:
:$\dbinom n k \equiv \dbinom {\floor {n / p} } {\floor {k / p} } \dbinom {n \bmod p} {k \bmod p} \pmod p$
So, substituting $p$ for $n$:
:$\dbinom p k \equiv \dbinom {\floor {p / p} } {\floor {k / p} } \dbinom {p \bmod p} {k \bmod p} \pmod p$
But $p \bmod p = 0$ by definition.
Hence, if $0 < k < p$, we have that:
:$k \bmod p \ne 0$
and so:
:$\dbinom {p \bmod p} {k \bmod p} = \dbinom 0 {k \bmod p} = 0$
by definition of binomial coefficients.
The result follows immediately.
{{qed}}
Theorem: Binomial Coefficient of Prime

Let $p$ be a prime number.
Then:
:$\forall k \in \Z: 0 < k < p: \dbinom p k \equiv 0 \pmod p$
where $\dbinom p k$ is defined as a binomial coefficient.

Proof:
By the definition of binomial coefficient:
{{begin-eqn}}
{{eqn | l = \binom p k
      | r = \frac {p!} {k! \paren {n - k}!}
}}
{{eqn | ll= \leadstoandfrom
      | l = p!
      | r = k! \paren {p - k}! \binom p k
}}
{{end-eqn}}
Now, $p$ divides the {{LHS}} by Divisors of Factorial.
So $p$ must also divide the {{RHS}}.
By hypothesis $k < p$.
We have that:
:$k! = k \paren {k - 1} \dotsm \paren 2 \paren 1$
We also have that $p$ is prime, and each factor is less than $p$.
Thus $p$ is not a factor of $k!$.
Similarly:
:$\paren {p - k}! = \paren {p - k} \paren {p - k - 1} \dotsm \paren 2 \paren 1$
It follows, by the same reasoning as above, that $p$ is also not a factor of $\paren {p - k}!$.
The result then follows from Euclid's Lemma.
{{qed}}
Theorem: Prime Power of Sum Modulo Prime

Let $p$ be a prime number.
Then:
:$\forall n \in \N_{> 0}: \paren {a + b}^{p^n} \equiv a^{p^n} + b^{p^n} \pmod p$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\paren {a + b}^{p^n} \equiv a^{p^n} + b^{p^n} \pmod p$
Theorem: Binomial Coefficient involving Power of Prime

: $\dbinom {p^n k} {p^n} \equiv k \pmod p$
where $\dbinom {p^n k} {p^n}$ is a binomial coefficient.

Proof:
From  Prime Power of Sum Modulo Prime we have:
:$(1): \quad \paren {a + b}^{p^n} \equiv \paren {a^{p^n} + b^{p^n} } \pmod p$
We can write this:
:$\paren {a + b}^{p^n k} = \paren {\paren {a + b}^{p^n} }^k$
By $(1)$ and Congruence of Powers, we therefore have:
:$\paren {a + b}^{p^n k} \equiv \paren {a^{p^n} + b^{p^n} }^k \pmod p$
The coefficient $\dbinom {p^n k} {p^n}$ is the binomial coefficient of $b^{p^n}$ in $\paren {a + b}^{p^n k} = \paren {\paren {a + b}^{p^n} }^k$.
Expanding $\paren {a^{p^n} + b^{p^n} }^k$ using the Binomial Theorem, we find that the coefficient of $b^{p^n}$, the second term, is $\dbinom k 1 = k$.
So:
:$\dbinom {p^n k} {p^n} \equiv k \pmod p$
{{qed}}
Theorem: Binomial Coefficient involving Power of Prime

: $\dbinom {p^n k} {p^n} \equiv k \pmod p$
where $\dbinom {p^n k} {p^n}$ is a binomial coefficient.

Proof:
Lucas' Theorem states that for $n, k, p \in \Z$ and $p$ be a prime number, such that:
:$n = a_r p^r + \cdots + a_1 p + a_0$
:$k = b_r p^r + \cdots + b_1 p + b_0$
then:
:$\ds \binom n k \equiv \prod_{j \mathop = 0}^r \binom {a_j}{b_j} \pmod p$
Therefore:
{{begin-eqn}}
{{eqn | l = \binom {p^n k} {p^n}
      | o = \equiv
      | r = \binom k 1 \prod_{j \mathop = 0}^{n - 1} \binom 0 0 \pmod p
      | c = Lucas' Theorem
}}
{{eqn | o = \equiv
      | r = k \prod_{j \mathop = 0}^{n - 1} 1 \pmod p
      | c = Binomial Coefficient with One, Binomial Coefficient with Zero
}}
{{eqn | o = \equiv
      | r = k \pmod p
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Cassini's Identity

:$F_{n + 1} F_{n - 1} - F_n^2 = \paren {-1}^n$

Proof:
=== Basis for the Induction ===
We see that:
: $F_2 F_0 - F_1^2 = 1 \times 0 - 1 = -1 = \paren {-1}^1$
so the proposition holds for $n = 1$.
We also see that:
: $F_3 F_1 - F_2^2 = 2 \times 1 - 1 = \paren {-1}^2$
so the proposition holds for $n = 2$.
=== Induction Hypothesis ===
Suppose the proposition is true for $n = k$, that is:
: $F_{k + 1} F_{k - 1} - F_k^2 = \paren {-1}^k$
=== Induction Step ===
It remains to be shown that it follows from this that the proposition is true for $n = k + 1$, that is:
: $F_{k + 2} F_k - F_{k + 1}^2 = \paren {-1}^{k + 1}$
So:
{{begin-eqn}}
{{eqn | l = F_{k + 2} F_k - F_{k + 1}^2
      | r = \paren {F_k + F_{k + 1} } F_k - F_{k + 1}^2
}}
{{eqn | r = F_k^2 + F_k F_{k + 1} - F_{k + 1}^2
}}
{{eqn | r = F_k^2 + F_k F_{k + 1} - F_{k + 1} \paren {F_k + F_{k - 1} }
}}
{{eqn | r = F_k^2 + F_k F_{k + 1} - F_k F_{k + 1} - F_{k + 1} F_{k - 1}
}}
{{eqn | r = F_k^2 - F_{k + 1} F_{k - 1}
}}
{{eqn | r = \paren {-1} \paren {F_{k + 1} F_{k - 1} - F_k^2}
}}
{{eqn | r = \paren {-1} \paren {-1}^k
}}
{{eqn | r = \paren {-1}^{k + 1}
}}
{{end-eqn}}
By the Principle of Mathematical Induction, the proof is complete.
{{qed}}
Note that from the above we have that:
: $F_{k + 2} F_k - F_{k + 1}^2 = \paren {-1}^{k + 1}$
from which:
: $F_{n + 1}^2 - F_n F_{n + 2} = \paren {-1}^n$
follows immediately.
Theorem: Cassini's Identity

:$F_{n + 1} F_{n - 1} - F_n^2 = \paren {-1}^n$

Proof:
First we use this {{Lemma|Cassini's Identity}}:
=== Lemma ===
{{:Cassini's Identity/Lemma}}{{qed|lemma}}
Then the determinant of both sides is taken.
The {{LHS}} follows directly from Determinant of Order 2:
:<nowiki>$\begin{bmatrix}
F_{n + 1}  & F_n     \\
F_n        & F_{n - 1}
\end{bmatrix} = F_{n + 1} F_{n - 1} - F_n^2$</nowiki>
Now for the {{RHS}}:
==== Basis for the Induction ====
:<nowiki>$\begin{vmatrix}
1 & 1 \\
1 & 0
\end{vmatrix} = 1 \times 0 - 1 \times 1 = -1 = \paren {-1}^1$</nowiki>
==== Induction Hypothesis ====
For $k \in \Z_{>0}$, it is assumed that:
:<nowiki>$\begin{vmatrix}
1 & 1 \\
1 & 0
\end{vmatrix}^k = \paren {-1}^k$</nowiki>
It remains to be shown that:
:$<nowiki>\begin{vmatrix}
1 & 1 \\
1 & 0
\end{vmatrix}^{k + 1} = \paren {-1}^{k + 1}$</nowiki>
==== Induction Step ====
The induction step follows from Determinant of Matrix Product:
:$<nowiki>\begin{vmatrix}
1 & 1 \\
1 & 0
\end{vmatrix}^{k+1} = \begin{vmatrix}
1 & 1 \\
1 & 0
\end{vmatrix}^k \begin{vmatrix}
1 & 1 \\
1 & 0
\end{vmatrix} = \paren {-1}^k \paren {-1} = \paren {-1}^{k + 1}$</nowiki>
Hence by induction:
:$<nowiki>\forall n \in \Z_{>0}: \begin{vmatrix}
1 & 1 \\
1 & 0
\end{vmatrix}^n = \paren {-1}^n$</nowiki>
{{qed}}
Theorem: Rational Numbers are Countably Infinite

The set $\Q$ of rational numbers is countably infinite.

Proof:
The rational numbers are arranged thus:
:$\dfrac 0 1, \dfrac 1 1, \dfrac {-1} 1, \dfrac 1 2, \dfrac {-1} 2, \dfrac 2 1, \dfrac {-2} 1, \dfrac 1 3, \dfrac 2 3,  \dfrac {-1} 3, \dfrac {-2} 3, \dfrac 3 1, \dfrac 3 2, \dfrac {-3} 1, \dfrac {-3} 2, \dfrac 1 4, \dfrac 3 4, \dfrac {-1} 4, \dfrac {-3} 4, \dfrac 4 1, \dfrac 4 3, \dfrac {-4} 1, \dfrac {-4} 3 \ldots$
{{Explain|What is the pattern in the above arrangement?}}
It is clear that every rational number will appear somewhere in this list.
Thus it is possible to set up a bijection between each rational number and its position in the list, which is an element of $\N$.
{{qed}}
Theorem: Rational Numbers are Countably Infinite

The set $\Q$ of rational numbers is countably infinite.

Proof:
Let us define the mapping $\phi: \Q \to \Z \times \N$ as follows:
:$\forall \dfrac p q \in \Q: \phi \left({\dfrac p q}\right) = \left({p, q}\right)$
where $\dfrac p q$ is in canonical form.
Then $\phi$ is clearly injective.
From Cartesian Product of Countable Sets is Countable, we have that $\Z \times \N$ is countably infinite.
The result follows directly from Domain of Injection to Countable Set is Countable.
{{qed}}
Theorem: Rational Numbers are Countably Infinite

The set $\Q$ of rational numbers is countably infinite.

Proof:
For each $n \in \N$, define $S_n$ to be the set:
:$S_n := \set {\dfrac m n: m \in \Z}$
By Integers are Countably Infinite, each $S_n$ is countably infinite.
Because each rational number can be written down with a positive denominator, it follows that:
:$\forall q \in \Q: \exists n \in \N: q \in S_n$
which is to say:
:$\ds \bigcup_{n \mathop \in \N} S_n = \Q$
By Countable Union of Countable Sets is Countable, it follows that $\Q$ is countable.
Since $\Q$ is manifestly infinite, it is countably infinite.
{{qed}}
Theorem: Rational Numbers are Countably Infinite

The set $\Q$ of rational numbers is countably infinite.

Proof:
Let $Q_\pm = \set {q \in \Q: \pm q > 0}$.
For every $q \in Q_+$, there exists at least one pair $\tuple {m, n} \in \N \times \N$ such that $q = \dfrac m n$.
Therefore, we can find an injection $i: Q_+ \to \N \times \N$.
By Cartesian Product of Natural Numbers with Itself is Countable, $\N \times \N$ is countable.
Hence $Q_+$ is countable, by Domain of Injection to Countable Set is Countable.
The map $-: q \mapsto -q$ provides a bijection from $Q_-$ to $Q_+$, hence $Q_-$ is also countable.
Hence $\Q$ is countable.
{{qed}}
Theorem: Real Numbers form Totally Ordered Field

The set of real numbers $\R$ forms a totally ordered field under addition and multiplication: $\struct {\R, +, \times, \le}$.

Proof:
From Real Numbers form Field, we have that $\struct {\R, +, \times}$ forms a field.
From Ordering Properties of Real Numbers we have that $\struct {\R, +, \times, \le}$ is a totally ordered field.
{{qed}}
Theorem: Rational Numbers form Subfield of Real Numbers

The (ordered) field $\struct {\Q, +, \times, \le}$ of rational numbers forms a subfield of the field of real numbers $\struct {\R, +, \times, \le}$.
That is, the field of real numbers $\struct {\R, +, \times, \le}$ is an extension of the rational numbers $\struct {\Q, +, \times, \le}$.

Proof:
Recall that Rational Numbers form Totally Ordered Field.
Then from Rational Numbers form Subset of Real Numbers:
:$\Q \subseteq \R$
Hence the result by definition of subfield.
{{qed}}