avewright/proofwiki-math huggingface dataset:
Theorem: Integer is Sum of Three Triangular Numbers

Let $n$ be a positive integer.
Then $n$ is the sum of $3$ triangular numbers.

Proof:
From Integer as Sum of Three Odd Squares, $8 n + 3$ is the sum of $3$ odd squares.
So:
{{begin-eqn}}
{{eqn | q = \forall n \in \Z_{\ge 0}
      | l = 8 n + 3
      | r = \paren {2 x + 1}^2 + \paren {2 y + 1}^2 + \paren {2 z + 1}^2
      | c = for some $x, y, z \in \Z_{\ge 0}$
}}
{{eqn | r = 4 x^2 + 4 x + 4 y^2 + 4 y + 4 z^2 + 4 z + 3
      | c = 
}}
{{eqn | r = 4 \paren {x \paren {x + 1} + y \paren {y + 1} + z \paren {z + 1} } + 3
      | c = 
}}
{{eqn | ll= \leadsto
      | l = n
      | r = \frac {x \paren {x + 1} } 2 + \frac {y \paren {y + 1} } 2 + \frac {z \paren {z + 1} } 2
      | c = subtracting $3$ and dividing both sides by $8$
}}
{{end-eqn}}
By Closed Form for Triangular Numbers, each of $\dfrac {x \paren {x + 1} } 2$, $\dfrac {y \paren {y + 1} } 2$ and $\dfrac {z \paren {z + 1} } 2$ are triangular numbers.
{{qed}}
Theorem: Smallest Magic Square is of Order 3

Apart from the trivial order $1$ magic square:
{{:Magic Square/Examples/Order 1}}
the smallest magic square is the order $3$ magic square:
{{:Magic Square/Examples/Order 3}}

Proof:
Suppose there were an order $2$ magic square.
The row and column total is $\dfrac {1 + 2 + 3 + 4} 2 = 5$.
Any row or column with a $1$ in it must therefore also have a $4$ in it.
But there are:
:one row
:one column
:one diagonal
all of which have a $1$ in them.
Therefore the $4$ would need to go in all $3$ cells.
But $4$ appears in a magic square exactly once.
Hence there can be no order $2$ magic square.
{{qed}}
Theorem: Euler Phi Function of n equal to Euler Phi Function of n+3

Let $\phi$ denote the Euler $\phi$ function.
The only solutions to the equation:
:$\map \phi n = \map \phi {n + 3}$
less than $1 \, 000 \, 000$ are:
:$\map \phi 3 = \map \phi 6 = 2$
:$\map \phi 5 = \map \phi 8 = 4$

Proof:
{{ProofWanted|By exhaustion, I suppose}}
Theorem: Friendship Theorem

Let there be a group of $6$ people.
The traditional setting is that these $6$ people are at a party.
Then (at least) one of the following $2$ statements is true:
:$(1): \quad$ At least $3$ of these $6$ people have all met each other before
:$(2): \quad$ At least $3$ of these $6$ people have never met each other before.
That is, either there exists a set of $3$ mutual acquaintances, or there exists a set of $3$ mutual strangers.

Proof:
This is a simple example of Ramsey's Theorem.
{{ProofWanted}}
Theorem: Volume of Smallest Tetrahedron with Integer Edges and Integer Volume

The volume of the smallest tetrahedron with integer edges and integer volume is $3$.
There are $2$ possible sets of edges:
:$32, 33, 35, 44, 70, 76$
:$21, 32, 47, 56, 58, 76$

Proof:
{{tidy}}
Tartaglia's Formula gives us that:
:$V_T^2 = \dfrac {1} {288} \det \ \begin{vmatrix}  0 & 1 & 1 & 1 & 1 \\ 1 & 0 & d_{12}^2 & d_{13}^2 & d_{14}^2 \\ 1 & d_{12}^2 & 0 & d_{23}^2 & d_{24}^2 \\ 1 & d_{13}^2 & d_{23}^2 & 0 & d_{34}^2 \\ 1 & d_{14}^2 & d_{24}^2 & d_{34}^2 & 0 \end{vmatrix}$
where:
:$V_T$ denotes the volume of a tetrahedron
:$d_{ij}$ denotes the distance between vertex $\mathbf d_i$ and vertex $\mathbf d_j$
So the volume of the set lengths $32, 33, 35, 40, 70, 76$ is:
{{begin-eqn}}
{{eqn | l = V_T^2
      | r = \dfrac 1 {288} \det \ \begin{vmatrix}  0 & 1 & 1 & 1 & 1\\ 1 & 0 & 1024 & 1089 & 1936 \\ 1 & 1024 & 0 & 1225 & 4900 \\ 1 & 1089 & 1225 & 0 & 5776 \\ 1 & 1936 & 4900 & 5776 & 0 \end{vmatrix}
}}
{{eqn | r = \dfrac 1 {288} \det \ \begin{vmatrix}  0 & 1 & 1 & 1 & 1 \\ 1 & 0 & 1024 & 1089 & 1936 \\ 0 & 1024 & -1024 & 136 & 2964 \\ 0 & 1089 & 201 & -1089 & 3840 \\ 0 & 1936 & 3876 & 4687 & -1936 \end{vmatrix}
}}
{{eqn | r = \dfrac {-1} {288} \det \ \begin{vmatrix}  1 & 1 & 1 & 1 \\ 1024 & -1024 & 136 & 2964 \\ 1089 & 201 & -1089 & 3840 \\ 1936 & 3876 & 4687 & -1936 \end{vmatrix}
}}
{{eqn | r = \dfrac {-1} {288} \det \ \begin{vmatrix}  1 & 0 & 0 & 0 \\ 1024 & -2048 & -888 & 1940 \\ 1089 & -888 & -2178 & 2751 \\ 1936 & 1940 & 2751 & -3872 \end{vmatrix}
}}
{{eqn | r = \dfrac {-1} {288} \det \ \begin{vmatrix} -2048 & -888 & 1940 \\ -888 & -2178 & 2751 \\ 1940 & 2751 & -3872 \end{vmatrix}
}}
{{eqn | r = \dfrac {\paren {-2048 \times \paren {\paren {-2178} \times \paren {-3872} - 2751 \times 2751} + 888 \times \paren {\paren {-888} \times \paren {-3872} - 2751 \times 1940} + 1940 \times \paren {-888 \times 2751 + 2178 \times 1940} } } {-288}
}}
{{eqn | r = 9}}
{{end-eqn}}
Hence the result.
{{qed|lemma}}
{{finish|So far so good, and it has been demonstrated that the numbers given supply the tetrahedron with the volume quoted, but it remains of course to prove that this, and its companion, are the smallest.}}
Theorem: Ramanujan's Infinite Nested Roots

:$3 = \sqrt {1 + 2 \sqrt {1 + 3 \sqrt { 1 + \cdots} } }$

Proof:
We have:
{{begin-eqn}}
{{eqn | l = 3
      | r = \sqrt 9
      | c = 
}}
{{eqn | r = \sqrt {1 + 8}
      | c = 
}}
{{eqn | r = \sqrt {1 + 2 \sqrt {16} }
      | c = 
}}
{{eqn | r = \sqrt {1 + 2 \sqrt {1 + 15} }
      | c = 
}}
{{eqn | r = \sqrt {1 + 2 \sqrt {1 + 3 \sqrt {25} } }
      | c = 
}}
{{eqn | r = \sqrt {1 + 2 \sqrt {1 + 3 \sqrt {1 + 24} } }
      | c = 
}}
{{eqn | r = \sqrt {1 + 2 \sqrt {1 + 3 \sqrt {1 + 4 \sqrt {36} } } }
      | c = 
}}
{{end-eqn}}
In order for this sequence to continue, it needs to be shown that:
:$n + 1 = \sqrt {1 + n \left({n + 2}\right)}$
Thus:
{{begin-eqn}}
{{eqn | l = \sqrt {1 + n \left({n + 2}\right)}
      | r = \sqrt {1 + n^2 + 2 n}
      | c = 
}}
{{eqn | r = \sqrt {\left({n + 1}\right)^2}
      | c = Square of Sum
}}
{{eqn | r = n + 1
      | c = 
}}
{{end-eqn}}
The result follows.
{{qed}}
{{Namedfor|Srinivasa Ramanujan|cat = Ramanujan}}
Theorem: Product of Three Consecutive Integers is never Perfect Power

Let $n \in \Z_{> 1}$ be a (strictly) positive integer.
Then:
:$\paren {n - 1} n \paren {n + 1}$
cannot be expressed in the form $a^k$ for $a, k \in \Z$ where $k \ge 2$.
That is, the product of $3$ consecutive (strictly) positive integers can never be a perfect power.

Proof:
{{AimForCont}} $\paren {n - 1} n \paren {n + 1} = a^k$ for $a, k \in \Z$ where $k \ge 2$.
We have that:
:$\gcd \set {n − 1, n} = 1 = \gcd \set {n, n + 1}$
Thus $n$ must itself be a perfect power of the form $z^k$ for some $z \in \Z$.
That means $\paren {n - 1} \paren {n + 1} = n^2 - 1$ must also be a perfect power of the same form.
Let:
:$n = r^k$ and $n^2 − 1 = s^k$
for $r, s \in \Z$.
Then:
:$\paren {r^2}^k = 1 + s^k$
But the only consecutive integers that are $k$th powers are (trivially) $0$ and $1$.
Hence by Proof by Contradiction there can be no such $n$.
{{qed}}
Theorem: Barbier's Theorem

Let $K$ be a closed curve of constant diameter.
{{explain|"constant diameter"}}
Let the circumference of $K$ be $c$.
Let the diameter of $K$ be $d$.
Then:
:$\dfrac c d = \pi$

Proof:
{{ProofWanted}}
{{Namedfor|Joseph-Émile Barbier|cat = Barbier}}
Theorem: Machin's Formula for Pi

:$\dfrac \pi 4 = 4 \arctan \dfrac 1 5 - \arctan \dfrac 1 {239} \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
Let $\tan \alpha = \dfrac 1 5$.
Then:
{{begin-eqn}}
{{eqn | l = \tan 2 \alpha
      | r = \frac {2 \tan \alpha} {1 - \tan^2 \alpha}
      | c = Double Angle Formula for Tangent
}}
{{eqn | r = \frac {2 / 5} {1 - 1 / 25}
      | c = 
}}
{{eqn | r = \frac 5 {12}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tan 4 \alpha
      | r = \frac {2 \tan 2 \alpha} {1 - \tan^2 2 \alpha}
      | c = Double Angle Formula for Tangent
}}
{{eqn | r = \frac {2 \times 5 / 12} {1 - 25 / 144}
      | c = 
}}
{{eqn | r = \frac {120} {119}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \tan \left({4 \alpha - \frac \pi 4}\right)
      | r = \frac {\tan 4 \alpha - \tan \frac \pi 4} {1 + \tan 4 \alpha \tan \frac \pi 4}
      | c = Tangent of Difference
}}
{{eqn | r = \frac {\tan 4 \alpha - 1} {1 + \tan 4 \alpha}
      | c = Tangent of $45^\circ$
}}
{{eqn | r = \frac {120 / 119 - 1} {120 / 119 + 1}
      | c = 
}}
{{eqn | r = \frac 1 {239}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = 4 \alpha - \frac \pi 4
      | r = \arctan \frac 1 {239}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac \pi 4
      | r = 4 \arctan \frac 1 5 - \arctan \frac 1 {239}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Machin's Formula for Pi

:$\dfrac \pi 4 = 4 \arctan \dfrac 1 5 - \arctan \dfrac 1 {239} \approx 0 \cdotp 78539 \, 81633 \, 9744 \ldots$

Proof:
{{begin-eqn}}
{{eqn | l = \map \arg {\paren {5 + i }^4 \paren {239 - i} }
      | r = \map \arg {5 + i}^4 + \map \arg {239 - i}
      | c = Argument of Product equals Sum of Arguments
}}
{{eqn | r = 4 \map \arg {5 + i} + \map \arg {239 - i}
      | c = Argument of Product equals Sum of Arguments
}}
{{eqn | r = 4 \arctan \frac 1 5 + \arctan \frac {-1} {239}
}}
{{eqn | r = 4 \arctan \frac 1 5 - \arctan \frac 1 {239}
      | c = Inverse Tangent is Odd Function
}}
{{end-eqn}}
{{questionable|We cannot take it for granted that $\map \arg z {{=}} \arctan \dfrac {\Im z} {\Re z}$, we have to be sure we know what quadrant we are in. Clearly here $\Re z > 0$ so complications don't directly arise, but we might want to use the cosine/sine definition to be rigorous}}
Furthermore, because:
{{begin-eqn}}
{{eqn | l = \paren {5 + i}^4
      | r = 5^4 + 4 \times 5^3 i - 6 \times 5^2 - 4 \times 5 i + 1
      | c = Binomial Theorem
}}
{{eqn | r = 476 + 480i
      | c = simplifying
}}
{{end-eqn}}
we can write:
{{begin-eqn}}
{{eqn | l = \paren {5 + i}^4 \paren {239 - i}
      | r = \paren {476 + 480 i} \paren {239 - i}
      | c = 
}}
{{eqn | r = 113764 + 480 + 114720i - 476i
      | c = 
}}
{{eqn | r = 114244 + 114244i
      | c = 
}}
{{end-eqn}}
From there, we substitute:
{{begin-eqn}}
{{eqn | l = \map \arg {\paren {5 + i }^4 \paren {239 - i} }
      | r = \map \arg {114244 + 114244 i}
      | c =
}}
{{eqn | r = \arctan \frac {114244} {114244}
      | c = 
}}
{{eqn | r = \arctan 1
      | c = 
}}
{{eqn | r = \frac \pi 4
      | c = 
}}
{{end-eqn}}
By transitivity:
:$\dfrac \pi 4 = 4 \arctan \dfrac 1 5 - \arctan \dfrac 1 {239}$
{{qed}}
Theorem: Ordinals under Addition form Ordered Semigroup

$\struct {\On, +, \le}$ forms an ordered semigroup, where:
:$\On$ denotes the class of all ordinals
:$+$ denotes ordinal addition.

Proof:
The result follows from:
:Ordinals under Addition form Semigroup
:Subset is Compatible with Ordinal Addition.
{{qed}}
Category:Ordinal Arithmetic
8qttvuwa309nvykcf83jkgoc1e9zw3s
Theorem: Subset is Left Compatible with Ordinal Addition

Let $x, y, z$ be ordinals.
Then:
:$x \le y \implies \paren {z + x} \le \paren {z + y}$

Proof:
The result follows from Membership is Left Compatible with Ordinal Addition.
{{qed}}
Category:Ordinal Arithmetic
49mwa205l5rwaqgavvl8dr7kwd8c0x8
Theorem: Subset is Compatible with Ordinal Addition

Let $x, y, z$ be ordinals.
Then:
:$(1): \quad x \le y \implies \paren {z + x} \le \paren {z + y}$
:$(2): \quad x \le y \implies \paren {x + z} \le \paren {y + z}$

Proof:
The result follows from Subset is Left Compatible with Ordinal Addition and Subset is Right Compatible with Ordinal Addition.
{{qed}}
Category:Ordinal Arithmetic
tnh5ow7h12m60x4xi6nsx7h21p49lkp
Theorem: Ordinals under Addition form Semigroup

$\struct {\On, +}$ forms an semigroup, where:
:$\On$ denotes the class of all ordinals
:$+$ denotes ordinal addition.

Proof:
The result follows from Ordinal Addition is Closed and Ordinal Addition is Associative.
{{qed}}
Category:Ordinal Arithmetic
jnv27w4ulw2yj7bss9t1hpvl92khmel
Theorem: Ordinals under Multiplication form Semigroup

$\struct {\On, \times}$ forms an semigroup, where:
:$\On$ denotes the class of all ordinals
:$\times$ denotes ordinal multiplication.

Proof:
The result follows from Ordinal Multiplication is Closed and Ordinal Multiplication is Associative.
{{qed}}
Category:Ordinal Arithmetic
3ah3i1ewrt3oypxxa65nzung54kfen3
Theorem: Subset is Left Compatible with Ordinal Multiplication

Let $x, y, z$ be ordinals.
Then:
:$x \le y \implies \paren {z \cdot x} \le \paren {z \cdot y}$

Proof:
The result follows from Membership is Left Compatible with Ordinal Multiplication.
{{qed}}
Category:Ordinal Arithmetic
nbbl4noxedxydteko8x3i0py1q6rquy
Theorem: Subset is Compatible with Ordinal Multiplication

Let $x, y, z$ be ordinals.
Then:
:$(1): \quad x \le y \implies \paren {z \cdot x} \le \paren {z \cdot y}$
:$(2): \quad x \le y \implies \paren {x \cdot z} \le \paren {y \cdot z}$

Proof:
The result follows from Subset is Left Compatible with Ordinal Multiplication and Subset is Right Compatible with Ordinal Multiplication.
{{qed}}
Category:Ordinal Arithmetic
bgxr6qjjz1yiwwtldsoeknzd90zjzpd
Theorem: Ordinals under Multiplication form Ordered Semigroup

$\struct {\On, \times, \le}$ forms an ordered semigroup, where:
:$\On$ denotes the class of all ordinals
:$\times$ denotes ordinal multiplication.

Proof:
The result follows from Ordinals under Multiplication form Semigroup and Subset is Compatible with Ordinal Multiplication.
{{qed}}
Category:Ordinal Arithmetic
hrhb6j3x90u2f8z2aytlnh30sc8eeyq
Theorem: Ordinals under Addition form Monoid

$\struct {\On, +}$ forms an monoid, where:
:$\On$ denotes the class of all ordinals
:$+$ denotes ordinal addition.

Proof:
The result follows from Ordinals under Addition form Semigroup and Ordinal Addition by Zero.
{{qed}}
Category:Ordinal Arithmetic
3u2ecmtz643ai87qqd4p7eh1jdq5q43
Theorem: Ordinals under Addition form Ordered Monoid

$\struct {\On, +, \le}$ forms an ordered monoid, where:
:$\On$ denotes the class of all ordinals
:$+$ denotes ordinal addition.

Proof:
The result follows from Ordinals under Addition form Monoid and Ordinals under Addition form Ordered Semigroup.
{{qed}}
Category:Ordinal Arithmetic
pyuq3l2vwaucge2hh0q77jppigcjlpw
Theorem: Ordinals under Multiplication form Monoid

$\struct {\On, \times}$ forms an monoid, where:
:$\On$ denotes the class of all ordinals
:$\times$ denotes ordinal multiplication.

Proof:
The result follows from Ordinals under Multiplication form Semigroup and Ordinal Multiplication by One.
{{qed}}
Category:Ordinal Arithmetic
qf2fhfd9q8s8z4hh3vizhegcpnuvut1
Theorem: Ordinals under Multiplication form Ordered Monoid

$\struct {\On, \times, \le}$ forms an ordered monoid, where:
:$\On$ denotes the class of all ordinals
:$\times$ denotes ordinal multiplication.

Proof:
The result follows from Ordinals under Multiplication form Monoid and Ordinals under Multiplication form Ordered Semigroup.
{{qed}}
Category:Ordinal Arithmetic
3frch88jn92dtba6d2q09fwm97dzfqy
Theorem: Buffon's Needle

Let a horizontal plane be divided into strips by a series of parallel lines a fixed distance apart, like floorboards.
Let a needle whose length equals the distance between the parallel lines be dropped onto the plane randomly from a random height.
Then the probability that the needle falls across one of the parallel lines is $\dfrac 2 \pi$.

Proof:
Let $N$ refer to the needle.
For simplicity, consider the real number plane $\R^2$ divided into strips by the lines $x = k$ for each integer $k$.
Then $N$ would have length $1$, which is the distance between the lines.
Define $\theta \in \hointr {-\dfrac \pi 2} {\dfrac \pi 2}$ as the angle between $N$ and the $x$-axis.
Then the horizontal component of the length of $N$ is $\cos \theta$ for each $\theta$.
Let:
:$E$ be the event where $N$ falls across a vertical line
:$\Theta_\theta$ be the event where the angle between $N$ and the $x$-axis is $\theta$.
Let $N$ drop.
{{WLOG}}, let the end with the larger $x$-coordinate have $x$-coordinate $0 \le x_n < 1$.
Then for each $\theta$, $N$ falls across the line $x = 0$ exactly when $x_n \le \cos \theta$.
Therefore the probability that this happens is:
:$\condprob E {\Theta_\theta} = \dfrac {\cos \theta} 1 = \cos \theta$
By considering $\theta$ as a continuous random variable:
{{begin-eqn}}
{{eqn | l = \map \Pr E
      | r = \sum_{\theta \mathop \in \hointr {-\pi / 2} {\pi / 2} } \condprob E {\Theta_\theta} \map \Pr {\Theta_\theta}
      | c = Total Probability Theorem
}}
{{eqn | r = \int_{-\pi / 2}^{\pi / 2} \cos \theta \frac {\d \theta} \pi
}}
{{eqn | r = \intlimits {\frac 1 \pi \sin\theta} {-\pi / 2} {\pi / 2}
      | c = Primitive of Cosine Function
}}
{{eqn | r = \frac 1 \pi \paren {1 - \paren {-1} }
}}
{{eqn | r = \frac 2 \pi
}}
{{end-eqn}}
{{qed}}
Theorem: Pi as Sum of Odd Reciprocals Alternating in Sign in Pairs

:$\dfrac {\pi \sqrt 2} 4 = 1 + \dfrac 1 3 - \dfrac 1 5 - \dfrac 1 7 + \dfrac 1 9 + \dfrac 1 {11} - \dfrac 1 {13} - \dfrac 1 {15} \cdots$

Proof:
Let $f: \R \to \R$ be the real function defined as:
:$\forall x \in \R: \map f x = \dfrac {x^1} 1 + \dfrac {x^3} 3 - \dfrac {x^5} 5 - \dfrac {x^7} 7 + \dfrac {x^9} 9 + \dfrac {x^{11} } {11} - \dfrac {x^{13} } {13} - \dfrac {x^{15} } {15} \cdots$
We first confirm that the series will converge at $x = 1$.
By grouping the series two terms at a time, we are guaranteed convergence by the Alternating Series Test:
:$ \map f 1 = \paren {1 + \dfrac 1 3 } - \paren { \dfrac 1 5 + \dfrac 1 7 } + \paren { \dfrac 1 9 + \dfrac 1 {11} } - \cdots + \paren {-1}^{\floor {\frac {k - 1} 2} } \paren {\dfrac 1 {2k - 1 } + \dfrac 1 {2k + 1 } } $ 
We now move on to determining the sum of $\map f 1$.
We have:
{{begin-eqn}}
{{eqn | l = \map f x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \paren {\frac {x^{4 n + 1} } {4 n + 1} + \frac {x^{4 n + 3} } {4 n + 3} }
      | c =
}}
{{eqn | ll= \leadsto
      | l = \map {f'} x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \paren {x^{4 n} + x^{4 n + 2} }
      | c = Power Rule for Derivatives
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \paren {1 + x^2} \paren {x^{4 n} }
      | c = Product of Powers
}}
{{eqn | r = \paren {1 + x^2} \sum_{n \mathop = 0}^\infty \paren {-1}^n \paren {x^{4 n} }
      | c = 
}}
{{eqn | r = \paren {1 + x^2} \sum_{n \mathop = 0}^\infty \paren {-x^4 }^n
      | c = Power of Power and Power of Product
}}
{{eqn | r = \dfrac {1 + x^2} {1 - \paren{-x^4 } }
      | c = Sum of Infinite Geometric Sequence
}}
{{eqn | r = \dfrac {1 + x^2} {1 + x^4}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \map f 1
      | r = \int_0^1 \dfrac {1 + x^2} {1 + x^4} \rd x
      | c = Fundamental Theorem of Calculus/Second Part
}}
{{eqn | r = \intlimits {\dfrac 1 {\sqrt 2} \map \arctan {\dfrac 1 {\sqrt 2} \paren {x - \dfrac 1 x} } } 0 1
      | c = Primitive of One plus x Squared over One plus Fourth Power of x
}}
{{eqn | r = \dfrac 1 {\sqrt 2} \map \arctan {\dfrac 1 {\sqrt 2} \paren {1 - \dfrac 1 1} } - \dfrac 1 {\sqrt 2} \map \arctan {\dfrac 1 {\sqrt 2} \paren {0 - \dfrac 1 0} }
      | c = 
}}
{{eqn | r = \dfrac 1 {\sqrt 2} \paren {\map \arctan 0 - \map \arctan {-\infty} }
      | c =
}}
{{eqn | r = \dfrac 1 {\sqrt 2} \paren {0 - \paren {-\dfrac \pi 2} }
      | c = {{Defof|Real Arctangent}}
}}
{{eqn | r = \dfrac {\pi \sqrt 2} 4
      | c =
}}
{{end-eqn}}
{{qed}}
Theorem: Pi as Sum of Alternating Sequence of Products of 3 Consecutive Reciprocals

:$\dfrac {\pi - 3} 4 = \dfrac 1 {2 \times 3 \times 4} - \dfrac 1 {4 \times 5 \times 6} + \dfrac 1 {6 \times 7 \times 8} \cdots$

Proof:
The alternating sum can be written as $\ds \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1}} {2 n \paren{2 n + 1} \paren{2 n + 2}}$.
By partial fraction decomposition:
:$\ds \frac 1 {2 n \paren {2 n + 1} \paren {2 n + 2}} = \frac 1 2 \paren{\frac 1 {2 n} - \frac 2 {2 n + 1} + \frac 1 {2 n + 2}}$
Therefore:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } {2 n \paren{2 n + 1} \paren{2 n + 2} }
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } 2 \paren{\frac 1 {2 n} - \frac 2 {2 n + 1} + \frac 1 {2 n + 2} }
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } {4 n} - \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } {2 n + 1} - \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 2} } {4 \paren {n + 1} }
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n + 1} } {4 n} - \sum_{n \mathop = 2}^\infty \frac {\paren {-1}^{n + 1} } {4 n} + \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n} {2 n + 1} - 1
      | c = Translation of Index Variable of Summation
}}
{{eqn | r = \frac 1 4 + \frac \pi 4 - 1
      | c = Leibniz's Formula for Pi
}}
{{eqn | r = \frac {\pi - 3} 4
}}
{{end-eqn}}
{{qed}}
Theorem: Basel Problem as Infinite Product

:$\ds \dfrac {\pi^2} 6 = \prod_{p \mathop \in \mathbb P} \dfrac {p^2} {p^2 - 1}$

Proof:
From Sum of Reciprocals of Powers as Euler Product:
:$\ds \sum_{n \mathop \ge 1} \dfrac 1 {n^z} = \prod_p \frac 1 {1 - p^{-z} }$
for $z \in \C$ such that $\map \Re z > 1$.
Putting $z = 2$:
{{begin-eqn}}
{{eqn | l = \sum_{n \mathop \ge 1} \dfrac 1 {n^2}
      | r = \prod_p \frac 1 {1 - p^{-2} }
      | c = 
}}
{{eqn | r = \prod_p \frac {p^2} {p^2 - 1}
      | c = multiplying top and bottom by $p^2$
}}
{{end-eqn}}
The result follows from Riemann Zeta Function of $2$.
{{qed}}
Theorem: Convergence of Taylor Series of Function Analytic on Disk

Let $F$ be a complex function.
Let $x_0$ be a point in $\R$.
Let $R$ be an extended real number greater than zero.
Let $F$ be analytic at every point $z \in \C$ satisfying $\size {z - \tuple {x_0, 0} } < R$
where $\tuple {x_0, 0}$ denotes the complex number with real part $x_0$ and imaginary part $0$.
Let the restriction of $F$ to $\R \to \C$ be a real function $f$.
This means:
:$\forall x \in \R:$
::$\map f x = \map \Re {\map F {x, 0} }$
::$0 = \map \Im {\map F {x, 0} }$
where $\tuple {x, 0}$ denotes the complex number with real part $x$ and imaginary part $0$.
Then:
:the Taylor series of $f$ about $x_0$ converges to $f$ at every point $x \in \R$ satisfying $\size {x - x_0} < R$

Proof:
Let $z$ be a real number.
We have:
:$\ds \sum_{n \mathop = 0}^\infty n z^n$ has radius of convergence of $1$
by Complex Power Series/Examples/n.
This leads to that:
:$\ds \sum_{n \mathop = 0}^\infty n \paren {\frac 1 y}^n$ converges
as $\ds \frac 1 y < 1$ as $y > 1$.
This leads to that:
:the sequence $\ds \sequence {\frac n {y^n}}$ converges to the limit $0$
by Terms in Convergent Series Converge to Zero.
This means that:
:$\ds \lim_{n \mathop \to \infty} \frac n {y^n}$ = $0$
by definition of limit.
This concludes the proof.
{{qed}}
Theorem: Convergence of Taylor Series of Function Analytic on Disk

Let $F$ be a complex function.
Let $x_0$ be a point in $\R$.
Let $R$ be an extended real number greater than zero.
Let $F$ be analytic at every point $z \in \C$ satisfying $\size {z - \tuple {x_0, 0} } < R$
where $\tuple {x_0, 0}$ denotes the complex number with real part $x_0$ and imaginary part $0$.
Let the restriction of $F$ to $\R \to \C$ be a real function $f$.
This means:
:$\forall x \in \R:$
::$\map f x = \map \Re {\map F {x, 0} }$
::$0 = \map \Im {\map F {x, 0} }$
where $\tuple {x, 0}$ denotes the complex number with real part $x$ and imaginary part $0$.
Then:
:the Taylor series of $f$ about $x_0$ converges to $f$ at every point $x \in \R$ satisfying $\size {x - x_0} < R$

Proof:
Note that $\ln y > 0$ as $y > 1$.
{{begin-eqn}}
{{eqn | l = \lim_{n \mathop \to \infty} \frac n {y^n}
      | r = \lim_{n \mathop \to \infty} \frac n {\paren {e^{\ln y} }^n}
}}
{{eqn | r = \lim_{n \mathop \to \infty} \frac n {e^{\paren {\ln y} n} }
}}
{{eqn | r = 0
      | c = as $\ds \lim_{x \mathop \to \infty} \frac x {e^{\paren {\ln y} x} } = 0$ by Limit at Infinity of Polynomial over Complex Exponential as $\ln y > 0$
}}
{{end-eqn}}
{{qed}}
Theorem: Taylor Series of Analytic Function has infinite Radius of Convergence

Let $F$ be a complex function.
Let $F$ be analytic everywhere.
Let the restriction of $F$ to $\R \to \C$ be a real function $f$.
This means:
:$\forall x \in \R: \map f x = \map \Re {\map F {x, 0} }, 0 = \map \Im {\map F {x, 0} }$
where $\tuple {x, 0}$ denotes the complex number with real part $x$ and imaginary part $0$.
Let $x_0$ be a point in $\R$.
Then:
:the Taylor series of $f$ about $x_0$ converges to $f$ at every point in $\R$.

Proof:
The result follows by Convergence of Taylor Series of Function Analytic on Disk for the case $R = \infty$.
{{qed}}