avewright/proofwiki-math huggingface dataset:
Theorem: Gamma Function of One Half

:$\map \Gamma {\dfrac 1 2} = \sqrt \pi$

Proof:
{{begin-eqn}}
{{eqn | l = \map \Gamma 1 \, \map \Gamma {\frac 1 2} 
      | r = 2^0 \sqrt \pi \ \map \Gamma 1 
      | c = Legendre's Duplication Formula 
}} 
{{eqn | ll= \leadsto 
      | l = 0! \, \map \Gamma {\frac 1 2} 
      | r = 0! \, \sqrt \pi
      | c = {{Defof|Gamma Function}}
}}
{{eqn | ll= \leadsto 
      | l = \map \Gamma {\frac 1 2} 
      | r = \sqrt \pi
      | c = Factorial of Zero
}}
{{end-eqn}}
{{qed}}
Theorem: Integral of Exponent of Half Square over Reals

:$\ds \int_{\mathop \to -\infty}^{\mathop \to +\infty} e^{- x^2 / 2} \rd x = \sqrt {2 \pi}$

Proof:
Let $t = \dfrac {x^2} 2$.
Then:
{{begin-eqn}}
{{eqn | l = \int_0^{\mathop \to +\infty} e^{- x^2 / 2} \rd x
      | r = \int_0^{\mathop \to +\infty} \paren {2 t} e^{-t} \rd t
      | c = Integration by Substitution
}}
{{eqn | r = \frac 1 {\sqrt 2} \map \Gamma {\frac 1 2}
      | c = {{Defof|Gamma Function|subdef = Integral Form}}
}}
{{eqn | r = \frac 1 {\sqrt 2} \sqrt \pi
      | c = Gamma Function of One Half
}}
{{eqn | r = \frac {\sqrt {2 \pi} } 2
      | c = multiplying top and bottom by $\sqrt 2$
}}
{{end-eqn}}
We have that $e^{- x^2 / 2}$ is an even function.
From {{Corollary|Definite Integral of Even Function}}:
:$\ds \int_{\mathop \to -\infty}^{\mathop \to +\infty} e^{- x^2 / 2} \rd x = 2 \int_0^{\mathop \to +\infty} e^{- x^2 / 2} \rd x$
Hence the result.
{{qed}}
Theorem: Sum of Reciprocals of Primes is Divergent/Proof 2

The series:
:$\ds \sum_{p \mathop \in \Bbb P} \frac 1 p$
where:
:$\Bbb P$ is the set of all prime numbers
is divergent.

Proof:
Let $n \in \N$ be a natural number.
Let $p_n$ denote the $n$th prime number.
Consider the continued product:
:$\ds \prod_{k \mathop = 1}^n \frac 1 {1 - 1 / p_k}$
By Sum of Infinite Geometric Sequence:
{{begin-eqn}}
{{eqn | l = \frac 1 {1 - \frac 1 2}
      | r = 1 + \frac 1 2 + \frac 1 {2^2} + \cdots
      | c = 
}}
{{eqn | l = \frac 1 {1 - \frac 1 3}
      | r = 1 + \frac 1 3 + \frac 1 {3^2} + \cdots
      | c = 
}}
{{eqn | l = \frac 1 {1 - \frac 1 5}
      | r = 1 + \frac 1 5 + \frac 1 {5^2} + \cdots
      | c = 
}}
{{eqn | o = \cdots
      | c = 
}}
{{eqn | l = \frac 1 {1 - \frac 1 {p_n} }
      | r = 1 + \frac 1 {p_n} + \frac 1 {p_n^2} + \cdots
      | c = 
}}
{{end-eqn}}
Consider what happens when all these series are multiplied together.
A new series will be generated whose terms consist of all possible products of one term selected from each of the series on the {{RHS}}.
This new series will converge in any order to the product of the terms on the {{LHS}}.
By the Fundamental Theorem of Arithmetic, every integer greater than $1$ is uniquely expressible as a product of powers of different primes.
Hence the product of these series is the series of reciprocals of all (strictly) positive integers whose prime factors are no greater than $p_n$.
In particular, all (strictly) positive integers up to $p_n$ have this property.
So:
:$\ds \prod_{k \mathop = 1}^n \frac 1 {1 - 1 / p_k}$
{{begin-eqn}}
{{eqn | l = \prod_{k \mathop = 1}^n \frac 1 {1 - 1 / p_k}
      | o = \ge
      | r = \sum_{k \mathop = 1}^{p_n} \frac 1 k
      | c = 
}}
{{eqn | o = >
      | r = \int_1^{p_n + 1} \dfrac {\d x} x
      | c = 
}}
{{eqn | r = \map \ln {p_n + 1}
      | c = 
}}
{{eqn | r = \ln p_n
      | c = 
}}
{{end-eqn}}
It follows by taking reciprocals that:
:$\ds \prod_{k \mathop = 1}^n \paren {1 - \frac 1 {p_k} } < \frac 1 {\ln p_n}$
Taking logarithms of each side:
:$(1): \quad \ds \sum_{k \mathop = 1}^n \map \ln {1 - \frac 1 {p_k} } < - \ln \ln p_n$
Next, note that the line $y = 2 x$ in the cartesian plane lies below the curve $y = \map \ln {1 + x}$ on the interval $\closedint {-\frac 1 2} 0$.
Also note that all primes are greater than or equal to $2$.
Thus it follows that:
:$-\dfrac 2 {p_k} < \map \ln {1 - \dfrac 1 {p_k} }$
Applying this to $(1)$ yields:
:$\ds -2 \sum_{k \mathop = 1}^n \dfrac 1 {p_k} < -\ln \ln p_n$
and so:
:$\ds \sum_{k \mathop = 1}^n \dfrac 1 {p_k} > \dfrac 1 2 \ln \ln p_n$
But:
:$\ds \lim_{n \mathop \to \infty} \ln \ln p_n \to \infty$
and so the series:
:$\ds \sum_{p \mathop \in \Bbb P} \frac 1 p$
is divergent.
{{qed}}
Theorem: Sum of Reciprocals of Primes is Divergent/Lemma

Let $C \in \R_{>0}$ be a (strictly) positive real number.
Then:
:$\ds \lim_{n \mathop \to \infty} \paren {\map \ln {\ln n} - C} = + \infty$

Proof:
Fix $c \in \R$.
It is sufficient to show there exists $N \in \N$, such that:
:$(1): \quad n \ge N \implies \map \ln {\ln n} - C > c$
Proceed as follows:
{{begin-eqn}}
{{eqn | l = \map \ln {\ln n} - C
      | o = >
      | r = c
}}
{{eqn | ll= \leadstoandfrom
      | l = \ln n
      | o = >
      | r = \map \exp {c + C}
      | c = {{Defof|Exponential Function/Real|subdef = Power Series Expansion|Exponential}}
}}
{{eqn | ll= \leadstoandfrom
      | l = n
      | o = >
      | r = \map \exp {\map \exp {c + C} }
      | c = {{Defof|Exponential Function/Real|subdef = Power Series Expansion|Exponential}}
}}
{{end-eqn}}
Let $N \in \N$ such that $N > \map \exp {\map \exp {c + C} }$.
By Logarithm is Strictly Increasing it follows that $N$ satisfies condition $(1)$.
Hence the result.
{{qed}}
Theorem: Strictly Increasing Infinite Sequence of Integers is Cofinal in Natural Numbers

Let $S = \left\langle{x_n}\right\rangle$ be an infinite sequence of integers which is strictly increasing.
Then $S$ is a cofinal subset of $\left({\Z, \le}\right)$ where $\le$ is the usual ordering on the integers.

Proof:
{{ProofWanted}}
Category:Integers
4lesc476t30awzjfte4szdcdh1hi33j
Theorem: Product of Even and Odd Functions

Let $\OO$ be an odd real function defined on some symmetric set $S$.
Let $\EE$ be an even real function defined on some symmetric set $S'$.
Let $\OO \EE$ be their pointwise product, defined on the intersection of the domains of $\OO$ and $\EE$.
Then $\OO \EE$ is odd. 
That is:
:$\forall x \in S \cap S': \map {\paren {\OO \EE}} {-x} = - \map {\paren {\OO \EE} } x$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\paren {\OO \EE} } {-x}
      | r = \map \OO {-x} \map \EE {-x}
      | c = {{Defof|Pointwise Multiplication of Real-Valued Functions}}
}}
{{eqn | r = -\map \OO x \map \EE x
      | c = as $\OO$ is odd and $\EE$ is even
}}
{{eqn | r = -\map {\paren {\OO \EE} } x
}}
{{end-eqn}}
The result follows from the definition of an odd function.
{{qed}}
Theorem: Dirichlet Integral

:$\ds \int_0^\infty \frac {\sin x} x \rd x = \frac \pi 2$

Proof:
By Fubini's Theorem:
:$\ds \int_0^\infty \paren {\int_0^\infty e^{- x y} \sin x \rd y} \rd x = \int_0^\infty \paren {\int_0^\infty e^{- x y} \sin x \rd x} \rd y$
Then:
{{begin-eqn}}
{{eqn | l = \int_0^\infty e^{- x y} \sin x \rd y
      | r = \intlimits {-e^{- x y} \frac {\sin x} x} 0 \infty 
      | c = Primitive of $e^{a x}$
}}
{{eqn | r = \frac {\sin x} x
      | c = 
}}
{{end-eqn}}
and:
{{begin-eqn}}
{{eqn | l = \int_0^\infty e^{- x y} \sin x \rd x
      | r = \intlimits {\frac {-e^{- x y} \paren {y \sin x + \cos x} } {y^2 + 1} } 0 \infty
      | c = Primitive of $e^{a x} \sin b x$
}}
{{eqn | r = \frac 1 {y^2 + 1}
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \int_0^\infty \frac {\sin x} x \rd x
      | r = \int_0^\infty \frac 1 {y^2 + 1} \rd y
      | c =
}}
{{eqn | r = \bigintlimits {\arctan y} 0 \infty
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn | r = \frac \pi 2
      | c = as $\ds \lim_{y \mathop \to \infty} \arctan y = \frac \pi 2$
}}
{{end-eqn}}
{{qed}}
Theorem: Dirichlet Integral

:$\ds \int_0^\infty \frac {\sin x} x \rd x = \frac \pi 2$

Proof:
By Modulus of Sine of x Less Than or Equal To Absolute Value of x:
:$\ds \size {\frac {e^{-\alpha x} \sin x} x} \le e^{-\alpha x}$
From Laplace Transform of Real Power: 
:$\ds \int_0^\infty e^{-\alpha x} x^0 \rd x = \frac {\map \Gamma {0 + 1} } {\alpha^{0 + 1} } = \frac 1 \alpha$
Hence by Comparison Test for Improper Integral:
:$\ds \int_0^\infty \frac {e^{-\alpha x} \sin x} x \rd x$
converges whenever $\alpha > 0$.
Therefore, we can define a real function $I : \openint 0 \infty \to \R$ by: 
:$\ds \map I \alpha = \int_0^\infty \frac {e^{-\alpha x} \sin x} x \rd x$
for each $\alpha \in \openint 0 \infty$.
Using Improper Integral of Partial Derivative on segments included in $\openint 0 \infty$:
{{begin-eqn}}
{{eqn | l = \map {I'} \alpha
      | r = \frac \partial {\partial \alpha} \int_0^\infty \frac {e^{-\alpha x} \sin x} x \rd x
}}
{{eqn | r = \int_0^\infty \frac \partial {\partial \alpha} \frac {e^{-\alpha x} \sin x} x \rd x
      | c = Leibniz's Integral Rule
}}
{{eqn | r = -\int_0^\infty e^{-\alpha x} \sin x \rd x
      | c = Derivative of Exponential Function
}}
{{eqn | r = \intlimits {-\frac {e^{-\alpha x} \paren {-\alpha \sin x - \cos x} } {\paren {-\alpha}^2 + 1} } 0 \infty 
      | c = Primitive of $e^{\alpha x} \sin b x$
}}
{{eqn | r = -\frac 1 {\alpha^2 + 1} 
}}
{{end-eqn}}
Therefore, by Derivative of Arctangent Function
:$\map I \alpha = -\arctan \alpha + K$
for some $K \in \R$.
We now observe:
{{begin-eqn}}
{{eqn | l = \lim_{\alpha \mathop \to \infty} \map I \alpha
      | r = \lim_{\alpha \mathop \to \infty} \int_0^\infty \frac {e^{-\alpha x} \sin x} x \rd x
      | c =
}}
{{eqn | r = 0
      | c = Exponential Tends to Zero and Infinity
}}
{{end-eqn}}
Therefore:
{{begin-eqn}}
{{eqn | l = \lim_{\alpha \mathop \to \infty} \map I \alpha
      | r = \lim_{\alpha \mathop \to \infty} -\arctan \alpha + K
      | c =
}}
{{eqn | ll = \leadsto
      | l = 0
      | r = -\frac \pi 2 + K
      | c = 
}}
{{eqn | ll = \leadsto
      | l = K
      | r = \frac \pi 2
      | c = 
}}
{{end-eqn}}
Therefore:
:$\map I \alpha = \dfrac \pi 2 - \arctan \alpha$
Setting $\alpha = 0$, we obtain:
{{begin-eqn}}
{{eqn | l = \int_0^\infty \frac {\sin x} x \rd x
      | r = \int_0^\infty \frac {e^{-\paren 0 x} \sin x} x \rd x
      | c = Exponential of Zero
}}
{{eqn | r = \map I 0
      | c =
}}
{{eqn | r = \frac \pi 2 - \arctan 0
      | c =
}}
{{eqn | r = \frac \pi 2
      | c = Arctangent of Zero is Zero
}}
{{eqn | ll = \leadsto
      | l = \int_0^\infty \frac {\sin x} x \rd x
      | r = \frac \pi 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Dirichlet Integral

:$\ds \int_0^\infty \frac {\sin x} x \rd x = \frac \pi 2$

Proof:
Let:
:$\map f x = \begin {cases} \dfrac {e^{i x} - 1} x & x \ne 0 \\ i & x = 0 \end {cases}$
We have, by Euler's Formula, for $x \in \R$:
:$\map \Im {\map f x} = \begin {cases} \dfrac {\sin x} x & x \ne 0 \\ 1 & x = 0 \end {cases}$
So: 
:$\ds \map \Im {\int_0^\infty \dfrac {e^{i x} - 1} x \rd x} = \int_0^\infty \dfrac {\sin x} x \rd x$
Let $C_R$ be the arc of the circle of radius $R$ centred at the origin connecting $R$ and $-R$ anticlockwise.
Let $\Gamma_R = C_R \cup \closedint {-R} R$.
Then, by Contour Integral of Concatenation of Contours:
:$\ds \oint_{\Gamma_R} \frac {e^{i x} - 1} x \rd x = \int_{C_R} \frac {e^{i x} - 1} x \rd x + \int_{-R}^R \frac {e^{i x} - 1} x \rd x$
From Linear Combination of Contour Integrals, we write: 
:$\ds \oint_{\Gamma_R} \frac {e^{i x} - 1} x \rd x = \int_{C_R} \frac {e^{i x} } x \rd x - \int_{C_R} \frac {\rd x} x + \int_{-R}^R \frac {e^{i x} - 1} x \rd x$
Note that $f$ is holomorphic inside our contour. 
It then follows from the Cauchy-Goursat Theorem, that:
:$\ds \oint_{\Gamma_R} \frac {e^{i x} - 1} x \rd x = 0$
We also have: 
{{begin-eqn}}
{{eqn	| l = \size {\int_{C_R} \frac { e^{i x} } x \rd x}
	    | o = \le
	    | r = \pi \max_{0 \mathop \le \theta \mathop \le \pi} \size {\frac 1 {R e^{i \theta} } }
	    | c = Jordan's Lemma
}}
{{eqn	| r = \frac \pi R
}}
{{eqn	| o = \to
	    | r = 0
	    | c = as $R \to \infty$
}}
{{end-eqn}}
Therefore: 
:$\ds \lim_{R \mathop \to \infty} \int_{C_R} \frac {\rd x} x = \lim_{R \mathop \to \infty} \int_{-R}^R \frac {e^{i x} - 1} x \rd x = \int_{-\infty}^\infty \frac {e^{i x} - 1} x \rd x$
Evaluating the integral on the {{LHS}}: 
{{begin-eqn}}
{{eqn	| l = \int_{C_R} \frac {\rd x} x
	    | r = \int_0^\pi \frac {i R e^{i \theta} } {R e^{i \theta} } \rd \theta
	    | c = {{Defof|Complex Contour Integral}}
}}
{{eqn	| r = i \int_0^\pi \rd \theta
}}
{{eqn	| r = \pi i
}}
{{end-eqn}}
So:
:$\ds \int_{-\infty}^\infty \frac {e^{i x} - 1} x \rd x = \pi i$
Taking the imaginary part:
:$\ds \int_{-\infty}^\infty \frac {\sin x} x \rd x = \pi$
From Definite Integral of Even Function:
:$\ds \int_{-\infty}^\infty \frac {\sin x} x \rd x = 2 \int_0^\infty \frac {\sin x} x \rd x$
Hence: 
:$\ds \int_0^\infty \frac {\sin x} x \rd x = \frac \pi 2$
{{qed}}
Theorem: Dirichlet Integral

:$\ds \int_0^\infty \frac {\sin x} x \rd x = \frac \pi 2$

Proof:
From Integral to Infinity of Function over Argument:
:$\ds \int_0^\infty {\dfrac {\map f x} x} = \int_0^{\to \infty} \map F u \rd u$
for a real function $f$ and its Laplace transform $\laptrans f = F$, provided they exist.
Let $\map f x := \sin x$.
Then from Laplace Transform of Sine:
:$\laptrans {\map f x} = \dfrac 1 {s^2 + 1}$
Hence:
{{begin-eqn}}
{{eqn | l = \int_0^\infty \frac {\sin x} x \rd x
      | r = \int_0^{\to \infty} \dfrac {\d u} {u^2 + 1}
      | c = 
}}
{{eqn | r = \bigintlimits {\arctan u} 0 \infty
      | c = Primitive of $\dfrac 1 {x^2 + a^2}$
}}
{{eqn | r = \dfrac \pi 2
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Riemann Zeta Function and Prime Counting Function

For $\map \Re s > 1$:
:$\ds \log \map \zeta s = s \int_0^{\mathop \to \infty} \frac {\map \pi x} {x \paren {x^s - 1} } \rd x$
where:
:$\zeta$ denotes the Riemann Zeta Function
:$\pi$ denotes the Prime-Counting Function.

Proof:
From the definition of the Riemann Zeta Function: 
{{begin-eqn}}
{{eqn | l = \map \zeta s
      | r = \prod_p \frac 1 {1 - p^{-s} }
      | c =
}}
{{eqn | ll= \leadsto
      | l = \log \map \zeta s
      | r = \log \prod_p \frac 1 {1 - p^{-s} } 
      | c = 
}}
{{eqn | r = \sum_p \map \log {\frac 1 {1 - p^{-s} } }
      | c = Sum of Logarithms
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \paren {\map \pi n - \map \pi {n - 1} } \map \log {\frac 1 {1 - n^{-s} } }
      | c = {{Defof|Prime-Counting Function}}
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \map \pi n \paren {\map \log {\frac 1 {1 - n^{-s} } } - \map \log {\frac 1 {1 - \paren {n + 1}^{-s} } } }
      | c = as $\map \pi {-1} = 0$
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty \map \pi n \paren {\map \log {1 - \paren {n + 1}^{-s} } - \map \log {1 - n^{-s} } }
      | c = Logarithm of Power
}}
{{end-eqn}}
By Derivative of Logarithm Function and the Chain Rule for Derivatives:
{{begin-eqn}}
{{eqn | l = \frac \d {\d x} \map \log {1 - x^{-s} }
      | r = \frac {s x^{- s - 1} } {1 - x^{-s} }
      | c = 
}}
{{eqn | r = \frac s {x \paren {x^s - 1} }
      | c = 
}}
{{end-eqn}}
Hence:
{{begin-eqn}}
{{eqn | l = \log \map \zeta s
      | r = \sum_{n \mathop = 0}^\infty \map \pi n \int_n^{n + 1} \frac s {x \paren {x^s - 1} } \rd x
      | c = Fundamental Theorem of Calculus
}}
{{eqn | r = \sum_{n \mathop = 0}^\infty s \int_n^{n + 1} \frac {\map \pi x} {x \paren {x^s - 1} } \rd x
      | c = 
}}
{{eqn | r = s \int_0^{\mathop \to \infty} \frac {\map \pi x} {x \paren {x^s - 1} } \rd x
      | c = 
}}
{{end-eqn}}
{{qed}}
Category:Riemann Zeta Function
Category:Number Theory
iirjiaopxt9eynzrfc8tg03evk25jmt
Theorem: Complex Exponential Tends to Zero

Let $\exp z$ be the complex exponential function.
Then:
:$\ds \lim_{\map \Re z \mathop \to +\infty} e^{-z} = 0$
where $\map \Re z$ denotes the real part of $z$.

Proof:
Let $z = x + iy$.
Let $\epsilon > 0$.
By the definition of limits at infinity, we need to show that there is some $M > 0$ such that:
:$x > M \implies \size {e^{-z} - 0} < \epsilon$
But:
{{begin-eqn}}
{{eqn | l = \size {e^{-z} - 0}
      | r = \size {e^{-z} }
}}
{{eqn | r = \size {e^{-x} }
      | c = Modulus of Exponential is Modulus of Real Part
}}
{{eqn | r = \size {e^{-x} - 0}
}}
{{end-eqn}}
so we need an $M$ such that:
:$x > M \implies \size {e^{-x} - 0} < \epsilon$
This is the definition of the limits at infinity of the ''real'' exponential.
The result follows from Exponential Tends to Zero and Infinity.
{{qed}}
Category:Exponential Function
53fi1qi3cf4sygogeuboajj3tlfvp34
Theorem: Modulus of Exponential is Exponential of Real Part

Let $z \in \C$ be a complex number.
Let $\exp z$ denote the complex exponential function.
Let $\cmod {\, \cdot \,}$ denote the complex modulus
Then:
:$\cmod {\exp z} = \map \exp {\map \Re z}$
where $\map \Re z$ denotes the real part of $z$.

Proof:
Let $z = x + iy$.
{{begin-eqn}}
{{eqn | l = \cmod {\exp z}
      | r = \cmod {\map \exp {x + iy} }
}}
{{eqn | r = \cmod {\paren {\exp x} \paren {\exp i y} }
      | c = Exponential of Sum
}}
{{eqn | r = \cmod {\exp x} \cmod {\exp i y}
      | c = Modulus of Product
}}
{{eqn | r = \cmod {\exp x}
      | c = Modulus of Exponential of Imaginary Number is One
}}
{{eqn | r = e^x
      | c = Exponential of Real Number is Strictly Positive
}}
{{eqn | r = \map \exp {\map \Re z}
      | c = {{Defof|Real Part}}
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Exponential/Real Argument

Let $\laptrans f$ denote the Laplace transform of a function $f$.
Let $e^x$ be the real exponential.
Then:
:$\map {\laptrans {e^{a t} } } s = \dfrac 1 {s - a}$
where $a \in \R$ is constant, and $\map \Re s > \map \Re a$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {e^{a t} } } s
      | r = \int_0^{\to +\infty} e^{-s t} e^{a t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^{\to +\infty} e^{\paren {a - s} t} \rd t
      | c = Exponential of Sum
}}
{{eqn | r = \lim_{L \mathop \to \infty} \int_0^L e^{\paren {a - s} t} \rd t
      | c = {{Defof|Improper Integral}}
}}
{{eqn | r = \lim_{L \mathop \to \infty} \intlimits {\frac 1 {a - s} e^{\paren {a - s} t} } 0 L
      | c = Primitive of Exponential Function, Integration by Substitution
}}
{{eqn | r = \lim_{L \mathop \to \infty} \frac 1 {a - s} \paren {e^{\paren {a - s} L} - e^{\paren {a - s} 0} }
      | c = 
}}
{{eqn | r = \lim_{L \mathop \to \infty} \frac 1 {s - a} \paren {1 - e^{\paren {a - s} L} }
      | c = Exponential of Zero and rearranging
}}
{{end-eqn}}
Because $s > a$, we have that $a - s < 0$.
Hence:
:$\ds \lim_{L \mathop \to \infty} \paren {a - s} L \to -\infty$
So:
{{begin-eqn}}
{{eqn | l = \lim_{L \mathop \to \infty} \frac 1 {s - a} \paren {1 - e^{\paren {a - s} L} }
      | r = \frac 1 {s - a} \paren {1 - 0}
      | c = Exponential Tends to Zero
}}
{{eqn | r = \frac 1 {s - a}
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Exponential/Real Argument

Let $\laptrans f$ denote the Laplace transform of a function $f$.
Let $e^x$ be the real exponential.
Then:
:$\map {\laptrans {e^{a t} } } s = \dfrac 1 {s - a}$
where $a \in \R$ is constant, and $\map \Re s > \map \Re a$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {e^{a t} } } s
      | r = \map {\laptrans {1 \times e^{a t} } } s
      | c = 
}}
{{eqn | r = \map {\laptrans 1} {s - a}
      | c = First Translation Property of Laplace Transforms
}}
{{eqn | r = \frac 1 {s - a}
      | c = Laplace Transform of Constant Mapping
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Cosine

Let $\cos$ be the real cosine function.
Let $\laptrans f$ denote the Laplace transform of the real function $f$.
Then:
:$\laptrans {\cos a t} = \dfrac s {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > a$.

Proof:
Let $\map f t := \map \Ci t = \ds \int_t^\infty \dfrac {\cos u} u \rd u$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f'} t
      | r = -\dfrac {\cos t} t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = t \map {f'} t
      | r = -\cos t
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {t \map {f'} t}
      | r = -\laptrans {\cos t}
      | c = 
}}
{{eqn | r = -\dfrac s {s^2 + 1}
      | c = Laplace Transform of Cosine
}}
{{eqn | ll= \leadsto
      | l = -\dfrac \d {\d s} \laptrans {\map {f'} t}
      | r = -\dfrac s {s^2 + 1}
      | c = Derivative of Laplace Transform
}}
{{eqn | ll= \leadsto
      | l = \map {\dfrac \d {\d s} } {s \laptrans {\map f t} - \map f 0}
      | r = \dfrac s {s^2 + 1}
      | c = Laplace Transform of Derivative
}}
{{eqn | ll= \leadsto
      | l = s \laptrans {\map f t}
      | r = \int \dfrac s {s^2 + 1} \rd s
      | c = $\map f 0 = 0$, and integrating both sides {{WRT|Integration}} $s$
}}
{{eqn | ll= \leadsto
      | l = s \laptrans {\map f t}
      | r = \dfrac 1 2 \map \ln {s^2 + 1} + C
      | c = Primitive of $\dfrac x {x^2 + a^2}$
}}
{{end-eqn}}
By the Initial Value Theorem of Laplace Transform:
:$\ds \lim_{s \mathop \to \infty} s \laptrans {\map f t} = \lim_{t \mathop \to 0} \map f t = \map f 0 = 0$
which leads to:
:$c = 0$
Thus:
{{begin-eqn}}
{{eqn | l = s \laptrans {\map f t}
      | r = \dfrac 1 2 \map \ln {s^2 + 1}
      | c = 
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\map f t}
      | r = \dfrac {\map \ln {s^2 + 1} } {2 s}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Cosine

Let $\cos$ be the real cosine function.
Let $\laptrans f$ denote the Laplace transform of the real function $f$.
Then:
:$\laptrans {\cos a t} = \dfrac s {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > a$.

Proof:
Let $\map f t = \sin \sqrt t$.
Then:
{{begin-eqn}}
{{eqn | l = \map {f'} t
      | r = \dfrac {\cos \sqrt t} {2 \sqrt t}
      | c = 
}}
{{eqn | l = \map f 0
      | r = 0
      | c = 
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = \laptrans {\map {f'} t}
      | r = \dfrac 1 2 \laptrans {\dfrac {\cos \sqrt t} {\sqrt t} }
      | c = 
}}
{{eqn | r = s \map F s - \map f 0
      | c = Laplace Transform of Derivative
}}
{{eqn | r = \dfrac {\sqrt \pi} {2 s^{1/2} } \map \exp {-\dfrac 1 {4 s} }
      | c = Laplace Transform of Sine of Root
}}
{{eqn | ll= \leadsto
      | l = \laptrans {\dfrac {\cos \sqrt t} {\sqrt t} }
      | r = \sqrt {\dfrac \pi s} \map \exp {-\dfrac 1 {4 s} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Cosine

Let $\cos$ be the real cosine function.
Let $\laptrans f$ denote the Laplace transform of the real function $f$.
Then:
:$\laptrans {\cos a t} = \dfrac s {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > a$.

Proof:
{{begin-eqn}}
{{eqn | l = \map {\laptrans {\cos {a t} } } s
      | r = \int_0^{\to +\infty} e^{-s t} \cos {a t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \lim_{L \mathop \to \infty} \int_0^L e^{-s t} \cos {a t} \rd t
      | c = {{Defof|Improper Integral}}
}}
{{eqn | r = \lim_{L \mathop \to \infty} \intlimits {\frac {e^{-s t} \paren {-s \cos a t + a \sin a t} } {\paren {-s}^2 + a^2} } 0 L
      | c = Primitive of $e^{a x} \cos b x$
}}
{{eqn | r = \lim_{L \mathop \to \infty} \paren {\frac {e^{-s L} \paren {-s \cos a L + a \sin a L} } {s^2 + a^2} - \frac {e^{-s \times 0} \paren {-s \, \map \cos {0 \times a} + a \, \map \sin {0 \times a} } } {s^2 + a^2} }
      | c = 
}}
{{eqn | r = \lim_{L \mathop \to \infty} \paren {\frac {s \, \map \cos {0 \times a} - a \, \map \sin {0 \times a} } {s^2 + a^2} - \frac {e^{-s L} \paren {s \cos a L - a \sin a L} } {s^2 + a^2} }
      | c = rearranging
}}
{{eqn | r = \frac {s \, \map \cos {0 \times a} - a \, \map \sin {0 \times a} } {s^2 + a^2} - 0
      | c = Exponential Tends to Zero
}}
{{eqn | r = \frac {s \cos 0 - a \sin 0} {s^2 + a^2}
      | c = simplifying
}}
{{eqn | r = \frac s {s^2 + a^2}
      | c = Sine of Zero is Zero, Cosine of Zero is One
}}
{{end-eqn}}
{{qed}}
Theorem: Laplace Transform of Cosine

Let $\cos$ be the real cosine function.
Let $\laptrans f$ denote the Laplace transform of the real function $f$.
Then:
:$\laptrans {\cos a t} = \dfrac s {s^2 + a^2}$
where $a \in \R_{>0}$ is constant, and $\map \Re s > a$.

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {e^{i a t} }
      | r = \frac 1 {s - i a}
      | c = Laplace Transform of Exponential
}}
{{eqn | r = \frac {s + i a} {s^2 + a^2}
      | c = multiply top and bottom by $s + i a$
}} 
{{end-eqn}}
Also:
{{begin-eqn}}
{{eqn | l = \laptrans {e^{i a t} }
      | r = \laptrans {\cos a t + i \sin a t}
      | c = Euler's Formula
}}
{{eqn | r = \laptrans {\cos a t} + i \laptrans {\sin a t}
      | c = Linear Combination of Laplace Transforms
}}
{{end-eqn}}
So:
{{begin-eqn}}
{{eqn | l = \laptrans {\cos a t}
      | r = \map \Re {\laptrans {e^{i a t} } }
}}
{{eqn | r = \map \Re {\frac {s + i a} {s^2 + a^2} }
}}
{{eqn | r = \frac s {s^2 + a^2}
}}
{{end-eqn}}
{{qed}}