avewright/proofwiki-math huggingface dataset:
Theorem: Integral Ideal is Ideal of Ring

Let $J$ be a non-empty subset of the set of integers $\Z$.
Then:
:$J$ is an integral ideal
{{iff}}:
:$J$ is an ideal of the ring of integers $\struct {\Z, +, \times}$.

Proof:
Let $J \subseteq \Z$ fulfil the conditions of an integral ideal:
:$(1): \quad n, m \in J \implies m + n \in J, m - n \in J$
:$(2): \quad n \in J, r \in \Z \implies r n \in J$
First note that $J$ is non-empty by definition.
Then from $(1)$ we have in particular:
:$n, m \in J \implies m - n \in J$
Thus by the One-Step Subgroup Test:
:$\struct {J, +}$ is a subgroup of the additive group of integers $\struct {\Z, +}$.
Then from $(2)$ we have:
:$n \in J, r \in \Z \implies r n \in J$
and by Integer Multiplication is Commutative it follows that:
:$n \in J, r \in \Z \implies n r \in J$
Thus it is seen that the conditions are fulfilled for $J$ to be an ideal of the ring of integers $\struct {\Z, +, \times}$.
{{qed|lemma}}
Suppose $J \subseteq \Z$ such that:
:$(3): \quad \struct {J, +}$ is a subgroup of $\struct {\Z, +}$
:$(4): \quad \forall n \in J: \forall r \in R: n r \in J \land r n \in J$
From $(4)$, $(2)$ immediately follows.
From $(3)$ it follows from the One-Step Subgroup Test that:
:$\forall n, m \in J: m - n \in J$
which is a restatement of $(1)$.
Thus the conditions are fulfilled for $J$ to be an integral ideal.
{{qed}}
Theorem: Set of Integer Multiples is Integral Ideal

Let $m \in \Z$ be an integer.
Let $m \Z$ denote the set of integer multiples of $m$.
Then $m \Z$ is an integral ideal.

Proof:
First note that $m \times 0 \in m \Z$ whatever $m$ may be.
Thus $m \Z \ne \O$.
Let $a, b \in m \Z$.
Then:
{{begin-eqn}}
{{eqn | l = a + b
      | r = m j + m k
      | c = for some $j, k \in \Z$ by definition of $m \Z$
}}
{{eqn | r = m \paren {j + k}
      | c = 
}}
{{eqn | o = \in
      | r = m \Z
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = a - b
      | r = m j - m k
      | c = for some $j, k \in \Z$ by definition of $m \Z$
}}
{{eqn | r = m \paren {j - k}
      | c = 
}}
{{eqn | o = \in
      | r = m \Z
      | c = 
}}
{{end-eqn}}
Let $r \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = r a
      | r = r \paren {m j}
      | c = for some $j \in \Z$ by definition of $m \Z$
}}
{{eqn | r = m \paren {r j}
      | c = 
}}
{{eqn | o = \in
      | r = m \Z
      | c = 
}}
{{end-eqn}}
Thus the conditions for $m \Z$ to be an integral ideal are fulfilled.
Hence the result.
{{qed}}
Theorem: Minimal Smooth Surface Spanned by Contour

Let $\map z {x, y}: \R^2 \to \R$ be a real-valued function.
Let $\Gamma$ be a closed contour in $3$-dimensional Euclidean space.
Then the smooth surface of least area spanned by the contour $\Gamma$ has to satisfy the following Euler's equation:
:$r \paren {1 + q^2} - 2 s p q + t \paren {1 + p^2} = 0$
where:
{{begin-eqn}}
{{eqn | l = p
      | r = z_x
}}
{{eqn | l = q
      | r = z_y
}}
{{eqn | l = r
      | r = z_{xx}
}}
{{eqn | l = s
      | r = z_{xy}
}}
{{eqn | l = t
      | r = z_{yy}
}}
{{end-eqn}}
with subscript denoting respective partial derivatives.
In other words, its mean curvature has to vanish.

Proof:
The surface area for a smooth surface embedded in $3$-dimensional Euclidean space is given by:
:$\ds A \sqbrk z = \iint_\Gamma \sqrt {1 + z_x^2 + z_y^2} \rd x \rd y$
{{MissingLinks|We need a link to the above}}
It follows that:
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d x} \frac \partial {\partial z_x} \sqrt {1 + z_x^2 + z_y^2}
      | r = \dfrac \d {\d x} \frac {z_x} {\sqrt {1 + z_x^2 + z_y^2} }
}}
{{eqn | r = \frac {z_{xx} + z_y^2 z_{xx} - z_x z_y z_{xy} } {\paren {1 + z_x^2 + z_y^2}^{\frac 3 2} }
}}
{{eqn | r = \frac {r \paren {1 + q^2} - p q s } {\paren {1 + p^2 + q^2}^{\frac 3 2} }
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \dfrac \d {\d y} \frac \partial {\partial z_y} \sqrt {1 + z_x^2 + z_y^2}
      | r = \dfrac \d {\d y} \frac {z_y} {\sqrt {1 + z_x^2 + z_y^2} }
}}
{{eqn | r = \frac {z_{yy} + z_x^2 z_{yy} - z_x z_y z_{xy} } {\paren {1 + z_x^2 + z_y^2}^{\frac 3 2} }
}}
{{eqn | r = \frac {t \paren {1 + p^2} - p q s } {\paren {1 + p^2 + q^2}^{\frac 3 2} }
}}
{{end-eqn}}
By Euler's equation:
:$\dfrac {r \paren {1 + q^2} - 2 s p q + t \paren {1 + p^2} } {\paren {1 + p^2 + q^2}^{\frac 3 2} } = 0$
Due to the smoothness of the surface, $1 + p^2 + q^2$ is bounded.
Hence, the following equation is sufficient:
:$r \paren {1 + q^2} - 2 s p q + t \paren {1 + p^2} = 0$
Introduce the following change of variables:
{{begin-eqn}}
{{eqn | l = E
      | r = 1 + p^2
}}
{{eqn | l = F
      | r = p q
}}
{{eqn | l = G
      | r = 1 + q^2
}}
{{eqn | l = e
      | r = \dfrac r {\sqrt {1 + p^2 + q ^2} }
}}
{{eqn | l = f
      | r = \dfrac s {\sqrt {1 + p^2 + q^2} }
}}
{{eqn | l = g
      | r = \dfrac t {\sqrt {1 + p^2 + q^2} }
}}
{{end-eqn}}
Then Euler's equation can be rewritten as:
:$\dfrac {E g - 2 F f + G e} {2 \paren {E G - F^2} } = 0$
By definition, mean curvature is:
:$M = \dfrac {E g - 2 F f + G e} {2 \paren {E G - F^2} }$
Hence:
:$M = 0$
{{qed}}
Theorem: Integral Ideal is Set of Integer Multiples

Let $J$ be an integral ideal.
Then $J$ is in the form of a set of integer multiples $m \Z$ for some $m \in \Z$.

Proof:
By definition, $J$ satisfies the following conditions:
:$(1): \quad n, m \in J \implies m + n \in J, m - n \in J$
:$(2): \quad n \in J, r \in \Z \implies r n \in J$
First note that the null ideal $\set 0$ is an integral ideal.
This is of the form $0 \Z$.
Let $J \ne \set 0$.
Then $\exists a \in J: a \ne 0$.
As $0 \in \Z$ it follows from $(2)$ that:
:$0 \times a = 0 \in J$
Thus from $(1)$ we have that:
:$0 - a \in J$
so both $a \in J$ and $-a \in J$
Thus there exists $a \in J: a > 0$.
Consider the set $S = \set {x \in J: x > 0}$.
$S$ is bounded below by $0$, for example.
$S$ is not empty, because it has been established that $a \in S$.
By Set of Integers Bounded Below has Smallest Element, $S$ has a smallest element, $m$, say.
Consider $y \in m \Z$.
By definition of $m \Z$, $y = r m$ for some $r \in \Z$.
Thus, by $(2)$, $y \in J$.
So by definition of subset, $m \Z \subseteq J$.
It remains to be demonstrated that $J \subseteq m \Z$.
{{AimForCont}} $k \in J: k \notin m \Z$.
As $k \in J$, it follows from $(1)$ that $0 - k = -k \in J$ also.
Either $k > 0$ or $-k > 0$.
{{WLOG}}, let $k > 0$.
If $k < m$, then that contradicts the statement that $m \in J$ is the smallest element of $J$ that is (strictly) positive.
So $k > m$.
Consider the set $T = \set {x \in m \Z: x > k}$.
$T$ is not empty, as $m \paren {k + 1}$, for example, is bound to be in $T$ (even if $m = 1$, the smallest it can be).
By Set of Integers Bounded Below has Smallest Element, $T$ has a smallest element, $m s$, say.
Then:
:$m \paren {s - 1} < k < m s$
As $k > m$ it follows also that $m \paren {s - 1} > 0$.
Equality cannot happen because $k \notin m \Z$.
But we have that $k \in J$ and so:
:$m s - k \in J$
and:
:$k - m \paren {s - 1} \in J$
But $m s - k < m$, otherwise $m \paren {s - 1} > k$ which contradicts the statement that $m s \in J$ is the smallest element of $T$
Thus $m s - k \in J$ and $0 < m s - k < m$.
This contradicts the statement that $m$ is the smallest element of $J$ that is (strictly) positive.
Hence by Proof by Contradiction there is no such $k$.
Hence $J \subseteq m \Z$ and the result follows.
Theorem: Difference between Odd Squares is Divisible by 8

Let $a$ and $b$ be odd integers.
Then $a^2 - b^2$ is divisible by $8$.

Proof:
Let $a = 2 m + 1$, $b = 2 n + 1$.
Then:
{{begin-eqn}}
{{eqn | l = a^2 - b^2 
      | r = \paren {2 m + 1}^2 - \paren {2 n + 1}^2
      | c = 
}}
{{eqn | r = \paren {4 m^2 + 4 m + 1} - \paren {4 n^2 + 4 n - 1}
      | c = 
}}
{{eqn | r = 4 \paren {m^2 - n^2} + 4 \paren {m - n}
      | c = 
}}
{{eqn | r = 4 \paren {m + n} \paren {m - n} + 4 \paren {m - n}
      | c = Difference of Two Squares
}}
{{eqn | r = 4 \paren {m + n + 1} \paren {m - n}
      | c = 
}}
{{end-eqn}}
Suppose $m - n$ is even such that $m - n = 2 k$.
Then:
:$a^2 - b^2 = 4 \paren {2 k} \paren {m + n + 1} = 8 k \paren {m + n + 1}$
and so is divisible by $8$.
Suppose $m - n$ is odd such that $m - n = 2 k + 1$.
Then:
:$m + n + 1 = m + \paren {2 k + 1 + m} + 1 = 2 m + 2 k = 2 \paren {m + k}$
and so:
:$a^2 - b^2 = 4 \paren {2 k + 1} 2 \paren {m + k} = 8 \paren {2 k + 1} \paren {m + k}$
and so is again divisible by $8$.
The result follows.
{{qed}}
Theorem: Norms Equivalent to Absolute Value on Rational Numbers/Necessary Condition

Let $\alpha \in \R_{> 0}$.
Let $\norm {\,\cdot\,}:\Q \to \R$ be the mapping defined by:
:$\forall x \in \Q: \norm x = \size x^\alpha$
where $\size x$ is the absolute value of $x$ in $\Q$.
Let $\norm {\,\cdot\,}$ be a norm on $\Q$.
Then:
:$\alpha \le 1$

Proof:
The contrapositive is proved.
Let $\alpha > 1$.
The {{Norm-axiom-mult|3}} is not satisfied:
{{begin-eqn}}
{{eqn | l = \norm {1 + 1}
      | r = \size {1 + 1}^\alpha
}}
{{eqn | r = 2^\alpha
}}
{{eqn | o = >
      | r = 2
      | c = Power Function on Base Greater than One is Strictly Increasing
}}
{{eqn | r = \size 1^\alpha + \size 1^\alpha
}}
{{eqn | r = \norm 1 + \norm 1
}}
{{end-eqn}}
By Rule of Transposition the result follows.
Theorem: Norms Equivalent to Absolute Value on Rational Numbers/Sufficient Condition

Let $\alpha \in \R_{> 0}$.
Let $\norm {\,\cdot\,}: \Q \to \R$ be the mapping defined by:
:$\forall x \in \Q: \norm x = \size x^\alpha$
where $\size x$ is the absolute value of $x$ in $\Q$.
Then:
:$\alpha \le 1 \implies \norm {\,\cdot\,}$ is a norm on $\Q$

Proof:
Suppose $\alpha \le 1$.
It is shown that $\norm {\,\cdot\,}$ satisfies the norm axioms $(\text N 1)$-$(\text N 3)$.
=== {{Norm-axiom-mult|1|nolink}} ===
Let $x \in \Q$.
{{begin-eqn}}
{{eqn | l = \norm x = 0
      | o = \leadstoandfrom
      | r = \size x^\alpha = 0
      | c = Definition of $\norm {\,\cdot\,}$
}}
{{eqn | o = \leadstoandfrom
      | r = \size x = 0
      | c = Definition of $a$ to the power of $r$ for $a \in \R_{\ge 0}$ and $r \in \R_{> 0}$
}}
{{eqn | o = \leadstoandfrom
      | r = x = 0
      | c = Absolute Value is Norm and {{Norm-axiom-mult|1}}
}}
{{end-eqn}}
{{qed|lemma}}
=== {{Norm-axiom-mult|2|nolink}} ===
Let $x, y \in \Q$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {x y}
      | r = \size {x y}^\alpha
      | c = Definition of $\norm {\,\cdot\,}$
}}
{{eqn | r = \paren {\size x \size y}^\alpha
      | c = Absolute Value is Norm and {{Norm-axiom-mult|2}}
}}
{{eqn | r = \size x^\alpha \size {y}^\alpha
      | c = Power of Product
}}
{{eqn | r = \norm x \norm y
      | c = Definition of $\norm {\,\cdot\,}$
}}
{{end-eqn}}
{{qed|lemma}}
=== {{Norm-axiom-mult|3|nolink}} ===
Let $x, y \in \Q$.
{{WLOG}}, let $\norm y < \norm x$.
If $\norm x = 0$ then $\norm y = 0$.
By {{Norm-axiom-mult|1}} above:
:$x = y = 0$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {x + y}
      | r = \norm 0
}}
{{eqn | r = 0
}}
{{eqn | r = 0 + 0
}}
{{eqn | r = \norm x + \norm y
}}
{{end-eqn}}
If $\norm x > 0$ then:
:$\norm x > 0 \leadstoandfrom \size x^\alpha > 0 \leadstoandfrom \size x > 0$
Hence:
{{begin-eqn}}
{{eqn | l = \norm {x + y}
      | r = \size {x + y}^\alpha
}}
{{eqn | o = \le
      | r = \paren {\size x + \size y}^\alpha
      | c = {{Norm-axiom-mult|3}}
}}
{{eqn | r = \size x^\alpha \paren {1 + \dfrac {\size y} {\size x} }^\alpha
}}
{{eqn | o = \le
      | r = \size x^\alpha \paren {1 + \dfrac {\size y} {\size x} }
      | c = Power Function on Base Greater than One is Strictly Increasing
}}
{{eqn | o = \le
      | r = \size x^\alpha \paren {1 + \dfrac {\size y^\alpha} {\size x^\alpha} }
      | c = Power Function on Base between Zero and One is Strictly Decreasing
}}
{{eqn | o = \le
      | r = \size x^\alpha + \size y^\alpha
}}
{{eqn | r = \norm x + \norm y
}}
{{end-eqn}}
Theorem: Lowest Common Multiple of Integers with Common Divisor

Let $b, d \in \Z_{>0}$ be (strictly) positive integers
Then:
:$\lcm \set {a b, a d} = a \lcm \set {b, d}$
where:
:$a \in \Z_{>0}$
:$\lcm \set {b, d}$ denotes the lowest common multiple of $m$ and $n$.

Proof:
We have that:
{{begin-eqn}}
{{eqn | l = b
      | o = \divides
      | r = \lcm \set {b, d}
      | c = {{Defof|Lowest Common Multiple of Integers}}
}}
{{eqn | lo= \land
      | l = d
      | o = \divides
      | r = \lcm \set {b, d}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r b
      | r = \lcm \set {b, d}
      | c = for some $r \in \Z$
}}
{{eqn | lo= \land
      | l = s d
      | r = \lcm \set {b, d}
      | c = for some $s \in \Z$
}}
{{eqn | ll= \leadsto
      | l = r \paren {a b}
      | r = a \lcm \set {b, d}
      | c = 
}}
{{eqn | lo= \land
      | l = s \paren {a d}
      | r = a \lcm \set {b, d}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a b
      | o = \divides
      | r = a \lcm \set {b, d}
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | lo= \land
      | l = a d
      | o = \divides
      | r = a \lcm \set {b, d}
      | c = 
}}
{{end-eqn}}
Suppose $n \in \Z$ such that $a b \divides n$ and $a d \divides n$.
It will be shown that $a \lcm \set {b, d} \divides n$.
So:
{{begin-eqn}}
{{eqn | l = a b
      | o = \divides
      | r = n
      | c = by hypothesis
}}
{{eqn | lo= \land
      | l = a d
      | o = \divides
      | r = n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a r b
      | r = n
      | c = for some $r \in \Z$
}}
{{eqn | lo= \land
      | l = a s d
      | r = n
      | c = for some $s \in \Z$
}}
{{eqn | ll= \leadsto
      | l = r b
      | r = \dfrac n a
      | c = 
}}
{{eqn | lo= \land
      | l = s d
      | r = \dfrac n a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b
      | o = \divides
      | r = \dfrac n a
      | c = {{Defof|Divisor of Integer}}
}}
{{eqn | lo= \land
      | l = d
      | o = \divides
      | r = \dfrac n a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \lcm \set {b, d}
      | o = \divides
      | r = \dfrac n a
      | c = LCM Divides Common Multiple
}}
{{eqn | lo= \land
      | l = a \lcm \set {b, d}
      | o = \divides
      | r = n
      | c = 
}}
{{end-eqn}}
Thus we have:
:$a b \divides a \lcm \set {b, d} \land a d \divides a \lcm \set {b, d}$
and:
:$a b \divides n \land a d \divides n \implies a \lcm \set {b, d} \divides n$
It follows from LCM iff Divides All Common Multiples that:
:$\lcm \set {a b, a d} = a \lcm \set {b, d}$
{{qed}}
Theorem: Addition of Fractions

Let $a, b, c, d \in \Z$ such that $b d \ne 0$.
Then:
:$\dfrac a b + \dfrac c d = \dfrac {a D + B c} {\lcm \set {b, d} }$
where:
:$B = \dfrac b {\gcd \set {b, d} }$
:$D = \dfrac d {\gcd \set {b, d} }$
:$\lcm$ denotes lowest common multiple
:$\gcd$ denotes greatest common divisor.

Proof:
{{begin-eqn}}
{{eqn | l = \dfrac a b + \dfrac c d
      | r = \dfrac {a d} {b d} + \dfrac {b c} {b d}
      | c = 
}}
{{eqn | r = \dfrac {a d + b c} {b d}
      | c = 
}}
{{eqn | r = \dfrac {a d + b c} {\gcd \set {b, d} \lcm \set {b, d} }
      | c = Product of GCD and LCM
}}
{{eqn | r = \dfrac {a D \gcd \set {b, d} + B \gcd \set {b, d} c} {\gcd \set {b, d} \lcm \set {b, d} }
      | c = substituting for $b$ and $d$ as defined above
}}
{{eqn | r = \dfrac {a D + B c} {\lcm \set {b, d} }
      | c = dividing top and bottom by $\gcd \set {b, d}$
}}
{{end-eqn}}
{{qed}}
Theorem: GCD of Sum and Difference of Integers

:$\gcd \set {a + b, a - b} \ge \gcd \set {a, b}$

Proof:
Let $d = \gcd \set {a, b}$.
Then by definition of greatest common divisor:
:$d \divides a \land d \divides b$
From Common Divisor Divides Integer Combination:
:$d \divides \paren {a + b} \land d \divides \paren {a - b}$
By definition of common divisor:
:$d \divides \gcd \set {a + b, a - b}$
Hence from Absolute Value of Integer is not less than Divisors:
:$d \le \gcd \set{a + b, a - b}$
{{qed}}
Theorem: Greatest Common Divisor divides Lowest Common Multiple

Let $a, b \in \Z$ such that $a b \ne 0$.
Then:
:$\gcd \set {a, b} \divides \lcm \set {a, b}$
where:
:$\lcm$ denotes lowest common multiple
:$\gcd$ denotes greatest common divisor.
:$\divides$ denotes divisibility.

Proof:
We have that:
:$\gcd \set {a, b} \divides a$
and:
:$a \divides \lcm \set {a, b}$
The result follows from Divisor Relation is Transitive.
{{qed}}
Theorem: Intersection of Sets of Integer Multiples

Let $m, n \in \Z$ such that $m n \ne 0$.
Let $m \Z$ denote the set of integer multiples of $m$.
Then:
:$m \Z \cap n \Z = \lcm \set {m, n} \Z$
where $\lcm$ denotes lowest common multiple.

Proof:
Let $x \in m \Z \cap n \Z$.
Then by definition of set intersection:
:$m \divides x$ and $n \divides x$
So from LCM Divides Common Multiple:
:$\lcm \set {m, n} \divides x$
and so $x \in \lcm \set {m, n} \Z$
That is:
:$m \Z \cap n \Z \subseteq \lcm \set {m, n} \Z$
{{qed|lemma}}
Now suppose $x \in \lcm \set {m, n} \Z$.
Then $\lcm \set {m, n} \divides x$.
Thus by definition of lowest common multiple:
:$m \divides x$ 
and:
:$n \divides x$
and so:
:$x \in m \Z \land x \in n \Z$
That is:
:$x \in m \Z \cap n \Z$
and so:
:$\lcm \set {m, n} \Z \subseteq m \Z \cap n \Z$
{{qed|lemma}}
The result follows by definition of set equality.
{{qed}}
Theorem: Set of Integer Multiples of GCD

Let $m, n \in \Z$.
Let $m \Z$ denote the set of integer multiples of $m$
Then:
:$m \Z \cup n \Z \subseteq \gcd \set {m, n} \Z$
where $\gcd$ denotes greatest common divisor.

Proof:
Let $x \in m \Z \cup n \Z$.
Then either:
:$m \divides x$
or:
:$n \divides x$
In both cases:
:$\gcd \set {m, n} \divides x$
and so:
:$x \in \gcd \set {m, n} \Z$
Hence by definition of subset:
:$m \Z \cup n \Z \subseteq \gcd \set {m, n} \Z$
{{qed}}
Theorem: Join of Sets of Integer Multiples is Set of Integer Multiples of GCD

Let $m, n \in \Z$.
Let $m \Z$ denote the set of integer multiples of $m$
Let $r \in \Z$ such that:
:$m \Z \subseteq r \Z$
and:
:$n \Z \subseteq r \Z$
Then:
:$\gcd \set {m, n} \Z \subseteq r \Z$
where $\gcd$ denotes greatest common divisor.

Proof:
From Set of Integer Multiples is Integral Ideal, each of $m \Z$, $n \Z$, $r \Z$ and $\gcd \set {m, n} \Z$ are integral ideals.
Let $c \in \gcd \set {m, n} \Z$.
By definition of integral ideal:
:$\gcd \set {m, n} \divides c$
By Set of Integer Combinations equals Set of Multiples of GCD:
:$\exists x, y \in \Z: c = x m + y n$
But as $m \Z \subseteq r \Z$ and $n \Z \subseteq r \Z$:
:$m \in r \Z$ and $n \in \r Z$
Thus by definition of integral ideal:
:$x m + y n \in r \Z$
So:
:$c \in \gcd \set {m, n} \Z \implies c \in r \Z$
and the result follows by definition of subset.
{{qed}}
Theorem: GCD of Generators of General Fibonacci Sequence is Divisor of All Terms

Let $\FF = \sequence {a_n}$ be a general Fibonacci sequence generated by the parameters $r, s, t, u$:
:$a_n = \begin{cases}
r & : n = 0 \\
s & : n = 1 \\
t a_{n - 2} + u a_{n - 1} & : n > 1
\end{cases}$
Let:
:$d = \gcd \set {r, s}$
where $\gcd$ denotes greatest common divisor.
Then:
:$\forall n \in \Z_{>0}: d \divides a_n$

Proof:
From the construction of a general Fibonacci sequence, $a_n$ is an integer combination of $r$ and $s$.
From Set of Integer Combinations equals Set of Multiples of GCD, $a_n$ is divisible by $\gcd \set {r, s}$.
Hence the result.
{{qed}}
Theorem: GCD of Consecutive Integers of General Fibonacci Sequence

Let $\FF = \sequence {a_n}$ be a general Fibonacci sequence generated by the parameters $r, s, t, u$:
:$a_n = \begin{cases}
r & : n = 0 \\
s & : n = 1 \\
t a_{n - 2} + u a_{n - 1} & : n > 1
\end{cases}$
Let:
:$d = \gcd \set {r, s}$
where $\gcd$ denotes greatest common divisor.
Let $f = \gcd \set {a_m, a_{m - 1} }$ for some $m \in \N$.
Let $\gcd \set {f, t} = 1$.
Then:
:$f \divides d$

Proof:
Proof by induction:
Let $\map P m$ be the proposition:
:$\gcd \set {f_m, t} = 1 \implies f_m = d$
where $f_m = \gcd \set {a_m, a_{m - 1} }$.
For clarity, we have indexed $f$.
Theorem: Three Points in Ultrametric Space have Two Equal Distances/Corollary 3

Let $\struct {R, \norm {\,\cdot\,} }$ be a normed division ring with non-Archimedean norm $\norm{\,\cdot\,}$,
Let $x, y \in R$ and $\norm x \lt \norm y$.
Then:
:$\norm {x + y} = \norm {x - y} = \norm {y - x} = \norm y$

Proof:
By {{Corollary|Three Points in Ultrametric Space have Two Equal Distances|2}}:
:$\norm {x + y} = \norm {x - y} = \norm {y - x} = \max \set {\norm x, \norm y} = \norm y$
{{qed}}
Theorem: Three Points in Ultrametric Space have Two Equal Distances/Corollary 4

Let $\struct {R, \norm {\,\cdot\,} }$ be a normed division ring with non-Archimedean norm $\norm{\,\cdot\,}$,
Let $x, y \in R$.
Then:
{{begin-eqn}}
{{eqn | l = \norm {x + y} < \norm y
      | o = \implies
      | r = \norm x = \norm y
}}
{{eqn | l = \norm {x - y} < \norm y
      | o = \implies
      | r = \norm x = \norm y
}}
{{eqn | l = \norm {y - x} < \norm y
      | o = \implies
      | r = \norm x = \norm y
}}
{{end-eqn}}

Proof:
The contrapositive statements are proved.
Let $\norm x \ne \norm y$
By {{Corollary|Three Points in Ultrametric Space have Two Equal Distances|2}}:
:$\norm {x + y} = \norm {x - y} = \norm {y - x} = \max \set {\norm x, \norm y} \ge \norm y$
The result follows.
{{qed}}
Theorem: Equivalent Norms are both Non-Archimedean or both Archimedean

Let $R$ be a division ring with unity $1_R$.
Let $\norm {\,\cdot\,}_1$ and $\norm {\,\cdot\,}_2$ be equivalent norms on $R$.
Then $\norm {\,\cdot\,}_1$ and $\norm {\,\cdot\,}_2$ are either both non-Archimedean or both Archimedean.

Proof:
By Characterisation of Non-Archimedean Division Ring Norms then:
:$\norm {\,\cdot\,}_1$ is non-Archimedean $\iff \forall n \in \N_{>0}: \norm{n \cdot 1_R}_1 \le 1$.
By the definition of norm equivalence then:
:$\forall n \in \N: \norm {n \cdot 1_R}_1 \le 1 \iff \norm {n \cdot 1_R}_2 \le 1$
Similarly, by Characterisation of Non-Archimedean Division Ring Norms then:
:$\forall n \in \N_{>0}: \norm {n \cdot 1_R}_2 \le 1 \iff \norm {\,\cdot\,}_2$ is non-Archimedean.
The result follows.
{{qed}}
Theorem: Minimum Area of Triangle whose Vertices are Lattice Points

Let $T$ be a triangle embedded in a cartesian plane.
Let the vertices of $T$ be lattice points which are not all on the same straight line.
Then the area of $T$ is such that:
:$\map \Area T \ge \dfrac 1 2$

Proof:
{{WLOG}} let one of the vertices of $T$ be at $\tuple {0, 0}$.
Let the other $2$ vertices be at $\tuple {a, b}$ and $\tuple {x, y}$.
By Area of Triangle in Determinant Form with Vertex at Origin:
:$\map \Area T = \dfrac {\size {b y - a x} } 2$
As the vertices of $T$ are non-collinear, $\map \Area T \ge 0$.
Thus $\size {b y - a x} > 0$.
As $\tuple {a, b}$ and $\tuple {x, y}$ are lattice points, all of $a, b, x, y \in \Z$.
Thus $\size {b y - a x} \ge 1$.
Hence the result.
{{Qed}}
Theorem: Perpendicular Distance from Straight Line in Plane to Origin

Let $L$ be the straight line embedded in the cartesian plane whose equation is given as:
:$a x + b y = c$
Then the perpendicular distance $d$ between $L$ and $\tuple {0, 0}$ is given by:
:$d = \size {\dfrac c {\sqrt {a^2 + b^2} } }$

Proof:
From Perpendicular Distance from Straight Line in Plane to Point, the perpendicular distance $d$ between $L$ and the point $\tuple {x_0, y_0}$ is given by:
:$d = \dfrac {\size {a x_0 + b y_0 + c} } {\sqrt {a^2 + b^2} }$
The result follows by setting $x_0 = 0$ and $y_0 = 0$.
{{qed}}
Theorem: Line in Plane is Straight iff Slope is Constant

Let $\LL$ be a curve which can be embedded in the plane.
Then $\LL$ is a straight line {{iff}} it is of constant slope.

Proof:
Let $L$ be embedded in the cartesian plane.
The slope of $\LL$ at a point $p = \tuple {x, y}$ is defined as being its derivative at $p$ {{WRT|Differentiation}} $x$:
:$\grad p = \dfrac {\d y} {\d x}$
:500px
Let $\LL$ be a straight line.
Let $\triangle ABC$ and $\triangle DEF$ be right triangles constructed so that:
:$A, B, D, E$ are on $\LL$
:$AC$ and $DF$ are parallel to the $x$-axis
:$BC$ and $EF$ are parallel to the $y$-axis.
From Parallelism implies Equal Corresponding Angles:
:$\angle ABC = \angle DEF$
and:
:$\angle BAC = \angle EDF$
Also we have that $\angle ACB = \angle DFE$ and are right angles.
Thus $\triangle ABC$ and $\triangle DEF$ are similar.
Thus:
:$\dfrac {BC} {AC} = \dfrac {EF} {DF}$
That is, the slope of $\LL$ between $A$ and $B$ is the same as the slope of $\LL$ between $D$ and $E$.
The argument reverses.
{{Qed}}