avewright/proofwiki-math huggingface dataset:
Theorem: Correspondence between Irrational Numbers and Simple Infinite Continued Fractions

Let $\R \setminus \Q$ be the set of irrational numbers.
Let $S$ be the set of all simple infinite continued fractions in $\R$.
The mappings:
:$\R \setminus \Q \to S$ that sends an irrational number to its continued fraction expansion
:$S \to \R \setminus \Q$ that sends a simple infinite continued fractions to its value
are inverses of each other.

Proof:
Note that indeed a Simple Infinite Continued Fraction Converges to Irrational Number.
The result follows from:
: Continued Fraction Expansion of Irrational Number Converges to Number Itself
: Continued Fraction Expansion of Limit of Simple Infinite Continued Fraction equals Expansion Itself
{{qed}}
Theorem: Ultraconnected Space is Connected

Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
Then $T$ is connected.

Proof:
Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
From Ultraconnected Space is Path-Connected, $T$ is path-connected.
The result follows from Path-Connected Space is Connected.
{{qed}}
Theorem: Irreducible Space is not necessarily Path-Connected

Let $T = \struct {S, \tau}$ be a topological space which is irreducible.
Then $T$ is not necessarily path-connected.

Proof:
Let $T$ be a countable finite complement space.
From Finite Complement Space is Irreducible, $T$ is an irreducible space.
From Countable Finite Complement Space is not Path-Connected, $T$ is not path-connected.
Hence the result.
{{qed}}
Theorem: Ultraconnected Space is not necessarily Injectively Path-Connected

Let $T = \struct {S, \tau}$ be a topological space which is ultraconnected.
Then $T$ is not necessarily injectively path-connected.

Proof:
Let $T$ be an excluded point space.
From Excluded Point Space is Ultraconnected, $T$ is an ultraconnected space.
From Excluded Point Space is not Injectively Path-Connected, $T$ is not injectively path-connected.
Hence the result.
{{qed}}
Theorem: Correspondence between Rational Numbers and Simple Finite Continued Fractions

Let $\Q$ be the set of rational numbers.
Let $S$ be the set of all simple finite continued fractions in $\Q$, whose last partial denominators is not $1$.
The mappings:
:$\Q \to S$ that sends an rational number to its continued fraction expansion
:$S \to \Q$ that sends a simple finite continued fractions to its value
are inverses of each other.

Proof:
Note that indeed Simple Finite Continued Fraction has Rational Value.
The result follows from:
:Value of Continued Fraction Expansion of Rational Number equals Number Itself
:Continued Fraction Expansion of Value of Simple Finite Continued Fraction equals Expansion Itself
{{qed}}
Theorem: Existence of Non-Locally Connected Space where Components and Quasicomponents are Equal

There exists at least one example of a topological space which is not locally connected, but whose components and quasicomponents are equal.

Proof:
Let $T$ be the Arens-Fort space.
From Arens-Fort Space is not Locally Connected, $T$ is not a locally connected space.
The result follows from Components and Quasicomponents of Arens-Fort Space are Equal.
{{qed}}
Theorem: Finite Irreducible Space is Path-Connected

Let $T = \struct {S, \tau}$ be a finite irreducible topological space.
Then $T$ is path-connected.

Proof:
By Power Set of Finite Set is Finite, the power set $\powerset S$ is finite.
By Subset of Finite Set is Finite, $\tau \subseteq \powerset S$ is finite.
The result follows from Irreducible Space with Finitely Many Open Sets is Path-Connected.
{{qed}}
Theorem: Locally Connected Space is not necessarily Connected

Let $T = \struct {S, \tau}$ be a topological space which is locally connected.
Then it is not necessarily the case that $T$ is also a connected space.

Proof:
Let $T$ be a discrete topological space with more than $1$ point.
From Discrete Space is Locally Connected, $T$ is a locally connected space.
From Non-Trivial Discrete Space is not Connected, $T$ is not a connected space.
Hence the result.
{{qed}}
Theorem: Connected Space is not necessarily Locally Connected

Let $T = \struct {S, \tau}$ be a topological space which is connected.
Then it is not necessarily the case that $T$ is also a locally connected space.

Proof:
Let $C$ be the closed topologist's sine curve embedded in the real Euclidean plane.
From Closed Topologist's Sine Curve is Connected, $C$ is connected in $T$
From Closed Topologist's Sine Curve is not Locally Connected, $C$ is not locally connected.
Hence the result.
{{qed}}
Theorem: Irreducible Space with Finitely Many Open Sets is Path-Connected

Let $T = \struct {S, \tau}$ be an irreducible topological space.
Let its topology $\tau$ be finite.
Then $T$ is path-connected.

Proof:
Follows immediately from:
* Irreducible Space with Finitely Many Open Sets has Generic Point
* Topological Space with Generic Point is Path-Connected
{{qed}}
Theorem: Topological Space with Generic Point is Path-Connected

Let $T = \struct {S, \tau}$ be a topological space.
Let $T$ have a generic point $g \in S$.
Then $T$ is path-connected.

Proof:
By Path-Connectedness is Equivalence Relation, it suffices to prove that every point is path-connected with $g$.
Let $x \in S$.
Define a path $\gamma: \closedint 0 1 \to S$ by:
:<nowiki>$\map \gamma t = \begin{cases}
x & : t \le \dfrac 1 2 \\
g & : t > \dfrac 1 2
\end{cases}$</nowiki>
We show that $\gamma$ is indeed continuous.
Let $U \subseteq S$ be open and non-empty.
Because $g$ is a generic point, $g \in U$.
If $x \in U$, then its preimage $\gamma^{-1} \sqbrk U = \closedint 0 1$ is open.
If $x \notin U$, then its preimage $\gamma^{-1} \sqbrk U = \hointl {\dfrac 1 2} 1$ is also open.
Thus $x$ and $g$ are path-connected.
{{qed}}
Category:Path-Connected Spaces
mlxqc8e38775hpn2byjv5ivg98p8gkh
Theorem: Floor of Simple Finite Continued Fraction

Let $\sequence {a_k}_{k \mathop \ge 0}$ be a simple finite continued fraction of length $n \ge 0$.
Let $x = \sqbrk {a_0, \ldots, a_n}$ be its value.
Then the floor of $x$ is the partial denominator $a_0$:
:$\floor x = a_0$
unless $n = 1$ and $a_1 = 1$, in which case:
:$\floor x = x = a_0 + 1$

Proof:
;Length $0$
Let $n = 0$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \sqbrk {a_0}
      | c = {{hypothesis}}: $n = 0$
}}
{{eqn | r = a_0
      | c = {{Defof|Value of Finite Continued Fraction}}
}}
{{eqn | ll= \leadsto
      | l = \floor x
      | r = \floor {a_0}
      | c = 
}}
{{eqn | r = a_0
      | c = Real Number is Integer iff equals Floor
}}
{{end-eqn}}
{{qed|lemma}}
;Length $1$
Let $n = 1$.
Then:
{{begin-eqn}}
{{eqn | l = x
      | r = \sqbrk {a_0, a_1}
      | c = {{hypothesis}}: $n = 1$
}}
{{eqn | n = 1
      | r = a_0 + \dfrac 1 {a_1}
      | c = {{Defof|Value of Finite Continued Fraction}}
}}
{{end-eqn}}
Let $a_1 > 1$.
Then:
{{begin-eqn}}
{{eqn | l = a_0
      | o = <
      | r = a_0 + \dfrac 1 {a_1}
      | c = 
}}
{{eqn | o = <
      | r = a_0 + 1
      | c = Real Number is Integer iff equals Floor
}}
{{eqn | ll= \leadsto
      | l = \floor x
      | r = \floor {a_0 + \dfrac 1 {a_1} }
      | c = from $(1)$
}}
{{eqn | r = a_0
      | c = {{Defof|Floor Function}}
}}
{{end-eqn}}
Let $a_1 = 1$.
Then: $x = a_0 + 1$.
{{begin-eqn}}
{{eqn | l = x
      | r = a_0 + \dfrac 1 {a_1}
      | c = from $(1)$
}}
{{eqn | r = a_0 + 1
      | c = as $\dfrac 1 {a_1} = 1$
}}
{{eqn | ll= \leadsto
      | l = \floor x
      | r = \floor {a_0 + 1}
      | c = 
}}
{{eqn | r = a_0 + 1
      | c = Real Number is Integer iff equals Floor
}}
{{end-eqn}}
{{qed|lemma}}
;Length at least $2$
Let $n \ge 2$.
Then:
{{begin-eqn}}
{{eqn | l = \sqbrk {a_0, \ldots, a_n}
      | o = >
      | r = a_0
      | c = Value of Finite Continued Fraction of Real Numbers is at Least First Term
}}
{{eqn | l = \sqbrk {a_1, \ldots, a_n}
      | o = >
      | r = a_1
      | c = Value of Finite Continued Fraction of Real Numbers is at Least First Term
}}
{{eqn | l = a_0
      | o = <
      | r = \sqbrk {a_0, \ldots, a_n}
      | c = 
}}
{{eqn | r = a_0 + \dfrac 1 {\sqbrk {a_1, \ldots, a_n} }
      | c = {{Defof|Value of Finite Continued Fraction}}
}}
{{eqn | o = <
      | r = a_0 + 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \floor x
      | r = a_0
      | c = {{Defof|Floor Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Value of Finite Continued Fraction of Strictly Positive Real Numbers is Strictly Positive

Let $\sequence {a_0, \ldots, a_n}$ be a finite continued fraction in $\R$ of length $n \ge 0$.
Let all partial denominators $a_k > 0$ be strictly positive.
Let $x = \sqbrk {a_0, a_1, \ldots, a_n}$ be its value.
Then $x > 0$.

Proof:
{{proof wanted|use Definition:Value of Continued Fraction}}
Theorem: Value of Finite Continued Fraction of Real Numbers is at Least First Term

Let $\sequence {a_0, \ldots, a_n}$ be a finite continued fraction in $\R$ of length $n \ge 0$.
Let the partial denominators $a_k > 0$ be strictly positive for $k>0$.
Let $x = [a_0, a_1, \ldots, a_n]$ be its value.
Then $x \ge a_0$, and $x > a_0$ if the length $n \ge 1$.

Proof:
If $n = 0$, we have $x = \sqbrk {a_0} = a_0$ by definition of value.
Let $n>0$.
By definition of value:
:$\sqbrk {a_0, a_1, \ldots, a_n} = a_0 + \dfrac 1 {\sqbrk {a_1, a_2, \ldots, a_n} }$
By Value of Finite Continued Fraction of Strictly Positive Real Numbers is Strictly Positive:
:$\sqbrk {a_1, a_2, \ldots, a_n} > 0$
Thus:
:$\sqbrk {a_0, a_1, \ldots, a_n} = a_0 + \dfrac 1 {\sqbrk {a_1, a_2, \ldots, a_n} } > a_0$
{{qed}}
Theorem: Simple Finite Continued Fraction has Rational Value

Let $n \ge 0$ be a natural number.
Let $\tuple {a_0, \ldots, a_n}$ be a simple finite continued fraction of length $n$.
Then its value $\sqbrk {a_0, \ldots, a_n}$ is a rational number.

Proof:
This will be proved by induction on the number of partial denominators.
For all $n \in \N$, let $\map P n$ be the proposition that the continued fraction $\sqbrk {a_0, a_1, \ldots, a_n}$ has a rational value.
Theorem: Accuracy of Convergents of Convergent Simple Infinite Continued Fraction

Let $C = \tuple {a_0, a_1, \ldots}$ be an simple infinite continued fraction in $\R$.
Let $C$ converge to $x \in \R$.
For $n \ge 0$, let $C_n = \dfrac {p_n} {q_n}$ be the $n$th convergent of $C$, where $p_n$ and $q_n$ are the $n$th numerator and denominator.
Then for all $n \ge 0$:
:$\size {x - \dfrac {p_n} {q_n} } < \dfrac 1 {q_n q_{n + 1} }$

Proof:
We show that either:
:$x \in \closedint {C_n} {C_{n + 1} }$
or:
:$x \in \closedint {C_{n + 1} } {C_n}$
so that the result follows from:
:Difference between Adjacent Convergents of Simple Continued Fraction
:Distance between Point of Real Interval and Endpoint is at most Length
Theorem: Locally Path-Connected Space is not necessarily Locally Injectively Path-Connected

Let $T = \struct {S, \tau}$ be a topological space which is locally path-connected.
Then it is not necessarily the case that $T$ is also a locally injectively path-connected space.

Proof:
Let $T$ be the Either-Or topological space.
From Either-Or Topology is Locally Path-Connected, $T$ is a locally path-connected space.
From Either-Or Topology is not Locally Injectively Path-Connected, $T$ is not a locally injectively path-connected space.
Hence the result.
{{qed}}
Theorem: Locally Connected Space is not necessarily Locally Path-Connected

Let $T = \struct {S, \tau}$ be a topological space which is locally connected.
Then it is not necessarily the case that $T$ is also an locally path-connected space.

Proof:
Let $T$ be a countable finite complement Space.
From Finite Complement Space is Locally Connected, $T$ is a locally connected space.
From Countable Finite Complement Space is not Locally Path-Connected, $T$ is not a locally path-connected space.
Hence the result.
{{qed}}
Theorem: Path-Connected Space is not necessarily Locally Path-Connected

Let $T = \struct {S, \tau}$ be a topological space which is path-connected.
Then it is not necessarily the case that $T$ is also locally path-connected.

Proof:
Let $T$ be the extended topologist's sine curve.
From Extended Topologist's Sine Curve is Path-Connected, $T$ is a path-connected space.
From Extended Topologist's Sine Curve is not Locally Path-Connected, $T$ is not a locally path-connected space.
Hence the result.
{{qed}}
Theorem: Lower Bounds for Denominators of Simple Continued Fraction

Let $n \in \N \cup \{\infty\}$ be an extended natural number.
Let $\left[{a_0, a_1, a_2, \ldots}\right]$ be a simple continued fraction in $\R$ of length $N$.
Let $q_0, q_1, q_2, \ldots$ be its denominators.

Proof:
By Denominators of Simple Continued Fraction are Strictly Increasing, with the possible exception of $1 = q_0 = q_1$, the sequence $\left \langle {q_n}\right \rangle$ is strictly increasing.
Now, since $q_2 > q_1 \ge q_0 = 1$, we have $q_2 \geq 2$.
Then $q_{k+1} \ge q_k + q_{k-1}$ shows that from $q_3$ onwards, the $q_k$s increase in steps of at least $2$.
As $q_3 \ge 3$, it follows that $q_4 \ge 5$.
The result follows.
{{qed}}
Category:Simple Continued Fractions
k91ev6jtyyf4vz9np2blzw87oqpr2ec
Theorem: Equality of Rational Numbers

Let $a, b, c, d$ be integers, with $b$ and $d$ nonzero.
{{TFAE}}
:$(1): \quad$ The rational numbers $\dfrac a b$ and $\dfrac c d$ are equal.
:$(2): \quad$ The integers $a d$ and $b c$ are equal.

Proof:
Note that by definition, $\Q$ is the field of quotients of $\Z$.
Theorem: Locally Path-Connected Space is not necessarily Path-Connected

Let $T = \struct {S, \tau}$ be a topological space which is locally path-connected.
Then it is not necessarily the case that $T$ is also path-connected.

Proof:
Let $\struct {\R, \tau_d}$ be the real number line $\R$ under the usual (Euclidean) topology $\tau_d$.
Let $a, b, c \in \R$ where $a < b < c$.
Let $S$ be the union of the adjacent open intervals:
:$S := \openint a b \cup \openint b c$
Let $T := \struct {S, \tau_S}$ be the subspace composed of $S$ with the subspace topology induced on $S$ by $\tau_d$.
From Union of Adjacent Open Intervals is Locally Path-Connected, $T$ is a locally path-connected space.
From Union of Adjacent Open Intervals is not Path-Connected, $T$ is not a path-connected space.
Hence the result.
{{qed}}
Theorem: Injectively Path-Connected Space is not necessarily Locally Injectively Path-Connected

Let $T = \struct {S, \tau}$ be a topological space which is injectively path-connected.
Then it is not necessarily the case that $T$ is also locally arc-connected.

Proof:
Let $T$ be the extended topologist's sine curve.
From Extended Topologist's Sine Curve is Injectively Path-Connected, $T$ is an injectively path-connected space.
From Extended Topologist's Sine Curve is not Locally Injectively Path-Connected, $T$ is not a locally injectively path-connected space.
Hence the result.
{{qed}}
Theorem: Locally Injectively Path-Connected Space is not necessarily Injectively Path-Connected

Let $T = \struct {S, \tau}$ be a topological space which is locally injectively path-connected.
Then it is not necessarily the case that $T$ is also injectively path-connected.

Proof:
Let $\struct {\R, \tau_d}$ be the real number line $\R$ under the usual (Euclidean) topology $\tau_d$.
Let $a, b, c \in \R$ where $a < b < c$.
Let $S$ be the union of the adjacent open intervals:
:$S := \openint a b \cup \openint b c$
Let $T := \struct {S, \tau_S}$ be the subspace composed of $S$ with the subspace topology induced on $S$ by $\tau_d$.
From Union of Adjacent Open Intervals is Locally Injectively Path-Connected, $T$ is a locally injectively path-connected space.
From Union of Adjacent Open Intervals is not Injectively Path-Connected, $T$ is not an injectively path-connected space.
Hence the result.
{{qed}}
Theorem: Odd Convergents of Simple Continued Fraction are Strictly Decreasing

The odd convergents satisfy $C_1 > C_3 > C_5 > \cdots$

Proof:
Let $ k \ge 3$ be an odd integer.
From Difference between Adjacent Convergents But One of Simple Continued Fraction:
:$C_k - C_{k - 2} = \dfrac {\paren {-1}^k a_k} {q_k q_{k - 2} } = \dfrac {-a_k} {q_k q_{k - 2} }$
By definition of simple continued fraction, $a_k > 0$.
By Convergents of Simple Continued Fraction are Rationals in Canonical Form, $q_k > 0$ and $q_{k - 2} > 0$.
Thus $C_k < C_{k - 2}$.
{{qed}}
Theorem: Even Convergents of Simple Continued Fraction are Strictly Increasing

The even convergents satisfy $C_0 < C_2 < C_4 \cdots$.

Proof:
Let $k \ge 2$ be an even integer.
From Difference between Adjacent Convergents But One of Simple Continued Fraction:
:$C_k - C_{k - 2} = \dfrac {\paren {-1}^k a_k} {q_k q_{k - 2} } = \dfrac {a_k} {q_k q_{k - 2} }$
By definition of simple continued fraction, $a_k > 0$.
By Convergents of Simple Continued Fraction are Rationals in Canonical Form, $q_k > 0$ and $q_{k - 2} > 0$.
Thus $C_k > C_{k - 2}$.
{{qed}}
Theorem: Denominators of Simple Continued Fraction are Strictly Positive

Let $n \in \N \cup \set \infty$ be an extended natural number.
Let $\tuple {a_0, a_1, \ldots}$ be a simple continued fraction in $\R$ of length $n$.
Let $q_0, q_1, q_2, \ldots$ be its denominators.
Then for $0 \leq k \leq n$ we have $q_k > 0$.

Proof:
Follows from:
:$q_0 = 1$ by definition
:Denominators of Simple Continued Fraction are Strictly Increasing.
{{qed}}
Category:Simple Continued Fractions
rwuh6ocjib4wj0e04jrij048mh593gw
Theorem: Simple Finite Continued Fraction is Almost Determined by Value

Let $n,m \geq 0$ be natural number.
Let $\sequence {a_k}_{0 \mathop \le k \mathop \le m}$ and $\sequence {b_k}_{0 \mathop \le k \mathop \le n}$ be simple finite continued fractions in $\R$.
Let $\sequence {a_k}_{0 \mathop \le k \mathop \le m}$ and $\sequence {b_k}_{0 \mathop \le k \mathop \le n}$ have the same value.
Then either:
*$n = m$, and the sequences are equal.
*$n = m + 1$, $a_k = b_k$ for $k < m$, $a_m = b_m-1$ and $b_{m + 1} = 1$
*$m = n + 1$, $a_k = b_k$ for $k < n$, $b_n = a_n-1$ and $a_{n + 1} = 1$

Proof:
{{proof wanted|use Floor of Simple Finite Continued Fraction}}
Theorem: Subgroup Generated by One Element is Set of Powers

Let $G$ be a group.
Let $a \in G$.
Then the subgroup generated by $a$ is the set of powers:
:$\gen a  = \set {a^n : n \in \Z}$

Proof:
By definition, the subgroup generated by $a$ is the intersection of all subgroups containing $a$.
By Powers of Element form Subgroup, the set $H = \set {a^n : n \in \Z}$ is a subgroup.
Thus $\gen a \subseteq H$.
By Power of Element in Subgroup, $H \subseteq \gen a$.
By definition of set equality, $\gen a = H$.
{{qed}}
Theorem: Finite Product Space is Connected iff Factors are Connected

Let $T_1 = \struct {S_1, \tau_1}, T_2 = \struct {S_2, \tau_2}, \dotsc, T_n = \struct {S_n, \tau_n}$ be topological spaces.
Let $T = \ds \prod_{i \mathop = 1}^n T_i$ be the product space of $T_1, T_2, \ldots, T_n$.
Then $T$ is connected {{iff}} each of $T_1, T_2, \ldots, T_n$ are connected.

Proof:
The proof proceeds by induction.
For all $n \in \Z_{\ge 2}$, let $\map P n$ be the proposition:
:$T$ is connected {{iff}} each of $T_1, T_2, \ldots, T_n$ are connected.
Theorem: Equivalence of Definitions of Limit of Vector-Valued Function

Let $D \subseteq \R$ be a subset and $f: D \to \R^n, \map f x = \tuple {\map {f_1} x, \ldots, \map {f_n} x}$ a vector valued function.
Let $x_0 \in \R$ be a limit point of $D$ and $L = (L_1,\ldots,L_n) \in \R^n$.
Then $\ds \lim_{x \mathop \to x_0} \map f x = L$ {{iff}} $\ds \lim_{x \mathop \to x_0} \map {f_j} x = L_j$
In particular the limit of $f$ exists {{iff}} the limit of each component exists.

Proof:
=== Sufficient Condition ===
First assume that $\ds \lim_{x \mathop \to x_0} \map f x = L$.
Let $\epsilon \in \R_{\gt 0}$.
Then there exists $\delta \in \R_{\gt 0}$ such that for all $x \in D$ with $\size {x - x_0} \lt \delta$ we have $\size {\map f x - L} \lt \epsilon$.
Then it follows for all $j = \set {1, \ldots, n}$, that
$\ds \size {\map {f_j} x - L_j} = \sqrt {\paren {\map {f_j} x - L_j}^2} \le \sqrt {\sum_{j \mathop = 1}^n \paren {\map {f_j} x - L_j}^2} = \size {\map f x - L} \lt \epsilon$
And therefore $\ds \lim_{x \mathop \to x_0} \map {f_j} x = L_j$ for all $j$.
{{qed|lemma}}
Theorem: Binary Product in Preadditive Category is Biproduct

Let $A$ be a preadditive category.
Let $a_1, a_2$ be objects of $A$.
Let $(a_1 \times a_2, p_1, p_2)$ be their binary product, assuming it exists.
Let $i_1 : a_1 \to a_1 \times a_2$ be the unique morphism with:
:$p_1 \circ i_1 = 1 : a_1 \to a_1$
:$p_2 \circ i_1 = 0 : a_1 \to a_2$
Let $i_2 : a_1 \to a_1 \times a_2$ be the unique morphism with:
:$p_1 \circ i_2 = 0 : a_2 \to a_1$
:$p_2 \circ i_2 = 1 : a_2 \to a_2$
where $1$ is the identity morphism and $0$ is the zero morphism.
Then $(a_1 \times a_2, i_1, i_2, p_1, p_2)$ is the binary biproduct of $a_1$ and $a_2$.

Proof:
By definition of binary biproduct, it remains to verify that:
:$i_1\circ p_1 + i_2 \circ p_2 = 1 : a_1 \times a_2 \to a_1 \times a_2$.
By definition of binary product and identity morphism, $1 : a_1 \times a_2 \to a_1 \times a_2$ is the unique morphism with:
:$p_1 \circ 1 = p_1$
:$p_2 \circ 1 = p_2$
Thus it remains to verify that $i_1\circ p_1 + i_2 \circ p_2$ satisfies the same condition:
{{begin-eqn}}
{{eqn | l = p_1 \circ (i_1\circ p_1 + i_2 \circ p_2)
      | r = (p_1 \circ i_1) \circ p_1 + (p_1 \circ i_2) \circ p_2
      | c = 
}}
{{eqn | r = 1 \circ p_1 + 0 \circ p_2
      | c = 
}}
{{eqn | r = p_1
      | c = {{Defof|Identity Morphism}}, {{Defof|Bilinear Mapping}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = p_2 \circ (i_1\circ p_1 + i_2 \circ p_2)
      | r = (p_2 \circ i_1) \circ p_1 + (p_2 \circ i_2) \circ p_2
      | c = 
}}
{{eqn | r = 0 \circ p_1 + 1 \circ p_2
      | c = 
}}
{{eqn | r = p_2
      | c = {{Defof|Identity Morphism}}, {{Defof|Bilinear Mapping}}
}}
{{end-eqn}}
{{qed}}
Theorem: Binary Coproduct in Preadditive Category is Biproduct

Let $A$ be a preadditive category.
Let $a_1, a_2$ be objects of $A$.
Let $(a_1 \sqcup a_2, i_1, i_2)$ be their binary coproduct, assuming it exists.
Let $p_1 : a_1 \sqcup a_2 \to a_1$ be the unique morphism with:
:$p_1 \circ i_1 = 1 : a_1 \to a_1$
:$p_1 \circ i_2 = 0 : a_1 \to a_2$
Let $p_2 : a_1 \sqcup a_2 \to a_2$ be the unique morphism with:
:$p_2 \circ i_1 = 0 : a_2 \to a_1$
:$p_2 \circ i_2 = 1 : a_2 \to a_2$
where $1$ is the identity morphism and $0$ is the zero morphism.
Then $(a_1 \sqcup a_2, i_1, i_2, p_1, p_2)$ is the binary biproduct of $a_1$ and $a_2$.

Proof:
By definition of binary biproduct, it remains to verify that:
:$i_1\circ p_1 + i_2 \circ p_2 = 1 : a_1 \sqcup a_2 \to a_1 \sqcup a_2$.
By definition of binary coproduct and identity morphism, $1 : a_1 \sqcup a_2 \to a_1 \sqcup a_2$ is the unique morphism with:
:$1 \circ i_1 = i_1$
:$1 \circ i_2 = i_2$
Thus it remains to verify that $i_1\circ p_1 + i_2 \circ p_2$ satisfies the same condition:
{{begin-eqn}}
{{eqn | l = (i_1\circ p_1 + i_2 \circ p_2) \circ i_1
      | r = i_1 \circ (p_1 \circ i_1) + i_2 \circ (p_2 \circ i_1)
      | c = 
}}
{{eqn | r = i_1 \circ 1 + i_2 \circ 0
      | c = 
}}
{{eqn | r = i_1
      | c = {{Defof|Identity Morphism}}, {{Defof|Bilinear Mapping}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = (i_1\circ p_1 + i_2 \circ p_2) \circ i_2
      | r = i_1 \circ (p_1 \circ i_2) + i_2 \circ (p_2 \circ i_2)
      | c = 
}}
{{eqn | r = i_1 \circ 0 + i_2 \circ 1
      | c = 
}}
{{eqn | r = i_2
      | c = {{Defof|Identity Morphism}}, {{Defof|Bilinear Mapping}}
}}
{{end-eqn}}
{{qed}}