avewright/proofwiki-math huggingface dataset:
Theorem: Construction of Lattice Point in Cartesian Plane

Let $\CC$ be a Cartesian plane.
Let $P = \tuple {a, b}$ be a lattice point in $\CC$.
Then $P$ is constructible using a compass and straightedge construction.

Proof:
Let $O$ denote the point $\tuple {0, 0}$.
Let $A$ denote the point $\tuple {1, 0}$.
The $x$-axis is identified with the straight line through $O$ and $A$.
The $y$-axis is constructed as the line perpendicular to $OA$ through $O$.
From Construction of Integer Multiple of Line Segment, the point $\tuple {a, 0}$ is constructed.
Drawing a circle whose center is at $O$ and whose radius is $OA$ the point $A'$ is constructed on the $y$-axis where $OA' = OA$.
Thus $A'$ is the point $\tuple {0, 1}$.
From Construction of Integer Multiple of Line Segment, the point $\tuple {0, b}$ is constructed.
Using Construction of Parallel Line, a straight line is drawn through $\tuple {a, 0}$ parallel to the $y$-axis.
Using Construction of Parallel Line, a straight line is drawn through $\tuple {0, b}$ parallel to the $x$-axis.
By definition of Cartesian plane, their intersection is at $\tuple {a, b}$, which is the required point $P$.
{{qed}}
Theorem: Even Integers do not form Integral Domain

Let $2 \Z$ be the set of even integers.
Then $\struct {2 \Z, +, \times}$ is not an integral domain.

Proof:
From Integer Multiples form Commutative Ring, $\struct {2 \Z, +, \times}$ is a commutative ring.
As $2 \ne 1$, we also have from Integer Multiples form Commutative Ring that $\struct {2 \Z, +, \times}$ has no unity.
Hence by definition it is not an integral domain.
{{qed}}
Theorem: Rational Numbers with Denominator Power of Two form Integral Domain

Let $\Q$ denote the set of rational numbers.
Let $S \subseteq \Q$ denote the set of set of rational numbers of the form $\dfrac p q$ where $q$ is a power of $2$:
:$S = \set {\dfrac p q: p \in \Z, q \in \set {2^m: m \in \Z_{\ge 0} } }$
Then $\struct {S, +, \times}$ is an integral domain.

Proof:
From Rational Numbers form Integral Domain we have that $\struct {\Q, +, \times}$ is an integral domain.
Hence to demonstrate that $\struct {S, +, \times}$ is an integral domain, we can use the Subdomain Test.
We have that the unity of $\struct {\Q, +, \times}$ is $1$.
Then we note:
:$1 = \dfrac 1 1$
and:
:$1 = 2^0$
and so $1 \in S$.
Thus property $(2)$ of the Subdomain Test is fulfilled.
It remains to demonstrate that $\struct {S, +, \times}$ is a subring of $\struct {\Q, +, \times}$, so fulfilling property $(2)$ of the Subdomain Test.
Hence we use the Subring Test.
We note that $S \ne \O$ as $1 \in S$.
This fulfils property $(1)$ of the Subring Test.
Let $x, y \in S$.
Then:
{{begin-eqn}}
{{eqn | l = x + \paren {-y}
      | r = \dfrac a {2^p} + \dfrac b {2^q}
      | c = for some $a, b \in \Z$ and $p, q \in \Z_{\ge 0}$
}}
{{eqn | r = \dfrac {a 2^q - b 2^p} {2^p 2^q}
      | c = {{Defof|Rational Addition}}
}}
{{eqn | r = \dfrac {a 2^q - b 2^p} {2^{p + q} }
      | c = 
}}
{{eqn | o = \in
      | r = S
      | c = 
}}
{{end-eqn}}
This fulfils property $(2)$ of the Subring Test.
Then: 
{{begin-eqn}}
{{eqn | l = x \times y
      | r = \dfrac a {2^p} \times \dfrac b {2^q}
      | c = for some $a, b \in \Z$ and $p, q \in \Z_{\ge 0}$
}}
{{eqn | r = \dfrac {a b} {2^p 2^q}
      | c = {{Defof|Rational Multiplication}}
}}
{{eqn | r = \dfrac {a b} {2^{p + q} }
      | c = 
}}
{{eqn | o = \in
      | r = S
      | c = 
}}
{{end-eqn}}
This fulfils property $(3)$ of the Subring Test.
Hence the result.
{{qed}}
Theorem: Quadratic Integers over 3 form Integral Domain

Let $\R$ denote the set of real numbers.
Let $\Z \sqbrk {\sqrt 3} \subseteq \R$ denote the  set of quadratic integers over $3$:
:$\Z \sqbrk {\sqrt 3} = \set {a + b \sqrt 3: a, b \in \Z}$
Then $\struct {\Z \sqbrk {\sqrt 3}, +, \times}$ is an integral domain.

Proof:
From Real Numbers form Integral Domain we have that $\struct {\R, +, \times}$ is an integral domain.
Hence to demonstrate that $\struct {\Z \sqbrk {\sqrt 3}, +, \times}$ is an integral domain, we can use the Subdomain Test.
We have that the unity of $\struct {\R, +, \times}$ is $1$.
Then we note:
:$1 = 1 + 0 \times \sqrt 3$
and so $1 \in S$.
Thus property $(2)$ of the Subdomain Test is fulfilled.
It remains to demonstrate that $\struct {\Z \sqbrk {\sqrt 3}, +, \times}$ is a subring of $\struct {\R, +, \times}$, so fulfilling property $(2)$ of the Subdomain Test.
Hence we use the Subring Test.
We note that $\Z \sqbrk {\sqrt 3} \ne \O$ as $1 \in \Z \sqbrk {\sqrt 3}$.
This fulfils property $(1)$ of the Subring Test.
Let $x, y \in \Z \sqbrk {\sqrt 3}$ such that:
:$x = a + b \sqrt 3$
:$y = c + d \sqrt 3$
Then:
{{begin-eqn}}
{{eqn | l = x + \paren {-y}
      | r = \paren {a + b \sqrt 3} - \paren {c + d \sqrt 3}
      | c = 
}}
{{eqn | r = \paren {a - c} + \paren {b \sqrt 3 - d \sqrt 3}
      | c = {{Defof|Real Addition}}
}}
{{eqn | r = \paren {a - c} + \paren {b - d} \sqrt 3
      | c = 
}}
{{eqn | o = \in
      | r = \Z \sqbrk {\sqrt 3}
      | c = 
}}
{{end-eqn}}
This fulfils property $(2)$ of the Subring Test.
Then: 
{{begin-eqn}}
{{eqn | l = x \times y
      | r = \paren {a + b \sqrt 3} \paren {c + d \sqrt 3}
      | c = 
}}
{{eqn | r = a c + a d \sqrt 3 + b c \sqrt 3 + 3 b d
      | c = {{Defof|Real Multiplication}}
}}
{{eqn | r = \paren {a c + 3 b d} + \paren {a d + b c} \sqrt 3
      | c = 
}}
{{eqn | o = \in
      | r = \Z \sqbrk {\sqrt 3}
      | c = 
}}
{{end-eqn}}
This fulfils property $(3)$ of the Subring Test.
Hence the result.
{{qed}}
Theorem: Normal Subgroup of Order 25 in Group of Order 100

Let $G$ be a group of order $100$.
Then $G$ has a normal subgroup of order $25$.

Proof:
Let $r$ be the number of Sylow $p$-subgroup of order $5^2 = 25$
The First Sylow Theorem guarantees existence, so $r \ge 1$.
From the Fourth Sylow Theorem:
:$r \equiv 1 \pmod 5$
That is:
:$r \in \set {1, 6, 11, 16, \ldots}$
From the Fifth Sylow Theorem:
:$r \divides \dfrac {100} {25} = 4$
from which it follows that $r = 1$.
From Sylow p-Subgroup is Unique iff Normal, this unique Sylow $5$-subgroup must be normal.
{{qed}}
Theorem: Normal p-Subgroup contained in All Sylow p-Subgroups

Let $G$ be a finite group.
Let $p$ be a prime number.
Let $H$ be a normal subgroup of $G$ which is a $p$-group.
Then $H$ is a subset of every Sylow $p$-subgroup of $G$.

Proof:
Let $P$ be a Sylow $p$-subgroup of $G$.
By Second Sylow Theorem, $H$ is a subset of a conjugate of $P$.
Then:
:$\exists g \in G: H \subseteq g P g^{-1}$.
This implies:
{{begin-eqn}}
{{eqn | l = H
      | r = g^{-1} H g
      | c = Subgroup equals Conjugate iff Normal
}}
{{eqn | o = \subseteq
      | r = g^{-1} \paren {g P g^{-1} } g
      | c = Subset Relation is Compatible with Subset Product/Corollary 2
}}
{{eqn | r = P
}}
{{end-eqn}}
Since $P$ is arbitrary, $H$ is a subset of every Sylow $p$-subgroup of $G$.
{{qed}}
Theorem: Existence of Subgroup whose Index is Prime Power

Let $G$ be a finite group.
Let $H$ be a normal subgroup of $G$ which has a finite index in $G$.
Let:
:$p^k \divides \index G H$
where:
:$p$ is a prime number
:$k \in \Z_{>0}$ is a (strictly) positive integer
:$\divides$ denotes divisibility.
Then $G$ contains a subgroup $K$ such that:
:$\index K H = p^k$

Proof:
The order $\order {G / H}$ of the quotient group $G / H$ is $\index G H$.
Hence $p^k$ divides $\order {G / H}$.
By Group has Subgroups of All Prime Power Factors, $G / H$ has a subgroup of order $p^k$.
By Correspondence Theorem, this subgroup is in the form $K / H$ where $H \le K \le G$.
Hence the result.
{{qed}}
Theorem: Group of Order p^2 q is not Simple

Let $p$ and $q$ be prime numbers such that $p \ne q$.
Let $G$ be a group of order $p^2 q$.
Then $G$ is not simple.

Proof:
From Group of Order $p^2 q$ has Normal Sylow $p$-Subgroup, $G$ has a normal subgroup of order $p^2$.
Hence the result, by definition of simple group.
{{qed}}
Theorem: Simple Group of Order Less than 60 is Prime

Let $G$ be a simple group.
Let $\order G < 60$, where $\order G$ denotes the order of $G$.
Then $G$ is a prime group.

Proof:
First it is noted that Prime Group is Simple.
We also note from Alternating Group is Simple except on 4 Letters that the alternating group $A_5$, which is of order $60$, is simple.
Hence the motivation for the result.
It remains to be shown that all groups of composite order such that $\order G < 60$ are not simple.
Let $S$ be the set:
:$S = \set {n \in \Z: 0 < n < 60: \text { there exists a simple group of order $n$ such that $n$ is composite} }$
The aim is to show that $S$ is empty.
From Abelian Group is Simple iff Prime, all abelian groups of composite order are not simple.
Thus any simple group must be non-abelian.
Let $p$ and $q$ be prime.
From Prime Power Group has Non-Trivial Proper Normal Subgroup, no group of order $p^n$ is simple.
Thus:
:$\forall n \in \Z_{>0}: p^n \notin S$
Thus, with the primes and prime powers eliminated, we have:
:$S \subseteq \set {6, 10, 12, 14, 15, 18, 20, 21, 22, 24, 26, 28, 30, 33, 34, 35, 36, 38, 40, 42, 44, 45, 46, 48, 50, 51, 52, 54, 55, 56, 57, 58}$
From Group of Order $p q$ has Normal Sylow $p$-Subgroup:
:$p q \notin S$
The set of non-square semiprimes less than $60$ is:
:$\set {6, 10, 14, 15, 21, 22, 26, 33, 34, 35, 38, 39, 46, 51, 55, 57, 58}$
Thus we have so far:
:$S \subseteq \set {12, 18, 20, 24, 28, 30, 36, 40, 42, 44, 45, 48, 50, 52, 54, 56}$
From Group of Order $p^2 q$ is not Simple:
:$p^2 q \notin S$
This eliminates:
{{begin-eqn}}
{{eqn | l = 12
      | r = 2^2 \times 3
}}
{{eqn | l = 18
      | r = 3^2 \times 2
}}
{{eqn | l = 20
      | r = 2^2 \times 5
}}
{{eqn | l = 28
      | r = 2^2 \times 7
}}
{{eqn | l = 44
      | r = 2^2 \times 11
}}
{{eqn | l = 45
      | r = 3^2 \times 5
}}
{{eqn | l = 50
      | r = 5^2 \times 2
}}
{{eqn | l = 52
      | r = 2^2 \times 13
}}
{{end-eqn}}
Thus we are left with:
:$S \subseteq \set {24, 30, 36, 40, 42, 48, 54, 56}$
From Normal Subgroup of Group of Order 24, a group of order $24$ has a normal subgroup either of order $4$ or order $8$.
Hence $24 \notin S$.
From Group of Order 56 has Unique Sylow 2-Subgroup or Unique Sylow 7-Subgroup, a group of order $56$ has at least one normal subgroup.
Hence $56 \notin S$.
From Group of Order 30 is not Simple:
:$30 \notin S$
Thus we are left with:
:$S \subseteq \set {36, 40, 42, 48, 54}$
$40$ is eliminated by Group of Order 40 has Normal Subgroup of Order 5.
$42$ is eliminated by Group of Order 42 has Normal Subgroup of Order 7.
$54$ is eliminated by Group of Order 54 has Normal Subgroup of Order 27.
$36$ is eliminated by Group of Order 36 is not Simple.
$48$ is eliminated by Group of Order 48 is not Simple.
Hence $S$ is empty.
{{qed}}
Theorem: Group of Order 42 has Normal Subgroup of Order 7

Let $G$ be of order $42$.
Then $G$ has a normal subgroup of order $7$.

Proof:
We have that:
:$42 = 2 \times 3 \times 7$
From the First Sylow Theorem, $G$ has at least one Sylow $7$-subgroup, which is of order $7$.
Let $n_7$ denote the number of Sylow $7$-subgroups of $G$.
From the Fourth Sylow Theorem:
:$n_7 \equiv 1 \pmod 7$
and from the Fifth Sylow Theorem:
:$n_7 \divides 6$
where $\divides$ denotes divisibility.
It follows that $n_7 = 1$.
From Sylow $p$-Subgroup is Unique iff Normal, this Sylow $7$-subgroup is normal.
{{qed}}
Category:Groups of Order 42
qzh3u1kuc9cl8kk2l8oa9yookmzd6a5
Theorem: Group of Order 54 has Normal Subgroup of Order 27

Let $G$ be of order $54$.
Then $G$ has a normal subgroup of order $27$.

Proof:
We have that:
:$54 = 2 \times 3^3$
From the First Sylow Theorem, $G$ has at least one Sylow $3$-subgroup, which is of order $3^3 = 27$.
Let $n_3$ denote the number of Sylow $3$-subgroups of $G$.
From the Fourth Sylow Theorem:
:$n_3 \equiv 1 \pmod 3$
and from the Fifth Sylow Theorem:
:$n_3 \divides 2$
where $\divides$ denotes divisibility.
It follows that $n_3 = 1$.
From Sylow $p$-Subgroup is Unique iff Normal, this Sylow $3$-subgroup is normal.
{{qed}}
Category:Groups of Order 54
49bi4fhqoq3ujnnbiungpqlspagce6y
Theorem: Group of Order 40 has Normal Subgroup of Order 5

Let $G$ be of order $40$.
Then $G$ has a normal subgroup of order $5$.

Proof:
We have that:
:$40 = 2^3 \times 5$
From the First Sylow Theorem, $G$ has at least one Sylow $5$-subgroup, which is of order $5$.
Let $n_5$ denote the number of Sylow $5$-subgroups of $G$.
From the Fourth Sylow Theorem:
:$n_5 \equiv 1 \pmod 5$
and from the Fifth Sylow Theorem:
:$n_5 \divides 8$
where $\divides$ denotes divisibility.
It follows that $n_5 = 1$.
From Sylow $p$-Subgroup is Unique iff Normal, this Sylow $5$-subgroup is normal.
{{qed}}
Category:Groups of Order 40
djhna8lndx7fauabsnev82th3in9f1m
Theorem: Finite Group with One Sylow p-Subgroup per Prime Divisor is Isomorphic to Direct Product

Let $G$ be a finite group whose order is $n$ and whose identity element is $e$.
Let $G$ be such that it has exactly $1$ Sylow $p$-subgroup for each prime divisor of $n$.
Then $G$ is isomorphic to the internal direct product of all its Sylow $p$-subgroups.

Proof:
If each of the Sylow $p$-subgroups are unique, they are all normal.
As the order of each one is coprime to each of the others, their intersection is $\set e$.
{{finish|It remains to be shown that the direct product is what is is}}
Theorem: Number of Subgroups of Prime Power Order is Congruent to 1 modulo Prime

Let $G$ be a finite group whose order is $n$.
Let $p$ be a prime number such that $p^k$ is a divisor of $n$.
Then the number of subgroups of order $p^k$ is congruent to $1$ modulo $p$.

Proof:
Let $r_k$ denote the number of subgroups of $G$ of order $p^k$.
From Number of Order p Elements in Group with m Order p Subgroups:
:The number of elements of order $p$ is $r_1 (p - 1)$.
Since there exists $mp$ elements whose order divide $p$, for some $m \in \Z$:
:The number of elements of order $p$ is $mp - 1$.
Thus,
:$r_1 \equiv 1 \mod p$.
Let $H_1, H_2, \dots, H_{r_{k - 1}}$ be the $r_{k - 1}$ subgroups of order $p^{k - 1}$.
Let $K_1, K_2, \dots, K_{r_k}$ be the $r_k$ subgroups of order $p^k$.
Suppose $H_i$ is contained in $a_i$ of the subgroups $K_1, K_2, \dots, K_{r_k}$.
Suppose $K_j$ contains $b_j$ of the subgroups $H_1, H_2, \dots, H_{r_{k - 1}}$.
Then:
:$a_1 + a_2 + \dots + a_{k - 1} = b_1 + b_2 + \dots + b_k$
is the number of distinct pairs of subgroups $H_i, K_j$ for which $H_i$ is a subgroup of $K_j$.
Let $H$ be one of the subgroups of order $p^{k - 1}$.
Let $K_1, K_2, \dots, K_a$ be the subgroups of order $p^k$ which contain $H$.
Then from Composition Series of Group of Prime Power Order:
:$a > 0$
and:
:$H$ is normal in $K_1, K_2, ..., K_a$.
Hence, $H$ is also normal $G$.
{{Explain|why H is normal in G}}
By correspondence theorem:
:$G / H$ contains the subgroups $K_1 / H, K_2 / H, \dots, K_a / H$.
These are the only subgroups of $G / H$ of order $p$.
Then from above:
:$a \equiv 1 \mod p$.
Since this is the case for each $a_i$, we have:
:$a_1 + a_2 + \dots + a_{r_{k - 1}} \equiv r_{k - 1} \mod p$.
From Number of Order p^(n-1) Subgroups in Order p^n Group, we have also that:
:$b \equiv 1 \mod p$.
and:
:$b_1 + b_2 + \dots + b_{r_k} \equiv r_k \mod p$.
Therefore:
:$r_{k - 1} \equiv r_k \mod p$.
But $r_1 \equiv 1 \mod p$.
So we have, by induction:
:$1 \equiv r_1 \equiv r_2 \equiv \dots \equiv r_k \mod p$.
Hence the result.
{{qed}}
Theorem: Count of Distinct Homomorphisms between Additive Groups of Integers Modulo m

Let $m, n \in \Z_{>0}$ be (strictly) positive integers.
Let $\struct {\Z_m, +}$ denote the additive group of integers modulo $m$.
The number of distinct homomorphisms $\phi: \struct {\Z_m, +} \to \struct {\Z_n, +}$ is $\gcd \set {m, n}$.

Proof:
{{MissingLinks|Missing a lot of links I think...especially the last step. The result should exist in {{ProofWiki}}, but I don't know where it is.}}
$\Z_m$ is isomorphic to the quotient group $\Z / m\Z$.
By Universal Property of Quotient Group, to give a group homomorphism from $\Z_m$ to $\Z_n$ is equivalent to give a homomorphism $\varphi$ from $\Z$ to $\Z_n$ with kernel including the subgroup $m\Z \subset \Z$.
$\Z$ is generated by the element $1$.
By Homomorphism of Generated Group, $\varphi$ is determined by $\map \varphi 1$.
The kernel condition means $\map \varphi m = m \map \varphi 1 = 0 \in \Z_n$.
{{WIP|Links consisting completely of $\LaTeX$ are problematical, sorry, will address at some stage}}
Number of possible such $\map \varphi 1$ is exactly $\gcd \set {m, n}$.
{{qed}}
Theorem: P-adic Integer is Limit of Unique Coherent Sequence of Integers/Lemma 1

:$\forall n \in \N: \alpha_{n + 1} \equiv \alpha_n \pmod {p^{n + 1}}$

Proof:
For any $n \in \N$ then:
{{begin-eqn}}
{{eqn | l = \norm {\alpha_{n + 1} - \alpha_n }_p
      | r = \norm {\paren {\alpha_{n + 1} - x} + \paren {x - \alpha_n } }_p
}}
{{eqn | o = \le
      | r = \max \set {\norm {\alpha_{n + 1} - x}_p, \: \norm {x - \alpha_n }_p }
      | c = {{NormAxiomNonArch|4}}
}}
{{eqn | o = \le
      | r = \max \set {\norm {x - \alpha_{n + 1} }_p, \: \norm {x - \alpha_n }_p}
      | c = Norm of negative
}}
{{eqn | o = \le
      | r = \max \set {p^{-\paren{n + 2} } , p^{-\paren{n + 1} } }
}}
{{eqn | r = p^{-\paren{n + 1} }
      | c = Since $p^{-n - 1} < p^{-n}$
}}
{{end-eqn}}
Hence:
:$p^{n + 1} \divides \paren {\alpha_{n + 1} - \alpha_n} $
or equivalently:
:$\alpha_{n + 1} \equiv \alpha_n \pmod {p^{n + 1} }$
The result follows.
{{qed}}
Theorem: P-adic Integer is Limit of Unique Coherent Sequence of Integers/Lemma 3

$\sequence {\alpha_n}$ is a unique sequence satisfying properties $(1)$, $(2)$ and $(3)$ above.

Proof:
Suppose that there exists a sequence $\sequence {\alpha'_n}$ with:
:$(1'): \quad \forall n \in \N: \alpha'_n \in \Z$ and $0 \le \alpha'_n \le p^{n + 1} - 1$
:$(2'): \quad \forall n \in \N: \alpha'_{n + 1} \equiv \alpha'_n \pmod {p^{n + 1} }$
:$(3'): \quad \ds \lim_{n \mathop \to \infty} \alpha'_n = x$
{{AimForCont}}:
:$\alpha'_N \ne \alpha_N$ for some $N \in \N$
By Initial Segment of Natural Numbers forms Complete Residue System:
:$\alpha'_N \not \equiv \alpha_N \pmod {p^{N + 1} }$
Then for all $n > N$:
{{begin-eqn}}
{{eqn | l = \alpha'_n
      | o = \equiv
      | r = \alpha'_N \pmod {p^{N + 1} }
      | c = by $(2)$ above
}}
{{eqn | o = \not \equiv
      | r = \alpha_N \pmod {p^{N + 1} }
}}
{{eqn | o = \equiv
      | r = \alpha_n \pmod {p^{N + 1} }
      | c = by $(2)$ above
}}
{{end-eqn}}
That is, for all $n > N$:
:$\alpha'_n \not \equiv \alpha_n \pmod {p^{N + 1} }$
Hence for all $n > N$:
:$\norm {\alpha'_n - \alpha_n}_p > p^{-\paren {N + 1} }$
By $(3)$ the limit of $\sequence {\alpha_n}$ is $x$:
:$\exists N_1 \in \N: \forall n \ge N_1: \norm {x - \alpha_n}_p \le p^{-\paren {N + 1} }$
Similarly for $\sequence{\alpha'_n}$:
:$\exists N_2 \in \N: \forall n \ge N_2: \norm {x - \alpha'_n}_p \le p^{-\paren {N + 1} }$
Let $M = \max \set {N + 1, N_1, N_2}$.
Then:
:$\norm {\alpha'_M - \alpha_M}_p > p^{-\paren {N + 1} }$
:$\norm {x - \alpha_M} _p\le p^{-\paren {N + 1} }$
:$\norm {x - \alpha'_M}_p \le p^{-\paren {N + 1} }$
But:
{{begin-eqn}}
{{eqn | l = \norm {\alpha'_M - \alpha_M}_p
      | r = \norm {\paren {\alpha'_M - x} + \paren {x - \alpha_M} }_p
}}
{{eqn | o = \le
      | r = \max \set {\norm {\alpha'_M - x}_p, \: \norm {x - \alpha_M}_p}
      | c = {{NormAxiomNonArch|4}}
}}
{{eqn | r = \max \set {\norm {x - \alpha'_M}_p, \: \norm {x - \alpha_M}_p}
      | c = Norm of negative
}}
{{eqn | o = \le
      | r = \max \set {p^{-\paren {N + 1} } , p^{-\paren {N + 1} } }
}}
{{eqn | r = p^{-\paren {N + 1} }
}}
{{end-eqn}}
This contradicts the previous assertion that:
:$\norm {\alpha'_M - \alpha_M}_p > p^{-\paren {N + 1} }$
Hence:
:$\sequence {\alpha'_n} = \sequence {\alpha_n}$
The result follows.
{{qed}}
Theorem: P-adic Integer is Limit of Unique Coherent Sequence of Integers/Lemma 2

:$\ds \lim_{n \mathop \to \infty} \alpha_n = x$

Proof:
From Sequence of Powers of Number less than One:
:$\ds \lim_{n \mathop \to \infty} p^{-n} = 0$
From Multiple Rule for Real Sequences:
:$\ds \lim_{n \mathop \to \infty} p^{-\paren {n + 1} } = 0$
By the Squeeze Theorem for Real Sequences :
:$\ds \lim_{n \mathop \to \infty} \norm {x - \alpha_n}_p = 0$.
Hence the limit of $\sequence {\alpha_n}$ is by definition:
:$\ds \lim_{n \mathop \to \infty} \alpha_n = x$
{{qed}}
Theorem: Group Types of Order Prime Squared

Let $p$ be a prime number.
Let $G$ be a group of order $p^2$.
Then $G$ is isomorphic either to $\Z_{p^2}$ or to $\Z_p \times \Z_p$, where $\Z_p$ denotes the additive group of integers modulo $p$.

Proof:
From Group of Order Prime Squared is Abelian, $G$ is an abelian group.
From Abelian Group of Prime-power Order is Product of Cyclic Groups, $G$ is either:
:the cyclic group of order $p^2$
:the direct product of the cyclic group  of order $p$ with itself.
The result follows from Finite Cyclic Group is Isomorphic to Integers under Modulo Addition.
{{Qed}}
Theorem: Group/Examples/x+y over 1+xy/Isomorphic to Real Numbers

$\struct {G, \circ}$ is isomorphic to the additive group of real numbers $\struct {\R, +}$.

Proof:
To prove $G$ is isomorphic to $\struct {\R, +}$, we need to find a bijective homorphism $\phi: \openint {-1} 1 \to \R$:
:$\forall x, y \in G: \map \phi {x \circ y} = \map \phi x + \map \phi y$
From Group Examples: $\dfrac {x + y} {1 + x y}$:
:the identity element of $G$ is $0$
:the inverse of $x$ in $G$ is $-x$.
This also holds for $\struct {\R, +}$.
This hints at the structure of a possible isomorphism, namely:
:$(1): \quad$ that it is an odd function
:$(2): \quad$ that it passes through $0$
:$(3): \quad$ that it is defined on the open interval $\openint {-1} 1$.
One such function is the inverse hyperbolic arctangent function $\tanh^{-1}$, which is indeed defined on $\openint {-1} 1$ and has the above properties.
Hence:
{{begin-eqn}}
{{eqn | l = \map {\tanh^{-1} } x
      | r = \frac 1 2 \map \ln {\frac {x + 1} {x - 1} }
      | c = {{Defof|Inverse Hyperbolic Tangent|subdef = Real|index = 2}}
}}
{{eqn | ll= \leadsto
      | l = \map {\tanh^{-1} } {x \circ y}
      | r = \frac 1 2 \map \ln {\frac {\frac {x + y} {1 + x y} + 1} {\frac {x + y} {1 + x y} - 1} }
      | c = Definition of $\struct {G, \circ}$
}}
{{eqn | r = \frac 1 2 \map \ln {\frac {x + y + 1 + x y} {x + y - 1 - x y} }
      | c = 
}}
{{eqn | r = \frac 1 2 \map \ln {\frac {\paren {x + 1} \paren {y + 1} } {\paren {x - 1} \paren {y - 1} } }
      | c = 
}}
{{eqn | r = \frac 1 2 \map \ln {\frac {x + 1} {x - 1} } + \frac 1 2 \map \ln {\frac {y + 1} {y - 1} }
      | c = 
}}
{{eqn | r = \tanh^{-1} x + \tanh^{-1} y
      | c = 
}}
{{end-eqn}}
This demonstrates the homorphism between $\struct {G, \circ}$ and $\struct {\R,  +}$.
We have that Real Inverse Hyperbolic Tangent Function is Strictly Increasing over $\openint {-1} 1$.
Hence from Strictly Monotone Real Function is Bijective, $\tanh^{-1}: \openint {-1} 1 \to \R$ is a bijection.
Hence the result that $\struct {G, \circ} \cong \struct {\R,  +}$.
{{Qed}}
Theorem: Group/Examples/x+y over 1+xy/Isomorphic to Real Numbers

$\struct {G, \circ}$ is isomorphic to the additive group of real numbers $\struct {\R, +}$.

Proof:
To prove $G$ is isomorphic to $\struct {\R, +}$, it is sufficient to find a bijective homorphism $\phi: \to \R \to G$:
:$\forall x, y \in G: \map \phi {x + y} = \map \phi x \circ \map \phi y$
From Group Examples: $\dfrac {x + y} {1 + x y}$:
:the identity element of $G$ is $0$
:the inverse of $x$ in $G$ is $-x$.
This also holds for $\struct {\R, +}$.
This hints at the structure of a possible such $\phi$:
:$(1): \quad$ that it is an odd function
:$(2): \quad$ that it passes through $0$
:$(3): \quad$ that its image is the open interval $\openint {-1} 1$.
One such function is the hyperbolic tangent function $\tanh$, which indeed has the above properties on $\R$.
Then we have that:
{{begin-eqn}}
{{eqn | l = \map {\tanh } {x + y}
      | r = \dfrac {\tanh x + \tanh y} {1 + \tanh x \tanh y}
      | c = Hyperbolic Tangent of Sum
}}
{{eqn | r = \tanh x \circ \tanh y
      | c = 
}}
{{end-eqn}}
This demonstrates the homorphism between $\struct {\R,  +}$ and $\struct {G, \circ}$.
We have that Real Hyperbolic Tangent Function is Strictly Increasing over $\R$.
Hence from Strictly Monotone Real Function is Bijective, $\tanh: \R \to \openint {-1} 1$ is a bijection.
Hence the result that $\struct {\R,  +} \cong \struct {G, \circ}$.
{{Qed}}