avewright/proofwiki-math huggingface dataset:
Theorem: Irrational Number divided by Rational Number is Irrational

Let $x$ be a irrational number. 
Let $y$ be a non-zero rational number.
Then: 
:$\dfrac x y$
is irrational.

Proof:
{{AimForCont}} $\dfrac x y$ is rational number.
Then there exists an integer $p_1$ and a natural number $q_1$ such that: 
:$\dfrac x y = \dfrac {p_1} {q_1}$
That is: 
:$x = \dfrac {p_1} {q_1} y$
From the fact that $y$ is rational, we similarly have that there exists an integer $p_2$ and a natural number $q_2$ such that:
:$y = \dfrac {p_2} {q_2}$
Then: 
:$x = \dfrac {p_1 p_2} {q_1 q_2}$
From Integer Multiplication is Closed, we have that $p_1 p_2$ is an integer. 
From Natural Number Multiplication is Closed, we have that $q_1 q_2$ is a natural number.
Let $p_3 = p_1 p_2$ and $q_3 = q_1 q_2$.
Then $x$ is expressible in the form: 
:$x = \dfrac {p_3} {q_3}$
where $p_3$ is an integer and $q_3$ is a natural number.
This, however, implies that $x$ is rational, which is a contradiction.
By Proof by Contradiction, we conclude that $\dfrac x y$ is irrational.
{{qed}}
Category:Rational Numbers
Category:Irrational Numbers
5j6pxwvssz1xmuq7yfe91hgz9jz6uk3
Theorem: Cramer's Rule

Let $n \in \N$.
Let $b_1, b_2, \dots, b_n$ be real numbers.
Let $\mathbf b = \tuple {b_1, b_2, \dots, b_n}^\intercal$.
Let $x_1, x_2, \dots, x_n$ be real numbers.
Let $\mathbf x = \tuple {x_1, x_2, \dots, x_n}^\intercal$.
Let $A$ be a nonsingular $n \times n$ matrix whose elements are in $\R$.
For each $i \in \set {1, \dots, n}$, let $A_i$ be the matrix obtained by replacing the $i$th column with $\mathbf b$.
Let:
:$A \mathbf x = \mathbf b$
Then:
:$\mathbf x_i = \dfrac {\map \det {A_i} } {\map \det A}$
for each $i \in \set {1, \dots, n}$.

Proof:
Let $C$ be the cofactor matrix of $A$.
By definition, $C^\intercal$ is the adjugate matrix of $A$.
Therefore by Matrix Product with Adjugate Matrix:
:$A \cdot C^\intercal = \det A \cdot I_n$
Because $A$ is nonsingular, $A^{-1}$ exists.
From Matrix is Nonsingular iff Determinant has Multiplicative Inverse,  $1 / \det A$ also exists.
Therefore:
:$A^{-1} = \dfrac 1 {\det A} \cdot C^\intercal$
Since {{hypothesis}} $A \mathbf x = \mathbf b$:
:$\mathbf x = A^{-1} \mathbf b$
Therefore:
:$\mathbf x = \paren {\dfrac 1 {\det A} C^\intercal} \mathbf b$
For each $r, s \in \set {1, 2, \ldots, n}$, let $A_{r s}$ denote the element of $C$ whose index is $\tuple {r, s}$.
Then by the definition of transpose:
:$<nowiki>C^\intercal = \begin {bmatrix} A_{11} & A_{21} & \dots & A_{n1} \\
A_{12} & A_{22} & \dots & A_{n2} \\
\vdots & \vdots & \ddots & \vdots \\
A_{1n} & A_{2n} & \dots & A_{nn}
\end{bmatrix}$</nowiki>
By the definition of cofactor matrix, $A_{r s}$ is the cofactor of the element of $A$ whose index is $\tuple {r, s}$.
Let $i \in \set {1, 2, \ldots, n}$.
Then by definition of matrix product:
:$\ds x_i = \dfrac 1 {\det A} \paren {\sum_{j \mathop = 1}^n A_{ji} b_j}$
Recall that $A_i$ is the matrix obtained from $A$ by replacing the $i$th column with $\mathbf b$. 
Then if:
:<nowiki>$A = \begin {bmatrix} a_{1,1} & a_{1,2} & \dots & a_{1,n} \\
a_{2,1} & a_{2,2} & \dots & a_{2,n} \\
\vdots & \vdots & \ddots & \vdots \\
a_{n,1} & a_{n,2} & \dots & a_{n,n}
\end{bmatrix}$</nowiki>
then:
:<nowiki>$A_i = \begin{bmatrix}
a_{1,1} & a_{1,2} & \dots & a_{1, i - 1} & b_1 & a_{1, i + 1} & \dots & a_{1,n} \\
a_{2,1} & a_{2,2} & \dots & a_{2, i - 1} & b_2 & a_{2, i + 1} & \dots & a_{2,n} \\
\vdots & \vdots & \ddots & \vdots &  \vdots & \vdots & \ddots & \vdots \\
a_{n,1} & a_{n,2} & \dots & a_{n, i - 1} & b_n & a_{n, i + 1} & \dots & a_{n,n}
\end{bmatrix}$</nowiki>
For all $j \in \set {1, 2, \dots, n}$ the matrix obtained by deleting the $j$th row and the $i$th column of $A$ is equal to the matrix obtained by deleting the $j$th row and $i$th column of $A_i$.
Therefore, by definition, the cofactor of $\sqbrk {A_i}_{j,i}$ is equal to $A_{ji}$.
By the Laplace Expansion Theorem for Determinants, we now have:
:$\ds \det{A_i} = \sum_{j \mathop = 1}^n A_{ji} b_j$
Therefore:
:$x_i = \dfrac {\det {A_i} } {\det A}$
as desired.
{{qed}}
{{Namedfor|Gabriel Cramer|cat = Cramer}}
Theorem: Equation of Limaçon of Pascal/Polar Form

The limaçon of Pascal can be defined by the polar equation:
:$r = b + a \cos \theta$

Proof:
Let $C$ be a circle of diameter $a$ whose circumference passes through the origin $O$.
Let the diameter of $C$ which passes through $O$ lie on the polar axis.
Let $OQ$ be a chord of $C$.
Let $b$ be a real constant.
:400px
Let $P = \polar {r, \theta}$ denote an arbitrary point on a limaçon of Pascal $L$.
We have that:
{{begin-eqn}}
{{eqn | l = OP
      | r = OQ \pm QP
      | c = {{Defof|Limaçon of Pascal}}
}}
{{eqn | ll= \leadsto
      | l = r
      | r = a \cos \theta \pm b
      | c = {{Defof|Cosine of Angle}}
}}
{{end-eqn}}
When $-\dfrac \pi 2 \le \theta \le \dfrac \pi 2$, we have:
:$r = b + a \cos \theta$
When $\dfrac \pi 2 \le \theta \le \dfrac {3 \pi} 2$, we have:
{{begin-eqn}}
{{eqn | l = -r
      | r = -b + a \, \map \cos {\theta + \pi}
      | c = 
}}
{{eqn | r = -b - a \cos \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r
      | r = b + a \cos \theta
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Equation of Limaçon of Pascal/Cartesian Form

The limaçon of Pascal can be defined by the Cartesian equation:
:$\paren {x^2 + y^2 - a x}^2 = b^2 \paren {x^2 + y^2}$

Proof:
{{begin-eqn}}
{{eqn | l = r
      | r = b + a \cos \theta
      | c = Equation of Limaçon of Pascal: Polar Form
}}
{{eqn | ll= \leadsto
      | l = r^2
      | r = r b + r a \cos \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^2 + y^2
      | r = b \sqrt {x^2 + y^2} + a x
      | c = Conversion between Cartesian and Polar Coordinates in Plane
}}
{{eqn | ll= \leadsto
      | l = x^2 + y^2 - a x
      | r = b \sqrt {x^2 + y^2}
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \paren {x^2 + y^2 - a x}^2
      | r = b^2 \paren {x^2 + y^2}
      | c = squaring both sides
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Cissoid of Diocles/Polar Form

The '''cissoid of Diocles''' can be defined by the polar equation:
:$r = 2 a \sin \theta \tan \theta$

Proof:
:400px
By construction:
{{begin-eqn}}
{{eqn | l = OS
      | r = 2 a \sec \theta
      | c = {{Defof|Secant Function}}
}}
{{eqn | l = OR
      | r = 2 a \cos \theta
      | c = {{Defof|Cosine}}
}}
{{eqn | l = OP
      | r = RS
      | c = {{Defof|Cissoid of Diocles}}
}}
{{eqn | ll= \leadsto
      | l = OP
      | r = OS - OR
      | c = 
}}
{{eqn | ll= \leadsto
      | l = r
      | r = 2 a \paren {\sec \theta - \cos \theta}
      | c = 
}}
{{eqn | r = 2 a \sin \theta \tan \theta
      | c = Secant Minus Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Cissoid of Diocles/Cartesian Form

The '''cissoid of Diocles''' can be defined by the Cartesian equation:
:$x \paren {x^2 + y^2} = 2 a y^2$

Proof:
{{begin-eqn}}
{{eqn | l = r
      | r = 2 a \sin \theta \tan \theta
      | c = Equation of Cissoid of Diocles: Polar Form
}}
{{eqn | ll= \leadsto
      | l = r^2
      | r = 2 a r \sin \theta \tan \theta
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x^2 + y^2
      | r = 2 a y \dfrac y x
      | c = Conversion between Cartesian and Polar Coordinates in Plane
}}
{{eqn | ll= \leadsto
      | l = x \paren {x^2 + y^2}
      | r = 2 a y^2
      | c = rearranging
}}
{{end-eqn}}
{{qed}}
Theorem: Equation of Cissoid of Diocles/Parametric Form

The cissoid of Diocles can be defined by the parametric equation:
:$\begin {cases} x = 2 a \sin^2 \theta \\ \\ y = \dfrac {2 a \sin^3 \theta} {\cos \theta} \end {cases}$

Proof:
{{begin-eqn}}
{{eqn | l = r
      | r = 2 a \sin \theta \tan \theta
      | c = Equation of Cissoid of Diocles: Polar Form
}}
{{eqn | ll= \leadsto
      | l = r \cos \theta
      | r = 2 a \cos \sin \theta \paren {\dfrac {\sin \theta} {\cos \theta} }
      | c = 
}}
{{eqn | l = r \sin \theta
      | r = 2 a \sin \theta \sin \theta \paren {\dfrac {\sin \theta} {\cos \theta} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = 2 a \sin^2 \theta
      | c = Conversion between Cartesian and Polar Coordinates in Plane
}}
{{eqn | l = y
      | r = \dfrac {2 a \sin^3 \theta} {\cos \theta}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of One plus x Squared over One plus Fourth Power of x

:$\ds \int \frac {x^2 + 1} {x^4 + 1} \rd x = \frac 1 {\sqrt 2} \map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + C$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \int \frac {x^2 + 1} {x^4 + 1} \rd x
	| r = \int \frac {1 + \frac 1 {x^2} } {x^2 + \frac 1 {x^2} } \rd x
}}
{{eqn	| r = \int \frac {1 + \frac 1 {x^2} } {\paren {x - \frac 1 x}^2 + 2} \rd x
	| c = Completing the Square
}}
{{end-eqn}}
Note that, by Derivative of Power: 
:$\dfrac \d {\d x} \paren {x - \dfrac 1 x} = 1 + \dfrac 1 {x^2}$
So, we have:
{{begin-eqn}}
{{eqn	| r = \int \frac 1 {u^2 + 2} \rd u
	| c = substituting $u = x - \dfrac 1 x$
}}
{{eqn	| r = \frac 1 {\sqrt 2} \map \arctan {\frac 1 {\sqrt 2} u} + C
	| c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn	| r = \frac 1 {\sqrt 2} \map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + C
}}
{{end-eqn}}
{{qed}}
Category:Primitives involving Reciprocals
aw74gd67w94hv50ldvtpbimq4xmvyxe
Theorem: Primitive of Minus One plus x Squared over One plus Fourth Power of x

:$\ds \int \frac {x^2 - 1} {x^4 + 1} \rd x = \frac 1 {2 \sqrt 2} \ln \size {\frac {x^2 - \sqrt 2 x + 1} {x^2 + \sqrt 2 x + 1} } + C$

Proof:
We have:
{{begin-eqn}}
{{eqn	| l = \int \frac {x^2 - 1} {x^4 + 1} \rd x
	| r = \int \frac {1 - \frac 1 {x^2} } {x^2 + \frac 1 {x^2} } \rd x
}}
{{eqn	| r = \int \frac {1 - \frac 1 {x^2} } {\paren {x + \frac 1 x}^2 - 2} \rd x
	| c = Completing the Square
}}
{{end-eqn}}
Note that, by Derivative of Power: 
:$\dfrac \d {\d x} \paren {x + \dfrac 1 x} = 1 - \dfrac 1 {x^2}$
So, we have:
{{begin-eqn}}
{{eqn	| l = \int \frac {1 - \frac 1 {x^2} } {\paren {x + \frac 1 x}^2 - 2} \rd x
	| r = \int \frac 1 {u^2 - 2} \rd u
	| c = substituting $u = x + \dfrac 1 x$
}}
{{eqn	| r = \frac 1 {2 \sqrt 2} \ln \size {\frac {u - \sqrt 2} {u + \sqrt 2} } + C
	| c = Primitive of $\dfrac 1 {x^2 - a^2}$: Logarithm Form
}}
{{eqn	| r = \frac 1 {2 \sqrt 2} \ln \size {\frac {x + \frac 1 x - \sqrt 2} {x + \frac 1 x + \sqrt 2} } + C
}}
{{eqn	| r = \frac 1 {2 \sqrt 2} \ln \size {\frac {x^2 - \sqrt 2 x + 1} {x^2 + \sqrt 2 x + 1} } + C
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Minus One plus x Squared over One plus Fourth Power of x

:$\ds \int \frac {x^2 - 1} {x^4 + 1} \rd x = \frac 1 {2 \sqrt 2} \ln \size {\frac {x^2 - \sqrt 2 x + 1} {x^2 + \sqrt 2 x + 1} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {x^2 - 1} {x^4 + 1} \rd x
      | r = \int \frac {x^2} {x^4 + 1} \rd x - \int \frac 1 {x^4 + 1} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 {4 \sqrt 2} \map \ln {\frac {x^2 - x \sqrt 2 + 1} {x^2 + x \sqrt 2 + 1} } - \frac 1 {2 \sqrt 2} \paren {\map \arctan {1 - x \sqrt 2} - \map \arctan {1 + x \sqrt 2} }
      | c = Primitive of $\dfrac {x^2} {x^4 + a^4}$, setting $a = 1$
}}
{{eqn | o = 
      | ro= -
      | r = \frac 1 {2 \sqrt 2} \paren {\map \arctan {\frac 1 {\sqrt 2} \paren {x - \frac 1 x} } + \frac 1 2 \ln \size {\frac {x^2 + \sqrt 2 x + 1} {x^2 - \sqrt 2 x + 1} } }
      | c = Primitive of $\dfrac 1 {1 + x^4}$
}}
{{end-eqn}}
{{finish|Resolve the arctangent equality}}
Theorem: Dissection of Square into 8 Acute Triangles

A square can be dissected into $8$ acute triangles.

Proof:
{{ProofWanted|Trivial but wordy and tedious.}}
Category:Squares
Category:Dissections
Category:Acute Triangles
0osvjocw3tjip717wonyq7wrcbw7kre
Theorem: Dissection of Square into 9 Acute Triangles

A square can be dissected into $9$ acute triangles.

Proof:
{{ProofWanted|Trivial but wordy and tedious.}}
Theorem: Length of Chord Projected from Point on Intersecting Circle

Let $C_1$ and $C_2$ be two circles which intersect at $A$ and $B$.
Let $T$ be a point on $C_1$.
Let $P$ and $Q$ be the points $TA$ and $TB$ intersect $C_2$.
:400px
Then $PQ$ is constant, wherever $T$ is positioned on $C_1$.

Proof:
{{ProofWanted}}
Outline of proof:
By angle in the same segment, $\angle APB$ and $\angle ATB$ are constant.
Hence $\angle PBQ$ is constant.
This forces $PQ$ to be constant.
However this must be divided into multiple cases as sometimes $P, Q, T$ are contained in $C_1$.
The limit cases $T = A$ and $T = B$ can also be proven by interpreting $AT, BT$ as tangents at $T$.
Theorem: Regiomontanus' Angle Maximization Problem

Let $AB$ be a line segment.
Let $AB$ be produced to $P$.
Let $PQ$ be constructed perpendicular to $AB$.
Then the angle $AQB$ is greatest when $PQ$ is tangent to a circle passing through $A$, $B$ and $Q$.

Proof:
:400px
There exists a unique circle $C$ tangent to $PQ$ passing through $A$ and $B$.
From Angles in Same Segment of Circle are Equal, the angle subtended by $AB$ from any point on $C$ is the same as angle $\angle AQB$.
All other points on $PQ$ that are not $Q$ itself are outside $C$.
Hence the angle subtended by $AB$ to such points is smaller.
Hence the result.
{{qed}}
{{Namedfor|Regiomontanus|cat = Regiomontanus}}
Theorem: First Projection on Ordered Pair of Sets

Let $a$ and $b$ be sets.
Let $w = \tuple {a, b}$ denote the ordered pair of $a$ and $b$.
Let $\map {\pr_1} w$ denote the first projection on $w$.
Then:
:$\ds \map {\pr_1} w = \bigcup \bigcap w$
where $\ds \bigcup$ and $\ds \bigcap$ denote union and intersection respectively.

Proof:
We have by definition of first projection that:
:$\map {\pr_1} w = \map {\pr_1} {a, b} = a$
Then:
{{begin-eqn}}
{{eqn | l = \bigcup \bigcap w
      | r = \bigcup \bigcap \tuple {a, b}
      | c = Definition of $w$
}}
{{eqn | r = \bigcup \bigcap \set {\set a, \set {a, b} }
      | c = {{Defof|Kuratowski Formalization of Ordered Pair|Ordered Pair}}
}}
{{eqn | r = \map \bigcup {\set a \cap \set {a, b} }
      | c = Intersection of Doubleton
}}
{{eqn | r = \bigcup \set a
      | c = {{Defof|Set Intersection}}
}}
{{eqn | r = a
      | c = Union of Singleton
}}
{{end-eqn}}
{{qed}}
Theorem: Intersection of Doubleton

Let $x$ and $y$ be sets.
Let $\set {x, y}$ be a doubleton.
Then $\bigcap \set {x, y}$ is a set such that:
:$\bigcap \set {x, y} = x \cap y$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = z \in \bigcap \set {x, y}
      | c = 
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \forall w \in \set {x, y}: z \in w
      | c = {{Defof|Intersection of Class}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \forall w: \paren {\paren {w = x \land w = y} \land z \in w}
      | c = {{Defof|Doubleton Class}}
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = \paren {z \in x \land z \in y}
      | c = Equality implies Substitution
}}
{{eqn | ll= \leadstoandfrom
      | o = 
      | r = z \in \paren {x \cap y}
      | c = {{Defof|Class Intersection}}
}}
{{end-eqn}}
From Intersection of Non-Empty Class is Set it follows that $x \cap y$ is a set.
{{qed}}
Theorem: Second Projection on Ordered Pair of Sets

Let $a$ and $b$ be sets.
Let $w = \tuple {a, b}$ denote the ordered pair of $a$ and $b$.
Let $\map {\pr_2} w$ denote the second projection on $w$.
Then:
:$\ds \map {\pr_2} w = \begin {cases} \ds \map \bigcup {\bigcup w \setminus \bigcap w} & : \ds \bigcup w \ne \bigcap w \\ \ds \bigcup \bigcup w & : \bigcup w = \ds \bigcap w \end {cases}$
where:
:$\ds \bigcup$ and $\ds \bigcap$ denote union and intersection respectively.
:$\setminus$ denotes the set difference operator.

Proof:
We have by definition of second projection that:
:$\map {\pr_1} w = \map {\pr_1} {a, b} = b$
We consider:
{{begin-eqn}}
{{eqn | l = \bigcup w
      | r = \bigcup \tuple {a, b}
      | c = Definition of $w$
}}
{{eqn | r = \bigcup \set {\set a, \set {a, b} }
      | c = {{Defof|Kuratowski Formalization of Ordered Pair|Ordered Pair}}
}}
{{eqn | r = \set a \cup \set {a, b}
      | c = Union of Doubleton
}}
{{eqn | n = 1
      | r = \set {a, b}
      | c = {{Defof|Union of Set of Sets}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \bigcap w
      | r = \bigcap \tuple {a, b}
      | c = Definition of $w$
}}
{{eqn | r = \bigcap \set {\set a, \set {a, b} }
      | c = {{Defof|Kuratowski Formalization of Ordered Pair|Ordered Pair}}
}}
{{eqn | r = \set a \cap \set {a, b}
      | c = Intersection of Doubleton
}}
{{eqn | n = 2
      | r = \set a
      | c = {{Defof|Intersection of Set of Sets}}
}}
{{end-eqn}}
Suppose $\ds \bigcup w \ne \bigcap w$.
Then:
{{begin-eqn}}
{{eqn | l = \map \bigcup {\bigcup w \setminus \bigcap w}
      | r = \map \bigcup {\set {a, b} \setminus \set a}
      | c = from $(1)$ and $(2)$ above
}}
{{eqn | r = \bigcup \set b
      | c = {{Defof|Set Difference}}, which holds because $a \ne b$
}}
{{eqn | r = b
      | c = Union of Singleton
}}
{{end-eqn}}
demonstrating that the first case holds.
Now suppose that $\bigcup w = \bigcap w$.
Thus:
{{begin-eqn}}
{{eqn | l = \bigcup w
      | r = \bigcap w
      | c = 
}}
{{eqn | n = 3
      | ll= \leadsto
      | l = \set {a, b}
      | r = \set a
      | c = 
}}
{{eqn | n = 4
      | ll= \leadsto
      | l = a
      | r = b
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \bigcup \bigcup w
      | r = \bigcup \bigcup \tuple {a, b}
      | c = Definition of $w$
}}
{{eqn | r = \bigcup \bigcup \set {\set a, \set {a, b} }
      | c = {{Defof|Kuratowski Formalization of Ordered Pair|Ordered Pair}}
}}
{{eqn | r = \bigcup \bigcup \set {\set a, \set a}
      | c = from $(3)$ above
}}
{{eqn | r = \map \bigcup {\set a \cup \set a}
      | c = Union of Doubleton
}}
{{eqn | r = \bigcup \set a
      | c = Set Union is Idempotent
}}
{{eqn | r = a
      | c = Union of Singleton
}}
{{eqn | r = b
      | c = from $(4)$ above
}}
{{end-eqn}}
The result follows;
{{qed}}
Theorem: Order Isomorphism between Tosets is not necessarily Unique

Let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be tosets.
Let $\struct {S_1, \preccurlyeq_1} \cong \struct {S_2, \preccurlyeq_2}$, that is, let $\struct {S_1, \preccurlyeq_1}$ and $\struct {S_2, \preccurlyeq_2}$ be order isomorphic.
Then it is not necessarily the case that there is exactly one mapping $f: S_1 \to S_2$ such that $f$ is an order isomorphism.

Proof:
Proof by Counterexample:
Let $\Z$ denote the set of integers.
We have that Integers under Usual Ordering form Totally Ordered Set.
Let $m \in \Z$ be an arbitrary integer.
Let $f_m: \Z \to \Z$ be the order isomorphism defined as:
:$\forall a \in \Z: \map {f_m} a = a + m$
It follows that there are at least as many order isomorphisms of from $\Z$ to $\Z$ as there are integers.
Hence the result
{{qed}}
Theorem: Pi as Sum of Alternating Sequence of Products of 3 Consecutive Reciprocals/Lemma

:$\ds \iiint \dfrac x {x^2 + 1} \rd x \rd x \rd x = x \map \arctan x + \dfrac {\paren {x^2 - 1} \map \ln {x^2 + 1} - 3 x^2} 4$
with all integration constants at $0$.

Proof:
First primitive:
{{begin-eqn}}
{{eqn | l = \int \dfrac x {x^2 + 1} \rd x
      | r = \dfrac 1 2 \int \dfrac {2 x} {x^2 + 1} \rd x
      | c = 
}}
{{eqn | r = \dfrac {\map \ln {x^2 + 1} } 2
      | c = Primitive of Function under its Derivative
}}
{{end-eqn}}
The integration constant is not added due to the series never having a constant during its integration.
{{qed|lemma}}
Second primitive:
{{begin-eqn}}
{{eqn | l = \int \dfrac {\map \ln {x^2 + 1} } 2 \rd x
      | r = \dfrac 1 2 \paren {x \map \ln {x^2 + 1^2} - 2 x + 2 \times 1 \times \arctan \frac x 1}
      | c = Primitive of $\ln {x^2 + a^2}$, putting $a = 1$
}}
{{eqn | r = \dfrac {x \map \ln {x^2 + 1} } 2 - x + \map \arctan x
      | c =
}}
{{end-eqn}}
{{qed|lemma}}
Third primitive:
{{begin-eqn}}
{{eqn | l = \int \paren {\dfrac {x \map \ln {x^2 + 1} } 2 + \map \arctan x - x} \rd x
      | r = \int \dfrac {x \map \ln {x^2 + 1} } 2 \rd x + \int \map \arctan x \rd x - \int x \rd x
      | c =
}}
{{eqn | r = \int \dfrac {x \map \ln {x^2 + 1} } 2 \rd x + \int \map \arctan x \rd x - \dfrac {x^2} 2
      | c = Integral of Power
}}
{{eqn | r = \int \dfrac {x \map \ln {x^2 + 1} } 2 \rd x + x \map \arctan x - \dfrac {\map \ln {x^2 + 1} } 2 - \dfrac {x^2} 2
      | c = Primitive of $\arctan \dfrac x a$
}}
{{eqn | r = \frac 1 2 \paren {\frac {\paren {x^2 + 1} \map \ln {x^2 + 1} - x^2} 2} + x \map \arctan x - \dfrac {\map \ln {x^2 + 1} } 2 - \dfrac {x^2} 2
      | c = Primitive of $x \map \ln {x^2 + a^2}$ with $a = 1$
}}
{{eqn | r = x \map \arctan x + \dfrac {\paren {x^2 - 1} \map \ln {x^2 + 1} - 3 x^2} 4
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Category:Pi as Sum of Alternating Sequence of Products of 3 Consecutive Reciprocals
okhuq91pcvq5pixj7fysitw0sf8tp9z
Theorem: Supremum of Set Equals Maximum of Suprema of Subsets

Let $S$ be a non-empty real set.
Let $\set {S_i: i \in \set {1, 2, \ldots, n} }$, $n \in \N_{>0}$, be a set of non-empty subsets of $S$.
Let $S = \bigcup S_i$.
Then:
:$S_i$ has a supremum for every $i$ in $\set {1, 2, \ldots, n}$
{{iff}}:
:$S$ has a supremum
and, in either case:
:$\sup S = \max \set {\sup S_1, \sup S_2, \ldots, \sup S_n}$

Proof:
=== Necessary Condition ===
Let:
:$S$ have a supremum.
We need to show that:
:$(1): \quad S_i$ has a supremum for every $i$ in $\set {1, 2, \ldots, n}$
:$(2): \quad \sup S = \max \set {\sup S_1, \sup S_2, \ldots, \sup S_n}$
By Supremum of Set of Real Numbers is at least Supremum of Subset, $\sup S_i$ exists for every $i$ in $\set {1, 2, \ldots, n}$.
This proves $(1)$.
Also by Supremum of Set of Real Numbers is at least Supremum of Subset, $\sup S \ge \sup S_i$ for every $i$ in $\set {1, 2, \ldots, n}$.
Therefore:
:$\sup S \ge \max \set {\sup S_1, \sup S_2, \ldots, \sup S_n}$
In addition, by Supremum of Subset of Union Equals Supremum of Union:
:$\sup S = \sup S_j$ for a $j$ in $\set {1, 2, \ldots, n}$
Therefore:
:$\sup S \le \max \set {\sup S_1, \sup S_2, \ldots, \sup S_n}$
Accordingly:
:$\sup S = \max \set {\sup S_1, \sup S_2, \ldots, \sup S_n}$
This proves $(2)$.
{{qed|lemma}}
Theorem: P-adic Integer has Unique Coherent Sequence Representative/Lemma 1

:$\forall j \in \N: \norm {\beta_{\map N {j + 1} } - \beta_{\map N j} }_p \le p^{-\paren {j + 1} }$

Proof:
Let $j \in N$
Suppose $\map N {j + 1} \ge \map N j$
By definition:
:$\norm{\beta_{\map N {j + 1} } - \beta_{\map N j} }_p \le p^{-\paren {j + 1} }$
Now suppose $\map N j \ge \map N {j + 1}$
Then:
{{begin-eqn}}
{{eqn | l = \norm {\beta_{\map N {j + 1} } - \beta_{\map N j} }_p
      | o = \le 
      | r = p^{-\paren {j + 2} }
}}
{{eqn | o = < 
      | r = p^{-\paren {j + 1} }
      | c = Power Function on Integer between Zero and One is Strictly Decreasing
}}
{{end-eqn}}
In either case:
:$\norm {\beta_{\map N {j + 1} } - \beta_{\map N j} }_p \le p^{-\paren{j + 1} }$
Since $j$ was arbitrary, then:
:$\forall j \in \N: \norm {\beta_{\map N {j + 1} } - \beta_{\map N j} }_p \le p^{-\paren {j + 1} }$
{{qed}}
Category:P-adic Integer has Unique Coherent Sequence Representative
kd24khe0kfpb30xajqhqxlpo0b9o096
Theorem: P-adic Integer has Unique Coherent Sequence Representative/Lemma 2

:$\forall j \in \N: \norm {\alpha_{j + 1} - \alpha_j }_p \le p^{-\paren {j + 1} }$

Proof:
For all $j \in \N$:
{{begin-eqn}}
{{eqn | l = \norm {\alpha_{j + 1} - \alpha_j}_p
      | r = \norm {\alpha_{j + 1} - \gamma_{j + 1} + \gamma_{j + 1} - \gamma_j + \gamma_j - \alpha_j}_p
}}
{{eqn | o = \le
      | r = \max \set {\norm {\alpha_{j + 1} - \gamma_{j + 1} }_p \mathop , \norm {\gamma_{j + 1} - \gamma_j }_p \mathop , \norm{\gamma_j - \alpha_j}_p}
}}
{{eqn | o = \le
      | r = \max \set {p^{-\paren{j + 2} } , \norm{\gamma_{j + 1} - \gamma_j }_p \mathop , p^{-\paren {j + 1} } }
      | c = Assumption on $\sequence{\alpha_n}$
}}
{{eqn | o = \le
      | r = \max \set {p^{-\paren {j + 2} } , p^{-\paren {j + 1} } , p^{-\paren {j + 1} } }
      | c = Assumption on $\sequence{\gamma_n}$
}}
{{eqn | r = p^{-\paren {j + 1} }
      | c =  Power Function on Integer between Zero and One is Strictly Decreasing
}}
{{end-eqn}}
{{qed}}
Category:P-adic Integer has Unique Coherent Sequence Representative
bhc7whw1fv0wqumfehbnzq7lm494o4v