avewright/proofwiki-math huggingface dataset:
Theorem: Initial Segment Determined by Smallest Element is Empty

Let $\struct {S, \preceq}$ be a well-ordered set, where $S$ is non-empty.
Let $s_0 = \min S$, the smallest element of $S$.
Then the initial segment determined by $s_0$, $S_{s_0}$, is empty.

Proof:
By the definition of initial segment:
:$S_{s_0} := \set {b \in S: b \prec s_0}$
By the definition of smallest element:
:$\forall b \in S: s_0 \preceq b$
Thus $S_{s_0}$ is empty.
{{qed}}
Category:Initial Segments
Category:Well-Orderings
cxsawbph07ijlb2ilxdcb4u5ecu9848
Theorem: Equality to Initial Segment Imposes Well-Ordering

Let $X$ be a set.
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, <}$.
Then $\struct {B', <'}$ is strictly well-ordered set.

Proof:
If the set $X$ considered is empty or a singleton, the lemma holds vacuously or trivially.
Thus assume $X$ contains at least two elements.
We first prove that $\prec$ is a strict partial ordering on $\AA$.
From the definition of initial segment, no $\struct {A, <}$ can equal an initial segment of itself.
Thus $\prec$ is antireflexive.
Suppose $\struct {A, <_A}$ equals an initial segment of $\struct {B, <_B}$ and $\struct {B, <_B}$ equals an initial segment of $\struct {C, <_C}$.
Then $\struct {A, <_A}$ equals an initial segment of $\struct {C, <'}$ from Equality is Transitive.
Thus $\prec$ is a strict partial ordering on $\AA$.
We then prove that any $\struct {B', <'}$ is a strictly well-ordered set.
Let $x_1,x_2 \in B'$.
That is, let $x_i \in \struct {A_i, <_i}$ for $i = 1, 2$.
Suppose $x_2 \prec x_1$.
That is, $\struct {A_2, <_2}$ equals an initial segment in $\struct {A_1, <_1}$
By the definition of initial segment, both $x_1$ and $x_2$ are in $\struct {A_1, <_1}$.
Thus $<'$ is connected, as all $<_i$ are strict well-orderings by hypothesis.
For any $x_i \in \struct {A_i, <_i}$, $x_i \nprec x_i$ as all $<_i$ are strict well-orderings by hypothesis.
Thus $<'$ is antireflexive.
To show that $<'$ is transitive, consider $x_i \in \struct {B', <'}$ for $i = 1, 2, 3$.
Suppose $x_1 <' x_2 <' x_3$.
Then $x_1 <_1 x_2$ and $x_2 <_2 x_3$, from the definition of $<'$ as a union of relations $<_i$.
Then $\struct {A_j, <_j}$ is an initial segment of $\struct {A_i, <_i}$ for $j  = 1, 2; j < i$
Thus $x_1 <_i x_2 <_i x_3$.
Then $x_1 <_i x_3$, as all $<_i$ as all $<_i$ are strict well-orderings by hypothesis.
Conclude that $<'$ is itself a strict ordering.
It remains to be shown that $<'$ is a well-ordering.
Let $A$ be an arbitrary non-empty subset of $B'$.
Let $x \in A$ and $x \in \struct {B, <}$ for $\struct {B, <} \in \BB$.
Then for all $y \in A$, $y <' x$ {{iff}} $y < x$ and $y \in B$.
As $<$ is a well-ordering, $\struct {B \cap A, <}$ has a smallest element $b$.
This $b$ is then a smallest element of $<'$ in $A$.
Conclude that $<'$ is a strict well-ordering on $B'$.
{{qed}}
Theorem: Empty Mapping is Injective

Let $\nu: \O \to T$ be an empty mapping.
Then $\nu$ is an injection.

Proof:
There are no elements in the domain of $\nu$.
Thus $\nu$ is an injection vacuously.
{{qed}}
Theorem: Upper and Lower Bound of Fibonacci Number

For all $n \in \N_{> 0}$:
:$\phi^{n - 2} \le F_n \le \phi^{n - 1}$
where:
:$F_n$ is the $n$th Fibonacci number
:$\phi$ is the golden section: $\phi = \dfrac {1 + \sqrt 5} 2$

Proof:
From Fibonacci Number greater than Golden Section to Power less Two:
:$F_n \ge \phi^{n - 2}$
From Fibonacci Number less than Golden Section to Power less One:
:$F_n \le \phi^{n - 1}$
{{qed}}
Theorem: Generating Function for Fibonacci Numbers

Let $\map G z$ be the function defined as:
:$\map G z = \dfrac z {1 - z - z^2}$
Then $\map G z$ is a generating function for the Fibonacci numbers.

Proof:
Let the form of $\map G z$ be assumed as:
{{begin-eqn}}
{{eqn | l = \map G z
      | r = \sum_{k \mathop \ge 0} F_k z^k
      | c = 
}}
{{eqn | r = F_0 + F_1 z + F_2 z^2 + F_3 z^3 + F_4 z^4 + \cdots
      | c = 
}}
{{eqn | r = 0 + z + z^2 + 2 z^3 + 3 z^4 + \cdots
      | c = 
}}
{{end-eqn}}
where $F_n$ denotes the $n$th Fibonacci number.
Then:
{{begin-eqn}}
{{eqn | l = z \map G z
      | r = F_0 z + F_1 z^2 + F_2 z^3 + F_3 z^4 + F_4 z^5 + \cdots
      | c = 
}}
{{eqn | l = z^2 \map G z
      | r = F_0 z^2 + F_1 z^3 + F_2 z^4 + F_3 z^5 + F_4 z^6 + \cdots
      | c = 
}}
{{end-eqn}}
and so:
{{begin-eqn}}
{{eqn | l = \paren {1 - z - z^2} \map G z
      | r = F_0 + \paren {F_1 - F_0} z + \paren {F_2 - F_1 - F_0} z^2 + \paren {F_3 - F_2 - F_1} z^3 + \cdots
      | c = 
}}
{{eqn | r = F_0 + \paren {F_1 - F_0} z
      | c = {{Defof|Fibonacci Number}}: $F_n = F_{n - 1} + F_{n - 2}$
}}
{{eqn | r = z
      | c = {{Defof|Fibonacci Number}}: $F_0 = 0, F_1 = 1$
}}
{{end-eqn}}
Hence the result:
:$\map G z = \dfrac z {1 - z - z^2}$
{{qed}}
Theorem: Fibonacci Numbers which equal their Index

The only Fibonacci numbers which equal their index are:
{{begin-eqn}}
{{eqn | l = F_0
      | r = 0
}}
{{eqn | l = F_1
      | r = 1
}}
{{eqn | l = F_5
      | r = 5
}}
{{end-eqn}}

Proof:
By definition of the Fibonacci numbers:
{{begin-eqn}}
{{eqn | l = F_0
      | r = 0
}}
{{eqn | l = F_1
      | r = 1
}}
{{end-eqn}}
Then it is observed that $F_5 = 5$.
After that, for $n > 5$, we have that $F_n > n$.
{{qed}}
Theorem: Fibonacci Numbers which equal the Square of their Index

The only Fibonacci numbers which equal the square of their index are:
{{begin-eqn}}
{{eqn | l = F_0
      | r = 0
}}
{{eqn | l = F_1
      | r = 1
}}
{{eqn | l = F_{12}
      | r = 12^2 = 144
}}
{{end-eqn}}

Proof:
By definition of the Fibonacci numbers:
{{begin-eqn}}
{{eqn | l = F_0
      | r = 0
}}
{{eqn | l = F_1
      | r = 1
}}
{{end-eqn}}
Then it is observed that $F_{12} = 144$.
After that, for $n > 12$, we have that $F_n > n^2$.
{{qed}}
Theorem: Cassini's Identity/Negative Indices

Let $n \in \Z_{<0}$ be a negative integer.
Let $F_n$ be the $n$th Fibonacci number (as extended to negative integers).
Then Cassini's Identity:
:$F_{n + 1} F_{n - 1} - F_n^2 = \paren {-1}^n$
continues to hold.

Proof:
Let $n \in \Z_{> 0}$.
Then:
{{begin-eqn}}
{{eqn | l = F_{-\paren {n + 1} } F_{-\paren {n - 1} } - {F_{-n} }^2
      | r = \paren {-1}^{n + 2} F_{n + 1} \paren {-1}^n F_{n - 1} - \paren {\paren {-1}^{n + 1} F_n}^2
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = \paren {-1}^{2 n + 2} F_{n + 1} F_{n - 1} - \paren {-1}^{2 n + 2} F_n^2
      | c = 
}}
{{eqn | r = F_{n + 1} F_{n - 1} - F_n^2
      | c = $-1$ to an even power is $1$
}}
{{end-eqn}}
{{qed}}
Theorem: Honsberger's Identity/Negative Indices

Let $n \in \Z_{< 0}$ be a negative integer.
Let $F_n$ be the $n$th Fibonacci number (as extended to negative integers).
Then Honsberger's Identity:
:$F_{m + n} = F_{m - 1} F_n + F_m F_{n + 1}$
continues to hold, whether $m$ or $n$ are positive or negative.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\le 0}$, let $\map P n$ be the proposition:
:$F_{m + n} = F_{m - 1} F_n + F_m F_{n + 1}$
This can equivalently be written:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$F_{m - n} = F_{m - 1} F_{-n} + F_m F_{-n + 1}$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = F_{m - 1} F_0 + F_m F_1
      | r = F_m
      | c = {{Defof|Fibonacci Number}}: $F_0 = 0, F_1 = 1$
}}
{{eqn | r = F_{m + 0}
      | c = 
}}
{{end-eqn}}
Thus $\map P 0)$ is seen to hold.
Theorem: Euler-Binet Formula/Negative Index

Let $n \in \Z_{< 0}$ be a negative integer.
Let $F_n$ be the $n$th Fibonacci number (as extended to negative integers).
Then the Euler-Binet Formula:
:$F_n = \dfrac {\phi^n - \hat \phi^n} {\sqrt 5} = \dfrac {\phi^n - \hat \phi^n} {\phi - \hat \phi}$
continues to hold.

Proof:
Let $n \in \Z_{> 0}$.
Then:
{{begin-eqn}}
{{eqn | l = \dfrac {\phi^{-n} - \hat \phi^{-n} } {\sqrt 5}
      | r = \dfrac 1 {\sqrt 5} \paren {\phi^{-n} - \paren {-\dfrac 1 \phi}^{-n} }
      | c = Definition of $\hat \phi$
}}
{{eqn | r = \dfrac 1 {\sqrt 5} \paren {\dfrac 1 {\phi^n} - \paren {-1}^n \phi^n}
      | c = Exponent Combination Laws: Negative Power
}}
{{eqn | r = \dfrac 1 {\sqrt 5} \paren {\paren {-1}^n \paren {-\dfrac 1 \phi}^n - \paren {-1}^n \phi^n}
      | c = 
}}
{{eqn | r = \paren {-1}^n \dfrac 1 {\sqrt 5} \paren {\hat \phi^n - \phi^n}
      | c = Definition of $\hat \phi$
}}
{{eqn | r = \paren {-1}^{n + 1} \dfrac {\phi^n - \hat \phi^n} {\sqrt 5}
      | c = 
}}
{{eqn | r = \paren {-1}^{n + 1} F_n
      | c = Euler-Binet Formula for positive $n$
}}
{{eqn | r = F_{-n}
      | c = Fibonacci Number with Negative Index
}}
{{end-eqn}}
{{qed}}
Theorem: Fibonacci Number by Golden Mean plus Fibonacci Number of Index One Less

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

Proof:
=== Positive Index ===
First the result is proved for positive integers.
{{:Fibonacci Number by Golden Mean plus Fibonacci Number of Index One Less/Positive Index}}{{qed|lemma}}
Theorem: Fibonacci Number by Golden Mean plus Fibonacci Number of Index One Less/Positive Index

Let $n \in \Z_{\ge 0}$.
Then:
:$\phi^n = F_n \phi + F_{n - 1}$
where:
:$F_n$ denotes the $n$th Fibonacci number
:$\phi$ denotes the golden mean.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $P \left({n}\right)$ be the proposition:
:$\phi^n = F_n \phi + F_{n - 1}$
$P \left({0}\right)$ is the case:
{{begin-eqn}}
{{eqn | l = F_0 \times \phi + F_{-1}
      | r = F_0 \times \phi + \left({-1}\right)^0 F_1
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = F_0 \times \phi + 1
      | c = {{Defof|Fibonacci Number}} $F_1 = 1$
}}
{{eqn | r = 0 \times \phi + 1
      | c = {{Defof|Fibonacci Number}} $F_0 = 0$
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | r = \phi^0
      | c = 
}}
{{end-eqn}}
Thus $P \left({0}\right)$ is seen to hold.
==== Basis for the Induction ====
$P \left({1}\right)$ is the case:
{{begin-eqn}}
{{eqn | l = F_1 \times \phi + F_0
      | r = F_1 \times \phi
      | c = {{Defof|Fibonacci Number}} $F_0 = 0$
}}
{{eqn | r = 1 \times \phi
      | c = {{Defof|Fibonacci Number}} $F_1 = 1$
}}
{{eqn | r = \phi^1
      | c = 
}}
{{end-eqn}}
Thus $P \left({1}\right)$ is seen to hold.
This is the basis for the induction.
==== Induction Hypothesis ====
Now it needs to be shown that, if $P \left({k}\right)$ is true, where $k \ge 1$, then it logically follows that $P \left({k + 1}\right)$ is true.
So this is the induction hypothesis:
:$\phi^k = F_k \phi + F_{k - 1}$
from which it is to be shown that:
:$\phi^{k + 1} = F_{k + 1} \phi + F_k$
==== Induction Step ====
This is the induction step:
{{begin-eqn}}
{{eqn | l = F_{k + 1} \phi + F_k
      | r = \left({F_k + F_{k - 1} }\right) \phi + F_k
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = F_k \left({1 + \phi}\right) + F_{k - 1} \phi
      | c = 
}}
{{eqn | r = F_k \phi^2 + F_{k - 1} \phi
      | c = Square of Golden Mean equals One plus Golden Mean
}}
{{eqn | r = \phi \left({F_k \phi + F_{k - 1} }\right)
      | c = 
}}
{{eqn | r = \phi \left({\phi^n}\right)
      | c = Induction Hypothesis
}}
{{eqn | r = \phi^{n + 1}
      | c = 
}}
{{end-eqn}}
So $P \left({k}\right) \implies P \left({k + 1}\right)$ and it follows by the Principle of Mathematical Induction that:
:$\forall n \in \Z_{\ge 0}: \phi^n = F_n \phi + F_{n - 1}$
Theorem: Fibonacci Number by Golden Mean plus Fibonacci Number of Index One Less/Negative Index

Let $n \in \Z_{\le 0}$.
Then:
:$\phi^n = F_n \phi + F_{n - 1}$
where:
:$F_n$ denotes the $n$th Fibonacci number as extended to negative indices
:$\phi$ denotes the golden mean.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\le 0}$, let $\map P n$ be the proposition:
:$\phi^n = F_n \phi + F_{n - 1}$
This can equivalently be expressed as:
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\phi^{-n} = F_{-n} \phi + F_{-n - 1}$
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = F_0 \times \phi + F_{-1}
      | r = F_0 \times \phi + \paren {-1}^0 F_1
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = F_0 \times \phi + 1
      | c = {{Defof|Fibonacci Number}} $F_1 = 1$
}}
{{eqn | r = 0 \times \phi + 1
      | c = {{Defof|Fibonacci Number}} $F_0 = 0$
}}
{{eqn | r = 1
      | c = 
}}
{{eqn | r = \phi^0
      | c = 
}}
{{end-eqn}}
Thus $\map P 0$ is seen to hold.
==== Basis for the Induction ====
$\map P 1$ is the case:
{{begin-eqn}}
{{eqn | l = F_{-1} \times \phi + F_{-2} 
      | r = \paren {-1}^0 F_1 \times \phi + \paren {-1}^{-1} F_2
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = 1 \times \phi - F_2
      | c = {{Defof|Fibonacci Number}} $F_1 = 1$
}}
{{eqn | r = \phi - 1
      | c = {{Defof|Fibonacci Number}}: $F_2 = 1$
}}
{{eqn | r = \dfrac 1 \phi
      | c = {{Defof|Golden Mean|index = 3}}
}}
{{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:
:$\phi^{-k} = F_{-k} \phi + F_{-k - 1}$
from which it is to be shown that:
:$\phi^{-\paren {k + 1} } = F_{-\paren {k + 1} } \phi + F_{-\paren {k + 1} - 1}$
==== Induction Step ====
This is the induction step:
{{begin-eqn}}
{{eqn | l = F_{-\paren {k + 1} } \phi + F_{-\paren {k + 1} - 1}
      | r = \paren {-1}^{-\paren {k + 1} + 1} F_{k + 1} \phi + \paren {-1}^{-\paren {k + 1} } F_{\paren {k + 1} + 1}
      | c = 
}}
{{eqn | r = \paren {-1}^{k + 2} F_{k + 1} \phi - \paren {-1}^{k + 2} F_{k + 2}
      | c = 
}}
{{eqn | r = \paren {-1}^{k + 2} \paren {F_{k + 1} \phi - \paren {F_{k + 1} + F_k} }
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = \paren {-1}^{k + 2} \paren {F_{k + 1} \paren {\phi - 1} - F_k}
      | c = 
}}
{{eqn | r = \paren {-1}^{k + 2} \paren {F_{k + 1} \phi^{-1} - F_k}
      | c = {{Defof|Golden Mean|index = 3}}
}}
{{eqn | r = \paren {-1}^{k + 2} F_{k + 1} \phi^{-1} + \paren {-1}^{k + 1} F_k
      | c = 
}}
{{eqn | r = \frac 1 \phi \paren {F_{-k - 1}  + F_{-k} \phi}
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = \frac 1 \phi \paren {\phi^{-k} }
      | c = Induction Hypothesis
}}
{{eqn | r = \phi^{-\paren {k + 1} }
      | c = 
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and it follows by the Principle of Mathematical Induction that:
:$\forall n \in \Z_{\le 0}: \phi^n = F_n \phi + F_{n - 1}$
Theorem: Fibonacci Number by One Minus Golden Mean plus Fibonacci Number of Index One Less

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

Proof:
{{begin-eqn}}
{{eqn | l = F_n \hat \phi + F_{n - 1}
      | r = F_n \paren {-\dfrac 1 \phi} + F_{n - 1}
      | c = Reciprocal Form of One Minus Golden Mean
}}
{{eqn | r = -\dfrac 1 \phi \paren {F_n - \phi F_{n - 1} }
      | c = 
}}
{{eqn | r = -\dfrac 1 \phi \paren {\paren {-1}^{n + 1} F_{-n} - \phi \paren {-1}^n F_{-\paren {n - 1} } }
      | c = Fibonacci Number with Negative Index
}}
{{eqn | r = -\dfrac 1 \phi \paren {\paren {-1}^{n + 1} F_{-n} + \phi \paren {-1}^{n + 1} F_{-\paren {n - 1} } }
      | c = 
}}
{{eqn | r = \paren {-1}^{n + 1} \paren {-\dfrac 1 \phi \paren {F_{-n} + \phi F_{-n + 1} } }
      | c = 
}}
{{eqn | r = \paren {-1}^{n + 1} \paren {-\dfrac 1 \phi } \paren {\phi^{-n + 1} }
      | c = Fibonacci Number by Golden Mean plus Fibonacci Number of Index One Less
}}
{{eqn | r = \paren {-1}^n \paren {\dfrac 1 {\phi^n} }
      | c = 
}}
{{eqn | r = \paren {-\dfrac 1 \phi}^n
      | c = 
}}
{{eqn | r = \hat \phi^n
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal Form of One Minus Golden Mean

:$\hat \phi = - \dfrac 1 \phi$
where:
:$\phi$ denotes the golden mean
:$\hat \phi$ denotes one minus the golden mean: $\hat \phi = 1 - \phi$.

Proof:
{{begin-eqn}}
{{eqn | l = \hat \phi
      | r = 1 - \phi
      | c = 
}}
{{eqn | r = -\left({\phi - 1}\right)
      | c = 
}}
{{eqn | r = -\frac 1 \phi
      | c = {{Defof|Golden Mean|index = 3}}
}}
{{end-eqn}}
{{qed}}
Category:Golden Mean
k9cbb5cuwgltozh1uhujnnwmhw70wd4
Theorem: Closed Form of One Minus Golden Mean

:$\hat \phi = \dfrac {1 - \sqrt 5} 2$
where:
:$\hat \phi$ denotes one minus the golden mean: $\hat \phi = 1 - \phi$.

Proof:
{{begin-eqn}}
{{eqn | l = \hat \phi
      | r = 1 - \phi
      | c = 
}}
{{eqn | r = 1 - \dfrac {1 + \sqrt 5} 2
      | c = {{Defof|Golden Mean|index = 2}}
}}
{{eqn | r = \dfrac {2 - \left({1 + \sqrt 5}\right)} 2
      | c = common denominator
}}
{{eqn | r = \dfrac {1 - \sqrt 5} 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Golden Mean
2el2dbjxygiazzwehhobjulwa0dn2bq
Theorem: Second Order Fibonacci Number in terms of Fibonacci Numbers

The second order Fibonacci number $\FF_n$ can be expressed in terms of Fibonacci numbers as:
:$\dfrac {3 n + 3} 5 F_n - \dfrac n 5 F_{n + 1}$

Proof:
Let $\map \GG z = \ds \sum_{n \mathop \ge 0} \mathop F_n z^n$ be a generating function for $\FF_n$.
Then we have:
{{begin-eqn}}
{{eqn | l = \paren {1 - z - z^2} \map \GG z
      | r = \paren {\FF_0 + \FF_1 z + \FF_2 z^2 + \FF_3 z^3 + \FF_4 z^4 + \cdots}
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\FF_0 z + \FF_1 z^2 + \FF_2 z^3 + \FF_3 z^4 + \FF_4 z^5 + \cdots}
      | c = 
}}
{{eqn | o = 
      | ro= -
      | r = \paren {\FF_0 z^2 + \FF_1 z^3 + \FF_2 z^4 + \FF_3 z^5 + \FF_4 z^6 + \cdots}
      | c = 
}}
{{eqn | r = \FF_0 + \paren {\FF_1 - \FF_0} z + \paren {\FF_2 - \FF_1 - \FF_0} z^2 + \paren {\FF_3 - \FF_2 - \FF_1} z^3 + \cdots
      | c = 
}}
{{eqn | r = \FF_0 + \paren {\FF_1 - \FF_0} z + F_0 z^2 + F_1 z^3 + \cdots
      | c = {{Defof|Second Order Fibonacci Number}}: $\FF_n - \FF_{n - 1} - \FF_{n - 2} = F_{n - 2}$
}}
{{eqn | r = z + z^2 \sum_{k \mathop \ge 0} F_k z^k
      | c = {{Defof|Second Order Fibonacci Number}}: $\FF_0 = 0$, $\FF_1 = 1$
}}
{{eqn | r = z + z^2 \map G z
      | c = where $\map G z$ is a generating function for the Fibonacci numbers
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \map \GG z
      | r = \dfrac {z + z^2 \map G z} {1 - z - z^2}
      | c = 
}}
{{eqn | r = \dfrac z {1 - z - z^2} + \dfrac z {1 - z - z^2} z \map G z
      | c = 
}}
{{eqn | r = \map G z + z \paren {\map G z}^2
      | c = Generating Function for Fibonacci Numbers: $\map G z = \dfrac z {1 - z - z^2}$
}}
{{end-eqn}}
Then from Summation over k to n of Product of kth with n-kth Fibonacci Numbers, the coefficient of $z^n$ in $\paren {\map G z}^2$ is:
:$\dfrac {\paren {n - 1} F_n + 2n F_{n - 1} } 5$
Thus the coefficient of $z^{n + 1}$ in $z \paren {\map G z}^2$ is likewise:
:$\dfrac {\paren {n - 1} F_n + 2n F_{n - 1} } 5$
and so the coefficient of $z^n$ in $\map G z + z \paren {\map G z}^2$ is:
:$F_n + \dfrac {\paren {n - 2} F_{n - 1} + 2 \paren {n - 1} F_{n - 2} } 5$
Hence:
{{begin-eqn}}
{{eqn | l = F_n + \dfrac {\paren {n - 2} F_{n - 1} + 2 \paren {n - 1} F_{n - 2} } 5
      | r = F_n + \dfrac {\paren {2 n - 2} F_{n - 1} - n F_{n - 1} + \paren {2 n - 2} F_{n - 2} } 5
      | c = 
}}
{{eqn | r = F_n + \dfrac {\paren {2 n - 2} F_n - n F_{n - 1} } 5
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = \dfrac {5 F_n + \paren {2 n - 2} F_n - n F_{n - 1} } 5
      | c = common denominator
}}
{{eqn | r = \dfrac {\paren {2 n + 3} F_n - n F_{n - 1} } 5
      | c = 
}}
{{eqn | r = \dfrac {\paren {2 n + 3} F_n + n F_n - n F_n - n F_{n - 1} } 5
      | c = 
}}
{{eqn | r = \dfrac {\paren {2 n + 3} F_n + n F_n - n \paren {F_n + F_{n - 1} } } 5
      | c = 
}}
{{eqn | r = \dfrac {\paren {2 n + 3} F_n + n F_n - n F_{n + 1} } 5
      | c = {{Defof|Fibonacci Number}}
}}
{{eqn | r = \dfrac {\paren {3 n + 3} F_n} 5 - \dfrac {n F_{n + 1} } 5
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: General Fibonacci Number in terms of Fibonacci Numbers

Let $r$ and $s$ be numbers, usually integers but not necessarily so limited.
Let $\sequence {a_n}$ be the general Fibonacci sequence:
:<nowiki>$a_n = \begin{cases}
r & : n = 0 \\
s & : n = 1 \\
a_{n - 2} + a_{n - 1} & : n > 1
\end{cases}$</nowiki>
Then $a_n$ can be expressed in Fibonacci numbers as:
:$a_n = F_{n - 1} r + F_n s$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$a_n = F_{n - 1} r + F_n s$
Theorem: Fibonacci Number plus Constant in terms of Fibonacci Numbers

Let $c$ be a number.
Let $\sequence {b_n}$ be the sequence defined as:
:$b_n = \begin{cases}
0 & : n = 0 \\
1 & : n = 1 \\
b_{n - 2} + b_{n - 1} + c & : n > 1
\end{cases}$
Then $\sequence {b_n}$  can be expressed in Fibonacci numbers as:
:$b_n = c F_{n - 1} + \paren {c + 1} F_n - c$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$b_n = c F_{n - 1} + \paren {c + 1} F_n - c$
Theorem: Fibonacci Number plus Binomial Coefficient in terms of Fibonacci Numbers

Let $m \in \Z_{>0}$ be a positive integer.
Let $\sequence {a_n}$ be the sequence defined as:
:$a_n = \begin{cases} 0 & : n = 0 \\ 1 & : n = 1 \\ a_{n - 2} + a_{n - 1} + \dbinom {n - 2} m & : n > 1 \end{cases}$
where $\dbinom {n - 2} m$ denotes a binonial coefficient.
Then $\sequence {a_n}$  can be expressed in Fibonacci numbers as:
:$a_n = F_{m + 1} F_{n - 1} + \paren {F_{m + 2} + 1} F_n - \ds \sum_{k \mathop = 0}^m \binom {n + m - k} k$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$a_n = F_{m + 1} F_{n - 1} + \paren {F_{m + 2} + 1} F_n - \ds \sum_{k \mathop = 0}^m \binom {n + m - k} k$
Theorem: Fibonacci Number plus Arbitrary Function in terms of Fibonacci Numbers

Let $\map f n$ and $\map g n$ be arbitrary arithmetic functions.
Let $\sequence {a_n}$ be the sequence defined as:
:$a_n = \begin{cases}
0 & : n = 0 \\
1 & : n = 1 \\
a_{n - 1} + a_{n - 2} + \map f {n - 2} & : n > 1
\end{cases}$
Let $\sequence {b_n}$ be the sequence defined as:
:$b_n = \begin{cases}
0 & : n = 0 \\
1 & : n = 1 \\
b_{n - 1} + b_{n - 2} + \map g {n - 2} & : n > 1
\end{cases}$
Let $\sequence {c_n}$ be the sequence defined as:
:$c_n = \begin{cases}
0 & : n = 0 \\
1 & : n = 1 \\
c_{n - 1} + c_{n - 2} + x \map f {n - 2} + y \map g {n - 2} & : n > 1
\end{cases}$
where $x$ and $y$ are arbitrary.
Then $\sequence {c_n}$ can be expressed in Fibonacci numbers as:
:$c_n = x a_n + y b_n + \paren {1 - x - y} F_n$

Proof:
=== Lemma ===
{{:Fibonacci Number plus Arbitrary Function in terms of Fibonacci Numbers/Lemma}}{{qed|lemma}}
Hence also:
:$b_n = F_n + \ds \sum_{k \mathop = 0}^{n - 2} F_{n - k - 1} \map g k$
Thus:
{{begin-eqn}}
{{eqn | l = c_n
      | r = F_n + \sum_{k \mathop = 0}^{n - 2} F_{n - k - 1} \paren {x \map f k + y \map g k}
      | c = 
}}
{{eqn | r = F_n + x \sum_{k \mathop = 0}^{n - 2} F_{n - k - 1} \map f k + y \sum_{k \mathop = 0}^{n - 2} F_{n - k - 1} \map g k
      | c = 
}}
{{eqn | r = F_n + x \paren {a_n - F_n} + y \paren {b_n - F_n}
      | c = 
}}
{{eqn | r = x a_n + y b_n + \paren {1 - x - y} F_n
      | c = 
}}
{{end-eqn}}
{{qed}}