avewright/proofwiki-math huggingface dataset:
Theorem: Euler's Sine Identity

:$\sin z = \dfrac {e^{i z} - e^{-i z} } {2 i}$

Proof:
Recall the definition of the sine function:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = x - \frac {x^3} {3!} + \frac {x^5} {5!} - \frac {x^7} {7!} + \cdots + \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!} + \cdots
      | c = 
}}
{{end-eqn}}
Recall the definition of the exponential as a power series:
{{begin-eqn}}
{{eqn | l = e^x
      | r = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}
      | c = 
}}
{{eqn | r = 1 + \frac x {1!} + \frac {x^2} {2!} + \frac {x^3} {3!} + \cdots + \frac {x^n} {n!} + \cdots
      | c = 
}}
{{end-eqn}}
Then, starting from the {{RHS}}:
{{begin-eqn}}
{{eqn | l = \frac {e^{i x} - e^{-i x} } {2 i}
      | r = \frac 1 {2 i} \paren {\sum_{n \mathop = 0}^\infty \frac {\paren {i x}^n} {n!} - \sum_{n \mathop = 0}^\infty \frac {\paren {-i x}^n} {n!} }
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \sum_{n \mathop = 0}^\infty \paren {\frac {\paren {i x}^n - \paren {-i x}^n} {n!} }
      | c = 
}}
{{eqn | r = \frac 1 {2 i} \sum_{n \mathop = 0}^\infty \paren {\frac {\paren {i x}^{2 n} - \paren {-i x}^{2 n} } {\paren {2 n}!} + \frac {\paren {i x}^{2 n + 1} - \paren {-i x}^{2 n + 1} } {\paren {2 n + 1}!} }
      | c = split into even and odd $n$
}}
{{eqn | r = \frac 1 {2 i} \sum_{n \mathop = 0}^\infty \frac {\paren {i x}^{2 n + 1} - \paren {-i x}^{2 n + 1} } {\paren {2 n + 1}!}
      | c = as $\paren {-i x}^{2 n} = \paren {i x}^{2 n}$
}}
{{eqn | r = \frac 1 {2 i} \sum_{n \mathop = 0}^\infty \frac {2 \paren {i x}^{2 n + 1} } {\paren {2 n + 1}!}
      | c = as $\paren {-1}^{2 n + 1} = -1$
}}
{{eqn | r = \frac 1 i \sum_{n \mathop = 0}^\infty \frac {\paren {i x}^{2 n + 1} } {\paren {2 n + 1}!}
      | c = cancel $2$
}}
{{eqn | r = \frac 1 i \sum_{n \mathop = 0}^\infty \frac {i \paren {-1}^n x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = as $i^{2 n + 1} = i \paren {-1})^n $
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1!} }
      | c = cancel $i$
}}
{{eqn | r = \sin x
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Sine Identity

:$\sin z = \dfrac {e^{i z} - e^{-i z} } {2 i}$

Proof:
Recall Euler's Formula:
:$e^{i x} = \cos x + i \sin x$
Then, starting from the {{RHS}}:
{{begin-eqn}}
{{eqn | l = \frac {e^{i x} - e^{-i x} }{2 i}
      | r = \frac {\paren {\cos x + i \sin x} - \paren {\map \cos {-x} + i \map \sin {-x} } } {2 i}
}}
{{eqn | r = \frac {\paren {\cos x + i \sin x - \cos x - i \map \sin {-x} } } {2 i}
      | c = Cosine Function is Even
}}
{{eqn | r = \frac {i \sin x - i \map \sin {-x} } {2 i}
      | c = 
}}
{{eqn | r = \frac {i \sin x - i \paren {-\map \sin {-x} } } {2 i}
      | c = Sine Function is Odd
}}
{{eqn | r = \frac {2 i \sin x} {2 i}
      | c = 
}}
{{eqn | r = \sin x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Euler's Sine Identity

:$\sin z = \dfrac {e^{i z} - e^{-i z} } {2 i}$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | l = e^{i x}
      | r = \cos x + i \sin x
      | c = Euler's Formula
}}
{{eqn | n = 2
      | l = e^{-i x}
      | r = \cos x - i \sin x
      | c = Euler's Formula: Corollary
}}
{{eqn | ll= \leadsto
      | l = e^{i x} - e^{-i x}
      | r = \paren {\cos x + i \sin x} - \paren {\cos x - i \sin x}
      | c = $(1) - (2)$
}}
{{eqn | r = 2 i \sin x
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac {e^{i x} - e^{-i x} } {2 i}
      | r = \sin x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Sum

:$\map \sin {a + b} = \sin a \cos b + \cos a \sin b$

Proof:
{{begin-eqn}}
{{eqn | l = \map \cos {a + b} + i \, \map \sin {a + b}
      | r = e^{i \paren {a + b} }
      | c = Euler's Formula
}}
{{eqn | r = e^{i a} e^{i b}
      | c = Exponential of Sum
}}
{{eqn | r = \paren {\cos a + i \sin a} \paren {\cos b + i \sin b}
      | c = Euler's Formula
}}
{{eqn | r = \paren {\cos a \cos b - \sin a \sin b} + i \paren {\sin a \cos b + \cos a \sin b}
      | c = Complex Numbers form Field
}}
{{end-eqn}}
By equating the imaginary parts, the result follows.
{{qed}}
Theorem: Sine of Sum

:$\map \sin {a + b} = \sin a \cos b + \cos a \sin b$

Proof:
Recall the analytic definitions of sine and cosine:
:$\ds \sin x = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}$
:$\ds \cos x = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}$
Let:
{{begin-eqn}}
{{eqn | l = \map g a
      | r = \map \sin {a + b} - \sin a \cos b - \cos a \sin b
}}
{{eqn | l = \map h a
      | r = \map \cos {a + b} - \cos a \cos b + \sin a \sin b
}}
{{end-eqn}}
Let us differentiate these with respect to $a$, keeping $b$ constant.
Then from Derivative of Sine Function and Derivative of Cosine Function, we have:
{{begin-eqn}}
{{eqn | l = \map {g'} a
      | r = \map \cos {a + b} - \cos a \cos b + \sin a \sin b = \map h a
}}
{{eqn | l = \map {h'} a
      | r = -\map \sin {a + b} + \sin a \cos b + \cos a \sin b = -\map g a
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \map {D_a} {\paren {\map g a}^2 + \paren {\map h a}^2}
      | r = 2 \map g a \map {g'} a + 2 \map h a \map {h'} a
}}
{{eqn | r = 0
}}
{{end-eqn}}
Thus from Derivative of Constant:
:$\forall a \in \R: \map g a^2 + \map h a^2 = c$
In particular, it is true for $a = 0$, and so:
:$\map g 0^2 + \map h 0^2 = 0$
So:
:$\map g a^2 + \map h a^2 = 0$
But from Square of Real Number is Non-Negative:
:$\map g a^2 \ge 0$ and $\map h a^2 \ge 0$
So it follows that:
:$\map g a = 0$
and:
:$\map h a = 0$
Hence the result.
{{qed}}
Theorem: Sine of Sum

:$\map \sin {a + b} = \sin a \cos b + \cos a \sin b$

Proof:
{{begin-eqn}} 
{{eqn | l = \sin a \cos b + \cos a \sin b
      | r = \paren {\frac {e^{i a} - e^{-i a} }{2 i} } \cos b + \cos a \paren {\frac {e^{i b} - e^{-i b} }{2 i} }
      | c = Euler's Sine Identity
}}
{{eqn | r = \paren {\frac {e^{i a} - e^{-i a} } {2 i} } \paren {\frac {e^{i b} + e^{-i b} } 2} + \paren {\frac {e^{i a} + e^{-i a} } 2} \paren {\frac {e^{i b} - e^{-i b} } {2 i} }
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac {e^{i a} e^{i b} + e^{i a} e^{-i b} - e^{-i a} e^{i b} - e^{-i a} e^{-i b} } {4 i}
      | c = expanding
}}
{{eqn | o = 
      | ro= +
      | r = \frac {e^{i a} e^{i b} - e^{i a} e^{-i b} + e^{-i a} e^{i b} - e^{-i a} e^{-i b} } {4 i}
}}
{{eqn | r = \frac {e^{i a} e^{i b} - e^{-i a} e^{-i b} } {2 i}
      | c = simplifying
}}
{{eqn | r = \frac {e^{i \paren {a + b} } - e^{-i \paren {a + b} } } {2 i}
      | c = Exponential of Sum
}}
{{eqn | r = \map \sin {a + b}
      | c = Euler's Sine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Sum

:$\map \sin {a + b} = \sin a \cos b + \cos a \sin b$

Proof:
{{begin-eqn}}
{{eqn | l = \sin \left({a + b}\right)
      | r = \cos \left({\frac \pi 2 - \left({a + b}\right)}\right)
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = \cos \left({\left({\frac \pi 2 - a}\right) - b}\right)
}}
{{eqn | r = \cos \left({\frac \pi 2 - a}\right) \cos b + \sin \left({\frac \pi 2 - a}\right) \sin b
      | c = Cosine of Difference
}}
{{eqn | r = \sin a \cos b + \sin \left({\frac \pi 2 - a}\right) \sin b
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = \sin a \cos b + \cos a \sin b
      | c = Sine of Complement equals Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Sum

:$\map \sin {a + b} = \sin a \cos b + \cos a \sin b$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | l = 2 \sin a \cos b
      | r = \sin \paren {a + b} + \sin \paren {a - b}
      | c = Werner Formula for Sine by Cosine: Proof 2
}}
{{eqn | n = 2
      | l = 2 \cos a \sin b
      | r = \sin \paren {a + b} - \sin \paren {a - b}
      | c = Werner Formula for Cosine by Sine: Proof 2
}}
{{eqn | ll= \leadsto
      | l = 2 \sin \paren {a + b}
      | r = 2 \sin a \cos b + 2 \cos a \sin b
      | c = $(1) + (2)$
}}
{{eqn | ll= \leadsto
      | l = \sin \paren {a + b}
      | r = \sin a \cos b + \cos a \sin b
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Sum

:$\map \sin {a + b} = \sin a \cos b + \cos a \sin b$

Proof:
:900px
We begin by enclosing a right-angled triangle $BEF$ with hypotenuse $BF$ of length $1$, inside rectangle $ABCD$.
Let $\angle EBF = a$ and $\angle ABE = b$.
Therefore:
{{begin-eqn}}
{{eqn | l = BF
      | r = 1
      | c = Given
}}
{{eqn | l = BE
      | r = \cos a
      | c = {{Defof|Cosine of Angle}}
}}
{{eqn | l = EF
      | r = \sin a
      | c = {{Defof|Sine of Angle}}
}}
{{eqn | l = AB
      | r = \cos a \cos b
      | c =
}}
{{eqn | l = AE
      | r = \cos a \sin b
      | c =
}}
{{eqn | l = ED
      | r = \sin a \cos b
      | c = 
}}
{{eqn | l = DF
      | r = \sin a \sin b
      | c = 
}}
{{eqn | l = \map \sin {a + b }
      | r = BC
      | c = 
}}
{{eqn | r = AE + ED
      | c = 
}}
{{eqn | r = \cos a \sin b + \sin a \cos b
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sine of Sum

:$\map \sin {a + b} = \sin a \cos b + \cos a \sin b$

Proof:
350px
Let two triangles $\triangle ABC$ and $\triangle ADC$ be inscribed in a circle on opposite
sides of diameter $AC$.
By Thales' Theorem, they are both right triangles and $\angle ADC$ and $\angle ABC$ are right angles.
Let the diameter $AC = 1$.
Let $\angle DAC = \alpha$ and $\angle CAB = \beta$.
From the construction above, we have the following:
:$\cos \alpha = AD$
:$\cos \beta = AB$
:$\sin \alpha = DC$
:$\sin \beta = BC$
By Length of Chord of Circle:
:$DB \mathop = 2 r \map \sin {\alpha + \beta}$
Since $2r \mathop = 1$:
:$DB \mathop = \map \sin {\alpha + \beta}$
By Quadrilateral is Cyclic iff Opposite Angles sum to Two Right Angles:
:$\Box ABCD$ is a cyclic quadrilateral.
By Ptolemy's Theorem:
:$DB \times AC = AB \times CD + BC \times AD$
Substituting:
:$\map \sin {\alpha + \beta} \times 1 = \cos \beta \sin \alpha + \sin \beta \cos \alpha$
:$\map \sin {\alpha + \beta} = \sin \alpha \cos \beta + \sin \beta \cos \alpha$
By Equivalence of Definitions of Sine of Angle, the definition of sine from the circle, from the triangle and as a real function are equivalent.
It follows that all real numbers $x$ and $y$ correspond to values of $\alpha$ and $\beta$ for which the proof above applies, with one exception.
The exception occurs when both $\alpha$ and $\beta$ are equal to $\dfrac {\pi} 2$.
But then the result is simply:
:$ \sin {\pi} = \sin \dfrac {\pi} 2 \cos \dfrac {\pi} 2 + \sin \dfrac {\pi} 2 \cos \dfrac {\pi} 2$
:$ 0 = 0 \cdot 1 + 1 \cdot 0$
The result follows.
{{qed}}
Theorem: Hyperbolic Sine Function is Odd

:$\map \sinh {-x} = -\sinh x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \sinh {-x}
      | r = \frac {e^{-x} - e^{-\paren {-x} } } 2
      | c = {{Defof|Hyperbolic Sine}}
}}
{{eqn | r = \frac {e^{-x} - e^x} 2
}}
{{eqn | r = -\frac {e^x - e^{-x} } 2
}}
{{eqn | r = -\sinh x
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Sine Function is Odd

:$\map \sinh {-x} = -\sinh x$

Proof:
{{begin-eqn}}
{{eqn	| l = \map \sinh {-x}
	| r = -i \, \map \sin {-i x}
	| c = Hyperbolic Sine in terms of Sine
}}
{{eqn	| r = i \, \map \sin {i x}
	| c = Sine Function is Odd
}}
{{eqn	| r = -\sinh x
	| c = Hyperbolic Sine in terms of Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of Sum/Complex Numbers

Let $z_1, z_2 \in \C$ be complex numbers.
Let $\exp z$ be the exponential of $z$.
Then:
:$\map \exp {z_1 + z_2} = \paren {\exp z_1} \paren {\exp z_2}$

Proof:
This proof is based on the definition of the complex exponential as the unique solution of the differential equation:
:$\dfrac \d {\d z} \exp = \exp$
which satisfies the initial condition $\map \exp 0 = 1$.
Define the complex function  $f: \C \to \C$ by:
:$\map f z = \map \exp z \, \map \exp {z_1 + z_2 - z}$
Then find its derivative:
{{begin-eqn}}
{{eqn | l = D_z \, \map f z
      | r = \paren {D_z \, \map \exp z} \map \exp {z_1 + z_2 - z} + \map \exp z \paren {D_z \map \exp {z_1 + z_2 - z} }
      | c = Derivative of Complex Composite Function
}}
{{eqn | r = \map \exp z \, \map \exp {z_1 + z_2 - z} + \map \exp z \, \map \exp {z_1 + z_2 - z} \map {D_z} {z_1 + z_2 - z}
      | c = as $\exp$ is its own derivative
}}
{{eqn | r = \map \exp z \, \map \exp {z_1 + z_2 - z} - \map \exp z \, \map \exp {z_1 + z_2 - z}
      | c = Derivative of Complex Power Series
}}
{{eqn | r = 0
}}
{{end-eqn}}
From Zero Derivative implies Constant Complex Function, it follows that $f$ is constant.
Then:
{{begin-eqn}}
{{eqn | l = \map \exp {z_1} \, \map \exp {z_2}
      | r = \map f {z_1}
}}
{{eqn | r = \map f 0
      | c = as $f$ is constant
}}
{{eqn | r = \map \exp 0 \, \map \exp {z_1 + z_2}
}}
{{eqn | r = \map \exp {z_1 + z_2}
      | c = as $\map \exp 0 = 1$ 
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Cosine Function is Even

:$\map \cosh {-x} = \cosh x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \cosh {-x}
      | r = \frac {e^{-x} + e^{-\paren {-x} } } 2
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \frac {e^{-x} + e^x} 2
}}
{{eqn | r = \frac {e^x + e^{-x} } 2
}}
{{eqn | r = \cosh x
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Cosine Function is Even

:$\map \cosh {-x} = \cosh x$

Proof:
{{begin-eqn}}
{{eqn	| l = \map \cosh {-x}
	| r = \map \cos {-i x}
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn	| r = \map \cos {i x}
	| c = Cosine Function is Even
}}
{{eqn	| r = \cosh x
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Tangent Function is Odd

Let $\tanh: \C \to \C$ be the hyperbolic tangent function on the set of complex numbers.
Then $\tanh$ is odd:
:$\map \tanh {-x} = -\tanh x$

Proof:
{{begin-eqn}}
{{eqn | l = \map \tanh {-x}
      | r = \frac {\map \sinh {-x} } {\map \cosh {-x} } 
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{eqn | r = \frac {-\sinh x} {\map \cosh {-x} } 
      | c = Hyperbolic Sine Function is Odd
}}
{{eqn | r = \frac {-\sinh x} {\cosh x} 
      | c = Hyperbolic Cosine Function is Even
}}
{{eqn | r = -\tanh x
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Sine in terms of Sine

Let $z \in \C$ be a complex number.
Then:
:$i \sinh z = \map \sin {i z}$
where:
:$\sin$ denotes the complex sine
:$\sinh$ denotes the hyperbolic sine
:$i$ is the imaginary unit: $i^2 = -1$.

Proof:
{{begin-eqn}}
{{eqn | l = \map \sin {i z}
      | r = \frac {e^{i \paren {i z} } - e^{i \paren {-i z} } } {2 i}
      | c = Euler's Sine Identity
}}
{{eqn | r = \paren {-i} \frac {e^{-z} - e^z} 2
      | c = $i^2 = -1$
}}
{{eqn | r = i \frac {e^z - e^{-z} } 2
      | c = $i^2 = -1$
}}
{{eqn | r = i \sinh z
      | c = {{Defof|Hyperbolic Sine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Cosine in terms of Cosine

Let $z \in \C$ be a complex number.
Then:
:$\cosh z = \map \cos {i z}$
where:
:$\cos$ denotes the complex cosine
:$\cosh$ denotes the hyperbolic cosine
:$i$ is the imaginary unit: $i^2 = -1$.

Proof:
{{begin-eqn}} 
{{eqn | l = \map \cos {i z}
      | r = \frac {e^{i \paren {i z} } + e^{-i \paren {i z} } } 2
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac {e^{-z} + e^z} 2
      | c = $i^2 = -1$
}}
{{eqn | r = \cosh z
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Tangent in terms of Tangent

Let $z \in \C$ be a complex number.
Then:
:$i \tanh z = \map \tan {i z}$
where:
:$\tan$ denotes the tangent function
:$\tanh$ denotes the hyperbolic tangent
:$i$ is the imaginary unit: $i^2 = -1$.

Proof:
{{begin-eqn}} 
{{eqn | l = \map \tan {i z}
      | r = \frac {\map \sin {i z} } {\map \cos {i z} }
      | c = {{Defof|Complex Tangent Function}}
}}
{{eqn | r = \frac {i \sinh z} {\map \cos {i z} }
      | c = Hyperbolic Sine in terms of Sine
}}
{{eqn | r = \frac {i \sinh z} {\cosh z}
      | c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn | r = i \tanh z
      | c = {{Defof|Hyperbolic Tangent}}
}}
{{end-eqn}}
{{qed}}
Theorem: Order-Extension Principle

Let $S$ be a set.
Let $\preceq$ be an ordering on $S$.
Then there exists a total ordering $\le$ on $S$ such that:
:$\forall a, b \in S: \paren {a \preceq b \implies a \le b}$

Proof:
Let $\preceq$ be an ordering on the set $S$.
If $\preceq$ is a total ordering, the result is complete.
Suppose, then, that $\preceq$ is not a total ordering.
Let $\TT$ be the set of orderings on $S$ that extend $\preceq$, ordered by inclusion.
Let $C$ be a chain in $T$.
By Union of Chain of Orderings is Ordering, $\bigcup C$ is an ordering.
Thus every chain in $\TT$ has an upper bound in $\TT$.
By Zorn's Lemma, $\TT$ has a maximal element, $\RR$.
$\RR$ is seen to be the total ordering whose existence is to be demonstrated, as follows:
Suppose that:
:$\exists a, b \in S: \tuple {a, b} \notin \RR \land \tuple {b, a} \notin \RR$
Let $\RR'$ be the relation defined as:
:$\RR' := \RR \cup \set {\tuple {a, b} }$
Let $\RR'^-$ be the transitive closure of $\RR'$.
Then by Partial Ordering can be Expanded to compare Additional Pair, $\RR'^-$ is an ordering.
But $\RR'^- \supsetneq \RR$, contradicting the maximality of $\RR$.
Thus, $\RR$ is a total ordering.
{{qed}}
Theorem: Order-Extension Principle

Let $S$ be a set.
Let $\preceq$ be an ordering on $S$.
Then there exists a total ordering $\le$ on $S$ such that:
:$\forall a, b \in S: \paren {a \preceq b \implies a \le b}$

Proof:
Let $\prec$ be the reflexive reduction of $\preceq$.
By Reflexive Reduction of Ordering is Strict Ordering, $\prec$ is a strict ordering.
By the strict form of the Order-Extension Principle, there exists a strict total ordering $<$ on $S$ such that:
:$\forall a, b \in S: \paren {a \prec b \implies a < b}$
Let $\le$ be the reflexive closure of $<$.
Let $a, b \in S$.
If $a \preceq b$, then by Law of Excluded Middle either $a \prec b$ or $a = b$.
If $a = b$, then by the definition of reflexive closure, $a \le b$.
If $a \prec b$, then by the choice of $<$, $a < b$ so $a \le b$.
Thus for all $a, b \in S$, $a \preceq b \implies a < b$.
By Reflexive Closure of Strict Total Ordering is Total Ordering, $\le$ is a total ordering.
{{qed}}
Theorem: Order-Extension Principle

Let $S$ be a set.
Let $\preceq$ be an ordering on $S$.
Then there exists a total ordering $\le$ on $S$ such that:
:$\forall a, b \in S: \paren {a \preceq b \implies a \le b}$

Proof:
Let $\AA$ be the set of relations $A$ on $S$ with the property that the transitive closure $A^+$ of $A$ is a strict ordering of $S$.
For each $\tuple {x, y} \in S \times S$, let $\tuple {x, y}' = \tuple {y, x}$.
Let $A \in \AA$.
Let $\tuple {x, y} \in S \times S$.
Let $\tuple {x, y} \in A^+$.
Then:
:$\paren {A \cup \set {\tuple {x, y} } }^+ = A^+$
so:
:$A \cup \set {\tuple {x, y} } \in \AA$
Let $\tuple {y, x} \in A^+$.
Then:
:$\paren {A \cup \set {\tuple {y, x} } }^+ = A^+$
so:
:$A \cup \set {\tuple {x, y}'} = A \cup \set {\tuple {y, x} } \in \AA$
Otherwise, $x$ and $y$ are non-comparable by $A^+$.
So by Strict Ordering can be Expanded to Compare Additional Pair:
:$A \cup \set {\tuple {x, y} } \in \AA$
Thus it has been shown that for each $A \in \AA$ and each $\tuple {x, y} \in S$, either:
:$A \cup \set {\tuple {x, y} } \in \AA$
or:
:$A \cup \set {\tuple {x, y}'} \in \AA$
{{qed|lemma}}
Let $A \subseteq S \times S$.
Let $A \in \AA$.
Let $F$ be a finite subset of $A$.
Since $A^+$ is a strict ordering, it is asymmetric.
Since Transitive Closure is Closure Operator, $F^+ \subseteq A^+$.
So $F^+$ is also asymmetric.
Since $F^+$ is also transitive, it is a strict ordering.
So $F \in \AA$.
Suppose instead that each finite subset of $A$ is in $\AA$.
We must show that $A^+$ is antireflexive.
{{AimForCont}} that for some $x \in S$, $\tuple {x, x} \in A^+$.
Then by the definition of transitive closure, there are elements $y_0, \dots, y_n$ such that $x = y_0 = y_n$ and:
:$\tuple {y_0, y_1}, \tuple {y_1, y_2}, \dotsc, \tuple {y_{n - 1}, y_n} \in A$
Let $F = \set {\tuple {y_0, y_1}, \tuple {y_1, y_2}, \dotsc, \tuple {y_{n - 1}, y_n} }$.
Then $F$ is a finite subset of $A$.
But $\tuple {x, x} \in F^+$, contradicting the fact that $F \in \AA$.
Thus we see that $A^+$ is antireflexive, and thus a strict ordering of $S$.
Therefore, $\AA$ has finite character.
{{qed|lemma}}
Note that ${\prec} = {\prec^+}$, so ${\prec} \in \AA$.
By the Restricted Tukey's Theorem (Strong Form), there exists an $R \in \AA$ such that:
:${\prec} \subseteq R$
:For each $\tuple {m, n} \in S \times S$, either $\tuple {m, n} \in R$ or $\tuple {n, m} = \tuple {m, n}' \in R$.
Then:
:$R^+$ is a strict total ordering of $S$.
:$\forall a, b \in S: a \prec b \implies a < b$
{{qed}}
Theorem: Union of Chain of Orderings is Ordering

Let $S$ be a set.
Let $C$ be a non-empty chain of orderings on $S$.
Then $\bigcup C$ is an ordering on $S$.

Proof:
{{improve|Use letters (mathcaled if you like) to denote an arbitrary ordering rather than actual arbitrary ordering symbols which make it confusing and difficult to read}}
Let $\preceq$ be an arbitrary element of $C$.
Let ${\sim} = \bigcup C$.
Checking in turn each of the criteria for an ordering:
Let $a, b \in S$.
Let $a \sim b$ and $b \sim a$.
Since $a \sim b$ and $b \sim a$, there exist $\preceq_1, \preceq_2 \, \in \, C$ such that $a \preceq_1 b$ and $b \preceq_2 a$.
Since $C$ is a chain:
:${\preceq_1} \subset {\preceq_2}$
or:
:${\preceq_2} \subset {\preceq_1}$
{{WLOG}}, suppose ${\preceq_1} \subset {\preceq_2}$.
Then it must hold that $a \preceq_2 b$.
Since:
:$a \preceq_2 b$
:$b \preceq_2 a$
:${\preceq_2} \in T$ is an ordering
it follows that:
:$a = b$
and so $\sim$ is antisymmetric.
{{qed|lemma}}
Theorem: Partial Ordering can be Expanded to compare Additional Pair

Let $\struct {S, \preceq}$ be an ordered set.
Let $a$ and $b$ be non-comparable elements of $S$.
That is, let:
:$a \not\preceq b$
and:
:$b \not\preceq a$
Let ${\preceq'} = {\preceq} \cup \set {\tuple {a, b} }$.
Let $\preceq'^+$ be the transitive closure of $\preceq'$.
Then:
:$\preceq'^+$ is an ordering.
$\preceq'^+$ can be defined by letting $p \preceq'^+ q$ {{iff}}:
:$p \preceq q$ or
:$p \preceq a$ and $b \preceq q$.

Proof:
Let $\prec$ be the reflexive reduction of $\preceq$.
Let $\prec' = {\prec} \cup \set {\tuple {a, b} }$.
By Reflexive Reduction of Ordering is Strict Ordering, $\prec$ is a strict ordering.
Define a relation $\prec'_2$ by letting $p \prec'_2 q$ {{iff}}:
:$p \prec q$ or
:$p \preceq a$ and $b \preceq q$
By Strict Ordering can be Expanded to Compare Additional Pair, $\prec'_2$ is a strict ordering and is the transitive closure of $\prec'$.
Then the reflexive closure of $\prec'_2$, ${\prec'_2}^=$ is the transitive reflexive closure of $\prec'$.
From Equivalence of Definitions of Reflexive Transitive Closure, ${\prec'_2}^=$ is the transitive closure of the reflexive closure of $\prec'$.
The reflexive closure of $\prec'$ is $\preceq'$, so ${\prec'_2}^=$ is the transitive closure of $\preceq'$.
But ${\prec'_2}^=$ is clearly the relation defined by the two conditions in the theorem statement.
{{qed}}
Theorem: Recursive Construction of Transitive Closure

Let $\RR$ be a relation.
The '''transitive closure''' $\RR^+$ of $\RR$ can be constructed as follows:
Let:
:$\RR_n := \begin {cases} \RR & : n = 0 \\ \RR_{n - 1} \cup \set {\tuple {x_1, x_3}: \exists x_2: \tuple {x_1, x_2} \in \RR_{n-1} \land \tuple {x_2, x_3} \in \RR_{n - 1} } & : n > 0 \end{cases}$
Finally, let:
:$\ds \RR^+ = \bigcup_{i \mathop \in \N} \RR_i$
Then $R^+$ is the '''transitive closure''' of $R$.

Proof:
We must show that:
:$(1): \quad \RR \subseteq \RR^+$
:$(2): \quad \RR^+$ is transitive
:$(3): \quad \RR^+$ is the smallest relation with both of those characteristics.