avewright/proofwiki-math huggingface dataset:
Theorem: Polygon not Equal to Triangle has Chord

Let $P$ be a polygon that is not a triangle.
Then $P$ has a chord that lies completely in the interior of $P$.

Proof:
From Polygon has Salient Angle, it follows that $P$ has a convex internal angle.
Let $A, B, C$ be vertices of $P$ such that $\angle BAC$ is a convex internal angle of the vertex $A$.
Let $BC$ subtend the angle $\angle BAC$.
Suppose $BC$ is equal to a side of $P$.
Then $P = \triangle ABC$, which would contradict our assumption that $P$ is not a triangle.
Suppose $BC$ is a chord of $P$ that lies completely in the interior of $P$.
Then the proof is done.
Suppose $BC$ does not lie completely in the interior of $P$.
Then either a side of $P$ intersects $BC$, or a vertex of $P$ lies on $BC$.
In either case, one or more vertices of $P$ lie inside $\triangle ABC$, or on $BC$.
Let $\mathcal V$ be the set of those vertices.
Define $D$ as the vertex in $\mathcal V$ that lies furthest away from $BC$.
If more than one vertex in $\mathcal V$ have the same maximal distance from $BC$, pick $D$ among them arbitrarily.
File:FindChordInPolygon.png
Now $AD$ is a chord of $P$ that lies completely in the interior.
As any side of $P$ that would intersect $AD$ would either intersect $AB$ or $AC$, or end in a vertex that lie further away from $BC$ than $D$ does.
In all of these cases, we have a contradiction.
{{qed}}
Theorem: Reductio ad Absurdum for Hilbert Proof System Instance 1 for Predicate Logic

Let $\LL$ be the language of predicate logic.
Let $\mathscr H$ be instance 1 of a Hilbert proof system for predicate logic.
Then Reductio ad Absurdum is a derived rule of $\mathscr H$:
{{:Reductio ad Absurdum/Proof Rule}}

Proof:
{{MissingLinks|To the propositional tautologies}}
Suppose that $\Sigma, \neg \phi \vdash_{\mathscr H} \bot$.
By Contradictory Antecedent, $\bot \implies \phi$ is a tautology.
Therefore, $\bot \implies \phi$ is an axiom of $\mathscr H$, so that by Modus Ponendo Ponens:
:$\Sigma, \neg \phi \vdash_{\mathscr H} \phi$
By Deduction Theorem for Hilbert Proof System for Predicate Logic, it follows that:
:$\Sigma \vdash_{\mathscr H} \neg \phi \implies \phi$
Next, note that $\paren{ \neg \phi \implies \phi } \implies \phi$ is a tautology and so an axiom of $\mathscr H$.
Hence by Modus Ponendo Ponens:
:$\Sigma \vdash_{\mathscr H} \phi$
{{qed}}
Theorem: Proof by Contradiction for Hilbert Proof System Instance 1 for Predicate Logic

Let $\LL$ be the language of predicate logic.
Let $\mathscr H$ be instance 1 of a Hilbert proof system for predicate logic.
Then Proof by Contradiction is a derived rule of $\mathscr H$:
{{:Proof by Contradiction/Proof Rule}}

Proof:
{{MissingLinks|To the propositional tautologies}}
Suppose that $\Sigma, \phi \vdash_{\mathscr H} \bot$.
By Contradictory Antecedent, $\bot \implies \neg\phi$ is a tautology.
Therefore, $\bot \implies \neg\phi$ is an axiom of $\mathscr H$, so that by Modus Ponendo Ponens:
:$\Sigma, \phi \vdash_{\mathscr H} \neg \phi$
By Deduction Theorem for Hilbert Proof System for Predicate Logic, it follows that:
:$\Sigma \vdash_{\mathscr H} \phi \implies \neg \phi$
Next, note that $\paren {\phi \implies \neg \phi} \implies \neg \phi$ is a tautology and so an axiom of $\mathscr H$.
Hence by Modus Ponendo Ponens:
:$\Sigma \vdash_{\mathscr H} \neg \phi$
{{qed}}
Theorem: 3 is Divisor of one of n, n+2, n+4

Let $n \in \Z$ be an integer such that $n > 3$.
Then at least one of $n$, $n + 2$, $n + 4$ is divisible by $3$.

Proof:
Let $n \in \Z_{>0}$.
Then $n$ can be represented as either:
{{begin-eqn}}
{{eqn | l = n
      | r = 3 k
}}
{{eqn | l = n
      | r = 3 k + 1
}}
{{eqn | l = n
      | r = 3 k + 2
}}
{{end-eqn}}
Let $n = 3 k$.
Then $n$ is divisible by $3$.
Let $n = 3 k + 1$.
Then:
:$n + 2 = 3 k + 3 = 3 \paren {k + 1}$
which is divisible by $3$.
Let $n = 3 k + 2$.
Then:
:$n + 4 = 3 k + 6 = 3 \paren {k + 2}$
which is divisible by $3$.
Hence the result.
{{Qed}}
Theorem: Divisor of Integer/Examples/2 divides n(n+1)

Let $n$ be an integer.
Then:
:$2 \divides n \paren {n + 1}$

Proof:
Suppose $n$ is even.
Then $2 \divides n$ by definition.
Hence from Divisor Divides Multiple:
:$2 \divides n \paren {n + 1}$
{{qed|lemma}}
Suppose $n$ is odd.
Then $n + 1$ is even
Then $2 \divides n + 1$ by definition.
Hence from Divisor Divides Multiple:
:$2 \divides n \paren {n + 1}$
{{qed}}
Theorem: Divisor of Integer/Examples/3 divides n(n+1)(n+2)

Let $n$ be an integer.
Then:
:$3 \divides n \paren {n + 1} \paren {n + 2}$

Proof:
$n$ is of one of these forms:
{{begin-eqn}}
{{eqn | l = n
      | r = 3 k
}}
{{eqn | l = n
      | r = 3 k + 1
}}
{{eqn | l = n
      | r = 3 k + 2
}}
{{end-eqn}}
for some $k \in \Z$.
Suppose $n = 3 k$.
Then $3 \divides n$ by definition.
Suppose $n = 3 k + 1$.
Then:
:$n + 2 = 3 k + 3 = 3 \paren {k + 1}$
Thus:
:$3 \divides n + 2$.
Suppose $n = 3 k + 2$.
Then:
:$n + 1 = 3 k + 3 = 3 \paren {k + 1}$
Thus:
:$3 \divides n + 1$.
Hence from Divisor Divides Multiple:
:$3 \divides n \paren {n + 1} \paren {n + 2}$
{{qed}}
Theorem: Divisor of Integer/Examples/7 divides 2^3n - 1

Let $n$ be an integer such that $n \ge 1$.
Then:
:$7 \divides 2^{3 n} - 1$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:$7 \divides 2^{3 n} - 1$
Theorem: Divisor of Integer/Examples/8 divides 3^2n + 7

Let $n$ be an integer such that $n \ge 1$.
Then:
:$8 \divides 3^{2 n} + 7$

Proof:
From Integer Less One divides Power Less One, we have that:
:$\forall m, n \in \Z: \paren {m - 1} \divides \paren {m^n - 1}$
Hence we have the special case where $m = 3^2$:
:$8 \divides 3^{2 n} - 1$
from which it follows immediately that:
:$8 \divides 3^{2 n} - 1 + 8 = 3^{2 n} + 7$
{{qed}}
Theorem: Divisor of Integer/Examples/3 divides 2^n + (-1)^(n+1)

Let $n$ be an integer such that $n \ge 1$.
Then:
:$3 \divides 2^n + \paren {-1}^{n + 1}$

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 1}$, let $\map P n$ be the proposition:
:$3 \divides 2^n + \paren {-1}^{n + 1}$
Theorem: Chinese Remainder Theorem (Groups)

Let $G$ be a group.
Let $N_1, \ldots, N_n$ for some $n \ge 1$ be normal subgroups of $G$.
Let $\pi_i: G \rightarrow G / N_i$ be the canonical projections.
Then the homomorphism $\pi: G \to G / N_1 \times \cdots \times G / N_n$ defined as:
:$\map \pi x = \tuple {\map {\pi_1} x, \ldots, \map {\pi_n} x}$
has the kernel $\ds N := \bigcap_{i \mathop = 1}^n N_i$.
Further, $\pi$ is surjective {{iff}} the normal subgroups have the following property:
:$\ds \forall k \le n - 1: N_{k + 1} \bigcap_{i \mathop = 1}^k N_i = G$

Proof:
By Quotient Group Epimorphism is Epimorphism, each canonical projection $\pi_i: G \to G / N_i$ is a group homomorphism.
Hence the mapping $\pi$ is indeed a group homomorphism.
The kernel of $\pi$ is given by:
:$\ds \ker \pi = \set {x \in G: \forall i, 1 \le i \le n: \map {\pi_i} x = \map {\pi_i} e} = \set {x \in G: \forall i, 1 \le i \le n: x \in N_i} = \bigcap_{1 \mathop \le i \mathop \le n} N_i =: N$
We will now establish the necessity and sufficiency of the condition for surjectivity of $\pi$.
Indeed, we will demonstrate that if $\pi$ is surjective, then:
:$\ds \forall k: N_k \bigcap_{j \mathop \ne k} N_j = G$
which will complete the proof together with a deduction of surjectivity from the condition that:
:$\ds \forall k \le n - 1: N_{k + 1} \bigcap_{i \mathop = 1}^k N_i = G$
Theorem: Square Modulo 24 of Odd Integer Not Divisible by 3

Let $a \in \Z$ be an integer such that:
:$2 \nmid a$
:$3 \nmid a$
where $\nmid$ denotes non-divisibility.
Then:
:$a^2 \equiv 1 \pmod {24}$
That is:
:$24 \divides \paren {a^2 - 1}$
where $\divides$ denotes divisibility.

Proof:
Let $a$ be as asserted.
We have that:
:$2 \nmid a$
From Odd Square Modulo 8:
:$a^2 \equiv 1 \pmod 8$
which means:
:$8 \divides a^2 - 1$
We also have that:
:$3 \nmid a$
From Square Modulo 3: Corollary 3:
:$3 \divides a^2 - 1$
We have from Coprime Integers: $3$ and $8$ that:
:$3 \perp 8$
where $\perp$ denotes coprimality.
As we have that:
:$8 \divides a^2 - 1$
and:
:$3 \divides a^2 - 1$
it follows from Product of Coprime Factors that:
:$24 \divides a^2 - 1$
Hence the result.
{{qed}}
Theorem: Sum of Squares of Two Odd Integers is not Square

Let $m$ and $n$ be odd integers.
Then $m^2 + n^2$ is not a square number.

Proof:
{{AimForCont}} $m^2 + n^2$ is a square number.
Because $m$ and $n$ are both  odd, we have:
{{begin-eqn}}
{{eqn | l = m^2
      | o = \equiv
      | r = 1
      | rr= \pmod 4
      | c = Square Modulo 4
}}
{{eqn | l = n^2
      | o = \equiv
      | r = 1
      | rr= \pmod 4
      | c = Square Modulo 4
}}
{{eqn | ll= \leadsto
      | l = m^2 + n^2
      | o = \equiv
      | r = 2
      | rr= \pmod 4
      | c = 
}}
{{end-eqn}}
From Parity of Integer equals Parity of its Square, $m^2$ and $n^2$ are both odd integers.
Hence $m^2 + n^2$ is an even integer.
But from Square Modulo 4, $m^2 + n^2$ is even {{iff}} $x^2 \equiv 0 \pmod 4$.
This contradicts the deduction that $m^2 + n^2 \equiv 2 \pmod 4$.
Hence by Proof by Contradiction it follows that $m^2 + n^2$ cannot be square.
{{qed}}
Theorem: Polygon Triangulation Theorem

Let $P$ be a polygon with $n$ sides, where $n \in \N_{ \ge 3 }$.
Then there exists a triangulation of $P$ that fulfills this condition:
* If $AB$ is a side of a triangle in the triangulation of $P$, then $AB$ is either a side of $P$, or a chord of $P$ that lies completely in the interior of $P$.
All triangulations of $P$ that fulfill this condition consist of exactly $n-2$ triangles.

Proof:
We show existence by using strong induction over $n$, the number of sides of $P$.
Theorem: Product of Consecutive Integers is Even

Let $a$ and $b$ be consecutive integers.
Then $a b$ is even.

Proof:
{{WLOG}} let $a < b$.
Then $b$ can be expressed as $a + 1$.
Hence:
{{begin-eqn}}
{{eqn | l = a b
      | r = a \paren {a + 1}
      | c = 
}}
{{eqn | r = a^2 + a
      | c = 
}}
{{end-eqn}}
From Parity of Integer equals Parity of its Square, $a$ and $a^2$ are either both even or both odd.
The result follows from:
:Sum of Even Integers is Even
and:
:Sum of Even Number of Odd Numbers is Even
{{qed}}
Category:Even Integers
gowmy1mgo46c723wb6rgjn11rnxg5wx
Theorem: GCD with Self

Let $a \in \Z$ be an integer such that $a \ne 0$.
Then:
:$\gcd \set {a, a} = \size a$
where $\gcd$ denotes greatest common divisor (GCD).

Proof:
From Integer Divides its Absolute Value:
:$\size a \divides a$
Then from Absolute Value of Integer is not less than Divisors:
:$\forall x \in \Z: x \divides a \implies x \le \size a$
The result follows by definition of GCD.
{{qed}}
Theorem: GCD of Integer with Integer + n

Let $a \in \Z$ be an integer.
Let $n \in \Z_{\ge 0}$ be a positive integer.
Then:
:$\gcd \set {a, a + n} \divides n$
where:
:$\gcd$ denotes the greatest common divisor
:$\divides$ denotes divisibility.

Proof:
Let $g = \gcd \set {a, a + n}$.
By definition of $\gcd$, there exist $b, b' \in \Z$ such that:
:$a = g b$
:$a + n = g b'$
Therefore:
{{begin-eqn}}
{{eqn | l = n
      | r = \paren{ a + n } - a
}}
{{eqn | r = g b' - g b
}}
{{eqn | r = g \paren{ b' - b }
}}
{{end-eqn}}
Since $b' - b \in \Z$, it follows by definition of divisibility that:
:$g \divides n$
as desired.
{{qed}}
Theorem: Two Ears Theorem

Let $P$ be a polygon that is not a triangle.
Then $P$ has at least two ears that do not overlap each other.

Proof:
Let $P$ have $n$ sides, where $n \in \N_{ \ge 3 }$.
Polygon Triangulation Theorem shows that there exists a triangulation $\family { \triangle_i }_{i \mathop = 1}^{n-2}$ of $P$, and the sides of each triangle $\triangle_i$ are either sides of $P$ or chords of $P$.
Suppose $\triangle_i$ has $0$ or $1$ sides in common with $P$.
In this case, $\triangle_i$ cannot be an ear of $P$.
Suppose $\triangle_i$ has $2$ sides in common with $P$.
In this case, $\triangle_i$ is an ear of $P$.
Suppose $\triangle_i$ has $3$ sides in common with $P$.
In this case, we have $\triangle_i = P$, which would contradict our assumption that $P$ is not a triangle.
Now, suppose that at most one of the triangles $\family { \triangle_i }_{i \mathop = 1}^{n-2}$ is an ear.
The maximal number of sides that the $n-2$ triangles could have in common with $P$ is:
:$2 + 1 \paren { n-2-1} = n-1$
As the triangulation covers all $n$ sides of $P$, this is a contradiction.
It follows that at least two of the triangles $\family { \triangle_i }_{i \mathop = 1}^{n-2}$ are ears.
As the two ears are part of a triangulation, they do not overlap.
{{qed}}
Theorem: Intersection of Ideals of Ring contains Product

Let $R$ be a ring.
Let $I$ be a right ideal of $R$.
Let $J$ be a left ideal of $R$.
Let $I J$ be their product.
Then $I J \subseteq I \cap J$.

Proof:
Let $a_1, \ldots, a_n \in I$ and $b_1, \ldots, b_n \in J$ be arbitrary.
Then:
{{begin-eqn}}
{{eqn | q = \forall k \in \set {1, \ldots, n}
      | l = a_k b_k
      | o = \in
      | r = I
      | c = {{Defof|Right Ideal of Ring}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^n a_k b_k
      | o = \in
      | r = I
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | q = \forall k \in \set {1, \ldots, n}
      | l = a_k b_k
      | o = \in
      | r = J
      | c = {{Defof|Left Ideal of Ring}}
}}
{{eqn | ll= \leadsto
      | l = \sum_{k \mathop = 1}^n a_k b_k
      | o = \in
      | r = J
}}
{{end-eqn}}
By definition of set intersection:
:$\ds \sum_{k \mathop = 1}^n a_k b_k \in I \cap J$
As $a_1, \ldots, a_n$ and $b_1, \ldots, b_n$ were arbitrary, this completes the proof.
{{qed}}
Category:Ideal Theory
d4fszo5nbp2631qungzltvhul0pes0n
Theorem: Universal Instantiation/Proof System

Let $\map {\mathbf A} x$ be a WFF of predicate logic.
Let $\tau$ be a term which is freely substitutable for $x$ in $\mathbf A$.
Let $\mathscr H$ be Hilbert proof system instance 1 for predicate logic.
Then:
:$\forall x: \map {\mathbf A} x \vdash_{\mathscr H} \map {\mathbf A} \tau$
is a provable consequence in $\mathscr H$.

Proof:
{{WIP}}
Theorem: Universal Generalisation/Informal Statement

Let $\mathbf a$ be any arbitrarily selected object in the universe of discourse.
Then:
{{begin-eqn}}
{{eqn | l = \map P {\mathbf a}
      | o =
}}
{{eqn | ll= \vdash
      | q = \forall x
      | l = \map P x
      | o =
}}
{{end-eqn}}
In natural language:
:''Suppose $P$ is true of any arbitrarily selected $\mathbf a$'' in the universe of discourse.''
:''Then $P$ is true of everything in the universe of discourse.''

Proof:
We can express $\forall x$ using its propositional expansion:
:$\map P {\mathbf X_1} \land \map P {\mathbf X_2} \land \map P {\mathbf X_3} \land \ldots$
where $\mathbf X_1, \mathbf X_2, \mathbf X_3 \ldots{}$ is the complete set of the objects in the universe of discourse.
The fact that any object we care to choose has the property in question means that they ''all'' must have this property.
The result then follows by generalizing the Rule of Conjunction.
{{qed}}
{{questionable|This only works for a countable universe of discourse. Use $\ds \bigwedge_{\alpha \mathop \in I} P_\alpha$. The page propositional expansion is suspect.}}
Theorem: Universal Generalisation/Proof System

Let $\LL$ be a specific signature for the language of predicate logic.
Let $\mathscr H$ be Hilbert proof system instance 1 for predicate logic.
Let $\map {\mathbf A} x$ be a WFF of $\LL$.
Let $\FF$ be a collection of WFFs of $\LL$.
Let $c$ be an arbitrary constant symbol which is not in $\LL$.
Let $\LL'$ be the signature $\LL$ extended with the constant symbol $c$.
Suppose that we have the provable consequence (in $\LL'$):
:$\FF \vdash_{\mathscr H} \map {\mathbf A} c$
Then we may infer (in $\LL$):
:$\FF \vdash_{\mathscr H} \forall x: \map {\mathbf A} x$

Proof:
{{WIP}}
Theorem: Existential Instantiation/Informal Statement

:$\exists x: \map P x, \map P {\mathbf a} \implies y \vdash y$
Suppose we have the following:
:From our universe of discourse, ''any'' arbitrarily selected object $\mathbf a$ which has the property $P$ implies a conclusion $y$
:$\mathbf a$ is not free in $y$
:It is known that there ''does'' actually exists an object that has $P$.
Then we may infer $y$.
This is called the '''Rule of Existential Instantiation''' and often appears in a proof with its abbreviation $\text {EI}$.
When using this rule of existential instantiation:
:$\exists x: \map P x, \map P {\mathbf a} \implies y \vdash y$
the instance of $\map P {\mathbf a}$ is referred to as the '''typical disjunct'''.

Proof:
This is an extension of Proof by Cases.
The propositional expansion of $\exists x: \map P x$ is:
:$\map P {\mathbf X_1} \lor \map P {\mathbf X_2} \lor \map P {\mathbf X_3} \lor \ldots$
We know that any arbitrarily selected $\mathbf a$ with the property $P$ implies $y$.
From this we can infer that ''all'' such $\mathbf a$ which have that property imply $y$.
This is equivalent to the step in Proof by Cases in which we need to prove that both disjuncts lead to the same conclusion.
The fact that we only need one of them in fact to ''be'' true is quite enough to draw the conclusion that $y$ is true.
In this context, we are assured by the statement $\exists x: \map P x$ that at least one such disjunct in the above propositional expansion is true.
Thus the conclusion follows, and the result is proved.
{{qed}}
Theorem: Existential Instantiation/Proof System

Let $\LL$ be a specific signature for the language of predicate logic.
Let $\mathscr H$ be Hilbert proof system instance 1 for predicate logic.
Let $\map {\mathbf A} x, \mathbf B$ be WFFs of $\LL$.
Let $\FF$ be a collection of WFFs of $\LL$.
Let $c$ be an arbitrary constant symbol which is not in $\LL$.
Let $\LL'$ be the signature $\LL$ extended with the constant symbol $c$.
Suppose that we have the provable consequence (in $\LL'$):
:$\FF, \map {\mathbf A} c \vdash_{\mathscr H} \mathbf B$
Then we may infer (in $\LL$):
:$\FF, \exists x: \map {\mathbf A} x \vdash_{\mathscr H} \mathbf B$

Proof:
{{WIP}}
Theorem: Components of Separation are Separated Sets

Let $T = \struct {S, \tau}$ be a topological space.
Let $A \mid B$ be a separation of $T$.
Then $A$ and $B$ are separated sets of $T$.

Proof:
By definition of closure, $A^-$ is the smallest closed set of $T$ that contains $A$.
Components of Separation are Clopen shows that $A$ and $B$ are closed.
It follows that $A^- = A$, and $B^- = B$.
Definition of separation shows that $A \cap B = \O$, so we have:
{{begin-eqn}}
{{eqn | l = A^- \cap B
      | r = A \cap B
      | rr= = \O
}}
{{eqn | l = A \cap B^-
      | r = A \cap B
      | rr= = \O
}}
{{end-eqn}}
Hence the result by definition of separated sets.
{{qed}}
Category:Separated Sets
Category:Separations
sk0ef1xio5k3mqnzwi0ms15rfbrl7t4
Theorem: Integer Combination of Coprime Integers/Sufficient Condition

Let $a, b \in \Z$ be integers, not both zero.
Let $a$ and $b$ be coprime to each other.
Then there exists an integer combination of them equal to $1$:
:$\forall a, b \in \Z: a \perp b \implies \exists m, n \in \Z: m a + n b = 1$

Proof:
{{begin-eqn}}
{{eqn | l = a
      | o = \perp
      | r = b
}}
{{eqn | ll= \leadsto
      | l = \gcd \set {a, b}
      | r = 1
      | c = {{Defof|Coprime Integers}}
}}
{{eqn | ll= \leadsto
      | q = \exists m, n \in \Z
      | l = m a + n b
      | r = 1
      | c = Bézout's Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Integer Combination of Coprime Integers/Sufficient Condition

Let $a, b \in \Z$ be integers, not both zero.
Let $a$ and $b$ be coprime to each other.
Then there exists an integer combination of them equal to $1$:
:$\forall a, b \in \Z: a \perp b \implies \exists m, n \in \Z: m a + n b = 1$

Proof:
Let $a \perp b$.
Thus they are not both $0$.
Let $S$ be defined as:
:$S = \set {a m + b n: m, n \in \Z}$
$S$ contains at least one strictly positive integer, because for example $a^2 + b^2 \in S$.
By Set of Integers Bounded Below has Smallest Element, let $d$ be the smallest element of $S$ which is strictly positive.
Let $d = a x + b y$.
It remains to be shown that $d = 1$.
By the Division Theorem:
:$a = d q + r$ where $0 \le r < d$
Then:
{{begin-eqn}}
{{eqn | l = r
      | r = a - d q
      | c = 
}}
{{eqn | r = a - \paren {a x + b y} q
      | c = 
}}
{{eqn | r = a \paren {1 - x q} + b \paren {- y q}
      | c = 
}}
{{eqn | o = \in
      | r = S
      | c = 
}}
{{end-eqn}}
But we have that $0 \le r < d$.
We have defined $d$ as the smallest element of $S$ which is strictly positive
Hence it follows that $r$ cannot therefore be strictly positive itself.
Hence $r = 0$ and so $a = d q$.
That is:
:$d \divides a$
By a similar argument:
:$d \divides b$
and so $d$ is a common divisor of both $a$ and $b$.
But the GCD of $a$ and $b$ is $1$.
Thus it follows that, as $d \in S$:
:$\exists m, n \in \Z: m a + n b = 1$
{{qed}}
Theorem: Integer Combination of Coprime Integers/Sufficient Condition

Let $a, b \in \Z$ be integers, not both zero.
Let $a$ and $b$ be coprime to each other.
Then there exists an integer combination of them equal to $1$:
:$\forall a, b \in \Z: a \perp b \implies \exists m, n \in \Z: m a + n b = 1$

Proof:
Let $a \perp b$.
Thus they are not both $0$.
Let $S$ be defined as:
:$S = \set {\lambda a + \mu b: \lambda, \mu \in \Z}$
$S$ contains at least one strictly positive integer, because for example:
:$a \in S$ (setting $\lambda = 1$ and $\mu = 0$)
:$b \in S$ (setting $\lambda = 0$ and $\mu = 1$)
By Set of Integers Bounded Below has Smallest Element, let $d$ be the smallest element of $S$ which is strictly positive.
Let $d = \alpha a + \beta b$.
Let $c \in S$, such that $\lambda_0 a + \mu_0 b = c$ for some $\lambda_0, \mu_0 \in \Z$.
By the Division Algorithm:
:$\exists \gamma, \delta \in \Z: c = \gamma d + \delta$
where $0 \le \delta < d$
Then:
{{begin-eqn}}
{{eqn | l = \delta
      | r = c - \gamma d
      | c = 
}}
{{eqn | r = \paren {\lambda_0 a + \mu_0 b} - \gamma \paren {\alpha a + \beta b}
      | c = 
}}
{{eqn | r = \paren {\lambda_0 - \gamma \alpha} a + \paren {\mu_0 - \gamma \beta} b
      | c = 
}}
{{eqn | o = \in
      | r = S
      | c = 
}}
{{end-eqn}}
But we have that $0 \le \delta < d$.
We have defined $d$ as the smallest element of $S$ which is strictly positive
Hence it follows that $\delta$ cannot therefore be strictly positive itself.
Hence $\delta = 0$ and so $c = \gamma d$.
That is:
:$d \divides c$
and so the smallest element of $S$ which is strictly positive is a divisor of both $a$ and $b$.
But $a$ and $b$ are coprime.
Thus it follows that, as $d \divides 1$:
:$d = 1$
and so, by definition of $S$:
:$\exists m, n \in \Z: m a + n b = 1$
{{qed}}
Theorem: Integer Combination of Coprime Integers/Necessary Condition

Let $a, b \in \Z$ be integers, not both zero.
Let $a$ and $b$ be such that there exists an integer combination of them equal to $1$.
Then $a$ and $b$ are coprime:
:$\forall a, b \in \Z: \exists m, n \in \Z: m a + n b = 1 \implies a \perp b$
In such an integer combination $m a + n b = 1$, the integers $m$ and $n$ are also coprime.

Proof:
{{begin-eqn}}
{{eqn | q = \exists m, n \in \Z
      | l = m a + n b
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \gcd \set {a, b}
      | o = \divides
      | r = 1
      | c = Set of Integer Combinations equals Set of Multiples of GCD
}}
{{eqn | ll= \leadsto
      | l = \gcd \set {a, b}
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \perp
      | r = b
      | c = {{Defof|Coprime Integers}}
}}
{{end-eqn}}
{{qed}}
Theorem: Integer Combination of Coprime Integers/Necessary Condition

Let $a, b \in \Z$ be integers, not both zero.
Let $a$ and $b$ be such that there exists an integer combination of them equal to $1$.
Then $a$ and $b$ are coprime:
:$\forall a, b \in \Z: \exists m, n \in \Z: m a + n b = 1 \implies a \perp b$
In such an integer combination $m a + n b = 1$, the integers $m$ and $n$ are also coprime.

Proof:
Let $a, b \in \Z$ be such that $\exists m, n \in \Z: m a + n b = 1$.
Let $d$ be a divisor of both $a$ and $b$.
Then:
:$d \divides m a + n b$
and so:
:$d \divides 1$
Thus:
:$d = \pm 1$
and so:
:$\gcd \set {a, b} = 1$
Thus, by definition, $a$ and $b$ are coprime.
{{qed}}