avewright/proofwiki-math huggingface dataset:
Theorem: Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \Z$.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad \map P {n_0}$ is true
:$(2): \quad \forall k \in \Z: k \ge n_0 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \Z$ such that $n \ge n_0$.

Proof:
Let $M$ be the set of all $n \in \N_{>0}$ for which $\map P n$ holds.
By $(1)$ we have that $1 \in M$.
By $(2)$ we have that if $k \in M$ then $k + 1 \in M$.
From the Axiomatization of $1$-Based Natural Numbers, Axiom $(\text F)$, it follows that $M = \N_{>0}$.
{{qed}}
Theorem: Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \Z$.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad \map P {n_0}$ is true
:$(2): \quad \forall k \in \Z: k \ge n_0 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \Z$ such that $n \ge n_0$.

Proof:
We have that Natural Numbers are Non-Negative Integers.
Then we have that Integers form Well-Ordered Integral Domain.
The result follows from Induction on Well-Ordered Integral Domain.
{{qed}}
Theorem: Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \Z$.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad \map P {n_0}$ is true
:$(2): \quad \forall k \in \Z: k \ge n_0 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \Z$ such that $n \ge n_0$.

Proof:
Let $\Z_{\ge n_0}$ denote the set:
:$\Z_{\ge n_0} = \set {n \in \Z: n \ge n_0}$
Let $S$ be the set of integers defined as:
:$S = \set {n \in \Z_{\ge n_0}: \map P n}$
That is, the set of all integers for which $n \ge n_0$ and for which $\map P n$ holds.
From Subset of Set with Propositional Function we have that:
:$S \subseteq \Z_{\ge n_0}$
From $(1)$ we have that $\map P {n_0}$.
Hence $n_0 \in S$.
Let $k \in S$.
Then $\map P k$ holds.
But by $(2)$, $\map P {k + 1}$ also holds.
This implies $k + 1 \in S$.
So as:
:$S \subseteq \Z_{\ge n_0}$
and:
:$S$ satisfies $(1)$ and $(2)$
it follows by the Principle of Finite Induction that $S = \Z_{\ge n_0}$.
Hence for all $n \ge n_0$, $\map P n$ holds.
{{qed}}
Theorem: Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \Z$.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad \map P {n_0}$ is true
:$(2): \quad \forall k \in \Z: k \ge n_0 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \Z$ such that $n \ge n_0$.

Proof:
For each $n \in \N_{>0}$, let $\map {P'} n$ be defined as:
:$\map {P'} n := \map P 1 \land \dots \land \map P n$
It suffices to show that $\map {P'} n$ is true for all $n \in \N_{>0}$.
It is immediate from the assumption $\map P 1$ that $\map {P'} 1$ is true.
Now suppose that $\map {P'} n$ holds.
By $(2)$, this implies that $\map P {n + 1}$ holds as well.
Consequently, $\map {P'} n \land \map P {n + 1} = \map {P'} {n + 1}$ holds.
Thus by the Principle of Mathematical Induction:
:$\map {P'} n$ holds for all $n \in \N_{>0}$
as desired.
{{Qed}}
Theorem: Principle of Mathematical Induction

Let $\map P n$ be a propositional function depending on $n \in \Z$.
Let $n_0 \in \Z$ be given.
Suppose that:
:$(1): \quad \map P {n_0}$ is true
:$(2): \quad \forall k \in \Z: k \ge n_0 : \map P k \implies \map P {k + 1}$
Then:
:$\map P n$ is true for all $n \in \Z$ such that $n \ge n_0$.

Proof:
Let $S \subseteq \N_{>0}$ containing those $n \in \N_{>0}$ for which $\map P n$ does not hold.
{{AimForCont}} $S \ne \O$.
Then by the Well-Ordering Principle $S$ contains a minimal element $s$.
We have that $s \ne 1$ because $\map P 1$ is true from $(1)$.
Thus there must exist some $k \in \N_{>0}$ such that $s = k + 1$.
As $k + 1$ is the minimal element of $S$ it follows that all $n$ such that $n < k + 1 = s$ are not in $S$
But this means that $\map P n$ is true for all $n < s$
But by $(2)$ it follows that $\map P s$ is true.
That is, $s \notin S$.
This contradicts our assertion that $s \in S$.
Hence our assumption that $S \ne \O$ is false.
It follows by Proof by Contradiction that $S = \O$.
So $\map P n$ holds for all $n \in \N_{>0}$.
{{Qed}}
Theorem: Principle of Finite Induction

Let $n_0 \in \Z$ be given.
Let $\Z_{\ge n_0}$ denote the set:
:$\Z_{\ge n_0} = \set {n \in \Z: n \ge n_0}$
Let $S \subseteq \Z_{\ge n_0}$ be a subset of $\Z_{\ge n_0}$.
Suppose that:
:$(1): \quad n_0 \in S$
:$(2): \quad \forall n \ge n_0: n \in S \implies n + 1 \in S$
Then:
:$\forall n \ge n_0: n \in S$
That is:
:$S = \Z_{\ge n_0}$

Proof:
Consider $\N$ defined as a naturally ordered semigroup.
The result follows directly from Principle of Mathematical Induction for Naturally Ordered Semigroup: General Result.
{{qed}}
Theorem: Principle of Finite Induction

Let $n_0 \in \Z$ be given.
Let $\Z_{\ge n_0}$ denote the set:
:$\Z_{\ge n_0} = \set {n \in \Z: n \ge n_0}$
Let $S \subseteq \Z_{\ge n_0}$ be a subset of $\Z_{\ge n_0}$.
Suppose that:
:$(1): \quad n_0 \in S$
:$(2): \quad \forall n \ge n_0: n \in S \implies n + 1 \in S$
Then:
:$\forall n \ge n_0: n \in S$
That is:
:$S = \Z_{\ge n_0}$

Proof:
Let $T$ be the set of all $1$-based natural numbers not in $S$:
:$T = \N_{>0} \setminus S$
{{AimForCont}} $T$ is non-empty.
From the Well-Ordering Principle, $T$ has a smallest element.
Let this smallest element be denoted $a$.
We have been given that $1 \in S$.
So:
:$a > 1$
and so:
:$0 < a - 1 < a$
As $a$ is the smallest element of $T$, it follows that:
:$a - 1 \notin T$
That means $a - 1 \in S$.
But then by hypothesis:
:$\paren {a - 1} + 1 \in S$
But:
:$\paren {a - 1} + 1 = a$
and so $a \notin T$.
This contradicts our assumption that $a \in T$.
It follows by Proof by Contradiction that $T$ has no such smallest element.
Hence it follows that $T$ can have no elements at all.
That is:
:$\N_{>0} \setminus S = \O$
That is:
:$S = \N_{>0}$
Theorem: Principle of Finite Induction

Let $n_0 \in \Z$ be given.
Let $\Z_{\ge n_0}$ denote the set:
:$\Z_{\ge n_0} = \set {n \in \Z: n \ge n_0}$
Let $S \subseteq \Z_{\ge n_0}$ be a subset of $\Z_{\ge n_0}$.
Suppose that:
:$(1): \quad n_0 \in S$
:$(2): \quad \forall n \ge n_0: n \in S \implies n + 1 \in S$
Then:
:$\forall n \ge n_0: n \in S$
That is:
:$S = \Z_{\ge n_0}$

Proof:
Let $\Z_{\ge n_0} := \set {n \in \Z: n \ge n_0}$.
{{AimForCont}} $S \ne \Z_{\ge n_0}$.
Let $S' = \Z_{\ge n_0} \setminus S$.
Because $S \ne \Z_{\ge n_0}$ and $S \subseteq \Z_{\ge n_0}$, we have that $S' \ne \O$.
By definition, $\Z_{\ge n_0}$ is bounded below by $n_0$.
From Set of Integers Bounded Below by Integer has Smallest Element, $S'$ has a minimal element.
Let $k$ be this minimal element of $S'$.
By $(1)$ we have that:
:$n_0 \in S$
and so:
:$n_0 \notin S'$
Hence:
:$k \ne n_0$
and so:
:$k > n_0$
It follows that:
:$k - 1 \le n_0$
Because $k$ is the minimal element of $S'$:
:$k - 1 \notin S'$
and so:
:$k - 1 \in S$
But by $(2)$:
:$\paren {k - 1} + 1 = k \in S$
So we have:
:$k \in S$
and:
:$k \notin S$
Hence by Proof by Contradiction $S = \Z_{\ge n_0}$.
{{qed}}
Theorem: Principle of Finite Induction

Let $n_0 \in \Z$ be given.
Let $\Z_{\ge n_0}$ denote the set:
:$\Z_{\ge n_0} = \set {n \in \Z: n \ge n_0}$
Let $S \subseteq \Z_{\ge n_0}$ be a subset of $\Z_{\ge n_0}$.
Suppose that:
:$(1): \quad n_0 \in S$
:$(2): \quad \forall n \ge n_0: n \in S \implies n + 1 \in S$
Then:
:$\forall n \ge n_0: n \in S$
That is:
:$S = \Z_{\ge n_0}$

Proof:
{{questionable|This only takes on board a subset of $\N$, where we need a subset of $\Z$}}
Consider $\N$ defined as a naturally ordered semigroup.
The result follows directly from Principle of Mathematical Induction for Naturally Ordered Semigroup: General Result.
{{qed}}
Theorem: Principle of Mathematical Induction/Peano Structure

Let $\struct {P, s, 0}$ be a Peano structure.
Let $\map Q n$ be a propositional function depending on $n \in P$.
Suppose that:
:$(1): \quad \map Q 0$ is true
:$(2): \quad \forall n \in P: \map Q n \implies \map Q {\map s n}$
Then:
:$\forall n \in P: \map Q n$

Proof:
Let $A \subseteq P$ be defined by:
:$A := \set {n \in P: \map Q n}$
From $(1)$, $0 \in A$.
From $(2)$:
:$\forall n \in P: n \in A \implies \map s n \in A$
As this holds for all $n \in P$, it holds a fortiori for all $n \in A$.
Thus the condition:
:$n \in A \implies \map s n \in A$
is satisfied.
So by Axiom $(\text P 5)$ of the Peano Axioms:
:$A = P$
That is:
:$\forall n \in P: \map Q n$
{{qed}}
Theorem: Principle of Finite Induction/Peano Structure

Let $\struct {P, s, 0}$ be a Peano structure.
Let $S \subseteq P$.
Suppose that:
:$(1): \quad 0 \in S$
:$(2): \quad \forall n: n \in S \implies \map s n \in S$
Then:
:$S = P$

Proof:
This is nothing but a reformulation of Axiom $(P5)$ of the Peano Axioms.
{{qed}}
Category:Peano's Axioms
Category:Principle of Finite Induction
m9ssfkhi9gsur18ot0230664iewgd4i
Theorem: Principle of Mathematical Induction/Naturally Ordered Semigroup

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $T \subseteq S$ such that $0 \in T$ and $n \in T \implies n \circ 1 \in T$.
Then $T = S$.

Proof:
{{AimForCont}} that $T \subsetneq S$.
That is, $T$ is a proper subset of $S$:
: $T \ne S$
Let $T' = S \setminus T$.
Then by Set Difference with Proper Subset:
:$T' \ne \O$
By {{NOSAxiom|1}}, $S$ is well-ordered.
By definition of well-ordered set, it follows that $T'$ has a smallest element $x$.
By definition of $T$:
:$0 \in T$
and so by  definition of $T'$:
:$0 \notin T'$
so:
:$0 \prec x$
By Sum with One is Immediate Successor in Naturally Ordered Semigroup:
:$1 \preceq x$
By the definition of a naturally ordered semigroup:
:$\exists y \in S: y \circ 1 = x$
Again by Sum with One is Immediate Successor in Naturally Ordered Semigroup:
:$y \prec x$
We have that $x$ is the smallest element of $T'$ and $y \prec x$.
Therefore:
:$y \notin T'$
and so
:$y \in T$
But from the definition of $T$:
:$y \in T \implies y \circ 1 = x \in T$
But then by the definition of $T'$:
:$x \in T' \implies x \notin T$
From this contradiction, it follows that:
:$T = S$
{{qed}}
Theorem: Consecutive Fibonacci Numbers are Coprime

Let $F_k$ be the $k$th Fibonacci number.
Then:
:$\forall n \ge 2: \gcd \set {F_n, F_{n + 1} } = 1$
where $\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.
That is, a Fibonacci number and the one next to it are coprime.

Proof:
From the definition of Fibonacci numbers:
:$F_1 = 1, F_2 = 1, F_3 = 2$
Proof by induction:
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$\gcd \set {F_n, F_{n + 1} } = 1$
Theorem: Divisibility of Fibonacci Number

:$\forall m, n \in \Z_{> 2} : m \divides n \iff F_m \divides F_n$
where $\divides$ denotes divisibility.

Proof:
From the initial definition of Fibonacci numbers:
:$F_1 = 1, F_2 = 1, F_3 = 2, F_4 = 3$
Let $n = k m - r$ where $0 \le r < m$
We have:
:$m \divides n \iff r = 0$
The proof proceeds by induction on $k$.
For all $k \in \N_{>0}$, let $\map P k$ be the proposition:
:$r = 0 \iff F_m \divides F_{k m - r}$
Theorem: Honsberger's Identity

:$\forall m, n \in \Z_{>0}: F_{m + n} = F_{m - 1} F_n + F_m F_{n + 1}$

Proof:
From the initial definition of Fibonacci numbers, we have:
:$F_1 = 1, F_2 = 1, F_3 = 2, F_4 = 3$
Proof by induction:
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$\forall m \in \Z_{>0} : F_{m + n} = F_{m - 1} F_n + F_m F_{n + 1}$
=== Basis for the Induction ===
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = F_{m + 1}
      | r = F_{m - 1} + F_m
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = F_{m - 1} \times 1 + F_m \times 1
      | c = 
}}
{{eqn | r = F_{m - 1} F_1 + F_m F_2
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = F_{m - 1} F_n + F_m F_{n + 1}
      | c = for $n = 1$
}}
{{end-eqn}}
and so $\map P 1$ is seen to hold.
$\map P 2$ is the case:
{{begin-eqn}}
{{begin-eqn}}
{{eqn | l = F_{m + 2}
      | r = F_{m + 1} + F_m
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = F_{m - 1} + F_m + F_m
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = F_{m - 1} \times 1 + F_m \times 2
      | c = 
}}
{{eqn | r = F_{m - 1} F_2 + F_m F_3
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = F_{m - 1} F_n + F_m F_{n + 1}
      | c = for $n = 2$
}}
{{end-eqn}}
and so $\map P 2$ is seen to hold.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ and $\map P {k - 1}$ are true, where $k > 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$F_{m + k} = F_{m - 1} F_k + F_m F_{k + 1}$
and:
:$F_{m + k - 1} = F_{m - 1} F_{k - 1} + F_m F_k$
from which it is to be shown:
:$F_{m + k + 1} = F_{m - 1} F_{k + 1} + F_m F_{k + 2}$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = F_{m + k + 1}
      | r = F_{m + k} + F_{m + k - 1}
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = F_{m - 1} F_k + F_m F_{k + 1} + F_{m - 1} F_{k - 1} + F_m F_k
      | c = Induction Hypothesis
}}
{{eqn | r = F_{m - 1} \paren {F_k + F_{k - 1} } + F_m \paren {F_{k + 1} + F_k}
      | c = 
}}
{{eqn | r = F_{m - 1} F_{k + 1} + F_m F_{k + 2}
      | c = {{Defof|Fibonacci Number}}
}}
{{end-eqn}}
So $\map P k \land \map P {k - 1} \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall m, n \in \Z_{>0} : F_{m + n} = F_{m - 1} F_n + F_m F_{n + 1}$
{{qed}}
Theorem: Honsberger's Identity

:$\forall m, n \in \Z_{>0}: F_{m + n} = F_{m - 1} F_n + F_m F_{n + 1}$

Proof:
{{begin-eqn}}
{{eqn | r = F_{m - 1} F_n + F_m F_{n + 1}
      | o = 
}}
{{eqn | r = \dfrac {\phi^{m - 1} - \hat \phi^{m - 1} } {\sqrt 5} \dfrac {\phi^n - \hat \phi^n} {\sqrt 5} + \dfrac {\phi^m - \hat \phi^m} {\sqrt 5} \dfrac {\phi^{n + 1} - \hat \phi^{n + 1} } {\sqrt 5}
      | c = Euler-Binet Formula
}}
{{eqn | r = \dfrac {\phi^{m + n - 1} - \phi^{m - 1} \hat \phi^n - \phi^n \hat \phi^{m - 1} + \hat \phi^{m + n - 1} + \phi^{m + n + 1} - \phi^m \hat \phi^{n + 1} - \phi^{n + 1} \hat \phi^m + \hat \phi^{m + n + 1} } 5
      | c = 
}}
{{eqn | r = \dfrac {\phi^{m + n - 1} \paren {1 + \phi^2} + \hat \phi^{m + n - 1} \paren {1 + \hat \phi^2} - \phi^{m - 1} \hat \phi^n \paren {1 + \phi \hat \phi} -\phi^n \hat \phi^{m - 1} \paren {1 + \phi \hat \phi} } 5
      | c = 
}}
{{eqn | r = \dfrac {\phi^{m + n - 1} \paren {1 + \phi^2} + \hat \phi^{m + n - 1} \paren {1 + \hat \phi^2} } 5
      | c = as $\phi \hat \phi = -1$
}}
{{eqn | r = \dfrac {\phi^{m + n - 1} \paren {2 + \phi} + \hat \phi^{m + n - 1} \paren {2 + \hat \phi} } 5
      | c = as both $\phi$ and $\hat \phi$ satisfy $x^2 = x + 1$
}}
{{eqn | r = \dfrac {\phi^{m + n - 1} \paren {2 + \dfrac {1 + \sqrt 5} 2} + \hat \phi^{m + n - 1} \paren {2 + \dfrac {1 - \sqrt 5} 2} } 5
      | c = {{Defof|Golden Mean|$\phi$ and $\hat \phi$}}
}}
{{eqn | r = \dfrac {\phi^{m + n - 1} \paren {\dfrac {5 + \sqrt 5} 2} + \hat \phi^{m + n - 1} \paren {\dfrac{ 5 - \sqrt 5} 2} } 5
      | c = 
}}
{{eqn | r = \dfrac {\phi^{m + n - 1} \paren {\dfrac {1 + \sqrt 5} 2} - \hat \phi^{m + n - 1} \paren {\dfrac {1 - \sqrt 5} 2} } {\sqrt 5}
      | c = dividing numerator and denominator by $\sqrt 5$
}}
{{eqn | r = \dfrac {\phi^{m + n} - \hat \phi^{m + n} } {\sqrt 5}
      | c = {{Defof|Golden Mean|$\phi$ and $\hat \phi$}}
}}
{{eqn | r = F_{m + n}
      | c = Euler-Binet Formula
}}
{{end-eqn}}
{{qed}}
Theorem: GCD of Fibonacci Numbers

:$\forall m, n \in \Z_{> 2}: \gcd \set {F_m, F_n} = F_{\gcd \set {m, n} }$
where $\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.

Proof:
From the initial definition of Fibonacci numbers, we have:
:$F_1 = 1, F_2 = 1, F_3 = 2, F_4 = 3$
{{WLOG}}, let $m \le n$.
Let $h$ be $\gcd \set {m, n}$.
Let $a$ and $b$ be integers such that $m = h a$ and $n = \map h {a + b}$.
$a$ and $a + b$ are coprime by Integers Divided by GCD are Coprime.
Therefore, $a$ and $b$ are coprime by Integer Combination of Coprime Integers.
{{begin-eqn}}
{{eqn | l = \gcd \set {F_m, F_n}
      | r = \gcd \set {F_{h a}, F_{h a - 1} F_{h b} + F_{h a} F_{h b + 1} }
      | c = Honsberger's Identity
}}
{{eqn | r = \gcd \set {F_{h a}, F_{h a - 1} F_{h b} }
      | c = GCD with Remainder
}}
{{end-eqn}}
Let $u$ and $v$ be integers such that $F_{h a} = u F_h$ and $F_{h b} = v F_h$, whose existence is proved by Divisibility of Fibonacci Number.
We have that $F_{h a}$ and $F_{h a - 1}$ are coprime by Consecutive Fibonacci Numbers are Coprime.
Therefore, $u$ and $F_{h a - 1}$ are coprime by Divisor of One of Coprime Numbers is Coprime to Other.
{{begin-eqn}}
{{eqn | l = \gcd \set {F_{h a}, F_{h a - 1} F_{h b} }
      | r = F_h \gcd \set {u, v F_{h a - 1} }
      | c = Honsberger's Identity
}}
{{eqn | r = F_h \gcd \set {u, v}
      | c = Solution of Linear Diophantine Equation
}}
{{eqn | r = \gcd \set {F_m, F_{n - m} }
      | c =
}}
{{end-eqn}}
Therefore:
:$\forall m, n \in \Z_{>2} : \gcd \set {F_m, F_n} = \gcd \set {F_m, F_{n - m} }$
This can be done recurrently to produce the result, in a fashion similar to the Euclidean Algorithm. 
Since $a$ and $b$ are coprime, the result would be $\gcd \set {F_h, F_h}$.
Therefore:
:$\forall m, n > 2 : \gcd \set {F_m, F_n} = F_{\gcd \set {m, n} }$
{{qed}}
Theorem: Catalan's Identity

:${F_n}^2 - F_{n - r} F_{n + r} = \left({-1}\right)^{n - r} {F_r}^2$

Proof:
From the definition of Fibonacci numbers:
:$F_1 = 1, F_2 = 1, F_3 = 2, F_4 = 3$
By Honsberger's Identity:
:$F_n = F_{n - r} F_{r - 1} + F_{n - r + 1} F_r$
Also:
{{begin-eqn}}
{{eqn | l = F_{n + r}
      | r = F_{n - r} F_{2 r - 1} + F_{n - r + 1} F_{2 r}
      | c = Honsberger's Identity
}}
{{eqn | r = F_{n - r} \paren {F_{r - 1}^2 + {F_r}^2} + F_{n - r + 1} \paren {F_{r - 1} F_r + F_r F_{r + 1} }
      | c = Honsberger's Identity
}}
{{eqn | r = F_{n - r} \paren { {F_{r - 1} }^2 + {F_r}^2} + F_{n - r + 1} \paren {F_{r - 1} F_r + F_r \paren {F_{r - 1} + F_r} }
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = F_{n - r} \paren { {F_{r - 1} }^2 + {F_r}^2} + F_{n - r + 1} \paren {F_r \paren {F_{r - 1} + F_{r - 1} + F_r} }
      | c = 
}}
{{eqn | r = F_{n - r} \paren { {F_{r - 1} }^2 + {F_r}^2} + F_{n - r + 1} \paren {2 F_r F_{r - 1} + {F_r}^2}
      | c = 
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | o = 
      | r = F_n^2 - F_{n - r} F_{n + r}
      | c = 
}}
{{eqn | r = \paren {F_{n - r} F_{r - 1} + F_{n - r + 1} F_r}^2 - F_{n - r} \paren {F_{n - r} \paren { {F_{r - 1} }^2 + {F_r}^2} + F_{n - r + 1} \paren {2 F_r F_{r - 1} + {F_r}^2} }
      | c = from above
}}
{{eqn | r = \paren { {F_{n - r + 1} }^2 {F_r}^2} - \paren { {F_{n - r} }^2 {F_r}^2 + F_{n - r} F_{n - r + 1} {F_r}^2}
      | c = Expansion and Simplification
}}
{{eqn | r = {F_r}^2 \paren { {F_{n - r + 1} }^2 - {F_{n - r} }^2 - F_{n - r} F_{n - r + 1} }
      | c = 
}}
{{eqn | r = {F_r}^2 \paren {F_{n - r + 1} \paren {F_{n - r + 1} - F_{n - r} } - {F_{n - r} }^2}
      | c = 
}}
{{eqn | r = {F_r}^2 \paren {F_{n - r  + 1} \paren {F_{n - r - 1} } - {F_{n-r} }^2}
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = {F_r}^2 \paren {-1}^{n - r}
      | c = Cassini's Identity
}}
{{eqn | r = \paren {-1}^{n - r} {F_r}^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Fibonacci Number with Negative Index

:$\forall n \in \Z_{> 0} : F_{-n} = \paren {-1}^{n + 1} F_n$

Proof:
From the initial definition of Fibonacci numbers, we have:
:$F_0 = 0, F_1 = 1, F_2 = 1, F_3 = 2, F_4 = 3$
By definition of the extension of the Fibonacci numbers to negative integers:
:$F_n = F_{n + 2} - F_{n - 1}$
The proof proceeds by induction.
For all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:$F_{-n} = \paren {-1}^n F_n$
Theorem: Fibonacci Number in terms of Larger Fibonacci Numbers

:$\forall m, n \in \Z_{>0} : \paren {-1}^n F_{m - n} = F_m F_{n - 1} - F_{m - 1} F_n$

Proof:
{{begin-eqn}}
{{eqn | l = F_{m - n}
      | r = F_{m + \paren {-n} }
      | c = {{Defof|Integer Subtraction}}
}}
{{eqn | r = F_{m - 1} F_{-n} + F_m F_{-n + 1}
      | c = Honsberger's Identity
}}
{{eqn | r = \paren {-1}^{n + 1} F_{m - 1} F_n + \paren {-1}^n F_m F_{n - 1}
      | c = Fibonacci Number with Negative Index
}}
{{eqn | ll= \leadsto
      | l = \paren {-1}^n F_{m - n}
      | r = \paren {-1} F_{m - 1} F_n + F_m F_{n - 1}
      | c = multiplying both sides by $\paren {-1}^n$
}}
{{eqn | r = F_m F_{n - 1} - F_{m - 1} F_n
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Category:Fibonacci Numbers
l1mi5t1nghus98l0gd2tzcw7h6h1d6p
Theorem: Fibonacci Number as Sum of Binomial Coefficients

{{begin-eqn}}
{{eqn | q = \forall n \in \Z_{>0}
      | l = F_n
      | r = \sum_{k \mathop = 0}^{\floor {\frac {n - 1} 2} } \dbinom {n - k - 1} k
      | c = 
}}
{{eqn | r = \binom {n - 1} 0 + \binom {n - 2} 1 + \binom {n - 3} 2 + \dotsb + \binom {n - j} {j - 1} + \binom {n - j - 1} j
      | c = where $j = \floor {\dfrac {n - 1} 2}$
}}
{{end-eqn}}

Proof:
By definition of Fibonacci numbers:
:$F_1 = 1, F_2 = 1, F_3 = 2, F_4 = 3, \ldots$
The proof proceeds by induction.
For all $n \in \Z_{>0}$, let $\map P n$ be the proposition:
:$\ds F_n = \sum_{k \mathop = 0}^{\floor {\frac {n - 1} 2} } \dbinom {n - k - 1} k$
Theorem: Determinant of Matrix Product/General Case

Let $\mathbf A_1, \mathbf A_2, \cdots, \mathbf A_n$ be square matrices of order $n$, where $n > 1$.
Then:
:$\map \det {\mathbf A_1 \mathbf A_2 \cdots \mathbf A_n} = \map \det {\mathbf A_1} \map \det {\mathbf A_2} \cdots \map \det {\mathbf A_n}$

Proof:
Proof by induction:
Theorem: Opposite Sides Equal implies Parallelogram

Let $ABCD$ be a convex quadrilateral with $AB = CD$ and $BC = AD$.
Then $ABCD$ is a parallelogram.

Proof:
Join $AC$.
{{begin-eqn}}
{{eqn | n = 1
      | l = AB
      | r = CD
      | c = {{hypothesis}}
}}
{{eqn | n = 2
      | l = BC
      | r = DA
      | c = {{hypothesis}}
}}
{{eqn | n = 3
      | l = AC
      | r = CA
      | c = Equality is Reflexive
}}
{{eqn | n = 4
      | l = \Delta ABC
      | r = \Delta CDA
      | c = SSS from $(1)$, $(2)$, and $(3)$
}}
{{eqn | n = 5
      | l = \angle BCA
      | r = \angle DAC
      | c = from $(4)$
}}
{{eqn | n = 6
      | l = \angle BAC
      | r = \angle DCA
      | c = from $(4)$
}}
{{eqn | n = 7
      | l = BC
      | o = \parallel
      | r = DA
      | c = Equal Alternate Angles implies Parallel Lines from $(5)$
}}
{{eqn | n = 8
      | l = BA
      | o = \parallel
      | r = DC
      | c = Equal Alternate Angles implies Parallel Lines from $(6)$
}}
{{end-eqn}}
From $(7)$ and $(8)$, it follows by definition that $ABCD$ is a parallelogram.
{{qed}}
Theorem: Principle of Mathematical Induction/Naturally Ordered Semigroup/General Result

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $p \in S$.
Let $T \subseteq S$ such that:
:$x \in T \implies p \preceq x \land \paren {x \in T \implies x \circ 1 \in T}$
Then:
:$S \setminus S_p \subseteq T$
where:
:$\setminus$ denotes set difference
:$S_p$ denotes the set of all elements of $S$ preceding $p$.

Proof:
Let $S_p$ be the set of all elements of $S$ preceding $p$:
:$S_p = \set {x \in S: x \prec p}$
Let $T' = T \cup S_p$.
Then the set $T'$ satisfies the conditions of the Principle of Mathematical Induction for a Naturally Ordered Semigroup.
From that result:
:$T' = S$
By Set Difference with Union is Set Difference:
:$S \setminus S_p = T \setminus S_p$
By Set Difference is Subset:
:$T \setminus S_p \subseteq T$
completing the proof.
{{qed}}
Theorem: Principle of Mathematical Induction for Minimally Inductive Set

Let $\omega$ be the minimally inductive set.
Let $S \subseteq \omega$.
Suppose that:
:$(1): \quad \O \in S$
:$(2): \quad \forall x: x \in S \implies x^+ \in S$
where $x^+$ is the successor set of $x$.
Then:
:$S = \omega$
</onlyinclude>

Proof:
The hypotheses state precisely that $S$ is an inductive set.
Then the minimally inductive set $\omega$ being defined as the intersection of all inductive sets, we conclude that:
:$\omega \subseteq S$
by Intersection is Subset: General Result.
Thus, by definition of set equality:
:$S = \omega$
{{qed}}
Theorem: Principle of Mathematical Induction for Natural Numbers in Real Numbers

Let $\struct {\R, +, \times, \le}$ be the field of real numbers.
Let $\N$ be the natural numbers in $\R$.
Suppose that $A \subseteq \N$ is an inductive set.
Then $A = \N$.

Proof:
By definition of the natural numbers in $\R$:
:$\N = \ds \bigcap \II$
where $\II$ is the set of inductive sets in $\R$.
Since $A$ was supposed to be inductive, it follows that:
:$\N \subseteq A$
from Intersection is Subset: General Result.
Hence by definition of set equality:
:$A = \N$
{{qed}}