avewright/proofwiki-math huggingface dataset:
Theorem: Derivative of Inverse Hyperbolic Sine

:$\map {\dfrac \d {\d x} } {\arsinh x} = \dfrac 1 {\sqrt {x^2 + 1} }$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \arsinh x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \sinh y
      | c = {{Defof|Real Inverse Hyperbolic Sine}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = \cosh y
      | c = Derivative of Hyperbolic Sine
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac 1 {\cosh y}
      | c = Derivative of Inverse Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \pm \frac 1 {\sqrt {\sinh^2 y + 1} }
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{end-eqn}}
For all $x \in \R$ we have that $\cosh y \ge 1$.
Thus it follows that it is necessary to take the positive root of $\sqrt {\sinh^2 y + 1}$.
So:
{{begin-eqn}}
{{eqn | l = \frac {\d y} {\d x}
      | r = \frac 1 {\sqrt {\sinh^2 y + 1} }
      | c =
}}
{{eqn | ll= \leadsto
      | l = \map {\frac \d {\d x} } {\arsinh x}
      | r = \frac 1 {\sqrt {x^2 + 1} }
      | c = Definition of $x$ and $y$
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Real Area Hyperbolic Cosine

:$\map {\dfrac \d {\d x} } {\arcosh x} = \dfrac 1 {\sqrt {x^2 - 1} }$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \arcosh x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \cosh y
      | c = {{Defof|Real Area Hyperbolic Cosine}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = \sinh y
      | c = Derivative of Hyperbolic Cosine
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac 1 {\sinh y}
      | c = Derivative of Inverse Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \pm \frac 1 {\sqrt {\cosh^2 y - 1} }
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{end-eqn}}
Note that when $y = 0$, $\cosh y$ is defined and equals $1$.
But from Derivative of Hyperbolic Cosine:
:$\valueat {\dfrac \d {\d y} \cosh y} {y \mathop = 0} = \sinh 0 = 0$
Thus $\dfrac {\d y} {\d x} = \dfrac 1 {\sinh y}$ is not defined at $y = 0$.
Hence the limitation of the domain of $\map {\dfrac \d {\d x} } {\arcosh x}$ to exclude $x = 1$.
Now it is necessary to determine the sign of $\dfrac {\d y} {\d x}$.
From:
:Real Area Hyperbolic Cosine is Strictly Increasing
:Derivative of Strictly Increasing Real Function is Strictly Positive
it follows that $\map {\dfrac \d {\d x} } {\arcosh x} > 0$ on $\R_{>1}$.
Thus:
:$\dfrac {\d y} {\d x} = \dfrac 1 {\sqrt {\cosh^2 y - 1} }$
where $\sqrt {\cosh^2 y - 1}$ denotes the positive square root of $\cosh^2 y - 1$.
Hence by definition of $x$ and $y$ above:
:$\map {\dfrac \d {\d x} } {\arcosh x} = \dfrac 1 {\sqrt {x^2 - 1} }$
{{qed}}
Theorem: Derivative of Inverse Hyperbolic Tangent

:$\map {\dfrac \d {\d x} } {\tanh^{-1} x} = \dfrac 1 {1 - x^2}$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \tanh^{-1} x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \tanh y
      | c = {{Defof|Real Inverse Hyperbolic Tangent}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = \sech^2 y
      | c = Derivative of Hyperbolic Tangent
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac 1 {\sech^2 y}
      | c = Derivative of Inverse Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac 1 {1 - \tanh^2 y}
      | c = Sum of Squares of Hyperbolic Secant and Tangent
}}
{{eqn | ll= \leadsto
      | l = \map {\frac \d {\d x} } {\tanh^{-1} x}
      | r = \frac 1 {1 - x^2}
      | c = Definition of $x$ and $y$
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Inverse Hyperbolic Cotangent

:$\map {\dfrac \d {\d x} } {\coth^{-1} x} = \dfrac {-1} {x^2 - 1}$

Proof:
{{begin-eqn}}
{{eqn | l = y
      | r = \coth^{-1} x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \coth y
      | c = {{Defof|Real Inverse Hyperbolic Cotangent}}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = -\csch^2 y
      | c = Derivative of Hyperbolic Cotangent
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac {-1} {\csch^2 y}
      | c = Derivative of Inverse Function
}}
{{eqn | r = \frac {-1} {\coth^2 y - 1}
      | c = Difference of Squares of Hyperbolic Cotangent and Cosecant
}}
{{eqn | ll= \leadsto
      | l = \map {\frac \d {\d x} } {\coth^{-1} x}
      | r = \frac {-1} {x^2 - 1}
      | c = Definition of $x$ and $y$
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Inverse Hyperbolic Secant

:$\map {\dfrac \d {\d x} } {\arsech x} = \dfrac {-1} {x \sqrt{1 - x^2} }$

Proof:
$\arsech x$ is defined only on the half-open real interval $\hointl 0 1$.
Thus on $\hointl 0 1$:
{{begin-eqn}}
{{eqn | l = y
      | r = \arsech x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \sech y
      | c = where $y \in \R_{>0}$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = -\sech y \tanh y
      | c = Derivative of Hyperbolic Secant
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \dfrac {-1} {\sech y \ \tanh y}
      | c = Derivative of Inverse Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac {-1} {\sech y \sqrt {1 - \sech^2 y} }
      | c = Sum of Squares of Hyperbolic Secant and Tangent
}}
{{eqn | ll= \leadsto
      | l = \map {\frac \d {\d x} } {\arsech x}
      | r = \frac {-1} {x \sqrt {1 - x^2} }
      | c = Definition of $x$ and $y$
}}
{{end-eqn}}
When $x = 1$, however, $\sqrt{1 - x^2} = 0$ and so $\dfrac {-1} {x \sqrt {1 - x^2} }$ is undefined.
Hence $\arsech x$ can be defined only on $\openint 0 1$.
{{explain|Explain why positive square root is taken at Sum of Squares of Hyperbolic Secant and Tangent}}
{{qed}}
Theorem: Derivative of Inverse Hyperbolic Cosecant

:$\map {\dfrac \d {\d x} } {\arcsch x} = \dfrac {-1} {\size x \sqrt {1 + x^2} }$

Proof:
500pxright
Let $x > 1$.
Then we have:
{{begin-eqn}}
{{eqn | l = y
      | r = \arcsch x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = \csch y
      | c = where $y \ne 0$
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d y}
      | r = -\csch y \coth y
      | c = Derivative of Hyperbolic Cosecant
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \dfrac {-1} {\csch y \coth y}
      | c = Derivative of Inverse Function
}}
{{eqn | ll= \leadsto
      | l = \frac {\d y} {\d x}
      | r = \frac {-1} {\csch y \sqrt {1 + \csch^2 y} }
      | c = Difference of Squares of Hyperbolic Cotangent and Cosecant
}}
{{eqn | ll= \leadsto
      | l = \map {\frac \d {\d x} } {\arcsch x}
      | r = \frac {-1} {x \sqrt {1 + x^2} }
      | c = Definition of $x$ and $y$
}}
{{eqn | r = \frac {-1} {\size x \sqrt {1 + x^2} }
      | c = as $x > 0$
}}
{{end-eqn}}
We have that Inverse Hyperbolic Cosecant is Odd Function.
Hence from Derivative of Odd Function is Even, $\map {\dfrac \d {\d x} } {\arcsch x}$ is even.
Hence for $x < -1$ we have that:
:$\map {\dfrac \d {\d x} } {\arcsch x} = \dfrac {-1} {\paren {-x} \sqrt {1 + x^2} }$
and so for $x < -1$:
:$\map {\dfrac \d {\d x} } {\arcsch x} = \dfrac {-1} {\size x \sqrt {1 + x^2} }$
and the result follows.
{{qed}}
Theorem: Sum of Cosecant and Cotangent

:$\csc x + \cot x = \cot {\dfrac x 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \csc x + \cot x
      | r = \frac 1 {\sin x} + \frac {\cos x} {\sin x}
      | c = {{Defof|Cosecant}} and {{Defof|Cotangent}}
}}
{{eqn | r = \frac {1 + \cos x} {\sin x}
      | c =
}}
{{eqn | r = \frac {2 \cos^2 {\frac x 2} } {2 \sin {\frac x 2} \cos {\frac x 2} }
      | c = Double Angle Formula for Sine and {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | r = \frac {\cos {\frac x 2} } {\sin {\frac x 2} }
      | c =
}}
{{eqn | r = \cot {\frac x 2}
      | c = {{Defof|Cotangent}}
}}
{{end-eqn}}
{{qed}}
Category:Trigonometric Identities
cvaa2ej0mtojjj4xslufiyb10t05kbm
Theorem: Leibniz's Rule/One Variable/Second Derivative

Let $f$ and $g$ be real functions defined on the open interval $I$.
Let $x \in I$ be a point in $I$ at which both $f$ and $g$ are twice differentiable.
Then:
:$\paren {\map f x \map g x}' ' = \map f x \map {g' '} x + 2 \map {f'} x \map {g'} x + \map {f' '} x \map g x$

Proof:
From Leibniz's Rule in One Variable:
:$\ds \paren {\map f x \map g x}^{\paren n} = \sum_{k \mathop = 0}^n \binom n k \map {f^{\paren k} } x \map {g^{\paren {n - k} } } x$
where $\paren n$ denotes the order of the derivative.
Setting $n = 2$:
{{begin-eqn}}
{{eqn | l = \paren {\map f x \map g x}' '
      | r = \paren {\map f x \map g x}^{\paren 2}
      | c = {{Defof|Nth Derivative}}
}}
{{eqn | r = \sum_{k \mathop = 0}^2 \binom n k \map {f^{\paren k} } x \map {g^{\paren {n - k} } } x
      | c = Leibniz's Rule in One Variable
}}
{{eqn | r = \binom 2 0 \map {f^{\paren 0} } x \map {g^{\paren 2} } x + \binom 2 1 \map {f^{\paren 1} } x \map {g^{\paren 1} } x + \binom 2 2 {f^{\paren 2} } x \map {g^{\paren 0} } x
      | c = 
}}
{{eqn | r = \map {f^{\paren 0} } x \map {g^{\paren 2 } } x + 2 \map {f^{\paren 1} } x \map {g^{\paren 1} } x + \map {f^{\paren 2} } x \map {g^{\paren 0} } x
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | r = \map f x \map {g' '} x + 2 \map {f'} x \map {g'} x + \map {f' '} x \map g x
      | c = {{Defof|Nth Derivative}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Gottfried Wilhelm von Leibniz}}
Theorem: Leibniz's Rule/One Variable/Third Derivative

Let $f$ and $g$ be real functions defined on the open interval $I$.
Let $x \in I$ be a point in $I$ at which both $f$ and $g$ are thrice differentiable.
Then:
:$\paren {\map f x \map g x}' ' ' = \map f x \map {g' ' '} x + 3 \map {f'} x \map {g' '} x + 3 \map {f' '} x \map {g'} x + \map {f' ' '} x \map g x$

Proof:
From Leibniz's Rule in One Variable:
:$\ds \paren {\map f x \map g x}^{\paren n} = \sum_{k \mathop = 0}^n \binom n k \map {f^{\paren k} } x \map {g^{\paren {n - k} } } x$
where $\paren n$ denotes the order of the derivative.
Setting $n = 3$:
{{begin-eqn}}
{{eqn | l = \paren {\map f x \map g x}' ' '
      | r = \paren {\map f x \map g x}^{\paren 3}
      | c = {{Defof|Nth Derivative}}
}}
{{eqn | r = \sum_{k \mathop = 0}^3 \binom n k \map {f^{\paren k} } x \map {g^{\paren {n - k} } } x
      | c = Leibniz's Rule in One Variable
}}
{{eqn | r = \binom 3 0 \map {f^{\paren 0} } x \map {g^{\paren 3} } x + \binom 3 1 \map {f^{\paren 1} } x \map {g^{\paren 2} } x + \binom 3 2 \map {f^{\paren 2} } x \map {g^{\paren 1} } x + \binom 3 3 \map {f^{\paren 3} } x \map {g^{\paren 0} } x
      | c = 
}}
{{eqn | r = \map {f^{\paren 0} } x \map {g^{\paren 3} } x + 3 \map {f^{\paren 1} } x \map {g^{\paren 2} } x + 3 \map {f^{\paren 2} } x \map {g^{\paren 1} } x + \map {f^{\paren 3} } x \map {g^{\paren 0} } x
      | c = {{Defof|Binomial Coefficient}}
}}
{{eqn | r = \map f x \map {g' ' '} x + 3 \map {f'} x \map {g' '} x + 3 \map {f' '} x \map {g'} x + \map {f' ' '} x \map g x
      | c = {{Defof|Nth Derivative}}
}}
{{end-eqn}}
{{qed}}
{{Namedfor|Gottfried Wilhelm von Leibniz}}
Theorem: Power Series Expansion for Tangent Function

The tangent function has a Taylor series expansion:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = x + \frac {x^3} 3 + \frac {2 x^5} {15} + \frac {17 x^7} {315} + \cdots
      | c = 
}}
{{end-eqn}}
where $B_{2 n}$ denotes the Bernoulli numbers.
This converges for $\size x < \dfrac \pi 2$.

Proof:
From Power Series Expansion for Cotangent Function:
:$(1): \quad \cot x = \ds \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}$
Then:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \cot x - 2 \cot 2 x
      | c = Double Angle Formula for Cotangent
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!} - 2 \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} \, \paren {2 x}^{2 n - 1} } {\paren {2 n}!} 
      | c = by $(1)$
}}
{{eqn | r =  \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} \paren {1 - 2^{2 n} } B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c =
}}
{{eqn | r =  \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c =
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Power Series Expansion for Tangent Function

The tangent function has a Taylor series expansion:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = x + \frac {x^3} 3 + \frac {2 x^5} {15} + \frac {17 x^7} {315} + \cdots
      | c = 
}}
{{end-eqn}}
where $B_{2 n}$ denotes the Bernoulli numbers.
This converges for $\size x < \dfrac \pi 2$.

Proof:
We have:
{{begin-eqn}}
{{eqn | l = \frac x {e^x - 1}
      | r = \frac x 2 \paren {\frac 2 {e^x -  1} }
      | c = 
}}
{{eqn | r = \frac x 2 \paren {\frac {e^x - e^x + 2} {e^x - 1} }
      | c = 
}}
{{eqn | r = \frac x 2 \paren {\frac {\paren {e^x + 1} - \paren {e^x - 1} } {e^x - 1} }
      | c = 
}}
{{eqn | r = \frac x 2 \paren {\frac {e^x + 1} {e^x - 1} - 1}
      | c = 
}}
{{eqn | r = -\frac x 2 + \frac x 2 \paren {\frac {e^x + 1} {e^x - 1} }
      | c = 
}}
{{eqn | r = -\frac x 2 + \frac x 2 \paren {\frac {e^{x/2} + e^{-x/2} } {e^{x/2} - e^{-x/2} } }
      | c = multiplying top and bottom by $e^{-x/2}$
}}
{{end-eqn}}
Thus:
{{begin-eqn}}
{{eqn | n = 1
      | l = \frac x 2 \paren {\frac {e^{x/2} + e^{-x/2} } {e^{x/2} - e^{-x/2} } }
      | r = \sum_{n \mathop = 0}^\infty \frac {B_{2 n} } {\paren {2 n!} } x^{2 n}
      | c = {{Defof|Bernoulli Numbers/Generating Function|Bernoulli numbers}}
}}
{{end-eqn}}
Replacing $x$ with $2 i x$ in the {{LHS}} of $(1)$:
{{begin-eqn}}
{{eqn | o = 
      | r = \frac {2 i x} 2 \paren {\frac {e^{2 i x / 2} + e^{-2 i x / 2} } {e^{2 i x / 2} - e^{-2 i x / 2} } }
      | c = 
}}
{{eqn | r = i x \paren {\frac {e^{i x} + e^{-i x} } {e^{i x} - e^{-i x} } }
      | c = 
}}
{{eqn | r = x \cot x
      | c = Euler's Cotangent Identity
}}
{{end-eqn}}
Replacing $x$ with $2 i x$ in the {{RHS}} of $(1)$:
{{begin-eqn}}
{{eqn | o = 
      | r = \sum_{n \mathop = 0}^\infty \frac {B_{2 n} } {\paren {2 n!} } \paren {2 i x}^{2 n}
      | c = 
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {2^{2 n} B_{2 n} } {\paren {2 n!} } x^{2 n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x \cot x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {2^{2 n} B_{2 n} } {\paren {2 n!} } x^{2 n}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \cot x
      | r = \sum_{n \mathop = 0}^\infty \paren {-1}^n \frac {2^{2 n} B_{2 n} } {\paren {2 n!} } x^{2 n - 1}
      | c = 
}}
{{end-eqn}}
Then from Double Angle Formula for Cotangent:
:$\tan x = \cot x - 2 \cot 2 x$
from which:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} } {\paren {2 n}!} x^{2 n - 1} - 2 \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} B_{2 n} } {\paren {2 n}!} \paren {2 x}^{2 n - 1}
      | c = by $(1)$
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \frac {\paren {-1}^n 2^{2 n} (1 - 2^{2 n}) B_{2 n} } {\paren {2 n}!} x^{2 n - 1}
      | c =
}}
{{eqn | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} (2^{2 n} - 1) B_{2 n} } {\paren {2 n}!} x^{2 n - 1}
      | c =
}}
{{end-eqn}}
{{qed|lemma}}
Theorem: Power Series Expansion for Tangent Function

The tangent function has a Taylor series expansion:
{{begin-eqn}}
{{eqn | l = \tan x
      | r = \sum_{n \mathop = 1}^\infty \frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} \, x^{2 n - 1} } {\paren {2 n}!}
      | c = 
}}
{{eqn | r = x + \frac {x^3} 3 + \frac {2 x^5} {15} + \frac {17 x^7} {315} + \cdots
      | c = 
}}
{{end-eqn}}
where $B_{2 n}$ denotes the Bernoulli numbers.
This converges for $\size x < \dfrac \pi 2$.

Proof:
By Combination Theorem for Limits of Real Functions we can deduce the following.
{{begin-eqn}}
{{eqn | o = 
      | r = \lim_{n \mathop \to \infty} \size {\frac {\frac {\paren {-1}^n 2^{2 n + 2} \paren {2^{2 n + 2} - 1} B_{2 n + 2} } {\paren {2 n + 2}!} x^{2 n + 1} } {\frac {\paren {-1}^{n - 1} 2^{2 n} \paren {2^{2 n} - 1} B_{2 n} } {\paren {2 n}!} x^{2 n - 1} } }
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac {\paren {2^{2 n + 2} - 1} } {\paren {2^{2 n} - 1} } \frac 1 {\paren {2 n + 1} \paren {2 n + 2} } \frac {B_{2 n + 2} } {B_{2 n} } } 4 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac {2^{2 n + 2} - 1} {2^{2 n} - 1} } \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {B_{2 n + 2} } {B_{2 n} } } 2 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {4 \frac {2^{2 n} } {2^{2 n} - 1} - \frac 1 {2^{2 n} - 1} } \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {B_{2 n + 2} } {B_{2 n} } } 2 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {4 + \frac 4 {2^{2 n} - 1} - \frac 1 {2^{2 n} - 1} } \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {B_{2 n + 2} } {B_{2 n} } } 2 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {B_{2 n + 2} } { B_{2 n} } } 8 x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac 1 {\paren {2 n + 1} \paren {n + 1} } \frac {\paren {-1}^{n + 2} 4 \sqrt {\pi \paren {n + 1} } \paren {\frac {n + 1} {\pi e} }^{2 n + 2} } {\paren {-1}^{n + 1} 4 \sqrt {\pi n} \paren {\frac n {\pi e} }^{2 n} } } 8 x^2
      | c = Asymptotic Formula for Bernoulli Numbers
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\frac {\paren {n + 1}^2} {\paren {2 n + 1} \paren {n + 1} } \sqrt {\frac {n + 1} n } \paren {\frac {n + 1} n}^{2 n} } \frac 8 {\pi^2 e^2} x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\paren {\frac {n + 1} n}^{2 n} } \frac 4 {\pi^2 e^2} x^2
      | c =
}}
{{eqn | r = \lim_{n \mathop \to \infty} \size {\paren {\paren {1 + \frac 1 n}^n}^2} \frac 4 {\pi^2 e^2} x^2
      | c =
}}
{{eqn | r = \frac {4 e^2} {\pi^2 e^2} x^2
      | c = {{Defof|Euler's Number as Limit of Sequence}}
}}
{{eqn | r = \frac 4 {\pi^2} x^2
      | c =
}}
{{end-eqn}}
This is less than $1$ {{iff}}:
:$\size x < \dfrac \pi 2$
Hence by the Ratio Test, the series converges for $\size x < \dfrac \pi 2$.
Theorem: Primitive of Constant Multiple of Function

Let $f$ be a real function which is integrable.
Let $c$ be a constant.
Then:
:$\ds \int c \map f x \rd x = c \int \map f x \rd x$

Proof:
From Linear Combination of Primitives:
:$\ds \int \paren {\lambda \map f x + \mu \map g x} \rd x = \lambda \int \map f x \rd x + \mu \int \map g x \rd x$
The result follows by setting $\lambda = c$ and $\mu = 0$.
{{qed}}
Theorem: Primitive of Constant Multiple of Function

Let $f$ be a real function which is integrable.
Let $c$ be a constant.
Then:
:$\ds \int c \map f x \rd x = c \int \map f x \rd x$

Proof:
From Derivative of Constant Multiple:
:$\map {\dfrac \d {\d x} } {c \map f x} = c \map {\dfrac \d {\d x} } {\map f x}$
The result follows from the definition of primitive.
Theorem: Primitive of Pointwise Sum of Functions

Let $f_1, f_2, \ldots, f_n$ be real functions which are integrable.
Then:
:$\ds \int \map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_n} } x \rd x = \int \map {f_1} x \rd x \pm \int \map {f_2} x \rd x \pm \, \cdots \pm \int \map {f_n} x \rd x$

Proof:
Proof by induction:
For all $n \in \N_{> 0}$, let $\map P n$ be the proposition:
:$\ds \int \map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_n} } x \rd x = \int \map {f_1} x \rd x \pm \int \map {f_2} x \rd x \pm \, \cdots \pm \int \map {f_n} x \rd x$
$\map P 1$ is true, as this just says:
:$\ds \int \map {f_1} x \rd x = \int \map {f_1} x \rd x$
=== Basis for the Induction ===
$\map P 2$ is the case:
{{begin-eqn}}
{{eqn | l = \int \map {\paren {f_1 \pm f_2} } x \rd x
      | r = \int \paren {\map {f_1} x \pm \map {f_2} x} \rd x
      | c = {{Defof|Pointwise Addition of Real-Valued Functions}}
}}
{{eqn | r = \int \map {f_1} x \rd x \pm \map {f_2} x \rd x
      | c = Linear Combination of Primitives
}}
{{end-eqn}}
This is our basis for the induction.
=== Induction Hypothesis ===
Now we need to show that, if $\map P k$ is true, where $k \ge 2$, then it logically follows that $\map P {k + 1}$ is true.
So this is our induction hypothesis:
:$\ds \int \map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_k} } x \rd x = \int \map {f_1} x \rd x \pm \int \map {f_2} x \rd x \pm \, \cdots \pm \int \map {f_k} x \rd x$
Then we need to show:
:$\ds \int \map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_{k + 1} } } x \rd x = \int \map {f_1} x \rd x \pm \int \map {f_2} x \rd x \pm \, \cdots \pm \int \map {f_{k + 1} } x \rd x$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | o = 
      | r = \int \map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_{k + 1} } } x \rd x
      | c = 
}}
{{eqn | r = \int \paren {\map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_k} } x + \map {f_{k + 1} } x} \rd x
      | c = {{Defof|Pointwise Addition of Real-Valued Functions}}
}}
{{eqn | r = \int \map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_k} } x \rd x + \int \map {f_{k + 1} } x \rd x
      | c = Basis for the Induction
}}
{{eqn | r = \int \map {f_1} x \rd x \pm \int \map {f_2} x \rd x \pm \, \cdots \pm \int \map {f_k} x \rd x + \int \map {f_{k + 1} } x \rd x
      | c = Induction Hypothesis
}}
{{end-eqn}}
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall n \in \N: \ds \int \map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_n} } x \rd x = \int \map {f_1} x \rd x \pm \int \map {f_2} x \rd x \pm \, \cdots \pm \int \map {f_n} x \rd x$
{{qed}}
Theorem: Primitive of Pointwise Sum of Functions

Let $f_1, f_2, \ldots, f_n$ be real functions which are integrable.
Then:
:$\ds \int \map {\paren {f_1 \pm f_2 \pm \, \cdots \pm f_n} } x \rd x = \int \map {f_1} x \rd x \pm \int \map {f_2} x \rd x \pm \, \cdots \pm \int \map {f_n} x \rd x$

Proof:
From Sum Rule for Derivatives:
:$\ds \map {\dfrac \d {\d x} } {\sum_{i \mathop = 1}^n \map {f_i} x} = \sum_{i \mathop = 1}^n \map {\dfrac \d {\d x} } {\map {f_i} x}$
The result follows by definition of primitive.
{{qed}}
Theorem: Hurwitz's Theorem (Number Theory)

Let $\xi$ be an irrational number.
Then there are infinitely many relatively prime integers $p, q \in \Z$ such that:
:$\size {\xi - \dfrac p q} < \dfrac 1 {\sqrt 5 \, q^2}$

Proof:
=== Lemma 1 ===
{{:Hurwitz's Theorem (Number Theory)/Lemma 1}}{{qed|lemma}}
Theorem: Primitive of Function of Constant Multiple

Let $f$ be a real function which is integrable.
Let $c$ be a constant.
Then:
:$\ds \int \map f {c x} \rd x = \frac 1 c \int \map f u \d u$
where $u = c x$.

Proof:
Let $u = c x$.
By {{Corollary|Derivative of Identity Function}}:
:$\dfrac {\d u} {\d x} = c$
Thus:
{{begin-eqn}}
{{eqn | l = \int \map f {c x} \rd x
      | r = \int \frac {\map f u} c \rd u
      | c = Primitive of Composite Function
}}
{{eqn | r = \frac 1 c \int \map f u \rd u
      | c = Primitive of Constant Multiple of Function
}}
{{end-eqn}}
{{qed}}