avewright/proofwiki-math huggingface dataset:
Theorem: Space of Continuous on Closed Interval Real-Valued Functions with Supremum Norm forms Banach Space

Let $I = \closedint a b$ be a closed real interval.
Let $\map C I$ be the space of real-valued functions, continuous on $I$.
Let $\norm {\,\cdot\,}_\infty$ be the supremum norm on real-valued functions, continuous on $I$.
Then $\struct {\map C I, \norm {\,\cdot\,}_\infty}$ is a Banach space.

Proof:
A Banach space is a normed vector space, where a Cauchy sequence converges {{WRT}} the supplied norm.
To prove the theorem, we need to show that a Cauchy sequence in $\struct {\map C I, \norm {\,\cdot\,}_\infty}$ converges.
We take a Cauchy sequence $\sequence {x_n}_{n \mathop \in \N}$ in $\struct {\map C I, \norm {\,\cdot\,}_\infty}$.
Then we fix $t \in I$ and show, that a real Cauchy sequence $\sequence {\map {x_n} t}_{n \mathop \in \N}$ converges in $\struct {\R, \size {\, \cdot \,}}$ with the limit $\map x t$.
Then we prove the continuity of $\map x t$.
Finally, we show that $\sequence {x_n}_{n \mathop \in \N}$ converges in $\struct {\map C I, \norm {\,\cdot\,}_\infty}$ with the limit $\map x t$.
Theorem: Inductive Set under Mapping has Minimally Inductive Subset

Let $A$ be an inductive class under a mapping $g$.
Let $A$ be a set.
Then there exists some subset $S$ of $A$ such that $S$ is minimally inductive under $g$.

Proof:
Let $S$ be the set defined as:
:$S = \set {s: \exists t \in A: t = \map g s} \cup \set \O$
By definition, we have that:
:$\O \in S$
:$s \in S \implies \map g s \in S$
So, by definition, $S$ is inductive under $g$.
Because $A$ is inductive under $g$:
:$\O \in A$
and so by definition of subset:
:$S \subseteq A$
It remains to be shown that $S$ is minimally inductive under $g$.
Let $T \subseteq S$ such that $T$ is inductive under $g$.
It will be demonstrated by the Principle of General Induction that $T = S$.
That is:
:$\forall x \in T: x \in S$
Let $P: T \to \set {\T, \F}$ be the propositional function defined as:
:$\forall x \in T: \map P x \iff x \in S$
First it is noted that as $T$ is inductive under $g$:
:$\O \in T$
But {{apriori}} $\O \in S$.
Hence we have that:
:$\map P \O = \T$
This is the basis for the induction.
Now suppose $x \in T$ such that $\map P x = \T$.
That is:
:$x \in S$
This is the induction hypothesis.
The induction step is to show that $\map P {\map g x} = \T$.
That is:
:$\map g x \in S$
Indeed, as $T$ is inductive under $g$:
:$x \in T \implies \map g x \in T$
But again, {{apriori}}:
:$\map g x \in S$
Hence we have shown that:
:$\map P x = \T \implies \map P {\map g x} = \T$
Hence it follows by the Principle of General Induction:
:$\forall x \in T: \map P x = \T$
That is:
:$\forall x \in T: x \in S$
That is:
:$T = S$
Thus a subset of $S$ which is inductive under $g$ is necessarily equal to $S$.
Hence $S$ has no proper subset which is inductive under $g$.
Hence, by definition, $S$ is minimally inductive under $g$.
The result follows.
{{qed}}
Theorem: Recurrence Relation for Bell Numbers

Let $B_n$ be the Bell number for $n \in \Z_{\ge 0}$.
Then:
:$B_{n + 1} = \ds \sum_{k \mathop = 0}^n \dbinom n k B_k$
where $\dbinom n k$ are binomial coefficients.

Proof:
By definition of Bell numbers:
:$B_{n + 1}$ is the number of partitions of a (finite) set whose cardinality is $n + 1$.
Let $k \in \set {k \in \Z: 0 \le k \le n}$.
Let us form a partition of a (finite) set $S$ with cardinality $n + 1$ such that one component has $n + 1 - k > 0$ elements.
We can do this by first choosing $1$ element from $S$. We put this element into that single component.
Then choose $k$ more elements from $S$, and let the remaining $n - k$ elements be put into the same component as the first element.
From Cardinality of Set of Subsets and the definition of binomial coefficient, there are $\dbinom n k$ ways to do this.
For the chosen $k$ elements, there are $B_k$ ways to partition them.
Thus there are $\dbinom n k B_k$ possible partitions for $S$:
:$\dbinom n k$ of selecting $n - k$ elements to form one component with the one singled-out element
:for each of these, $B_k$ ways to partition the remaining $k$ elements.
Summing the number of ways to do this over all possible $k$:
:$\ds B_{n + 1} = \sum_{k \mathop = 0}^n \dbinom n k B_k$
{{qed}}
Theorem: Natural Numbers are Comparable/Strong Result

Let $\N$ be the natural numbers.
Let $m, n \in \N$.
Then either:
:$(1): \quad m + 1 \le n$
or:
:$(2): \quad n \le m$

Proof:
Let $\N$ be defined as the von Neumann construction $\omega$.
By definition of the ordering on von Neumann construction:
:$m \le n \iff m \subseteq n$
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is minimally inductive class under the successor mapping.
Then from Minimally Inductive Class under Progressing Mapping induces Nest, $\omega$ is a nest in which:
:$\forall m, n \in \omega: \map g x \subseteq y \lor y \subseteq x$
From the definition of $\map g x$ in this context:
:$\forall x \in \omega: \map g x = x^+$
That is:
:$\forall m, n \in \N: m + 1 \subseteq n \lor n \subseteq m$
whence the result.
{{qed}}
Theorem: Natural Numbers are Comparable/Strong Result

Let $\N$ be the natural numbers.
Let $m, n \in \N$.
Then either:
:$(1): \quad m + 1 \le n$
or:
:$(2): \quad n \le m$

Proof:
{{ProofWanted|Proof using Minimally Inductive Class under Slowly Progressing Mapping is Nest by exploiting Successor Mapping is Slowly Progressing.}}
Theorem: Natural Number m is Less than n implies n is not Greater than Successor of n

Let $\N$ be the natural numbers.
Let $m, n \in \N$.
Then:
:$m < n \implies m + 1 \le n$

Proof:
Let $\N$ be considered as the naturally ordered semigroup:
:$\struct {\N, +, \le}$
The result follows from Sum with One is Immediate Successor in Naturally Ordered Semigroup.
Theorem: Natural Number m is Less than n implies n is not Greater than Successor of n

Let $\N$ be the natural numbers.
Let $m, n \in \N$.
Then:
:$m < n \implies m + 1 \le n$

Proof:
Let $\N$ be defined as the von Neumann construction $\omega$.
By definition of the ordering on von Neumann construction:
:$m \le n \iff m \subseteq n$
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is minimally inductive class under the successor mapping.
The result is then a direct application of Characteristics of Minimally Inductive Class under Progressing Mapping: Image of Proper Subset is Subset:
:$m \subset n \implies m^+ \subseteq n$
{{qed}}
Theorem: Natural Number Ordering is Preserved by Successor Mapping

Let $\N$ be the natural numbers.
Let $m, n \in \N$.
Then:
:$n \le m \implies n^+ \le m^+$

Proof:
Let $\N$ be defined as the von Neumann construction $\omega$.
By definition of the ordering on von Neumann construction:
:$m \le n \iff m \subseteq n$
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is minimally inductive class under the successor mapping.
From Successor Mapping on Natural Numbers is Progressing, this successor mapping is a progressing mapping.
From Characteristics of Minimally Inductive Class under Progressing Mapping: Mapping Preserves Subsets:
:$\forall m, n \in \omega: m \subseteq n \implies m^+ \subseteq n^+$
{{qed}}
Theorem: Non-Empty Bounded Subset of Natural Numbers has Greatest Element

Let $\omega$ be the set of natural numbers defined as the von Neumann construction.
Then every non-empty bounded subset of $\omega$ has a greatest element.

Proof:
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\omega$ is minimally inductive class under the successor mapping.
From Successor Mapping on Natural Numbers is Progressing, this successor mapping is a progressing mapping.
The result is a direct application of Non-Empty Bounded Subset of Minimally Inductive Class under Progressing Mapping has Greatest Element.
{{qed}}
Theorem: Natural Number m is Less than n iff m is an Element of n

Let $\omega$ be the set of natural numbers defined as the von Neumann construction.
Let $m, n \in \omega$.
Then:
:$m < n \iff m \in n$
That is, every natural number is the set of all smaller natural numbers.

Proof:
By definition of the ordering on von Neumann construction:
:$m \le n \iff m \subseteq n$
Theorem: Trichotomy Law for Natural Numbers

Let $\omega$ be the set of natural numbers defined as the von Neumann construction.
Let $m, n \in \omega$.
Then one of the following cases holds:
:$m \in n$
:$m = n$
:$n \in m$

Proof:
By definition of the ordering on von Neumann construction:
:$m \le n \iff m \subseteq n$
From Natural Number m is Less than n iff m is an Element of n, we have:
:$m < n \iff m \in n$
Hence the theorem is equivalent to the statement that for every $m, n \in \omega$, one of the following holds:
:$m \subsetneq n$
:$m = n$
:$n \subsetneq m$
The result follows from Natural Numbers are Comparable: Strong Result.
{{qed}}
Theorem: Natural Number Less than or Equal to Successor of Another

Let $\N$ be the natural numbers.
Let $m, n \in \N$ such that $m \le n^+$.
Then either:
:$(1): \quad m \le n$
or:
:$(2): \quad m = n^+$

Proof:
Let $m \le n^+$.
Suppose $m \le n$ is false.
Then:
:$n^+ \le m$
and because $m \le n^+$:
:$m = n^+$
{{qed}}
Theorem: Mapping whose Image of Natural Number n is Subset of Image of Successor

Let $f: \N \to A$ be a mapping from the set of natural numbers $\N$ to a class $A$.
Let $f$ have the property that:
:$\forall n \in \N: \map f n \subseteq \map f {n^+}$
where $n^+$ is the successor of $n$.
Then:
:$\forall n, m \in N: n \le m \implies \map f n \subseteq \map f m$

Proof:
Let us establish that:
:$n = m \implies \map f n = \map f m$
and so:
:$n = m \implies \map f n \subseteq \map f m$
Hence it is sufficient to demonstrate that:
:$\forall n < m: \map f n \subseteq \map f m$
The proof will proceed by the Principle of Finite Induction on $\N$.
Let $S$ be the set defined as:
:$S := \set {m \in \N: \forall n < m: \map f n \subseteq \map f m}$
That is, $S$ is to be the set of all $n$ such that:
:$\forall n < m: \map f n \subseteq \map f m$
First we note that:
:$\not \exists n \in \N: n < 0$
Thus $0 \in S$ vacuously.
Theorem: Mapping whose Image of Natural Number n is Subset of Image of Successor/Corollary

Let $f$ have the property that:
:$\forall n \in \N: \map f n \subsetneqq \map f {n^+}$
where $n^+$ is the successor of $n$.
Then:
:$\forall n, m \in N: n < m \implies \map f n \subsetneqq \map f m$

Proof:
The proof will proceed by the Principle of Finite Induction on $\N$.
Let $S$ be the set defined as:
:$S := \set {m \in \N: \forall n < m: \map f n \subsetneqq \map f m}$
That is, $S$ is to be the set of all $n$ such that:
:$\forall n < m: \map f n \subsetneqq \map f m$
First we note that:
:$\not \exists n \in \N: n < 0$
Thus $0 \in S$ vacuously.
Theorem: Finite Class is Set

Let $A$ be a finite class.
Then $A$ is a set.

Proof:
Let it be assumed that all classes are subclasses of a basic universe $V$.
The proof proceeds by induction.
For all $n \in \N$, let $\map P n$ be the proposition:
:If $A$ is a finite class with $n$ elements, then $A$ is a set.
The {{axiom-link|the Empty Set|Class Theory}} gives that the empty class $\O$ is a set.
From Empty Set is Unique, $\O$ is the only set (and hence class) with $0$ elements.
Thus $\map P 0$ is seen to hold.
Theorem: Non-Empty Finite Set of Natural Numbers has Greatest Element

Let $A$ be a non-empty finite set of natural numbers.
Then $A$ has a greatest element.

Proof:
The proof proceeds by induction.
By definition, if $A$ is a non-empty finite set, then $A$ has $m$ elements for some $m \in \N$ such that $m > 0$.
So, for all $n \in \N_{>0}$, let $\map P n$ be the proposition:
:If $A$ has $n$ elements, then $A$ has a greatest element.
Theorem: Set of Subsets of Element of Minimally Inductive Class under Progressing Mapping is Finite

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Let $x \in M$.
Let $S$ be the set of all $y \in M$ such that $y \subseteq x$.
Then $S$ is finite.

Proof:
The proof proceeds by general induction.
For all $x \in M$, let $\map P x$ be the proposition:
:$\set {y \in M: y \subseteq x}$ is finite.
Theorem: Minimally Inductive Class under Progressing Mapping with Fixed Element is Finite

Let $M$ be a class which is minimally inductive under a progressing mapping $g$.
Let there exist an element $x \in M$ such that $x = \map g x$.
Then $M$ is a finite class.

Proof:
By Set of Subsets of Element of Minimally Inductive Class under Progressing Mapping is Finite, the set:
:$\set {y \in M: y \subseteq x}$
is finite.
From Fixed Point of Progressing Mapping on Minimally Inductive Class is Greatest Element, $x$ is the greatest element of $M$.
Thus:
:$M = \set {y \in M: y \subseteq x}$
Hence the result.
{{qed}}
Theorem: Subset of Natural Numbers is either Finite or Denumerable

Let $S$ be a subset of the natural numbers $\N$.
Then $S$ is either finite or denumerable.

Proof:
Let $\omega$ denote the set of natural numbers as defined by the von Neumann construction.
By the Well-Ordering Principle, $\omega$ is well-ordered by the $\le$ relation.
Thus from the Well-Ordering Principle, $S$ has a smallest element.
Let this smallest element of $S$ be denoted $s_0$.
Also from the Well-Ordering Principle, every subset of $S$ also has a smallest element.
{{ProofWanted|establish a sequence where $s_k$ is the smallest element of $S_k$ where $S_k {{=}} S_{k - 1} \setminus \set {s_{k - 1} }$, and then build a mapping $f$ such that $\map f {s_k} \to \set {s_0, s_1, \ldots, s_{k - 1} }$ and show it's progressing, or something, but it's tedious.}}
Theorem: Non-Empty Set of Natural Numbers with no Greatest Element is Denumerable

Let $A$ be a non-empty set of natural numbers.
Let $A$ have no greatest element.
Then $A$ is a countably infinite set.

Proof:
{{AimForCont}} $A$ is finite.
From Subset of Naturals is Finite iff Bounded, it follows that $A$ is bounded.
Hence $A$ has a greatest element.
This contradicts the fact that $A$ has no greatest element.
Hence by Proof by Contradiction it follows that $A$ is not finite.
From Subset of Natural Numbers is either Finite or Denumerable, $A$ is a countably infinite set.
{{Qed}}
Theorem: Like Electric Charges Repel

Let $a$ and $b$ be stationary particles, each carrying an electric charge of $q_a$ and $q_b$ respectively.
Let $q_a$ and $q_b$ be of the same polarity.
That is, let $q_a$ and $q_b$ be like charges.
Then the forces exerted by $a$ on $b$, and by $b$ on $a$, are such as to cause $a$ and $b$ to repel each other.

Proof:
By Coulomb's Law of Electrostatics:
:$\mathbf F_{a b} \propto \dfrac {q_a q_b {\mathbf r_{a b} } } {r^3}$
where:
:$\mathbf F_{a b}$ is the force exerted on $b$ by the electric charge on $a$
:$\mathbf r_{a b}$ is the displacement vector from $a$ to $b$
:$r$ is the distance between $a$ and $b$.
Let $q_a$ and $q_b$ both be positive.
Then $q_a q_b$ is a positive number multiplied by a positive number. 
Thus $q_a q_b$ is a positive number.
Similarly, let $q_a$ and $q_b$ both be negative.
Then $q_a q_b$ is a negative number multiplied by a negative number.
Thus $q_a q_b$ is similarly a positive number.
So, when $q_a$ and $q_b$ are like charges, $\dfrac {q_a q_b} {r^3}$ is a positive number.
Hence $\mathbf F_{a b}$ is in the same direction as the displacement vector from $a$ to $b$.
That is, the force exerted on $b$ by the electric charge on $a$ is in the direction away from $a$.
The same applies to the force exerted on $a$ by the electric charge on $b$.
That is, the force exerted on $b$ by the electric charge on $a$ is in the direction away from $b$.
The effect of these forces is to cause $a$ and $b$ to push apart, that is, to repel each other.
Theorem: Unlike Electric Charges Attract

Let $a$ and $b$ be stationary particles, each carrying an electric charge of $q_a$ and $q_b$ respectively.
Let $q_a$ and $q_b$ be of the opposite polarity.
That is, let $q_a$ and $q_b$ be unlike charges.
Then the forces exerted by $a$ on $b$, and by $b$ on $a$, are such as to cause $a$ and $b$ to attract each other.

Proof:
By Coulomb's Law of Electrostatics:
:$\mathbf F_{a b} \propto \dfrac {q_a q_b {\mathbf r_{a b} } } {r^3}$
where:
:$\mathbf F_{a b}$ is the force exerted on $b$ by the electric charge on $a$
:$\mathbf r_{a b}$ is the displacement vector from $a$ to $b$
:$r$ is the distance between $a$ and $b$.
{{WLOG}}, let $q_a$ be positive and $q_b$ be negative.
Then $q_a q_b$ is a positive number multiplied by a negative number. 
Thus $q_a q_b$ is a negative number.
Hence $\mathbf F_{a b}$ is in the opposite direction to the displacement vector from $a$ to $b$.
That is, the force exerted on $b$ by the electric charge on $a$ is in the direction towards $a$.
The same applies to the force exerted on $a$ by the electric charge on $b$.
That is, the force exerted on $b$ by the electric charge on $a$ is in the direction towards $b$.
The effect of these forces is to cause $a$ and $b$ to pull together, that is, to attract each other.
Theorem: Value of Vacuum Permittivity

The value of the '''vacuum permittivity''' is calculated as:
:$\varepsilon_0 = 8 \cdotp 85418 \, 78128 (13) \times 10^{-12} \, \mathrm F \, \mathrm m^{-1}$ (farads per metre)
with a relative uncertainty of $1 \cdotp 5 \times 10^{-10}$.

Proof:
The '''vacuum permittivity''' is the physical constant denoted $\varepsilon_0$ defined as:
:$\varepsilon_0 := \dfrac {e^2} {2 \alpha h c}$
where:
:$e$ is the elementary charge
:$\alpha$ is the fine-structure constant
:$h$ is Planck's constant
:$c$ is the speed of light defined in $\mathrm m \, \mathrm s^{-1}$
$e$ is defined precisely as:
:$e = 1 \cdotp 60217 \, 6634 \times 10^{-19} \, \mathrm C$ (coulombs)
$\alpha$ has the value determined experimentally as:
:$\alpha \approx 0 \cdotp 00729 \, 73525 \, 693 (11)$
$h$ is defined precisely as:
:$h = 6 \cdotp 62607 \, 015 \times 10^{-34} \, \mathrm J \, \mathrm s$ (joule seconds)
$c$ is defined precisely as:
:$c = 299 \, 792 \, 458 \, \mathrm m \, \mathrm s^{-1}$ (metres per second)
Hence $\varepsilon_0$ can be calculated as:
{{begin-eqn}}
{{eqn | l = \varepsilon_0
      | r = \dfrac {e^2} {2 \alpha h c}
      | rr= \dfrac {\mathrm C^2} {\mathrm J \, s \times \mathrm m \, \mathrm s^{-1} }
      | c = 
}}
{{eqn | r = \dfrac {\paren {1 \cdotp 60217 \, 6634 \times 10^{-19} }^2} {0 \cdotp 00729 \, 73525 \, 693 (11) \times 6 \cdotp 62607 \, 015 \times 10^{-34} \times 299 \, 792 \, 458}
      | rr= \dfrac {\paren {\mathrm A \, \mathrm s}^2} {\frac {\mathrm {kg} \times \mathrm m^2} {\mathrm s^2} \times \mathrm s \times \mathrm m \, \mathrm s^{-1} }
      | c = Base Units of Coulomb, Base Units of Joule
}}
{{eqn | r = 8 \cdotp 85418 \, 78128 (13) \times 10^{-12}
      | rr= \dfrac {\mathrm A^2 \times \mathrm s^4} {\mathrm {kg} \times \mathrm m^3}
      | c = 
}}
{{eqn | r = 8 \cdotp 85418 \, 78128 (13) \times 10^{-12}
      | rr= \dfrac {\mathrm F} {\mathrm m}
      | c = Base Units of Farad
}}
{{end-eqn}}
{{qed}}
Theorem: Value of Vacuum Permittivity

The value of the '''vacuum permittivity''' is calculated as:
:$\varepsilon_0 = 8 \cdotp 85418 \, 78128 (13) \times 10^{-12} \, \mathrm F \, \mathrm m^{-1}$ (farads per metre)
with a relative uncertainty of $1 \cdotp 5 \times 10^{-10}$.

Proof:
The '''vacuum permittivity''' is the physical constant denoted $\varepsilon_0$ defined as:
:$\varepsilon_0 := \dfrac 1 {\mu_0 c^2}$
where:
:$\mu_0$ is the vacuum permeability defined in $\mathrm H \, \mathrm m^{-1}$ (henries per metre)
:$c$ is the speed of light defined in $\mathrm m \, \mathrm s^{-1}$
$\mu_0$ has the value determined experimentally as:
:$\mu_0 \approx 1 \cdotp 25663 \, 70621 \, 2 (19) \times 10^{-6} \, \mathrm H \, \mathrm m^{-1}$
$c$ is defined precisely as:
:$c = 299 \, 792 \, 458 \, \mathrm m \, \mathrm s^{-1}$
Hence $\varepsilon_0$ can be calculated as:
{{begin-eqn}}
{{eqn | l = \varepsilon_0
      | r = \dfrac 1 {\mu_0 c^2}
      | rr= \dfrac 1 {\mathrm H \, \mathrm m^{-1} \times \paren {\mathrm m \, \mathrm s^{-1} }^2}
      | c = 
}}
{{eqn | r = \dfrac 1 {1 \cdotp 25663 \, 70621 \, 2 (19) \times 10^{-6} \times \paren {299 \, 792 \, 458}^2}
      | rr= \dfrac 1 {\frac {\mathrm {kg} \times \mathrm m^2} {\mathrm s^2 \times \mathrm A^2} \, \mathrm m^{-1} \times \paren {\mathrm m \, \mathrm s^{-1} }^2}
      | c = Base Units of Henry
}}
{{eqn | r = 8 \cdotp 85418 \, 78128 (13) \times 10^{-12}
      | rr= \dfrac {\mathrm A^2 \times \mathrm s^4} {\mathrm {kg} \times \mathrm m^3}
      | c = 
}}
{{eqn | r = 8 \cdotp 85418 \, 78128 (13) \times 10^{-12}
      | rr= \dfrac {\mathrm F} {\mathrm m}
      | c = Base Units of Farad
}}
{{end-eqn}}
{{qed}}
Theorem: Successor Mapping on Natural Numbers has no Fixed Element

Let $\N$ denote the set of natural numbers.
Then:
:$\forall n \in \N: n + 1 \ne n$

Proof:
Consider the set of natural numbers as defined by the von Neumann construction.
From Von Neumann Construction of Natural Numbers is Minimally Inductive, $\N$ is a minimally inductive class under the successor mapping.
Let $s: \N \to \N$ denote this successor mapping:
:$\forall x \in \N: \map s x := x + 1$
{{AimForCont}} $\exists n \in \N: n = n + 1$
From Fixed Point of Progressing Mapping on Minimally Inductive Class is Greatest Element, $n$ is the greatest element of $\N$.
From Minimally Inductive Class under Progressing Mapping with Fixed Element is Finite it follows that $\N$ is a finite set.
This contradicts the fact that the natural numbers are by definition countably infinite.
{{qed}}
Theorem: Residue of Fibonacci Number Modulo Fibonacci Number/Lemma

:<nowiki>$F_{m n + 1} \equiv \paren {\begin{cases} F_1 & : m \bmod 4 = 0 \\
F_{n - 1} & : m \bmod 4 = 1 \\
\paren {-1}^n F_1 & : m \bmod 4 = 2 \\
\paren {-1}^n F_{n - 1} & : m \bmod 4 = 3 \end{cases} } \pmod {F_n}$</nowiki>

Proof:
We prove this by induction on $m$.
For all $m \in \N$, let $\map P m$ be the proposition:
:<nowiki>$F_{m n + 1} \equiv \paren {\begin{cases} F_1 & : m \bmod 4 = 0 \\
F_{n - 1} & : m \bmod 4 = 1 \\
\paren {-1}^n F_1 & : m \bmod 4 = 2 \\
\paren {-1}^n F_{n - 1} & : m \bmod 4 = 3 \end{cases} } \pmod {F_n}$</nowiki>
Theorem: Complement of Open Interval Defined by Absolute Value

:$\set {x \in \R: \size {\xi - x} \ge \delta} = \R \setminus \openint {\xi - \delta} {\xi + \delta}$
where:
:$\openint {\xi - \delta} {\xi + \delta}$ is the open real interval between $\xi - \delta$ and $\xi + \delta$
:$\setminus$ denotes the set difference operator.

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \set {x \in \R: \size {\xi - x} \ge \delta}
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \notin
      | r = \set {x \in \R: \size {\xi - x} < \delta}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \notin
      | r = \openint {\xi - \delta} {\xi + \delta}
      | c = Open Interval Defined by Absolute Value
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \in
      | r = \R \setminus \openint {\xi - \delta} {\xi + \delta}
      | c = {{Defof|Set Difference}}
}}
{{end-eqn}}
{{qed}}
Theorem: Complement of Closed Interval Defined by Absolute Value

:$\set {x \in \R: \size {\xi - x} > \delta} = \R \setminus \closedint {\xi - \delta} {\xi + \delta}$
where:
:$\closedint {\xi - \delta} {\xi + \delta}$ is the closed real interval between $\xi - \delta$ and $\xi + \delta$
:$\setminus$ denotes the set difference operator.

Proof:
{{begin-eqn}}
{{eqn | l = y
      | o = \in
      | r = \set {x \in \R: \size {\xi - x} > \delta}
      | c =
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \notin
      | r = \set {x \in \R: \size {\xi - x} \le \delta}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \notin
      | r = \closedint {\xi - \delta} {\xi + \delta}
      | c = Closed Interval Defined by Absolute Value
}}
{{eqn | ll= \leadstoandfrom
      | l = y
      | o = \in
      | r = \R \setminus \closedint {\xi - \delta} {\xi + \delta}
      | c = {{Defof|Set Difference}}
}}
{{end-eqn}}
{{qed}}