avewright/proofwiki-math huggingface dataset:
Theorem: Hyperbolic Cosine of Sum

:$\map \cosh {a + b} = \cosh a \cosh b + \sinh a \sinh b$

Proof:
{{begin-eqn}}
{{eqn | r = \cosh a \cosh b + \sinh a \sinh b
      | o = 
      | c = 
}}
{{eqn | r = \frac {e^a + e^{-a} } 2 \frac {e^b + e^{-b} } 2 + \frac {e^a - e^{-a} } 2 \frac {e^b - e^{-b} } 2
      | c = {{Defof|Hyperbolic Sine}} and {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \frac {e^{a + b} + e^{-a + b} + e^{a + b} + e^{-a - b} } 4 
      | c = Exponential of Sum
}}
{{eqn | o = 
      | ro= +
      | r = \frac {e^{a + b} - e^{-a + b} - e^{a - b} + e^{-a - b} } 4
      | c = 
}}
{{eqn | r = \frac {2 e^{a + b} + 2 e^{-\paren {a + b} } } 4
      | c = 
}}
{{eqn | r = \frac {e^{a + b} + e^{-\paren {a + b} } } 2
      | c = 
}}
{{eqn | r = \map \cosh {a + b}
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Tangent of Sum

:$\map \tanh {a + b} = \dfrac {\tanh a + \tanh b} {1 + \tanh a \tanh b}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \tanh {a + b}
      | r = \frac {\map \sinh {a + b} } {\map \cosh {a + b} }
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{eqn | r = \frac {\sinh a \cosh b + \cosh a \sinh b} {\cosh a \cosh b + \sinh a \sinh b}
      | c = Hyperbolic Sine of Sum and Hyperbolic Cosine of Sum
}}
{{eqn | r = \frac {\frac {\sinh a} {\cosh a} + \frac {\sinh b} {\cosh b} } {1 + \frac {\sinh a \sinh b} {\cosh a \cosh b} }
      | c = dividing the top and bottom by $\cosh a \cosh b$
}}
{{eqn | r = \frac {\tanh a + \tanh b} {1 + \tanh a \tanh b}
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Cotangent of Sum

:$\map \coth {a + b} = \dfrac {\coth a \coth b + 1} {\coth b + \coth a}$

Proof:
{{begin-eqn}}
{{eqn | l = \map \coth {a + b}
      | r = \frac {\map \cosh {a + b} } {\map \sinh {a + b} }
      | c = {{Defof|Hyperbolic Cotangent|index = 2}}
}}
{{eqn | r = \frac {\cosh a \cosh b + \sinh a \sinh b} {\sinh a \cosh b + \cosh a \sinh b}
      | c = Hyperbolic Sine of Sum and Hyperbolic Cosine of Sum
}}
{{eqn | r = \frac {\frac {\cosh a \cosh b} {\sinh a \sinh b} + 1} {\frac {\cosh b} {\sinh b} + \frac {\cosh a} {\sinh a} }
      | c = dividing the numerator and denominator by $\sinh a \sinh b$
}}
{{eqn | r = \frac {\coth a \coth b + 1} {\coth b + \coth a}
      | c = {{Defof|Hyperbolic Cotangent|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Double Angle Formulas/Hyperbolic Sine

:$\sinh 2 x = 2 \sinh x \cosh x$

Proof:
{{begin-eqn}}
{{eqn | l = \sinh 2 x
      | r = \map \sinh {x + x}
}}
{{eqn | r = \sinh x \cosh x + \cosh x \sinh x
      | c = Hyperbolic Sine of Sum
}}
{{eqn | r = 2 \sinh x \cosh x
}}
{{end-eqn}}
{{qed}}
Theorem: Double Angle Formulas/Hyperbolic Sine

:$\sinh 2 x = 2 \sinh x \cosh x$

Proof:
{{begin-eqn}}
{{eqn	| l = \sinh 2 x
	| r = \frac 1 2 \paren {e^{2 x} - e^{-2 x} }
	| c = {{Defof|Hyperbolic Sine}}
}}
{{eqn	| r = \frac 1 2 \paren {e^x + e^{-x} } \paren {e^x - e^{-x} }
	| c = Difference of Two Squares
}}
{{eqn	| r = 2 \paren {\frac{e^x + e^{-x} } 2 \cdot \frac {e^x - e^{-x} } 2}
}}
{{eqn	| r = 2 \sinh x \cosh x
	| c = {{Defof|Hyperbolic Sine}}, {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Double Angle Formulas/Hyperbolic Sine

:$\sinh 2 x = 2 \sinh x \cosh x$

Proof:
{{begin-eqn}}
{{eqn	| l = \sinh 2 x
	| r = -i \sin 2 i x
	| c = Hyperbolic Sine in terms of Sine
}}
{{eqn	| r = -2 i \sin i x \cos i x
	| c = Double Angle Formula for Sine
}}
{{eqn	| r = 2 \sinh x \cosh x
	| c = Hyperbolic Sine in terms of Sine, Hyperbolic Cosine in terms of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Double Angle Formulas/Hyperbolic Cosine

:$\cosh 2 x = \cosh^2 x + \sinh^2 x$

Proof:
{{begin-eqn}}
{{eqn | l = \cosh 2 x
      | r = \map \cosh {x + x}
}}
{{eqn | r = \cosh x \cosh x + \sinh x \sinh x
      | c = Hyperbolic Cosine of Sum
}}
{{eqn | r = \cosh^2 x + \sinh^2 x
}}
{{end-eqn}}
{{qed}}
Theorem: Double Angle Formulas/Hyperbolic Tangent

: $\tanh 2 x = \dfrac {2 \tanh x} {1 + \tanh^2 x}$

Proof:
{{begin-eqn}}
{{eqn | l = \tanh 2 x
      | r = \frac {\sinh 2 x} {\cosh 2 x}
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{eqn | r = \frac {2 \cosh x \sinh x} {\cosh^2 x + \sinh^2 x}
      | c = Double Angle Formula for Hyperbolic Sine and Double Angle Formula for Hyperbolic Cosine
}}
{{eqn | r = \frac {\frac {2 \cosh x \sinh x} {\cosh^2 x} } {\frac {\cosh^2 x + \sinh^2 x} {\cosh^2 x} }
      | c = dividing top and bottom by $\cosh^2 x$
}}
{{eqn | r = \frac {2 \tanh x} {1 + \tanh^2 x}
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Double Angle Formulas/Hyperbolic Tangent

: $\tanh 2 x = \dfrac {2 \tanh x} {1 + \tanh^2 x}$

Proof:
{{begin-eqn}}
{{eqn | l = \tanh 2 x
      | r = \tanh \left({x + x}\right)
}}
{{eqn | r = \frac {\tanh x + \tanh x} {1 + \tanh x \tanh x}
      | c = Hyperbolic Tangent of Sum
}}
{{eqn | r = \frac {2 \tanh x} {1 + \tanh^2 x}
}}
{{end-eqn}}
{{qed}}
Theorem: Double Angle Formulas/Hyperbolic Tangent

: $\tanh 2 x = \dfrac {2 \tanh x} {1 + \tanh^2 x}$

Proof:
Starting from the right, we have
{{begin-eqn}}
{{eqn | l = \dfrac {2 \tanh x} {1 + \tanh^2 x}
      | r = \dfrac {2 \paren {\dfrac {e^x - e^{-x} } {e^x + e^{-x} } } } {1 + \paren {\dfrac{e^x - e^{-x} } {e^x + e^{-x} } }^2}
      | c = {{Defof|Hyperbolic Tangent|index = 1}}
}}
{{eqn | r = \dfrac {2 \paren {e^x + e^{-x} } \paren {e^x - e^{-x} } } {\paren {e^x + e^{-x} }^2 + \paren {e^x - e^{-x} }^2}
      | c = multiplying both numerator and denominator by $\paren {e^x + e^{-x} }^2$
}}
{{eqn | r = \dfrac {2 \paren {e^{2 x} - e^{-2 x} } } {e^{2 x} + 2 + e^{-2 x} + e^{2 x} - 2 + e^{-2 x} }
      | c = Difference of Two Squares, Square of Sum, Square of Difference
}}
{{eqn | r = \dfrac {2 \paren {e^{2 x} - e^{-2 x} } } {2 e^{2 x} + 2 e^{-2 x} }
      | c = simplifying
}}
{{eqn | r = \dfrac {e^{2 x} - e^{-2 x} } {e^{2 x} + e^{-2 x} }
      | c = simplifying
}}
{{eqn | r = \tanh {2 x}
      | c = {{Defof|Hyperbolic Tangent|index = 1}}
}}
{{end-eqn}}
{{qed}}
Theorem: Half Angle Formulas/Hyperbolic Sine

{{begin-eqn}}
{{eqn | l = \sinh \frac x 2
      | r = +\sqrt {\frac {\cosh x - 1} 2}
      | c = for $x \ge 0$
}}
{{eqn | l = \sinh \frac x 2
      | r = -\sqrt {\dfrac {\cosh x - 1} 2}
      | c = for $x \le 0$
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \cosh x
      | r = 1 + 2 \ \sinh^2 \frac x 2
      | c = {{Corollary|Double Angle Formula for Hyperbolic Cosine|2}}
}}
{{eqn | ll= \leadsto
      | l = 2 \ \sinh^2 \frac x 2
      | r = \cosh x - 1
}}
{{eqn | ll= \leadsto
      | l = \sinh \frac x2
      | r = \pm \sqrt {\frac {\cosh x - 1} 2}
}}
{{end-eqn}}
We also have that:
:when $x \ge 0$, $\sinh x \ge 0$
:when $x \le 0$, $\sinh x \le 0$.
{{qed}}
Theorem: Half Angle Formulas/Hyperbolic Cosine

:$\cosh \dfrac x 2 = +\sqrt {\dfrac {\cosh x + 1} 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \cosh x
      | r = 2 \cosh^2 \frac x 2 - 1
      | c = {{Corollary|Double Angle Formula for Hyperbolic Cosine|1}}
}}
{{eqn | ll= \leadsto
      | l = 2 \cosh^2 \frac x 2
      | r = \cosh x + 1
}}
{{eqn | ll= \leadsto
      | l = \cosh \frac x 2
      | r = \pm \sqrt {\frac {\cosh x + 1} 2}
}}
{{end-eqn}}
As $\forall x \in \R: \cosh x > 0$, the result follows.
{{qed}}
Theorem: Half Angle Formulas/Hyperbolic Tangent

{{begin-eqn}}
{{eqn | l = \tanh \frac x 2
      | r = +\sqrt {\frac {\cosh x - 1} {\cosh x + 1} }
      | c = for $x \ge 1$
}}
{{eqn | l = \tanh \frac x 2
      | r = -\sqrt {\frac {\cosh x - 1} {\cosh x + 1} }
      | c = for $x \le 1$
}}
{{end-eqn}}

Proof:
{{begin-eqn}}
{{eqn | l = \tanh \frac x 2
      | r = \frac {\sinh \frac x 2} {\cosh \frac x 2}
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{eqn | r = \frac {\pm \sqrt {\frac {\cosh x - 1} 2} } {\pm \sqrt {\frac {\cosh x + 1} 2} }
      | c = Half Angle Formula for Hyperbolic Sine and Half Angle Formula for Hyperbolic Cosine
}}
{{eqn | r = \pm \sqrt {\frac {\cosh x - 1} {\cosh x + 1} }
}}
{{end-eqn}}
We also have that:
:when $x \ge 0$, $\tanh \dfrac x 2 \ge 0$
:when $x \le 0$, $\tanh \dfrac x 2 \le 0$.
{{qed}}
Theorem: Half Angle Formula for Hyperbolic Tangent/Corollary 1

:$\tanh \dfrac x 2 = \dfrac {\sinh x} {\cosh x + 1}$

Proof:
{{begin-eqn}}
{{eqn | l = \tanh \frac x 2
      | r = \pm \sqrt {\frac {\cosh x - 1} {\cosh x + 1} }
      | c = Half Angle Formula for Hyperbolic Tangent
}}
{{eqn | r = \pm \sqrt {\frac {\paren {\cosh x - 1} \paren {\cosh x + 1} } {\paren {\cosh x + 1}^2} }
      | c = multiplying top and bottom by $\sqrt {\cosh x + 1}$
}}
{{eqn | r = \pm \sqrt {\frac {\cosh x - 1} {\paren {\cosh x + 1}^2} }
      | c = Difference of Two Squares
}}
{{eqn | r = \pm \sqrt {\frac {\sinh^2 x} {\paren {\cosh x + 1}^2} }
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = \pm \frac {\sinh x} {\cosh x + 1}
}}
{{end-eqn}}
Since $\cosh x > 0$, it follows that $\cosh x + 1 > 0$.
We also have that:
:when $x \ge 0$, $\tanh \dfrac x 2 \ge 0$ and $\sinh x \ge 0$
:when $x \le 0$, $\tanh \dfrac x 2 \le 0$ and $\sinh x \le 0$.
Thus:
:$\tanh \dfrac x 2 = \dfrac {\sinh x} {\cosh x + 1}$
{{qed}}
Theorem: Half Angle Formula for Hyperbolic Tangent/Corollary 2

For $x \ne 0$:
:$\tanh \dfrac x 2 = \dfrac {\cosh x - 1} {\sinh x}$

Proof:
{{begin-eqn}}
{{eqn | l = \tanh \frac x 2
      | r = \pm \sqrt {\frac {\cosh x - 1} {\cosh x + 1} }
      | c = Half Angle Formula for Hyperbolic Tangent
}}
{{eqn | r = \pm \sqrt {\frac {\paren {\cosh x - 1}^2} {\paren {\cosh x + 1} \paren {\cosh x - 1} } }
      | c = multiplying numerator and denominator by $\sqrt {\cosh x - 1}$
}}
{{eqn | r = \pm \sqrt {\frac {\paren {\cosh x - 1}^2} {\cosh^2 x - 1} }
      | c = Difference of Two Squares
}}
{{eqn | r = \pm \sqrt {\frac {\paren {\cosh x - 1}^2} {\sinh^2 x} }
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = \pm \frac {\cosh x - 1} {\sinh x}
}}
{{end-eqn}}
Since $\cosh x \ge 1$, it follows that $\cosh x - 1 \ge 0$, with equality happening at $x = 0$.
We also have that:
:when $x > 0$, $\tanh \dfrac x 2 > 0$ and $\sinh x > 0$
:when $x < 0$, $\tanh \dfrac x 2 < 0$ and $\sinh x < 0$.
Thus:
:$\tanh \dfrac x 2 = \dfrac {\cosh x - 1} {\sinh x}$
{{qed}}
Theorem: Triple Angle Formulas/Hyperbolic Sine

:$\sinh 3 x = 3 \sinh x + 4 \sinh^3 x$

Proof:
{{begin-eqn}}
{{eqn | l = \sinh {3 x}
      | r = \map \sinh {2 x + x}
}}
{{eqn | r = \sinh 2 x \cosh x + \cosh 2 x \sinh x
      | c = Hyperbolic Sine of Sum
}}
{{eqn | r = \paren {2 \sinh x \cosh x} \cosh x + \cosh 2 x \sinh x
      | c = Double Angle Formula for Hyperbolic Sine
}}
{{eqn | r = \paren {2 \sinh x \cosh x} \cosh x + \paren {\cosh^2 x + \sinh^2 x} \sinh x
      | c = Double Angle Formula for Hyperbolic Cosine
}}
{{eqn | r = 2 \sinh x \cosh^2 x + \cosh^2 x \sinh x + \sinh^3 x
      | c = multiplying out
}}
{{eqn | r = 2 \sinh x \paren {1 + \sinh^2 x} + \paren {1 + \sinh^2 x} \sinh x + \sinh^3 x
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = 2 \sinh x + 2 \sinh^3 x + \sinh x + \sinh^3 x + \sinh^3 x
      | c = multiplying out
}}
{{eqn | r = 3 \sinh x + 4 \sinh^3 x
      | c = gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Triple Angle Formulas/Hyperbolic Cosine

: $\cosh 3 x = 4 \cosh^3 x - 3 \cosh x$

Proof:
{{begin-eqn}}
{{eqn | l = \cosh 3 x
      | r = \cosh \paren {2 x + x}
}}
{{eqn | r = \cosh 2 x \cosh x + \sinh 2 x \sinh x
      | c = Hyperbolic Cosine of Sum
}}
{{eqn | r = \paren {\cosh^2 x + \sinh^2 x} \cosh x + \sinh 2 x \sinh x
      | c = Double Angle Formula for Hyperbolic Cosine
}}
{{eqn | r = \paren {\cosh^2 x + \sinh^2 x} \cosh x + \paren {2 \sinh x \cosh x} \sinh x
      | c = Double Angle Formula for Hyperbolic Sine
}}
{{eqn | r = \cosh^3 x + \sinh^2 x \cosh x + 2 \sinh^2 x \cosh x
      | c = multiplying out
}}
{{eqn | r = \cosh^3 x + \paren {\cosh^2 x - 1} \cosh x + 2 \paren {\cosh^2 x - 1} \cosh x
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = \cosh^3 x + \cosh^3 x - \cosh x + 2 \cosh^3 x - 2 \cosh x
      | c = multiplying out
}}
{{eqn | r = 4 \cosh^3 x - 3 \cosh x
      | c = gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Triple Angle Formulas/Hyperbolic Tangent

:$\tanh {3 x} = \dfrac {3 \tanh x + \tanh^3 x} {1 + 3 \tanh^2 x}$

Proof:
{{begin-eqn}}
{{eqn | l = \tanh {3 x}
      | r = \frac {\sinh {3 x} } {\cosh {3 x} }
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{eqn | r = \frac {3 \sinh x + 4 \sinh^3 x} {\cosh {3 x} }
      | c = Triple Angle Formula for Hyperbolic Sine
}}
{{eqn | r = \frac {3 \sinh x + 4 \sinh^3 x} {4 \cosh^3 x - 3 \cosh x}
      | c = Triple Angle Formula for Hyperbolic Cosine
}}
{{eqn | r = \frac {3 \sinh x + 4 \sinh^3 x} {4 \cosh^3 x - 3 \cosh x} \frac {\paren {1 / \cosh^3 x} } {\paren {1 / \cosh^3 x} }
      | c = 
}}
{{eqn | r = \frac {\frac {3 \tanh x} {\cosh^2 x} + 4 \tanh^3 x} {4 - \frac {3 \cosh x} {\cosh^3 x} }
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{eqn | r = \frac {3 \tanh x \sech^2 x + 4 \tanh^3 x} {4 - 3 \sech^2 x}
      | c = {{Defof|Hyperbolic Secant|index = 2}}
}}
{{eqn | r = \frac {3 \tanh x \paren {1 - \tanh^2 x} + 4 \tanh^3 x} {4 - 3 \paren {1 - \tanh^2 x} }
      | c = Sum of Squares of Hyperbolic Secant and Tangent
}}
{{eqn | r = \frac {3 \tanh x - 3 \tanh^3 x + 4 \tanh^3 x} {4 - 3 + 3 \tanh^2 x}
      | c = multipying out
}}
{{eqn | r = \frac {3 \tanh x + \tanh^3 x} {1 + 3 \tanh^2 x}
      | c = gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Quadruple Angle Formulas/Hyperbolic Sine

:$\sinh 4 x = 8 \sinh^3 x \cosh x + 4 \sinh x \cosh x$

Proof:
{{begin-eqn}}
{{eqn | l = \sinh 4 x
      | r = \map \sinh {3 x + x}
}}
{{eqn | r = \sinh 3 x \cosh x + \cosh 3 x \sinh x
      | c = Hyperbolic Sine of Sum
}}
{{eqn | r = \paren {3 \sinh x + 4 \sinh^3 x} \cosh x + \cosh 3 x \sinh x
      | c = Triple Angle Formula for Hyperbolic Sine
}}
{{eqn | r = \paren {3 \sinh x + 4 \sinh^3 x} \cosh x + \paren {4 \cosh^3 x - 3 \cosh x} \sinh x
      | c = Triple Angle Formula for Hyperbolic Cosine
}}
{{eqn | r = 3 \sinh x \cosh x + 4 \sinh^3 x \cosh x + 4 \cosh^3 x \sinh x - 3 \cosh x \sinh x
      | c = multiplying out
}}
{{eqn | r = 3 \sinh x \cosh x + 4 \sinh^3 x \cosh x
      | c = 
}}
{{eqn | o = 
      | ro= +
      | r = 4 \cosh x \paren {1 + \sinh^2 x} \sinh x - 3 \cosh x \sinh x
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = 8 \sinh^3 x \cosh x + 4 \sinh x \cosh x
      | c = multiplying out and gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Quadruple Angle Formulas/Hyperbolic Cosine

:$\cosh 4 x = 8 \cosh^4 x - 8 \cosh^2 x + 1$

Proof:
{{begin-eqn}}
{{eqn | l = \cosh 4 x
      | r = \map \cosh {2 x + 2 x}
}}
{{eqn | r = \cosh 2 x \cosh 2 x + \sinh 2 x \sinh 2 x
      | c = Hyperbolic Cosine of Sum
}}
{{eqn | r = \paren {\cosh^2 x + \sinh^2 x} \paren {\cosh^2 x + \sinh^2 x} + \paren {2 \sinh x \cosh x} \paren {2 \sinh x \cosh x}
      | c = Double Angle Formulas
}}
{{eqn | r = \cosh^4 x + 2 \cosh^2 x \sinh^2 x + \sinh^4 x + 4 \cosh^2 x \sinh^2 x
      | c = multiplying out
}}
{{eqn | r = \cosh^4 x + 2 \cosh^2 x \paren {\cosh^2 x - 1} + \paren {\cosh^2 x - 1}^2 + 4 \cosh^2 x \paren {\cosh^2 x - 1}
      | c = Difference of Squares of Hyperbolic Cosine and Sine
}}
{{eqn | r = 8 \cosh^4 x - 8 \cosh^2 x + 1
      | c = multiplying out and gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Quadruple Angle Formulas/Hyperbolic Tangent

:$\tanh 4 x = \dfrac {4 \tanh x + 4 \tanh^3 x} {1 + 6 \tanh^2 x + \tanh^4 x}$

Proof:
{{begin-eqn}}
{{eqn | l = \tanh 4 x)
      | r = \frac {\sinh 4 x} {\cosh 4 x}
      | c = {{Defof|Hyperbolic Tangent|index = 2}}
}}
{{eqn | r = \frac {8 \sinh^3 x \cosh x + 4 \sinh x \cosh x} {\cosh 4 x}
      | c = Quadruple Angle Formula for Hyperbolic Sine
}}
{{eqn | r = \frac {8 \sinh^3 x \cosh x + 4 \sinh x \cosh x} {8 \cosh^4 x - 8 \cosh^2 x + 1}
      | c = Quadruple Angle Formula for Hyperbolic Cosine
}}
{{eqn | r = \frac {8 \tanh^3 x + 4 \frac {\tanh x} {\cosh^2 x} } {8 - \frac 8 {\cosh^2 x} + \frac 1 {\cosh^4 x} }
      | c = dividing top and bottom by $\cosh^4 x$
}}
{{eqn | r = \frac {8 \tanh^3 x + 4 \tanh x \sech^2 x} {8 - 8 \sech^2 x + \sech^4 x}
      | c = {{Defof|Hyperbolic Secant|index = 2}}
}}
{{eqn | r = \frac {8 \tanh^3 x + 4 \tanh x \paren {1 - \tanh^2 x} } {8 - 8 \paren {1 - \tanh^2 x} + \paren {1 - \tanh^2 x}^2}
      | c = Sum of Squares of Hyperbolic Secant and Tangent
}}
{{eqn | r = \frac {4 \tanh^3 x + 4 \tanh x} {1 + 6 \tanh^2 x + \tanh^4 x}
      | c = multiplying out and gathering terms
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Sine Squared

:$\sinh^2 x = \dfrac {\cosh 2 x - 1} 2$

Proof:
{{begin-eqn}}
{{eqn | l = 2 \sinh^2 x + 1
      | r = \cosh 2 x
      | c = {{Corollary|Double Angle Formula for Hyperbolic Cosine|2}}
}}
{{eqn | ll= \leadsto
      | l = \sinh^2 x
      | r = \frac {\cosh 2 x - 1} 2
      | c = solving for $\sinh^2 x$
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Sine Squared

:$\sinh^2 x = \dfrac {\cosh 2 x - 1} 2$

Proof:
{{begin-eqn}}
{{eqn	| l = \sinh^2 x
	| r = \paren {\frac {e^x - e^{-x} } 2}^2
	| c = {{Defof|Hyperbolic Sine}}
}}
{{eqn	| r = \frac 1 4 \paren {e^{2 x} + e^{-2 x} - 2}
	| c = multiplying out
}}
{{eqn	| r = \frac 1 2 \paren {\dfrac {e^{2 x} + e^{-2 x} } 2 - 1}
	| c = rearranging
}}
{{eqn	| r = \frac {\cosh 2 x - 1} 2
	| c = {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine Squared

:$\cosh^2 x = \dfrac {\cosh 2 x + 1} 2$

Proof:
{{begin-eqn}}
{{eqn | l = 2 \cosh^2 x - 1
      | r = \cosh 2 x
      | c = {{Corollary|Double Angle Formula for Hyperbolic Cosine|1}}
}}
{{eqn | l = \cosh^2 x
      | r = \frac {\cosh 2 x + 1} 2
      | c = solving for $\cosh^2 x$
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine Squared

:$\cosh^2 x = \dfrac {\cosh 2 x + 1} 2$

Proof:
{{begin-eqn}}
{{eqn | l = \cosh^2 x
      | r = \frac 1 4 \paren {e^x + e^{-x} }^2
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \frac {e^{2 x} + e^{-2 x} + 2} 4
}}
{{eqn | r = \frac {\cosh 2 x + 1} 2
      | c = {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine Squared

:$\cosh^2 x = \dfrac {\cosh 2 x + 1} 2$

Proof:
{{begin-eqn}}
{{eqn	| l = \cosh^2 x
	| r = \cos^2 i x
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn	| r = \frac {\map \cos {2 i x} + 1} 2
	| c = Square of Cosine
}}
{{eqn	| r = \frac {\cosh 2 x + 1} 2
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Sine Cubed

:$\sinh^3 x = \dfrac {\sinh 3 x - 3 \sinh x} 4$

Proof:
{{begin-eqn}}
{{eqn | l = \sinh 3 x
      | r = 3 \sinh x + 4 \sinh^3 x
      | c = Triple Angle Formula for Hyperbolic Sine
}}
{{eqn | ll= \leadsto
      | l = 4 \sinh^3 x
      | r = \sinh 3 x - 3 \sinh x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \sinh^3 x
      | r = \frac {\sinh 3 x - 3 \sinh x} 4
      | c = dividing both sides by $4$
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine Cubed

:$\cosh^3 x = \dfrac {\cosh 3 x + 3 \cosh x} 4$

Proof:
{{begin-eqn}}
{{eqn | l = \cosh 3 x
      | r = 4 \cosh^3 x - 3 \cosh x
      | c = Triple Angle Formula for Hyperbolic Cosine
}}
{{eqn | ll= \leadsto
      | l = 4 \cosh^3 x
      | r = \cosh 3 x + 3 \cosh x
      | c = rearranging
}}
{{eqn | ll= \leadsto
      | l = \cosh^3 x
      | r = \dfrac {\cosh 3 x + 3 \cosh x} 4
      | c = dividing both sides by $4$
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine Cubed

:$\cosh^3 x = \dfrac {\cosh 3 x + 3 \cosh x} 4$

Proof:
{{begin-eqn}}
{{eqn	| l = \cosh^3 x
	| r = \frac 1 {2^3} \paren {e^x + e^{-x} }^3
	| c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn	| r = \frac 1 8 \paren {e^{3x} + e^{-3x} + 3e^{x} + 3e^{-x} }
}}
{{eqn	| r = \frac 1 4 \paren {\frac{ e^{3x} + e^{-3x} } 2} + \frac 3 4 \paren {\frac{e^{x} + e^{-x} } 2}
}}
{{eqn	| r = \frac {\cosh 3x} 4 + \frac {3 \cosh x} 4
	| c = {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine Cubed

:$\cosh^3 x = \dfrac {\cosh 3 x + 3 \cosh x} 4$

Proof:
{{begin-eqn}}
{{eqn	| l = \cosh^3 x
	| r = \cos^3 i x
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn	| r = \frac {\map \cos {3 i x} + 3 \cos i x} 4
	| c = Cube of Cosine
}}
{{eqn	| r = \frac {\cosh 3 x + 3 \cosh x} 4
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Sine to 4th

:$\sinh^4 x = \dfrac {3 - 4 \cosh 2 x + \cosh 4 x} 8$

Proof:
{{begin-eqn}}
{{eqn|l = \sinh^4 x
     |r = \left({\sinh^2 x}\right)^2
}}
{{eqn|r = \left({\frac {\cosh 2 x - 1} 2}\right)^2
     |c = Square of Hyperbolic Sine
}}
{{eqn|r = \frac {\cosh^2 2 x - 2 \cosh 2 x + 1} 4
     |c = multiplying out
}}
{{eqn|r = \frac {\frac {\cosh 4 x + 1} 2 - 2 \cosh 2 x + 1} 4
     |c = Square of Hyperbolic Cosine
}}
{{eqn|r = \frac {\cosh 4 x + 1 - 4 \cosh 2 x + 2} 8
     |c = multiplying top and bottom by $2$
}}
{{eqn|r = \frac {3 - 4 \cosh 2 x + \cosh 4 x} 8
     |c = rearrangement
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine to 4th

:$\cosh^4 x = \dfrac {3 + 4 \cosh 2 x + \cosh 4 x} 8$

Proof:
{{begin-eqn}}
{{eqn | l = \cosh 4 x
      | r = \paren {\cosh^2 x}^2
}}
{{eqn | r = \paren {\frac {\cosh 2 x + 1} 2}^2
      | c = Square of Hyperbolic Cosine
}}
{{eqn | r = \frac {\cosh^2 2 x + 2 \cosh 2 x + 1} 4
      | c = multiplying out
}}
{{eqn | r = \frac {\frac {\cosh 4 x + 1} 2 + 2 \cosh 2 x + 1} 4
      | c = Square of Hyperbolic Cosine
}}
{{eqn | r = \frac {\cosh 4 x + 1 + 4 \cosh 2 x + 2} 8
      | c = multiplying top and bottom by $2$
}}
{{eqn | r = \frac {3 + 4 \cosh 2 x + \cosh 4 x} 8
      | c = rearrangement
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine to 4th

:$\cosh^4 x = \dfrac {3 + 4 \cosh 2 x + \cosh 4 x} 8$

Proof:
{{begin-eqn}}
{{eqn	| l = \cosh^4 x
	| r = \frac 1 {2^4}\left(e^{x} + e^{-x}\right)^4
	| c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn	| r = \frac 1 {16} \left({e^{4 x} + 4 e^{2 x} + 6 e^{0 x} + 4 e^{-2 x} + e^{-4 x} }\right)
	| c = Binomial Theorem
}}
{{eqn	| r = \frac 1 8 \left({\frac{e^{4 x} + e^{-4 x} } 2}\right) + \frac 4 8 \left({\frac{e^{2 x} + e^{-2 x} } 2 }\right) + \frac 6 {16}
}}
{{eqn	| r = \frac {3 + 4 \cosh 2 x + \cosh 4 x} 8
	| c = {{Defof|Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Theorem: Power Reduction Formulas/Hyperbolic Cosine to 4th

:$\cosh^4 x = \dfrac {3 + 4 \cosh 2 x + \cosh 4 x} 8$

Proof:
{{begin-eqn}}
{{eqn	| l = \cosh^4 x
	| r = \cos^4 i x
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{eqn	| r = \frac {3 + 4 \cos \paren {2 i x} + \cos \paren {4 i x} } 8
	| c = Fourth Power of Cosine
}}
{{eqn	| r = \frac {3 + 4 \cosh 2 x + \cosh 4 x} 8
	| c = Hyperbolic Cosine in terms of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Prosthaphaeresis Formulas/Hyperbolic Sine plus Hyperbolic Sine

:$\sinh x + \sinh y = 2 \map \sinh {\dfrac {x + y} 2} \map \cosh {\dfrac {x - y} 2}$

Proof:
{{begin-eqn}}
{{eqn | o = 
      | r = 2 \map \sinh {\frac {x + y} 2} \map \cosh {\frac {x - y} 2}
      | c = 
}}
{{eqn | r = 2 \frac {\map \sinh {\dfrac {x + y} 2 + \dfrac {x - y} 2} + \map \sinh {\dfrac {x + y} 2 - \dfrac {x - y} 2} } 2
      | c = Werner Formula for Hyperbolic Sine by Hyperbolic Cosine
}}
{{eqn | r = \sinh \frac {2 x} 2 + \sinh \frac {2 y} 2
      | c = 
}}
{{eqn | r = \sinh x + \sinh y
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Prosthaphaeresis Formulas/Hyperbolic Sine minus Hyperbolic Sine

:$\sinh x - \sinh y = 2 \map \cosh {\dfrac {x + y} 2} \map \sinh {\dfrac {x - y} 2}$

Proof:
{{begin-eqn}}
{{eqn | o =
      | r = 2 \map \cosh {\frac {x + y} 2} \map \sinh {\frac {x - y} 2}
      | c = 
}}
{{eqn | r = 2 \frac {\map \sinh {\dfrac {x - y} 2 + \dfrac {x + y} 2} + \map \sinh {\dfrac {x - y} 2 - \dfrac {x + y} 2} } 2
      | c = Werner Formula for Hyperbolic Sine by Hyperbolic Cosine
}}
{{eqn | r = \sinh \frac {2 x} 2 + \map \sinh {-\frac {2 y} 2}
      | c = 
}}
{{eqn | r = \sinh \frac {2 x} 2 - \sinh \frac {2 y} 2
      | c = Hyperbolic Sine Function is Odd
}}
{{eqn | r = \sinh x - \sinh y
      | c = 
}}
{{end-eqn}}
{{qed}}