avewright/proofwiki-math huggingface dataset:
Theorem: Naturally Ordered Semigroup forms Peano Structure

Let $\struct {S, \circ, \preceq}$ be a naturally ordered semigroup.
Let $0 \in S$ be the zero of $S$.
Let $1 \in S$ be the one of $S$.
Let $s: S \to S$ be the mapping defined as:
:$\map s n := n \circ 1$
Then $\struct {S, 0, s}$ is a Peano structure.

Proof:
We verify Peano's axioms in turn.
First, suppose that $\map s m = \map s n$ for some $m, n \in S$.
That is:
:$m \circ 1 = n \circ 1$
By Axiom $(\text {NO} 2)$, it follows that $m = n$.
Hence Axiom $(\text P 3)$ holds.
{{AimForCont}} that $\map s n = 0$ for some $n \in S$.
That is:
:$n \circ 1 = 0$
By Sum with One is Immediate Successor in Naturally Ordered Semigroup, this would imply:
:$n \prec 0$
However, this contradicts the definition of $0$.
Consequently, Axiom $(\text P 4)$ is satisfied.
Finally, let $A \subseteq S$ be such that $0 \in A$ and, for all $n \in S$:
:$n \in A \implies \map s n \in A$
Define $T := S \setminus A$.
{{AimForCont}} $T \ne \O$.
Then by Axiom $(\text {NO} 3)$, $T$ has a minimal element $n$.
By assumption, $0 \in A$, so that $n \ne 0$.
Therefore, by definition of $1$:
:$1 \preceq n$
By Ordering in terms of Addition, there exists a $p \in S$ such that:
:$p \circ 1 = n$
since $\circ$ is commutative.
By Sum with One is Immediate Successor in Naturally Ordered Semigroup:
:$p \prec n$
Since $n$ is the minimal element of $T$, it follows that $p \notin T$.
Therefore, by definition, $p \in A$.
But by assumption on $A$, this means that $n = p \circ 1 \in A$.
This is a contradiction, hence $T = \O$.
That is to say, $A = S$, and Axiom $(\text P 5)$ holds as well.
Having verified all the axioms, we conclude that $\struct {S, 0, s}$ is a Peano structure.
{{qed}}
Category:Naturally Ordered Semigroup
Category:Peano's Axioms
j4yi4h9e3xfztxtgyrihi0so0y1xep0
Theorem: Divisibility of Elements in Geometric Sequence of Integers

Let $Q_n = \sequence {a_j}_{0 \mathop \le j \mathop \le n}$ be a geometric sequence of integers.
Let $j \ne k$.
Then:
:$\paren {\exists j \in \set {0, 1, \ldots, n - 1}: a_j \divides a_{j + 1} } \iff \paren {\forall j, k \in \set {0, 1, \ldots, n}, j < k: a_j \divides a_k}$
where $\divides$ denotes integer divisibility.
That is:
:One term of a geometric sequence of integers is the divisor of the next term
{{iff}}
:All terms are divisors of all later terms.

Proof:
Let $a_j \divides a_{j + 1}$ for some $j \in \set {0, 1, \ldots, n - 1}$.
Then by definition of integer divisibility:
:$\exists r \in \Z: r a_j = a_{j + 1}$
Thus the common ratio of $Q_n$ is $r$.
So by definition of geometric sequence:
:$\forall j, k \in \set {0, 1, \ldots, n}, j < k: r^{k - j} a_j = a_k$
and so $a_j \divides a_k$.
The converse is trivial.
{{qed}}
Category:Geometric Sequences of Integers
9wvw4e48rd7y1uyoccxqq5hzi2ue3tc
Theorem: Form of Geometric Sequence of Integers from One

Let $Q_n = \sequence {a_j}_{0 \mathop \le j \mathop \le n}$ be a geometric sequence consisting of integers only.
Let $a_0 = 1$.
Then the $j$th term of $Q_n$ is given by:
:$a_j = a^j$
where:
:the common ratio of $Q_n$ is $a$
:$a = a_1$.
Thus:
:$Q_n = \tuple {1, a, a^2, \ldots, a^n}$

Proof:
From Form of Geometric Sequence of Integers, the $j$th term of $Q_n$ is given by:
:$a_j = k q^j p^{n - j}$
where:
:the common ratio of $Q_n$ expressed in canonical form is $\dfrac q p$
:$k$ is an integer.
As $a_0 = 1$ it follows that:
:$1 = k p^{n - j}$
from which it follows that:
:$k = 1$
:$p = 1$
and the common ratio of $Q_n$ is $q$.
Thus:
:$a_1 = q$
Setting $a = a_1$ yields the result as stated.
{{qed}}
Category:Geometric Sequences of Integers
oe6s3lsppor1abhbcntfeh882woz8za
Theorem: Divisors of Power of Prime

Let $p$ be a prime number.
Let $n \in \Z_{> 0}$ be a (strictly) positive integer.
Then the only divisors of $p^n$ are $1, p, p^2, \ldots, p^{n - 1}, p^n$.

Proof:
First it is necessary to establish that every element of the set $\set {1, p, p^2, \ldots, p^{n - 1}, p^n}$ is in fact a divisor of $p^n$.
For any $j \in \set {1, 2, \ldots, n}$:
:$p^n = p^j p^{n - j}$
and so each of $1, p, p^2, \ldots, p^{n - 1}, p^n$ is a divisor of $p^n$.
{{qed|lemma}}
Let:
:$a \in \Z_{>0}: a \notin \set {1, p, p^2, \ldots, p^{n - 1}, p^n}$
Let $a = p^j$ where $j \in \Z: j > n$.
Then:
:$p^j = p^n p^{j - n}$
and so $p^n$ is a divisor of $p^j$.
Hence $p_j \nmid p^n$.
Now let:
:$a \notin \set {p^k: k \in \Z_{>0} }$
Then:
:$\exists q \in \Bbb P: q \divides a$
where:
:$\Bbb P$ is the set of all prime numbers
:$\divides$ denotes divisibility.
{{AimForCont}} $a \divides p^n$.
From Divisor Relation is Transitive it follows that $q \divides p^n$.
From Euclid's Lemma for Prime Divisors: General Result it follows that:
:$q \divides p$
As $p$ is a prime, by definition its only divisors are $1$ and $p$.
This contradicts the supposition that $q$ is a divisor of $p^n$.
Hence $a \nmid p^n$.
{{qed}}
Category:Prime Numbers
7rk579ji8oqt9bogdoui6eysst01x2q
Theorem: Chebyshev Distance is Limit of P-Product Metric

Let $M_{1'} = \struct {A_{1'}, d_{1'} }$ and $M_{2'} = \struct {A_{2'}, d_{2'} }$ be metric spaces.
Let $\AA = A_{1'} \times A_{2'}$ be the cartesian product of $A_{1'}$ and $A_{2'}$.
Let $p \in \R_{\ge 1}$.
Let $d_p: \AA \times \AA \to \R$ be the $p$-product metric on $\AA$:
:$\map {d_p} {x, y} := \paren {\paren {\map {d_{1'} } {x_1, y_1} }^p + \paren {\map {d_{2'} } {x_2, y_2} }^p}^{1/p}$
and let $d_\infty: \AA \times \AA \to \R$ be the Chebyshev distance on $\AA$:
:$\ds \map {d_\infty} {x, y} := \max \set {\map {d_{1'} } {x_1, y_1}, \map {d_{2'} } {x_2, y_2} }$
where $x = \tuple {x_1, x_2}, y = \tuple {y_1, y_2} \in \AA$.
Then:
:$\ds d_\infty = \lim_{p \mathop \to \infty} d_p$
in the sense that:
:$\ds \max \set {\map {d_{1'} } {x_1, y_1}, \map {d_{2'} } {x_2, y_2} } = \lim_{p \mathop \to \infty} \paren {\paren {\map {d_{1'} } {x_1, y_1} }^p + \paren {\map {d_{2'} } {x_2, y_2} }^p}^{1/p}$

Proof:
Let $x$ and $y$ be arbitrary.
Let $a = \map {d_{1'} } {x_1, y_1}, b = \map {d_{2'} } {x_2, y_2}$.
{{WLOG}}, suppose that $\max \set {a, b} = a$.
Then:
{{begin-eqn}}
{{eqn | l = \lim_{p \mathop \to \infty} \paren {a^p + b^p}^{1/p}
      | o = \ge
      | r = \lim_{p \mathop \to \infty} \paren {a^p}^{1/p}
      | c = 
}}
{{eqn | r = \lim_{p \mathop \to \infty} a
      | c = 
}}
{{eqn | r = a
      | c = 
}}
{{eqn | r = \max \set {a, b}
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \lim_{p \mathop \to \infty} \paren {a^p + b^p}^{1/p}
      | o = \le
      | r = \lim_{p \mathop \to \infty} \paren {a^p + a^p}^{1/p}
      | c = 
}}
{{eqn | r = \lim_{p \mathop \to \infty} \paren {2 a^p}^{1/p}
      | c = 
}}
{{eqn | r = \lim_{p \mathop \to \infty} a \cdot 2^{1/p}
      | c = 
}}
{{eqn | r = a \lim_{p \mathop \to \infty} 2^{1/p}
      | c = 
}}
{{eqn | r = a
      | c = 
}}
{{eqn | r = \max \set {a, b}
      | c = 
}}
{{end-eqn}}
The result follows by the Squeeze Theorem for Functions.
{{qed}}
Category:Chebyshev Distance
Category:P-Product Metrics
9d3391e8lu7ws0dji7h9py3wk48g6j8
Theorem: Bertrand's Theorem

Let $U: \R_{>0} \to \R$ be analytic for $r > 0$.
Let $M > 0$ be a nonvanishing angular momentum such that a stable circular orbit exists.
Suppose that every orbit sufficiently close to the circular orbit is closed.
Then $U$ is either $k r^2$ or $-\dfrac k r$ (for $k > 0$) up to an additive constant.

Proof:
The substitution $x = M / r$ gives:
:$\ds \Phi = \sqrt 2 \int_{x_\min}^{x_\max} \frac {\d x} {\sqrt {E - \map W x}}$
where $\map W x \equiv \map U {\dfrac M x} + \dfrac 1 2 x^2$.
In general, the frequency of oscillations around a stable equilibrium at $x = x_0$ for a particle of mass $m$ in a potential $V$ is given by:
:$\omega = \sqrt {\dfrac {\map {V' '} {x_0} } m}$
{{explain|Provide a link to a proof of the above, and explain what $m$ is.}}
which means that:
:$\Phi \approx 2 \pi \dfrac M {x_0^2} \sqrt {\map {W' '} {x_0} } = 2 \pi \sqrt {\dfrac {U'} {3 U' + x_0 U' '} }$
Suppose $\Phi$ were constant.
Then the solutions are:
:$\map U r = k r^\alpha, \alpha \ge - 2, \alpha \ne 0$
and:
:$\map U r = b \log r$
Therefore:
: $\Phi = \dfrac {2 \pi} {\sqrt{\alpha + 2}}$
with $\alpha = 0$ corresponding to the logarithmic solution.
This is discarded, since in that case $\Phi$ is not commensurable with $\pi$.
Now consider $\alpha > 0$, so that $\map U r \to \infty$ as $r \to \infty$.
The substitution $x = y x_\max$ reduces $\Phi$ to:
:$\ds \Phi = \sqrt 2 \int_{y_\min}^1 \frac {\d y} {\sqrt {\map W 1 - \map W y} }$
where:
:$\map W y \equiv \dfrac {y^2} 2 + \dfrac 1 { {x_\max}^2} \map U {\dfrac M {y x_\max} }$
Therefore, when $E \to \infty$:
:$x_\max \to \infty$ and $y_\min \to 0$
This means that:
:$\ds \lim_{E \mathop \to \infty} \Phi = \pi$
Equating this with the previous result gives:
:$\dfrac {2 \pi} {\sqrt {\alpha + 2}} = \pi$
Therefore:
:$\alpha=2$
Now let $\map U r = -k r^{-\beta}, 0 < \beta < 2$.
A similar approach gives:
:$\ds \lim_{E \mathop \to -0} \Phi = \frac {2 \pi} {2 - \beta}$
so that:
:$\dfrac {2 \pi} {2 + \alpha} = \dfrac {2 \pi} {\sqrt {2 + \alpha} }$
It follows that:
:$\alpha = -1$
and the result follows.
{{qed}}
Theorem: Bertrand's Theorem

Let $U: \R_{>0} \to \R$ be analytic for $r > 0$.
Let $M > 0$ be a nonvanishing angular momentum such that a stable circular orbit exists.
Suppose that every orbit sufficiently close to the circular orbit is closed.
Then $U$ is either $k r^2$ or $-\dfrac k r$ (for $k > 0$) up to an additive constant.

Proof:
In general $U_M$ is not monotonic on $\openint {r_\min} {r_\max}$.
{{explain|Link to a proof of that statement.}}
Therefore a unique inverse $\map r {U_M}$ does not exist.
However, suppose it is possible to construct separate inverse functions $r_{1, 2}$ for the intervals $\openint {r_0} {r_\min}$ and $\openint {r_0} {r_\max}$, where $r_0$ is the minimum of $U_M$ on $\openint {r_\min} {r_\max}$.
{{explain|What does $r_{1, 2}$ mean in this context?}}
Note that the orbit corresponding to $r_0$ is the stable circular orbit.
{{explain|Link to a proof of the above.}}
Therefore this will be possible for orbits sufficiently close to it. 
Now write:
:$\ds \Phi = \int_{U_0}^E \map F {U_M} \frac {\d U_{eff} } {\sqrt {E - U_M} }$
where:
:$F = \sqrt 2 M \, \map {\dfrac {\d} {\d U_M} } {\dfrac 1 {r_1} - \dfrac 1 {r_2} }$
:$U_0 \equiv \map {U_M} {r_0}$
{{explain|What does $U_{eff}$ mean?}}
This is Abel's Integral Equation which can be solved for $\map F {U_M}$, giving:
:$\ds \map F U = \dfrac 1 \pi \int_{U_0}^{U_M} \frac {\Phi \rd E} {\sqrt {U_M - E} }$
$\Phi$ may have energy dependence.
However, we require:
:$\map \Phi E = 2 \pi \map q E$
such that $q: \R \to \Q$ is continuous, and a rational continuous function must be constant.
{{Explain|Link to a result explaining why a rational continuous function must be constant.}}
Finally, integrating gives:
:$\dfrac 1 {r_1} - \dfrac 1 {r_2} = \gamma \sqrt{U_M - U_0}, \gamma = \dfrac {\sqrt 2 \Phi} {\pi M}$
{{explain|Provide a link demonstrating the solution of that integral.}}
Now consider defining the {{LHS}} to be a single function $\dfrac 1 {\map r U}$, meromorphic with a simple pole at $r = 0$.
{{explain|The definitions for meromorphic and simple pole as given on {{ProofWiki}} are specifically for complex functions. Either these need to be expanded to define them in the specific context of real functions, or the above definition is actually for a complex function. In any case, the domain of all the functions defined in this proof need to be clarified.}}
Write:
:$\dfrac 1 r = \gamma \sqrt {U_M - U_0} + \map \Omega {U_0, U}$
where $\Omega$ is an analytic function in $U$ in an open neighborhood of $U_0$ such that:
:$\map \Omega {U_0, U_0} = \dfrac 1 {r_0}$
{{explain|What are $\tuple {U_0, U}$ and $\tuple {U_0, U_0}$ in this context?}}
Explicitly:
:$\sqrt {U_M - U_0} = \sqrt {U + \dfrac {M^2} {2 r^2} - U_0} = \dfrac 1 r \sqrt {\dfrac {M^2} 2 + \paren {U - U_0} r^2}$
It can be seen that the {{RHS}} also has a simple pole at $r=0$.
However, it also has a branch point at $r = r_0$.
To avoid this, the radicand must be the square of an analytic function with a zero at $r_0$.
The only possibilities are:
:$U \propto r^2, -\dfrac 1 {r^2}$
{{qed}}
Theorem: Cube Root of 2 is Irrational

:$\sqrt [3] 2$ is irrational.

Proof:
{{AimForCont}} that $\sqrt [3] 2$ is rational.
Then:
{{begin-eqn}}
{{eqn | l = \sqrt [3] 2
      | r = \frac p q
      | c = for some integer $p$ and $q$
}}
{{eqn | ll= \leadsto
      | l = p^3
      | r = q^3 + q^3
      | c = 
}}
{{end-eqn}}
which contradicts Fermat's Last Theorem.
{{qed}}
Category:Number Theory
nr8x21nbup2ti86dxhgykhenszrsgs1
Theorem: Piecewise Continuously Differentiable Function/Definition 2 is Continuous

Let $f$ be a real function defined on a closed interval $\closedint a b$.
Let $f$ satisfy the definition Piecewise Continuously Differentiable Function/Closed Intervals.
Then $f$ is continuous.

Proof:
$f$ satisfies the conditions of Piecewise Continuously Differentiable Function/Closed Intervals.
Therefore, there exists a finite subdivision $\set {x_0, \ldots, x_n}$ of $\closedint a b$, $x_0 = a$ and $x_n = b$, such that $f$ is continuously differentiable on $\closedint {x_{i - 1} } {x_i}$ for every $i \in \set {1, \ldots, n}$.
Here, the derivatives at $x_{i - 1}$ and $x_i$ are understood as one-sided derivatives.
$f$ is differentiable on $\closedint {x_{i - 1} } {x_i}$ for every $i \in \set {1, \ldots, n}$.
Therefore, by Differentiable Function is Continuous, $f$ is continuous at every point of $\closedint {x_{i - 1} } {x_i}$ for every $i \in \set {1, \ldots, n}$.
Here, the continuities at $x_{i - 1}$ and $x_i$ are one-sided.
We use this result to go through every point of every $\closedint {x_{i - 1} } {x_i}$ in order to establish the continuity of $f$ there:
$f$ is continuous on $\closedint {x_{i - 1} } {x_i}$ for every $i \in \set {1, \ldots, n}$.
$\openint {x_{i - 1} } {x_i}$ is a subset of $\closedint {x_{i - 1} } {x_i}$ for every $i \in \set {1, \ldots, n}$.
Therefore, $f$ is continuous at every point of $\openint {x_{i - 1} } {x_i}$ for every $i \in \set {1, \ldots, n}$.
$x_0$ ($= a$) is the leftmost point in the domain of $f$.
$f$ is right-continuous at $x_0$.
Therefore, $f$ is continuous at $x_0$.
$x_n$ ($= b$) is the rightmost point in the domain of $f$.
$f$ is left-continuous at $x_n$.
Therefore, $f$ is continuous at $x_n$.
$f$ is continuous at every point $x_i$, $i \in \set {1, \ldots, n - 1}$, because $f$ is both left- and right-continuous at these points.
All in all, we have found that $f$ is continuous at every point of $\closedint {x_{i - 1} } {x_i}$ for every $i \in \set {1, \ldots, n}$.
$f$ is therefore continuous at every point of the union of those intervals: $\ds \bigcup_{i \mathop = 1}^n \closedint {x_{i - 1}} {x_i}$.
$\ds \bigcup_{i \mathop = 1}^n \closedint {x_{i - 1}} {x_i}$ equals $\closedint a b$, the domain of $f$.
Therefore, $f$ is continuous as $f$ is continuous at every point of its domain.
{{qed}}
Category:Real Analysis
cfh80ujkchf35ete10j67x44lk20h8k
Theorem: Homomorphism of Chain Complexes induces Homomorphism of Homology

Let $A_\bullet$ and $B_\bullet$ be chain complexes of abelian groups.
Let $f: A_\bullet \to B_\bullet$ be a homomorphism.
Then for every $n$, $f$ induces a morphism $\map {H_n} {A_\bullet} \to \map {H_n} {B_\bullet}$ of homology groups.
{{explain|Domain of $n$}}

Proof:
Let $\partial^A_\bullet$, $\partial^B_\bullet$ denote the differential on $A_\bullet$, respectively $B_\bullet$. 
First it will be demonstrated that:
:$\forall a \in \map \ker {\partial^A_n} \subseteq A_n: \map {f_n} a \in \map \ker {\partial^B_n}$
Thus:
:$\partial^B_n \map {f_n} a = \map {f_{n - 1} } {\partial^A_n a} = \map {f_{n - 1} } 0 = 0$
Thus there exists a map:
:$\bar f_n: \map \ker {\partial^A_n} \to \map \ker {\partial^B_n}$
via the restriction of $f$.
{{explain|Restriction of $f$ to what?}}
Next will be shown that:
:$\forall a \in \Img {\partial^A_{n + 1} }: \map {f_n} a \in \Img {\partial^B_{n + 1} }$
Let $a = \partial^A_{n + 1}a'$
Then:
:$\partial^B_{n + 1} \map {f_{n + 1} } {a'} = \map {f_n} {\partial^A_n a'} = \map {f_n} a$.
Let $\pi: \map \ker {\partial^B_n} \to \map {H_n} {B_\bullet}$ be the quotient mapping.
Let $\rho = \pi \circ \bar f_n$.
From above:
:$\Img {\partial^A_{n + 1} } \subseteq \map \ker \rho$
Thus $\rho$ factors through a map:
:$\tilde f_n: \map {H_n} {A_\bullet} \to \map {H_n} {B_\bullet}$
completing the proof.
{{qed}}
Category:Homological Algebra
k9spnqpurlrdx3tfz5nzfcwuj12q65h
Theorem: Homotopic Chain Maps Induce Equal Maps on Homology

Let $A_\bullet$, $B_\bullet$ be chain complexes of abelian groups.
Let $f, g: A_\bullet \to B_\bullet$ be chain maps which are homotopic.
Then $f$ and $g$ induce equal maps on homology.

Proof:
Let $\partial^A_\bullet, \partial^B_\bullet$ be the differentials on $A_\bullet$ and $B_{\bullet}$ respectively.
Let $h$ be a homotopy between $f$ and $g$. 
Let:
:$a \in \map {H_n} A \cong \map \ker {\partial^A_n} / \Img {\partial^A_{n + 1} }$
There exists $\tilde a \in \map \ker {\partial^A_n}$ representing $a$.
It is enough to show that:
:$\map {f_n} {\tilde a} \sim \map {g_n} {\tilde a}$
Equivalently:
:$\map {f_n} {\tilde a} - \map {g_n} {\tilde a} \in \Img {\partial^B_{n + 1} }$
We know that:
:$\partial h - h \partial = f - g$
This means:
:$\partial^B_{n + 1} h_n - h_{n - 1} \partial^A_n = f_n - g_n$
Plugging in $\tilde a$: 
:$\map {\partial^B_{n + 1} } {\map {h_n} {\tilde a} } - \map {h_{n - 1}} {\map {\partial^A_n} {\tilde a} } = \map {f_n} {\tilde a} - \map {g_n} {\tilde a}$
Since $\tilde a \in \map \ker {\partial^A_n}$:
:$\map {\partial^B_{n + 1} } {\map {h_n} {\tilde a} } = \map {f_n} {\tilde a} - \map {g_n} {\tilde a}$
Therefore:
:$\map {f_n} {\tilde a} - \map {g_n} {\tilde a} \in \Img {\partial^B_{n + 1} }$
{{qed}}
Category:Homological Algebra
8aknbguht3kg3f8f8nh9alozjpic0ga
Theorem: Equivalence of Definitions of Piecewise Continuously Differentiable Function

A function satisfying Piecewise Continuously Differentiable Function With Closed Intervals is equivalent to being continuous and satisfying Piecewise Continuously Differentiable Function With One-Sided Limits.
Let $f$ be a real function defined on a closed interval $\closedint a b$.

Proof:
=== Piecewise Continuously Differentiable Function With Closed Intervals implies continuity and Piecewise Continuously Differentiable Function With One-Sided Limits ===
Assume that $f$ satisfies the requirement of Piecewise Continuously Differentiable Function With Closed Intervals.
We need to prove that $f$ satisfies the requirements of Piecewise Continuously Differentiable Function With One-Sided Limits and that $f$ is continuous.
$f$ is continuous by Piecewise Continuously Differentiable Function/Definition 2 is Continuous.
This proves the continuity requirement.
$f$ is continuously differentiable on $\closedint {x_{i - 1} } {x_i}$, the derivatives at $x_{i - 1}$ and $x_i$ understood as one-sided derivatives, for every $i \in \set {1, \ldots, n}$, by definition.
Therefore, $f$ is continuously differentiable at every point of every $\openint {x_{i - 1} } {x_i}$ since $\openint {x_{i - 1} } {x_i}$ is a subset of $\closedint {x_{i - 1} } {x_i}$.
This proves $(1)$ in Piecewise Continuously Differentiable Function With One-Sided Limits.
$f$ has a continuous right-hand derivative at $x_{i - 1}$ for every $i \in \set {1, \ldots, n}$.
This means that:
:$\map {f'_+} {x_{i - 1} } = \ds \lim_{x \mathop \to {x_{i - 1} }^+} \map {f'} x$
This implies that $\ds \lim_{x \mathop \to {x_{i - 1} }^+} \map {f'} x$ exists for every $i \in \set {1, \ldots, n}$.
Also, $f$ has a continuous left-hand derivative at $x_i$ for every $i \in \set {1, \ldots, n}$.
This means that
:$\map {f'_-} {x_i} = \ds \lim_{x \mathop \to {x_i}^-} \map {f'} x$
This implies that $\ds \lim_{x \mathop \to {x_i}^-} \map {f'} x$ exists for every $i \in \set {1, \ldots, n}$.
These two conclusions prove that requirement $(2)$ in Piecewise Continuously Differentiable Function With One-Sided Limits is satisfied.
This finishes the proof that $f$ satisfies the requirements of Piecewise Continuously Differentiable Function With One-Sided Limits and that $f$ is continuous.
{{qed|lemma}}
Theorem: Square Inscribed in Circle is greater than Half Area of Circle

A square inscribed in a circle has an area greater than half that of the circle.

Proof:
:300px
Let $ABCD$ be a square inscribed in a circle.
Let $EFGH$ be a square circumscribed around the same circle.
We have that:
:$ABCD$ is twice the area of the triangle $ADB$.
:$EFGH$ is twice the area of the rectangle $EFBD$.
From Area of Rectangle, the area of $EFBD$ is $ED \cdot DB$.
From Area of Triangle in Terms of Side and Altitude, the area of $ADB$ is $\dfrac 1 2 \cdot ED \cdot DB$.
Thus:
:$EFGH = 2 \cdot ABCD$
But the area of $EFGH$ is greater than the area of the circle around which it is circumscribed.
Therefore half of the area of $EFGH$ is greater than half of the area of the circle around which it is circumscribed.
Therefore the area of $ABCD$ is greater than half of the area of the circle within which it is inscribed.
{{qed}}
Theorem: Bounded Piecewise Continuous Function is Darboux Integrable

Let $f$ be a real function defined on the closed interval $\closedint a b$.
Let $f$ be piecewise continuous and bounded on $\closedint a b$.
Then $f$ is Darboux integrable on $\closedint a b$.

Proof:
We are given that $f$ is piecewise continuous and bounded on $\closedint a b$.
Therefore, there exists a finite subdivision $\set {x_0, x_1, \ldots, x_n}$ of $\closedint a b$, where $x_0 = a$ and $x_n = b$, such that for all $i \in \set {1, 2, \ldots, n}$:
:$f$ is continuous on $\openint {x_{i - 1} } {x_i}$
:$f$ is bounded on $\closedint {x_{i - 1} } {x_i}$.
Note that $n$ is the number of intervals $\openint {x_{i - 1} } {x_i}$ defined from the (finite) subdivision $\set {x_0, x_1, \ldots, x_n}$.
We shall use proof by induction on these $n$ intervals.
For all $k \in \set {1, 2, \ldots, n}$, let $\map P k$ be the proposition:
:$f$ is Darboux integrable on $\closedint {x_0} {x_k}$.
Theorem: Bounded Piecewise Continuous Function may not have One-Sided Limits

Let $f$ be a real function defined on a closed interval $\closedint a b$, $a < b$. 
Let $f$ be a bounded piecewise continuous function.
{{:Definition:Bounded Piecewise Continuous Function}}
Then it is not necessarily the case that $f$ is a piecewise continuous function with one-sided limits:
{{:Definition:Piecewise Continuous Function with One-Sided Limits}}

Proof:
Consider the function:
:$\map f x = \begin{cases}
0 & : x = a \\
\map \sin {\dfrac 1 {x - a} } & : x \in \hointr a b
\end{cases}$
Consider the (finite) subdivision $\set {a, b}$ of $\closedint a b$.
We observe that $\map \sin {\dfrac 1 {x - a} }$ is continuous on $\openint a b$.
Since $\map f x = \map \sin {\dfrac 1 {x - a} }$ on $\openint a b$, it follows that $f$ is continuous on $\openint a b$.
Also, $f$ is bounded by the bound $1$ on $\closedint a b$.
Therefore $f$ is a bounded piecewise continuous function on the closed interval $\closedint a b$.
We now investigate whether $f$ has one-sided limits at the endpoints of $\closedint a b$.
The function $\map \sin {\dfrac 1 {x - a} }$ varies between $-1$ and $+1$ as $x$ approaches $a$ from above.
Thus it does not converge. 
Since $\map f x = \map \sin {\dfrac 1 {x - a} }$ when $x > a$ we conclude that $\ds \lim_{x \mathop \to a^+} \map f x$ does not exist either.
$f$ has no one-sided limit at $a$.
Hence $f$ is not a piecewise continuous function with one-sided limits.
{{qed}}
Category:Piecewise Continuous Functions
2nesxucxjf34l2eb2ki8rla54aod69f
Theorem: Rational Numbers form Subset of Real Numbers

The set $\Q$ of rational numbers forms a subset of the real numbers $\R$.

Proof:
Let $x \in \Q$, where $\Q$ denotes the set of rational numbers.
Consider the rational sequence:
:$x, x, x, \ldots$
This sequence is trivially Cauchy.
Thus there exists a Cauchy sequence $\eqclass {\sequence {x_n} } {}$ which is identified with a rational number $x \in \Q$ such that:
So by the definition of a real number:
:$x \in \R$
where $\R$ denotes the set of real numbers.
Thus, by definition of subset:
:$\Q \subseteq \R$
{{qed}}