avewright/proofwiki-math huggingface dataset:
Theorem: Increasing Real Function has Countably Many Discontinuities

Let $f: \R \to \R$ be an increasing real function.
Then $f$ has at most countably many discontinuities.

Proof:
Let $D \subseteq \R$ be the set of discontinuities of $f$. 
From Limit of Monotone Real Function: Increasing: Corollary, we have that:
:$\ds \lim_{x \mathop \to b^-} \map f x = l_x$ and $\ds \lim_{x \mathop \to b^+} \map f x = r_x$
both exist for each $x \in \R$.
Further:
:$l_x \le r_x$ 
Let $x \in D$. 
Then since:
:$f$ is discontinuous at $x$
:both the left and right limit exist at $x$
we have:
:$l_x \ne r_x$
Hence:
:$l_x < r_x$.
We argue that the open intervals $\openint {l_x} {r_x}$ are disjoint.
Let $x, y \in D$ be such that $x < y$. 
Let $\xi \in \R$ be such that $x < \xi < y$.
Then by {{Corollary|Limit of Increasing Function}}, we have:
:$r_x \le \map f \xi \le l_y$ 
Hence if $x < y$, we have:
:$\openint {l_x} {r_x} \cap \openint {l_y} {r_y} = \O$
By swapping $x$ and $y$, we have:
:$\openint {l_x} {r_x} \cap \openint {l_y} {r_y} = \O$
for $x \ne y$ with $x, y \in D$. 
Hence $\DD = \set {\openint {l_x} {r_x} : x \in D}$ is a set of disjoint open intervals.
From:
:Real Number Line is Separable Space
:Separable Space satisfies Countable Chain Condition
$\DD$ is countable.
Since the map $g : D \to \DD$ defined by:
:$\map g x = \openint {l_x} {r_x}$
for each $x \in D$ is a bijection, it follows that $D$ is countable.
{{qed}}
Theorem: Tartaglia's Formula

Let $T$ be a tetrahedron with vertices $\mathbf d_1, \mathbf d_2, \mathbf d_3$ and $\mathbf d_4$.
For all $i$ and $j$, let the distance between $\mathbf d_i$ and $\mathbf d_j$ be denoted $d_{ij}$.
Then the volume $V_T$ of $T$ satisfies:
$\quad V_T^2 = \dfrac 1 {288} \det \ \begin{vmatrix}  
0 & 1 & 1 & 1 & 1 \\
1 & 0 & d_{12}^2 & d_{13}^2 & d_{14}^2 \\
1 & d_{12}^2 & 0 & d_{23}^2 & d_{24}^2 \\
1 & d_{13}^2 & d_{23}^2 & 0 & d_{34}^2 \\
1 & d_{14}^2 & d_{24}^2 & d_{34}^2 & 0
\end{vmatrix}$

Proof:
A proof of Tartaglia's Formula will be found in a proof of the Value of Cayley-Menger Determinant as a tetrahedron is a $3$-simplex.
{{proof wanted}}
Theorem: 0 in B-Algebra is Left Cancellable Element

Let $\struct {X, \circ}$ be a $B$-Algebra.
Then:
:$\forall x, y \in X: 0 \circ x = 0 \circ y \implies x = y$

Proof:
Let $x, y \in X$ and let $0 \circ x = 0 \circ y$.
Then:
{{begin-eqn}}
{{eqn | l = 0
      | r = x \circ x
      | c = {{B-algebra-axiom|1}}
}}
{{eqn | r = \paren {x \circ x} \circ 0
      | c = {{B-algebra-axiom|2}}
}}
{{eqn | r = x \circ \paren {0 \circ \paren {0 \circ x} }
      | c = {{B-algebra-axiom|3}}
}}
{{eqn | r = x \circ \paren {0 \circ \paren {0 \circ y} }
      | c = {{hypothesis}}
}}
{{eqn | r = \paren {x \circ y} \circ 0
      | c = {{B-algebra-axiom|3}}
}}
{{eqn | r = x \circ y
      | c = {{B-algebra-axiom|2}}
}}
{{end-eqn}}
So we have shown:
:$\forall x, y \in X: 0 \circ x = 0 \circ y \implies x \circ y = 0$
From $B$-Algebra Identity: $x \circ y = 0 \iff x = y$:
:$\forall x, y \in X: 0 \circ x = 0 \circ y \implies x = y$
Hence the result.
{{qed}}
Category:B-Algebras
4pvsit62v0jmrto07t9079nz4gcu5qd
Theorem: B-Algebra Identity: 0(0x)=x

Let $\struct {X, \circ}$ be a $B$-algebra. 
Then:
:$\forall x \in X: 0 \circ \paren {0 \circ x} = x$

Proof:
Let $x \in X$.
Then:
{{begin-eqn}}
{{eqn | l = 0 \circ x
      | r = \paren {0 \circ x} \circ 0
      | c = {{B-algebra-axiom|2}}
}}
{{eqn | r = 0 \circ \paren {0 \circ \paren {0 \circ x} }
      | c = {{B-algebra-axiom|3}}
}}
{{eqn | ll= \leadsto
      | l = x
      | r = 0 \circ \paren {0 \circ x}
      | c = $0$ in $B$-Algebra is Left Cancellable Element
}}
{{end-eqn}}
{{qed}}
Category:B-Algebras
gmi2j80y4bz4rfow7dhw28k81qzqp39
Theorem: B-Algebra Induces Group

Let $\struct {X, \circ}$ be a $B$-algebra.
Let $*$ be the binary operation on $X$ defined as:
:$\forall a, b \in X: a * b := a \circ \paren {0 \circ b}$
Then the algebraic structure $\struct {X, *}$ is a group such that:
:$\forall x \in X: 0 \circ x$ is the inverse element of $x$ under $*$.
That is:
:$\forall a, b \in X: a * b^{-1} := a \circ b$

Proof:
Let $x, y, z \in X$:
We will show that $\struct {X, *}$ satisfies each of the group axioms in turn:
Theorem: Klein Four-Group as Order 2 Matrices

Let $G$ be the set of order $2$ square matrices:
:$G = \set {I, A, B, C}$
where:
:$I = \begin{bmatrix} 1 & 0 \\ 0 & 1 \end{bmatrix}, \quad A = \begin{bmatrix} 1 & 0 \\ 0 & -1 \end{bmatrix}, \quad B = \begin{bmatrix} -1 & 0 \\ 0 & 1 \end{bmatrix}, \quad C = \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix}$
Then the algebraic structure $\struct {G, \times}$, where $\times$ denotes (conventional) matrix multiplication, forms the Klein four-group.

Proof:
From Unit Matrix is Unity of Ring of Square Matrices, $I$ can be identified as the unit matrix of order $2$.
Then:
:$A^2 = \begin{bmatrix} 1 & 0 \\ 0 & -1 \end{bmatrix} \begin{bmatrix}  1 & 0 \\ 0 & -1 \end{bmatrix} = \begin{bmatrix}  1 & 0 \\ 0 &  1 \end{bmatrix} = I$
:$A B = \begin{bmatrix} 1 & 0 \\ 0 & -1 \end{bmatrix} \begin{bmatrix} -1 & 0 \\ 0 &  1 \end{bmatrix} = \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix} = C$
:$A C = \begin{bmatrix} 1 & 0 \\ 0 & -1 \end{bmatrix} \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix} = \begin{bmatrix} -1 & 0 \\ 0 &  1 \end{bmatrix} = B$
:$B^2 = \begin{bmatrix} -1 & 0 \\ 0 & 1 \end{bmatrix} \begin{bmatrix} -1 & 0 \\ 0 &  1 \end{bmatrix} = \begin{bmatrix}  1 & 0 \\ 0 &  1 \end{bmatrix} = I$
:$B A = \begin{bmatrix} -1 & 0 \\ 0 & 1 \end{bmatrix} \begin{bmatrix}  1 & 0 \\ 0 & -1 \end{bmatrix} = \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix} = C$
:$B C = \begin{bmatrix} -1 & 0 \\ 0 & 1 \end{bmatrix} \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix} = \begin{bmatrix}  1 & 0 \\ 0 & -1 \end{bmatrix} = A$
:$C^2 = \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix} \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix} = \begin{bmatrix}  1 & 0 \\ 0 &  1 \end{bmatrix} = I$
:$C A = \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix} \begin{bmatrix}  1 & 0 \\ 0 & -1 \end{bmatrix} = \begin{bmatrix} -1 & 0 \\ 0 &  1 \end{bmatrix} = B$
:$C B = \begin{bmatrix} -1 & 0 \\ 0 & -1 \end{bmatrix} \begin{bmatrix} -1 & 0 \\ 0 &  1 \end{bmatrix} = \begin{bmatrix}  1 & 0 \\ 0 & -1 \end{bmatrix} = A$
Putting this together into a Cayley table:
:$\begin{array}{c|cccccc}
  & I & A & B & C \\
\hline
I & I & A & B & C \\
A & A & I & C & B \\
B & B & C & I & A \\
C & C & B & A & I \\
\end{array}$
it is verified by inspection that this is an instance of the Klein four-group.
{{qed}}
Theorem: F-Sigma Sets Closed under Union

Let $T = \struct {S, \tau}$ be a topological space.
Let $F, F'$ be $F_\sigma$ sets of $T$.
Then their union $F \cup F'$ is also an $F_\sigma$ set of $T$.

Proof:
By definition of $F_\sigma$ set, there exist sequences $\sequence {C_n}_{n \mathop \in \N}$ and $\sequence {C'_n}_{n \mathop \in \N}$ of closed sets of $T$ such that:
:$F = \ds \bigcup_{n \mathop \in \N} C_n$
:$F' = \ds \bigcup_{n \mathop \in \N} C'_n$
By General Self-Distributivity of Set Union, we have:
:$F \cup F' = \ds \bigcup_{n \mathop \in \N} \paren {C_n \cup C'_n}$
By Finite Union of Closed Sets is Closed in Topological Space, $C_n \cup C'_n$ is closed, for all $n \in \N$.
Thus $F \cup F'$ is seen to be an $F_\sigma$ set.
{{qed}}
Theorem: F-Sigma Sets Closed under Intersection

Let $T = \struct {S, \tau}$ be a topological space.
Let $F, F'$ be $F_\sigma$ sets of $T$.
Then their intersection $F \cap F'$ is also a $F_\sigma$ set of $T$.

Proof:
By definition of $F_\sigma$ set, there exist sequences $\sequence {C_n}_{n \mathop \in \N}$ and $\sequence {C'_n}_{n \mathop \in \N}$ of closed sets of $T$ such that:
:$F = \ds \bigcup_{n \mathop \in \N} C_n$
:$F' = \ds \bigcup_{n \mathop \in \N} C'_n$
Now compute:
{{begin-eqn}}
{{eqn | l = F \cap F'
      | r = \bigcup_{n \mathop \in \N} \paren {C_n \cap F'}
      | c = Intersection Distributes over Union: General Result
}}
{{eqn | r = \bigcup_{n \mathop \in \N} \bigcup_{m \mathop \in \N} \paren {C_n \cap C'_m}
      | c = Intersection Distributes over Union: General Result
}}
{{end-eqn}}
By Intersection of Closed Sets is Closed in Topological Space, $C_n \cap C'_m$ is closed, for all $n, m \in \N$.
By Cartesian Product of Countable Sets is Countable, $\N \times \N$ is countable.
Thus $F \cap F'$ is seen to be a countable union of closed sets, hence a $F_\sigma$ set.
{{qed}}
Theorem: G-Delta Sets Closed under Union

Let $T = \struct {S, \tau}$ be a topological space.
Let $G, G'$ be $G_\delta$ sets of $T$.
Then their union $G \cup G'$ is also a $G_\delta$ set of $T$.

Proof:
By definition of $G_\delta$ set, there exist sequences $\sequence {U_n}_{n \mathop \in \N}$ and $\sequence {U'_n}_{n \mathop \in \N}$ of open sets of $T$ such that:
:$G = \ds \bigcap_{n \mathop \in \N} U_n$
:$G' = \ds \bigcap_{n \mathop \in \N} U'_n$
Now compute:
{{begin-eqn}}
{{eqn | l = G \cup G'
      | r = \bigcap_{n \mathop \in \N} \paren {U_n \cup G'}
      | c = Intersection Distributes over Union: General Result
}}
{{eqn | r = \bigcap_{n \mathop \in \N} \bigcap_{m \mathop \in \N} \paren {U_n \cup U'_m}
      | c = Intersection Distributes over Union: General Result
}}
{{end-eqn}}
By axiom $(1)$ of a topology, $U_n \cup U'_m$ is open, for all $n, m \in \N$.
By Cartesian Product of Countable Sets is Countable, $\N \times \N$ is countable.
Thus $G \cup G'$ is seen to be a $G_\delta$ set.
{{qed}}
Theorem: G-Delta Sets Closed under Intersection

Let $T = \struct {S, \tau}$ be a topological space.
Let $G, G'$ be $G_\delta$ sets of $T$.
Then their intersection $G \cap G'$ is also a $G_\delta$ set of $T$.

Proof:
By definition of $G_\delta$ set, there exist sequences $\sequence {U_n}_{n \mathop \in \N}$ and $\sequence {U'_n}_{n \mathop \in \N}$ of open sets of $T$ such that:
:$G = \ds \bigcap_{n \mathop \in \N} U_n$
:$G' = \ds \bigcap_{n \mathop \in \N} U'_n$
By General Self-Distributivity of Intersection, we have:
:$G \cap G' = \ds \bigcap_{n \mathop \in \N} \paren {U_n \cap U'_n}$
By Intersection of Closed Sets is Closed in Topological Space, $U_n \cap U'_m$ is closed, for all $n, m \in \N$.
Thus $G \cap G'$ is seen to be a $G_\delta$ set.
{{qed}}
Theorem: F-Sigma Sets form Lattice

Let $T = \struct {S, \tau}$ be a topological space.
Let $\FF$ be the collection of all $F_\sigma$ sets of $T$.
Then $\struct {\FF, \subseteq}$ is a lattice, where $\subseteq$ denotes the subset relation.

Proof:
From Subset Relation is Ordering, $\subseteq$ is an ordering on $\FF$.
Let $F, F'$ be $F_\sigma$ sets of $T$.
We have $F_\sigma$ Sets Closed under Union, so that $F \cup F' \in \FF$.
From Union is Smallest Superset and Subset of Union, it follows that $F \cup F'$ is the supremum of $F$ and $F'$.
Similarly, we have $F_\sigma$ Sets Closed under Intersection, and so $F \cap F' \in \FF$.
From Intersection is Largest Subset and Intersection is Subset, it follows that $F \cap F'$ is the infimum of $F$ and $F'$.
Thus any two elements of $\FF$ are seen to have both a supremum and an infimum in $\FF$.
Hence $\struct {\FF, \subseteq}$ is a lattice.
{{qed}}
Theorem: G-Delta Sets form Lattice

Let $T = \struct {S, \tau}$ be a topological space.
Let $\GG$ be the collection of all $G_\delta$ sets of $T$.
Then $\struct {\GG, \subseteq}$ is a lattice, where $\subseteq$ denotes the subset relation.

Proof:
From Subset Relation is Ordering, $\subseteq$ is an ordering on $\GG$.
Let $G, G'$ be $G_\delta$ sets of $T$.
We have $G_\delta$ Sets Closed under Union, so that $G \cup G' \in \GG$.
From Union is Smallest Superset and Subset of Union, it follows that $G \cup G'$ is the supremum of $G$ and $G'$.
Similarly, we have $G_\delta$ Sets Closed under Intersection, and so $G \cap G' \in \GG$.
From Intersection is Largest Subset and Intersection is Subset, it follows that $G \cap G'$ is the infimum of $G$ and $G'$.
Thus any two elements of $\GG$ are seen to have both a supremum and an infimum in $\GG$.
Hence $\struct {\GG, \subseteq}$ is a lattice.
{{qed}}
Theorem: Bounded Sequence in Euclidean Space has Convergent Subsequence

Let $\sequence {x_i}_{i \mathop \in \N}$ be a bounded sequence in the Euclidean space $\R^n$.
Then some subsequence of $\sequence {x_i}_{i \mathop \in \N}$ converges to a limit.

Proof:
Denote with $d$ the Euclidean metric on $\R^n$.
Because $\sequence {x_i}_{i \mathop \in \N}$ is bounded, we find $v \in \R^n$ and $\epsilon \in \R_{>0}$ such that:
:$\forall i \in \N: \map d {v, x_i} < \epsilon$
Therefore, all $x_i$ are members of the closed $\epsilon$-ball $S = \map {B_\epsilon^-} v$.
By Closed Ball in Euclidean Space is Compact, $S$ is compact.
Thus $\sequence {x_i}_{i \mathop \in \N}$ can be considered as a sequence in the compact metric space $\struct {S, d \restriction_{S \times S} }$.
By Compact Subspace of Metric Space is Sequentially Compact in Itself, $\sequence {x_i}_{i \mathop \in \N}$ has a convergent subsequence in $S$.
In particular, since $S$ is a metric subspace of $\R^n$, it follows that $\sequence {x_i}_{i \mathop \in \N}$ has a convergent subsequence in $\R^n$ as well.
{{qed}}
Theorem: Bounded Sequence in Euclidean Space has Convergent Subsequence

Let $\sequence {x_i}_{i \mathop \in \N}$ be a bounded sequence in the Euclidean space $\R^n$.
Then some subsequence of $\sequence {x_i}_{i \mathop \in \N}$ converges to a limit.

Proof:
Let the range of $\sequence {x_i}$ be $S$.
By Closure of Bounded Subset of Metric Space is Bounded $\map \cl S$ is bounded in $\R^n$.
By Topological Closure is Closed, $\map \cl S$ is closed in $\R^n$.
By the Heine-Borel Theorem, $S$ is compact.
The result follows from Compact Subspace of Metric Space is Sequentially Compact in Itself.
{{qed}}
Theorem: Bounded Sequence in Euclidean Space has Convergent Subsequence

Let $\sequence {x_i}_{i \mathop \in \N}$ be a bounded sequence in the Euclidean space $\R^n$.
Then some subsequence of $\sequence {x_i}_{i \mathop \in \N}$ converges to a limit.

Proof:
We have that all norms on $\R^n$ are equivalent.
Choose the Euclidean norm $\norm {\, \cdot \,}_2$.
Proof by induction will be used.
=== Basis for the induction ===
Let $n = 1$.
Then the proof is given by Bolzano-Weierstrass theorem.
=== Induction hypothesis ===
Suppose, a bounded sequence $\sequence {\boldsymbol x_i}_{i \mathop \in \N}$ in $\R^n$ has a convergent subsequence $\sequence {\boldsymbol x_{i_k}}_{k \mathop \in \N}$.
Then we have to show, that the same property holds for $\R^{n + 1}$.
=== Induction step ===
Let $\sequence {\mathbf x_n}_{n \mathop \in \N}$ be a bounded sequence in $\R^{n + 1}$.
Split $\mathbf x_n$ into its first $n$ components and the last one:
:$\mathbf x_n := \tuple {\boldsymbol \alpha_n, \beta_n}$
where $\boldsymbol \alpha_n \in \R^n$ and $\beta_n \in \R$
Then:
{{begin-eqn}}
{{eqn | l = \norm {\boldsymbol \alpha_n}_2
      | o = \le
      | r = \sqrt {\norm {\boldsymbol \alpha_n}_2^2 + \beta_n^2}
}}
{{eqn | r = \norm {\mathbf x_n}_2
      | c = {{defof|Euclidean Norm}}
}}
{{end-eqn}}
Hence, $\sequence {\boldsymbol \alpha_n}_{n \mathop \in \N}$ is a bounded sequence in $\R^n$.
By induction hypothesis, it has a convergent subsequence $\sequence {\mathbf \alpha_{n_k} }_{k \mathop \in \N}$.
Denote its limit by $\alpha$.
Furthermore:
{{begin-eqn}}
{{eqn | l = \norm {\beta_n}_2
      | o = \le
      | r = \sqrt {\norm {\boldsymbol \alpha_n}_2^2 + \beta_n^2}
}}
{{eqn | r = \norm {\mathbf x_n}_2
      | c = {{defof|Euclidean Norm}}
}}
{{end-eqn}}
Therefore, $\sequence {\beta_n}_{n \mathop \in \N}$ is bounded.
By Bolzano-Weierstrass theorem, $\sequence {\beta_n}_{n \mathop \in \N}$ has a convergent subsequence  $\sequence {\beta_{n_k}}_{k \mathop \in \N}$.
Denote its limit by $\beta$.
Then we have that:
{{begin-eqn}}
{{eqn | l = \lim_{k \to \infty} \mathbf x_{n_k}
      | r = \lim_{k \to \infty} \tuple {\boldsymbol \alpha_{n_k}, \beta_{n_k} }
}}
{{eqn | r = \tuple {\boldsymbol \alpha, \beta}
      | rr = \in \R^{n + 1}
}}
{{end-eqn}}
Hence, the bounded sequence $\sequence {\mathbf x_n}_{n \mathop \in \N}$ has a convergent subsequence $\sequence {\mathbf x_{n_k}}_{k \mathop \in \N}$.
{{qed}}
Theorem: Exponential Growth Equation/Special Case

All solutions of the differential equation $y' = y$ take the form $y = C e^x$.

Proof:
Let $\map f x = C e^x$.
Then by Derivative of Exponential Function:
:$\map {f'} x = \map f x$
From Exponential of Zero:
:$\map f 0 = C$
Hence $C e^x$ is a solution of $y' = y$.
Now suppose that a function $f$ satisfies $\map {f'} x = \map f x$. 
Consider $\map h x = \map f x e^{-x}$.
By the Product Rule for Derivatives:
{{begin-eqn}}
{{eqn | l = \map {h'} x
      | r = \map {f'} x e^{-x} - \map f x e^{-x}
}}
{{eqn | r = \map f x e^{-x} - \map f x e^{-x}
}}
{{eqn | r = 0
}}
{{end-eqn}}
From Zero Derivative implies Constant Function, $h$ must be a constant function.
Therefore, $\map h x = \map h 0 = \map f 0$.
Recalling the definition of $h$, it follows that:
:$\map f x = \map f 0 e^x$
{{qed}}
Theorem: Existence-Uniqueness Theorem for Homogeneous First-Order Differential Equation

Let $\map P x$ be a continuous function on an open interval $I \subseteq \R$.
Let $a \in I$.
Let $b \in \R$.
Let $\map f x = y$ be a function satisfying the differential equation:
:$y' + \map P x y = 0$
and the initial condition:
:$\map f a = b$
Then there exists a unique function satisfying these initial conditions on the interval $I$.
That function takes the form:
:$\map f x = b e^{-\map A x}$
where:
:$\ds \map A x = -\int_a^x \map P t \rd t$

Proof:
=== Existence ===
Differentiating $\map f x = b e^{-\map A x}$ {{WRT|Differentiation}} $x$:
{{begin-eqn}}
{{eqn | l = \map {f'} x
      | r = b e^{-\map A x} \cdot \paren {-\map {A'} x}
      | c = 
}}
{{eqn | r = -b \map P x e^{-\map A x}
      | c = 
}}
{{eqn | r = -\map P x \map f x
      | c = 
}}
{{end-eqn}}
So thedifferential equation becomes:
:$\map {f'} x + \map P x \map f x = -\map P x \map f x + \map P x \map f x = 0$
For the initial condition:
{{begin-eqn}}
{{eqn | l = \map f a
      | r = b e^{-\map A a}
      | c = 
}}
{{eqn | r = b e^{-\int_a^a \map P x \rd x}
      | c = 
}}
{{eqn | r = b e^0
      | c = 
}}
{{eqn | r = b
      | c = 
}}
{{end-eqn}}
Thus such a function exists satisfying the conditions.
{{qed|lemma}}
Theorem: Existence-Uniqueness Theorem for First-Order Differential Equation

Let $P$ and $Q$ be continuous real functions on some open interval $I \subseteq \R$.
Let $a \in I$.
Let $b \in \R$.
There exists a unique function $\map f x = y$ on $I$ that satisfies the linear first order ordinary differential equation: 
:$(1): \quad y' + \map P x y = \map Q x$
along with the initial condition:
:$\map f a = b$
This function is:
:$\ds \map f x = be^{-\map A x} + e^{-\map A x} \int_a^x \map Q t e^{\map A t} \rd t$
where $\ds \map A x = \int_a^x \map P t \rd t$

Proof:
=== Existence ===
Because $P$ and $Q$ are continuous, they are integrable.
Hence we may use the Fundamental Theorem of Calculus.
{{begin-eqn}}
{{eqn | l = \map {f'} x
      | r = -b \map P x e^{-\map A x} - \map P x e^{-\map A x} \int_a^x \map Q t e^{\map A t} \rd t + e^{-\map A x} \map Q x e^{\map A x}
      | c = Product Rule for Derivatives
}}
{{eqn | r = -\map P x \paren {b e^{-\map A x} + e^{-\map A x} \int_a^x \map Q t e^{\map A t} \rd t} + \map Q x
      | c = by factoring
}}
{{eqn | r = -\map P x \map f x + \map Q x
      | c = by substitution
}}
{{end-eqn}}
Therefore:
:$\map {f'} x + \map P x \map f x = \map Q x$
For the initial condition:
{{begin-eqn}}
{{eqn | l = \map f a
      | r = b e^{-\map A a} + e^{-\map A a} \int_a^a \map Q t e^{\map A t}dt
      | c = substituting of $a$ into $\map f x$
}}
{{eqn | r = b e^0 + e^0 \cdot 0
      | c = Integral on Zero Interval
}}
{{eqn | r = b
      | c = simplification
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Proper Well-Ordering determines Smallest Elements

Let $S$ be a class.
Let $\preceq$ be a proper well-ordering on $S$.
Let $B$ be a nonempty subclass of $S$.
Then $B$ has a $\preceq$-smallest element.

Proof:
Because $B \ne \O$ it follows that $B$ has an element $x$.
If $x$ is the smallest element of $B$ then the theorem holds.
Otherwise, there is an element $y \in B$ such that $x \npreceq y$.
By Well-Ordering is Total Ordering, $y \prec x$.
Thus $S_x$, the $\preceq$-initial segment of $x$, is not empty.
By the hypothesis, $S_x$ is a set.
By Intersection is Subset, $B \cap S_x \subseteq S_x$
Thus by the subset axiom, $B \cap S_x$ is a set.
Thus by the definition of proper well-ordering, $B \cap S_x$ has a smallest element $a$.
Let $z$ be any element of $B$.
{{AimForCont}} $z \prec a$.
Then by Extended Transitivity, $z \prec x$, so $z \in B \cap S_x$.
But this contradicts the fact that $a$ is the smallest element of $B \cap S_x$.
Thus $z \nprec a$.
Since $\preceq$ is a total ordering, $a \preceq z$.
As this holds for all $z \in B$, $a$ is the smallest element of $B$.
{{qed}}
Theorem: Well-Ordered Induction

Let $\struct {A, \prec}$ be a strict well-ordering.
For all $x \in A$, let the $\prec$-initial segment of $x$ be a small class.
Let $B$ be a class such that $B \subseteq A$.
Let:
:$(1): \quad \forall x \in A: \paren {\paren {A \mathop \cap \map {\prec^{-1} } x} \subseteq B \implies x \in B}$
Then:
:$A = B$
That is, if a property passes from the initial segment of $x$ to $x$, then this property is true for all $x \in A$.

Proof:
{{AimForCont}} that $A \nsubseteq B$.
Then:
:$A \setminus B \ne 0$.
By Proper Well-Ordering Determines Smallest Elements, $A \setminus B$ must have some $\prec$-minimal element.
Thus:
:$\ds \exists x \in \paren {A \setminus B}: \paren {A \setminus B} \cap \map {\prec^{-1} } x = \O$
implies that:
:$A \cap \map {\prec^{-1} } x \subseteq B$
Hence this fulfils the hypothesis for $(1)$.
We have that $x \in A$.
so by $(1)$:
:$x \in B$
But this contradicts the fact that $x \in \paren {A \setminus B}$.
Thus by Proof by Contradiction:
:$A \subseteq B$
It follows by definition of set equality that:
:$A = B$
{{qed}}
Theorem: Subset of Ordinals has Minimal Element

Let $A$ be an ordinal (we shall allow $A$ to be a proper class).
Let $B$ be a nonempty subset of $A$.
Then $B$ has an $\Epsilon$-minimal element.
{{explain|$\Epsilon$}}
That is:
:$\exists x \in B: B \cap x = \O$

Proof:
We have that $\Epsilon$ creates a well-ordering on any ordinal.
Also, the initial segments of $x$ are sets.
Therefore from Proper Well-Ordering Determines Smallest Elements:
:$B$ has an $\Epsilon$-minimal element.
Theorem: Union of Set of Ordinals is Ordinal

Let $A$ be a set of ordinals.
Then $\bigcup A$ is an ordinal.

Proof:
By the Axiom of Replacement, $\map F y$ is a set.
Thus by the Axiom of Unions, $\bigcup \map F y$ is a set.
By Union of Set of Ordinals is Ordinal, $\bigcup \map F y$ is transitive.
{{mistake|This link is the result which needs to be proved. Something with transitive instead?}}
By the epsilon relation $\bigcup \map F y$ is well-ordered.
{{explain|What does the above sentence mean?}}
Thus $\bigcup \map F y$ is a member of $\On$, the class of all ordinals.
{{qed}}
Theorem: Union of Set of Ordinals is Ordinal

Let $A$ be a set of ordinals.
Then $\bigcup A$ is an ordinal.

Proof:
By Class of All Ordinals is Well-Ordered by Subset Relation, a set of ordinals forms a chain.
The result then follows from Union of Chain of Ordinals is Ordinal.
Theorem: Union of Set of Ordinals is Ordinal

Let $A$ be a set of ordinals.
Then $\bigcup A$ is an ordinal.

Proof:
{{begin-eqn}}
{{eqn | l = x 
      | o = \in
      | r = \bigcup A
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists y \in A
      | l = x
      | o = \in
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists y \subseteq \bigcup A
      | l = x
      | o = \subseteq 
      | r = y
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | o = \subseteq
      | r = \bigcup A
      | c = 
}}
{{end-eqn}}
{{explain|Why does the third line follow from the second?}}
From this, we conclude that $\bigcup A$ is a transitive set.
From Class is Transitive iff Union is Subclass, it follows that:
:$\bigcup A \subseteq A \subseteq \On$
Note that the above applies as well to sets as it does to classes.
By Subset of Well-Ordered Set is Well-Ordered, $A$ is also well-ordered by $\Epsilon$.
Thus by Alternative Definition of Ordinal, $\bigcup A$ is an ordinal.
{{qed}}