avewright/proofwiki-math huggingface dataset:
Theorem: Composition of Mappings is Associative

The composition of mappings is an associative binary operation:
:$\paren {f_3 \circ f_2} \circ f_1 = f_3 \circ \paren {f_2 \circ f_1}$
where $f_1, f_2, f_3$ are arbitrary mappings which fulfil the conditions for the relevant compositions to be defined.

Proof:
:<nowiki>$\begin{xy}
<0em,12em>*+{E} = "TL",
<12em,12em>*+{G} = "TR",
<0em,0em>*+{F} = "BL",
<12em,0em>*+{H} = "BR",
"TL";"TR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f_2 \circ f_1},
"BL";"BR" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f_3 \circ f_2},
"TL";"BL" **@{-} ?>*@{>} ?<>(.5)*!/^1em/{f_1},
"BL";"TR" **@{-} ?>*@{>} ?<>(.3)*!/_1em/{f_2},
"TR";"BR" **@{-} ?>*@{>} ?<>(.5)*!/_1em/{f_3},
"TL";"BR" **@{.} ?>*@{>} ?<>(.7)*!/_-1.8em/{f_3 \circ f_2 \circ f_1},
\end{xy}$</nowiki>
From the definition, we know that a mapping is a relation.
First, note that from the definition of composition of relations, the following must be the case before the above expression is even to be defined:
:$(1): \quad \Dom {f_2} = \Cdm {f_1}$
:$(2): \quad \Dom {f_3} = \Cdm {f_2}$
where $\Cdm f$ denotes the codomain of the mapping $f$.
The two '''composite relations''' can be seen to have the same domain, as follows:
{{begin-eqn}}
{{eqn | l = \Dom {\paren {f_3 \circ f_2} \circ f_1}
      | r = \Dom {f_1}
      | c = Domain of Composite Relation
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \Dom {f_3 \circ \paren {f_2 \circ f_1} }
      | r = \Dom {f_2 \circ f_1}
      | c = Domain of Composite Relation
}}
{{eqn | r = \Dom {f_1}
      | c = Domain of Composite Relation
}}
{{end-eqn}}
Also they have the same codomain, as is seen by:
{{begin-eqn}}
{{eqn | l = \Cdm {\paren {f_3 \circ f_2} \circ f_1}
      | r = \Cdm {f_3 \circ f_2}
      | c = Codomain of Composite Relation
}}
{{eqn | r = \Cdm {f_3}
      | c = Codomain of Composite Relation
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \Cdm {f_3 \circ \paren {f_2 \circ f_1} }
      | r = \Cdm {f_3}
      | c = Codomain of Composite Relation
}}
{{end-eqn}}
As a mapping is a relation, we can use that the Composition of Relations is Associative:
:$\forall x \in \Dom {f_1}: \map {\paren {f_3 \circ f_2} \circ f_1} x = \map {f_3 \circ \paren {f_2 \circ f_1} } x$
Hence the result.
{{qed}}
Theorem: Group is Abelian iff it has Cross Cancellation Property

Let $G$ be a group.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$G$ is abelian}}
{{item|(2):|$G$ has the cross cancellation property}}
{{end-itemize}}

Proof:
Let us suppress the operation of $G$ for brevity.
Theorem: Group is Abelian iff it has Middle Cancellation Property

Let $G$ be a group.
{{TFAE}}
{{begin-itemize}}
{{item|(1):|$G$ is abelian}}
{{item|(2):|$G$ satisfies the middle cancellation property}}
{{end-itemize}}

Proof:
Let us suppress the operation of $G$ for brevity.
Theorem: Rational Numbers form Totally Ordered Field

The set of rational numbers $\Q$ forms a totally ordered field under addition and multiplication: $\struct {\Q, +, \times, \le}$.

Proof:
Recall that by Integers form Ordered Integral Domain, $\struct {\Z, +, \times, \le}$ is an ordered integral domain
By Rational Numbers form Field, $\struct {\Q, +, \times}$ is a field.
In the formal definition of rational numbers, $\struct {\Q, +, \times}$ is the field of quotients of $\struct {\Z, +, \times, \le}$
By Total Ordering on Field of Quotients is Unique, it follows that $\struct {\Q, +, \times}$ has a unique total ordering on it that is compatible with its ring structure.
{{explain|Review the ordering / total ordering question}}
Thus $\struct {\Q, +, \times, \le}$ is a totally ordered field.
{{Qed}}
Theorem: Rational Numbers are Densely Ordered

Let $a, b \in \Q$ such that $a < b$.
Then $\exists c \in \Q: a < c < b$.
That is, the set of rational numbers is densely ordered.

Proof:
From the definition of rational numbers, we can express $a$ and $b$ as $a = \dfrac {p_1} {q_1}, b = \dfrac {p_2} {q_2}$.
Thus from Mediant is Between:
:$\dfrac {p_1} {q_1} < \dfrac {p_1 + p_2} {q_1 + q_2} < \dfrac {p_2} {q_2}$
From Rational Numbers form Field:
:$\dfrac {p_1 + p_2} {q_1 + q_2} \in \Q$
Hence $c = \dfrac {p_1 + p_2} {q_1 + q_2}$ is an element of $\Q$ strictly between $a$ and $b$.
{{qed}}
Theorem: Real Addition is Closed

The set of real numbers $\R$ is closed under addition:
:$\forall x, y \in \R: x + y \in \R$

Proof:
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
From the definition of real addition, $x + y$ is defined as:
:$\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n + y_n} } {}$
We have that $\forall i \in \N: x_i \in \Q, y_i \in \Q$, therefore $x_i + y_i \in \Q$.
So it follows that $\eqclass {\sequence {x_n + y_n} } {} \in \R$.
{{qed}}
Theorem: Real Addition is Well-Defined

The operation of addition on the set of real numbers $\R$ is well-defined.

Proof:
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers:
:$\eqclass {\sequence {x_n} } {} \equiv \eqclass {\sequence {y_n} } {} \iff \forall \epsilon > 0: \exists n \in \N: \forall i, j > n: \size {x_i - y_j} < \epsilon$
Let $x = \eqclass {\sequence {x_n} } {}$ and $y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
From the definition of real addition, $x + y$ is defined as:
:$\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n + y_n} } {}$.
We need to show that:
:$\sequence {x_n}, \sequence {x'_n} \in \eqclass {\sequence {x_n} } {}, \sequence {y_n}, \sequence {y'_n} \in \eqclass {\sequence {y_n} } {} \implies \sequence {x_n + y_n} = \sequence {x'_n + y'_n}$
That is:
:$\forall \epsilon > 0: \exists N: \forall i, j > N: \size {\paren {x_i + y_i} - \paren {x'_j + y'_j} } < \epsilon$
Let $\epsilon > 0$, such that:
:$\exists N_1: \forall i, j \ge N_1: \size {x_i - x'_j} < \epsilon / 2$
:$\exists N_2: \forall i, j \ge N_2: \size {y_i - y'_j} < \epsilon / 2$
Now let $N = \max \set {N_1, N_2}$.
Then we have:
:$\forall i, j \ge N: \size {x_i - x'_j} + \size {y_i - y'_j} < \epsilon$
But:
{{begin-eqn}}
{{eqn | l = \epsilon
      | o = >
      | r = \size {x_i - x'_j} + \size {y_i - y'_j}
      | c = 
}}
{{eqn | o = >
      | r = \size {\paren {x_i - x'_j} + \paren {y_i - y'_j} }
      | c = Triangle Inequality
}}
{{eqn | r = \size {\paren {x_i + y_i} - \paren {x'_j + y'_j} }
      | c = 
}}
{{end-eqn}}
So:
:$\forall i, j \ge N: \size {\paren {x_i + y_i} - \paren {x'_j + y'_j} } < \epsilon$
Hence the result.
{{qed}}
Category:Real Addition
8qgf4h4p5nwy6mzoo9i5n9beoijf0e7
Theorem: Real Multiplication is Well-Defined

The operation of multiplication on the set of real numbers $\R$ is well-defined.

Proof:
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let:
:$x = \eqclass {\sequence {x_n} } {}$
:$y = \eqclass {\sequence {y_n} } {}$
where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
From the definition of real multiplication, $x \times y$ is defined as:
:$\eqclass {\sequence {x_n} } {} \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n \times y_n} } {}$
We need to show that:
:$\sequence {x_n}, \sequence {x'_n} \in \eqclass {\sequence {x_n} } {}, \sequence {y_n}, \sequence {y'_n} \in \eqclass {\sequence {y_n} } {} \implies \sequence {x_n \times y_n} = \sequence {x'_n \times y'_n}$
That is:
:$\forall \epsilon > 0: \exists N: \forall i, j > N: \size {\paren {x_i \times y_i} - \paren {x'_j \times y'_j} } < \epsilon$
As $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are Cauchy sequences, from Cauchy Sequence in Metric Space is Bounded they are bounded.
Let:
:$B_x = 2 \map \sup {\sequence {x_n} }$
:$B_y = 2 \map \sup {\sequence {y_n} }$
Let:
:$B = \max \set {B_x, B_y}$
where $\max \set {B_x, B_y}$ denotes the max operation on $B_x$ and $B_y$.
Now let $\epsilon > 0$.
Then:
:$\exists N_1: \forall i, j > N_1: \size B \size {x_i - x'_j} < \epsilon / 2$
:$\exists N_2: \forall i, j > N_2: \size B \size {y_i - y'_j} < \epsilon / 2$
Now let $N = \max \set {N_1, N_2}$.
Then we have:
:$\forall i, j \ge N: \size B \size {x_i - x'_j} + \size B \size {y_i - y'_j} < \epsilon$
So:
{{begin-eqn}}
{{eqn | l = \epsilon
      | o = >
      | r = \size B \size {x_i - x'_j} + \size B \size {y_i - y'_j}
      | c = 
}}
{{eqn | o = \ge
      | r = \size {B \paren {x_i - x'_j} + B \paren {y_i - y'_j} }
      | c = Triangle Inequality
}}
{{eqn | o = \ge
      | r = \size {\paren {x_i - x'_j} \paren {y_i + y'_j} + \paren {y_i - y'_j} \paren {x_i + x'_j} }
      | c = 
}}
{{eqn | r = \size {x_i y_i - x'_j y_i + x_i y'_j - x'_j y'_j + x_i y_i + x'_j y_i - x_i y'_j - x'_j y'_j}
      | c = 
}}
{{eqn | r = \size {2 x_i y_i - 2 x'_j y'_j}
      | c = 
}}
{{eqn | r = \size {x_i y_i - x'_j y'_j}
      | c = 
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Real Multiplication
tm7vlng9ns6eh8pbbe3b2b8m4su3e2i
Theorem: Real Multiplication is Closed

The operation of multiplication on the set of real numbers $\R$ is closed:
:$\forall x, y \in \R: x \times y \in \R$

Proof:
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
From the definition of real multiplication, $x \times y$ is defined as:
:$\eqclass {\sequence {x_n} } {} \times \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n \times y_n} } {}$
We have that:
:$\forall i \in \N: x_i \in \Q, y_i \in \Q$
therefore $x_i \times y_i \in \Q$.
So it follows that:
:$\eqclass {\sequence {x_n \times y_n} } {} \in \R$
{{qed}}
Theorem: Real Addition is Associative

The operation of addition on the set of real numbers $\R$ is associative:
:$\forall x, y, z \in \R: x + \paren {y + z} = \paren {x + y} + z$

Proof:
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}, z = \eqclass {\sequence {z_n} } {}$, where $\eqclass {\sequence {x_n} } {}$, $\eqclass {\sequence {y_n} } {}$ and $\eqclass {\sequence {z_n} } {}$ are such equivalence classes.
From the definition of real addition, $x + y$ is defined as $\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n + y_n} } {}$.
Thus we have:
{{begin-eqn}}
{{eqn | l = x + \paren {y + z}
      | r = \eqclass {\sequence {x_n} } {} + \paren {\eqclass {\sequence {y_n} } {} + \eqclass {\sequence {z_n} } {} }
      | c = 
}}
{{eqn | r = \eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n + z_n} } {}
      | c = 
}}
{{eqn | r = \eqclass {\sequence {x_n + \paren {y_n + z_n} } } {}
      | c = 
}}
{{eqn | r = \eqclass {\sequence {\paren {x_n + y_n} + z_n} } {}
      | c = Rational Addition is Associative
}}
{{eqn | r = \eqclass {\sequence {x_n + y_n} } {} + \eqclass {\sequence {z_n} } {}
      | c = 
}}
{{eqn | r = \paren {\eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {} } + \eqclass {\sequence {z_n} } {}
      | c = 
}}
{{eqn | r = \paren {x + y} + z
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Real Multiplication is Associative

The operation of multiplication on the set of real numbers $\R$ is associative:
:$\forall x, y, z \in \R: x \times \paren {y \times z} = \paren {x \times y} \times z$

Proof:
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}, z = \eqclass {\sequence {z_n} } {}$, where $\eqclass {\sequence {x_n} } {}$, $\eqclass {\sequence {y_n} } {}$ and $\eqclass {\sequence {z_n} } {}$ are such equivalence classes.
From the definition of real multiplication, $x \times y$ is defined as $\eqclass {\sequence {x_n} } {} \times \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n \times y_n} } {}$.
Thus we have:
{{begin-eqn}}
{{eqn | l = x \times \paren {y \times z}
      | r = \eqclass {\sequence {x_n} } {} \times \paren {\eqclass {\sequence {y_n} } {} \times \eqclass {\sequence {z_n} } {} }
      | c = 
}}
{{eqn | r = \eqclass {\sequence {x_n} } {} \times \eqclass {\sequence {y_n \times z_n} } {}
      | c = 
}}
{{eqn | r = \eqclass {\sequence {x_n \times \paren {y_n \times z_n} } } {}
      | c = 
}}
{{eqn | r = \eqclass {\sequence {\paren {x_n \times y_n} \times z_n} } {}
      | c = Rational Multiplication is Associative
}}
{{eqn | r = \eqclass {\sequence {x_n \times y_n} } {} \times \eqclass {\sequence {z_n} } {}
      | c = 
}}
{{eqn | r = \paren {\eqclass {\sequence {x_n} } {} \times \eqclass {\sequence {y_n} } {} } \times \eqclass {\sequence {z_n} } {}
      | c = 
}}
{{eqn | r = \paren {x \times y} \times z
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Real Addition is Commutative

The operation of addition on the set of real numbers $\R$ is commutative:
:$\forall x, y \in \R: x + y = y + x$

Proof:
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
Thus:
{{begin-eqn}}
{{eqn | l = x + y
      | r = \eqclass {\sequence {x_n} } {} + \eqclass {\sequence {y_n} } {}
      | c = {{Defof|Real Number|subdef = Cauchy Sequences}}
}}
{{eqn | r = \eqclass {\sequence {x_n + y_n} } {}
      | c = {{Defof|Real Addition}}
}}
{{eqn | r = \eqclass {\sequence {y_n + x_n} } {}
      | c = Rational Addition is Commutative
}}
{{eqn | r = \eqclass {\sequence {y_n} } {} + \eqclass {\sequence {x_n} } {}
      | c = {{Defof|Real Addition}}
}}
{{eqn | r = y + x
      | c = {{Defof|Real Number|subdef = Cauchy Sequences}}
}}
{{end-eqn}}
{{qed}}
Theorem: Real Multiplication is Commutative

The operation of multiplication on the set of real numbers $\R$ is commutative:
:$\forall x, y \in \R: x \times y = y \times x$

Proof:
From the definition, the real numbers are the set of all equivalence classes $\eqclass {\sequence {x_n} } {}$ of Cauchy sequences of rational numbers.
Let $x = \eqclass {\sequence {x_n} } {}, y = \eqclass {\sequence {y_n} } {}$, where $\eqclass {\sequence {x_n} } {}$ and $\eqclass {\sequence {y_n} } {}$ are such equivalence classes.
From the definition of real multiplication, $x \times y$ is defined as $\eqclass {\sequence {x_n} } {} \times \eqclass {\sequence {y_n} } {} = \eqclass {\sequence {x_n \times y_n} } {}$.
Thus we have:
{{begin-eqn}}
{{eqn | l = x \times y
      | r = \eqclass {\sequence {x_n} } {} \times \eqclass {\sequence {y_n} } {}
      | c = 
}}
{{eqn | r = \eqclass {\sequence {x_n \times y_n} } {}
      | c = 
}}
{{eqn | r = \eqclass {\sequence {y_n \times n_n} } {}
      | c = Rational Multiplication is Commutative
}}
{{eqn | r = \eqclass {\sequence {y_n} } {} \times \eqclass {\sequence {x_n} } {}
      | c = 
}}
{{eqn | r = y \times x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Equidecomposable Nested Sets

Let $A, B, C$ be sets such that $A$ and $C$ are equidecomposable and $A \subseteq B \subseteq C$.
Then $B$ and $C$ are equidecomposable.

Proof:
Let $\set {X_k}_{k \mathop = 1}^n$ be a decomposition of $A$ and $C$, so that there are isometries $\set {\phi_k}_{k \mathop = 1}^n$ and $\set {\psi_k}_{k \mathop = 1}^n$ such that:
$\ds A = \bigcup_{k \mathop = 1}^n \map {\phi_k} {X_k}$
$\ds C = \bigcup_{k \mathop = 1}^n \map {\psi_k} {X_k}$
Let $Y_k = \map {\psi_k^{-1} } {B \cap \map {\psi_k} {X_k} }$.
Then:
:$\ds \bigcup_{k \mathop = 1}^n \map {\psi_k} {Y_k} = B \cap \bigcup_{k \mathop = 1}^n \map {\psi_k} {X_k} = B \cap C = B$
Let $Z_k = \map {\phi^{-1} } {A \cap \map {\phi_k} {X_k} }$.
Then:
:$\ds \bigcup_{k \mathop = 1}^n \map {\phi_k} {Z_k} = A \cap \bigcup_{k \mathop = 1}^n \map {\phi_k} {X_k} = A \cap C = A$
{{finish}}
Category:Equidecomposable Sets
Category:Topology
ax83z1k3d25iigzf6d1x1igldvml00g
Theorem: Rational Numbers form Metric Space

Let $\Q$ be the set of all rational numbers.
Let $d: \Q \times \Q \to \R$ be defined as:
:$\map d {x_1, x_2} = \size {x_1 - x_2}$
where $\size x$ is the absolute value of $x$.
Then $d$ is a metric on $\Q$ and so $\struct {\Q, d}$ is a metric space.

Proof:
From the definition of absolute value:
:$\size {x_1 - x_2} = \sqrt {\paren {x_1 - x_2}^2}$
This is the same as the Euclidean metric.
This is shown in Euclidean Metric on Real Vector Space is Metric to be a metric.
From Rational Numbers form Vector Space, it follows that the set of all rational numbers is a $1$-dimensional Euclidean space.
{{qed}}
Theorem: Rational Numbers form Vector Space

Let $\Q$ be the set of rational numbers.
Then the $\Q$-module $\Q^n$ is a vector space.
It follows directly, by setting $n = 1$, that the $\Q$-module $\Q$ itself can also be regarded as a vector space.

Proof:
From the definition, a vector space is a unitary module whose scalar ring is a field.
From Rational Numbers form Field, we have that $\Q$ is a field.
So the $\Q$-module $\Q^n$ fits the description.
{{qed}}
Category:Linear Algebra
Category:Rational Numbers
n74hux90kj7e88gtvcb4nzycbi1nbre
Theorem: Five Color Theorem

A planar graph $G$ can be assigned a proper vertex $k$-coloring such that $k \le 5$.

Proof:
The proof proceeds by the Principle of Mathematical Induction on the number of vertices.
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$G_n$ can be assigned a proper vertex $k$-coloring such that $k \le 5$.
Theorem: Limit of (Cosine (X) - 1) over X at Zero

:$\ds \lim_{x \mathop \to 0} \frac {\cos x - 1} x = 0$

Proof:
This proof works directly from the definition of the cosine function:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}
      | c = {{Defof|Real Cosine Function}}
}}
{{eqn | r = \paren {-1}^0 \cdot \frac {x^{2 \cdot 0} } {\paren {2 \cdot 0}!} + \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}
}}
{{eqn | r = 1 + \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}
      | c = {{Defof|Factorial|Zero Factorial}} and {{Defof|Power (Algebra)|Zeroth Power}}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0} \frac {\cos x - 1} x
      | r = \lim_{x \mathop \to 0} \frac {1 + \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!} - 1} x
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac {\sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!} } x
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac {\sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n - 1} } {\paren {2 n - 1}!} } 1
      | c = Power Series is Differentiable on Interval of Convergence and L'Hôpital's Rule
}}
{{eqn | r = \lim_{x \mathop \to 0} \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n - 1} } {\paren {2 n - 1}!}
}}
{{end-eqn}}
Now let:
:$\map {f_n} x = \paren {-1}^n \dfrac {x^{2 n - 1} } {\paren {2 n - 1}!}$
Then for every $n \in \N_{> 0}$, and for all $x \in \closedint {\dfrac 1 2} {\dfrac 1 2}$:
{{begin-eqn}}
{{eqn | l = \map {f_n} x
      | o = \le
      | r = \size {\paren {-1}^n \frac {x^{2 n - 1} } {\paren {2 n - 1}!} }
      | rr= \; = \frac { {\size x}^{2 n - 1} } {\paren {2 n - 1}!}
      | c = Absolute Value Function is Completely Multiplicative
}}
{{eqn | o = \le
      | r = \frac 1 {2^{2 n - 1} \paren {2 n - 1}!}
      | c = Power Function is Strictly Increasing over Positive Reals
}}
{{eqn | o = \le
      | r = \frac 1 {2^{2 n - 1} }
      | c = because the factorial is strictly increasing
}}
{{eqn | o = \le
      | r = \frac 1 {2^n}
      | c = because $n \ge 1 \iff 2 n - 1 \ge n$
}}
{{end-eqn}}
But from Sum of Infinite Geometric Sequence:
:$\ds \sum_{n \mathop = 1}^\infty \frac 1 {2^n} = 2 < \infty$
By the Weierstrass M-Test, $\ds \sum_{n \mathop = 1}^\infty \map {f_n} x$ converges uniformly to some function $f$ on $\closedint {\dfrac 1 2} {\dfrac 1 2}$.
But from Real Polynomial Function is Continuous, and the Uniform Limit Theorem $f$ is continuous on $\closedint {\dfrac 1 2} {\dfrac 1 2}$.
So:
:$\ds \lim_{x \mathop \to 0} \map f x = \map f 0 = \sum_{n \mathop = 1}^\infty \paren {-1} \frac {0^{2 n - 1} } {\paren {2 n - 1}!} = 0$
{{qed}}
Theorem: Limit of (Cosine (X) - 1) over X at Zero

:$\ds \lim_{x \mathop \to 0} \frac {\cos x - 1} x = 0$

Proof:
This proof assumes the truth of the Derivative of Cosine Function:
From Cosine of Zero is One:
:$\cos 0 = 1$
From Derivative of Cosine Function:
:$\map {D_x} {\cos x} = -\sin x$
and by Derivative of Constant:
:$\map {D_x} {-1} = 0$
So by Sum Rule for Derivatives:
:$\map {D_x} {\cos x - 1} = -\sin x$
By Sine of Zero is Zero:
:$\sin 0 = 0$
From Derivative of Identity Function:
:$\map {D_x} x = 1$
Thus L'Hôpital's Rule applies and so:
:$\ds \lim_{x \mathop \to 0} \frac {\cos x - 1} x = \lim_{x \mathop \to 0} \frac {-\sin x} 1 = \frac {-0} 1 = 0$
{{qed}}
Theorem: Limit of (Cosine (X) - 1) over X at Zero

:$\ds \lim_{x \mathop \to 0} \frac {\cos x - 1} x = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0} \frac {\cos x - 1} x
      | r = \lim_{x \mathop \to 0} \frac {\paren {\cos x - 1} \paren {\cos x + 1} } {x \paren {\cos x + 1} }
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac {\cos^2 x - 1} {x \paren {\cos x + 1} }
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac {-\sin^2 x} {x \paren {\cos x + 1} }
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | r = \paren {\lim_{x \mathop \to 0} \frac {\sin x} x} \paren {\lim_{x \mathop \to 0} \frac {-\sin x} {\cos x + 1} }
      | c = Product Rule for Limits of Real Functions
}}
{{eqn | r = 1 \times \paren {\lim_{x \mathop \to 0} \frac{-\sin x} {\cos x + 1} }
      | c = Limit of $\dfrac {\sin x} x$ at Zero
}}
{{eqn | r = \frac {\ds \lim_{x \mathop \to 0} \paren {-\sin x} } {\ds \lim_{x \mathop \to 0} \paren {\cos x + 1} }
      | c = Quotient Rule for Limits of Real Functions
}}
{{eqn | r = \frac 0 2
}}
{{eqn | r = 0
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of (Cosine (X) - 1) over X at Zero

:$\ds \lim_{x \mathop \to 0} \frac {\cos x - 1} x = 0$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {\cos x - 1} x 
      | r = \frac {\cos x - \cos 0} x
      | c = Cosine of Zero is One
}}
{{eqn | o = \to
      | r = \valueat {\dfrac \d {\d x} \cos x} {x \mathop = 0}
      | c = as $x \to 0$, from {{Defof|Derivative of Real Function at Point}}
}}
{{eqn | r = \bigvalueat {\sin x} {x \mathop = 0}
      | c = Derivative of Cosine Function
}}
{{eqn | r = 0
      | c = Sine of Zero is Zero
}}
{{end-eqn}}
{{qed}}