avewright/proofwiki-math huggingface dataset:
Theorem: Exponential of Real Number is Strictly Positive

Let $x$ be a real number.
Let $\exp$ denote the (real) exponential function.
Then:
:$\forall x \in \R : \exp x > 0$

Proof:
This proof assumes the limit definition of $\exp$.
That is, let:
:$\ds \exp x = \lim_{n \mathop \to \infty} \map {f_n} x$
where $\map {f_n} x = \paren {1 + \dfrac x n}^n$
First, fix $x \in \R$.
Let $N = \ceiling {\size x}$, where $\ceiling {\, \cdot \,}$ denotes the ceiling function.
Then:
{{begin-eqn}}
{{eqn | l = \exp x
      | r = \lim_{n \mathop \to \infty} \map {f_n} x
}}
{{eqn | r = \lim_{n \mathop \to \infty} \map {f_{n + N} } x
      | c = Tail of Convergent Sequence
}}
{{eqn | o = \ge
      | r = \map {f_{n + N} } x
      | c = Exponential Sequence is Eventually Increasing and Limit of Bounded Convergent Sequence is Bounded
}}
{{eqn | o = >
      | r = 0
      | c = Corollary to Exponential Sequence is Eventually Increasing
}}
{{end-eqn}}
{{MissingLinks|Corollary to Exponential Sequence is Eventually Increasing does not actually exist. The page it gets sent to does not give that result.}}
{{qed}}
Theorem: Exponential of Real Number is Strictly Positive

Let $x$ be a real number.
Let $\exp$ denote the (real) exponential function.
Then:
:$\forall x \in \R : \exp x > 0$

Proof:
This proof assumes the definition of $\exp x$ as the unique continuous extension of $e^x$.
Since $e > 0$, the result follows immediately from Power of Positive Real Number is Positive over Rationals.
{{qed}}
Theorem: Exponential of Real Number is Strictly Positive

Let $x$ be a real number.
Let $\exp$ denote the (real) exponential function.
Then:
:$\forall x \in \R : \exp x > 0$

Proof:
This proof assumes the definition of $\exp$ as the inverse mapping of extension of $\ln$, where $\ln$ denotes the natural logarithm.
Recall that the domain of $\ln$ is $\R_{>0}$.
From the definition of inverse mapping, the image of $\exp$ is the domain of $\ln$.
That is, the image of $\exp$ is $\R_{>0}$.
Hence the result.
{{qed}}
Theorem: Exponential of Real Number is Strictly Positive

Let $x$ be a real number.
Let $\exp$ denote the (real) exponential function.
Then:
:$\forall x \in \R : \exp x > 0$

Proof:
This proof assumes the definition of $\exp$ as the solution to an initial value problem.
That is, suppose $\exp$ satisfies:
:$ (1): \quad D_x \exp x = \exp x$
:$ (2): \quad \map \exp 0 = 1$
on $\R$.
=== Lemma ===
{{:Exponential of Real Number is Strictly Positive/Proof 5/Lemma}}{{qed|lemma}}
{{AimForCont}} that $\exists \alpha \in \R: \exp \alpha < 0$.
Then $0 \in \openint {\exp \alpha} 1$.
From Intermediate Value Theorem:
:$\exists \zeta \in \openint \alpha 0: \map f \zeta = 0$
This contradicts the lemma.
{{qed}}
Theorem: Real Power of Strictly Positive Real Number is Strictly Positive

Let $x$ be a strictly positive real number.
Let $y$ be a real number.
Then:
:$x^y > 0$
where $x^y$ denotes $x$ raised to the $y$th power.

Proof:
From the definition of power:
:$x^y = \exp \left({y \ln x}\right)$
From Exponential of Real Number is Strictly Positive:
:$x^y = \exp \left({y \ln x}\right) > 0$
{{qed}}
Category:Real Analysis
oa8bjlxwrg5kas1mcyixm085z7x58vm
Theorem: Derivative of Power of Function

Let $\map u x$ be a differentiable real function of $x$.
Let $n$ be a real number such that $n \ne -1$.
Then:
:$\map {\dfrac \d {\d x} } {\map u x^n} = n \map u x^{n - 1} \map {\dfrac \d {\d x} } {\map u x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\frac \d {\d x} } {\map u x^n}
      | r = \map {\frac \d {\d u} } {\map u x^n} \map {\frac \d {\d x} } {\map u x}
      | c = Chain Rule for Derivatives
}}
{{eqn | r = n \map u x^{n - 1} \map {\frac {\d u} {\d x} } {\map u x}
      | c = Derivative of Hyperbolic Sine
}}
{{end-eqn}}
{{qed}}
Theorem: Derivative of Power of Function

Let $\map u x$ be a differentiable real function of $x$.
Let $n$ be a real number such that $n \ne -1$.
Then:
:$\map {\dfrac \d {\d x} } {\map u x^n} = n \map u x^{n - 1} \map {\dfrac \d {\d x} } {\map u x}$

Proof:
{{begin-eqn}}
{{eqn | l = \map {\dfrac \d {\d x} } {\map u x^n}
      | r = \lim_{h \mathop \to 0} \frac {\paren {\map u {x + h} }^n - \paren {\map u x}^n} h
      | c = 
}}
{{eqn | r = \paren {\map u x}^n \lim_{h \mathop \to 0} \frac {\paren {\frac {\map u {x + h} } {\map u x} }^n - 1} h
      | c = Power of Product
}}
{{eqn | r = \paren {\map u x}^n \lim_{h \mathop \to 0} \frac {\exp \paren {n \ln \frac {\map u {x + h} } {\map u x} } - 1} h
      | c = {{Defof|Power to Real Number}}
}}
{{eqn | r = \paren {\map u x}^n \lim_{h \mathop \to 0} \paren {\frac {\map \exp {n \ln \frac {\map u {x + h} } {\map u x} } - 1} {n \ln \frac {\map u {x + h} } {\map u x} } } \paren {\frac {n \ln \frac {\map u {x + h} } {\map u x} } h}
      | c = 
}}
{{eqn | r = \paren {\map u x}^n \lim_{h \mathop \to 0} \frac {n \ln \frac {\map u {x + h} } {\map u x} } h
      | c = Derivative of Exponential at Zero
}}
{{eqn | r = n \paren {\map u x}^n \lim_{h \mathop \to 0} \frac {\ln \frac {\map u {x + h} } {\map u x} } h
      | c = 
}}
{{eqn | r = n \paren {\map u x}^n \lim_{h \mathop \to 0} \frac {\map \ln {1 + \frac {\map u {x + h} - \map u x} {\map u x} } } h
      | c = 
}}
{{eqn | r = n \paren {\map u x}^n \lim_{h \mathop \to 0} \paren {\frac {\map \ln {1 + \frac {\map u {x + h} - \map u x} {\map u x} } } {\frac {\map u {x + h} - \map u x} {\map u x} } } \paren {\frac {\frac {\map u {x + h} - \map u x} {\map u x} } h }
      | c = 
}}
{{eqn | r = n \paren {\map u x}^n \lim_{h \mathop \to 0} \frac {\paren {\frac {\map u {x + h} - \map u x} {\map u x} } } h
      | c = Derivative of Logarithm at One
}}
{{eqn | r = n \paren {\map u x}^n \lim_{h \mathop \to 0} \frac 1 {\map u x} \frac {\map u {x + h} - \map u x} h
      | c = 
}}
{{eqn | r = n \paren {\map u x}^{n - 1} \lim_{h \mathop \to 0} \frac {\map u {x + h} - \map u x} h
      | c = Product of Powers
}}
{{eqn | r = n \paren {\map u x}^{n - 1} \map {\dfrac \d {\d x} } {\map u x}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Natural Logarithm of e is 1

:$\ln e = 1$

Proof:
The definition of the Euler's number as the Base of Logarithm will be used.
Then the result follows directly.
{{qed}}
Theorem: Real Area Hyperbolic Cosine is Strictly Increasing

The real area hyperbolic cosine function is strictly increasing, that is:
:$\forall x, y \ge 1 : x < y \implies \arcosh x < \arcosh y$

Proof:
{{begin-eqn}}
{{eqn | n = 1
      | l = x
      | o = <
      | r = y
      | c = Assumption
}}
{{eqn | ll= \leadsto
      | l = x^2
      | o = <
      | r = y^2
      | c = {{Real-number-axiom|O2}}
}}
{{eqn | ll= \leadsto
      | l = x^2 - 1
      | o = <
      | r = y^2 - 1
      | c = 
}}
{{eqn | n = 2
      | ll= \leadsto
      | l = \sqrt {x^2 - 1}
      | o = <
      | r = \sqrt {y^2 - 1}
      | c = Square Root is Strictly Increasing
}}
{{eqn | ll= \leadsto
      | l = x + \sqrt {x^2 - 1}
      | o = <
      | r = y + \sqrt {y^2 - 1}
      | c = $(1) + (2)$
}}
{{eqn | ll= \leadsto
      | l = \arcosh x
      | o = <
      | r = \arcosh y
      | c = {{Defof|Real Inverse Hyperbolic Cosine}}
}}
{{end-eqn}}
{{qed}}
Category:Inverse Hyperbolic Cosine
Category:Examples of Strictly Increasing Real Functions
ccjo3q1hwak65t6s59ojnh0o2oizvmm
Theorem: Laplace Transform of Function of Constant Multiple

Let $a \in \C$ or $\R$ be constant.
Then:
:$a \laptrans {\map f {a t} } = \map F {\dfrac s a}$

Proof:
{{begin-eqn}}
{{eqn | l = a \laptrans {\map f {a t} }
      | r = a \int_0^{\to + \infty} e^{-s t} \map f {a t} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = a \paren {\frac 1 a} \int_0^{\to + \infty} e^{-s t} \map f {a t} \rd \paren {a t}
      | c = Primitive of Function of Constant Multiple
}}
{{eqn | r = \int_0^{\to + \infty} e^{-u a t} \map f {a t} \rd \paren {a t}
      | c = where $u = \dfrac s a$
}}
{{eqn | r = \int_0^{\to + \infty} e^{-u a t} \map f {a t} \rd \paren {a t}
}}
{{eqn | r = \map F u
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \map F {\dfrac s a}
}}
{{end-eqn}}
{{qed}}
Theorem: Second Translation Property of Laplace Transforms

Let $g$ be the function defined as:
:$\map g t = \begin {cases} \map f {t - a} & : t > a \\ 0 & : t \le a \end {cases}$
Then:
:$\laptrans {\map g t} = e^{-a s} \map F s$

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map f t}
      | r = \exp \dfrac {-2 \pi s} 3 \laptrans {\cos t}
      | c = Second Translation Property of Laplace Transforms
}}
{{eqn | r = \exp \dfrac {-2 \pi s} 3 \dfrac s {s^2 + 1}
      | c = Laplace Transform of Cosine
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Second Translation Property of Laplace Transforms

Let $g$ be the function defined as:
:$\map g t = \begin {cases} \map f {t - a} & : t > a \\ 0 & : t \le a \end {cases}$
Then:
:$\laptrans {\map g t} = e^{-a s} \map F s$

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map f t}
      | r = \int_0^\infty e^{-s t} \map f t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^{\frac {-2 \pi s} 3} e^{-s t} \map f t \rd t + \int_{\frac {-2 \pi s} 3}^\infty e^{-s t} \map f t \rd t
      | c = 
}}
{{eqn | r = \int_0^{\frac {-2 \pi s} 3} e^{-s t} \times 0 \rd t + \int_{\frac {-2 \pi s} 3}^\infty e^{-s t} \map \cos {t - \dfrac {2 \pi} 3} \rd t
      | c = Definition of $f$
}}
{{eqn | r = \int_0^\infty e^{-s \paren {u + 2 \pi / 3} } \map \cos u \rd u
      | c = Integration by Substitution: $t = u + \dfrac {2 \pi} 3$
}}
{{eqn | r = \exp \dfrac {-2 \pi s} 3 \int_0^\infty e^{-s u} \map \cos u \rd u
      | c = 
}}
{{eqn | r = \exp \dfrac {-2 \pi s} 3 \laptrans {\cos u}
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \exp \dfrac {-2 \pi s} 3 \dfrac s {s^2 + 1}
      | c = Laplace Transform of Cosine
}}
{{end-eqn}}
and the result follows.
{{qed}}
Theorem: Second Translation Property of Laplace Transforms

Let $g$ be the function defined as:
:$\map g t = \begin {cases} \map f {t - a} & : t > a \\ 0 & : t \le a \end {cases}$
Then:
:$\laptrans {\map g t} = e^{-a s} \map F s$

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map f {t - a} }
      | r = \int_0^{\to + \infty} e^{-s t} \map f {t - a} \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^{\to + \infty} e^{-s \paren {t - a} } e^{-a s} \map f {t - a} \rd \paren {t - a}
      | c = 
}}
{{eqn | r = e^{-a s} \int_0^{\to + \infty} e^{-s \paren {t - a} } \map f {t - a} \rd \paren {t - a}
      | c = 
}}
{{eqn | r = e^{-a s}\map F s
      | c = {{Defof|Laplace Transform}}
}}
{{end-eqn}}
{{qed}}
Theorem: Second Translation Property of Laplace Transforms

Let $g$ be the function defined as:
:$\map g t = \begin {cases} \map f {t - a} & : t > a \\ 0 & : t \le a \end {cases}$
Then:
:$\laptrans {\map g t} = e^{-a s} \map F s$

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map g t}
      | r = \int_0^\infty e^{-s t} \map g t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int_0^a e^{-s t} \map g t \rd t + \int_a^\infty e^{-s t} \map g t \rd t
      | c = 
}}
{{eqn | r = \int_0^a 0 \times e^{-s t} \rd t + \int_a^\infty e^{-s t} \map f {t - a} \rd t
      | c = Definition of $\map g t$
}}
{{eqn | r = \int_a^\infty e^{-s t} \map f {t - a} \rd t
      | c = 
}}
{{eqn | r = \int_0^\infty e^{-s \paren {u + a} } \map f u \rd u
      | c = Integration by Substitution: $t = u + a$
}}
{{eqn | r = e^{-a s} \int_0^\infty e^{-s u} \map f u \rd u
      | c = 
}}
{{eqn | r = e^{-a s} \map F s
      | c = {{Defof|Laplace Transform}}
}}
{{end-eqn}}
{{qed}}
Theorem: Seifert-van Kampen Theorem

The functor $\pi_1 : \mathbf{Top_\bullet} \to \mathbf{Grp}$ preserves pushouts of inclusions.

Proof:
Let $\struct {X, \tau}$ be a topological space.
Let $U_1, U_2 \in \tau$ such that:
: $U_1 \cup U_2 = X$
: $U_1 \cap U_2 \ne \O$ is connected
Let $\ast \in U_1 \cap U_2$.
Let:
: $i_k : U_1 \cap U_2 \hookrightarrow U_k$
: $j_k : U_k \hookrightarrow U_1 \cup U_2$
be inclusions.
For simplicity, let:
:$\map {\pi_1} X = \map {\pi_1} {X, \ast}$
It is to be shown that $\map {\pi_1} X$ is the amalgamated free product:
:$\map {\pi_1} {U_1} *_{\map {\pi_1} {U_1 \cap U_2} } \map {\pi_1} {U_2}$
{{ProofWanted}}
{{Namedfor|Karl Johannes Herbert Seifert|name2 = Egbert Rudolf van Kampen|cat = Seifert|cat2 = van Kampen}}
Category:Category Theory
mp40a0v6x0sfddtexnp7q51sqz8gjw6
Theorem: Functions of Independent Random Variables are Independent

Let $X$ and $Y$ be independent random variables on a probability space $\struct {\Omega, \Sigma, \Pr}$.
Let $g$ and $h$ be real-valued functions defined on the codomains of $X$ and $Y$ respectively.
Then $\map g X$ and $\map h Y$ are independent random variables.

Proof:
Let $A$ and $B$ be subsets of the real numbers $\R$.
Let $g^{-1} \sqbrk A$ and $h^{-1} \sqbrk B$ denote the preimages of $A$ and $B$ under $g$ and $h$ respectively. 
Applying the definition of independent random variables:
{{begin-eqn}}
{{eqn | l = \map \Pr {\map g X \in A, \map h Y \in B}
      | r = \map \Pr {X \in g^{-1} \sqbrk A, Y \in h^{-1} \sqbrk B}
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{eqn | r = \map \Pr {X \in g^{-1} \sqbrk A} \map \Pr {Y \in h^{-1} \sqbrk B}
      | c = {{Defof|Independent Random Variables}}
}}
{{eqn | r = \map \Pr {\map g X \in A} \map \Pr {\map h Y \in B}
      | c = {{Defof|Preimage of Subset under Mapping}}
}}
{{end-eqn}}
Hence $\map g X$ and $\map h Y$ are independent random variables.
{{qed}}
Theorem: Multiplication Property of Characteristic Functions

Let $X$ and $Y$ be independent random variables on a probability space $\struct {\Omega, \Sigma, \Pr}$.
Let $\phi_X$ and $\phi_Y$ denote the characteristic functions of $X$ and $Y$ respectively.
Then:
:$\phi_{X + Y} = \phi_X \phi_Y$

Proof:
Let $i = \sqrt{-1}$.
Let $\expect X$ denote the expectation of $X$.
{{begin-eqn}}
{{eqn | l = \map {\phi_{X + Y} } t
      | r = \expect {e^{i t \paren {X + Y} } }
      | c = {{Defof|Characteristic Function of Random Variable}}
}}
{{eqn | r = \expect {e^{i t X} e^{i t Y} }
      | c = 
}}
{{eqn | r = \expect {e^{i t X} } \expect {e^{ i t Y} }
      | c = Functions of Independent Random Variables are Independent, Expected Value of Product is Product of Expected Value
}}
{{eqn | r = \map {\phi_X} t \map {\phi_Y} t
      | c = 
}}
{{end-eqn}}
Hence: 
:$\phi_{X + Y} = \phi_X \phi_Y$
{{qed}}
Theorem: Relationship between Limit Inferior and Lower Limit

Let $\struct {S, \tau}$ be a topological space.
Let $f: S \to \R \cup \set {-\infty, \infty}$ be an extended real-valued function.
Let $\sequence {s_n}_{n \mathop \in \N}$ be a convergent sequence in $S$ such that $s_n \to \bar s$.
Then the lower limit of $f$ at $\bar s$ is bounded above by the limit inferior of $\sequence {\map f {s_n} }$:
:$\ds \liminf_{s \mathop \to \bar s} \map f s \le \liminf_{n \mathop \to \infty} \map f {s_n}$

Proof:
Let $\NN_{\bar s}$ denote the neighborhood filter of $\bar s$.
By definition of the lower limit, there exists a sequence of open neighborhoods $\sequence {V_k}_{k \mathop \in \N} \in \NN_{\bar s}$ such that:
:$\ds \lim_{k \mathop \to \infty} \set {\inf_{s \mathop \in V_k} \map f s} = \liminf_{s \mathop \to \bar s} \map f s$
This implies that $\forall \epsilon > 0 \exists k_\epsilon \in \N$ such that:
:$\ds \inf_{s \mathop \in V_{k_\epsilon} } \map f s \ge \liminf_{s \mathop \to \bar s} \map f s - \epsilon$
By our hypothesis $s_n \to \bar s$ and because $V_{k_\epsilon} \in N_{\bar s}$ there exists $\map N {k_\epsilon} \in \N$ such that:
:$\ds \forall n \ge \map N {k_\epsilon}: s_n \in V_{k_\epsilon}$
Consequently:
{{begin-eqn}}
{{eqn | o = \le
      | l = \inf_{s \mathop \in V_{k_\epsilon} } \map f s
      | r = \inf_{n \mathop \ge \map N {k_\epsilon} } \map f {s_n}
      | c = because $\set {s_n : n \ge \map N {k_\epsilon} } \subseteq V_{k_\epsilon}$
}}
{{eqn | o = \le
      | r = \sup_{N \mathop \in \N} \set {\inf_{n \mathop \ge N} \map f {s_n} }
      | c = {{Defof|Supremum}}
}}
{{eqn | r = \liminf_{n \mathop \to \infty} \map f {s_n}
      | c = {{Defof|Limit Inferior}}
}}
{{end-eqn}}
Combining these estimates, it follows that for all $\epsilon > 0$:
:$\ds \liminf_{s \mathop \to \bar s} \map f s \le \liminf_{n \mathop \to \infty} \map f {s_n} + \epsilon$
Hence the result.
{{qed}}
Category:Topology
f20revgqbqmujlqx1prnqddmx2wndnc
Theorem: Group is Abelian iff Opposite Group is Itself

Let $\struct {G, \circ}$ be a  group.
Let $\struct {G, *}$ be the opposite group to $\struct {G, \circ}$.
$\struct {G, \circ}$ is an Abelian group {{iff}}:
:$\struct {G, \circ} = \struct {G, *}$

Proof:
By definition of opposite group:
:$(1): \quad \forall a, b \in G : a \circ b = b * a$
Theorem: Sequence on Product Space Converges to Point iff Projections Converge to Projections of Point

Let $I$ be an arbitrary index set.
For all $i \in I$, let $T_i = \struct {X_i, \tau_i}$ be topological spaces.
Let $\ds X = \prod_{i \mathop \in I} X_i$ be the cartesian product of $\family {X_i}_{i \mathop \in I}$.
Let $\tau$ be the product topology on $X$.
Denote by $\pr_i : X \to X_i$ the projection from $X$ onto $X_i$.
Let $\sequence {x_n}$ be a sequence on $X$ and let $x \in X$.
Then $\sequence {x_n}$ converges to $x$ {{iff}}:
:for all $i \in I$ the sequence $\sequence {\map {\pr_i} {x_n} }$ converges to $\map {\pr_i} x$.

Proof:
=== Necessary Condition ===
Let $x_n \to x$.
Let $i \in I$.
From Projection from Product Topology is Continuous it follows that $\pr_i$ is continuous.
By Continuous Mapping is Sequentially Continuous, $\pr_i$ is also sequentially continuous.
Hence $\map {\pr_i} {x_n} \to \map {\pr_i} x$.
{{qed|lemma}}
Theorem: Cauchy's Convergence Criterion/Complex Numbers

Let $\sequence {z_n}$ be a complex sequence.
Then $\sequence {z_n}$ is a Cauchy sequence {{iff}} it is convergent.

Proof:
=== Lemma ===
{{:Cauchy's Convergence Criterion/Complex Numbers/Lemma 1}}{{qed|lemma}}
Let $\sequence {x_n}$ be a real sequence where:
:$x_n = \map \Re {z_n}$ for every $n$
:$\map \Re {z_n}$ is the real part of $z_n$
Let $\sequence {y_n}$ be a real sequence where:
:$y_n = \map \Im {z_n}$ for every $n$
:$\map \Im {z_n}$ is the imaginary part of $z_n$
=== Necessary Condition ===
Let $\sequence {z_n}$ be a Cauchy sequence.
We aim to prove that $\sequence {z_n}$ is convergent.
We find:
:$\sequence {z_n}$ is a Cauchy sequence
:$\leadsto \sequence {x_n}$ and $\sequence {y_n}$ are Cauchy sequences by Lemma
:$\leadsto \sequence {x_n}$ and $\sequence {y_n}$ are convergent by Cauchy's Convergence Criterion on Real Numbers
:$\leadsto \sequence {z_n}$ is convergent by definition of convergent complex sequence.
{{qed|lemma}}
=== Sufficient Condition ===
Let $\sequence {z_n}$ be convergent.
We aim to prove that $\sequence {z_n}$ is a Cauchy sequence.
We find:
:$\sequence {z_n}$ is convergent
:$\leadsto \sequence {x_n}$ and $\sequence {y_n} $ are convergent by definition of convergent complex sequence
:$\leadsto \sequence {x_n}$ and $\sequence {y_n}$ are Cauchy sequences by Cauchy's Convergence Criterion on Real Numbers
:$\leadsto \sequence {z_n}$ is a Cauchy sequence by Lemma
{{qed}}
Theorem: Cauchy's Convergence Criterion/Complex Numbers

Let $\sequence {z_n}$ be a complex sequence.
Then $\sequence {z_n}$ is a Cauchy sequence {{iff}} it is convergent.

Proof:
=== Lemma ===
{{:Cauchy's Convergence Criterion/Complex Numbers/Lemma 1}}{{qed|lemma}}
Let $\sequence {x_n}$ be a real sequence where:
:$x_n = \map \Re {z_n}$ for every $n$
:$\map \Re {z_n}$ is the real part of $z_n$
Let $\sequence {y_n}$ be a real sequence where
:$y_n = \map \Im {z_n}$ for every $n$
:$\map \Im {z_n}$ is the imaginary part of $z_n$
We find:
:$\sequence {z_n}$ is a Cauchy sequence
:$\leadstoandfrom \sequence {x_n}$ and $\sequence {y_n}$ are Cauchy sequences by Lemma
:$\leadstoandfrom \sequence {x_n}$ and $\sequence {y_n}$ are convergent by Cauchy's Convergence Criterion on Real Numbers
:$\leadstoandfrom \sequence {z_n}$ is convergent by definition of convergent complex sequence
{{qed}}
Theorem: Sum of Arctangents

Let $\arctan a + \arctan b \in \openint {-\dfrac \pi 2} {\dfrac \pi 2}$ 
Then:
:$\arctan a + \arctan b = \map \arctan {\dfrac {a + b} {1 - a b} }$
where $\arctan$ denotes the arctangent.

Proof:
Let $x = \arctan a$ and $y = \arctan b$.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = \tan x
      | r = a
      | c = 
}}
{{eqn | n = 2
      | l = \tan y
      | r = b
      | c = 
}}
{{eqn | l = \map \tan {\arctan a + \arctan b}
      | r = \map \tan {x + y}
      | c =
}}
{{eqn | r = \frac {\tan x + \tan y} {1 - \tan x \tan y}
      | c = Tangent of Sum
}}
{{eqn | r = \frac {a + b} {1 - a b}
      | c = by $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = \arctan a + \arctan b
      | r = \map \arctan {\frac {a + b} {1 - a b} }
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Sum of Arccotangents

:$\arccot a + \arccot b = \arccot \dfrac {a b - 1} {a + b}$
where $\arccot$ denotes the arccotangent.

Proof:
Let $x = \arccot a$ and $y = \arccot b$.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = \cot x
      | r = a
      | c = 
}}
{{eqn | n = 2
      | l = \cot y
      | r = b
      | c = 
}}
{{eqn | l = \map \cot {\arccot a + \arccot b}
      | r = \map \cot {x + y}
      | c =
}}
{{eqn | r = \frac {\cot x \cot y - 1} {\cot x + \cot y}
      | c = Cotangent of Sum
}}
{{eqn | r = \frac {a + b} {1 - a b}
      | c = by $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = \arccot a + \arccot b
      | r = \arccot \frac {a b - 1} {a + b}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Difference of Arccotangents

:$\arccot a - \arccot b = \arccot \dfrac {a b + 1} {a - b}$
where $\arccot$ denotes the arccotangent.

Proof:
Let $x = \arccot a$ and $y = \arccot b$.
Then:
{{begin-eqn}}
{{eqn | n = 1
      | l = \cot x
      | r = a
      | c = 
}}
{{eqn | n = 2
      | l = \cot y
      | r = b
      | c = 
}}
{{eqn | l = \map \cot {\arccot a - \arccot b}
      | r = \map \cot {x - y}
      | c =
}}
{{eqn | r = \frac {\cot x \cot y + 1} {\cot x - \cot y}
      | c = Cotangent of Difference
}}
{{eqn | r = \frac {a - b} {1 + a b}
      | c = by $(1)$ and $(2)$
}}
{{eqn | ll= \leadsto
      | l = \arccot a - \arccot b
      | r = \arccot \frac {a b + 1} {a - b}
      | c = 
}}
{{end-eqn}}
{{qed}}
Theorem: Multiple Angle Formula for Tangent

:$\ds \map \tan {n \theta} = \frac {\ds \sum_{i \mathop = 0}^{\floor{\frac {n - 1} 2} } \paren {-1}^i \binom n {2 i + 1} \tan^{2 i + 1}\theta} {\ds \sum_{i \mathop = 0}^{\floor {\frac n 2} } \paren {-1}^i \binom n {2 i} \tan^{2 i}\theta}$

Proof:
Proof by induction:
For all $n \in \N_{\ge 0}$, let $\map P n$ be the proposition:
:$\ds \map \tan {n \theta} = \frac {\ds \sum_{i \mathop = 0}^{\floor{\frac {n - 1} 2} } \paren {-1}^i \binom n {2 i + 1} \tan^{2 i + 1}\theta} {\ds \sum_{i \mathop = 0}^{\floor {\frac n 2} } \paren {-1}^i \binom n {2 i} \tan^{2 i}\theta}$
Theorem: Laplace Transform of Dirac Delta Function by Function

Let $\map f t: \R \to \R$ or $\R \to \C$ be a function.
Let $\map \delta t$ denote the Dirac delta function.
Let $c$ be a positive constant real number.
Let $\laptrans {\map f t} = \map F s$ denote the Laplace transform of $f$.
Then:
:$\laptrans {\map \delta {t - c} \map f t} = e^{- s c} \map f c$

Proof:
{{begin-eqn}}
{{eqn | l = \laptrans {\map \delta {t - c} \map f t}
      | r = \int^{\to+\infty}_0 e^{-s t} \map \delta {t - c} \map f t \rd t
      | c = {{Defof|Laplace Transform}}
}}
{{eqn | r = \int^{c^+}_{c^-} e^{-s t} \map \delta {t - c} \map f t \rd t
      | c = Integrand elsewhere zero by {{Defof|Dirac Delta Function}}
}}
{{eqn | r = \int^{c^+}_{c^-} e^{-s c} \map \delta {t - c} \map f c \rd t
      | c = $e^{-s t}$ and $\map f t$ are constant in interval $\closedint {c^-} {c^+}$
}}
{{eqn | r = e^{-s c} \map f c \int^{c^+}_{c^-} \map \delta {t - c} \rd t
      | c = Primitive of Constant Multiple of Function
}}
{{eqn | r = e^{-s c} \map f c \int^{0^+}_{0^-} \map \delta {t - c} \map \rd {t - c}
      | c = Integration by Substitution
}}
{{eqn | r = e^{-s c} \map f c
      | c = {{Defof|Dirac Delta Function}}
}}
{{end-eqn}}
{{qed}}
Category:Dirac Delta Function
Category:Examples of Laplace Transforms
1jacsfiwuiadg5byjgzq89ofjz0jzfn