avewright/proofwiki-math huggingface dataset:
Theorem: Derivative of Exponential at Zero

Let $\exp x$ be the exponential of $x$ for real $x$.
Then:
:$\ds \lim_{x \mathop \to 0} \frac {\exp x - 1} x = 1$

Proof:
For all $x \in \R$:
:$\exp 0 - 1 = 0$ from Exponential of Zero
:$\map {D_x} {\exp x - 1} = \exp x$ from Sum Rule for Derivatives
:$D_x x = 1$ from Derivative of Identity Function.
Its prerequisites having been verified, {{Corollary|L'Hôpital's Rule|1}} yields immediately:
:$\ds \lim_{x \mathop \to 0} \frac {\exp x - 1} x = \lim_{x \mathop \to 0} \frac {\exp x} 1 = \exp 0 = 1$
{{qed}}
Theorem: Derivative of Exponential at Zero

Let $\exp x$ be the exponential of $x$ for real $x$.
Then:
:$\ds \lim_{x \mathop \to 0} \frac {\exp x - 1} x = 1$

Proof:
Note that this proof does not presuppose Derivative of Exponential Function.
We use the definition of the exponential as a limit of a sequence:
{{begin-eqn}}
{{eqn | l = \frac {\exp h - 1} h
      | r = \frac {\lim_{n \mathop \to \infty} \paren {1 + \dfrac h n}^n - 1} h
      | c = {{Defof|Exponential Function/Real|subdef = Limit of Sequence|Exponential Function}}
}}
{{eqn | r = \frac {\ds \lim_{n \mathop \to \infty} \sum_{k \mathop = 0}^n {n \choose k} \paren {\frac h n}^k - 1} h
      | c = Binomial Theorem
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac {\ds \sum_{k \mathop = 0}^n {n \choose k} \paren {\frac h n}^k - 1} h
      | c = as $h$ is constant
}}
{{eqn | r = \lim_{n \mathop \to \infty} \paren { {n \choose 0} 1 - 1 + {n \choose 1} \paren {\frac h n} \frac 1 h + \sum_{k \mathop = 2}^n {n \choose k} \paren {\frac h n}^k \frac 1 h}
}}
{{eqn | r = \lim_{n \mathop \to \infty}1 + \lim_{n \mathop \to \infty} \sum_{k \mathop = 2}^n {n \choose k} \frac {h^{k - 1} }{n^k}
      | c = Powers of Group Elements
}}
{{eqn | r = 1 + h \lim_{n \mathop \to \infty} \sum_{k \mathop = 2}^n {n \choose k} \frac {h^{k - 2} } {n^k}
      | c = Powers of Group Elements
}}
{{end-eqn}}
The right summand converges to zero as $h \to 0$, and so:
:$\ds \lim_{h \mathop \to 0} \frac {\exp h - 1} h = 1$
{{qed}}
Theorem: Derivative of Exponential at Zero

Let $\exp x$ be the exponential of $x$ for real $x$.
Then:
:$\ds \lim_{x \mathop \to 0} \frac {\exp x - 1} x = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \frac {e^x - 1} x
      | r = \frac {e^x - e^0} x
      | c = Exponential of Zero
}}
{{eqn | o = \to
      | r = \valueat {\dfrac \d {\d x} e^x} {x \mathop = 0} {}
      | c = {{Defof|Derivative of Real Function at Point}}, as $x \to 0$
}}
{{eqn | r = \valueat {e^x} {x \mathop = 0} {}
      | c = Derivative of Exponential Function
}}
{{eqn | r = 1
      | c = Exponential of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Exponential at Zero

Let $\exp x$ be the exponential of $x$ for real $x$.
Then:
:$\ds \lim_{x \mathop \to 0} \frac {\exp x - 1} x = 1$

Proof:
As we consider $x \to 0$, we may assume that $0 < \size x \le 1$.
Then:
{{begin-eqn}}
{{eqn | l = \size {\frac {e^x - 1} x - 1}
      | r = \size {\frac {e^x - 1 - x} x}
}}
{{eqn | r = \size {\frac {\sum_{n \mathop = 0}^\infty \frac {x^n} {n!} - 1 - x} x }
      | c = {{Defof|Exponential Function|subdef = Real/Power Series Expansion}}
}}
{{eqn | r = \size {x \sum_{n \mathop = 2}^\infty \frac {x^{n-2} } {n !} }
}}
{{eqn | o = \le
      | r = \size x \sum_{n \mathop = 2}^\infty \frac 1 {n !}
      | c = as $\size x \le 1$
}}
{{eqn | o = \le
      | r = \size x \sum_{n \mathop = 0}^\infty \frac 1 {n !}
}}
{{eqn | r = \size x e
      | c = {{Defof|Euler's Number as Limit of Series}}
}}
{{eqn | o = \to
      | r = 0
      | c = as $x \to 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Classification of Groups of Order up to 15

Up to isomorphism, every group of order $\order G \le 15$ is one of the below:
{| class="sortable wikitable"
|- bgcolor="#ececec"
! Order !! Abelian !! Non-Abelian
|-
|1 || $\Z_1$ || 
|-
|2 || $\Z_2$ ||
|-
|3 || $\Z_3$ ||
|-
|4 || $\Z_4, \Z_2 \oplus \Z_2$ || 
|-
|5 || $\Z_5$ ||
|-
|6 || $\Z_6$ || $D_3 \cong S_3$
|- 
|7 || $\Z_7$ ||
|-
|8 || $\Z_8, \Z_4 \oplus \Z_2, \Z_2 \oplus \Z_2 \oplus \Z_2$ || $D_4, \Dic 2$
|-
|9 || $\Z_9, \Z_3 \oplus \Z_3$ || 
|-
|10 || $\Z_{10}$ || $D_5$
|-
|11 || $\Z_{11}$ ||
|-
|12 || $\Z_{12}, \Z_6 \oplus \Z_2$ || $D_6, A_4, \Dic 3$
|-
|13 || $\Z_{13}$ ||
|-
|14 || $\Z_{14}$ || $D_7$
|-
|15 || $\Z_{15}$ || 
|}
where:
: $D_n$ is the dihedral group of order $2 n$
: $S_n$ is the $n$th symmetric group
: $A_n$ is the alternating group on $n$ points
: $\Dic n$ is the dicyclic group of order $4 n$.

Proof:
The Abelian cases are the direct result of the Fundamental Theorem of Finite Abelian Groups.
The non-Abelian cases follow from seven separate theorems:
:$(1): \quad$ Trivial Group is Cyclic Group - determines theorem for order $1$
:$(2): \quad$ Prime Group is Cyclic - determines theorem for orders $2$, $3$, $5$, $7$, $11$, and $13$
:$(3): \quad$ Group of Order Prime Squared is Abelian - determines theorem for orders $4$ and $9$
:$(4): \quad$ Group of Order p q is Cyclic - determines theorem for order $15$
:$(5): \quad$ Groups of Order Twice a Prime - determines theorem for orders $6$, $10$, $14$
:$(6): \quad$ Groups of Order 8 - determines theorem for order $8$
:$(7): \quad$ Groups of Order 12 - determines theorem for order $12$
{{qed}}
Theorem: Existence of Euler-Mascheroni Constant

The real sequence:
:$\ds \sequence {\sum_{k \mathop = 1}^n \frac 1 k - \ln n}$
converges to a limit.
This limit is known as the Euler-Mascheroni constant.

Proof:
Let $f: \R \setminus \set 0 \to \R: \map f x = \dfrac 1 x$.
Clearly $f$ is continuous and positive on $\hointr 1 {+\infty}$.
From Reciprocal Sequence is Strictly Decreasing, $f$ is decreasing on $\hointr 1 {+\infty}$.
Therefore the conditions of the Cauchy Integral Test hold.
Thus the sequence $\sequence {\Delta_n}$ defined as:
:$\ds \Delta_n = \sum_{k \mathop = 1}^n \map f k - \int_1^n \map f x \rd x$
is decreasing and bounded below by zero.
But from the definition of the natural logarithm:
:$\ds \int_1^n \frac {\d x} x = \ln n$
Hence the result.
{{qed}}
Theorem: Existence of Euler-Mascheroni Constant

The real sequence:
:$\ds \sequence {\sum_{k \mathop = 1}^n \frac 1 k - \ln n}$
converges to a limit.
This limit is known as the Euler-Mascheroni constant.

Proof:
For $n \in \N_{>0}$ let:
:$\ds \gamma_n := \sum_{k \mathop = 1}^n \frac 1 k - \ln n$
Then:
{{begin-eqn}}
{{eqn | l = \gamma_n
      | r =  1 + \int_1^n \dfrac {\floor u} {u^2} \rd u - \ln n
      | c = Integral Expression of Harmonic Number
}}
{{eqn | r =  1 + \int_1^n \dfrac {\floor u} {u^2} \rd u - \int _1 ^n \dfrac 1 u \rd u
      | c = {{Defof|Real Natural Logarithm}}
}}
{{eqn | n = 1
      | r = 1 - \int_1^n \dfrac {u - \floor u} {u^2} \rd u
      | c = Linear Combination of Definite Integrals
}}
{{eqn | o = \ge
      | r = 1 - \int_1^n \dfrac 1 {u^2} \rd u
      | c = Relative Sizes of Definite Integrals as $0 \le u - \floor u < 1$
}}
{{eqn | r = \dfrac 1 n
}}
{{eqn | o = \ge
      | r = 0
}}
{{end-eqn}}
On the other hand:
{{begin-eqn}}
{{eqn | l = \gamma_n - \gamma_{n + 1}
      | r = \paren {1 - \int_1^n \dfrac {u - \floor u} {u^2} \rd u} - \paren {1 - \int_1^{n + 1} \dfrac {u - \floor u} {u^2} \rd u}
      | c = by $\paren 1$
}}
{{eqn | r = \int_n^{n + 1} \dfrac {u - \floor u} {u^2} \rd u
      | c = Sum of Integrals on Adjacent Intervals for Integrable Functions
}}
{{eqn | o = \ge
      | r = 0
      | c = as $u - \floor u \ge 0$
}}
{{end-eqn}}
Thus by monotone convergence theorem, the sequence $\sequence {\gamma_n}$ converges to a limit in $\R_{\ge 0}$.
{{qed}}
Theorem: Group of Order p q is Cyclic

Let $p, q$ be primes such that $p < q$ and $p$ does not divide $q - 1$.
Let $G$ be a group of order $p q$.
Then $G$ is cyclic.

Proof:
By Sylow $p$-Subgroup is Unique iff Normal, $H$ and $K$ are normal subgroups of $G$.
Let $H = \gen x$ and $K = \gen y$.
To show $G$ is cyclic, it is sufficient to show that $x$ and $y$ commute, because then:
:$\order {x y} = \order x \order y = p q$
where $\order x$ denotes the order of $x$ in $G$.
{{explain|Why does it follow that $\order {x y} {{=}} \order x \order y {{=}} p q$?}}
Since $H$ and $K$ are normal:
:$x y x^{-1} y^{-1} = \paren {x y x^{-1} } y^{-1} \in K y^{-1} = K$
and 
:$x y x^{-1} y^{-1} = x \paren {y x ^{-1} y^{-1} } \in x H = H$
Now suppose $a \in H \cap K$.
Then:
{{begin-eqn}}
{{eqn | l = \order a
      | o = \divides
      | r = p
      | c = 
}}
{{eqn | lo= \land
      | l = \order a
      | o = \divides
      | r = q
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \order a
      | r = 1
      | c = 
}}
{{eqn | ll= \leadsto
      | l = a
      | r = e
      | c = 
}}
{{end-eqn}}
where $e$ is the identity of $G$.
Thus:
:$x y x^{-1}y^{-1} \in K \cap H = e$
Hence $x y = y x$ and the result follows.
{{Qed}}
Theorem: Group of Order p q is Cyclic

Let $p, q$ be primes such that $p < q$ and $p$ does not divide $q - 1$.
Let $G$ be a group of order $p q$.
Then $G$ is cyclic.

Proof:
Let the Sylow $p$-subgroup of $G$ be denoted $P$.
Let the Sylow $q$-subgroup of $G$ be denoted $Q$.
We have that:
:$P \cap Q = \set e$
where $e$ is the identity element of $G$.
Hence in $P \cup Q$ there are $q + p - 1$ elements.
As $p q \ge 2 q > q + p - 1$, there exists a non- identity element in $G$ that is not in $H$ or $K$.
Its order must be $p q$.
Hence, by definition, $G$ is cyclic.
{{qed}}
Theorem: Derivative of Logarithm at One

Let $\ln x$ be the natural logarithm of $x$ for real $x$ where $x > 0$.
Then:
:$\ds \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x = 1$

Proof:
L'Hôpital's Rule gives:
:$\ds \lim_{x \mathop \to c} \frac {\map f x} {\map g x} = \lim_{x \mathop \to c} \frac {\map {f'} x} {\map {g'} x}$
(provided the appropriate conditions are fulfilled).
Here we have:
{{begin-eqn}}
{{eqn | l = \map \ln {1 + 0}
      | r = 0
}}
{{eqn | l = \map {D_x} {\map \ln {1 + x} }
      | r = \dfrac 1 {1 + x}
      | c = Chain Rule for Derivatives
}}
{{eqn | l = \map {D_x} x
      | r = 1
      | c = Derivative of Identity Function
}}
{{end-eqn}}
Thus:
:$\ds \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x = \lim_{x \mathop \to 0} \frac {\paren {1 + x}^{-1} } 1 = \frac 1 {1 + 0} = 1$
{{qed}}
Theorem: Derivative of Logarithm at One

Let $\ln x$ be the natural logarithm of $x$ for real $x$ where $x > 0$.
Then:
:$\ds \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x
      | r = \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} - \ln 1} x
      | c = subtract $\ln 1 = 0$ from the numerator, from Logarithm of 1 is 0
}}
{{eqn | r = \intlimits {\dfrac {\d} {\d x} \ln x} {x \mathop = 1} {}
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{eqn | r = \frac 1 1
      | c = Derivative of Natural Logarithm Function
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Logarithm at One

Let $\ln x$ be the natural logarithm of $x$ for real $x$ where $x > 0$.
Then:
:$\ds \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x = 1$

Proof:
Note that this proof does not presuppose Derivative of Natural Logarithm Function.
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0} \frac {\map \ln {1 + x} } x
      | r = \lim_{n \mathop \to \infty} \frac {\map \ln {1 + \frac 1 n} } {\frac 1 n}
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} n \, \map \ln {1 + \frac 1 n}
      | c = 
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map \ln {\paren {1 + \frac 1 n}^n}
      | c = 
}}
{{eqn | r = \ln e
      | c = {{Defof|Euler's Number as Limit of Sequence}}
}}
{{eqn | r = 1
      | c = Natural Logarithm of e is 1
}}
{{end-eqn}}
{{qed}}
Theorem: Dicyclic Group is Non-Abelian Group

The dicyclic group $\Dic n$ is a non-abelian group on two generators.

Proof:
The dicyclic group $\Dic n$ is defined as follows:
{{:Definition:Dicyclic Group}}
First it is to be demonstrated that $\Dic n$ is a group.
First we deduce the following:
$(1): \quad b^4 = e$:
{{begin-eqn}}
{{eqn | l = b^2
      | r = a^n
      | c = {{Defof|Dicyclic Group}}
}}
{{eqn | ll= \leadsto
      | l = \paren {b^2}^2
      | r = \paren {a^n}^2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b^4
      | r = a^{2 n}
      | c = 
}}
{{eqn | r = e
      | c = {{Defof|Dicyclic Group}}
}}
{{end-eqn}}
$(2): \quad b^2 a^k = a^{k + n} = a^k b^2$:
{{begin-eqn}}
{{eqn | l = b^2 a^k
      | r = b^2 a^{2 n} a^k
      | c = {{Defof|Dicyclic Group}}: $a^{2 n} = e$
}}
{{eqn | r = b^2 \paren {b^2 a^n} a^k
      | c = {{Defof|Dicyclic Group}}: $b^2 = a^n$
}}
{{eqn | r = b^4 a^{n + k}
      | c = 
}}
{{eqn | r = a^{k + n}
      | c = {{Defof|Dicyclic Group}}: $b^4 = e$
}}
{{eqn | r = a^k a^n b^4
      | c = {{Defof|Dicyclic Group}}: $b^4 = e$
}}
{{eqn | r = a^k \paren {a^n b^2} b^2
      | c = 
}}
{{eqn | r = a^k \paren {a^n a^n} b^2
      | c = {{Defof|Dicyclic Group}}: $b^2 = a^n$
}}
{{eqn | r = a^k \paren {a^{2 n} } b^2
      | c = 
}}
{{eqn | r = a^k b^2
      | c = {{Defof|Dicyclic Group}}: $a^{2 n} = e$
}}
{{end-eqn}}
$(3): \quad j = \pm 1 \implies b^j a^k = a^{-k} b^j$
{{begin-eqn}}
{{eqn | n = 4
      | l = a^k b^{-1}
      | r = a^{k - n} a^n b^{-1}
      | c = 
}}
{{eqn | r = a^{k - n} b^2 b^{-1}
      | c = 
}}
{{eqn | r = a^{k - n} b
      | c = 
}}
{{end-eqn}}
Thus, every element of $\Dic n$ can be uniquely written as $a^k b^j$, where $0 \le k < 2 n$ and $j \in \set {0, 1}$. 
The definition of the group product gives:
:$a^k a^m = a^{k + m}$
:$a^k a^m b = a^{k + m} b$
:$a^k b a^m = a^{k - m} b$
:$a^k b a^m x = a^{k - m + n}$
Taking the group axioms in turn:
{{finish|In my naivety with the below, I am at the moment unaware of the concept of a group presentation being a concept defined from a free group, with the assumption that being a quotient group, a lot of the properties (e.g. associativity, identity) are inherited from the Group Presentation itself. But I need to understand this. So far the only help I've been given is that this area is all "trivial" and "obvious".}}
Theorem: Existence of Interval of Convergence of Power Series

Let $\xi \in \R$ be a real number.
Let $\ds \map S x = \sum_{n \mathop = 0}^\infty a_n \paren {x - \xi}^n$ be a power series about $\xi$.
Then the interval of convergence of $\map S x$ is a real interval whose midpoint is $\xi$.

Proof:
Suppose $\map S x$ converges when $x = y$.
We need to show that it converges for all $x$ which satisfy $\size {x - \xi} < \size {y - \xi}$.
So, let $\map S x$ converge when $x = y$.
Then from Terms in Convergent Series Converge to Zero:
:$a_n \paren {y - \xi}^n \to 0$ as $n \to \infty$
Hence, from Convergent Sequence is Bounded:
:$\sequence {a_n \paren {y - \xi}^n}$ is bounded
Thus:
:$\exists H \in \R: \forall n \in \N_{>0}: \size {a_n \paren {y - \xi}^n} \le H$
Now suppose $\size {x - \xi} < \size {y - \xi}$.
Then:
:$\rho = \dfrac {\size {x - \xi} } {\size {y - \xi} } < 1$
(Note that if $\size {x - \xi} < \size {y - \xi}$ then $\size {y - \xi} > 0$ and the above fraction always exists.)
Hence:
:$\forall n \in \N_{>0} \size {a_n \paren {x - \xi}^n} = \rho^n \size {a_n \paren {y - \xi}^n} \le H \rho^n$
By Sequence of Powers of Number less than One:
:$\ds \sum_{n \mathop = 1}^\infty \rho^n$ converges
Thus $\ds \sum_{n \mathop = 0}^\infty a_n \paren {x - \xi}^n$ converges by the Comparison Test.
The result follows.
{{qed}}
Theorem: Power Series Expansion for Exponential Function

Let $\exp x$ be the exponential function.
Then:
{{begin-eqn}}
{{eqn | q = \forall x \in \R
      | l = \exp x
      | r = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}
      | c = 
}}
{{eqn | r = 1 + x + \frac {x^2} {2!} + \frac {x^3} {3!} + \cdots
      | c = 
}}
{{end-eqn}}

Proof:
From Higher Derivatives of Exponential Function, we have:
:$\forall n \in \N: \map {f^{\paren n} } {\exp x} = \exp x$
Since $\exp 0 = 1$, the Taylor series expansion for $\exp x$ about $0$ is given by:
:$\ds \exp x = \sum_{n \mathop = 0}^\infty \frac {x^n} {n!}$
From Radius of Convergence of Power Series over Factorial, we know that this power series expansion converges for all $x \in \R$.
From Taylor's Theorem, we know that
:$\ds \exp x = 1 + \frac x {1!} + \frac {x^2} {2!} + \cdots + \frac {x^{n - 1} } {\paren {n - 1}!} + \frac {x^n} {n!} \map \exp \eta$
where $0 \le \eta \le x$.
Hence:
{{begin-eqn}}
{{eqn | l = \size {\exp x - \paren {1 + \frac x {1!} + \frac {x^2} {2!} + \cdots + \frac {x^{n - 1} } {\paren {n - 1}!} } }
      | r = \size {\frac {x^n} {n!} \map \exp \eta}
      | c = 
}}
{{eqn | o = \le
      | r = \frac {\size {x^n} } {n!} \map \exp {\size x}
      | c = Exponential is Strictly Increasing
}}
{{eqn | o = \to
      | r = 0
      | rr= \text { as } n \to \infty
      | c = Series of Power over Factorial Converges
}}
{{end-eqn}}
So the partial sums of the power series converge to $\exp x$.
The result follows.
{{qed}}
Theorem: Derivative of Cosine Function

:$\map {\dfrac \d {\d x} } {\cos x} = -\sin x$

Proof:
From the definition of the cosine function, we have:
:$\ds \cos x = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}$
Then:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\cos x}
      | r = \sum_{n \mathop = 1}^\infty \paren {-1}^n 2 n \frac {x^{2 n - 1} } {\paren {2 n}!}
      | c = Power Series is Differentiable on Interval of Convergence
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n - 1} } {\paren {2 n - 1}!}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^{n + 1} \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = changing summation index
}}
{{eqn | r = -\sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
}}
{{end-eqn}}
The result follows from the definition of the sine function.
{{qed}}
Theorem: Derivative of Cosine Function

:$\map {\dfrac \d {\d x} } {\cos x} = -\sin x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\cos x}
      | r = \lim_{h \mathop \to 0} \frac {\map \cos {x + h} - \cos x} h
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\cos x \cos h - \sin x \sin h - \cos x} h
      | c = Cosine of Sum
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\cos x \cos h - \cos x} h + \lim_{h \mathop \to 0} \frac {-\sin x \sin h} h
      | c = Sum Rule for Limits of Real Functions
}}
{{eqn | r = \cos x \lim_{h \mathop \to 0} \frac {\cos h - 1} h - \sin x \lim_{h \mathop \to 0} \frac {\sin h} h
      | c = Multiple Rule for Limits of Real Functions
}}
{{eqn | r = \cos x \times 0 - \sin x \times 1
      | c = Limit of $\dfrac {\cos x - 1} x$ at Zero and Limit of $\dfrac {\sin x} x$ at Zero
}}
{{eqn | r = -\sin x
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Cosine Function

:$\map {\dfrac \d {\d x} } {\cos x} = -\sin x$

Proof:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \cos x
      | r = \frac \d {\d x} \map \sin {\frac \pi 2 - x}
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = -\map \cos {\frac \pi 2 - x}
      | c = Derivative of Sine Function and Chain Rule for Derivatives 
}}
{{eqn | r = -\sin x
      | c = Cosine of Complement equals Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Cosine Function

:$\map {\dfrac \d {\d x} } {\cos x} = -\sin x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\cos x}
      | r = \lim_{h \mathop \to 0} \frac {\map \cos {x + h} - \cos x} h
      | c = {{Defof|Derivative of Real Function at Point}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\map \cos {\paren {x + \frac h 2} + \frac h 2} - \map \cos {\paren {x + \frac h 2} - \frac h 2} } h
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {-2 \map \sin {x + \frac h 2} \map \sin {\frac h 2} } h
      | c = Werner Formula for Sine by Sine
}}
{{eqn | r = -\lim_{h \mathop \to 0} \map \sin {x + \frac h 2} \lim_{h \mathop \to 0} \frac {\map \sin {\frac h 2} } {\frac h 2}
      | c = Multiple Rule for Limits of Real Functions and Product Rule for Limits of Real Functions
}}
{{eqn | r = -\sin x \times 1
      | c = Real Sine Function is Continuous and Limit of $\dfrac {\sin x} x$ at Zero
}}
{{eqn | r = -\sin x
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Cosine Function

:$\map {\dfrac \d {\d x} } {\cos x} = -\sin x$

Proof:
{{begin-eqn}}
{{eqn | l = 1
      | r = \cos^2 x + \sin^2 x
      | c = Sum of Squares of Sine and Cosine
}}
{{eqn | ll= \leadsto
      | l = \map {D_x} 1
      | r = \map {D_x} {\cos^2 x + \sin^2 x}
      | c = differentiating both sides
}}
{{eqn | ll= \leadsto
      | l = 0
      | r = 2 \map {D_x} {\cos x} \cos x  + 2 \sin x \cos x
      | c = Product Rule for Derivatives or Chain Rule for Derivatives and Derivative of Sine Function 
}}
{{eqn | ll= \leadsto
      | l = \map {D_x} {\cos x}
      | r = -\sin x
      | c = provided $\cos x \ne 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of Sinc Function at Zero

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

Proof:
{{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 = {{Defof|Real Sine Function}}
}}
{{eqn | r = \paren {-1}^0 \frac {x^{2 \cdot 0 + 1} } {\paren {2 \cdot 0 + 1}!} + \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
}}
{{eqn | r = x + \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
}}
{{end-eqn}}
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0} \frac {\sin x} x
      | r = \lim_{x \mathop \to 0} \frac {x + \sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!} } x
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac x x + \lim_{x \mathop \to 0} \frac{\sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!} } x
}}
{{eqn | r = 1 + \lim_{x \mathop \to 0} \frac {\sum_{n \mathop = 1}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!} } 1
      | c = Power Series is Differentiable on Interval of Convergence and L'Hôpital's Rule
}}
{{eqn | r = 1 + \lim_{x \mathop \to 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 {0^{2 n} } {\paren {2 n}!}
      | c = Real Polynomial Function is Continuous
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of Sinc Function at Zero

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

Proof:
From Sine of Zero is Zero:
:$\sin 0 = 0$
From Derivative of Sine Function:
:$\map {D_x} {\sin x} = \cos x$
Then by Cosine of Zero is One:
:$\cos 0 = 1$
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 {\sin x} x = \lim_{x \mathop \to 0} \frac {\map {D_x} {\sin x} } {\map {D_x} x} = \lim_{x \mathop \to 0} \frac {\cos x} 1 = \frac 1 1 = 1$
{{qed}}
Theorem: Sum of Squares of Sine and Cosine

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

Proof:
{{begin-eqn}}
{{eqn | l = 1
      | r = \cos 0
      | c = Cosine of Zero is One
}}
{{eqn | r = \map \cos {x - x}
      | c = 
}}
{{eqn | r = \cos x \map \cos {-x} - \sin x \map \sin {-x}
      | c = Cosine of Sum
}}
{{eqn | r = \cos x \cos x - \paren {-\sin x \sin x}
      | c = Cosine Function is Even and Sine Function is Odd
}}
{{eqn | r = \cos^2 x + \sin^2 x
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Squares of Sine and Cosine

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

Proof:
From the trigonometric definitions of sine and cosine:
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \frac{\text{opposite} } {\text{hypotenuse} }
}}
{{eqn | l = \cos x
      | r = \frac{\text{adjacent} } {\text{hypotenuse} }
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \sin^2 x + \cos^2 x
      | r = \frac{\text{opposite}^2 + \text{adjacent}^2} {\text{hypotenuse}^2}
      | c = squaring both sides and adding
}}
{{eqn | r = \frac{\text{hypotenuse}^2} {\text{hypotenuse}^2}
      | c = Pythagoras's Theorem
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Squares of Sine and Cosine

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

Proof:
Let $P = \tuple {x, y}$ be a point on the circumference of a unit circle whose center is at the origin of a cartesian plane.
From Sine of Angle in Cartesian Plane and Cosine of Angle in Cartesian Plane:
:$P = \tuple {\cos \theta, \sin \theta}$
The graph of the unit circle is the locus of:
:$x^2 + y^2 = 1$
as given by Equation of Circle.
Substituting $x = \cos \theta$ and $y = \sin \theta$ yields:
:$\cos^2 \theta + \sin^2 \theta = 1$
{{qed}}