avewright/proofwiki-math huggingface dataset:
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
:400px
Let $ABC$ be a right triangle whose angle $BAC$ is a right angle.
Construct squares $BDEC$ on $BC$, $ABFG$ on $AB$ and $ACKH$ on $AC$.
Construct $AL$ parallel to $BD$ (or $CE$).
Since $\angle BAC$ and $\angle BAG$ are both right angles, from Two Angles making Two Right Angles make Straight Line it follows that $CA$ is in a straight line with $AG$.
For the same reason $BA$ is in a straight line with $AH$.
We have that $\angle DBC = \angle FBA$, because both are right angles.
We add $\angle ABC$ to each one to make $\angle FBC$ and $\angle DBA$.
By common notion 2, $\angle FBC = \angle DBA$.
By Triangle Side-Angle-Side Congruence, $\triangle ABD = \triangle FBC$.
We have that the parallelogram $BDLM$ is on the same base $BD$ and between the same parallels $BD$ and $AL$ as the triangle $\triangle ABD$.
So, by Parallelogram on Same Base as Triangle has Twice its Area, the parallelogram $BDLM$ is twice the area of $\triangle ABD$.
Similarly, we have that the parallelogram $ABFG$ (which happens also to be a square) is on the same base $FB$ and between the same parallels $FB$ and $GC$ as the triangle $\triangle FBC$.
So, by Parallelogram on Same Base as Triangle has Twice its Area, the parallelogram $ABFG$ is twice the area of $\triangle FBC$.
So $BDLM = 2 \triangle ABD = 2 \triangle FBC = ABFG$.
By the same construction, we have that $CELM = 2 \triangle ACE = 2 \triangle KBC = ACKH$.
But $BDLM + CELM$ is the whole of the square $BDEC$.
Therefore the area of the square $BDEC$ is equal to the combined area of the squares $ABFG$ and $ACKH$.
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
Consider the triangle shown below.
:350px
We can take $4$ copies of this triangle and form them into a square using isometries, specifically rotations and translations.
This new figure is shown below.
:500px
This figure is clearly a square, since all the angles are right angles, and the lines connecting the corners are easily seen to be straight.
Now to calculate the area of this figure.
On the one hand, we can add up the area of the component parts of the square.
Specifically, we can add up the $4$ triangles and the inner square.
Thus we calculate the area of the large square to be:
:$4 \paren {\dfrac 1 2 a b} + c^2 = 2 a b + c^2$
On the other hand, we can similarly calculate the area of the large square to be:
:$\paren {a + b}^2 = a^2 + 2 a b + b^2$
Now these two expressions have to be equal, since they both represent the area of the square.
Thus:
:$a^2 + 2 a b + b^2 = 2 a b + c^2 \iff a^2 + b^2 = c^2$
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
:400px
We have:
:$\dfrac b c = \dfrac d b$
and:
:$\dfrac a c = \dfrac e a$
using the fact that all the triangles involved are similar.
That is:
:$b^2 = c d$
:$a^2 = c e$
Adding, we now get:
:$a^2 + b^2 = c d + c e = c \paren {d + e} = c^2$
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
:300px
The area of the big square is $c^2$.
It is also equal to $4 \dfrac {a b} 2 + \paren {a - b}^2$.
So:
{{begin-eqn}}
{{eqn | l = c^2
      | r = 4 \frac {a b} 2 + \paren {a - b}^2
      | c = 
}}
{{eqn | r = 2 a b + a^2 - 2 a b + b^2
      | c = 
}}
{{eqn | r = a^2 + b^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
:800px
Dissect the square on the left (which has area $c^2$) as shown.
Rearrange the pieces to make the two squares on the right, with areas $a^2$ and $b^2$.
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
:700px
The two squares both have the same area, that is, $\paren {a + b}^2$.
The one on the left has four triangles of area $\dfrac {a b} 2$ and a square of area $c^2$.
The one on the right has four triangles of area $\dfrac {a b} 2$ and two squares: one of area $a^2$ and one of area $b^2$.
Take away the triangles from both of the big squares and you are left with $c^2 = a^2 + b^2$.
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
:500px
We have that $CH = BS = AB = AJ$.
Hence the result follows directly from Pythagoras's Theorem for Parallelograms.
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
:500px
Let $\triangle ABC$ be a right triangle and $h_c$ the altitude from $c$.
We have:
:$\angle CAB \cong \angle DCB$
:$\angle ABC \cong \angle ACD$
Then we have:
:$\triangle ADC \sim \triangle ACB \sim \triangle CDB$
Use the fact that if $\triangle XYZ \sim \triangle X'Y'Z'$ then by Ratio of Areas of Similar Triangles:
:$\dfrac {\paren {XYZ} } {\paren {X' Y' Z'} } = \dfrac {XY^2} {X'Y'^2}$
where $\paren {XYZ}$ denotes the area of $\triangle XYZ$.
This gives us:
:$\dfrac {\paren {ADC} } {\paren {ACB} } = \dfrac {AC^2} {AB^2}$
and
:$\dfrac {\paren {CDB} } {\paren {ACB} } = \dfrac {BC^2} {AB^2}$
Taking the sum of these two equalities we obtain:
:$\dfrac {\paren {ADC} } {\paren {ACB} } + \dfrac {\paren {CDB} } {\paren {ACB} } = \dfrac {BC^2} {AB^2} + \dfrac {AC^2} {AB^2}$
Thus:
:$\dfrac {\overbrace {\paren {ADC} + \paren {CDB} }^{\paren {ACB} } } {\paren {ACB} } = \dfrac {BC^2 + AC^2} {AB^2}$
Thus:
:$AB^2 = BC^2 + AC^2$
as desired.
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
Let $\Box ABCD$ be an arbitrary rectangle with opposing sides $AB = CD$ and $AD = BC$.
300px
Let $O$ be the point where the diameters of $\Box ABCD$ meet.
By Diagonals of Rectangle are Equal:
:$AC = BD$
By Diameters of Parallelogram Bisect each other:
:$OA = OB = OC = OD$
Let a circle be constructed on center $O$ with radius $OA$.
Then $\Box ABCD$ is inscribed in the circle.
This also follows from the converse to Thales' Theorem.
{{refactor|2 separate proofs here}}
By Ptolemy's Theorem:
:$AD \cdot BC + AB \cdot CD = AC \cdot BD$
But $AD = BC$ and $AB = CD$ and $AC = BD$ so:
:$AD \cdot AD + AB \cdot AB = AC \cdot AC$
Hence the result follows.
{{qed}}
Theorem: Pythagoras's Theorem

Let $\triangle ABC$ be a right triangle with $c$ as the hypotenuse.
Then:
:$a^2 + b^2 = c^2$

Proof:
thumb
From Perpendicular in Right-Angled Triangle makes two Similar Triangles, we have that $\triangle c'c_{upper}b$ is similar to $\triangle c_{lower}c'a$ is similar to $\triangle abc$
{{improve|probably better to refer to triangles by their vertices than their sides, makes it easier for several reasons}}
Looking at the hypotenuse and altitudes of the three similar triangles, we can write the following products and ratios relationships, then multiply them:
Twice the area of the lower right triangle plus twice the area of the upper right triangle equals twice the area of the entire right triangle.
{{begin-eqn}}
{{eqn | l = a a' + b b'
      | r = c c'
      | c = Area of Triangle in Terms of Side and Altitude
}}
{{eqn | l = \dfrac {a} {a′} 
      | m = \dfrac {b} {b′}
      | ro = =
      | r = \dfrac {c} {c′}
      | c = ratios
}}
{{eqn | ll = \leadsto
      | l = a^2 + b^2
      | r = c^2
      | c = 
}}
{{end-eqn}}
Note, dividing them gives us: $ {a′}^2   +   {b′}^2   =   {c′}^2$
Theorem: Euclid's Theorem

For any finite set of prime numbers, there exists a prime number not in that set.
{{:Euclid:Proposition/IX/20}}

Proof:
Let $\mathbb P$ be a finite set of prime numbers.
Consider the number:
:$\ds n_p = \paren {\prod_{p \mathop \in \mathbb P} p} + 1$
Take any $p_j \in \mathbb P$.
We have that:
:$\ds p_j \divides \prod_{p \mathop \in \mathbb P} p$
Hence:
:$\ds \exists q \in \Z: \prod_{p \mathop \in \mathbb P} p = q p_j$
So:
{{begin-eqn}}
{{eqn | l = n_p
      | r = q p_j + 1
      | c = Division Theorem
}}
{{eqn | ll= \leadsto
      | l = n_p
      | o = \perp
      | r = p_j
      | c = {{Defof|Coprime Integers}}
}}
{{end-eqn}}
So $p_j \nmid n_p$.
There are two possibilities:
:$(1): \quad n_p$ is prime, which is not in $\mathbb P$. 
:$(2): \quad n_p$ is composite.
But from Positive Integer Greater than 1 has Prime Divisor, it must be divisible by ''some'' prime.
That means it is divisible by a prime which is not in $\mathbb P$.
So, in either case, there exists at least one prime which is not in the original set $\mathbb P$ we created.
{{qed}}
{{Euclid Note|20|IX}}
Theorem: Euclid's Theorem

For any finite set of prime numbers, there exists a prime number not in that set.
{{:Euclid:Proposition/IX/20}}

Proof:
Assume that there are only finitely many prime numbers, and that there is a grand total of $n$ primes.
Then it is possible to define the set of all primes:
: $\mathbb P = \set {p_1, p_2, \ldots, p_n}$
From Euclid's Theorem, however, we can always create a prime which is not in $\mathbb P$.
So we can never create a finite list of all the primes, because we can guarantee to construct a number which has prime factors that are not in this list.
Thus, there are infinitely many prime numbers.
{{qed}}
Theorem: Euclid's Theorem

For any finite set of prime numbers, there exists a prime number not in that set.
{{:Euclid:Proposition/IX/20}}

Proof:
Assume that there are only finitely many prime numbers.
Let $p$ be the largest of these.
Then from Existence of Prime between Prime and Factorial there exists a prime number $q$ such that:
:$p < q \le p! + 1$
So there cannot be such a $p$.
{{qed}}
Theorem: Euclid's Theorem

For any finite set of prime numbers, there exists a prime number not in that set.
{{:Euclid:Proposition/IX/20}}

Proof:
Let $\mathbb P$ be the set of all prime numbers.
{{AimForCont}} there exists a largest prime number $p_m$.
Then:
:$\mathbb P \subseteq \closedint 1 {p_m} = \set {1, 2, \ldots, p_m}$
and so $\mathbb P$ is a finite set.
By Euclid's Theorem, there exists a prime number $q$ such that $q \notin \mathbb P$.
But that means $q \notin \closedint 1 {p_m}$.
That is, $q > p_m$.
So $p_m$ is not the largest prime number after all.
Hence the result, by Proof by Contradiction.
{{qed}}
Theorem: Euclid's Theorem

For any finite set of prime numbers, there exists a prime number not in that set.
{{:Euclid:Proposition/IX/20}}

Proof:
{{AimForCont}} there exists a largest prime number $p$.
Let $b = p! + 1$.
Let $q$ be a prime number that divides $b$.
Since $p$ is the largest prime number, $q \le p$.
However, no positive integer $d \le p$ is a divisor of $b$.
Hence $q \not \le p$.
Hence the result, by Proof by Contradiction.
{{qed}}
Theorem: Square Root of Prime is Irrational

The square root of a prime number is irrational.

Proof:
Let $p$ be prime.
{{AimForCont}} that $\sqrt p$ is rational.
Then there exist natural numbers $m$ and $n$ such that:
{{begin-eqn}}
{{eqn | l = \sqrt p
      | r = \frac m n
      | c = 
}}
{{eqn | ll= \leadsto
      | l = p
      | r = \frac {m^2} {n^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n^2 p
      | r = m^2
      | c = 
}}
{{end-eqn}}
Any prime in the prime factorizations of $n^2$ and $m^2$ must occur an even number of times because they are squares.
Thus, $p$ must occur in the prime factorization of $n^2 p$ an odd number of times.
Therefore, $p$ occurs as a factor of $m^2$ an odd number of times, which is a contradiction.
So $\sqrt p$ must be irrational.
{{qed}}
Theorem: Square Root of Prime is Irrational

The square root of a prime number is irrational.

Proof:
Let $p \in \Z$ be a prime number.
Consider the polynomial:
:$\map P x = x^2 - p$
over the ring of polynomials $\Q \sqbrk X$ over the rational numbers.
From Difference of Two Squares:
:$x^2 - p = \paren {x + \sqrt p} \paren {x - \sqrt p}$
Because $p$ is prime, $\sqrt p$ is not an integer.
From Polynomial which is Irreducible over Integers is Irreducible over Rationals it follows that $\paren {x + \sqrt p}$ and $\paren {x - \sqrt p}$ do not have rational coefficients.
That is:
:$\sqrt p$ is not rational.
Hence the result.
{{qed}}
Theorem: Derivative of Exponential Function

Let $\exp$ be the exponential function.
Then:
:$\map {\dfrac \d {\d x} } {\exp x} = \exp x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\exp x}
      | r = \lim_{h \mathop \to 0} \frac {\map \exp {x + h} - \exp x} h
      | c = {{Defof|Derivative}}
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\exp x \cdot \exp h - \exp x} h
      | c = Exponential of Sum
}}
{{eqn | r = \lim_{h \mathop \to 0} \frac {\exp x \paren {\exp h - 1} } h
}}
{{eqn | r = \exp x \paren {\lim_{h \mathop \to 0} \frac {\exp h - 1} h}
      | c = Multiple Rule for Limits of Real Functions, as $\exp x$ is constant
}}
{{eqn | r = \exp x
      | c = Derivative of Exponential at Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Exponential Function

Let $\exp$ be the exponential function.
Then:
:$\map {\dfrac \d {\d x} } {\exp x} = \exp x$

Proof:
We use the fact that the exponential function is the inverse of the natural logarithm function:
:$y = e^x \iff x = \ln y$
{{begin-eqn}}
{{eqn |  l = \dfrac {\d x} {\d y}
      |  r = \dfrac 1 y
      |  c = Derivative of Natural Logarithm Function
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d y} {\d x}
      | r = \dfrac 1 {1 / y}
      | c = Derivative of Inverse Function
}}
{{eqn | r = y
}}
{{eqn | r = e^x
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Exponential Function

Let $\exp$ be the exponential function.
Then:
:$\map {\dfrac \d {\d x} } {\exp x} = \exp x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\ln e^x}
      | r = \map {\frac \d {\d x} } x
      | c = Exponential of Natural Logarithm
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {e^x} \map {\frac \d {\d x} } {e^x}
      | r = 1
      | c = Chain Rule for Derivatives, Derivative of Natural Logarithm Function, Derivative of Identity Function
}}
{{eqn | ll= \leadsto
      | l = \map {\frac \d {\d x} } {e^x}
      | r = e^x
      | c = multiply both sides by $e^x$
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Exponential Function

Let $\exp$ be the exponential function.
Then:
:$\map {\dfrac \d {\d x} } {\exp x} = \exp x$

Proof:
This proof assumes the power series definition of $\exp$.
That is, let:
:$\ds \exp x = \sum_{k \mathop = 0}^\infty \frac {x^k} {k!}$
From Series of Power over Factorial Converges, the interval of convergence of $\exp$ is the entirety of $\R$.
So we may apply Differentiation of Real Power Series to $\exp$ for all $x \in \R$.
Thus we have:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \exp x
      | r = \frac \d {\d x} \sum_{k \mathop = 0}^\infty \frac {x^k} {k!}
}}
{{eqn | r = \sum_{k \mathop = 1}^\infty \frac k {k!} x^{k - 1}
      | c = Differentiation of Real Power Series, with $n = 1$
}}
{{eqn | r = \sum_{k \mathop = 1}^\infty \frac {x^{k - 1} } {\paren {k - 1}!}
}}
{{eqn | r = \sum_{k \mathop = 0}^\infty \frac {x^k} {k!}
}}
{{eqn | r = \exp x
}}
{{end-eqn}}
Hence the result.
{{qed}}
Theorem: Derivative of Exponential Function

Let $\exp$ be the exponential function.
Then:
:$\map {\dfrac \d {\d x} } {\exp x} = \exp x$

Proof:
This proof assumes the limit definition of $\exp$.
So let:
:$\forall n \in \N: \forall x \in \R: \map {f_n} x = \paren {1 + \dfrac x n}^n$
Let $x_0 \in \R$.
Consider $I := \closedint {x_0 - 1} {x_0 + 1}$.
Let:
:$N = \ceiling {\max \set {\size {x_0 - 1}, \size {x_0 + 1} } }$
where $\ceiling {\, \cdot \,}$ denotes the ceiling function.
From Closed Real Interval is Compact in Metric Space, $I$ is compact.
From Chain Rule for Derivatives:
:$\dfrac \d {\d x} \map {f_n} x = \dfrac n {n + x} \map {f_n} x$
=== Lemma ===
{{:Derivative of Exponential Function/Proof 5/Lemma}}{{qed|lemma}}
From the lemma:
:$\forall x \in I: \sequence {\dfrac \d {\d x} \map {f_{n + N} } x}$ is increasing
Hence, from Dini's Theorem, $\sequence {\dfrac \d {\d x} f_{n + N} }$ is uniformly convergent on $I$.
Therefore, for $x \in I$:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \exp x
      | r = \frac \d {\d x} \lim_{n \mathop \to \infty} \map {f_n} x
}}
{{eqn | r = \frac \d {\d x} \lim_{n \mathop \to \infty} \map {f_{n + N} } x
      | c = Tail of Convergent Sequence
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac \d {\d x} \map {f_{n + N} } x
      | c = Derivative of Uniformly Convergent Sequence of Differentiable Functions
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac n {n + x} \map {f_n} x
      | c = from above
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map {f_n} x
      | c = Combination Theorem for Sequences
}}
{{eqn | r = \exp x
}}
{{end-eqn}}
In particular:
:$\dfrac \d {\d x} \exp x_0 = \exp x_0$
{{qed}}
Theorem: Derivative of Sine Function

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

Proof:
From the definition of the sine function, we have:
:$\ds \sin x = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}$
From Radius of Convergence of Power Series over Factorial, this series converges for all $x$.
From Power Series is Differentiable on Interval of Convergence:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\sin x}
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n + 1} } {\paren {2 n + 1}!}
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {x^{2 n} } {\paren {2 n}!}
      | c = 
}}
{{end-eqn}}
The result follows from the definition of the cosine function.
{{qed}}
Theorem: Derivative of Sine Function

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

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

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

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

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

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

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

Proof:
{{begin-eqn}}
{{eqn | l = \map \arcsin x
      | r = \int_0^x \frac {\d x} {\sqrt {1 - x^2} }
      | c = Arcsine as Integral
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\map \d {\map \arcsin y} } {\d y}
      | r = \dfrac {\map \d {\ds \int_0^y \dfrac 1 {\sqrt {1 - y^2} } \rd y} } {\d y}
}}
{{eqn | r = \dfrac 1 {\sqrt {1 - y^2} }
      | c = {{Corollary|Fundamental Theorem of Calculus/First Part|disp = Fundamental Theorem of Calculus: First Part}}
}}
{{end-eqn}}
Note that we get the same answer as Derivative of Arcsine Function.
By definition of real $\arcsin$ function, $\arcsin$ is bijective on its domain $\closedint {-1} 1$.
Thus its inverse is itself a mapping.
From Inverse of Inverse of Bijection, its inverse is the $\sin$ function.
{{begin-eqn}}
{{eqn | l = \dfrac {\map \d {\sin \theta} } {\d \theta}
      | r = 1 / \dfrac 1 {\sqrt {1 - \sin^2 \theta} }
      | c = Derivative of Inverse Function
}}
{{eqn | r = \pm \sqrt {1 - \sin^2 \theta}
      | c = Positive in Quadrant $\text I$ and Quadrant $\text {IV}$, Negative in Quadrant $\text {II}$ and Quadrant $\text {III}$
}}
{{eqn | l = \dfrac {\map \d {\sin \theta} } {\d \theta}
      | r = \cos \theta
}}
{{end-eqn}}
{{qed}}
Theorem: 0.999...=1

:$0.999 \ldots = 1$

Proof:
By Sum of Infinite Geometric Sequence:
:$0.999 \ldots = \dfrac a {1 - r}$
where $a = \dfrac 9 {10}$ and $r = \dfrac 1 {10}$.
Since our ratio is less than $1$, then we know that $\ds \sum_{n \mathop = 0}^\infty \frac 9 {10} \paren {\frac 1 {10} }^n$ must converge to:
:$\dfrac a {1 - r} = \dfrac {\frac 9 {10} } {1 - \frac 1 {10} } = \dfrac {\frac 9 {10} } {\frac 9 {10} } = 1$
{{qed}}
Theorem: 0.999...=1

:$0.999 \ldots = 1$

Proof:
{{begin-eqn}}
{{eqn | l = 0.333 \ldots
      | r = 1 / 3
}}
{{eqn | ll= \leadsto
      | l = 3 \paren {0.333 \ldots}
      | r = 3 \paren {1 / 3}
}}
{{eqn | ll= \leadsto
      | l = 0.999 \ldots
      | r = 3 / 3
}}
{{eqn | r = 1
}}
{{end-eqn}}
{{qed}}
Theorem: 0.999...=1

:$0.999 \ldots = 1$

Proof:
Let  $c = 0.999 \ldots$
Then:
{{begin-eqn}}
{{eqn | l = c
      | r = 0.999 \ldots
}}
{{eqn | ll= \leadsto
      | l = 10 c 
      | r = \paren {9.999 \ldots}
      | c = multiplying $c$ by $10$
}}
{{eqn | ll= \leadsto
      | l = 10 c - c
      | r = \paren {9.999 \ldots} - \paren {0.999 \ldots}
      | c = subtracting $c$ from each side
}}
{{eqn | ll= \leadsto
      | l = 9 c
      | r = 9
}}
{{eqn | ll= \leadsto
      | l = c
      | r = 1
}}
{{end-eqn}}
It follows that:
:$0.999 \ldots = 1$
{{qed}}
Theorem: 0.999...=1

:$0.999 \ldots = 1$

Proof:
We begin with the knowledge that:
{{begin-eqn}}
{{eqn | l = \frac 9 9
      | r = \frac 1 1 = 1
}}
{{end-eqn}}
Now we divide $9$ by $9$ using the standard process of long division, only instead of stating that $90$ divided by $9$ is $10$, we say that it is "$9$ remainder $9$," yielding the following result:
<pre>
     0.9999...
    -----------
   9)9.0000...
     8.1
     ---
       90
       81
       --
        90
        81
        --
         9...
</pre>
Thus, we are compelled to believe that:
:$0.999\ldots = \dfrac 9 9 = 1$
{{qed}}
Theorem: 0.999...=1

:$0.999 \ldots = 1$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | l = 0 . \underset n {\underbrace {999 \cdots 9} }
      | r = 1 - 0.1^n
      | c = 
}}
{{eqn | l = 0.999 \cdots
      | r = \eqclass {\sequence {0.9, \, 0.99, \, 0.999, \, \cdots} } {}
      | c = {{Defof|Real Numbers}}
}}
{{eqn | r = \eqclass {\sequence {1 - 0.1^1, \, 1 - 0.1^2, \, 1 - 0.1^3, \, \cdots} } {}
      | c = from $(1)$
}}
{{eqn | r = \eqclass {\sequence {1, \, 1, \, 1, \, \cdots} } {} - \eqclass {\sequence {0.1^1, \, 0.1^2, \, 0.1^3, \, \cdots} } {}
      | c = 
}}
{{eqn | r = 1 - 0
      | c = Sequence of Powers of Number less than One, {{Defof|Real Numbers}}
}}
{{eqn | r = 1
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Sequence of Cubes

:$\ds \sum_{i \mathop = 1}^n i^3 = \paren {\sum_{i \mathop = 1}^n i}^2 = \frac {n^2 \paren {n + 1}^2} 4$

Proof:
{{begin-eqn}}
{{eqn | l = \sum_{i \mathop = 1}^n i^3
      | r =  \frac {n^2 \paren {n + 1}^2} 4
      | c = Sum of Sequence of Cubes
}}
{{eqn | r = \paren {\frac {n \paren {n + 1} } 2}^2
      | c = 
}}
{{eqn | r = {T_n}^2
      | c = Closed Form for Triangular Numbers
}}
{{end-eqn}}
{{qed}}