avewright/proofwiki-math huggingface dataset:
Theorem: Einstein's Mass-Energy Equation

The energy imparted to a body to cause that body to move causes the body to increase in mass by a value $M$ as given by the equation:
:$E = M c^2$
where $c$ is the speed of light.

Proof:
From Einstein's Law of Motion, we have:
:$\mathbf F = \dfrac {m_0 \mathbf a} {\paren {1 - \dfrac {v^2} {c^2} }^{\tfrac 3 2} }$
where:
:$\mathbf F$ is the force on the body
:$\mathbf a$ is the acceleration induced on the body
:$v$ is the magnitude of the velocity of the body
:$c$ is the speed of light
:$m_0$ is the rest mass of the body.
{{WLOG}}, assume that the body is starting from rest at the origin of a cartesian plane.
Assume the force $\mathbf F$ on the body is in the positive direction along the $x$-axis.
To simplify the work, we consider the acceleration as a scalar quantity and write it $a$.
Thus, from the Chain Rule for Derivatives:
:$a = \dfrac {\d v} {\d t} = \dfrac {\d v} {\d x} \dfrac {\d x} {\d t} = v \dfrac {\d v} {\d x}$
Then from the definition of energy:
:$\ds E = \int_0^x F \rd x$
which leads us to:
{{begin-eqn}}
{{eqn | l = E
      | r = m_0 \int_0^x \frac a {\paren {1 - v^2 / c^2}^{\tfrac 3 2} } \rd x
      | c = 
}}
{{eqn | r = m_0 \int_0^v \frac v {\paren {1 - v^2 / c^2}^{\tfrac 3 2} } \rd v
      | c = substituting $v \rd v = a \rd x$ from above
}}
{{eqn | r = m_0 \int_0^v \frac v {\paren {1 - v^2 / c^2}^{\tfrac 3 2} } \rd v \times \paren {-\frac {c^2} 2} \times \paren {-\frac 2 {c^2} }
      | c = multiplying top and bottom by $-\dfrac {c^2} 2$
}}
{{eqn | r = m_0 \paren {- \frac {c^2} 2} \int_0^v \paren {1 - \frac {v^2} {c^2} }^{-\tfrac 3 2} \paren {- \frac {2 v \rd v} {c^2} }
      | c = 
}}
{{eqn | r = \intlimits {m_0 c^2 \paren {1 - \frac {v^2} {c^2} }^{- \tfrac 1 2} } 0 v
      | c = 
}}
{{eqn | r = m_0 c^2 \paren {\frac 1 {\sqrt {1 - \frac {v^2} {c^2} } } - 1}
      | c = 
}}
{{eqn | r = c^2 \paren {\frac {m_0} {\sqrt {1 - \frac {v^2} {c^2} } } - m_0}
      | c = 
}}
{{eqn | r = c^2 \paren {m - m_0}
      | c = Einstein's Mass-Velocity Equation
}}
{{eqn | r = M c^2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Dimension of Universal Gravitational Constant

The dimension of the universal gravitational constant $G$ is $M^{-1} L^3 T^{-2}$.

Proof:
From Newton's Law of Universal Gravitation:
:$\mathbf F = \dfrac {G m_1 m_2 \mathbf r} {r^3}$
We have that:
: The dimension of force is $M L T^{-2}$
: The dimension of displacement is $L$
: The dimension of mass is $M$.
Let $x$ be the dimension of $G$.
Then we have:
:$M L T^{-2} = x \dfrac {M^2 L}{L^3}$
Hence, after algebra:
:$x = M^{-1} L^3 T^{-2}$
{{qed}}
Category:Universal Gravitational Constant
Category:Dimensional Analysis
lw0fpvrt2u4q1gitfc5a0ismujmfjti
Theorem: Dimension of Spring Force Constant

The dimension of a spring force constant is $\mathsf {M T}^{-2}$.

Proof:
From Hooke's Law, we have:
:$\mathbf F = -k \mathbf x$
where:
:$\mathbf F$ is a force, of dimension $\mathsf {M L T}^{-2}$
:$k$ is the spring force constant
:$\mathbf x$ is a displacement, of dimension $\mathsf L$.
Let the dimension of $k$ be $D$.
Then we have:
:$\mathsf {M L T}^{-2} = D \mathsf L$
from which the result follows immediately:
:$D = \mathsf {M T}^{-2}$
{{qed}}
Category:Dimensional Analysis
qeswg8tbvk3ce0qlt9rlqfjw1er197i
Theorem: Vieta's Formula for Pi

:$\pi = 2 \times \dfrac 2 {\sqrt 2} \times \dfrac 2 {\sqrt {2 + \sqrt 2} } \times \dfrac 2 {\sqrt {2 + \sqrt {2 + \sqrt 2} } } \times \dfrac 2 {\sqrt {2 + \sqrt {2 + \sqrt {2 + \sqrt 2 } } } } \times \cdots$

Proof:
{{begin-eqn}}
{{eqn | l = 1
      | r = \sin \frac \pi 2
      | c = Sine of Half-Integer Multiple of Pi
}}
{{eqn | r = 2 \sin \frac \pi 4 \cos \frac \pi 4
      | c = Double Angle Formula for Sine
}}
{{eqn | r = 2 \paren {2 \sin \frac \pi 8 \cos \frac \pi 8} \cos \frac \pi 4
      | c = Double Angle Formula for Sine
}}
{{eqn | r = 2 \paren {2 \paren {2 \sin \frac \pi {16} \cos \frac \pi {16} } \cos \frac \pi 8} \cos \frac \pi 4
      | c = Double Angle Formula for Sine
}}
{{eqn | r = \cdots
      | c = 
}}
{{eqn | r = 2^{n - 1} \sin \frac \pi {2^n} \cos \frac \pi {2^n} \cos \frac \pi {2^{n - 1} } \cdots \cos \frac \pi 8 \cos \frac \pi 4
      | c = 
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | l = \frac 1 {2^{n - 1} \sin \frac \pi {2^n} }
      | r = \cos \frac \pi 4 \cos \frac \pi 8 \cos \frac \pi {16} \cdots \cos \frac \pi {2^{n - 1} } \cos \frac \pi {2^n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac 2 \pi \times \frac {\pi / 2^n} {\map \sin {\pi / 2^n} }
      | r = \cos \frac \pi 4 \cos \frac \pi 8 \cos \frac \pi {16} \cdots \cos \frac \pi {2^{n - 1} } \cos \frac \pi {2^n}
      | c = multiplying top and bottom by $\pi$ 
}}
{{eqn | ll= \leadsto
      | l = \pi \times \frac {\map \sin {\pi / 2^n} } {\pi / 2^n}
      | r = 2 \times \frac 1 {\cos \frac \pi 4 \cos \frac \pi 8 \cos \frac \pi {16} \cdots \cos \frac \pi {2^{n - 1} } \cos \frac \pi {2^n} }
      | c = 
}}
{{end-eqn}}
Then we have from the Half Angle Formula for Cosine that:
{{begin-eqn}}
{{eqn | l = \cos \frac \pi {2^{k} }
      | r = \sqrt {\frac {1 + \map \cos {\pi / 2^{k - 1} } } 2 } 
      | c = 
}}
{{eqn | r = \sqrt {\frac {2 + 2 \map \cos {\pi / 2^{k - 1} } } {2 \times 2} } 
      | c = multiplying top and bottom by $2$ 
}}
{{eqn | r = \frac {\sqrt {2 + 2 \map \cos {\pi / 2^{k - 1} } } } 2
      | c = 
}}
{{eqn | r = \frac {\sqrt {2 + \sqrt {2 + 2 \map \cos {\pi / 2^{k - 2} } } } } 2
      | c = 
}}
{{eqn | r = \frac {\sqrt {2 + \sqrt {2 + \sqrt {2 + 2 \map \cos {\pi / 2^{k - 3} } } } } } 2
      | c = 
}}
{{end-eqn}}
So we can replace all the instances of $\cos \dfrac \pi 4$, $\cos \dfrac \pi 8$, etc. with their expansions in square roots of $2$.
Finally, we note that from Limit of $\dfrac {\sin x} x$ at Zero we have:
:$\ds \lim_{\theta \mathop \to 0} \frac {\sin \theta} \theta = 1$
As $n \to \infty$, then, we have that $\dfrac \pi {2^n} \to 0$, and so:
:$\ds \lim_{n \mathop \to \infty} \frac {\map \sin {\pi / 2^n} } {\pi / 2^n} = 1$
The result follows after some algebra.
{{qed}}
Theorem: Leibniz's Formula for Pi

:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
First we note that:
:$(1): \quad \dfrac 1 {1 + t^2} = 1 - t^2 + t^4 - t^6 + \cdots + t^{4 n} - \dfrac {t^{4 n + 2} } {1 + t^2}$
which is demonstrated here.
Now consider the real number $x \in \R: 0 \le x \le 1$.
We can integrate expression $(1)$ {{WRT|Integration}} $t$ from $0$ to $x$:
:$(2): \quad \ds \int_0^x \frac {\d t} {1 + t^2} = x - \frac {x^3} 3 + \frac {x^5} 5 - \frac {x^7} 7 + \cdots + \frac {x^{4 n + 1} } {4 n + 1} - \map {R_n} x$
where:
:$\ds \map {R_n} x = \int_0^x \frac {t^{4 n + 2} } {1 + t^2} \rd t$
From Square of Real Number is Non-Negative we have that:
:$t^2 \ge 0$
and so:
:$1 \le 1 + t^2$
From Relative Sizes of Definite Integrals, we have:
:$\ds 0 \le \map {R_n} x \le \int_0^x t^{4 n + 2} \rd t$
that is:
:$0 \le \map {R_n} x \le \dfrac {x^{4n + 3} } {4 n + 3}$
But as $0 \le x \le 1$ it is clear that:
:$\dfrac {x^{4 n + 3} } {4 n + 3} \le \dfrac 1 {4 n + 3}$
So:
:$0 \le \map {R_n} x \le \dfrac 1 {4 n + 3}$
From Basic Null Sequences and the Squeeze Theorem, $\dfrac 1 {4 n + 3} \to 0$ as $n \to \infty$.
This leads us directly to:
:$(3): \quad \ds \int_0^x \frac {\d t} {1 + t^2} = x - \frac {x^3} 3 + \frac {x^5} 5 - \frac {x^7} 7 + \frac {x^9} 9 \cdots$
But from Derivative of Arctangent Function, we also have that:
:$\dfrac \d {\d x} \arctan t = \dfrac 1 {1 + t^2}$
and thence from the Fundamental Theorem of Calculus we have:
:$\ds \arctan x = \int_0^x \frac {\d t} {1 + t^2}$
From $(3)$ it follows immediately that:
:$(4): \quad \arctan x =  x - \dfrac {x^3} 3 + \dfrac {x^5} 5 - \dfrac {x^7} 7 + \dfrac {x^9} 9 \cdots$
Now all we need to do is plug $x = 1$ into $(4)$.
{{qed}}
Theorem: Leibniz's Formula for Pi

:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
:500px
The area $OAT$ is a quarter-circle whose area is $\dfrac \pi 4$ by Area of Circle.
Now consider the area $C$ of the segment $OPQT$, bounded by the arc $OT$ and the chord $OT$.
Consider the area $OPQ$, bounded by the line segments $OP$ and $OQ$ and the arc $PQ$.
As $P$ and $Q$ approach each other, the arc $PQ$ tends towards the straight line segment $\d s = PQ$.
We can therefore consider the area $OPQ$ as a triangle.
We extend the line segment $PQ$ and drop a perpendicular $OR$ to $O$.
Using Area of Triangle in Terms of Side and Altitude, we see that the area $\d C$ of $\triangle OPQ$ is given by:
:$\d C = \triangle OPQ = \dfrac {OR \cdot PQ} 2 = \dfrac {OR \cdot \d s} 2$
We also note from elementary Euclidean geometry that $\triangle ORS$ is similar to the small triangle on $PQ$.
Thus:
:$\dfrac {\d s} {\d x} = \dfrac {OS} {OR} \iff OR \cdot \d s = OS \cdot \d x$
Thus:
:$\d C = \dfrac {OS \cdot \d x} 2 = \dfrac {y \rd x} 2$
where $y = OS$.
We set the horizontal coordinate of $P$ as equal to $x$.
Thus the total area $C$ is equal to the total of all the areas of these small triangles as $x$ increases from $0$ to $1$.
So:
:$\ds C = \int \rd C = \frac 1 2 \int_0^1 y \rd x$
Now we use Integration by Parts to swap $x$ and $y$:
:$\ds C = \intlimits {\frac 1 2 x y} 0 1 - \frac 1 2 \int_0^1 x \rd y = \frac 1 2 - \frac 1 2 \int_0^1 x \rd y$
It can be seen that the limits on this new integral have to be $0$ and $1$ from the geometry of the situation.
Now we note that:
:$y = \tan \dfrac \phi 2$
From {{Corollary|Double Angle Formula for Cosine|2}}:
:$x = 1 - \cos \phi = 2 \sin^2 \dfrac \phi 2$
Thus:
{{begin-eqn}}
{{eqn | l = \tan^2 \frac \phi 2
      | r = \frac {\sin^2 \frac \phi 2}{\cos^2 \frac \phi 2}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \sin^2 \frac \phi 2 \sec^2 \frac \phi 2
      | c = Secant is Reciprocal of Cosine
}}
{{eqn | r = \sin^2 \frac \phi 2 \paren {1 + \tan^2 \frac \phi 2}
      | c = Difference of Squares of Secant and Tangent
}}
{{end-eqn}}
and so:
:$\dfrac x 2 = \dfrac {y^2} {1 + y^2}$
Using Sum of Infinite Geometric Sequence:
:$\dfrac {y^2} {1 + y^2} = y^2 - y^4 + y^6 - y^8 + \cdots$
This gives us:
{{begin-eqn}}
{{eqn | l = C
      | r = \frac 1 2 - \int_0^1 \paren {y^2 - y^4 + y^6 - y^8 + \cdots} \d y
      | c = 
}}
{{eqn | r = \frac 1 2 - \intlimits {\frac {y^3} 3 - \frac {y^5} 5 + \frac {y^7} 7 - \frac {y^9} 9 + \cdots} 0 1
      | c = 
}}
{{eqn | r = \frac 1 2 - \paren {\frac 1 3 - \frac 1 5 + \frac 1 7 - \frac 1 9 + \cdots}
      | c = 
}}
{{eqn | r = \frac 1 2 - \frac 1 3 + \frac 1 5 - \frac 1 7 + \frac 1 9 - \cdots
      | c = 
}}
{{end-eqn}}
Remember, $C$ is the area of the segment $OPQT$.
Now we add to it the area of $\triangle OTA$, which trivially equals $\dfrac 1 2$, to get the area of the quarter circle which we know as equal to $\dfrac \pi 4$.
Putting it all together, this gives us:
:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots$
{{qed}}
Theorem: Leibniz's Formula for Pi

:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
{{begin-eqn}}
{{eqn | l = 2 b \sum_{k \mathop = 1}^\infty \dfrac {\paren {-1}^{k + 1} } {a + b k}
      | r = \map \psi {\dfrac a {2 b} + 1} - \map \psi {\dfrac a {2 b} + \dfrac 1 2}
      | c = {{Corollary|Reciprocal times Derivative of Gamma Function|2}}
}}
{{eqn | ll= \leadsto
      | l = -4 \sum_{k \mathop = 1}^\infty \dfrac {\paren {-1}^k} {1 + 2 k}
      | r = \map \psi {\dfrac 1 4 + 1} - \map \psi {\dfrac 1 4 + \dfrac 1 2}
      | c = $a := 1$ and $b := 2$
}}
{{eqn | ll= \leadsto
      | l = 4 \sum_{k \mathop = 1}^\infty \dfrac {\paren {-1}^k} {1 + 2 k}
      | r = \map \psi {\dfrac 3 4} - \map \psi {\dfrac 5 4}
      | c = multiplying both sides by $-1$
}}
{{eqn | r = \paren {-\gamma - 3 \ln 2 + \dfrac \pi 2} - \paren {-\gamma - 3 \ln 2 - \dfrac \pi 2 + 4}
      | c = Digamma Function of Three Fourths and Digamma Function of Five Fourths
}}
{{eqn | r = \pi - 4
      | c = grouping terms
}}
{{eqn | ll= \leadsto
      | l = 4 + 4 \sum_{k \mathop = 1}^\infty \dfrac {\paren {-1}^k} {1 + 2 k}
      | r = \pi
      | c = adding $4$ to both sides
}}
{{eqn | ll= \leadsto
      | l = 4 \times \paren {1 - \frac 1 3 + \frac 1 5 - \frac 1 7 + \cdots}
      | r = \pi
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 4 \sum_{k \mathop = 0}^\infty \dfrac {\paren {-1}^k} {1 + 2 k}
      | r = \pi
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Leibniz's Formula for Pi

:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
{{Recall|Dirichlet Beta Function}}
{{:Definition:Dirichlet Beta Function}}
From Dirichlet Beta Function at Odd Positive Integers, we obtain:
:$\map \beta {2 n + 1} = \paren {-1}^n \dfrac {E_{2 n} \pi^{2 n + 1} } {4^{n + 1} \paren {2 n}!}$
Therefore, setting $n = 0$ above:
{{begin-eqn}}
{{eqn | l = \map \beta 1
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {\paren {2 n + 1}^1}
      | c = {{Defof|Dirichlet Beta Function}}
}}
{{eqn | r = \paren {-1}^0 \dfrac {E_0 \pi } {4 \times 0!}
      | c = Dirichlet Beta Function at Odd Positive Integers
}}
{{eqn | r = \frac \pi 4
      | c = {{Defof|Euler Numbers}} and Factorial of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Leibniz's Formula for Pi

:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
From {{Corollary|Mittag-Leffler Expansion for Cotangent Function|1}}, we have:
{{begin-eqn}}
{{eqn | l = \frac \pi {2 n} \map \cot {\frac {\pi m} {2 n} }
      | r = \frac 1 m + \sum_{k \mathop = 1}^\infty \paren {\frac 1 {2 k n + m} - \frac 1 {2 k n - m} }
      | c = 
}}
{{eqn | r = \frac 1 m + \paren {\frac 1 {2 n + m} - \frac 1 {2 n - m} } + \paren {\frac 1 {4 n + m} - \frac 1 {4 n - m} } + \paren {\frac 1 {6 n + m} - \frac 1 {6 n - m} } + \cdots
      | c = 
}}
{{end-eqn}}
Let $m := 1$ and $n := 2$.
Then:
{{begin-eqn}}
{{eqn | l = \frac \pi 4 \map \cot {\frac \pi 4}
      | r = 1 + \sum_{k \mathop = 1}^\infty \paren {\frac 1 {4 k + 1} - \frac 1 {4 k - 1} }
      | c = 
}}
{{eqn | r = 1 + \sum_{k \mathop = 1}^\infty \paren {-\frac 1 {4 k - 1} + \frac 1 {4 k + 1} }
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac \pi 4
      | r = 1 + \paren {-\frac 1 3 + \frac 1 5} + \paren {-\frac 1 7 + \frac 1 9} + \paren {-\frac 1 {11} + \frac 1 {13} } + \cdots
      | c = {{cot|45}}
}}
{{end-eqn}}
{{qed}}
Theorem: Leibniz's Formula for Pi

:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
From {{Corollary|Mittag-Leffler Expansion for Tangent Function}}, we have:
{{begin-eqn}}
{{eqn | l = \frac \pi {2 n} \map \tan {\frac {\pi m} {2 n} }
      | r = \sum_{k \mathop = 0}^\infty \paren {\frac 1 {\paren {2 k + 1} n - m} - \frac 1 {\paren {2 k + 1} n + m} }
      | c = 
}}
{{eqn | r = \paren {\frac 1 {n - m} - \frac 1 {n + m} } + \paren {\frac 1 {3 n - m} - \frac 1 {3 n + m} } + \paren {\frac 1 {5 n - m} - \frac 1 {5 n + m} } + \cdots
      | c = 
}}
{{end-eqn}}
Let $m := 1$ and $n := 2$.
Then:
{{begin-eqn}}
{{eqn | l = \frac \pi 4 \map \tan {\frac \pi 4}
      | r = \sum_{k \mathop = 0}^\infty \paren {\frac 1 {4 k + 1} - \frac 1 {4 k + 3} }
      | c = 
}}
{{eqn | ll = \leadsto
      | l = \frac \pi 4
      | r = \paren {\frac 1 1 - \frac 1 3} + \paren {\frac 1 5 - \frac 1 7} + \paren {\frac 1 9 - \frac 1 {11} } + \cdots
      | c = {{tan|45}}
}}
{{end-eqn}}
{{qed}}
Theorem: Leibniz's Formula for Pi

:$\dfrac \pi 4 = 1 - \dfrac 1 3 + \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 - \cdots \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
From Power Series Expansion for Real Arctangent Function, we obtain:
:$\arctan x = x - \dfrac {x^3} 3 + \dfrac {x^5} 5 - \dfrac {x^7} 7 + \dfrac {x^9} 9 - \cdots$
Substituting $x = 1$ gives the required result.
{{qed}}
Theorem: Derivative of Arc Length

Let $C$ be a curve in the cartesian plane described by the equation $y = \map f x$.
Let $s$ be the length along the arc of the curve from some reference point $P$.
Then the derivative of $s$ with respect to $x$ is given by:
:$\dfrac {\d s} {\d x} = \sqrt {1 + \paren {\dfrac {\d y} {\d x} }^2}$

Proof:
Consider a length $\d s$ of $C$, short enough for it to be approximated to a straight line segment:
:250px
By Pythagoras's Theorem, we have:
:$\d s^2 = \d x^2 + \d y^2$
Dividing by $\d x^2$ we have:
{{begin-eqn}}
{{eqn | l = \paren {\frac {\d s} {\d x} }^2
      | r = \paren {\frac {\d x} {\d x} }^2 + \paren {\frac {\d y} {\d x} }^2
      | c = 
}}
{{eqn | r = 1 + \paren {\frac {\d y} {\d x} }^2
      | c = 
}}
{{end-eqn}}
Hence the result, by taking the principal square root of both sides.
{{qed}}
Theorem: Derivative of Arc Length

Let $C$ be a curve in the cartesian plane described by the equation $y = \map f x$.
Let $s$ be the length along the arc of the curve from some reference point $P$.
Then the derivative of $s$ with respect to $x$ is given by:
:$\dfrac {\d s} {\d x} = \sqrt {1 + \paren {\dfrac {\d y} {\d x} }^2}$

Proof:
From Continuously Differentiable Curve has Finite Arc Length, $s$ exists and is given by:
{{begin-eqn}}
{{eqn | l = s
      | r = \int_P^x \sqrt {1 + \paren {\frac {\d y} {\d u} }^2} \rd u
}}
{{eqn | ll= \leadsto
      | l = \frac {\d s} {\d x}
      | r = \frac {\d} {\d x} \int_P^x \sqrt {1 + \paren {\frac {\d y} {\d u} } ^2} \rd u
      | c = differentiating both sides {{WRT|Differentiation}} $x$
}}
{{eqn | r = \sqrt {1 + \paren {\frac {\d y} {\d x} }^2}
      | c = Fundamental Theorem of Calculus: First Part
}}
{{end-eqn}}
{{qed}}
Theorem: Duality Principle for Sets

Any identity in set theory which uses any or all of the operations:
:Set intersection $\cap$
:Set union $\cup$
:Empty set $\O$
:Universal set $\mathbb U$
and none other, remains valid if:
:$\cap$ and $\cup$ are exchanged throughout
:$\O$ and $\mathbb U$ are exchanged throughout.

Proof:
Follows from:
* Algebra of Sets is Huntington Algebra
* Principle of Duality of Huntington Algebras
{{qed}}
Theorem: Rational Addition is Commutative

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

Proof:
Follows directly from the definition of rational numbers as the field of quotients of the integral domain $\struct {\Z, +, \times}$ of integers.
So $\struct {\Q, +, \times}$ is a field, and therefore a fortiori $+$ is commutative on $\Q$.
{{qed}}
Theorem: Rational Addition is Associative

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

Proof:
Follows directly from the definition of rational numbers as the field of quotients of the integral domain $\struct {\Z, +, \times}$ of integers.
So $\struct {\Q, +, \times}$ is a field, and therefore a fortiori $+$ is associative on $\Q$.
{{qed}}
Theorem: Subtraction on Numbers is Anticommutative

The operation of subtraction on the numbers is anticommutative.
That is:
:$a - b = b - a \iff a = b$

Proof:
=== Natural Numbers ===
{{:Subtraction on Numbers is Anticommutative/Natural Numbers}}
Theorem: Integer Addition is Commutative

The operation of addition on the set of integers $\Z$ is commutative:
:$\forall x, y \in \Z: x + y = y + x$

Proof:
From the formal definition of integers, $\eqclass {a, b} {}$ is an equivalence class of ordered pairs of natural numbers.
From Integers under Addition form Abelian Group, the integers under addition form an abelian group, from which commutativity follows {{afortiori}}.
{{qed}}
Theorem: Integer Addition is Commutative

The operation of addition on the set of integers $\Z$ is commutative:
:$\forall x, y \in \Z: x + y = y + x$

Proof:
Let $x = \eqclass {a, b} {}$ and $y = \eqclass {c, d} {}$ for some $x, y \in \Z$.
Then:
{{begin-eqn}}
{{eqn | l = x + y
      | r = \eqclass {a, b} {} + \eqclass {c, d} {}
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{eqn | r = \eqclass {a + c, b + d} {}
      | c = {{Defof|Integer Addition}}
}}
{{eqn | r = \eqclass {c + a, d + b} {}
      | c = Natural Number Addition is Commutative
}}
{{eqn | r = \eqclass {c, d} {} + \eqclass {a, b} {}
      | c = {{Defof|Integer Addition}}
}}
{{eqn | r = y + x
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Integer Addition is Associative

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

Proof:
From the formal definition of integers, $\eqclass {a, b} {}$ is an equivalence class of ordered pairs of natural numbers.
From Integers under Addition form Abelian Group, the integers under addition form a group, from which associativity follows from {{Group-axiom|1}}.
{{qed}}
Theorem: Integer Addition is Associative

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

Proof:
Let $a, b, c, d, e, f \in \N$ such that:
:$x = \eqclass {a, b} {}$, $y = \eqclass {c, d} {}$ and $z = \eqclass {e, f} {}$.
Then:
{{begin-eqn}}
{{eqn | l = x + \paren {y + z}
      | r = \eqclass {a, b} {} + \paren {\eqclass {c, d} {} + \eqclass {e, f} {} }
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{eqn | r = \eqclass {a, b} {} + \eqclass {c + e, d + f} {}
      | c = {{Defof|Integer Addition}}
}}
{{eqn | r = \eqclass {a + \paren {c + e}, b + \paren {d + f} } {}
      | c = {{Defof|Integer Addition}}
}}
{{eqn | r = \eqclass {\paren {a + c} + e, \paren {b + d} + f} {}
      | c = Natural Number Addition is Associative
}}
{{eqn | r = \eqclass {a + c, b + d} {} + \eqclass {e, f} {}
      | c = {{Defof|Integer Addition}}
}}
{{eqn | r = \paren {\eqclass {a, b} {} + \eqclass {c, d} {} } + \eqclass {e, f} {}
      | c = {{Defof|Integer Addition}}
}}
{{eqn | r = \paren {x + y} + z
      | c = {{Defof|Integer|subdef = Formal Definition}}
}}
{{end-eqn}}
{{qed}}
Theorem: Natural Number Addition is Commutative

The operation of addition on the set of natural numbers $\N$ is commutative:
:$\forall m, n \in \N: m + n = n + m$

Proof:
Consider the natural numbers defined as a naturally ordered semigroup.
By definition, the operation in a naturally ordered semigroup is commutative.
Hence the result.
{{qed}}
Theorem: Natural Number Addition is Commutative

The operation of addition on the set of natural numbers $\N$ is commutative:
:$\forall m, n \in \N: m + n = n + m$

Proof:
Proof by induction.
Consider the natural numbers $\N$ defined as the elements of the minimally inductive set $\omega$.
From the definition of addition in $\omega$, we have that:
{{begin-eqn}}
{{eqn | q = \forall m, n \in \N
      | l = m + 0
      | r = m
}}
{{eqn | l = m + n^+
      | r = \paren {m + n}^+
}}
{{end-eqn}}
For all $n \in \N$, let $\map P n$ be the proposition:
:$\forall m \in \N: m + n = n + m$
=== Basis for the Induction ===
From Natural Number Addition Commutes with Zero, we have:
:$\forall m \in \N: m + 0 = m = 0 + m$
Thus $\map P 0$ is seen to be true.
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 0$, then it logically follows that $\map P {k^+}$ is true.
So this is our induction hypothesis $\map P k$:
:$\forall m \in \N: m + k = k + m$
Then we need to show that $\map P {k^+}$ follows directly from $\map P k$:
:$\forall m \in \N: m + k^+ = k^+ + m$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = k^+ + m
      | r = \paren {k + m}^+
      | c = Natural Number Addition Commutativity with Successor
}}
{{eqn | r = \paren {m + k}^+
      | c = from the induction hypothesis
}}
{{eqn | r = m + k^+
      | c = by definition
}}
{{end-eqn}}
So $\map P k \implies \map P {k^+}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall m, n \in \N: m + n = n + m$
{{qed}}