avewright/proofwiki-math huggingface dataset:
Theorem: Sum of Squares of Sine and Cosine

:$\cos^2 x + \sin^2 x = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \cos^2 x + \sin^2 x
      | r = \paren {\cos x + i \, \sin x} \paren {\cos x - i \, \sin x}
      | c = factoring over the complex numbers
}}
{{eqn | r = \paren {\cos x + i \, \sin x} \paren {\map \cos {-x} + i \, \map \sin {-x} }
      | c = Cosine Function is Even and Sine Function is Odd
}}
{{eqn | r = e^{ix} \, e^{-ix}
      | c = Euler's Formula
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Squares of Sine and Cosine

:$\cos^2 x + \sin^2 x = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \cos^2 x + \sin^2 x
      | r = \paren {\frac {e^{i x} + e^{-i x} } 2}^2 + \sin^2 x
      | c = Euler's Cosine Identity
}}
{{eqn | r = \paren {\frac {e^{i x} + e^{-i x} } 2}^2 + \paren {\frac {e^{i x} - e^{-i x} } {2 i} }^2
      | c = Euler's Sine Identity
}}
{{eqn | r = \frac {\paren {e^{i x} }^2 + 2 e^{-i x} e^{i x} + \paren {e^{-i x} }^2} 4 + \paren {\frac {e^{i x} - e^{-i x} } {2 i} }^2
      | c = Square of Sum
}}
{{eqn | r = \frac {\paren {e^{i x} }^2 + 2 e^{-i x} e^{i x} + \paren {e^{-i x} }^2} 4 + \frac {\paren {e^{i x} }^2 - e^{-i x} e^{i x} + \paren {e^{-i x} }^2} {-4} 
      | c = Square of Difference and $i^2 = -1$
}}
{{eqn | r = \frac {e^{2 i x} + 2 + e^{-2 i x} } 4 + \frac {e^{2 i x} - 2 + e^{-2 i x} } {-4} 
      | c = Exponential of Sum
}}
{{eqn | r = \frac {e^{2 i x} + 2 + e^{-2 i x} - e^{2 i x} + 2 - e^{-2 i x} } 4
      | c = simplifying
}}
{{eqn | r = \frac 4 4
      | c = simplifying
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Sum

:$\map \cos {a + b} = \cos a \cos b - \sin 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}}
The result follows by equating the real parts.
{{qed}}
Theorem: Cosine of Sum

:$\map \cos {a + b} = \cos a \cos b - \sin 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 {{WRT|Differentiation}} $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: Cosine of Sum

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

Proof:
{{begin-eqn}} 
{{eqn | l = \cos a \cos b - \sin a \sin b
      | r = \paren {\frac {e^{i a} + e^{-i a} } 2} \paren {\frac {e^{i b} + e^{-i b} } 2} - \sin a \sin b
      | c = Euler's Cosine Identity
}}
{{eqn | r = \paren {\frac {e^{i a} + e^{-i a} } 2} \paren {\frac {e^{i b} + e^{-i b} } 2} - \paren {\frac {e^{i a} - e^{-i a} } {2 i} } \paren {\frac {e^{i b} - e^{-i b} } {2 i} }
      | c = Euler's Sine 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
}}
{{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^2}
}}
{{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
}}
{{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
      | c = as $i^2 = -1$
}}
{{eqn | r = \frac {e^{i a} e^{i b} + e^{-ia} e^{-ib} } 2
}}
{{eqn | r = \frac {e^{i \paren {a + b} } + e^{-i \paren {a + b} } } 2
      | c = Exponential of Sum 
}}
{{eqn | r = \map \cos {a + b}
      | c = Euler's Cosine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Sum

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

Proof:
:File:Tri1.PNG
$AB$, $AC$, $AE$, and $AD$ are radii of the circle centered at $A$.
Let $\angle BAC = a$ and $\angle DAC = \angle BAE = b$.
By Euclid's First Postulate, we can construct line segments $BD$ and $CE$.
By Euclid's second common notion, $\angle DAB = \angle CAE$.
Thus by Triangle Side-Angle-Side Congruence, $\triangle DAB \cong \triangle CAE$.
Therefore, $DB = CE$.
We now assign Cartesian coordinates to the points $B$, $C$, $D$, and $E$:
{{begin-eqn}}
{{eqn | l = B
      | r = \tuple {1, 0}
      | c = 
}}
{{eqn | l = C
      | r = \tuple {\cos a, \sin a}
      | c = 
}}
{{eqn | l = D
      | r = \tuple {\map \cos {a + b}, \map \sin {a + b} }
      | c = 
}}
{{eqn | l = E
      | r = \tuple {\cos b, -\sin b}
      | c = Cosine Function is Even and Sine Function is Odd
}}
{{end-eqn}}
We use the definition of the distance function on the Euclidean space $\struct {\R^2, d}$ as defined by the Euclidean metric:
:$\forall x, y \in \R^2: \map d {x, y} = \sqrt {\paren {x_1 - x_2}^2 + \paren {y_1 - y_2}^2}$
where $x = \tuple {x_1, y_1}, y = \tuple {x_2, y_2}$.
Thus:
:$DB \cong CE \iff \map d {D, B} = \map d {C, E}$
So, plugging in the coordinates of $B, C, D, E$, we get:
{{begin-eqn}}
{{eqn | l = \paren {\map \cos {a + b} } - 1)^2 + \map {\sin^2} {a + b}
      | r = \paren {\cos a - \cos b}^2 + \paren {\sin a + \sin b}^2
}}
{{eqn | ll= \leadsto
      | l = \cos^2 \left({a + b}\right) + \sin^2 \left({a + b}\right)
      | o = 
      | c = multiplying out {{LHS}}
}}
{{eqn | l = {} - 2 \, \map \cos {a + b} + 1
      | r = \paren {\cos a - \cos b}^2 + \paren {\sin a + \sin b}^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 1 - 2 \, \map \cos {a + b} + 1
      | r = \paren {\cos a - \cos b}^2 + \paren {\sin a + \sin b}^2
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = 2 - 2 \, \map \cos {a + b}
      | r = \cos^2 a - 2 \cos a \cos b + \cos^2 b
      | c = multiplying out {{RHS}}
}}
{{eqn | o = 
      | ro= +
      | r = \sin^2 a + 2 \sin a \sin b + \sin^2 b
}}
{{eqn | ll= \leadsto
      | l = 2 - 2 \, \map \cos {a + b}
      | r = 2 - 2 \cos a \cos b + 2 \sin a \sin b
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \map \cos {a + b}
      | r = \cos a \cos b - \sin a \sin b
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Sum

:$\map \cos {a + b} = \cos a \cos b - \sin 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 \cos {a + b }
      | r = FC
      | c = 
}}
{{eqn | r = AB - DF
      | c = 
}}
{{eqn | r = \cos a \cos b - \sin a \sin b
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Sum

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

Proof:
{{begin-eqn}}
{{eqn | l = \map \cos {a + b}
      | r = \map \cos {a - \paren {-b} }
      | c = 
}}
{{eqn | r = \cos a \map \cos {-b} + \sin a \map \sin {-b}
      | c = Cosine of Difference
}}
{{eqn | r = \cos a \cos b + \sin a \paren {-\sin b}
      | c = Cosine Function is Even, Sine Function is Odd
}}
{{eqn | r = \cos a \cos b - \sin a \sin b
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Cosine of Sum

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

Proof:
400px
Let two triangles $\triangle ABC$ and $\triangle ABD$ be inscribed in a circle in the same semicircle:.
By Thales' Theorem, these are both right triangles with:
:$ \angle ACB = \angle ADB = 90 \degrees$
Let $AB = 1$.
Join $DC$.
By construction, $\Box ABCD$ is a cyclic quadrilateral.
Let:
:$\angle CAB = \alpha$
:$\angle DBA = \beta$
:$\angle DAC = \gamma$
From the construction above, we have the following:
:$\cos \alpha = AC$
:$\cos \beta = BD$
:$\sin \alpha = CB$
:$\sin \beta = AD$
:$\gamma = \dfrac \pi 2 - \alpha - \beta$
By Length of Chord of Circle:
:$CD = 2 r \map \sin {\gamma}$
Since $2r \mathop = 1$:
:$CD = \map \sin {\gamma}$
Therefore:
{{begin-eqn}}
{{eqn | l = CD
      | r = \map \sin {\gamma}
      | c = 
}}
{{eqn | r = \map \cos {\dfrac \pi 2 - \gamma}
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = \map \cos {\alpha + \beta}
      | c = $\gamma$ is complementary to $\alpha + \beta$
}}
{{end-eqn}}
By Ptolemy's Theorem:
:$AC \times BD = AD \times BC + AB \times CD$
Substituting:
:$\cos \alpha \times \cos \beta  = \sin \beta \times \sin \alpha + 1 \times \map \cos {\alpha + \beta}$
Rearranging:
:$\cos \tuple {\alpha + \beta} = \cos \alpha \cos \beta - \sin \alpha \sin \beta$
By Equivalence of Definitions of Cosine of Angle, the definition of cosine 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:
:$ \cos {\pi} = \cos \dfrac {\pi} 2 \cos \dfrac {\pi} 2 - \sin \dfrac {\pi} 2 \sin \dfrac {\pi} 2$
:$ -1 = 0 \cdot 0  - 1 \cdot 1$
The result follows.
{{qed}}
Theorem: Characterisation of Sine and Cosine

Let $\map s x: \R \to \R$, $\map c x: \R \to \R$ be differentiable real functions that satisfy:
:$(1): \quad \map {s'} x = \map c x$
:$(2): \quad \map {c'} x = -\map s x$
:$(3): \quad \map s 0 = 0$
:$(4): \quad \map c 0 = 1$
:$(5): \quad \forall x: \map {s^2} x + \map {c^2} x = 1$
Then, for every $x \in \R$:
:$\map s x = \map \sin x$
:$\map c x = \map \cos x$

Proof:
Define:
:$\map h x = \paren {\map c x - \map \cos x}^2 + \paren {\map s x - \map \sin x}^2$
Then:
{{begin-eqn}}
{{eqn | l = \map h x
      | r = \map {c^2} x - 2 \map c x \map \cos x + \map {\cos^2} x + \map {s^2} x - 2 \map s x \map \sin x + \map {\sin^2} x
      | c = Square of Difference
}}
{{eqn | r = 2 - 2 \paren {\map c x \map \cos x + \map s x \map \sin x}
      | c = Property $(5)$, Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
By taking $\map {h'} x$:
{{begin-eqn}}
{{eqn | l = \map {h'} x
      | r = -2 \paren {\map c x \map \cos x + \map s x \map \sin x}'
      | c = Linear Combination of Derivatives, Derivative of Constant
}}
{{eqn | r = -2 \paren {\map c x \map {\cos'} x + \map {c'} x \map \cos x + \map s x \map {\sin'} x + \map {s'} x \map \sin x}
      | c = Product Rule for Derivatives
}}
{{eqn | r = -2 \paren {-\map c x \map \sin x - \map s x \map \cos x + \map s x \map \cos x + \map c x \map \sin x}
      | c = Properties $(1)$ and $(2)$, Derivative of Cosine Function, Derivative of Sine Function
}}
{{eqn | r = -2 \paren {\map c x \map \sin x - \map c x \map \sin x} - 2 \paren {\map s x \map \cos x - \map s x \map \cos x}
}}
{{eqn | r = 0
}}
{{end-eqn}}
By Zero Derivative implies Constant Function, $\map h x$ is a constant function:
:$\map h x = k$
Also:
{{begin-eqn}}
{{eqn | l = \map h 0
      | r = \paren {1 - 1}^2 + \paren {0 - 0}^2
      | c = Properties $(3)$ and $(4)$, Cosine of Zero is One, Sine of Zero is Zero
}}
{{eqn | r = 0
}}
{{end-eqn}}
Since $\map h x$ is constant:
:$\map h x = 0$
Therefore:
:$\paren {\map c x - \map \cos x}^2 + \paren {\map s x - \map \sin x}^2 = 0$
for every $x \in \R$.
But since Square of Real Number is Non-Negative and Square of Non-Zero Real Number is Strictly Positive:
:$\map c x - \map \cos x = 0$
:$\map s x - \map \sin x = 0$
The result follows.
{{qed}}
Category:Sine Function
Category:Cosine Function
6itor0t8ntefy8v25lw79ra6dsg0ony
Theorem: Real Cosine Function is Bounded

:$\size {\cos x} \le 1$

Proof:
From the algebraic definition of the real cosine function:
:$\ds \cos x = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}$
it follows that $\cos x$ is a real function.
Similarly, $\sin x$ is also a real function.
Thus it follows that:
{{begin-eqn}}
{{eqn | l = \cos^2 x
      | o = \le
      | r = \cos^2 x + \sin^2 x
      | c = as $\sin^2 x \ge 0$ by Square of Real Number is Non-Negative
}}
{{eqn | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{end-eqn}}
From Ordering of Squares in Reals and the definition of absolute value, we have that:
:$x^2 \le 1 \iff \size x \le 1$
The result follows.
{{qed}}
Theorem: Boundedness of Sine X over X

Let $x \in \R$.
Then:
:$\size {\dfrac {\sin x} x} \le 1$

Proof:
From Derivative of Sine Function, we have:
:$D_x \paren {\sin x} = \cos x$
So by the Mean Value Theorem, there exists $\xi \in \R$ between $0$ and $x$ such that:
:$\dfrac {\sin x - \sin 0} {x - 0} = \cos \xi$
From Real Cosine Function is Bounded we have that:
:$\size {\cos \xi} \le 1$
{{qed}}
Theorem: Sine and Cosine are Periodic on Reals

The real sine function and real cosine function are periodic on the set of real numbers $\R$:

Proof:
From the Real Cosine Function is Periodic and Real Sine Function is Periodic, we have that $\cos x$ and $\sin x$ are periodic on $\R$ with the same period.
If we denote the period of $\cos x$ and $\sin x$ as $p$, it follows that $\pi = \dfrac p 2$ is uniquely defined.
{{qed}}
Theorem: Sine and Cosine are Periodic on Reals

The real sine function and real cosine function are periodic on the set of real numbers $\R$:

Proof:
By Cosine of Zero is One:
:$\cos 0 = 1$
By Cosine of 2 is Strictly Negative:
:$\cos 2 < 0$
Thus by {{Corollary|Intermediate Value Theorem}} there exists an $h \in \openint 0 2$ such that:
:$\cos h = 0$
By Sine of Sum for all $x \in \R$:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \map \sin {x - h} \cos h + \map \cos {x -h} \sin h
}}
{{eqn | n = 1
      | r = \map \cos {x -h} \sin h
}}
{{end-eqn}}
By Cosine of Sum for all $x \in \R$:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \map \cos {x - h} \cos h - \map \sin {x -h} \sin h
}}
{{eqn | n = 2
      | r = -\map \sin {x - h} \sin h
}}
{{end-eqn}}
By Sum of Squares of Sine and Cosine:
{{begin-eqn}}
{{eqn | l = \sin^2 h
      | r = \cos^2 h + \sin^2 h
}}
{{eqn | n = 3
      | r = 1
}}
{{end-eqn}}
Thus for all $x \in \R$:
{{begin-eqn}}
{{eqn | l = \map \cos {x + 4 h}
      | r = - \map \sin {x + 3 h} \sin h
      | c = by $(2)$
}}
{{eqn | r = - \map \cos {x + 2 h} \sin^2 h
      | c = by $(1)$
}}
{{eqn | r = \map \cos {x + h} \sin^3 h
      | c = by $(2)$
}}
{{eqn | r = \cos x \sin^4 h
      | c = by $(1)$
}}
{{eqn | r = \cos x
      | c = by $(3)$
}}
{{end-eqn}}
In particular, $\cos$ is periodic.
By Nonconstant Periodic Function with no Period is Discontinuous Everywhere, $\cos$ has a period $p \in \R_{>0}$.
In view of $(1)$ and $\sin h \ne 0$, the periodic elements of $\sin$ are exactly those of $\cos$.
Thus $p$ is also the period of $\sin$.
{{qed}}
Theorem: Sine and Cosine are Periodic on Reals

The real sine function and real cosine function are periodic on the set of real numbers $\R$:

Proof:
Since Real Cosine Function is Periodic, let $K$ be its period.
Then:
:$\cos K = \map \cos {0 + K} = \cos 0$
Because Cosine of Zero is One:
:$\cos K = 1$
Furthermore:
{{begin-eqn}}
{{eqn | l = \cos^2 K + \sin^2 K
      | r = 1
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | l = \sin^2 K
      | r = 0
      | c = $\cos K = 1$
}}
{{eqn | l = \sin K
      | r = 0
}}
{{end-eqn}}
Then, the following holds:
{{begin-eqn}}
{{eqn | l = \map \sin {x + K}
      | r = \sin x \cos K + \cos x \sin K
      | c = Sine of Sum
}}
{{eqn | r = \sin x \cdot 1 + \cos x \cdot 0
      | c = $\cos K = 1$; $\sin K = 0$
}}
{{eqn | r = \sin x}}
{{end-eqn}}
Thus $\sin$ is periodic with some period $L \leq K$.
{{qed|lemma}}
The following also hold:
{{begin-eqn}}
{{eqn | l = \sin L
      | r = \map \sin {0 + L}
}}
{{eqn | r = \sin 0
      | c = Period of Periodic Real Function
}}
{{eqn | r = 0
      | c = Sine of Zero is Zero
}}
{{eqn | l = \cos L
      | r = \bigvalueat { \dfrac{\d \sin x} {\d x} } {x \mathop = L}
      | c = Derivative of Sine Function
}}
{{eqn | r = \lim_{h \mathop \to 0} \dfrac{\map \sin {L + h} - \map \sin L}{h}
      | c = Derivative of Real Function at Point
}}
{{eqn | r = \lim_{h \mathop \to 0} \dfrac{\map \sin {0 + h} - \map \sin 0}{h}
      | c = Period of Periodic Real Function
}}
{{eqn | r = \bigvalueat { \dfrac{\d \sin x} {\d x} } {x \mathop = 0}
      | c = Derivative of Real Function at Point
}}
{{eqn | r = \cos 0
      | c = Derivative of Sine Function
}}
{{eqn | r = 1
      | c = Cosine of Zero is One
}}
{{end-eqn}}
So we may conclude:
{{begin-eqn}}
{{eqn | l = \map \cos {x + L}
      | r = \cos x \cos L - \sin x \sin L
      | c = Cosine of Sum
}}
{{eqn | r = \cos x \cdot 1 - \sin x \cdot 0
      | c = $\cos L = 1$ and $\sin L = 0$
}}
{{eqn | r = \cos x}}
{{end-eqn}}
Therefore the period of cosine is at most that of sine:
:$K \leq L$
But if $K \leq L \leq K$ then:
:$K = L$
{{qed}}
Theorem: Sine and Cosine are Periodic on Reals

The real sine function and real cosine function are periodic on the set of real numbers $\R$:

Proof:
Since Real Cosine Function is Periodic, let $L$ be its period.
From Primitive of Cosine Function:
{{:Primitive of Cosine Function}}
for any constant $C$.
Therefore $\sin x$ is a Primitive of $\cos x$, for the special case of $C = 0$.
From Primitive of Periodic Real Function, it follows that $\sin x$ is periodic with period $L$.
{{qed}}
Theorem: Differentiable Bounded Convex Real Function is Constant

Let $f$ be a real function which is:
:$(1): \quad$ differentiable on $\R$
:$(2): \quad$ bounded on $\R$
:$(3): \quad$ convex on $\R$.
Then $f$ is constant.

Proof:
Let $f$ be differentiable and bounded on $\R$.
Let $f$ be convex on $\R$.
Let $\xi \in \R$.
{{AimForCont}} $\map {f'} \xi > 0$.
Then by Mean Value of Convex Real Function it follows that:
:$\map f x \ge \map f \xi + \map {f'} \xi \paren {x - \xi} \to + \infty$ as $x \to +\infty$
and therefore is not bounded.
Similarly, suppose $\map {f'} \xi < 0$.
Then by Mean Value of Convex Real Function it follows that:
:$\map f x \ge \map f \xi + \map {f'} \xi \paren {x - \xi} \to + \infty$ as $x \to -\infty$
and therefore is likewise not bounded.
Hence $\map {f'} \xi = 0$.
From Zero Derivative implies Constant Function, it follows that $f$ is constant.
{{qed}}
Theorem: Banach-Tarski Paradox

Let $\mathbb D^3 \subset \R^3$ be a unit ball in real Euclidean space of $3$ dimensions.
Then $\mathbb D^3$ is equidecomposable to the union of two such unit balls.

Proof:
Let $\mathbb D^3$ be centered at the origin, and $D^3$ be some other unit ball in $\R^3$ such that $\mathbb D^3 \cap D^3 = \O$.
Let $\mathbb S^2 = \partial \mathbb D^3$.
By the Hausdorff Paradox, there exists a decomposition of $ \mathbb S^2$ into four sets $A, B, C, Q$ such that $A, B, C$ and $B \cup C$ are congruent, and $Q$ is countable.
For $r \in \R_{>0}$, define a function $r^*: \R^3 \to \R^3$ as $\map {r^*} {\mathbf x} = r \mathbf x$, and define the sets:
{{begin-eqn}}
{{eqn | l = W
      | r = \bigcup_{0 \mathop < r \mathop \le 1} \map {r^*} A
}}
{{eqn | l = X
      | r = \bigcup_{0 \mathop < r \mathop \le 1} \map {r^*} B
}}
{{eqn | l = Y
      | r = \bigcup_{0 \mathop < r \mathop \le 1} \map {r^*} C
}}
{{eqn | l = Z
      | r = \bigcup_{0 \mathop < r \mathop \le 1} \map {r^*} Q
}}
{{end-eqn}}
Let $T = W \cup Z \cup \set {\mathbf 0}$.
$W$ and $X \cup Y$ are clearly congruent by the congruency of $A$ with $B \cup C$, hence $W$ and $X \cup Y$ are equidecomposable.
Since $X$ and $Y$ are congruent, and $W$ and $X$ are congruent, $X \cup Y$ and $W \cup X$ are equidecomposable.  
$W$ and $X \cup Y$ as well as $X$ and $W$ are congruent, so $W \cup X$ and $W \cup X \cup Y$ are equidecomposable.  
Hence $W$ and $W \cup X \cup Y$ are equidecomposable, by Equidecomposability is Equivalence Relation.
So $T$ and $\mathbb D^3$ are equidecomposable, from Equidecomposability Unaffected by Union.
Similarly we find $X$, $Y$, and $W \cup X \cup Y$ are equidecomposable.
Since $Q$ is only countable, but $\map {\operatorname {SO} } 3$ is not, we have:
:$\exists \phi \in \map {\operatorname {SO} } 3: \map \phi Q \subset A \cup B \cup C$
so that $I = \map \phi Q \subset W \cup X \cup Y$.
Since $X$ and $W \cup X \cup Y$ are equidecomposable, by Subsets of Equidecomposable Subsets are Equidecomposable, $\exists H \subseteq X$ such that $H$ and $I$ are equidecomposable.
Finally, let $p \in X - H$ be a point and define $S = Y \cup H \cup \set p$.
Since:
:$Y$ and $W \cup X \cup Y$
:$H$ and $Z$
:$\set 0$ and $\set p$
are all equidecomposable in pairs, $S$ and $\mathbb B^3$ are equidecomposable by Equidecomposability Unaffected by Union.
Since $D^3$ and $\mathbb D^3$ are congruent, $D^3$ and $S$ are equidecomposable, from Equidecomposability is Equivalence Relation.  
By Equidecomposability Unaffected by Union, $T \cup S$ and $\mathbb D^3 \cup D^3$ are equidecomposable.
Hence $T \cup S \subseteq \mathbb D^3 \subset \mathbb D^3 \cup D^3$ are equidecomposable and so, by the chain property of equidecomposability, $\mathbb D^3$ and $\mathbb D^3 \cup D^3$ are equidecomposable.
{{qed}}