avewright/proofwiki-math huggingface dataset:
Theorem: Vajda's Identity/Formulation 1

:$F_{n + i} F_{n + j} - F_n F_{n + i + j} = \paren {-1}^n F_i F_j$

Proof:
From Honsberger's Identity:
{{begin-eqn}}
{{eqn | l = F_{n + i}
      | r = F_n F_{i - 1} + F_{n + 1} F_i
}}
{{eqn | l = F_{n + j}
      | r = F_n F_{j - 1} + F_{n + 1} F_j
}}
{{eqn | l = F_{n + i + j}
      | r = F_{i - 1} F_{n + j} + F_i F_{n + j + 1}
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | o =
      | r = F_{n + i} F_{n + j} - F_n F_{n + i + j}
}}
{{eqn | r = \paren {F_n F_{i - 1} + F_{n + 1} F_i} F_{n + j} - F_n \paren {F_{i - 1} F_{n + j} + F_i F_{n + j + 1} }
      | c = {{apriori}}
}}
{{eqn | r = \paren {F_n F_{i - 1} + F_{n + 1} F_i} F_{n + j} - F_n F_{i - 1} F_{n + j} - F_n F_i F_{n + j + 1}
      | c = 
}}
{{eqn | r = \paren {F_n F_{i - 1} + F_{n + 1} F_i - F_n F_{i - 1} } F_{n + j} - F_n F_i F_{n + j + 1}
      | c = 
}}
{{eqn | r = \paren {F_{n + 1} F_i} F_{n + j} - F_n F_i F_{n + j + 1}
      | c = 
}}
{{eqn | r = F_i \paren {F_{n + 1} F_{n + j} - F_n F_{n + j + 1} }
      | c = 
}}
{{eqn | r = F_i \paren {-1}^{2 n + 1} \paren {F_n F_{n + j + 1} - F_{n + 1} F_{n + j} }
      | c = 
}}
{{eqn | r = F_i \paren {-1}^{n - j - 1} \paren {\paren {-1}^{n + j} F_n F_{n + j + 1} - \paren {-1}^{n + j} F_{n + 1} F_{n + j} }
      | c = 
}}
{{eqn | r = F_i \paren {-1}^{n - j - 1} \paren {\paren {-1}^{n + j} F_n F_{n + j + 1} + \paren {-1}^{n + j + 1} F_{n + 1} F_{n + j} }
      | c = 
}}
{{eqn | r = F_i \paren {-1}^{n - j - 1} F_{\paren {n + 1} - \paren {n + j + 1} }
      | c = Fibonacci Number in terms of Larger Fibonacci Numbers
}}
{{eqn | r = F_i \paren {-1}^{n - j - 1} F_{-j}
      | c = 
}}
{{eqn | r = F_i \paren {-1}^{n - j - 1} \paren {-1}^{j + 1} F_j
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = \paren {-1}^n F_i F_j
      | c = 
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Steven Vajda}}
Category:Vajda's Identity
hi4s04rqltvh9bfildq7u8wd7zc8rj6
Theorem: Vajda's Identity/Formulation 2

:$F_{n + k} F_{m - k} - F_n F_m = \paren {-1}^n F_{m - n - k} F_k$

Proof:
We have:
{{begin-eqn}}
{{eqn | n = 1
      | o = 
      | r = \paren {x^{n + k} - y^{n + k} } \paren {x^{m - k} - y^{m - k} } - \paren {x^n - y^n} \paren {x^m - y^m}
      | c = 
}}
{{eqn | r = x^{n + m} + y^{n + m} - x^{m - k} y^{n + k} - x^{n + k} y^{m - k} - x^{n + m} - y^{n + m} + x^n y^m + x^m y^n
      | c = 
}}
{{eqn | r = x^n y^m + x^m y^n - x^{m - k} y^{n + k} - x^{n + k} y^{m - k}
      | c = 
}}
{{eqn | r = x^n y^n \paren {y^{m - n} + x^{m - n} - x^{m - n - k} y^k - x^k y^{m - n - k} }
      | c = 
}}
{{eqn | r = x^n y^n \paren {x^{m - n - k} \paren {x^k - y^k} - y^{m - n - k} \paren {x^k - y^k} }
      | c = 
}}
{{eqn | n = 2
      | r = \paren {x y}^n \paren {x^{m - n - k} - y^{m - n - k} } \paren {x^k - y^k}
      | c = 
}}
{{end-eqn}}
Now substitute:
{{begin-eqn}}
{{eqn | l = x
      | r = \phi
      | c = 
}}
{{eqn | l = y
      | r = \hat \phi
      | c = 
}}
{{end-eqn}}
where:
: $\phi$ denotes the golden mean
: $\hat \phi = 1 - \phi$
first into $(2)$:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {\phi \hat \phi}^n \paren {\phi^{m - n - k} - \hat \phi^{m - n - k} } \paren {\phi^k - \hat \phi^k}
      | c = 
}}
{{eqn | r = \paren {-1}^n \paren {\phi^{m - n - k} - \hat \phi^{m - n - k} } \paren {\phi^k - \hat \phi^k}
      | c = Reciprocal Form of One Minus Golden Mean: $\hat \phi = -\dfrac 1 \phi$
}}
{{eqn | r = \paren {-1}^n F_{m - n - k} F_k \times \paren {\sqrt 5}^2
      | c = Euler-Binet Formula
}}
{{end-eqn}}
and then into $(1)$:
{{begin-eqn}}
{{eqn | o = 
      | r = \paren {\phi^{n + k} - \hat \phi^{n + k} } \paren {\phi^{m - k} - \hat \phi^{m - k} } - \paren {\phi^n - \hat \phi^n} \paren {\phi^m - \hat \phi^m}
      | c = 
}}
{{eqn | r = F_{n + k} F_{m - k} - F_n F_m \times \paren {\sqrt 5}^2
      | c = Euler-Binet Formula
}}
{{end-eqn}}
$(1) = (2)$ and hence the result.
{{qed}}
{{Namedfor|Steven Vajda}}
Theorem: Sum of Squares of Consecutive Fibonacci Numbers

:${F_n}^2 + {F_{n + 1} }^2 = F_{2 n + 1}$
where $F_n$ denotes the $n$th Fibonacci number.

Proof:
{{begin-eqn}}
{{eqn | l = {F_n}^2 + {F_{n + 1} }^2
      | r = F_{n + 1} F_{n - 1} - \paren {-1}^n + F_{n + 2} F_n - \paren {-1}^{n + 1}
      | c = Cassini's Identity
}}
{{eqn | r = F_n F_{n + 2} + F_{n - 1} F_{n + 1}
      | c = 
}}
{{eqn | r = F_{n + n + 1}
      | c = Honsberger's Identity
}}
{{eqn | r = F_{2 n + 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Hausdorff's Maximal Principle implies Zermelo's Well-Ordering Theorem

Let Hausdorff's Maximal Principle hold.
Then Zermelo's Well-Ordering Theorem holds.

Proof:
{{tidy|Work in progress}}
Let $X$ be a non-empty set.
Let $X$ contain at least two elements; otherwise, $X$ can be trivially well-ordered.
We use Hausdorff's Maximal Principle to construct a well-ordering on $X$.
We note that there exists at least the following strict well-orderings on subsets of $X$: 
For any singleton $\set x$, $x$ is vacuously well-ordered with respect to every other element in the subset, of which there are none.
{{explain|Can you describe an element of a set as being well-ordered? A well-ordering applies to a set, not an element in it. Recommend the above statement about singletons be extracted into a result about the triviality of imposing an ordering upon a singleton.}}
Any doubleton $\set {y, z}$ can be strictly well-ordered by defining $x < y$ and $y \not < x$.
{{explain|Again, the above can be extracted into a result about doubletons. In fact, I believe we may be able to cut through a lot of this by using Finite Totally Ordered Set is Well-Ordered.}}
Let $\AA$ be the set of all ordered pairs $\struct {A, <}$ such that $A$ is a subset of $X$ and $<$ is a strict well-ordering of $A$.
Define $\prec$ as:
:$\struct {A, <} \prec \struct {A', <'}$
{{iff}} 
:$\struct {A, <}$ equals an initial segment of $\struct {A', <'}$.
Let $\BB$ be a set of ordered pairs in $\AA$ such that $\BB$ is ordered by $\prec$.
Let $B'$ be the union of the sets $B$ for all $\struct {B, <} \in \BB$.
Let $<'$ be the union of the relations $<$ for all $\struct {B, <}$.
By Equality to Initial Segment Imposes Well-Ordering, $\struct {B', <'}$ is strictly well-ordered set.
By Hausdorff's Maximal Principle, there exists a maximal chain defined by $<'$ imposed on a maximal subset of $X$.
We claim that this maximal chain is imposed on the entirety of $X$.
{{AimForCont}} that $\struct {B', <'}$ is a maximal chain but $B' \ne X$.
Then consider $B' \cup \set x$, with $x \in X \setminus B'$, with the extension of $<'$ such that:
:$\forall a \in B': a <' x$. 
Then $B' = S_x$, the initial segment in $B' \cup \set x$ determined by $x$.
But by the definition of $\prec$, we then have:
:$\struct {B' \cup \set x, \text {extension of } <'} \prec \struct {B', <'}$
But then by the definition of $B'$, we would have $B' \cup \set x \subseteq B'$, contrary to the assumption that $x \in X \setminus B'$.
From this contradiction infer that $B' = X$.
That is, all of $X$ can be well-ordered.
{{qed}}
Theorem: Cosine of 36 Degrees

:$\cos 36 \degrees = \cos \dfrac \pi 5 = \dfrac \phi 2 = 2^{-1} \phi = \dfrac {1 + \sqrt 5} 4$
where $\phi$ denotes the golden mean.

Proof:
Let $u = \cos 72 \degrees, v = \cos 36 \degrees$.
Recall from Cosine of Complement equals Sine that $\map \cos {\dfrac \pi 2 - \theta} = \sin \theta$
Therefore:
{{begin-eqn}}
{{eqn | l = \map \cos {90 \degrees - 18 \degrees}
      | r = \map \sin {18 \degrees}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map \cos {72 \degrees}
      | r = \map \sin {18 \degrees}
      | c = 
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \cos 36 \degrees
      | r = 1 - 2 \sin^2 18 \degrees
      | c = {{Corollary|Double Angle Formula for Cosine|2}}
}}
{{eqn | ll = \leadsto
      | l = v
      | r = 1 - 2 u^2
      | c = substituting for $u$ and $v$
}}
{{eqn | l = \cos 72 \degrees
      | r = 2 \cos^2 36 \degrees - 1
      | c = {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | ll = \leadsto
      | l = u
      | r = 2 v^2 - 1
      | c = substituting for $u$ and $v$
}}
{{eqn | ll= \leadsto
      | l = u + v
      | r = 2 \paren {v^2 - u^2}
      | c = 
}}
{{eqn | r = 2 \paren {v + u} \paren {v - u}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = 2 \paren {v - u}
      | c = dividing both sides by $\paren {v + u}$
}}
{{eqn | r = 2 v - 4 v^2 + 2
      | c = substituting $u = 2 v^2 - 1$
}}
{{eqn | ll= \leadsto
      | l = \paren {2 v}^2
      | r = 2 v + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 v
      | r = \phi
      | c = Square of Golden Mean equals One plus Golden Mean
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of 36 Degrees

:$\cos 36 \degrees = \cos \dfrac \pi 5 = \dfrac \phi 2 = 2^{-1} \phi = \dfrac {1 + \sqrt 5} 4$
where $\phi$ denotes the golden mean.

Proof:
From Complex Algebra: $z^4 - 3z^2 + 1 = 0$, the roots of $z^4 - 3z^2 + 1 = 0$ are:
:$2 \cos 36 \degrees, 2 \cos 72 \degrees, 2 \cos 216 \degrees, 2 \cos 252 \degrees$
Then:
{{begin-eqn}}
{{eqn | l = z^4 - 3z^2 + 1
      | r = 0
      | c = 
}}
{{eqn | ll= \leadsto
      | l = z^2
      | r = \dfrac {3 \pm \sqrt {\paren {-3}^2 - 4 \times 1} } 2
      | c = Quadratic Formula
}}
{{eqn | r = \dfrac 3 2 \pm \dfrac {\sqrt 5} 2
      | c = 
}}
{{end-eqn}}
By Shape of Cosine Function:
:$\paren {2 \cos 36^\circ}^2 > \paren {2 \cos 45^\circ}^2 = 2 > \dfrac 3 2 - \dfrac {\sqrt 5} 2$
so $\paren {2 \cos 36^\circ}^2 = \dfrac 3 2 + \dfrac {\sqrt 5} 2$.
Let $z = k \paren {a + \sqrt 5}$, where $k \in \Q$ and $a \in \Z$.
Then for $z = 2 \cos 36^\circ$:
{{begin-eqn}}
{{eqn | l = k^2 \paren {a + \sqrt 5}^2
      | r = \dfrac 3 2 + \dfrac {\sqrt 5} 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 k^2 \paren {a^2 + 5 + 2 a \sqrt 5}
      | r = 3 + \sqrt 5
      | c = Square of Sum
}}
{{end-eqn}}
By comparing coefficients:
{{begin-eqn}}
{{eqn | l = \paren {a^2 + 5} : 2 a
      | r = 3 : 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a^2 + 5
      | r = 6 a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a^2 - 6 a + 5
      | r = 0
      | c = 
}}
{{eqn | r = \paren {a - 5} \paren {a - 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | r = 1 \text{ or } 5
      | c = 
}}
{{end-eqn}}
We have, from the expansion above:
:$4 a k^2 = 1$
which leads to:
:$\sqrt a = \dfrac 1 {2 k}$
so $a$ must be square.
Thus $a = 1$ and hence:
:$2 \cos 36^\circ = k \paren {a + \sqrt 5} = \dfrac {1 + \sqrt 5} 2$
:$\cos 36^\circ = \dfrac {1 + \sqrt 5} 4$
{{qed}}
Theorem: Cosine of 36 Degrees

:$\cos 36 \degrees = \cos \dfrac \pi 5 = \dfrac \phi 2 = 2^{-1} \phi = \dfrac {1 + \sqrt 5} 4$
where $\phi$ denotes the golden mean.

Proof:
{{begin-eqn}}
{{eqn | l = \sin 108 \degrees
      | r = 3 \sin 36 \degrees - 4 \sin^3 36 \degrees
      | c = Triple Angle Formula for Sine
}}
{{eqn | l = \sin 72 \degrees
      | r = 3 \sin 36 \degrees - 4 \sin^3 36 \degrees
      | c = Sine of Supplementary Angle
}}
{{eqn | l = 2 \sin 36 \degrees \cos 36 \degrees
      | r = 3 \sin 36 \degrees - 4 \sin^3 36 \degrees
      | c = Double Angle Formula for Sine
}}
{{eqn | l = 2 \cos 36 \degrees
      | r = 3 - 4 \sin^2 36 \degrees
      | c = dividing both sides by $\sin 36 \degrees$
}}
{{eqn | r = 4 \cos^2 36 \degrees - 1
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = 4 \cos^2 36 \degrees - 2 \cos 36 \degrees - 1
      | r = 0
}}
{{eqn | l = \cos 36 \degrees
      | r = \frac {2 \pm \sqrt {2^2 + 4 \times 4} } {2 \times 4}
      | c = Quadratic Formula
}}
{{eqn | r = \frac {2 \pm \sqrt {20} } 8
}}
{{eqn | r = \frac {1 + \sqrt 5} 4
      | c = negative root is rejected as $\cos 36 \degrees > 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of 36 Degrees

:$\sin 36 \degrees = \sin \dfrac \pi 5 = \dfrac {\sqrt {\sqrt 5 / \phi} } 2 = 2^{-1} 5^{\frac 1 4} \phi^{-\frac 1 2}= \dfrac {\sqrt {3 - \phi} } 2 = \sqrt {\dfrac 5 8 - \dfrac {\sqrt 5} 8}$

Proof:
{{begin-eqn}}
{{eqn | l = \sin 36 \degrees
      | r = \sqrt {1 - \cos^2 36 \degrees}
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \sqrt {1 - \frac {\phi^2} 4}
      | c = {{cos|36}}
}}
{{eqn | r = \frac 1 2 \sqrt {4 - \phi^2}
      | c = 
}}
{{eqn | r = \frac 1 2 \sqrt {4 - \paren {\frac 1 2 + \frac {\sqrt 5} 2}^2}
      | c = {{Defof|Golden Mean|index = 2}}
}}
{{eqn | r = \frac 1 2 \sqrt {4 - \paren {\frac 1 4 + \frac 5 4 + 2 \cdot \frac 1 2 \cdot \frac {\sqrt 5} 2} }
      | c = Square of Sum
}}
{{eqn | r = \frac 1 2 \sqrt {4 - \paren {\frac 3 2 + \frac {\sqrt 5} 2} }
      | c = 
}}
{{eqn | r = \frac 1 2 \sqrt {3 - \paren {\frac 1 2 + \frac {\sqrt 5} 2} }
      | c = $= \dfrac {\sqrt {3 - \phi} } 2$
}}
{{eqn | r = \frac 1 2 \sqrt {\frac 5 2 - \frac {\sqrt 5} 2}
      | c = 
}}
{{eqn | r = \sqrt {\frac 5 8 - \frac {\sqrt 5} 8}
      | c = 
}}
{{end-eqn}}
We also have:
{{begin-eqn}}
{{eqn | l = 2^{-1} 5^{\frac 1 4} \phi^{-\frac 1 2}
      | r = \frac {\sqrt {\sqrt 5 / \phi} } 2
      | c = 
}}
{{eqn | r = \frac 1 2 \sqrt {\sqrt 5 \paren {\phi - 1} }
      | c = {{Defof|Golden Mean|index = 3}} 
}}
{{eqn | r = \frac 1 2 \sqrt {\sqrt 5 \paren {\frac 1 2 + \frac {\sqrt 5} 2 - 1} }
      | c = {{Defof|Golden Mean|index = 2}} 
}}
{{eqn | r = \frac 1 2 \sqrt {\frac 5 2 - \frac {\sqrt 5} 2}
}}
{{eqn | r = \sqrt {\frac 5 8 - \frac {\sqrt 5} 8}
}}
{{end-eqn}}
{{qed}}
Theorem: Partial Sums of Power Series with Fibonacci Coefficients

:<nowiki>$\ds \sum_{k \mathop = 0}^n F_k x^k = \begin {cases}
\dfrac {x^{n + 1} F_{n + 1} + x^{n + 2} F_n - x} {x^2 + x - 1} & : x^2 + x - 1 \ne 0 \\
\dfrac {\paren {n + 1} x^n F_{n + 1} + \paren {n + 2} x^{n + 1} F_n - 1} {2 x + 1} & : x^2 + x - 1 = 0 \end {cases}$</nowiki>
where $F_n$ denotes the $n$th Fibonacci number.

Proof:
Multiplying the summation by $x^2 + x - 1$:
{{begin-eqn}}
{{eqn | r = \sum_{k \mathop = 0}^n F_k x^k \paren {x^2 + x - 1}
      | o = 
      | c = 
}}
{{eqn | r = F_0 x^2 + F_1 x^3 + F_2 x^4 + \cdots + F_{n - 2} x^n + F_{n - 1} x^{n + 1} + F_n x^{n + 2}
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = F_0 x + F_1 x^2 + F_2 x^3 + \cdots + F_{n - 2} x^{n - 1} + F_{n - 1} x^n + F_n x^{n + 1}
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = F_0 - F_1 x - F_2 x^2 - \cdots - F_{n - 2} x^{n - 2} - F_{n - 1} x^{n - 1} - F_n x^n
      | c = 
}}
{{eqn | r = F_0 + \paren {F_0 - F_1} x + \paren {F_{n - 1} + F_n} x^{n + 1} + F_n x^{n + 2}
      | c = as, in general, $\paren {F_{j - 2} + F_{j - 1} - F_j} x^j = 0$ by {{Defof|Fibonacci Number}}
}}
{{eqn | r = 0 + \paren {-1} x + F_{n + 1} x^{n + 1} + F_n x^{n + 2}
      | c = {{Defof|Fibonacci Number}}: $F_0 = 0, F_1 = 1$
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 0}^n F_k x^k
      | r = \dfrac {F_{n + 1} x^{n + 1} + F_n x^{n + 2} - x} {x^2 + x - 1}
      | c = 
}}
{{end-eqn}}
If the denominator is $0$, then $x = \dfrac 1 \phi$ or $x = \dfrac 1 {\hat \phi}$ and the numerator is $0$ also.
Thus we can differentiate the numerator and denominator {{WRT|Differentiation}} $x$ and use L'Hôpital's Rule:
{{begin-eqn}}
{{eqn | r = \dfrac {\map {\dfrac \d {\d x} } {F_{n + 1} x^{n + 1} + F_n x^{n + 2} - x} } {\map {\dfrac \d {\d x} } {x^2 + x - 1} }
      | o = 
      | c = 
}}
{{eqn | r = \dfrac {\paren {n + 1} F_{n + 1} x^n + \paren {n + 2} F_n x^{n + 1} - 1} {2 x + 1}
      | c = Power Rule for Derivatives
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Sum over k of n Choose k by Fibonacci Number with index m+k

:$\ds \sum_{k \mathop \ge 0} \binom n k F_{m + k} = F_{m + 2 n}$
where:
:$\dbinom n k$ denotes a binomial coefficient
:$F_n$ denotes the $n$th Fibonacci number.

Proof:
From Sum over k of n Choose k by Fibonacci t to the k by Fibonacci t-1 to the n-k by Fibonacci m+k:
:$(1): \quad \ds \sum_{k \mathop \ge 0} \binom n k {F_t}^k {F_{t - 1} }^{n - k} F_{m + k} = F_{m + t n}$
Letting $t = 2$ in $(1)$:
{{begin-eqn}}
{{eqn | l = \sum_{k \mathop \ge 0} \binom n k {F_2}^k {F_{2 - 1} }^{n - k} F_{m + k}
      | r = \sum_{k \mathop \ge 0} \binom n k 1^k 1^{n - k} F_{m + k}
      | c = {{Defof|Fibonacci Number}}: $F_1 = 1, F_2 = 1$
}}
{{eqn | r = \sum_{k \mathop \ge 0} \binom n k F_{m + k}
      | c = 
}}
{{eqn | r = F_{m + 2 n}
      | c = from $(1)$
}}
{{end-eqn}}
{{qed}}
Theorem: Sum over k of n Choose k by Fibonacci t to the k by Fibonacci t-1 to the n-k by Fibonacci m+k

:$\ds \sum_{k \mathop \ge 0} \binom n k {F_t}^k {F_{t - 1} }^{n - k} F_{m + k} = F_{m + t n}$
where:
:$\dbinom n k$ denotes a binomial coefficient
:$F_n$ denotes the $n$th Fibonacci number.

Proof:
The proof proceeds by induction on $n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\forall m, t \in \N: \ds \sum_{k \mathop \ge 0} \binom n k {F_t}^k {F_{t - 1} }^{n - k} F_{m + k} = F_{m + t n}$
$\map P 0$ is the case:
:$\ds \binom 0 0 {F_t}^0 {F_{t - 1} }^0 F_{m + 0} = F_m$
Thus $\map P 0$ is seen to hold.
Theorem: Matrix whose Determinant is Fibonacci Number

The $n \times n$ determinant:
:<nowiki>$D_n = \begin{vmatrix}
1 & -1 & 0 & 0 & \cdots & 0 & 0 & 0 \\
1 & 1 & -1 & 0 & \cdots & 0 & 0 & 0 \\
0 & 1 & 1 & -1 & \cdots & 0 & 0 & 0 \\
\vdots & \vdots & \vdots & \vdots & \ddots & \vdots & \vdots & \vdots \\
0 & 0 & 0 & 0 & \cdots & 1 & 1 & -1 \\
0 & 0 & 0 & 0 & \cdots & 0 & 1 & 1 \\
\end{vmatrix}$</nowiki>
evaluates to $F_{n + 1}$.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 2}$, let $\map P n$ be the proposition:
:$D_n = F_{n + 1}$
Theorem: Determinant with Unit Element in Otherwise Zero Column

Let $D$ be the determinant:
:<nowiki>$D = \begin{vmatrix}
  1 & b_{12} & \cdots & b_{1n} \\
  0 & b_{22} & \cdots & b_{2n} \\
\vdots & \vdots & \ddots & \vdots \\
  0 & b_{n2} & \cdots & b_{nn}
\end{vmatrix}$</nowiki>
Then:
:<nowiki>$D = \begin{vmatrix}
  b_{22} & \cdots & b_{2n} \\
\vdots & \ddots & \vdots \\
  b_{n2} & \cdots & b_{nn}
\end{vmatrix}$</nowiki>

Proof:
We note that:
:<nowiki>$D = \begin{vmatrix}
  1 & b_{12} & \cdots & b_{1n} \\
  0 & b_{22} & \cdots & b_{2n} \\
\vdots & \vdots & \ddots & \vdots \\
  0 & b_{n2} & \cdots & b_{nn}
\end{vmatrix}$</nowiki>
is the transpose of:
:<nowiki>$D^\intercal = \begin{vmatrix}
  1 & 0 & \cdots & 0 \\
  b_{12} & b_{22} & \cdots & b_{n2} \\
\vdots & \vdots & \ddots & \vdots \\
  b_{1n} & b_{2n} & \cdots & b_{nn}
\end{vmatrix}$</nowiki>
From Determinant with Unit Element in Otherwise Zero Row:
:<nowiki>$D^\intercal = \begin{vmatrix}
  b_{22} & \cdots & b_{n2} \\
\vdots & \ddots & \vdots \\
  b_{2n} & \cdots & b_{nn}
\end{vmatrix}$</nowiki>
The result follows by Determinant of Transpose.
{{Qed}}
Theorem: Zermelo's Well-Ordering Theorem implies Hausdorff's Maximal Principle

Let Zermelo's Well-Ordering Theorem hold.
Then Hausdorff's Maximal Principle holds.

Proof:
Let $X$ be a non-empty set.
Let $X$ contain at least two elements.
Otherwise, any non-empty ordering on $X$ is trivially a maximal chain.
By Zermelo's Well-Ordering Theorem, $X$ can be well-ordered set.
Fix such a well-ordering.
Let $\le$ be any ordering on $X$.
Let $\map P {a, Y}$ be the predicate:
:$a$ is $\le$-comparable with every $y \in Y$.
Here, $a$ and $Y$ are bound variables.
That is, $\map P {a, Y}$ holds if, for every $y \in Y$, $a \le y$ or $y \le a$.
Define the mapping:
:$\map \rho {f: S_x \to \powerset X} = \begin {cases}
f \sqbrk {S_x}  \cup \set x & : \map P {x, S_x} \\
f \sqbrk {S_x} & : \text {otherwise}
\end{cases}$
where $S_x$ is the initial segment in $X$ defined by $x$, and $\map f {\,\cdot\,}$ denotes an image set.
Using the Principle of Recursive Definition for Well-Ordered Sets, we can use $\rho$ to uniquely define:
:$h: X \to \powerset X$: 
:$\map h \alpha = \map \rho {h {\restriction_{S_\alpha} } } = \begin {cases}
h \sqbrk {S_\alpha} \cup \set \alpha & : \map P {\alpha, S_\alpha} \\ h \sqbrk {S_\alpha} & : \text {otherwise} \end{cases}$
Then $\map h \alpha$ is a $\le$-totally ordered set, by virtue of the construction of $h$ in terms of the predicate $P$.
Similarly, $h \sqbrk {S_\alpha}$ is totally ordered, for the same reason.
Then the union:
:$Z = \ds \bigcup_{\alpha \mathop \in X} \map h \alpha$
admits an ordered sum in terms of $\le$ imposed on each $\map h \alpha$.
By Ordered Sum of Tosets is Totally Ordered Set, this is a totally ordered set.
In particular, it is a chain of $\struct {X, \le}$.
We claim this chain is maximal.
To see this, consider $x_0 \notin \ds \bigcup_{\alpha \mathop \in X} \map h \alpha$.
Then $x_0$ is not $\le$-comparable with the elements of $Z$, because $\neg \map P {x, Z}$.
That is, there are no proper supersets of $Z$ that are totally ordered.
Therefore the ordered sum on $Z$ is a maximal chain in $\struct {X, \le}$.
{{qed}}
Theorem: Fibonacci Number with Prime Index 2n+1 is Congruent to 5^n Modulo p

Let $p = 2 n + 1$ be an odd prime.
Then:
:$F_p \equiv 5^n \pmod p$

Proof:
From Fibonacci Number by Power of 2:
:$2^p F_p = 2 \ds \sum_{k \mathop \in \Z} \dbinom p {2 k + 1} 5^k$
From Binomial Coefficient of Prime:
:$\forall k \in \Z: 0 < k < p: \dbinom p k \equiv 0 \pmod p$
and from Fermat's Little Theorem: Corollary 1:
:$2^p \equiv 2 \pmod p$
Hence:
{{begin-eqn}}
{{eqn | l = 2^p F_p
      | o = \equiv
      | r = 2 F_p
      | rr= \pmod p
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 2 \sum_{k \mathop \in \Z} \dbinom p {2 k + 1} 5^k
      | o = \equiv
      | r = 2 \times 5^n
      | c = as all $\dbinom p k \equiv 0 \pmod p$ except $\dbinom p p$
}}
{{eqn | ll= \leadsto
      | l = 2^p F_p
      | o = \equiv
      | r = 2 \times 5^n
      | rr= \pmod p
      | c = 
}}
{{eqn | ll= \leadsto
      | l = F_p
      | o = \equiv
      | r = 5^n
      | rr= \pmod p
      | c = because $p \perp 2$
}}
{{end-eqn}}
{{qed}}
Theorem: Fibonacci Number whose Index is Plus or Minus Prime p is Multiple of p

Let $p$ be a prime number distinct from $5$.
Let $F_n$ denote the $n$th Fibonacci number.
Then either $F_{p - 1}$ or $F_{p + 1}$ (but not both) is a multiple of $p$.

Proof:
First we consider the edge cases:
For $p = 2$ we have that:
:$F_{2 + 1} = F_3 = 2$ which is a multiple of $2$.
:$F_{2 - 1} = F_1 = 1$ which is not a multiple of $2$.
For $p = 3$ we have that:
:$F_{3 + 1} = F_4 = 3$ which is a multiple of $3$.
:$F_{3 - 1} = F_2 = 1$ which is not a multiple of $3$.
Let $p$ be an odd prime.
From Cassini's Identity:
:$(1): \quad F_{p - 1} F_{p + 1} - {F_p}^2 = \left({-1}\right)^p = -1$
Then:
{{begin-eqn}}
{{eqn | l = F_p
      | o = \equiv
      | r = 5^{\left({p - 1}\right) / 2}
      | rr= \pmod p
      | c = Fibonacci Number with Prime Index 2n+1 is Congruent to 5^n Modulo p
}}
{{eqn | ll= \leadsto
      | l = {F_p}^2
      | o = \equiv
      | r = 5^{p - 1}
      | rr= \pmod p
      | c = 
}}
{{eqn | ll= \leadsto
      | l = {F_p}^2
      | o = \equiv
      | r = 1
      | rr= \pmod p
      | c = Fermat's Little Theorem, as long as $p \ne 5$
}}
{{eqn | ll= \leadsto
      | l = F_{p - 1} F_{p + 1}
      | o = \equiv
      | r = 0
      | rr= \pmod p
      | c = from $(1)$ above
}}
{{end-eqn}}
Hence either $F_{p - 1}$ or $F_{p + 1}$ is a multiple of $p$.
But as $F_{p + 1} = F_p + F_{p - 1}$, only one of them can be.
Finally, note that if $p = 5$:
:$F_{5 + 1} = F_6 = 8$ which is not a multiple of $5$.
:$F_{5 - 1} = F_4 = 3$ which is not a multiple of $5$.
{{qed}}
Theorem: Fibonacci Number n+1 Minus Golden Mean by Fibonacci Number n

:$F_{n + 1} - \phi F_n = \hat \phi^n$
where:
:$F_n$ denotes the $n$th Fibonacci number
:$\phi$ denotes the golden mean.

Proof:
{{begin-eqn}}
{{eqn | l = F_{n + 1} - \phi F_n
      | r = \dfrac 1 {\sqrt 5} \paren {\phi^{n + 1} - \hat \phi^{n + 1} } - \dfrac \phi {\sqrt 5} \paren {\phi^n - \hat \phi^n}
      | c = Euler-Binet Formula
}}
{{eqn | r = \dfrac 1 {\sqrt 5} \paren {\phi^{n + 1} - \hat \phi^{n + 1} - \phi^{n + 1} + \phi \hat \phi^n}
      | c = 
}}
{{eqn | r = \hat \phi^n \dfrac {\phi - \hat \phi} {\sqrt 5}
      | c = 
}}
{{eqn | r = \hat \phi^n F_1
      | c = Euler-Binet Formula
}}
{{eqn | r = \hat \phi^n
      | c = {{Defof|Fibonacci Number}}: $F_1 = 1$
}}
{{end-eqn}}
{{qed}}