nyuuzyou/wikis huggingface dataset:
Canonical Injection is Injection

== Theorem ==
Let $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$ be algebraic structures with identities $e_1, e_2$ respectively.
The canonical injections:
:$\inj_1: \struct {S_1, \circ_1} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}: \forall x \in S_1: \map {\inj_1} x = \tuple {x, e_2}$
:$\inj_2: \struct {S_2, \circ_2} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}: \forall x \in S_2: \map {\inj_2} x = \tuple {e_1, x}$
are injections.
=== General Result ===
== Proof ==
Let $x, x' \in S_1$.
Suppose that:
:$\map {\inj_1} x = \map {\inj_1} {x'}$
Then by definition of canonical injection:
:$\tuple {x, e_2} = \tuple {x', e_2}$
By Equality of Ordered Pairs:
:$x = x'$
That is, $\inj_1$ is an injection.
Similarly, let $x, x' \in S_2$.
Suppose that:
:$\map {\inj_2} x = \map {\inj_2} {x'}$
Then by definition of canonical injection:
:$\tuple {e_1, x} = \tuple {e_1, x'}$
Again by Equality of Ordered Pairs:
:$x = x'$
That is, $\inj_2$ is an injection.
So $\inj_1$ and $\inj_2$ are injections.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 13$: Compositions Induced on Cartesian Products and Function Spaces: Theorem $13.3$
* : Chapter $\text {II}$: New Structures from Old: $\S 13$: Compositions Induced on Cartesian Products and Function Spaces: Exercise $13.3$
Category:Canonical Injections
Canonical Injection is Injection/General Result

== Theorem ==
Let $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \dotsc, \struct {S_j, \circ_j}, \dotsc, \struct {S_n, \circ_n}$ be algebraic structures with identities $e_1, e_2, \ldots, e_j, \ldots, e_n$ respectively.
The canonical injection:
:$\ds \inj_j: \struct {S_j, \circ_j} \to \prod_{i \mathop = 1}^n \struct {S_i, \circ_i}$
defined as:
:$\map {\inj_j} x = \tuple {e_1, e_2, \dotsc, e_{j - 1}, x, e_{j + 1}, \dotsc, e_n}$
is an injection.
== Proof ==
Let:
:$x, y \in S_j: \map {\inj_j} x = \map {\inj_j} y$
Then:
:$\tuple {e_1, e_2, \dotsc, e_{j - 1}, x, e_{j + 1}, \dotsc, e_n} = \tuple {e_1, e_2, \dotsc, e_{j - 1}, y, e_{j + 1}, \dotsc, e_n}$
By Equality of Ordered Tuples, it follows directly that:
:$x = y$
Thus the canonical injections are injective.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 18$: Induced $N$-ary Operations
Category:Canonical Injections
Canonical Injection is Monomorphism

== Theorem ==
Let $\struct {S_1, \circ_1}$ and $\struct {S_2, \circ_2}$ be algebraic structures with identities $e_1, e_2$ respectively.
The canonical injections:
:$\inj_1: \struct {S_1, \circ_1} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}: \forall x \in S_1: \map {\inj_1} x = \tuple {x, e_2}$
:$\inj_2: \struct {S_2, \circ_2} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}: \forall x \in S_2: \map {\inj_2} x = \tuple {e_1, x}$
are monomorphisms.
=== General Result ===
== Proof ==
From Canonical Injection is Injection we have that the canonical injections are in fact injective.
It remains to prove the morphism property.
Let $x, y \in \struct {S_1, \circ_1}$.
Then:
and the morphism property has been demonstrated to hold for $\inj_1$.
Thus $\inj_1: \struct {S_1, \circ_1} \to \struct {S_1, \circ_1} \times \struct {S_2, \circ_2}$ has been shown to be an injective homomorphism and therefore a monomorphism.
The same argument applies to $\inj_2$.
== Sources ==
* : Chapter $\text {II}$: New Structures from Old: $\S 13$: Compositions Induced on Cartesian Products and Function Spaces: Theorem $13.3$
* : Chapter $\text {II}$: New Structures from Old: $\S 13$: Compositions Induced on Cartesian Products and Function Spaces: Exercise $13.3$
Category:Canonical Injection is Monomorphism
Category:Canonical Injections
Category:Monomorphisms (Abstract Algebra)
Canonical Injection is Monomorphism/General Result

== Theorem ==
Let $\struct {S_1, \circ_1}, \struct {S_2, \circ_2}, \dotsc, \struct {S_j, \circ_j}, \dotsc, \struct {S_n, \circ_n}$ be algebraic structures with identities $e_1, e_2, \dotsc, e_j, \dotsc, e_n$ respectively.
Then the canonical injection:
:$\ds \inj_j: \struct {S_j, \circ_j} \to \prod_{i \mathop = 1}^n \struct {S_i, \circ_i}$
defined as:
:$\map {\inj_j} x = \tuple {e_1, e_2, \dotsc, e_{j - 1}, x, e_{j + 1}, \dotsc, e_n}$
is a monomorphism.
== Proof ==
From Canonical Injection is Injection we have that the canonical injections are in fact injective.
It remains to prove the morphism property.
Let $x, y \in \struct {S_j, \circ_j}$.
Then:
and the morphism property has been demonstrated to hold.
Thus $\ds \inj_j: \struct {S_j, \circ_j} \to \prod_{i \mathop = 1}^n \struct {S_i, \circ_i}$ has been shown to be an injective homomorphism and therefore a monomorphism.
== Sources ==
* : Chapter $\text {III}$: The Natural Numbers: $\S 18$: Induced $N$-ary Operations: Theorem $18.12$
Category:Canonical Injection is Monomorphism
Canonical Injection is Right Inverse of Projection

== Theorem ==
Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups with identity elements $e_1$ and $e_2$ respectively.
Let $\struct {G_1 \times G_2, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$
Let:
:$\pr_1: \struct {G_1 \times G_2, \circ} \to \struct {G_1, \circ_1}$ be the first projection from $\struct {G_1 \times G_2, \circ}$ to $\struct {G_1, \circ_1}$
:$\pr_2: \struct {G_1 \times G_2, \circ} \to \struct {G_2, \circ_2}$ be the second projection from $\struct {G_1 \times G_2, \circ}$ to $\struct {G_2, \circ_2}$.
Let:
:$\inj_1: \struct {G_1, \circ_1} \to \struct {G_1 \times G_2, \circ}$ be the canonical injection from $\struct {G_1, \circ_1}$ to $\struct {G_1 \times G_2, \circ}$
:$\inj_2: \struct {G_2, \circ_2} \to \struct {G_1 \times G_2, \circ}$ be the canonical injection from $\struct {G_2, \circ_2}$ to $\struct {G_1 \times G_2, \circ}$.
Then:
:$(1): \quad \pr_1 \circ \inj_1 = I_{G_1}$
:$(2): \quad \pr_2 \circ \inj_2 = I_{G_2}$
where $I_{G_1}$ and $I_{G_2}$ are the identity mappings on $G_1$ and $G_2$ respectively.
== Proof ==
This is a specific instance of External Direct Product of Projection with Canonical Injection, where the algebraic structures in question are groups.
== Sources ==
* : Chapter $\text{II}$: Groups: Direct Products
Category:Group Homomorphisms
Category:Group Direct Products
Canonical Injection of Real Number Line into Complex Plane

== Theorem ==
Let $\struct {\C, +}$ be the additive group of complex numbers.
Let $\struct {\R, +}$ be the additive group of real numbers.
Let $f: \R \to \C$ be the mapping from the real numbers to the complex numbers defined as:
:$\forall x \in \R: \map f z = x + 0 y$
Then $f: \struct {\R, +} \to \struct {\C, +}$ is a monomorphism.
== Proof ==
Consider the mapping $g: \C \to \R$ defined as:
:$\forall z \in \C: \map f z = \map \Re z$
where $\map \Re z$ denotes the real part of $z$.
From Real Part as Mapping is Endomorphism for Complex Addition, this is a projection from $\C$ to $\R$.
The result follows from Canonical Injection is Right Inverse of Projection.
== Sources ==
* : Chapter $\text{II}$: Groups: Direct Products
Category:Real Numbers
Category:Complex Numbers
Category:Group Direct Products
Canonical Injection on Group Direct Product is Monomorphism

== Theorem ==
Let $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$ be groups with identities $e_1, e_2$ respectively.
Let $\struct {G_1 \times G_2, \circ}$ be the group direct product of $\struct {G_1, \circ_1}$ and $\struct {G_2, \circ_2}$
Then the canonical injections:
:$\inj_1: \struct {G_1, \circ_1} \to \struct {G_1, \circ_1} \times \struct {G_2, \circ_2}: \forall x \in G_1: \map {\inj_1} x = \tuple {x, e_2}$
:$\inj_2: \struct {G_2, \circ_2} \to \struct {G_1, \circ_1} \times \struct {G_2, \circ_2}: \forall x \in G_2: \map {\inj_2} x = \tuple {e_1, x}$
are group monomorphisms.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : Chapter $\text{II}$: Groups: Direct Products
Category:Group Monomorphisms
Category:Group Direct Products
Category:Canonical Injection on Group Direct Product is Monomorphism
Canonical Injection on Group Direct Product is Monomorphism/Proof 1

== Theorem ==
== Proof ==
From Canonical Injection is Injection we have that the canonical injections are in fact injective.
It remains to prove the morphism property.
Let $x, y \in G_1$.
Then:
and the morphism property has been demonstrated to hold for $\inj_1$.
Thus $\inj_1: \struct {G_1, \circ_1} \to \struct {G_1, \circ_1} \times \struct {G_2, \circ_2}$ has been shown to be an injective group homomorphism and therefore a group monomorphism.
The same argument applies to $\inj_2$.
Category:Canonical Injection on Group Direct Product is Monomorphism
Canonical Mapping of Locale to Powerset of Points is Frame Homomorphism

== Theorem ==
Let $\struct{L, \preceq}$ be a locale.
Let $\map {\operatorname{pt}} L$ denote the points of $L$ as completely prime filters.
For each $a \in L$, let:
:$\Sigma_a = \set{p \in \map {\operatorname{pt}} L : a \in p}$
Let $\Sigma : L \to \powerset {\map {\operatorname{pt}} L}$ be the mapping defined by:
:$\forall a \in L : \map \Sigma a = \Sigma_a$
where $\powerset {\map {\operatorname{pt}} L}$ denotes the powerset of $\map {\operatorname{pt}} L$.
Then:
:$\Sigma: \struct{L, \preceq} \to \struct{\powerset {\map {\operatorname{pt}} L}, \subseteq}$ is a frame homomorphism.
== Proof ==
=== $\Sigma$ Preserves Arbitrary Supremums ===
Let $\set{a_i : i \in I}$ be an indexed family of elements of $L$.
Let $\ds \bigvee_{i \in I} a_i$ denote the supremum of $\set{a_i : i \in I}$.
We have:
By definition of set Equlity:
:$\ds \map \Sigma {\bigvee_{i \in I} a_i} = \bigcup_{i \in I} \map \Sigma {a_i}$
It follows that $\Sigma$ is arbitrary join preserving by definition. 
=== $\Sigma$ Preserves Finite Infimums ===
Let $\set{a_i : i \in I}$ be an indexed family of elements of $L$ where the indexing set $I$ finite.
Let $\ds \bigwedge_{i \in I} a_i$ denote the infimum of $\set{a_i : i \in I}$.
We have:
By definition of set Equlity:
:$\ds \map \Sigma {\bigwedge_{i \in I} a_i} = \bigcap_{i \in I} \map \Sigma {a_i}$
It follows that $\Sigma$ is finite meet preserving by definition. 
It has been shown that $\Sigma$ is both arbitrary join preserving and finite meet preserving and so is a frame homomorphism by definition.
== Sources ==
* : Chapter $\text {II}$: Introduction to locales, $\S 1$ Frames and locales, Lemma $1.3$
Category:Spectra of Locales
Canonical Order Well-Orders Ordered Pairs of Ordinals

== Theorem ==
The canonical order, $R_0$ strictly well-orders the ordered pairs of ordinal numbers.
== Proof ==
=== Strict Ordering ===
Let $\tuple {x, y} \mathrel {R_0} \tuple {x, y}$.
Then:
:$\map \max {x, y} < \map \max {x, y} \lor \tuple {x, y} \mathrel {\operatorname {Le} } \tuple {x, y}$
Both lead to contradictions, so:
:$\neg \tuple {x, y} \mathrel {R_0} \tuple {x, y}$
and $R_0$ is antireflexive.
Let:
:$(1): \quad \tuple {\alpha, \beta} \mathrel {R_0} \tuple {\gamma, \delta}$
and:
:$(2): \quad \tuple {\gamma, \delta} \mathrel {R_0} \tuple {\epsilon, \zeta}$
There are two cases:
:$\map \max {\alpha, \beta} < \map \max {\gamma, \delta}$
or:
:$\map \max {\alpha, \beta} = \map \max {\gamma, \delta}$
In either case:
:$\tuple {\alpha, \beta} \mathrel {R_0} \tuple {\epsilon, \zeta}$
and $R_0$ is transitive.
=== Strict Total Ordering ===
Suppose:
:$\neg \tuple {\alpha, \beta} \mathrel {R_0} \tuple {\gamma, \delta}$
and:
:$\neg \tuple {\gamma, \delta} \mathrel {R_0} \tuple {\alpha, \beta}$
Then:
:$\map \max {\alpha, \beta} \le \map \max {\gamma, \delta}$
and:
:$\map \max {\gamma, \delta} \le \map \max {\alpha, \beta}$
So:
:$\map \max {\alpha, \beta} = \map \max {\gamma, \delta}$
Therefore:
:$\neg \tuple {\alpha, \beta} \mathrel {\operatorname {Le} } \tuple {\gamma, \delta}$
and:
:$\neg \tuple {\gamma, \delta} \mathrel {\operatorname {Le} } \tuple {\alpha, \beta}$
From Lexicographic Order forms Well-Ordering on Ordered Pairs of Ordinals:
:$\tuple {\alpha, \beta} = \tuple {\gamma, \delta}$
=== Well-Ordering ===
Take any nonempty subset $A$ of $\paren {\On \times \On}$.
We shall allow $A$ to be any class.
This isn't strictly necessary, but it will not alter the proof.
The $\max$ mapping sends each element in $A$ to an element of $\On$.
Therefor the image of $\max$ has a minimal element, $N$.
Take $B$ to be the class of all ordered pairs $\tuple {x, y}$, such that $\map \max {x, y} = N$.
Let the $\operatorname {Le}$-minimal element of $B$ be denoted $C$.
Then:
:$\map \max C = N$
and $C$ is seen to be $\operatorname {Le}$-minimal.
Therefore $C$ is the $R_0$-minimal element of $A$.
== Sources ==
* : $\S 7.56 \ (1)$
Category:Ordinals
Category:Well-Orderings
Canonical P-adic Expansion of Rational is Eventually Periodic

== Theorem ==
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $x \in \Q_p$.
Then:
:$x$ is a rational number the canonical expansion of $x$ is eventually periodic.
== Proof ==
=== Necessary Condition ===
Let $x$ be a rational number.
=== Sufficient Condition ===
== Sources ==
* : $\S 1.6$ The $p$-adic expansion of rational numbers: Theorem $1.38$
Category:P-adic Number Theory
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 1

== Theorem ==
Let $p$ be a prime number.
Let $b \in \Z_{>0}$ such that $b$ and $p$ are coprime.
Let $a \in \Z$.
Then:
:$\forall n \in \N: \exists r_n \in \Z : \dfrac a b - \paren{p^{n + 1} \dfrac {r_n} b} \in \set{0, 1, \ldots, p^{n + 1} - 1}$
== Proof ==
Let $n \in \N$.
From Integer Coprime to all Factors is Coprime to Whole:
:$b, p^{n + 1}$ are coprime
From Integer Combination of Coprime Integers:
:$\exists c_n, d_n \in \Z : c_n b + d_n p^{n + 1} = 1$
Multiplying both sides by $a$:
:$a = a c_n b + a d_n p^{n + 1}$
Let $A_n$ be the least positive residue of $a c_n \pmod {p^{n + 1} }$.
By definition of least positive residue:
:$0 \le A_n \le p^{n + 1} - 1$
:$p^{n + 1} \divides \paren{a c_n - A_n}$
By definition of divisor: 
:$\exists x_n \in \Z : x_n p^{n + 1} = a c_n - A_n$
Re-arranging terms:
:$a c_n = x_n p^{n + 1} + A_n$
We have:
Let $r_n = b x_n + a d_n$.
Then:
By definition of least positive residue:
:$A_n \in \set{0, 1, \ldots, p^{n + 1} - 1}$
The result follows.
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 10

== Theorem ==
Let $p$ be a prime.
Let $b \in Z_{>0}$ be a (strictly) positive integer such that $b, p$ are coprime.
Let $\sequence {d_n}$ be a sequence of $p$-adic digits.
Let $\sequence {r_n}$ be an integer sequence such that:
Let: 
:$n, k \in \N : k > 0 : r_n = r_{n + k}$
Then:
:$d_{n + 1} = d_{n + k + 1}$
:$r_{n + 1} = r_{n + k + 1}$
== Proof ==
We have:
As $b, p$ are coprime:
:$p \nmid b$
From Euclid's Lemma:
:$p \divides \paren {d_{n + 1} - d_{n + k + 1} }$
By definition of $p$-adic digits:
:$d_{n + 1}, d_{n + k + 1} \in \set {0, 1, \ldots, p - 1}$
Hence:
:$d_{n + 1} = d_{n + k + 1}$
We have:
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 11

== Theorem ==
Let $p$ be a prime number.
Let $a \in \Z, b \in Z_{> 0}$
Let:
:$\forall n \in \N: \exists r_n \in \Z : \dfrac a b - \paren{p^{n + 1} \dfrac {r_n} b} \in \set{0, 1, \ldots, p^{n + 1} - 1}$
Then:
:$\forall n \in \N : \dfrac {a - \paren {p^{n + 1} - 1} b } {p^{n + 1} } \le r_n \le \dfrac a {p^{n + 1} }$
== Proof ==
We have:
The result follows.
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 2

== Theorem ==
Let $p$ be a prime number.
Let $a \in \Z, b \in Z_{> 0}$
Let:
:$\forall n \in \N: \exists r_n \in \Z : \dfrac a b - \paren{p^{n + 1} \dfrac {r_n} b} \in \set{0, 1, \ldots, p^{n + 1} - 1}$
Then:
:$\exists n_0 \in \N : \forall n \ge n_0 : -b \le r_n \le 0$
== Proof ==
=== Lemma 11 ===
=== Lemma 8 ===
In the real numbers $\R$:
By definition of convergence:
:$\exists n_1 \in \N: \forall n \ge n_1 : - \dfrac 1 2 < \dfrac a {p^{n+1}} < \dfrac 1 2$
=== Lemma 9 ===
In the real numbers $\R$:
By definition of convergence:
:$\exists n_2 \in \N: \forall n \ge n_2 : -b - \dfrac 1 2 < \dfrac {a - \paren{p^{n+1} - 1} b } {p^{n+1}} < -b + \dfrac 1 2$
Let:
:$n_0 = \max \set{n_1, n_2}$
Then:
:$\forall n \ge n_0 : -b - \dfrac 1 2 < \dfrac {a - \paren{p^{n+1} - 1} b } {p^{n+1}} \le r_n \le \dfrac a {p^{n+1}} < \dfrac 1 2$
By hypothesis:
:$b \in \Z$ and $\forall n \in \N: r_n \in \Z$
Hence:
:$\forall n \ge n_0 : -b \le r_n \le 0$
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 3

== Theorem ==
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let:
:$a \in \Z, b \in Z_{> 0}$
Let:
:$\forall n \in \N: \exists A_n, r_n \in \Z$:
::$(\text a) \quad \dfrac a b = A_n + p^{n+1} \dfrac {r_n} b$
::$(\text b) \quad \exists n_0 \in \N : \forall n \ge n_0 : -b \le r_n \le 0$
Then:
:$\ds \lim_{n \mathop \to \infty} A_n = \dfrac a b$
== Proof ==
Let $\epsilon \in \R_{> 0}$.
Let $M = \max \set {\norm{r_0}_p, \norm{r_1}_p, \ldots, \norm{r_{n_0}}_p, \norm{-1}_p, \norm{-2}_p, \ldots, \norm{-b}_p}$
From Power Function is Unbounded Above:
:$\exists N \in \N: p^{N+1} > \dfrac M {\epsilon \norm b_p}$
We have:
By definition of convergence in $\struct {\Q_p, \norm {\,\cdot\,}_p}$:
:$\ds \lim_{n \mathop \to \infty} A_n = \dfrac a b$
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 4

== Theorem ==
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $y $ be a rational $p$-adic integer.
Let $\ldots d_n \ldots d_2 d_1 d_0$ be the canonical expansion of $y$.
Let:
:$y = \dfrac a b : a \in \Z, b \in Z_{> 0}$
Let:
:$\forall n \in \N: \exists A_n, r_n \in \Z$:
::$(\text a) \quad \dfrac a b = A_n + p^{n + 1} \dfrac {r_n} b$
::$(\text b) \quad 0 \le A_n \le p^{n + 1} - 1$
::$(\text c) \quad \ds \lim_{n \mathop \to \infty} A_n = \dfrac a b$
Then:
:$\forall n \in \N: r_n = d_{n + 1} b + p r_{n + 1}$
== Proof ==
We have:
From Characterization of Rational P-adic Integer:
:$p \nmid b$
From Prime not Divisor implies Coprime:
:$b, p$ are coprime
From Integer Coprime to all Factors is Coprime to Whole:
:$b, p^{n+1}$ are coprime
Hence:
$b \nmid p^{n + 1}$
From Euclid's Lemma:
:$b \divides \paren {r_n - p r_{n + 1} }$
Then:
:$\dfrac {r_n - p r_{n + 1} } b \in \Z$
Hence:
:$A_{n + 1} \equiv A_n \pmod {p^{n + 1} }$
By definition of coherent sequence:
:the sequence $\sequence{A_n}$ is a coherent sequence
From Coherent Sequence is Partial Sum of P-adic Expansion:
:the sequence $\sequence{A_n}$ is the sequence of partial sums of a $p$-adic expansion $\ds \sum_{i \mathop = 0}^n e_i p^i$
Hence:
:$y = \dfrac a b = \ds \sum_{n \mathop = 0}^\infty e_n p^n$
From P-adic Number is Limit of Unique P-adic Expansion:
:$\forall n \in \N: e_n = d_n$
By definition of partial sums:
:$\forall n \in \N: A_{n + 1} = A_n + d_{n + 1} p^{n + 1}$
Hence:
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 5

== Theorem ==
Let $p$ be a prime.
Let $b \in Z_{>0}$ such that $b, p$ are coprime.
Let $\sequence {d_n}$ be a sequence of $p$-adic digits.
Let $\sequence {r_n}$ be an integer sequence such that:
Then:
:$\exists \mathop m, l \in \N : \forall n \ge m: r_n = r_{n + l}$ and $d_n = d_{n + l}$
== Proof ==
We have that the set $\set {r_n : n \in \N}$ of values of $\sequence {r_n}$ is a subset of:
:$\set {r_0, r_1, \ldots, r_{n_0} } \cup \set {-b, -b + 1, -b + 2, \ldots, 2, 1, 0}$
It follows that $\set {r_n : n \in \N}$ takes only finitely many values.
Hence:
:$\exists m_0, l \in \N : l > 0 : r_{m_0} = r_{ {m_0} + l}$
=== Lemma 10 ===
Let $m = m_0 + 1$
The proof now proceeds by induction.
For all $n \ge m$, let $\map P n$ be the proposition:
:$r_n = r_{n + l}$ and $d_n = d_{n + l}$
=== Basis for the Induction ===
$\map P m$ is the proposition:
:$r_m = r_{m + l}$ and $d_m = d_{m + l}$
We have that:
:$r_{m_0} = r_{ {m_0} + l}$
From lemma $10$:
:$d_m = d_{m + l}$
:$r_m = r_{m + l}$
This proves proposition $\map P m$.
This is the basis for the induction.
=== Induction Hypothesis ===
Let $n \ge m$.
The induction hypothesis is the proposition $\map P {n}$:
:$r_n = r_{n+l}$ and $d_n = d_{n + l}$
It has to be shown that the proposition $\map P {n+1}$ is true:
:$r_{n + 1} = r_{n + l + 1}$ and $d_{n + 1} = d_{n + l + 1}$
=== Induction Step ===
From the induction hypothesis:
:$r_n = r_{n + l}$
From lemma $10$:
:$d_{n + 1} = d_{n + l + 1}$
:$r_{n + 1} = r_{n + l + 1}$
Hence:
:$\forall n \ge m: r_n = r_{n + l}$ and $d_n = d_{n + l}$
The result follows.
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 6

== Theorem ==
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Let $x \in \Q_p$.
Let the canonical expansion of $x$ be eventually periodic.
Then:
:$\exists r \in \Q, n \in \Z, y \in \Z_p$:
::$(1) \quad x = r + p^n y$
::$(2) \quad$ the canonical expansion of $y$ is periodic.
== Proof ==
Let $\ldots d_i \ldots d_2 d_1 d_0 . d_{-1} d_{-2} \ldots d_{-m}$ be the canonical expansion of $x$.
By definition of eventually periodic there exists a finite sequence of $k$ digits of $x$:
:$\tuple {d_{n + k - 1} \ldots d_{n + 1} d_n }$
such that $n \ge 0$ and for all $s \in \Z_{\ge 0}$ and for all $j \in \set {0, 2, \ldots, k - 1}$:
:$d_{n + j + s k} = d_{n + j}$
where $k$ is the smallest $k$ to have this property.
We have:
Let:
:$\ds r = \begin{cases}
0 & : -m = n \\
\ds \sum_{i \mathop = -m}^{n - 1} d_i p^i & : -m < n 
\end{cases}$
:$\ds y = \sum_{i \mathop = n}^\infty d_i p^{i - n}$
Then:
:$x = r + p^n y$
We have that:
:$r \in \Q$
Re-indexing the series for $y$, we have:
:$\ds y = \sum_{i \mathop = 0}^\infty d_{i + n} p^i$
By definition of $p$-adic integer:
:$y \in \Z_p$
By definition of canonical expansion, the canonical expansion of $y$ is:
:$\ldots d_{n + i} \ldots d_{n + 2} d_{n + 1} d_n$
Recall that for all $s \in \Z_{\ge 0}$ and for all $j \in \set {0, 2, \ldots, k - 1}$:
:$d_{n + j + s k} = d_{n + j}$
By definition of periodic:
:the canonical expansion of $y$ is periodic
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 7

== Theorem ==
Let $\struct {\Q_p, \norm {\,\cdot\,}_p}$ be the $p$-adic numbers for some prime $p$.
Then:
:$1 + p^k + p^{2 k} + p^{3 k} + \cdots = \dfrac 1 {1 - p^k}$
== Proof ==
Let $S_n$ be the partial sum:
:$\ds S_n = \sum_{j \mathop = 0}^n p^{j k}$
We have:
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 8

== Theorem ==
Let $p$ be a prime number.
Let $a \in \Z$
Then:
:$\ds \lim_{n \mathop \to \infty} \dfrac a {p^{n+1}} = 0$
== Proof ==
From Sequence of Powers of Rational Number less than One:
:$\ds \lim_{n \mathop \to \infty} \dfrac 1 {p^n} = 0$
From Multiple Rule for Sequences:
:$\ds \lim_{n \mathop \to \infty} \dfrac a p \cdot \paren{\dfrac 1 {p^n} } = \dfrac a p \cdot 0 = 0$
The result follows.
Category:Canonical P-adic Expansion of Rational is Eventually Periodic
Canonical P-adic Expansion of Rational is Eventually Periodic/Lemma 9

== Theorem ==
Let $p$ be a prime number.
Let $a \in \Z, b \in Z_{> 0}$
Then:
:$\ds \lim_{n \mathop \to \infty} \dfrac {a - \paren{p^{n+1} - 1} b } {p^{n+1}} = -b$
== Proof ==
From Sequence of Reciprocals is Null Sequence:
:$\ds \lim_{n \mathop \to \infty} \dfrac 1 n = 0$
From Combined Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \dfrac {n - 1} n = \lim_{n \mathop \to \infty} 1 - \dfrac 1 n = 1$ 
From Limit of Subsequence equals Limit of Real Sequence:
:$\ds \lim_{n \mathop \to \infty} \dfrac {p^{n + 1} - 1} {p^{n + 1} } = 1$
=== Lemma 8 ===
In the real numbers $\R$:
From Combined Sum Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} \dfrac a {p^{n + 1} } - b \paren {\dfrac {p^{n + 1} - 1} {p^{n + 1} } } = -b$
The result follows.
Category:Canonical P-adic Expansion of Rational is Eventually Periodic