avewright/proofwiki-math huggingface dataset:
Theorem: Laplace Transform of Positive Integer Power

Let $\laptrans f$ denote the Laplace transform of a function $f$.
Let $t^n: \R \to \R$ be $t$ to the $n$th power for some $n \in \N_{\ge 0}$.
Then:
:$\laptrans {t^n} = \dfrac {n!} {s^{n + 1} }$
for $\map \Re s > 0$.

Proof:
The proof proceeds by induction on $n$ for $t^n$.
For all $n \in \Z_{\ge 0}$, let $\map P n$ be the proposition:
:$\laptrans {t^n} = \dfrac {n!} { s^{n + 1} }$
=== Basis for the Induction ===
$\map P 0$ is the case:
{{begin-eqn}}
{{eqn | l = \laptrans {t^0}
      | r = \laptrans 1
}}
{{eqn | r = \frac 1 s
      | c = Laplace Transform of 1
}}
{{eqn | r = \frac {0!} {s^{0 + 1} }
      | c = {{Defof|Factorial}}: $0! = 1$
}}
{{end-eqn}}
This is the basis for the induction.
=== Induction Hypothesis ===
Now it needs to be shown that if $\map P k$ is true, where $k \ge 1$, then it logically follows that $\map P {k + 1}$ is true.
So this is the induction hypothesis:
:$\laptrans {t^k} = \dfrac {k!} {s^{k + 1} }$
from which it is to be shown that:
:$\laptrans {t^{k + 1} } = \dfrac {\paren {k + 1}!} {s^{k + 2} }$
=== Induction Step ===
This is our induction step:
{{begin-eqn}}
{{eqn | l = \laptrans {t^{k + 1} }
      | r = \int_0^{\to +\infty} t^{k + 1} e^{-s t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{end-eqn}}
From Integration by Parts:
:$\ds \int f g' \rd t = f g - \int f' g \rd t$
Here:
{{begin-eqn}}
{{eqn | l = f
      | r = t^{k + 1}
}}
{{eqn | ll= \leadsto
      | l = f'
      | r = \paren {k + 1}  t^n
      | c = Power Rule for Derivatives
}}
{{eqn | l = g'
      | r = e^{-s t}
}}
{{eqn | ll= \leadsto
      | l = g
      | r = -\frac 1 s e^{-s t}
      | c = Primitive of Exponential Function
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = \int t^{k + 1} e^{-s t} \rd t
      | r = -\frac {t^{k + 1} } s e^{-s t} + \frac {k + 1} s \int t^k e^{-s t} \rd t
}}
{{end-eqn}}
Evaluating at $t = 0$ and $t \to +\infty$:
{{begin-eqn}}
{{eqn | l = \laptrans {t^{k + 1} }
      | r = -\intlimits {\frac 1 s t^{k + 1} e^{-s t} } {t \mathop = 0} {t \mathop \to +\infty} + \frac {k + 1} s \laptrans {t^n}
}}
{{eqn | r = -\intlimits {\frac {s^{-1} t^{k + 1} } {e^{s t} } } {t \mathop = 0} {t \mathop \to +\infty} + \frac {k + 1} s \laptrans {t^n}
      | c = Exponent Combination Laws
}}
{{eqn | r = 0 - 0 + \frac {k + 1} s \laptrans {t^n}
      | c = Limit at Infinity of Polynomial over Complex Exponential
}}
{{eqn | r = \frac {k + 1} s \times \frac {k!} {s^{k + 1} }
      | c = Induction Hypothesis
}}
{{eqn | r = \frac {\paren {k + 1}!} {s^{k + 1 + 1} }
      | c = Exponent Combination Laws, Definition of Factorial
}}
{{end-eqn}}
The result follows by the Principle of Mathematical Induction.
{{qed}}
Theorem: Primitive of Function under its Derivative

Let $f$ be a real function which is integrable.
Then:
:$\ds \int \frac {\map {f'} x} {\map f x} \rd x = \ln \size {\map f x} + C$
where $C$ is an arbitrary constant.

Proof:
By Integration by Substitution (with appropriate renaming of variables):
:$\ds \int \map g u \rd u = \int \map g {\map f x} \map {f'} x \rd x$
Then:
{{begin-eqn}}
{{eqn | l = \int \frac {\map {f'} x} {\map f x} \rd x
      | r = \int \frac {\d u} u
      | c = putting $\map g u := \dfrac 1 u$
}}
{{eqn | r = \ln \size u + C
      | c = Primitive of Reciprocal
}}
{{eqn | r = \ln \size {\map f x} + C
      | c = Definition of $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Exponential Function/General Result

Let $a \in \R_{>0}$ be a constant such that $a \ne 1$.
Then:
:$\ds \int a^x \rd x = \frac {a^x} {\ln a} + C$
where $C$ is an arbitrary constant.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {a^x}
      | r = a^x \ln a
      | c = Derivative of General Exponential Function
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d x} } {\dfrac {a^x} {\ln a} }
      | r = a^x
      | c = Derivative of Constant Multiple
}}
{{eqn | ll= \leadsto
      | l = \int a^x \rd x
      | r = \dfrac {a^x} {\ln a}
      | c = {{Defof|Primitive (Calculus)}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Exponential Function/General Result

Let $a \in \R_{>0}$ be a constant such that $a \ne 1$.
Then:
:$\ds \int a^x \rd x = \frac {a^x} {\ln a} + C$
where $C$ is an arbitrary constant.

Proof:
Let $u = x \ln a$.
{{begin-eqn}}
{{eqn | l = \int a^x \rd x
      | r = \int \map \exp {x \ln a} \rd x
      | c = {{Defof|Power to Real Number}}
}}
{{eqn | r = \frac 1 {\ln a} \int \map \exp u \rd u
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = \frac {\map \exp u} {\ln a} + C
      | c = Primitive of Exponential Function
}}
{{eqn | r = \frac {\map \exp {x \ln a} } {\ln a} + C
      | c = Definition of $u$
}}
{{eqn | r = \frac {a^x} {\ln a} + C
      | c = {{Defof|Power to Real Number}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Tangent Function/Secant Form

:$\ds \int \tan x \rd x = \ln \size {\sec x} + C$
where $\sec x$ is defined.

Proof:
{{begin-eqn}}
{{eqn | l = \int \tan x \rd x
      | r = -\ln \size {\cos x} + C
      | c = Primitive of $\tan x$: Cosine Form
}}
{{eqn | r = \ln \size {\frac 1 {\cos x} } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \ln \size {\sec x} + C
      | c = Secant is Reciprocal of Cosine
}}
{{end-eqn}}
{{qed}}
Theorem: Exponential of x not less than 1+x

:$e^x \ge 1 + x$
for all $x \in \R$.

Proof:
For $x > - 1$:
{{begin-eqn}}
{{eqn | l = e^x
      | r = \lim_{n \mathop \to \infty} \left({1 + \frac x n}\right)^n
      | c = {{Defof|Real Exponential Function}}
}}
{{eqn | o = \ge
      | r = \lim_{n \mathop \to \infty} \left({1 + x}\right)
      | c = Bernoulli's Inequality
}}
{{eqn | r = 1 + x
      | c = 
}}
{{end-eqn}}
as required.
For $x \le -1$, the inequality follows from the fact that $e^x$ is positive for all $x$.
{{qed}}
Category:Exponential Function
Category:Inequalities
hqlcsp872ooy00iyqpsw50x7c4n1qxm
Theorem: Primitive of Cosecant Function/Cosecant minus Cotangent Form

:$\ds \int \csc x \rd x = \ln \size {\csc x - \cot x} + C$
where $\csc x - \cot x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \csc x \rd x
      | r = \ln \size {\tan \frac x 2} + C
      | c = Primitive of $\csc x$: Tangent Form
}}
{{eqn | r = \ln \size {\frac {1 - \cos x} {\sin x} } + C
      | c = {{Corollary|Half Angle Formula for Tangent|2}}
}}
{{eqn | r = \ln \size {\frac 1 {\sin x} - \frac {\cos x} {\sin x} } + C
      | c = 
}}
{{eqn | r = \ln \size {\csc x - \cot x} + C
      | c = {{Defof|Cosecant}} and {{Defof|Cotangent}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosecant Function/Tangent Form

:$\ds \int \csc x \rd x = \ln \size {\tan \frac x 2} + C$
where $\tan \dfrac x 2 \ne 0$.

Proof:
{{Mistake|Review grammar in the below. Recall the rule about when capital letters are used. See Help:Editing/House Style#Capital Letters begin Sentences.}}
Since:
:$\tan \dfrac x 2 \ne 0$
It follows that $\forall n \in \Z$: 
:$ 2\pi n < x < 2\pi n + \pi$
So:
:$\csc x + \cot x \ne 0$
And:
:$\dfrac {1 + \cos x} {\sin x} \ne 0$ 
Hence:
{{begin-eqn}}
{{eqn | l = \int \csc x \rd x
      | r = -\ln \size {\csc x + \cot x} + C
      | c = Primitive of $\csc x$: Cosecant plus Cotangent Form
}}
{{eqn | r = \ln \size {\frac 1 {\csc x + \cot x} } + C
      | c = Logarithm of Reciprocal
}}
{{eqn | r = \ln \size {\frac 1 {\frac 1 {\sin x} + \frac {\cos x} {\sin x} } } + C
      | c = {{Defof|Cosecant}} and {{Defof|Cotangent}}
}}
{{eqn | r = \ln \size {\frac {\sin x} {1 + \cos x} } + C
      | c = 
}}
{{eqn | r = \ln \size {\tan \frac x 2} + C
      | c = {{Corollary|Half Angle Formula for Tangent|1}}
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Cosecant Function/Tangent Form

:$\ds \int \csc x \rd x = \ln \size {\tan \frac x 2} + C$
where $\tan \dfrac x 2 \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \csc x \rd x 
      | r = \int \frac 1 {\sin x} \rd x
      | c = Cosecant is Reciprocal of Sine
}}
{{end-eqn}}
We make the Weierstrass Substitution:
{{begin-eqn}}
{{eqn | l = u
      | r = \tan \frac x 2
}}
{{eqn | ll= \leadsto
      | l = \sin x
      | r = \frac {2 u} {u^2 + 1}
}}
{{eqn | ll= \leadsto
      | l = \frac {\d x} {\d u}
      | r = \frac 2 {u^2 + 1}
}}
{{eqn | ll= \leadsto
      | l = \int \frac 1 {\sin x} \rd x
      | r = \int \frac {u^2 + 1} {2 u} \frac 2 {u^2 + 1} \rd u
}}
{{eqn | r = \int \frac 1 u \rd u
}}
{{eqn | r = \ln \size u + C
      | c = Primitive of Reciprocal
}}
{{eqn | r = \ln \size {\tan \frac x 2} + C
      | c = substituting back for $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Secant Function

:$\ds \int \sec^2 x \rd x = \tan x + C$
where $C$ is an arbitrary constant.

Proof:
From Derivative of Tangent Function:
:$\map {\dfrac \d {\d x} } {\tan x} = \sec^2 x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Square of Cosecant Function

:$\ds \int \csc^2 x \rd x = -\cot x + C$

Proof:
From Derivative of Cotangent Function:
:$\dfrac \d {\d x} \cot x = -\csc^2 x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Square of Tangent Function

:$\ds \int \tan^2 x \rd x = \tan x - x + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \tan^2 x \rd x
      | r = \int \paren {\sec^2 x - 1} \rd x
      | c = Difference of Squares of Secant and Tangent
}}
{{eqn | r = \int \sec^2 x \rd x + \int \paren {-1} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \tan x + C + \int \paren {-1} \rd x
      | c = Primitive of Square of Secant Function
}}
{{eqn | r = \tan x - x + C
      | c = Primitive of Constant
}}
{{end-eqn}}
{{Qed}}
Theorem: Primitive of Square of Tangent Function

:$\ds \int \tan^2 x \rd x = \tan x - x + C$

Proof:
{{begin-eqn}}
{{eqn	| l = I_n
	| r = \int \tan^n x \rd x
}}
{{eqn	| r = \frac {\tan^{n - 1} x} {n - 1} - I_{n - 2} 
	| c = Reduction Formula for Integral of Power of Tangent
}}
{{eqn	| l = I_0
	| r = \int \paren {\tan x}^0 \rd x
}}
{{eqn	| r = \int \d x
	| c =
}}
{{eqn	| r = x + C
	| c = Primitive of Constant
}}
{{eqn	| ll= \leadsto
	| l = I_2
	| r = \tan x - x + C'
	| c = setting $n = 2$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Cotangent Function

:$\ds \int \cot^2 x \rd x = -\cot x - x + C$
where $C$ is an arbitrary constant.

Proof:
{{begin-eqn}}
{{eqn | l = \int \cot^2 x \rd x
      | r = \int \paren {\csc^2 x - 1} \rd x
      | c = Difference of Squares of Cosecant and Cotangent
}}
{{eqn | r = \int \csc^2 x \rd x + \int \paren {-1} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = -\cot x + C + \int \paren {-1} \rd x
      | c = Primitive of Square of Cosecant Function
}}
{{eqn | r = -\cot x - x + C
      | c = Primitive of Constant
}}
{{end-eqn}}
{{Qed}}
Theorem: Primitive of Square of Sine Function

:$\ds \int \sin^2 x \rd x = \frac x 2 - \frac {\sin 2 x} 4 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \sin^2 x \rd x
      | r = \int \paren {\frac {1 - \cos 2 x} 2} \rd x
      | c = Square of Sine
}}
{{eqn | r = \frac 1 2 \int \d x - \frac 1 2 \int \cos 2 x \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac x 2 - \frac 1 2 \int \cos 2 x \rd x + C
      | c = Primitive of Constant
}}
{{eqn | r = \frac x 2 - \frac 1 2 \paren {\frac {\sin 2 x} 2} + C
      | c = Primitive of $\cos a x$
}}
{{eqn | r = \frac x 2 - \frac {\sin 2 x} 4 + C
      | c = rearranging
}}
{{end-eqn}}
{{Qed}}
Theorem: Primitive of Square of Cosine Function

:$\ds \int \cos^2 x \rd x = \frac x 2 + \frac {\sin 2 x} 4 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \cos^2 x \rd x
      | r = \int \paren {\frac {1 + \cos 2 x} 2} \rd x
      | c = Square of Cosine
}}
{{eqn | r = \int \frac 1 2 \rd x + \int \paren {\frac {\cos 2 x} 2} \rd x
      | c = Linear Combination of Primitives
}}
{{eqn | r = \frac x 2 + C + \int \paren {\frac {\cos 2 x} 2} \rd x
      | c = Primitive of Constant
}}
{{eqn | r = \frac x 2 + C + \frac 1 2 \int \cos 2 x \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = \frac x 2 + \frac 1 2 \paren {\frac {\sin 2 x} 2} + C
      | c = Primitive of Function of Constant Multiple and Primitive of Cosine Function
}}
{{eqn | r = \frac x 2 + \frac {\sin 2 x} 4 + C
      | c = Primitive of Function of Constant Multiple and Primitive of Cosine Function
}}
{{end-eqn}}
{{Qed}}
Theorem: Primitive of Square of Cosine Function

:$\ds \int \cos^2 x \rd x = \frac x 2 + \frac {\sin 2 x} 4 + C$

Proof:
{{begin-eqn}}
{{eqn	| l = I_n
	| r = \int \cos^n x \rd x
}}
{{eqn	| r = \dfrac {\cos^{n - 1} x \sin x} n + \dfrac {n - 1} n I_{n-2}
	| c = Reduction Formula for Integral of Power of Cosine
}}
{{eqn	| l = I_0
	| r = \int \left({\cos x}\right)^0 \rd x
	| c = 
}}
{{eqn	| r = \int \rd x
	| c = 
}}
{{eqn	| r = x + C
	| c = Primitive of Constant
}}
{{eqn	| ll= \leadsto
	| l  = I_2
	| r  = \frac {\cos x \sin x} 2 + \frac x 2 + \frac C 2
	| c  = setting $n = 2$
}}
{{eqn	| r = \frac {\sin 2 x} 4 + \frac x 2 + C'
	| c = Double Angle Formula for Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Square of Cosine Function

:$\ds \int \cos^2 x \rd x = \frac x 2 + \frac {\sin 2 x} 4 + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \cos^2 x \rd x 
      | r = \frac 1 4 \int \paren {e^{i x} + e^{-i x} }^2 \rd x
      | c = Euler's Cosine Identity
}}
{{eqn | r = \frac 1 4 \int \paren {e^{2 i x} + 2 + e^{-2 i x} } \rd x
}}
{{eqn | r = \frac 1 4 \paren {\frac{e^{2 i x} - e^{-2 i x} } {2 i} + 2 x} + C
      | c = Primitive of $e^{a x}$, Primitive of Constant
}}
{{eqn | r = \frac {\sin 2 x} 4 + \frac x 2 + C
      | c = Euler's Sine Identity
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Product of Secant and Tangent

:$\ds \int \sec x \tan x \rd x = \sec x + C$
where $C$ is an arbitrary constant.

Proof:
From Derivative of Secant Function:
:$\dfrac \d {\d x} \sec x = \sec x \tan x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Product of Cosecant and Cotangent

:$\ds \int \csc x \cot x \rd x = -\csc x + C$
where $C$ is an arbitrary constant.

Proof:
From Derivative of Cosecant Function:
:$\dfrac \d {\d x} \csc x = -\csc x \cot x$
The result follows from the definition of primitive.
{{Qed}}
Theorem: Primitive of Hyperbolic Sine Function

:$\ds \int \sinh x \rd x = \cosh x + C$

Proof:
From Derivative of Hyperbolic Cosine:
:$\map {\dfrac \d {\d x} } {\cosh x} = \sinh x$
The result follows from the definition of primitive.
{{qed}}
Theorem: Primitive of Hyperbolic Cosine Function

:$\ds \int \cosh x \rd x = \sinh x + C$

Proof:
From Derivative of Hyperbolic Sine:
:$\map {\dfrac \d {\d x} } {\sinh x} = \cosh x$
The result follows from the definition of primitive.
{{qed}}
Theorem: Primitive of Hyperbolic Tangent Function

:$\ds \int \tanh x \rd x = \map \ln {\cosh x} + C$

Proof:
{{begin-eqn}}
{{eqn | l = \int \tanh x \rd x
      | r = \int \frac {\sinh x} {\cosh x} \rd x
      | c = {{Defof|Hyperbolic Tangent}}
}}
{{eqn | r = \int \frac {\paren {\cosh x}'} {\cosh x} \rd x
      | c = Derivative of Hyperbolic Cosine
}}
{{eqn | r = \ln \size {\cosh x} + C
      | c = Primitive of Function under its Derivative
}}
{{eqn | r = \map \ln {\cosh x} + C
      | c = Graph of Hyperbolic Cosine Function: $\cosh x > 0$ for all $x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Hyperbolic Tangent Function

:$\ds \int \tanh x \rd x = \map \ln {\cosh x} + C$

Proof:
{{begin-eqn}}
{{eqn	| l = \int \tanh x \rd x
	| r = -i \int \tan i x \rd x
	| c = Hyperbolic Tangent in terms of Tangent
}}
{{eqn	| r = -\int \tan i x \rd \paren {i x}
	| c = Primitive of Function of Constant Multiple
}}
{{eqn	| r = \ln \cmod {\cos i x} + C
	| c = Primitive of $\tan x$: Cosine Form
}}
{{eqn	| r = \ln \cmod {\cosh x} + C
	| c = {{Defof|Hyperbolic Cosine}}
}}
{{eqn | r = \map \ln {\cosh x} + C
      | c = Graph of Hyperbolic Cosine Function: $\cosh x > 0$ for all $x$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Hyperbolic Cotangent Function

:$\ds \int \coth x \rd x = \ln \size {\sinh x} + C$
where $\sinh x \ne 0$.

Proof:
{{begin-eqn}}
{{eqn | l = \int \coth x \rd x
      | r = \int \frac {\cosh x} {\sinh x} \rd x
      | c = {{Defof|Hyperbolic Cotangent}}
}}
{{eqn | r = \int \frac {\paren {\sinh x}'} {\sinh x} \rd x
      | c = Derivative of Hyperbolic Sine
}}
{{eqn | r = \ln \size {\sinh x} + C
      | c = Primitive of Function under its Derivative
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of Tan X over X at Zero

:$\ds \lim_{x \mathop \to 0} \frac {\tan x} x = 1$

Proof:
By L'Hôpital's Rule:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0} \frac {\tan x} x 
      | r = \lim_{x \mathop \to 0} \frac {\sec^2 x} 1
      | c = Derivative of Tangent Function
}}
{{eqn | r = 1
      | c = Secant of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of Tan X over X at Zero

:$\ds \lim_{x \mathop \to 0} \frac {\tan x} x = 1$

Proof:
{{begin-eqn}}
{{eqn | l = \lim_{x \mathop \to 0} \frac {\tan x} x 
      | r = \lim_{x \mathop \to 0} \frac 1 {\cos x} \frac {\sin x} x
      | c = {{Defof|Tangent Function}}
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac 1 {\cos x} \lim_{x \mathop \to 0} \frac {\sin x} x
      | c = Product Rule for Limits of Real Functions
}}
{{eqn | r = \lim_{x \mathop \to 0} \frac {\sin x} x 
      | c = Cosine of Zero is One
}}
{{eqn | r = 1
      | c = Limit of $\dfrac {\sin x} x$ at Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Limit of Tan X over X at Zero

:$\ds \lim_{x \mathop \to 0} \frac {\tan x} x = 1$

Proof:
Let $f$ be the real function defined as:
:$\map f x = \sin x$
Let:
:$c = \pi$
:$h \in \openint 1 {\dfrac \pi 2}$
We have:
{{begin-eqn}}
{{eqn | l = \map f {c + h}
      | r = \map \sin {\pi + h}
      | c = 
}}
{{eqn | l = \map f c
      | r = \sin \pi
      | c = 
}}
{{eqn | ll= \leadsto
      | q = \exists \theta \in \openint 0 1
      | l = \dfrac {\map \sin {\pi + h} - \sin \pi} h
      | r = \map \cos {\pi + \theta h}
      | c = Mean Value Theorem
}}
{{eqn | ll= \leadsto
      | l = -\sin h - 1
      | r = -h \cos \theta h
      | c = Sine of Angle plus Straight Angle, Cosine of Angle plus Straight Angle
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | ll= \leadsto
      | l = -h
      | o = <
      | m = -\sin h
      | mo= <
      | r = -h \cos h
      | c = as $0 < \theta < 1$
}}
{{eqn | ll= \leadsto
      | l = 1
      | o = <
      | m = \dfrac {\tan h} h
      | mo= <
      | r = \sec h
      | c = 
}}
{{end-eqn}}
Hence by the Squeeze Theorem for Functions:
:$\ds \lim_{h \mathop \to 0} \dfrac {\tan h} h = 1$
The result follows on renaming $h$ to $x$.
{{qed}}
Theorem: Euler Formula for Sine Function/Real Numbers

{{begin-eqn}}
{{eqn | l = \sin x
      | r = x \prod_{n \mathop = 1}^\infty \paren {1 - \frac {x^2} {n^2 \pi^2} }
      | c = 
}}
{{eqn | r = x \paren {1 - \dfrac {x^2} {\pi^2} } \paren {1 - \dfrac {x^2} {4 \pi^2} } \paren {1 - \dfrac {x^2} {9 \pi^2} } \dotsm
      | c = 
}}
{{end-eqn}}
for all $x \in \R$.

Proof:
Using De Moivre's Formula:
:$\sin x = \dfrac {\left({\cos \dfrac x n + i \sin \dfrac x n}\right)^n - \left({\cos \dfrac x n - i \sin \dfrac x n}\right)^n} {2i}$
The difference between two $n$th powers can be extracted into linear factors using $n$th roots of unity.
For large $n$, we can replace:
: $\cos \dfrac x n$ by $1$
: $\sin \dfrac x n$ by $\dfrac x n$
{{proof wanted}}
Theorem: Euler Formula for Sine Function/Real Numbers

{{begin-eqn}}
{{eqn | l = \sin x
      | r = x \prod_{n \mathop = 1}^\infty \paren {1 - \frac {x^2} {n^2 \pi^2} }
      | c = 
}}
{{eqn | r = x \paren {1 - \dfrac {x^2} {\pi^2} } \paren {1 - \dfrac {x^2} {4 \pi^2} } \paren {1 - \dfrac {x^2} {9 \pi^2} } \dotsm
      | c = 
}}
{{end-eqn}}
for all $x \in \R$.

Proof:
We have that $\sin x$  has a power series representation:
:$\sin x = x - \dfrac {x^3} {3!} + \dfrac {x^5} {5!} - \dfrac {x^7} {7!} + \cdots$
The roots of sine are the numbers $k \pi$, where $k$ is any integer.
From the Polynomial Factor Theorem, the following ''might'' be true:
:$\ds \sin x = A x \prod \paren {1 - \frac x {k \pi} }$
where the product is taken over all $n \in \Z \setminus \set 0$, and $A$ is some constant.
The intuition is as follows.
{{begin-eqn}}
{{eqn | l = \sin x
      | r = \ldots \paren {1 - \frac x {2 \pi} } \paren {1 - \frac x \pi} A x \paren {1 + \frac x \pi} \paren {1 + \frac x {2 \pi} } \cdots
}}
{{eqn | r = A x \paren {1 - \frac {x^2} {\pi^2} } \paren {1 - \frac {x^2} {2^2 \pi^2} } \paren {1 - \frac {x^2} {3^2 \pi^2} } \cdots
}}
{{eqn | ll= \leadsto
      | l = \frac {\sin x} x
      | r = A \paren {1 - \frac {x^2} {\pi^2} } \paren {1 - \frac {x^2} {2^2 \pi^2} } \paren {1 - \frac {x^2} {3^2 \pi^2} } \cdots
      | c = for $x \ne 0$
}}
{{end-eqn}}
From Limit of $\dfrac {\sin x} x$ at Zero:
:$\dfrac {\sin x} x \to 1$ as $x \to 0$
Letting $x$ tend to $0$ in the above equation implies that $A = 1$.
We now formalize the above claims.
{{proof wanted}}
Theorem: Logarithm of Reciprocal

:$\map {\log_b} {\dfrac 1 x} = -\log_b x$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\log_b} {\dfrac 1 x}
      | r = \log_b 1 - \log_b x
      | c = Difference of Logarithms
}}
{{eqn | r = 0 - \log_b x
      | c = Logarithm of 1 is 0
}}
{{end-eqn}}
Hence the result.
{{qed}}
Category:Logarithms
Category:Reciprocals
kgfbjw7h1n6cupqiu7qtvossewt0xp8
Theorem: Primitive of Hyperbolic Secant Function/Arcsine Form

:$\ds \int \sech x \rd x = \map \arcsin {\tanh x} + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = \int \sech x \rd x
      | r = \int \frac {\sech^2 x} {\sech x} \rd x
      | c = 
}}
{{eqn | r = \int \frac {\sech^2 x} {\sqrt {1 - \tanh^2 x} } \rd x
      | c = Sum of Squares of Hyperbolic Secant and Tangent
}}
{{end-eqn}}
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \tanh x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u'
      | r = \sech^2 x
      | c = Derivative of Hyperbolic Tangent
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \sech x \rd x
      | r = \int \frac {\d u} {\sqrt {1 - u^2} }
      | c = Integration by Substitution
}}
{{eqn | r = \map \arcsin u + C
      | c = Primitive of $\dfrac 1 {\sqrt {a^2 - x^2} }$: Arcsine Form
}}
{{eqn | r = \map \arcsin {\tanh x} + C
      | c = Definition of $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Hyperbolic Secant Function/Arctangent of Exponential Form

:$\ds \int \sech x \rd x = 2 \map \arctan {e^x} + C$

Proof:
Let:
{{begin-eqn}}
{{eqn | l = \int \sech x \rd x
      | r = \int \frac 2 {e^x + e^{-x} } \rd x
      | c = {{Defof|Hyperbolic Secant|index = 1}}
}}
{{eqn | r = \int \frac {2 e^x} {e^{2 x} + 1} \rd x
      | c = multiplying top and bottom by $e^x$
}}
{{end-eqn}}
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = e^x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = u'
      | r = e^x
      | c = Derivative of Exponential Function
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \sech x \rd x
      | r = \int \frac {2 \rd u} {u^2 + 1}
      | c = Integration by Substitution
}}
{{eqn | r = 2 \arctan u + C
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$: Arctangent Form
}}
{{eqn | r = 2 \map \arctan {e^x} + C
      | c = Definition of $u$
}}
{{end-eqn}}
{{qed}}
Theorem: Primitive of Hyperbolic Cosecant Function/Logarithm Form

:$\ds \int \csch x \rd x = -\ln \size {\csch x + \coth x} + C$
where $\csch x + \coth x \ne 0$.

Proof:
Let:
{{begin-eqn}}
{{eqn | l = u
      | r = \coth x + \csch x
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \frac {\d u} {\d x}
      | r = \frac \d {\d x} \coth x + \frac \d {\d x} \csch x 
      | c = Linear Combination of Derivatives
}}
{{eqn | r = -\csch^2 x + \frac \d {\d x} \csch x 
      | c = Derivative of Hyperbolic Cotangent
}}
{{eqn | r = -\csch^2 x - \csch x \coth x 
      | c = Derivative of Hyperbolic Cosecant
}}
{{eqn | r = -\csch x \paren {\csch x + \coth x}
      | c = factorising
}}
{{end-eqn}}
Then:
{{begin-eqn}}
{{eqn | l = \int \csch x \rd x
      | r = \int \frac {\csch x \paren {\csch x + \coth x} } {\csch x + \coth x} \rd x
      | c = multiplying top and bottom by $\csch x + \coth x$
}}
{{eqn | r = -\int \frac {-\csch x \paren {\csch x + \coth x} } {\csch x + \coth x} \rd x
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = -\ln \size {\csch x + \coth x} + C
      | c = Primitive of Function under its Derivative
}}
{{end-eqn}}
{{qed}}