avewright/proofwiki-math huggingface dataset:
Theorem: Connected Subspace lies in One Component of Separation

Let $T = \struct {S, \tau}$ be a topological space.
Let $A_1 \mid A_2$ be a separation of $T$.
Let $X$ be a connected set of $T$.
Then there exist $i, j \in \set {1, 2}$ with $i \ne j$ such that $X \subseteq A_i$, and $X \cap A_j = \O$.

Proof:
By definition of separation, $A_1$ and $A_2$ are disjoint.
Define $B_i = X \cap A_i$ for $i \in \set {1, 2}$.
From Intersection is Subset, $B_i \subseteq A_i$ for $i \in \set {1, 2}$.
From Subsets of Disjoint Sets are Disjoint, $B_1$ and $B_2$ are disjoint.
The union of $B_1$ and $B_2$ is:
{{begin-eqn}}
{{eqn | l = B_1 \cup B_2
      | r = \paren {X \cap A_1} \cup \paren {X \cap A_2}
      | c =
}}
{{eqn | r = X \cap \paren {A_1 \cup A_2}
      | c = Intersection Distributes over Union
}}
{{eqn | r = X \cap S
      | c = {{Defof|Separation (Topology)}}
}}
{{eqn | r = X
      | c = Intersection with Subset is Subset
}}
{{end-eqn}}
By definition of separation, $A_1$ and $A_2$ are open in $T$.
Let $S_X = \struct {X, \tau_X}$ be the topological subspace of $T$.
Then $B_1$ and $B_2$ are open in $S_X$.
If both $B_1$ and $B_2$ are non-empty, they would form a separation of $S_X$, which contradicts the assumption that $X$ is connected.
Hence either $B_1 = \O$, or $B_2 = \O$.
{{qed}}
Theorem: Supremum Operator Norm Need not be Attained

Let $\Bbb K \in \set {\R, \C}$.
Let $\sequence {\lambda_n}_{n \mathop \in \N}$ be a bounded sequence in $\Bbb K$ such that:
:$\ds \forall n \in \N_{> 0} : \lambda_n = 1 - \frac 1 n$.
Let $\struct {\ell^2, \norm {\, \cdot \,}_2}$ be the normed $2$-sequence space.
Let $\mathbf x = \tuple {a_1, a_2, a_3, \ldots} \in \ell^2$.
Suppose $\Lambda : \ell^2 \to \ell^2$ is a diagonal operator such that:
:$\Lambda \tuple {a_1, a_2, a_3, \ldots} = \tuple {\lambda_1 a_1, \lambda_2 a_2, \lambda_3 a_3, \ldots}$
Then there is no $\mathbf x \in \ell^2$ such that:
:$\norm {\mathbf x}_2 \le 1$
and:
:$\norm {\Lambda \mathbf x}_2 = \norm \Lambda$

Proof:
Suppose $\ds \lambda_n = 1 - \frac 1 n$ with $n \in \N_{> 0}$.
By Supremum Operator Norm of Diagonal Operator over 2-Sequence Space:
{{begin-eqn}}
{{eqn | l = \norm \Lambda 
      | r = \sup_{n \mathop \in \N_{>0} } \set {1 - \frac 1 n} 
}}
{{eqn | r = 1
}}
{{end-eqn}}
Suppose:
:$\mathbf x = \tuple {a_n}_{n \mathop \in \N_{> 0} } \in \ell^2$ 
such that $\norm {\mathbf x}_2 \le 1$ and $\norm {\Lambda \mathbf x}_2 = 1$.
Suppose $0 = a_2 = a_3 = \ldots$.
Then 
{{begin-eqn}}
{{eqn | l = \Lambda \mathbf x 
      | r = \tuple {0 \cdot a_1, \frac 1 2 \cdot 0, \frac 2 3 \cdot 0 \ldots}
}}
{{eqn | r = \mathbf 0
}}
{{end-eqn}}
Also $\norm {\Lambda \mathbf x}_2 = 0$.
This is in contradiction with the assumption $\norm {\Lambda \mathbf x}_2 = 1$.
Hence, at least one of the terms $a_2, a_3, \ldots$ must be nonzero.
However:
{{begin-eqn}}
{{eqn | l = 1
      | o = \ge
      | r = \norm {\mathbf x}_2^2
}}
{{eqn | r = \size {a_1}^2 + \size {a_2}^2 + \size {a_3}^3 + \ldots
}}
{{eqn | o = \ge
      | r = \size {a_2}^2 + \size {a_3}^3 + \ldots
}}
{{eqn | o = >
      | r = \frac 1 4 \size {a_2}^2 + \frac 4 9 \size {a_3}^3 + \ldots
}}
{{eqn | r = \norm {\Lambda \mathbf x}_2^2
}}
{{eqn | r = 1
}}
{{eqn | ll = \leadsto
      | l = 1
      | o = >
      | r = 1
}}
{{end-eqn}}
This is a contradiction.
Hence, there exists no nonzero $\mathbf x \in \ell^2$ such that $\norm {\mathbf x}_2 \le 1$ and $\norm {\Lambda \mathbf x}_2 = \norm \Lambda$.
{{qed}}
Theorem: Coefficients in Linear Combination forming GCD are Coprime

Let $a$ and $b$ be integers.
Let there exist integers $x$ and $y$ such that:
:$a x + b y = \gcd \set {a, b}$
where $\gcd \set {a, b}$ denotes the greatest common divisor of $a$ and $b$.
Then:
:$x \perp y$
where $\perp$ denotes coprimality.

Proof:
Let $d = \gcd \set {a, b}$.
As $d$ is a divisor of both $a$ and $b$, both $\dfrac a d$ and $\dfrac b d$ are integers.
Hence, dividing through by $d$, we have:
:$\dfrac a d x + \dfrac b d y = \dfrac {\gcd \set {a, b} } d = 1$
Thus there exist integers $m = \dfrac a d$ and $n = \dfrac b d$ such that:
:$m x + n y = 1$
Hence from Integer Combination of Coprime Integers:
:$x \perp y$
{{qed}}
Theorem: Product of 3 Consecutive Integers is Divisible by 6

Let $a, b, c \in \Z$ be consecutive integers.
Then their product $a b c$ is divisible by $6$.

Proof:
This is an application of Divisibility of Product of Consecutive Integers with $n = 3$.
By the theorem, the product of $3$ consecutive integers is divisible by $3! = 6$.
{{qed}}
Theorem: Product of 4 Consecutive Integers is Divisible by 24

Let $a, b, c, d \in \Z$ be consecutive integers.
Then their product $a b c d$ is divisible by $24$.

Proof:
This is an application of Divisibility of Product of Consecutive Integers with $n = 4$.
By the theorem, the product of $4$ consecutive integers is divisible by $4! = 24$.
{{qed}}
Theorem: Product of 5 Consecutive Integers is Divisible by 120

Let $a, b, c, d, e \in Z$ be consecutive integers
Then their product $a b c d e$ is divisible by $120$.

Proof:
This is an application of Divisibility of Product of Consecutive Integers with $n = 5$.
By the theorem, the product of $5$ consecutive integers is divisible by $5! = 120$.
{{qed}}
Theorem: 24 divides a(a^2 - 1) when a is Odd

Let $a \in \Z$ be an odd integer.
Then:
:$24 \divides a \paren {a^2 - 1}$
where $\divides$ denotes divisibility.

Proof:
First suppose that $a$ is not divisible by $3$.
Then from Square Modulo 24 of Odd Integer Not Divisible by 3:
:$24 \divides \paren {a^2 - 1}$
from which the result follows immediately.
{{qed|lemma}}
Now suppose that $3 \divides a$.
Then immediately:
:$3 \divides a \paren {a^2 - 1}$
From Odd Square Modulo 8:
:$8 \divides \paren {a^2 - 1}$
and so:
:$8 \divides a \paren {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 \paren {a^2 - 1}$
and:
:$3 \divides a \paren {a^2 - 1}$
it follows from Product of Coprime Factors that:
:$24 \divides a \paren {a^2 - 1}$
{{qed}}
Theorem: 24 divides Square of Odd Integer Not Divisible by 3 plus 23

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

Proof:
Let $a$ be as defined.
Then:
{{begin-eqn}}
{{eqn | q = 
      | l = 24
      | o = \divides
      | r = \paren {a^2 - 1}
      | c = Square Modulo 24 of Odd Integer Not Divisible by 3
}}
{{eqn | ll= \leadsto
      | l = 24
      | o = \divides
      | r = \paren {a^2 - 1 + 24}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 24
      | o = \divides
      | r = \paren {a^2 + 23}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 24 divides Square of Odd Integer Not Divisible by 3 plus 23

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

Proof:
Let $a$ be as defined.
We have that $a$ is of the form:
:$a = 6 k + 1$
or:
:$a = 6 k + 5$
Hence:
{{begin-eqn}}
{{eqn | l = a^2 + 23
      | r = \paren {6 k + 1}^2 + 23
      | c = 
}}
{{eqn | r = 36 k^2 + 12 k + 24
      | c = 
}}
{{eqn | r = 24 \paren {\dfrac {k \paren {3 k + 1} } 2 + 1}
      | c = 
}}
{{end-eqn}}
or:
{{begin-eqn}}
{{eqn | l = a^2 + 23
      | r = \paren {6 k + 5}^2 + 23
      | c = 
}}
{{eqn | r = 36 k^2 + 60 k + 48
      | c = 
}}
{{eqn | r = 24 \paren {\dfrac {k \paren {3 k + 5} } 2 + 2}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: 360 divides a^2 (a^2 - 1) (a^2 - 4)

Let $a \in \Z$ be an integer.
Then:
:$360 \divides a^2 \paren {a^2 - 1} \paren {a^2 - 4}$
where $\divides$ denotes divisibility.

Proof:
By Difference of Two Squares:
:$a^2 \paren {a^2 - 1} \paren {a^2 - 4} = a \paren {a - 2} \paren {a - 1} a \paren {a + 1} \paren {a + 2}$
We have that $a - 2, a - 1, a, a + 1, a + 2$ are $5$ consecutive integers.
Hence from Product of 5 Consecutive Integers is Divisible by 120:
:$120 \divides a \paren {a^2 - 1} \paren {a^2 - 4}$
and so:
:$120 \divides a^2 \paren {a^2 - 1} \paren {a^2 - 4}$
As $120 = 2^3 \cdot 3 \cdot 5$, it suffices to show that
:$9 \divides a^2 \paren {a^2 - 1} \paren {a^2 - 4}$
Consider the following 3 cases.
If $a \in 3 \Z$, then $9 \divides a^2$.
If $a \in 3 \Z + 1$, then $a-1, a+2 \in 3 \Z$, so that $9 \divides \paren {a-1} \paren {a+2}$.
If $a \in 3 \Z + 2$, then $a-2, a+1 \in 3 \Z$, so that $9 \divides \paren {a-2} \paren {a+1}$.
{{qed}}
Theorem: GCD equals GCD with Product of Coprime Factor

Let $a, b, c \in \Z$ be integers.
Let:
:$a \perp b$
where $\perp$ denotes coprimality.
Then:
:$\gcd \set {a c, b} = \gcd \set {c, b}$
where $\gcd$ denotes greatest common divisor.

Proof:
Let $a, b, c \in \Z$ such that $a$ is coprime to $b$.
Let $d = \gcd \set {c, b}$.
We have:
{{begin-eqn}}
{{eqn | l = a
      | o = \perp
      | r = b
      | c = 
}}
{{eqn | n = 1
      | ll= \leadsto
      | q = \exists x, y \in \Z
      | l = 1
      | r = a x + b y
      | c = Integer Combination of Coprime Integers
}}
{{eqn | q = \exists u, v \in \Z
      | l = d
      | r = c u + b v
      | c = Bézout's Identity
}}
{{eqn | ll= \leadsto
      | l = d
      | r = \paren {a x + b y} \paren {c u + b v}
      | c = from $(1)$
}}
{{eqn | r = a c u x + a b v x + b c u y + b^2 v x
      | c = multiplying out
}}
{{eqn | r = a c \paren {u x} + b \paren {a v x + c u y + b v x}
      | c = rearranging
}}
{{eqn | r = \gcd \set {a c, b}
      | c = Bézout's Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Existence of Chebyshev Polynomials of the First Kind

There exists a Chebyshev polynomial of the first kind for each natural number $n$.

Proof:
For $n = 0$:
{{begin-eqn}}
{{eqn | l = \map \cos {0 \theta}
      | r = \map \cos 0
}}
{{eqn | r = 1
}}
{{end-eqn}}
:$\map {T_0} x = 1$, $T_0 \in \Bbb P$
{{MissingLinks|$\Bbb P$ as the set/space of polynomials}}
For $n = 1$:
{{begin-eqn}}
{{eqn | l = \map \cos {1 \theta}
      | r = \map \cos \theta
}}
{{end-eqn}}
:$\map {T_1} x = x$, $T_1 \in \Bbb P$
Assume $\map {T_n} {\cos \theta} = \map \cos {n \theta}$.
{{begin-eqn}}
{{eqn | l = \map {T_{n + 1} } {\cos \theta}
      | r = \map \cos {\paren {n + 1} \theta}
}}
{{eqn | r = \map \cos {n \theta + \theta}
}}
{{eqn | r = \map \cos {n \theta} \map \cos \theta - \map \sin {n \theta}  \map \sin \theta
      | c = Cosine of Sum
}}
{{eqn | r = 2 \map \cos {n \theta} \map \cos \theta - \map \cos {n \theta} \map \cos \theta - \map \sin {n \theta}  \map \sin \theta
}}
{{eqn | r = 2 \map \cos {n \theta} \map \cos \theta - \paren {\map \cos {n \theta} \map \cos \theta + \map \sin {n \theta}  \map \sin \theta}
}}
{{eqn | r = 2 \map \cos {n \theta} \map \cos \theta - \map \cos {n \theta - \theta}
      | c = Cosine of Difference
}}
{{eqn | r = 2 \map \cos \theta \map \cos {n \theta} - \map \cos {\paren {n - 1} \theta}
}}
{{eqn | r = 2 \map \cos \theta \map {T_n} {\cos \theta} - \map {T_{n - 1} } {\cos \theta}
      | c = {{hypothesis}}
}}
{{end-eqn}}
:$\map {T_{n + 1} } x = 2 x \map {T_n} x - \map {T_{n - 1} } x$, $T_{n + 1} \in \Bbb P$
By the Second Principle of Mathematical Induction, $T_n \in \Bbb P$ for all natural numbers $n$.
{{qed}}
Category:Chebyshev Polynomials of the First Kind
i2ir927m1w9dd6bngi174waxmoq8xzk
Theorem: Star Convex Set is Simply Connected

Let $A$ be a star convex subset of a topological vector space $\struct {V, \tau}$ over $\R$ or $\C$.
Let $\tau_A$ be the subspace topology on $A$ induced by $\tau$.
Then $\struct {A, \tau_A}$ is simply connected.

Proof:
Let $a \in A$ be a star center of $A$.
Define $\mathbb I := \closedint 0 1$ as a closed real interval.
Let $\gamma : \mathbb I \to A$ be a loop in $A$ with base point $a$.
Let $\sigma : \mathbb I \to \set a$ be the constant function.
Constant Function is Continuous shows that $\sigma$ is continuous, so $\sigma$ is a loop with base point $a$.
Define $H: \mathbb I \times \mathbb I \to A$ by:
:$\map H {s, t} = t \map \gamma s + \paren {1 - t} a$
By definition of star convex set, we have $\map H {s, t} \in A$ for all $\tuple {s, t} \in \mathbb I \times \mathbb I$.
Define $F : \mathbb I \times \mathbb I \to A \times \mathbb I$ by $\map F {s, t} = \tuple {\map \gamma s, t}$.
As a loop is continuous, it follows that $F$ is continuous.
Define $\tilde G : V \times \mathbb I \to V$ by $\map {\tilde G} {v, t} = t v + \paren {1 - t} a$.
By definition of topological vector space, it follows that $\tilde G$ is continuous.
Let $G = \tilde G {\restriction_{\paren {A \times \mathbb I} \times A} }$ be the restriction of $\tilde G$ to $\paren {A \times \mathbb I} \times A$.
Restriction of Continuous Mapping is Continuous:Topological Spaces shows that $G$ is continuous.
Composite of Continuous Mappings is Continuous shows that $ H = G \circ F$ is continuous.
For all $s, t \in \mathbb I$, we check that $H$ is a path homotopy between $\gamma$ and $\sigma$:
{{begin-eqn}}
{{eqn | l = \map H {s, 0}
      | r = a 
      | rr = = \: \map \sigma s
}}
{{eqn | l = \map H {s, 1}
      | r = \map \gamma s
}}
{{eqn | l = \map H {0, t}
      | r = t a + \paren {1 - t} a 
      | rr = = \: a
}}
{{eqn | l = \map H {1, t}
      | r = t a + \paren {1 - t} a
      | rr = = \: a
}}
{{end-eqn}}
It follows that all loops with base point $a$ are path-homotopic with $\sigma$.
Relative Homotopy is Equivalence Relation shows that all loops with base point $a$ are path-homotopic with each other.
This implies that the fundamental group $\map {\pi_1} {A, a}$ is trivial.
Star Convex Set is Path-Connected shows that $A$ is path-connected.
Hence the result.
{{qed}}
Theorem: Convex Set is Simply Connected

Let $\struct {V, \tau}$ be a topological vector space over $\R$ or $\C$.
Let $A \subseteq V$ be a non-empty convex set.
Let $\tau_A$ be the subspace topology on $A$ induced by $\tau$.
Then $\struct{ A, \tau_A }$ is simply connected.

Proof:
Follows from Convex Set is Star Convex Set and Star Convex Set is Simply Connected.
{{qed}}
Category:Convex Sets (Vector Spaces)
Category:Simply Connected Spaces
ahzeja1h0tv4z4g66of67a273cw7i4d
Theorem: De Morgan's Laws (Predicate Logic)/Denial of Universality/Formulation 1

:$\neg \paren {\forall x: \map P x} \dashv \vdash \exists x: \neg \map P x$

Proof:
{{BeginTableau|\neg \paren {\forall x: \map P x} \vdash \exists x: \neg \map P x}}
{{Premise|1|\neg \paren {\forall x: \map P x} }}
{{Assumption|2|\neg \paren {\exists x: \neg \map P x} }}
{{Assumption|3|\neg \map P {\mathbf a}|for an arbitrary $\mathbf a$}}
{{TableauLine|n = 4|pool = 3|f = \exists x: \neg \map P x|rlnk = Existential Generalisation|rtxt = Existential Generalisation|dep = 3}}
{{NonContradiction|5|2, 3|2|4}}
{{Reductio|6|2|\map P {\mathbf a}|3|5}}
{{TableauLine|n = 7|pool = 1, 2|f = \forall x: \map P x|rlnk = Universal Generalisation|rtxt = Universal Generalisation|dep = 6|c = as $\mathbf a$ was arbitrary}}
{{NonContradiction|8|2|1|7}}
{{Reductio|9|1|\exists x: \neg \map P x|2|8}}
{{EndTableau|lemma}}
{{BeginTableau|\exists x: \neg \map P x \vdash \neg \paren {\forall x: \map P x} }}
{{Premise|1|\exists x: \neg \map P x}}
{{Assumption|2|\forall x: \map P x}}
{{TableauLine|n = 3|pool = 1|f = \neg \map P {\mathbf a}|rlnk = Existential Instantiation|rtxt = Existential Instantiation|dep = 1}}
{{TableauLine|n = 4|pool = 2|f = \map P {\mathbf a}|rlnk = Universal Instantiation|rtxt = Universal Instantiation|dep = 2}}
{{NonContradiction|5|1, 2|3|4}}
{{Contradiction|6|1|\neg \paren {\forall x: \map P x}|2|5}}
{{EndTableau|qed}}
{{LEM|Reductio ad Absurdum}}
Theorem: De Morgan's Laws (Predicate Logic)/Denial of Universality/Formulation 2

:$\vdash \neg \paren {\forall x: \map P x} \iff \paren{ \exists x: \neg \map P x }$

Proof:
{{WIP}}
Theorem: De Morgan's Laws (Predicate Logic)/Denial of Universality/Formulation 2/Forward Implication

:$\vdash \neg \paren {\forall x: \map P x} \implies \paren{ \exists x: \neg \map P x }$

Proof:
{{improve|These template invocations can be improved but I am happy the argument is at least conveyed now}}
{{BeginTableau|\vdash \neg \paren {\forall x: \map P x} \implies \paren{ \exists x: \neg \map P x }|Hilbert Proof System Instance 1 for Predicate Logic}}
{{Premise|1|\neg\neg \map P c \vdash \map P c | Axiom 1: Propositional Tautology, $c$ arbitrary }}
{{TableauLine|n = 2|f = \forall x: \neg\neg \map P x \vdash \neg\neg \map P c|rlnk = Universal Instantiation|rtxt = Universal Instantiation}}
{{TheoremIntro|3|\forall x: \neg\neg \map P x \vdash \map P c|from 1, 2, Provable Consequence of Theorems is Theorem}}
{{TableauLine|n = 4|f = \forall x: \neg\neg \map P x \vdash \forall x: \map P x|rlnk = Universal Generalisation|rtxt = Universal Generalisation|dep = 3}}
{{TheoremIntro|5|\paren{ \forall x: \neg\neg \map P x } \implies \forall x: \map P x|from 4, Deduction Theorem for Hilbert Proof System for Predicate Logic}}
{{TheoremIntro|6|\neg \paren{ \forall x: \map P x } \implies \neg \paren{ \forall x: \neg\neg \map P x }|from 5, Rule of Transposition}}
{{Premise|7|\paren{ \forall x: \neg \neg \map P x } \iff \neg \paren{ \exists x: \neg \map P x } | Axiom 6}}
{{BiconditionalElimination|8||\neg \paren{ \exists x: \neg \map P x } \implies \paren{ \forall x: \neg \neg \map P x }|7|2}}
{{TheoremIntro|9|\neg \paren{ \forall x: \neg\neg \map P x } \implies \paren{ \exists x: \neg \map P x } |from 8, Rule of Transposition}}
{{TheoremIntro|10|\neg \paren {\forall x: \map P x} \implies \paren{ \exists x: \neg \map P x }|from 6, 9, Hypothetical Syllogism}}
{{EndTableau|qed}}
Theorem: De Morgan's Laws (Predicate Logic)/Denial of Universality/Formulation 2/Reverse Implication

:$\vdash \paren{ \exists x: \neg \map P x } \implies \neg \paren {\forall x: \map P x}$

Proof:
{{WIP}}
Theorem: Continuous Mapping from Compact Space to Hausdorff Space is Closed Mapping

Let $T_1 = \struct {S_1, \tau_1}$ be a compact topological space.
Let $T_2 = \struct {S_2, \tau_2}$ be a $T_2$ (Hausdorff) space.
Let $f: T_1 \to T_2$ be a continuous mapping.
Then $f$ is a closed mapping.

Proof:
Let $C$ be a closed subspace of $T_1$.
By Closed Subspace of Compact Space is Compact, $C$ is compact.
By Continuous Image of Compact Space is Compact, $f \sqbrk C$ is compact in $T_2$.
By Compact Subspace of Hausdorff Space is Closed, $f \sqbrk C$ is closed in $T_2$.
The result follows by definition of closed mapping.
{{qed}}
Category:Compact Topological Spaces
Category:Hausdorff Spaces
Category:Closed Mappings
kjec5jlzfp4m2og3atxnnd3gp05j2zi
Theorem: Lamé's Theorem/Least Absolute Remainder

Let $a, b \in \Z_{>0}$ be (strictly) positive integers.
Let $c$ and $d$ be the number of digits in $a$ and $b$ respectively when expressed in decimal notation.
Let the Euclidean Algorithm: Least Absolute Remainder variant be employed to find the GCD of $a$ and $b$.
Then it will in general take fewer integer divisions to find $\gcd \set {a, b}$ than it does to use the conventional form of the Euclidean Algorithm.
In fact, it will take fewer than $3 \times \min \set {c, d}$ integer divisions to find $\gcd \set {a, b}$.

Proof:
=== Lemma===
{{:Lamé's Theorem/Least Absolute Remainder/Lemma}}{{qed|lemma}}
{{WLOG}} suppose $a \ge b$. 
Then $\min \set {c, d}$ is the number of digits in $b$.
By Number of Digits in Number, we have:
:$\min \set {c, d} = \floor {\log b} + 1$
{{AimForCont}} it takes at least $3 \paren {\floor {\log b} + 1}$ cycles around the Euclidean Algorithm: Least Absolute Remainder variant to find $\gcd \set {a, b}$.
Then we have:
{{begin-eqn}}
{{eqn | l = b
      | o = \ge
      | r = P_{3 \paren {\floor {\log b} + 1} + 1}
      | c = Lemma
}}
{{eqn | o = \ge
      | r = 2 \paren {1 + \sqrt 2}^{3 \paren {\floor {\log b} + 1} - 1}
      | c = Lower Bound of Pell Number: $P_n \ge 2 \paren {1 + \sqrt 2}^{n - 2}$
}}
{{eqn | r = \frac 2 {1 + \sqrt 2} \paren {1 + \sqrt 2}^{3 \paren {\floor {\log b} + 1} }
}}
{{eqn | o = >
      | r = 1 \cdot \paren {1 + \sqrt 2}^{3 \log b}
      | c = {{Defof|Floor Function|subdef = Definition 3}}
}}
{{end-eqn}}
For $b = 1$, both sides are equal to $1$, giving $1 > 1$, which is a contradiction.
Hence we consider $b > 1$ and take $\log$ on both sides:
{{begin-eqn}}
{{eqn | ll= \leadsto
      | l = \log b
      | o = >
      | r = \paren {3 \log b} \log \paren {1 + \sqrt 2}
      | c = Logarithm of Power
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {\log \paren {1 + \sqrt 2} }
      | o = >
      | r = 3
}}
{{end-eqn}}
However, $\dfrac 1 {\log \paren {1 + \sqrt 2} } \approx 2.6125 < 3$.
This is a contradiction.
Hence the result by Proof by Contradiction.
{{qed}}
{{Namedfor|Gabriel Lamé}}
Theorem: GCD of Integers with Common Divisor/Corollary

Let $a, b \in \Z$ be integers such that not both $a = 0$ and $b = 0$.
Let $k \in \Z_{\ne 0}$ be a non-zero integer.
Then:
:$\gcd \set {k a, k b} = \size k \gcd \set {a, b}$
where $\gcd$ denotes the greatest common divisor.

Proof:
From GCD of Integers with Common Divisor the case where $k > 0$ has been demonstrated.
It remains to demonstrate the case where $k < 0$.
Indeed:
:$-k = \size k > 0$
and so:
{{begin-eqn}}
{{eqn | l = \gcd \set {a k, b k}
      | r = \gcd \set {-a k, -b k}
      | c = 
}}
{{eqn | r = \gcd \set {a \size k, b \size k}
      | c = 
}}
{{eqn | r = \size k \gcd \set {a, b}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equivalence of Definitions of Non-Archimedean Vector Space Norm

Let $\struct {R, +, \circ}$ be a division ring with norm $\norm {\,\cdot\,}_R$.
Let $X$ be a vector space over $R$, with zero $0_X$.
{{TFAE|def = Non-Archimedean Vector Space Norm}}
=== Definition 1 ===
{{:Definition:Non-Archimedean/Norm (Vector Space)/Definition 1}}
=== Definition 2 ===
{{:Definition:Non-Archimedean/Norm (Vector Space)/Definition 2}}

Proof:
=== Definition 1 implies Definition 2 ===
Let $\norm {\,\cdot\,} : X \to \R_{\ge 0}$ be a norm on a division ring satisfying:
{{begin-axiom}}
{{axiom | n = \text N 4
        | lc= Ultrametric Inequality:
        | q = \forall x, y \in X
        | ml= \norm {x + y}
        | mo= \le
        | mr= \max \set {\norm x, \norm y}
}}
{{end-axiom}}
It remains only to show that $\norm {\,\cdot\,}$ satisfies $(\text N 1)$ and $(\text N 2)$.
This follows from the definition of a norm on a division ring.
{{qed|lemma}}
Theorem: Path as Parameterization of Contour/Corollary 1

If $\gamma$ is a closed path, then $C$ is a closed contour.

Proof:
By definition of closed path, we have
:$\map \gamma a = \map {\gamma_1} {a_0} = \map {\gamma_n} {a_n}$
so:
:$C_1$ has start point $\map \gamma a$
and:
:$C_n$ has end point $\map \gamma a$.
By definition, it follows that $C$ is a closed contour.
{{qed}}
Category:Path as Parameterization of Contour
syjz8x3d90onovtv1n8rz41fjjrdlda
Theorem: Path as Parameterization of Contour/Corollary 2

If $\gamma$ is a Jordan arc, then $C$ is a simple contour, and if $\gamma$ is a Jordan curve, then $C$ is a simple closed contour.

Proof:
Let $k_1, k_2 \in \set {1, \ldots, n}$, and $t_1 \in \hointr {a_{k_1 - 1} } {a_{k_1} }, t_2 \in \hointr {a_{k_2 - 1} } {a_{k_2} }$.
Then by the definition of Jordan arc, or Jordan curve:
:$\map \gamma {t_1} \ne \map \gamma {t_2}$
so:
:$\map {\gamma_{k_1} } {t_1} \ne \map {\gamma_{k_2} } {t_2}$
Let instead:
:$k \in \set {1, \ldots, n}$
and:
:$t \in \hointr {a_{k - 1} } {a_k}$ with $t \ne a_1$.
Then by the definition of Jordan arc, or Jordan curve:
:$\map \gamma t \ne \map \gamma {a_n}$
so:
:$\map {\gamma_k} t \ne \map {\gamma_n} {a_n}$
By definition, it follows that $C$ is a simple contour.
A Jordan curve is a closed path by its definition.
Path as Parameterization of Contour/Corollary 1 shows that if $\gamma$ is a Jordan curve, then $C$ will be closed, so $C$ is a simple closed contour.
{{qed}}
Category:Path as Parameterization of Contour
ss6hwwi33z9xk8ddzw2tc5boz6684tf