avewright/proofwiki-math huggingface dataset:
Theorem: Primitive of Power of x by Inverse Hyperbolic Tangent of x over a

:$\ds \int x^m \artanh \frac x a \rd x = \frac {x^{m + 1} } {m + 1} \artanh \frac x a - \frac a {m + 1} \int \frac {x^{m + 1} } {a^2 - x^2} \rd x + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \artanh \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac a {a^2 - x^2}
      | c = Derivative of $\artanh \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \artanh \frac x a \rd x
      | r = \paren {\artanh \frac x a} \paren {\frac {x^{m + 1} } {m + 1} } - \int \paren {\frac {x^{m + 1} } {m + 1} } \paren {\frac a {a^2 - x^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \artanh \frac x a - \frac a {m + 1} \int \frac {x^{m + 1} } {a^2 - x^2} \rd x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Inverse Hyperbolic Cotangent of x over a

:$\ds \int x^m \arcoth \frac x a \rd x = \frac {x^{m + 1} } {m + 1} \arcoth \frac x a - \frac a {m + 1} \int \frac {x^{m + 1} } {a^2 - x^2} \rd x + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arcoth \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-a} {x^2 - a^2}
      | c = Derivative of $\arcoth \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arcoth \frac x a \rd x
      | r = \paren {\arcoth \frac x a} \paren {\frac {x^{m + 1} } {m + 1} } - \int \paren {\frac {x^{m + 1} } {m + 1} } \paren {\frac {-a} {x^2 - a^2} } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arcoth \frac x a - \frac a {m + 1} \int \frac {x^{m + 1} } {a^2 - x^2} \rd x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Inverse Hyperbolic Secant of x over a

:$\ds \int x^m \arsech \frac x a \rd x = \dfrac {x^{m + 1} } {m + 1} \arsech \dfrac x a + \dfrac a {m + 1} \int \dfrac {x^m} {\sqrt {a^2 - x^2} } \rd x + C$

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\d v} {\d x} \rd x = u v - \int v \frac {\d u} {\d x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arsech \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac {-a} {x \sqrt {a^2 - x^2} }
      | c = Derivative of $\arsech \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\d v} {\d x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int x^m \arsech \frac x a \rd x
      | r = \paren {\arsech \frac x a} \paren {\frac {x^{m + 1} } {m + 1} } - \int \paren {\frac {x^{m + 1} } {m + 1} } \paren {\frac {-a} {x \sqrt {a^2 - x^2} } } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = \frac {x^{m + 1} } {m + 1} \arsech \frac x a + \frac a {m + 1}  \int \frac {x^m} {\sqrt {a^2 - x^2} } \rd x + C
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Power of x by Inverse Hyperbolic Cosecant of x over a

:<nowiki>$\ds \int x^m \arcsch \frac x a \rd x = \begin{cases}
\ds \frac {x^{m + 1} } {m + 1} \arcsch \frac x a + \frac a {m + 1} \int \frac {x^m} {\sqrt {x^2 + a^2} } \rd x + C & : x > 0 \\ \\
\ds \frac {x^{m + 1} } {m + 1} \arcsch \frac x a - \frac a {m + 1} \int \frac {x^m} {\sqrt {x^2 + a^2} } \rd x + C & : x < 0
\end{cases}$</nowiki>

Proof:
With a view to expressing the primitive in the form:
:$\ds \int u \frac {\rd v} {\rd x} \rd x = u v - \int v \frac {\rd u} {\rd x} \rd x$
let:
{{begin-eqn}}
{{eqn | l = u
      | r = \arcsch \frac x a
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\rd u} {\rd x}
      | r = \frac {-a} {\size x \sqrt{a^2 + x^2} }
      | c = Derivative of $\arcsch \dfrac x a$
}}
{{end-eqn}}
and let:
{{begin-eqn}}
{{eqn | l = \frac {\rd v} {\rd x}
      | r = x^m
      | c = 
}}
{{eqn | ll= \leadsto
      | l = v
      | r = \frac {x^{m + 1} } {m + 1}
      | c = Primitive of Power
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int  x^m \arcsch \frac x a \rd x
      | r = \paren {\arcsch \frac x a} \paren {\frac {x^{m + 1} } {m + 1} } - \int \paren {\frac {x^{m + 1} } {m + 1} } \paren {\frac {-a} {\size x \sqrt{a^2 + x^2} } } \rd x + C
      | c = Integration by Parts
}}
{{eqn | r = <nowiki>\begin {cases}
\ds \frac {x^{m + 1} } {m + 1} \arcsch \frac x a + \frac a {m + 1} \int \frac {x^m} {\sqrt {x^2 + a^2} } \rd x + C & : x > 0 \\ \\
\ds \frac {x^{m + 1} } {m + 1} \arcsch \frac x a - \frac a {m + 1} \int \frac {x^m} {\sqrt {x^2 + a^2} } \rd x + C & : x < 0
\end {cases}</nowiki>
      | c = {{Defof|Absolute Value}}
}}
{{end-eqn}}
{{qed}}
Theorem: Hyperbolic Tangent Half-Angle Substitution

:$\ds \int \map F {\sinh x, \cosh x} \rd x = 2 \int \map F {\frac {2 u} {1 - u^2}, \frac {1 + u^2} {1 - u^2} } \frac {\d u} {1 - u^2}$
where $u = \tanh \dfrac x 2$.

Proof:
{{begin-eqn}}
{{eqn | l = u
      | r = \tanh \dfrac x 2
      | c = 
}}
{{eqn | ll= \leadsto
      | l = x
      | r = 2 \tanh^{-1} u
      | c = {{Defof|Inverse Hyperbolic Tangent|subdef = Real|index = 1}}
}}
{{eqn | ll= \leadsto
      | l = \dfrac {\d x} {\d u}
      | r = \dfrac 2 {1 - u^2}
      | c = Derivative of Inverse Hyperbolic Tangent and Derivative of Constant Multiple
}}
{{eqn | l = \sinh x
      | r = \dfrac {2 u} {1 - u^2}
      | c = Hyperbolic Tangent Half-Angle Substitution for Sine
}}
{{eqn | l = \cosh x
      | r = \dfrac {1 + u^2} {1 - u^2}
      | c = Hyperbolic Tangent Half-Angle Substitution for Cosine
}}
{{end-eqn}}
The result follows from Integration by Substitution.
{{qed}}
Theorem: Reciprocal of One Plus Cosine

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

Proof:
{{begin-eqn}}
{{eqn | l = 1 + \cos x
      | r = \cos 0 + \cos x
      | c = Cosine of Zero is One
}}
{{eqn | r = 2 \map \cos {\dfrac {0 + x} 2} \map \cos {\dfrac {0 - x} 2}
      | c = Cosine plus Cosine
}}
{{eqn | r = 2 \map \cos {\dfrac x 2} \map \cos {\dfrac {-x} 2}
      | c = simplifying
}}
{{eqn | r = 2 \map \cos {\dfrac x 2} \map \cos {\dfrac x 2}
      | c = Cosine Function is Even
}}
{{eqn | r = 2 \map {\cos^2} {\frac x 2}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {1 + \cos x}
      | r = \frac 1 2 \map {\sec^2} {\frac x 2}
      | c = {{Defof|Secant Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of One Plus Cosine

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

Proof:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = 2 \cos^2 \frac x 2 - 1
      | c = {{Corollary|Double Angle Formula for Cosine|1}}
}}
{{eqn | ll= \leadstoandfrom
      | l = 1 + \cos x
      | r = 2 \cos^2 \frac x 2
      | c = adding $1$ to both sides
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 {1 + \cos x}
      | r = \frac 1 2 \frac 1 {\cos^2 \frac x 2}
      | c = taking the reciprocal of both sides
}}
{{eqn | r = \frac 1 2 \sec^2 \frac x 2
      | c = {{Defof|Secant Function}}
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of One Plus Cosine

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

Proof:
{{begin-eqn}}
{{eqn	| l = \frac 1 {1 + \cos x} 
	| r = \frac 1 {1 + \frac {1- \tan^2 \frac x 2} {1 + \tan^2 \frac x 2} }
	| c = Tangent Half-Angle Substitution for Cosine
}}
{{eqn	| r = \frac {1 + \tan^2 \frac x 2} 2
	| c = multiplying through $\frac {1 + \tan^2 \frac x 2} {1 + \tan^2 \frac x 2}$
}}
{{eqn	| r = \frac 1 2 \sec^2 \frac x 2
	| c = Difference of Squares of Secant and Tangent
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of One Minus Cosine

:$\dfrac 1 {1 - \cos x} = \dfrac 1 2 \map {\csc^2} {\dfrac x 2}$

Proof:
{{begin-eqn}}
{{eqn | l = 1 - \cos x
      | r = \cos 0 - \cos x
      | c = Cosine of Zero is One
}}
{{eqn | r = -2 \map \sin {\dfrac {0 + x} 2} \map \sin {\dfrac {0 - x} 2}
      | c = Cosine minus Cosine
}}
{{eqn | r = -2 \map \sin {\dfrac x 2} \map \sin {\dfrac {-x} 2}
      | c = simplifying
}}
{{eqn | r = 2 \map \sin {\dfrac x 2} \map \sin {\dfrac x 2}
      | c = Sine Function is Odd
}}
{{eqn | r = 2 \map {\sin^2} {\frac x 2}
      | c = simplifying
}}
{{eqn | ll= \leadsto
      | l = \frac 1 {1 - \cos x}
      | r = \frac 1 2 \map {\csc^2} {\frac x 2}
      | c = {{Defof|Cosecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of One Minus Cosine

:$\dfrac 1 {1 - \cos x} = \dfrac 1 2 \map {\csc^2} {\dfrac x 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \cos x
      | r = 1 - 2 \sin^2 \frac x 2
      | c = {{Corollary|Double Angle Formula for Cosine|2}}
}}
{{eqn | ll= \leadstoandfrom
      | l = 1 - \cos x
      | r = 2 \sin^2 \frac x 2
      | c = rearranging
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 {1 - \cos x}
      | r = \frac 1 2 \frac 1 {\sin^2 \frac x 2}
      | c = taking the reciprocal of both sides
}}
{{eqn | r = \frac 1 2 \csc^2 \frac x 2
      | c = {{Defof|Cosecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of One Minus Cosine

:$\dfrac 1 {1 - \cos x} = \dfrac 1 2 \map {\csc^2} {\dfrac x 2}$

Proof:
{{begin-eqn}}
{{eqn | l = \frac 1 {1 - \cos x}
      | r = \frac 1 {1 - \frac {1 - \map {\tan^2} {\frac x 2} } {1 + \map {\tan^2} {\frac x 2} } }
      | c = Tangent Half-Angle Substitution for Cosine
}}
{{eqn | r = \frac {1 + \map {\tan^2} {\frac x 2} } {1 + \map {\tan^2} {\frac x 2} - 1 + \map {\tan^2} {\frac x 2} }
      | c = multiplying top and bottom by $1 + \map {\tan^2} {\dfrac x 2}$
}}
{{eqn | r = \frac {\map {\sec^2} {\frac x 2} } {2 \map {\tan^2} {\frac x 2} }
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \frac 1 2 \cdot \frac 1 {\map {\cos^2} {\frac x 2} } \cdot \frac {\map {\cos^2} {\frac x 2} } {\map {\sin^2} {\frac x 2} }
      | c = {{Defof|Secant Function}}, {{Defof|Tangent}}
}}
{{eqn | r = \frac 1 {2 \map {\sin^2} {\frac x 2} }
}}
{{eqn | r = \frac 1 2 \map {\csc^2} {\frac x 2}
      | c = {{Defof|Cosecant}}
}}
{{end-eqn}}
{{qed}}
Theorem: Irrationality of Logarithm

Let $a, b \in \N_{>0}$ such that both $\nexists m, n \in \N_{>0}: a^m = b^n$.
Then $\log_b a$ is irrational.

Proof:
{{AimForCont}} $\log_b a$ is rational.
Then:
:$\exists p, q \in \N_{>0} : \log_b a = \dfrac p q$
where $p \perp q$.
Then:
{{begin-eqn}}
{{eqn | l = \log_b a
      | r = \dfrac p q
      | c = 
}}
{{eqn | ll= \leadsto
      | l = b^{\frac p q}
      | r = a
      | c = {{Defof|Real General Logarithm}}
}}
{{eqn | ll= \leadsto
      | l = \sqrt [q] {\paren {b^p} }
      | r = a
      | c = {{Defof|Rational Power}}
}}
{{eqn | ll= \leadsto
      | l = b^p
      | r = a^q
      | c = {{Defof|Root of Number}}
}}
{{end-eqn}}
which contradicts the initial assumption:
:$\nexists m, n \in \N: a^m = b^n$
Hence the result by Proof by Contradiction.
{{qed}}
Category:Number Theory
Category:Irrationality Proofs
Category:Logarithms
1yhlemqz43hgq5hjcwff6f69qh6xlko
Theorem: Tangent of 22.5 Degrees

:$\tan 22.5 \degrees = \tan \dfrac \pi 8 = \sqrt 2 - 1$

Proof:
{{begin-eqn}}
{{eqn | l = \tan 22.5 \degrees
      | r = \tan \dfrac {45 \degrees} 2
      | c = 
}}
{{eqn | r = \dfrac {1 - \cos 45\degrees} {\sin 45\degrees}
      | c = {{Corollary|Half Angle Formula for Tangent|2}}
}}
{{eqn | r = \dfrac {1 - \frac {\sqrt 2} 2} {\frac {\sqrt 2} 2}
      | c = {{cos|45}} and {{sin|45}}
}}
{{eqn | r = \sqrt 2 - 1
      | c = multiplying top and bottom by $\sqrt 2$
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent of 22.5 Degrees

:$\tan 22.5 \degrees = \tan \dfrac \pi 8 = \sqrt 2 - 1$

Proof:
{{begin-eqn}}
{{eqn | l = \tan 22.5 \degrees
      | r = \dfrac {\sin 22.5 \degrees} {\cos 22.5 \degrees}
      | c = 
}}
{{eqn | r = \dfrac {\dfrac 1 2 \sqrt {2 - \sqrt 2} } {\dfrac 1 2 \sqrt {2 + \sqrt 2} }
      | c = {{sin|22.5}}, {{cos|22.5}}
}}
{{eqn | r = \dfrac {\sqrt {2 - \sqrt 2} \sqrt {2 - \sqrt 2}  } {\sqrt {2 + \sqrt 2} \sqrt {2 - \sqrt 2} }
      | c = multiplying top and bottom by $\sqrt {2 - \sqrt 2}$
}}
{{eqn | r = \dfrac {2 - \sqrt 2} {\sqrt {2^2 - 2} }
      | c = Difference of Two Squares
}}
{{eqn | r = \sqrt 2 - 1
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Theorem: Tangent of 67.5 Degrees

:$\tan 67.5 \degrees = \tan \dfrac {3 \pi} 8 = \sqrt 2 + 1$

Proof:
{{begin-eqn}}
{{eqn | l = \tan 67.5 \degrees
      | r = \map \tan {45 \degrees + 22.5 \degrees}
      | c = 
}}
{{eqn | r = \frac {\tan 45 \degrees + \tan 22.5 \degrees} {1 - \tan 45 \degrees \tan 22.5 \degrees}
      | c = Tangent of Sum
}}
{{eqn | r = \frac {1 + \paren {\sqrt 2 - 1} } {1 - 1 \times \paren {\sqrt 2 - 1} }
      | c = Tangent of $45 \degrees$ and Tangent of $22.5 \degrees$
}}
{{eqn | r = \frac {\sqrt 2} {2 - \sqrt 2}
      | c = simplifying
}}
{{eqn | r = \frac {\sqrt 2 \paren {2 + \sqrt 2} } {\paren {2 - \sqrt 2} \paren {2 + \sqrt 2} }
      | c = multiplying top and bottom by $2 + \sqrt 2$
}}
{{eqn | r = \frac {2 \sqrt 2 + 2} {4 - 2}
      | c = Difference of Two Squares
}}
{{eqn | r = \sqrt 2 + 1
      | c = simplifying
}}
{{end-eqn}}
{{qed}}
Category:Tangent Function
hul6jsgdvh6kjjq1uwbjqvmiu04qpvy
Theorem: Sine of x plus Cosine of x/Cosine Form

:$\sin x + \cos x = \sqrt 2 \, \map \cos {x - \dfrac \pi 4}$

Proof:
{{begin-eqn}}
{{eqn | l = \sin x + \cos x
      | r = \sin x + \map \sin {\frac \pi 2 - x}
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = 2 \, \map \sin {\frac {x + \paren {\frac \pi 2 - x} } 2} \map \cos {\frac {x - \paren {\frac \pi 2 - x} } 2}
      | c = Sine plus Sine
}}
{{eqn | r = 2 \sin \frac \pi 4 \, \map \cos {x - \frac \pi 4}
      | c = simplifying
}}
{{eqn | r = \sqrt 2 \, \map \cos {x - \frac \pi 4}
      | c = Sine of $\dfrac \pi 4$
}}
{{end-eqn}}
{{qed}}
Category:Sine Function
Category:Cosine Function
ql2x5t040ja58vjrf77oda0z3u4akgx
Theorem: Sine of x minus Cosine of x/Sine Form

:$\sin x - \cos x = \sqrt 2 \map \sin {x - \dfrac \pi 4}$

Proof:
{{begin-eqn}}
{{eqn | l = \sin x - \cos x
      | r = \sin x - \map \sin {\frac \pi 2 - x}
      | c = Sine of Complement equals Cosine
}}
{{eqn | r = 2 \map \cos {\frac {x + \paren {\frac \pi 2 - x} } 2} \map \sin {\frac {x - \paren {\frac \pi 2 - x} } 2}
      | c = Sine minus Sine
}}
{{eqn | r = 2 \cos \frac \pi 4 \map \sin {x - \frac \pi 4}
      | c = simplifying
}}
{{eqn | r = \sqrt 2 \map \sin {x - \frac \pi 4}
      | c = Cosine of $\dfrac \pi 4$
}}
{{end-eqn}}
{{qed}}
Category:Sine Function
Category:Cosine Function
mspsbupz2us525dig4ie48b7yulc8hn
Theorem: Sine of x minus Cosine of x/Cosine Form

:$\sin x - \cos x = \sqrt 2 \, \map \cos {x - \dfrac {3 \pi} 4}$

Proof:
{{begin-eqn}}
{{eqn | l = \sin x - \cos x
      | r = \sqrt 2 \, \map \sin {x - \dfrac \pi 4}
      | c = Sine of x minus Cosine of x: Sine Form
}}
{{eqn | r = \sqrt 2 \, \map \cos {\frac \pi 2 - \paren {x - \dfrac \pi 4} }
      | c = Cosine of Complement equals Sine
}}
{{eqn | r = \sqrt 2 \, \map \cos {\frac \pi 2 - x + \dfrac \pi 4}
      | c = simplifying
}}
{{eqn | r = \sqrt 2 \, \map \cos {\frac {3 \pi} 4 - x}
      | c = simplifying
}}
{{eqn | r = \sqrt 2 \, \map \cos {x - \frac {3 \pi} 4}
      | c = Cosine Function is Even
}}
{{end-eqn}}
{{qed}}
Category:Sine Function
Category:Cosine Function
4w1mna76rlqbh5e3l9cnpda8q6g5jgw
Theorem: Multiple of Sine plus Multiple of Cosine/Cosine Form

:$p \sin x + q \cos x = \sqrt {p^2 + q^2} \map \cos {x + \arctan \dfrac {-p} q}$

Proof:
Let it be assumed that $p \sin x + q \cos x$ can be expressed in the form $M \map \cos {x + \phi}$.
Then:
{{begin-eqn}}
{{eqn | l = p \sin x + q \cos x
      | r = M \map \cos {x + \phi}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac p M \sin x + \frac q M \cos x
      | r = \map \cos {x + \phi}
      | c = 
}}
{{eqn | r = \cos x \cos \phi - \sin x \sin \phi
      | c = Cosine of Sum
}}
{{eqn | ll= \leadsto
      | l = \sin x \sin \phi
      | r = \frac {-p} M \sin x
      | c = equating terms in $\sin x$
}}
{{eqn | l = \cos x \cos \phi
      | r = \frac q M \cos x
      | c =  and $\cos x$
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \sin \phi
      | r = \frac {-p} M
      | c = 
}}
{{eqn | n = 2
      | l = \cos \phi
      | r = \frac q M
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin^2 \phi + \cos^2 \phi
      | r = \paren {\frac {-p} M}^2 + \paren {\frac q M}^2
      | c = squaring and adding $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = \frac {p^2 + q^2} {M^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | r = M
      | l = \sqrt {p^2 + q^2}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \tan \phi
      | r = \frac {\sin \phi} {\cos \phi}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {-p / M} {q / M}
      | c = from $(1)$ and $(2)$
}}
{{eqn | r = \frac {-p} q
      | c = simplifying
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Multiple of Sine plus Multiple of Cosine
ov3q1thctvnrnbu2z08jrrfphky3up8
Theorem: Multiple of Sine plus Multiple of Cosine/Sine Form

:$p \sin x + q \cos x = \sqrt {p^2 + q^2} \map \sin {x + \arctan \dfrac q p}$

Proof:
Let it be assumed that $p \sin x + q \cos x$ can be expressed in the form $M \map \sin {x + \phi}$.
Then:
{{begin-eqn}}
{{eqn | l = p \sin x + q \cos x
      | r = M \map \sin {x + \phi}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac p M \sin x + \frac q M \cos x
      | r = \map \sin {x + \phi}
      | c = 
}}
{{eqn | r = \sin x \cos \phi + \cos x \sin \phi
      | c = Sine of Sum
}}
{{eqn | ll= \leadsto
      | l = \sin x \cos \phi
      | r = \frac p M \sin x
      | c = equating terms in $\sin x$
}}
{{eqn | l = \cos x \sin \phi
      | r = \frac q M \cos x
      | c =  and $\cos x$
}}
{{eqn | n = 1
      | ll= \leadsto
      | l = \sin \phi
      | r = \frac q M
      | c = 
}}
{{eqn | n = 2
      | l = \cos \phi
      | r = \frac p M
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \sin^2 \phi + \cos^2 \phi
      | r = \paren {\frac q M}^2 + \paren {\frac p M}^2
      | c = squaring and adding $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = 1
      | r = \frac {p^2 + q^2} {M^2}
      | c = 
}}
{{eqn | ll= \leadsto
      | r = M
      | l = \sqrt {p^2 + q^2}
      | c = 
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \tan \phi
      | r = \frac {\sin \phi} {\cos \phi}
      | c = Tangent is Sine divided by Cosine
}}
{{eqn | r = \frac {q / M} {p / M}
      | c = from $(1)$ and $(2)$
}}
{{eqn | r = \frac q p
      | c = simplifying
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Multiple of Sine plus Multiple of Cosine
ts4v3bj9miqxb5psypgjwxlr2jubnao
Theorem: Primitive of Cosine of a x over Sine of a x plus phi

:$\ds \int \frac {\cos a x \rd x} {\map \sin {a x + \phi} } = \frac {\ln \size {\map \sin {a x + \phi} } } {a \cos \phi} + \tan \phi \int \frac {\sin a x \rd x} {\map \sin {a x + \phi} } + C$

Proof:
First note that:
{{begin-eqn}}
{{eqn | n = 1
      | l = \map {\frac \d {\d x} } {\map \sin {a x + \phi} }
      | r = a \map \cos {a x + \phi}
      | c = Derivative of $\sin a x$ etc.
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\cos a x \rd x} {\map \sin {a x + \phi} }
      | r = \int \frac {\cos a x \cos \phi \rd x} {\cos \phi \map \sin {a x + \phi} }
      | c = multiplying top and bottom by $\cos \phi$
}}
{{eqn | r = \int \frac {\paren {\cos a x \cos \phi - \sin a x \sin \phi + \sin a x \sin \phi} \rd x} {\cos \phi \map \sin {a x + \phi} }
      | c = 
}}
{{eqn | r = \int \frac {\paren {\map \cos {a x + \phi} + \sin a x \sin \phi} \rd x} {\cos \phi \map \sin {a x + \phi} }
      | c = Cosine of Sum
}}
{{eqn | r = \frac 1 {\cos \phi} \int \frac {\map \cos {a x + \phi} \rd x} {\map \sin {a x + \phi} } + \frac {\sin \phi} {\cos \phi} \int \frac {\sin a x \rd x} {\map \sin {a x + \phi} }
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac 1 {\cos \phi} \ln \size {\map \sin {a x + \phi} } + \frac {\sin \phi} {\cos \phi} \int \frac {\sin a x \rd x} {\map \sin {a x + \phi} }
      | c = Primitive of Function under its Derivative and $(1)$
}}
{{eqn | r = \frac {\ln \size {\map \sin {a x + \phi} } } {a \cos \phi} + \tan \phi \int \frac {\sin a x \rd x} {\map \sin {a x + \phi} } + C
      | c = Tangent is Sine divided by Cosine
}}
{{end-eqn}}
{{qed}}
Category:Primitives involving Sine Function
Category:Primitives involving Cosine Function
py6xtc7vmbw2qrdx58kg4nk7opt88kh
Theorem: Primitive of Sine of a x over Sine of a x plus phi

:$\ds \int \frac {\sin a x \rd x} {\map \sin {a x + \phi} } = \frac x {\cos \phi} - \tan \phi \int \frac {\cos a x \rd x} {\map \sin {a x + \phi} } + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \frac {\sin a x \rd x} {\map \sin {a x + \phi} }
      | r = \frac 1 {\cos \phi} \int \frac {\sin a x \cos \phi \rd x} {\map \sin {a x + \phi} }
      | c = multiplying top and bottom by $\cos \phi$
}}
{{eqn | r = \frac 1 {\cos \phi} \int \frac {\paren {\sin a x \cos \phi + \cos a x \sin \phi - \cos a x \sin \phi} \rd x} {\map \sin {a x + \phi} }
      | c = 
}}
{{eqn | r = \frac 1 {\cos \phi} \int \frac {\paren {\map \sin {a x + \phi} - \cos a x \sin \phi} \rd x} {\map \sin {a x + \phi} }
      | c = Sine of Sum
}}
{{eqn | r = \frac 1 {\cos \phi} \int \frac {\paren {\map \sin {a x + \phi} - \cos a x \sin \phi} \rd x} {\map \sin {a x + \phi} }
      | c = Sine of Sum
}}
{{eqn | r = \frac 1 {\cos \phi} \int \d x  - \frac {\sin \phi} {\cos \phi} \int \frac {\cos a x \rd x} {\map \sin {a x + \phi} }
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac x {\cos \phi} - \tan \phi \int \frac {\cos a x \rd x} {\map \sin {a x + \phi} } + C
      | c = Tangent is Sine divided by Cosine
}}
{{end-eqn}}
{{qed}}
Category:Primitives involving Sine Function
Category:Primitives involving Cosine Function
h819g82wyysmokwhuxgge6uxacaencw
Theorem: Reciprocal of Hyperbolic Cosine Plus One

:$\dfrac 1 {\cosh x + 1} = \dfrac 1 2 \sech^2 \dfrac x 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= \leadstoandfrom
      | l = \cosh x + 1
      | r = 2 \cosh^2 \frac x 2
      | c = adding $1$ to both sides
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 {\cosh x + 1}
      | r = \frac 1 2 \frac 1 {\cosh^2 \frac x 2}
      | c = taking the reciprocal of both sides
}}
{{eqn | r = \frac 1 2 \sech^2 \frac x 2
      | c = {{Defof|Hyperbolic Secant|index = 2}}
}}
{{end-eqn}}
{{qed}}
Theorem: Reciprocal of Hyperbolic Cosine Minus One

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

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= \leadstoandfrom
      | l = \cosh x - 1
      | r = 2 \sinh^2 \frac x 2
      | c = subtracting $1$ from both sides
}}
{{eqn | ll= \leadstoandfrom
      | l = \frac 1 {\cosh x - 1}
      | r = \frac 1 2 \frac 1 {\sinh^2 \frac x 2}
      | c = taking the reciprocal of both sides
}}
{{eqn | r = \frac 1 2 \csch^2 \frac x 2
      | c = {{Defof|Hyperbolic Cosecant|index = 2}}
}}
{{end-eqn}}
{{qed}}