avewright/proofwiki-math huggingface dataset:
Theorem: Group Epimorphism preserves Central Subgroups

Let $G$ and $H$ be groups.
Let $\theta: G \to H$ be an epimorphism.
Let $Z \le G$ be a central subgroup of $G$.
Then $\theta \sqbrk Z$ is a central subgroup of $H$.

Proof:
By definition of central subgroup:
:$Z \subseteq \map Z G$
where $\map Z G$ denotes the center of $G$.
From Image under Epimorphism of Center is Subset of Center:
:$\theta \sqbrk {\map Z G} \subseteq \map Z H$
From Image of Subset under Mapping is Subset of Image it follows that:
:$\theta \sqbrk Z \subseteq \map Z H$
The result follows.
{{qed}}
Category:Central Subgroups
Category:Group Epimorphisms
9fdj8xamuhphxaj2xl5xszjyb657b1r
Theorem: Direct Product of Central Subgroups

Let $G$ and $H$ be groups.
Let $Z$ and $W$ be central subgroups of $G$ and $H$ respectively.
Then $Z \times W$ is a central subgroup of $G \times H$.

Proof:
Let $\tuple {z, w} \in Z \times W$.
Let $\tuple {x, y} \in G \times H$.
Then:
{{begin-eqn}}
{{eqn | l = \tuple {x, y} \tuple {z, w}
      | r = \tuple {x z, y w}
      | c = {{Defof|Group Direct Product}}
}}
{{eqn | r = \tuple {z x, w y}
      | c = {{Defof|Central Subgroup}}
}}
{{eqn | r = \tuple {z, w} \tuple {x, y}
      | c = {{Defof|Group Direct Product}}
}}
{{end-eqn}}
$\tuple {x, y}$ is arbitrary.
Thus $\tuple {z, w}$ commutes with all elements of $G \times H$.
Hence $\tuple {z, w}$ is in the center of $G \times H$
That is, $Z \times W$ is a subgroup of the center $G \times H$.
The result follows by definition of central subgroup.
{{qed}}
Category:Central Subgroups
Category:Group Direct Products
t3bozwduh2dv43876c7vq6v7lgk7520
Theorem: Sequence of Integers defining Abelian Group

Let $n \in \Z_{>0}$ be a strictly positive integer.
Let $C_n$ be a finite abelian group.
Then $C_n$ is of the form:
:$C_{n_1} \times C_{n_2} \times \cdots \times C_{n_r}$
such that:
:$n = \ds \prod_{k \mathop = 1}^r n_k$
:$\forall k \in \set {2, 3, \ldots, r}: n_k \divides n_{k - 1}$
where $\divides$ denotes divisibility.

Proof:
{{ProofWanted|This is probably just a statement of Fundamental Theorem of Finite Abelian Groups, which needs to be studied to see what it actually means}}
Theorem: Parallelism is Equivalence Relation

Let $S$ be the set of straight lines in the plane.
For $l_1, l_2 \in S$, let $l_1 \parallel l_2$ denote that $l_1$ is parallel to $l_2$.
Then $\parallel$ is an equivalence relation on $S$.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Connected Equivalence Relation is Trivial

Let $S$ be a set.
Let $\RR$ be a relation on $S$ which is both connected and an equivalence relation.
Then $\RR$ is the trivial relation on $S$.

Proof:
By definition of equivalence relation, $\RR$ is an equivalence relation {{iff}}:
:$\Delta_S \cup \RR^{-1} \cup \RR \circ \RR \subseteq \RR$
From Relation is Connected iff Union with Inverse and Diagonal is Trivial Relation:
:$\Delta_S \cup \RR^{-1} \cup \RR = S \times S$
Hence the result.
{{qed}}
Theorem: Characterisation of Non-Archimedean Division Ring Norms/Sufficient Condition/Lemma 3

Let $\sequence {x_n}$ be the real sequence defined as $x_n = \paren {n + 1}^{1/n}$, using exponentiation.
Then $\sequence {x_n}$ converges with a limit of $1$.

Proof:
We have the definition of the power to a real number:
:$\paren {n + 1}^{1/n} = \map \exp {\dfrac 1 n \map \ln {n + 1} }$
For $n \ge 1$ then $n + 1 \le 2 n$.
Hence:
{{begin-eqn}}
{{eqn | l = \frac 1 n \map \ln {n + 1}
      | o = \le
      | r = \frac 1 n \map \ln {2 n}
      | c = Logarithm is Strictly Increasing
}}
{{eqn | o =
}}
{{eqn | r = \frac 1 n \paren {\ln 2 + \ln n}
      | c = Logarithm on Positive Real Numbers is Group Isomorphism
}}
{{eqn | o =}}
{{eqn | r = \frac {\ln 2} n + \frac 1 n \ln n
      | c = 
}}
{{end-eqn}}
By Powers Drown Logarithms:
:$\ds \lim_{n \mathop \to \infty} \frac 1 n \ln n = 0$
By Sequence of Reciprocals is Null Sequence:
:$\ds \lim_{n \mathop \to \infty} \frac 1 n = 0$
By Combined Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {\frac {\ln 2} n + \frac 1 n \ln n} = \ln 2 \cdot 0 + 0 = 0$
By the Squeeze Theorem for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \paren {n + 1}^{1/n} = 0$
Hence:
:$\ds \lim_{n \mathop \to \infty} \paren {n + 1}^{1/n} = \exp 0 = 1$
and the result follows.
{{qed}}
Category:Characterisation of Non-Archimedean Division Ring Norms
nkvlqqj1fy3yebigclg1vyowc5o5n4o
Theorem: Characterisation of Non-Archimedean Division Ring Norms/Corollary 1

$\norm {\,\cdot\,}$ is non-Archimedean {{iff}}:
:$\sup \set {\norm {n \cdot 1_R}: n \in \N_{> 0}} = 1$.

Proof:
By Characterisation of Non-Archimedean Division Ring Norms then:
:$\norm {\,\cdot\,}$ is non-Archimedean {{iff}}:
::$\sup \set {\norm {n \cdot 1_R}: n \in \N_{\gt 0}} \le 1$
By norm of unity then:
:$\norm {1_R} = 1$
The result follows.
{{qed}}
Theorem: Characterisation of Non-Archimedean Division Ring Norms/Corollary 3

$\norm {\,\cdot\,}$ is Archimedean {{iff}}:
:$\sup \set {\norm {n \cdot 1_R}: n \in \N_{>0} } = +\infty$

Proof:
By Characterisation of Non-Archimedean Division Ring Norms:
:$\norm {\,\cdot\,}$ is Archimedean $\iff \sup \set {\norm {n \cdot 1_R}: n \in \N_{>0} } > 1$
By {{Corollary|Characterisation of Non-Archimedean Division Ring Norms|2}}:
:$\sup \set {\norm {n \cdot 1_R}: n \in \N_{>0} } > 1 \iff \sup \set {\norm {n \cdot 1_R}: n \in \N_{>0} } = +\infty$
{{qed}}
Theorem: Characterisation of Non-Archimedean Division Ring Norms/Corollary 2

Let $\sup \set {\norm {n \cdot 1_R}: n \in \N_{> 0} } = C < +\infty$.

Proof:
{{AimForCont}} $C > 1$.
By Characterizing Property of Supremum of Subset of Real Numbers:
:$\exists m \in \N_{> 0}: \norm {m \cdot 1_R} > 1$
Let   
:$x = m \cdot 1_R$ 
:$y = x^{-1}$
By Norm of Inverse:
:$\norm y < 1$
By Sequence of Powers of Number less than One:
:$\ds \lim_{n \mathop \to \infty} \norm y^n = 0$
By Reciprocal of Null Sequence then:
:$\ds \lim_{n \mathop \to \infty} \frac 1 {\norm y^n} = +\infty$
For all $n \in \N_{> 0}$:
{{begin-eqn}}
{{eqn | l = \dfrac 1 {\norm y^n}
      | r = \norm {y^{-1} }^n
      | c = Norm of Inverse
}}
{{eqn | r = \norm x^n
      | c = Definition of $y$
}}
{{eqn | r = \norm {x^n}
      | c = {{NormAxiomNonArch|2}}
}}
{{eqn | r = \norm {\paren {m \cdot 1_R}^n}
      | c = Definition of $x$
}}
{{eqn | r = \norm {m^n \cdot 1_R}
}}
{{end-eqn}}
So:
:$\ds \lim_{n \mathop \to \infty} \norm {m^n \cdot 1_R} = +\infty$
Hence:
:$\sup \set {\norm{n \cdot 1_R}: n \in \N_{> 0} } = +\infty$
This contradicts the assumption that $C < +\infty$.
{{qed|lemma}}
It follows that $C \le 1$.
Then:
:$\forall n \in \N_{>0}: \norm{n \cdot 1_R} \le 1$
By Characterisation of Non-Archimedean Division Ring Norms, $\norm{\,\cdot\,}$ is non-Archimedean.
By {{Corollary|Characterisation of Non-Archimedean Division Ring Norms|1}}:
:$\sup \set {\norm {n \cdot 1_R}: n \in \N_{> 0} } = 1$
So $C = 1$.
{{qed}}
Theorem: Characterisation of Non-Archimedean Division Ring Norms/Corollary 4

Let $R$ have characteristic $p > 0$.
Then $\norm {\,\cdot\,}$ is a non_Archimedean norm on $R$.

Proof:
Because $R$ has characteristic $p > 0$, the set:
:$\set {n \cdot 1_k: n \in \Z}$
has cardinality $p - 1$.
Therefore:
:$\sup \set {\norm {n \cdot 1_R}: n \in \Z} = \max \set {\norm {1 \cdot 1_R}, \norm {2 \cdot 1_R}, \cdots, \norm {\paren {p - 1} \cdot 1_R} } < +\infty$
By {{Corollary|Characterisation of Non-Archimedean Division Ring Norms|2}}:
:$\norm{\,\cdot\,}$ is non-Archimedean and $C = 1$.
{{qed}}
Category:Characterisation of Non-Archimedean Division Ring Norms
lmvyb40opk7g3jlkeickr9qlqzthv2s
Theorem: Norms Equivalent to Absolute Value on Rational Numbers

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:
:$\norm {\,\cdot\,}$ be a norm on $\Q$
{{iff}}:
:$\alpha \le 1$

Proof:
=== Necessary Condition ===
{{:Norms Equivalent to Absolute Value on Rational Numbers/Necessary Condition}}{{qed|lemma}}
Theorem: Reflexive Relation on Set of Cardinality 2 is Transitive

Let $S$ be a set whose cardinality is equal to $2$:
:$\card S = 2$
Let $\odot \subseteq S \times S$ be a reflexive relation on $S$.
Then $\odot$ is also transitive.

Proof:
{{WLOG}}, let $S = \set {a, b}$.
Let $\odot$ be reflexive.
By definition of reflexive relation:
:$\Delta_S \subseteq \odot$
where $\Delta_S$ is the diagonal relation:
:$\Delta_S = \set {\tuple {x, x}: x \in S}$
That is:
:$\set {\tuple {a, a}, \tuple {b, b} } \subseteq \odot$
Suppose $\set {\tuple {a, a}, \tuple {b, b} } = \odot$.
Then by Diagonal Relation is Equivalence, $\odot$ is transitive.
Suppose there exists $\tuple {x, y} \in \odot$ such that $\tuple x \ne y$ and $\tuple {y, x} \notin \odot$.
Then:
:$x \odot x, x \odot y \implies x \odot y$
and:
:$x \odot y, y \odot y \implies x \odot y$
Now suppose there exists $\tuple {x, y} \in \odot$ such that $\tuple x \ne y$ and $\tuple {y, x} \in \odot$.
Then we have:
:$x \odot y, y \odot x \implies x \odot x$
and:
:$y \odot x, x \odot y \implies y \odot y$
which hold because $\odot$ is reflexive
Hence in all cases, a reflexive relation on $S$ is also transitive.
{{qed}}
Category:Reflexive Relations
Category:Transitive Relations
lhc0zlz6rinxrqyqa85wu1x5pkupht9
Theorem: Relation on Set of Cardinality 2 cannot be Non-Symmetric and Non-Transitive

Let $S$ be a set whose cardinality is equal to $2$:
:$\card S = 2$
Let $\odot \subseteq S \times S$ be a relation on $S$.
Then it is not possible for $\odot$ to be not symmetric and also not transitive.

Proof:
{{WLOG}}, let $S = \set {a, b}$.
Let $\odot$ not be symmetric.
{{AimForCont}} $\odot$ is not transitive.
As $\odot$ is not symmetric:
:$\exists \tuple {x, y} \in \odot: \tuple {y, x} \notin \odot$
Thus there are two possibilities:
:$\exists \tuple {a, b} \in \odot: \tuple {b, a} \notin \odot$
:$\exists \tuple {b, a} \in \odot: \tuple {a, b} \notin \odot$
{{WLOG}}, let $\tuple {a, b} \in \odot$.
As $\odot$ is not transitive, either:
:$\exists \tuple {x, a} \in \odot: \tuple {x, b} \notin \odot$
or:
:$\exists \tuple {b, y} \in \odot: \tuple {a, y} \notin \odot$
In the first case, $x \ne b$ as that would make $\odot$ symmetric.
In the second case, $y \ne a$ as that would also make $\odot$ symmetric.
Hence $x = a$ and $y = b$, and we have either:
:$\exists \tuple {a, a} \in \odot: \tuple {a, b} \notin \odot$
or:
:$\exists \tuple {b, b} \in \odot: \tuple {a, b} \notin \odot$
But it has been established that $\tuple {a, b} \in \odot$.
From this contradiction it follows that $\odot$ is transitive.
Hence it is not possible for $\odot$ to be neither symmetric nor transitive.
{{qed}}
Category:Non-Symmetric Relations
Category:Non-Transitive Relations
9hfuuappaxw36t6gogcm2979gdnu0xt
Theorem: Relations with Combinations of Reflexivity, Symmetry and Transitivity Properties

Let $S$ be a set which has at least $3$ elements.
Then it is possible to set up a relation $\circledcirc$ on $S$ which has any combination of the $3$ properties:
:Reflexivity
:Symmetry
:Transitivity
but this is not possible for a set which has fewer than $3$ elements.

Proof:
In the following:
:$S_n$ denotes the set $S_n = \set {s_1, s_2, \ldots, s_n}$ of cardinality $n$, where $n \in \Z_{\ge 0}$ is a non-negative integer.
:$\circledcirc$ denotes an arbitrary relation on $S_n$.
Let:
:$\map R \circledcirc$ denote that $\circledcirc$ is reflexive
:$\map S \circledcirc$ denote that $\circledcirc$ is symmetric
:$\map T \circledcirc$ denote that $\circledcirc$ is transitive
Theorem: Relation on Set of Cardinality 1 is Symmetric and Transitive

Let $S$ be a set whose cardinality is equal to $1$:
:$\card S = 1$
Let $\odot \subseteq S \times S$ be a relation on $S$.
Then $\odot$ is both symmetric and transitive.

Proof:
{{WLOG}}, let $S = \set a$.
There are $2$ relations on $S$:
$(1): \quad \odot := \O$, which is the null relation on $S$.
From Null Relation is Antireflexive, Symmetric and Transitive, $\odot$ is antireflexive, symmetric and transitive.
Thus in this case $\odot$ is both symmetric and transitive.
$(2): \quad \odot := \set {\tuple {a, a} }$, which is the trivial relation on $S$.
From Trivial Relation is Equivalence, $\odot$ is reflexive, symmetric and transitive.
Thus in this case also, $\odot$ is both symmetric and transitive.
{{qed}}
Category:Symmetric Relations
Category:Transitive Relations
3mj1jd4zecex4gsih4bo4ufrwlqndfh
Theorem: Congruence of Triangles is Equivalence Relation

Let $S$ denote the set of all triangles in the plane.
Let $\triangle A \cong \triangle B$ denote the relation that $\triangle A$ is congruent to $\triangle B$.
Then $\cong$ is an equivalence relation on $S$.

Proof:
Checking in turn each of the criteria for equivalence:
Theorem: Cardinality of Mapping

Let $S$ be a finite set whose cardinality is $n$:
:$\card S = n$
Let $T$ be a non-empty set
Let $f: S \to T$ be a mapping.
Then:
:$\card f = n$

Proof:
First suppose $T = \O$ there are no elements in $f$
From Null Relation is Mapping iff Domain is Empty Set, there are no elements in $f$.
Hence in this case $\card f = 0$, whatever $\card S$ may be,
By definition of mapping, $f$ is a set of ordered pairs $\tuple {s, t}$ where $s \in S$ and $t \in T$, such that:
:$(1): \quad \forall s \in S: \exists \tuple {s, t} \in f$
and:
:$(2): \quad \forall x \in S: \tuple {s, t_1} \in f \land \tuple {s, t_2} \in f \implies t_1 = t_2$
From $(1)$ it follows that $\card f \ge n$.
{{AimForCont}} that $\card f > n$.
Then by the Pigeonhole Principle:
:$\exists x \in f: \exists y_1, y_2 \in T, y_1 \ne y_2: \tuple {x, y_1} \in f \land \tuple {x, y_2} \in f$
and so $f$ is not a mapping.
From this contradiction it follows that $\card f = n$.
{{qed}}
Theorem: Even Integer Plus 5 is Odd

Let $x \in \Z$ be an even integer.
Then $x + 5$ is odd.

Proof:
Let $x$ be an even integer.
Let $y = 2 n + 5$.
Assume $y = x + 5$ is not an odd integer.
Then:
:$y = x + 5 = 2 n$
where $n \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = 2 n - 5
      | c = 
}}
{{eqn | r = \paren {2 n - 6} + 1
      | c = 
}}
{{eqn | r = 2 \paren {n - 3} + 1
      | c = 
}}
{{eqn | r = 2 r + 1
      | c = where $r = n - 3 \in \Z$
}}
{{end-eqn}}
Hence $x$ is odd.
That is, it is false that $x$ is even.
It follows by the Rule of Transposition that if $x$ is even, then $y$ is odd.
{{qed}}
Theorem: Even Integer Plus 5 is Odd

Let $x \in \Z$ be an even integer.
Then $x + 5$ is odd.

Proof:
Let $x$ be an even integer.
Then by definition:
:$x = 2 n$
for some integer $n$.
{{AimForCont}} $y = x + 5 = 2 m$ for some integer $m$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = 2 m - 5
      | c = 
}}
{{eqn | r = \paren {2 m - 6} + 1
      | c = 
}}
{{eqn | r = 2 \paren {m - 3} + 1
      | c = 
}}
{{eqn | r = 2 r + 1
      | c = where $r = m - 3 \in \Z$
}}
{{end-eqn}}
Hence $x$ is odd.
But this contradicts our premise that $x$ is even.
Hence the result by Proof by Contradiction.
{{qed}}
Theorem: Arcsine as Integral

:$\ds \map \arcsin x = \int_0^x \frac {\d x} {\sqrt {1 - x^2} }$

Proof:
=== Lemma 1 ===
{{:Arcsine as Integral/Lemma 1}}{{qed|lemma}}
Theorem: Sum of Even Sequence of Products of Consecutive Fibonacci Numbers

:$\ds \sum_{j \mathop = 1}^{2 n} F_j F_{j + 1} = {F_{2 n + 1} }^2 - 1$

Proof:
From Sum of Odd Sequence of Products of Consecutive Fibonacci Numbers:
:$(1): \quad \ds \sum_{j \mathop = 1}^{2 n - 1} F_j F_{j + 1} = {F_{2 n} }^2$
Hence:
{{begin-eqn}}
{{eqn | l = \sum_{j \mathop = 1}^{2 n} F_j F_{j + 1}
      | r = \sum_{j \mathop = 1}^{2 n - 1} F_j F_{j + 1} + F_{2 n} F_{2 n + 1}
      | c = 
}}
{{eqn | r = {F_{2 n} }^2 + F_{2 n} F_{2 n + 1}
      | c = from $(1)$
}}
{{eqn | r = F_{2 n} \paren {F_{2 n} + F_{2 n + 1} }
      | c = 
}}
{{eqn | r = F_{2 n} F_{2 n + 2}
      | c = 
}}
{{eqn | r = {F_{2 n + 1} }^2 - 1
      | c = Cassini's Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Lucas Number as Element of Recursive Sequence

Let $L_k$ be the $k$th Lucas number, defined as the sum of two Fibonacci numbers:
:$L_n = F_{n - 1} + F_{n + 1}$
Then $L_n$ can be defined as the $n$th element of the recursive sequence:
:$L_n = \begin{cases}
2 & : n = 0 \\
1 & : n = 1 \\
L_{n - 1} + L_{n - 2} & : \text{otherwise} \end{cases}$

Proof:
Proof by induction:
Let $L_n$ be the Lucas number defined as the sum of two Fibonacci numbers:
:$L_n = F_{n - 1} + F_{n + 1}$
For all $n \in \N$, let $\map P n$ be the proposition:
:$L_n = \begin{cases}
2 & : n = 0 \\
1 & : n = 1 \\
L_{n - 1} + L_{n - 2} & : \text{otherwise} \end{cases}$
Theorem: Product of nth Lucas and Fibonacci Numbers

Let $L_k$ be the $k$th Lucas number.
Let $F_k$ be the $k$th Fibonacci number.
Then:
:$\forall n \in \N_{>0}: F_n L_n = F_{2 n}$

Proof:
By definition of Lucas numbers:
:$L_n = F_{n - 1} + F_{n + 1}$
Hence:
:$F_n L_n = F_n \paren {F_{n - 1} + F_{n + 1} }$
From Honsberger's Identity:
:$\forall m, n \in \Z_{>0}: F_{m + n} = F_{m - 1} F_n + F_m F_{n + 1}$
The result follows by setting $m = n$.
{{qed}}
Theorem: Representation of Integers in Balanced Ternary

Let $n \in \Z$ be an integer.
$n$ can be represented uniquely in balanced ternary:
:$\ds n = \sum_{j \mathop = 0}^m r_j 3^j$
:$\sqbrk {r_m r_{m - 1} \ldots r_2 r_1 r_0}$
such that:
where:
:$m \in \Z_{>0}$ is a strictly positive integer such that $3^m < \size {2 n} < 3^{m + 1}$
:all the $r_j$ are such that $r_j \in \set {\underline 1, 0, 1}$, where $\underline 1 := -1$.

Proof:
Let $n \in \Z$.
Let $m \in \Z_{\ge 0}$ be such that:
:$3^m + 1 \le \size {2 n} \le 3^{m + 1} - 1$
where $\size {2 n}$ denotes the absolute value of $2 n$.
As $2 n$ is even, this is always possible, because $3^r$ is always an odd integer for non-negative $r$.
Let $d = \dfrac {3^{m + 1} - 1} 2$.
Let $k = n + d$.
We have that:
{{begin-eqn}}
{{eqn | l = \size {2 n}
      | o = \le
      | r = 3^{m + 1} - 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \size n
      | o = \le
      | r = d
      | c = Definition of $d$
}}
{{eqn | ll= \leadsto
      | l = -d
      | o = \le
      | r = n \le d
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 0
      | o = \le
      | r = n + d \le 3^{m + 1} - 1
      | c = 
}}
{{end-eqn}}
Let $k = n + d \in \Z$ be represented in ternary notation:
:$k = \ds \sum_{j \mathop = 0}^m s_j 3^j$
where $s_j \in \set {0, 1, 2}$.
By the Basis Representation Theorem, this expression for $k$ is unique.
Now we have:
{{begin-eqn}}
{{eqn | l = d
      | r = \dfrac {3^{m + 1} - 1} {3 - 1}
      | c = by definition
}}
{{eqn | r = \sum_{j \mathop = 0}^m 3^j
      | c = Sum of Geometric Sequence
}}
{{end-eqn}}
Hence we see:
{{begin-eqn}}
{{eqn | l = n
      | r = k - d
      | c = by definition
}}
{{eqn | r = \sum_{j \mathop = 0}^m s_j 3^j - \sum_{j \mathop = 0}^m 3^j
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 0}^m \paren {s_j - 1} 3^j
      | c = 
}}
{{eqn | r = \sum_{j \mathop = 0}^m r_j 3^j
      | c = where $r_j \in \set {-1, 0, 1}$
}}
{{end-eqn}}
Hence $n$ has a representation in balanced ternary.
The representation for $k$ in ternary notation is unique, as established.
Hence the representation in balanced ternary for $n$ is also unique.
{{qed}}
{{Proofread|Not completely sure that uniqueness has been properly proved.}}
Theorem: Absolute Value is Norm

The absolute value is a norm on the set of real numbers $\R$.

Proof:
By Complex Modulus is Norm then the complex modulus satisfies the norm axioms on the set of complex numbers $\C$.
Since the real numbers $\R$ is a subset of the complex numbers $\C$ then the complex modulus satisfies the norm axioms on the real numbers $\R$.
By Complex Modulus of Real Number equals Absolute Value then the absolute value satisfies the norm axioms on set of real numbers $\R$.
{{qed}}
Theorem: Bounds for Integer Expressed in Base k

Let $n \in \Z$ be an integer.
Let $k \in \Z$ such that $k \ge 2$.
Let $n$ be expressed in base $k$ notation:
:$n = \ds \sum_{j \mathop = 1}^s a_j k^j$
where each of the $a_j$ are such that $a_j \in \set {0, 1, \ldots, k - 1}$.
Then:
:$0 \le n < k^{s + 1}$

Proof:
As none of the coefficients $a_j$ in $\ds \sum_{j \mathop = 1}^s a_j k^j$ is (strictly) negative, the summation itself likewise cannot be negative
Thus:
:$0 \le n$
The equality is satisfied when $a_j = 0$ for all $j$.
We then have:
{{begin-eqn}}
{{eqn | l = n
      | r = \sum_{j \mathop = 1}^s a_j k^j
      | c = 
}}
{{eqn | o = \le
      | r = \paren {k - 1} \sum_{j \mathop = 1}^s k^j
      | c = as $a_j \le k - 1$ for all $j$
}}
{{eqn | r = \paren {k - 1} \dfrac {k^{s + 1} - 1} {k - 1}
      | c = Sum of Geometric Sequence
}}
{{eqn | r = k^{s + 1} - 1
      | c = 
}}
{{eqn | o = <
      | r = k^{s + 1}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Different Representations to Number Base represent Different Integers

Let $k \in \Z$ such that $k \ge 2$.
Let $a$ and $b$ be representations of integers in base $k$ notation:
:$a = \ds \sum_{j \mathop = 0}^r a_j k^j$
:$b = \ds \sum_{j \mathop = 0}^s b_j k^j$
such that either:
:$r \ne s$
or:
:$\exists j \in \set {0, 1, \ldots, r}: a_j \ne b_j$
Then $a$ and $b$ represent different integers.

Proof:
First suppose that $r \ne s$.
{{WLOG}}, suppose $r > s$.
Then from Bounds for Integer Expressed in Base k:
{{begin-eqn}}
{{eqn | l = a_r k^r
      | o = >
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | o = >
      | r = b
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | o = \ne
      | r = b
      | c = 
}}
{{end-eqn}}
Otherwise $r = s$.
Let $l$ be the largest such that $a_l \ne b_l$.
{{WLOG}}, suppose $a_l > b_l$.
For all $j > l$, let $a_1 = a - a_j k_j$ and $b_1 = b - b_j k_j$.
As $a_j = b_j$ in this range, $a_j k_j = b_j k_j$ and so the same amount is being subtracted from both.
So consider $\paren {a_l - b_l} k_l$.
From Bounds for Integer Expressed in Base k:
:$\paren {a_l - b_l} k_l > \ds \sum_{j \mathop = 0}^{l - 1} a_j k^j$
and:
:$\paren {a_l - b_l} k_l > \ds \sum_{j \mathop = 0}^{l - 1} b_j k^j$
and so $a_1 > b_1$.
Hence:
:$a_1 + a_j k_j > b_1 + b_j k_j$
Hence:
:$a \ne b$
and hence the result.
{{qed}}
{{Proofread}}
Theorem: Existence of q for which j - qk is Positive

Let $j, k \in \Z$ be integers such that $k > 0$.
Then there exist $q \in \Z$ such that $j - q k > 0$.

Proof:
Let $q = -\size j - 1$.
Then:
{{begin-eqn}}
{{eqn | l = j - q k
      | r = j - \paren {-\size j - 1} k
      | c = 
}}
{{eqn | r = j + \size j + k
      | c = 
}}
{{end-eqn}}
We have that:
:$\forall j \le 0: j + \size j = 0$
and:
:$\forall j > 0: j + \size j = 2 j$
So:
:$j - q k \ge k$
and as $k > 0$ the result follows.
{{qed}}
Theorem: Power Function on Base between Zero and One is Strictly Decreasing/Real Number

Let $a \in \R$ be a real number such that $0 \lt a \lt 1$.
Let $f: \R \to \R$ be the real function defined as:
:$\map f x = a^x$
where $a^x$ denotes $a$ to the power of $x$.
Then $f$ is strictly decreasing.

Proof:
Let $x, y \in \R$ be such that $x < y$.
Since $0 < a < 1$, we have that:
:$\dfrac 1 a > 1$
Then we have that:
{{begin-eqn}}
{{eqn | l = \paren {\dfrac 1 a}^x 
      | o = <
      | r = \paren {\dfrac 1 a}^y
      | c = Real Power Function on Base Greater than One is Strictly Increasing
}}
{{eqn | ll= \leadstoandfrom
      | l = \dfrac 1 {a^x}
      | o = <
      | r = \dfrac 1 {a^y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | l = a^x
      | o = >
      | r = a^y
      | c = Reciprocal Function is Strictly Decreasing
}}
{{end-eqn}}
The result follows.
{{qed}}
Category:Power Function on Base between Zero and One is Strictly Decreasing
5b3907fc75dupddxgephkodb55l5y9t