nyuuzyou/wikis huggingface dataset:
Exponential Sequence is Uniformly Convergent on Compact Sets

== Theorem ==
Let $\EE = \sequence {E_n}$ denote the sequence of complex functions $E_n: \C \to \C$ defined as:
:$\map {E_n} z = \paren {1 + \dfrac z n}^n$
Let $K$ be a compact subset of $\C$.
Then $\EE$ is uniformly convergent on $K$.
== Proof ==
=== $\EE$ is Uniformly Bounded on an open space containing $K$ ===
First, from Equivalence of Definitions of Complex Exponential Function we see that $\EE$ is pointwise convergent to $\exp$.
From Combination Theorem for Continuous Complex Functions, $E_n$ is continuous for each $n \in \N$.
From Compact Subspace of Metric Space is Bounded, $K$ is bounded by some real number $M \in \R$.
Let:
:$M' = M + 1$
:$U = \set {z \in \C: \cmod z < M'}$
:$z \in U$
:$n \in \N$
From the Triangle Inequality for Complex Numbers:
:$\cmod {1 + \dfrac z n} \le 1 + \dfrac {\cmod z} n$
Thus, from Power Function is Strictly Increasing over Positive Reals: Natural Exponent:
:$\cmod {1 + \dfrac z n}^n \le \paren {1 + \dfrac {\cmod z} n}^n$
Call this result $(1)$.
Also:
Thus it is sufficient to show that $\paren {1 + \dfrac {M'} n}^n$ is bounded.
From Exponential Sequence is Eventually Increasing:
:$\exists N \in \N: n \ge N \implies \paren {1 + \dfrac {M'} n}^n \le \paren {1 + \dfrac {M'} {n + 1} }^{n + 1}$
So, for $n \ge N$:
Now, for each $n \in \set {1, 2, \ldots, N - 1}$:
:$\exists M_n \in \R: \paren {1 + \dfrac {M'} n}^n \le M_n$
by Continuous Function on Compact Subspace of Euclidean Space is Bounded.
So:
:$\forall n \in \N: \paren {1 + \dfrac {M'} n}^n \le \max \set {M_1, M_2, \ldots, M_{N - 1}, \exp M'}$
Call this result $(3)$.
Hence, for $z \in U$; that is, for $\cmod z < {M'}$:
That is, $\EE$ is uniformly bounded on $U$.
=== $\EE$ is Uniformly Convergent on $K$ ===
Note that, from Combination Theorem for Complex Derivatives:
:$\forall n \in \N: \map {E_n} z$ is holomorphic on $U$.
From Uniformly Bounded Family is Locally Bounded, $\EE$ is locally bounded on $U$.
From Montel's Theorem, $\EE$ is a normal family.
From Vitali's Convergence Theorem, $\EE$ converges uniformly on any compact subset of $U$.
In particular, $\EE$ converges uniformly on $K$.
Hence the result.
Category:Exponential Function
Exponential Tends to Zero and Infinity

== Theorem ==
Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Then:
:$\exp x \to +\infty$ as $x \to +\infty$
:$\exp x \to 0$ as $x \to -\infty$
Thus the exponential function has domain $\R$ and image $\openint 0 \infty$.
== Proof ==
=== The exponential function approaches positive infinity as x approaches positive infinity ===
Let $M$ be a strictly positive real number.
Let $N$ be $\ln M$.
$N$ is real because $M > 0$.
From Exponential is Strictly Increasing:
:$\forall x: x > N \implies \exp x > \exp N = M$
Therefore:
:$\forall M \in \R_{>0} : \exists N \in \R : \forall x > N : \exp x > M$
The result follows from the definition of infinite limit at infinity.
=== The exponential function approaches 0 as x approaches negative infinity ===
Let $\epsilon$ be a strictly positive real number.
Let $c$ be $\ln \epsilon$.
Let $x$ be any real number that is smaller than $c$.
From Exponential of Real Number is Strictly Positive:
:$\exp x > 0 \implies \size {\exp x} = \exp x$
From Exponential is Strictly Increasing:
:$\size {\exp x - 0} = \exp x < \exp c = \epsilon$
Therefore:
:$\forall \epsilon \in \R_{>0} : \exists c \in \R : \forall x < c : \size {\exp x - 0} < \epsilon$
From the definition of limit at minus infinity, the result follows.
=== The exponential function has domain $\R$ and image $\openint 0 \infty$ ===
We have that the Exponential is Strictly Increasing.
From above, $\ds \lim_{x \mathop \to \infty} \exp x = \infty$
From above, $\ds \lim_{x \mathop \to -\infty} \exp x = 0$
Hence the result.
== Sources ==
* : $\S 14.4$
Category:Exponential Function
Exponential Time/Examples/Print All Permutations of Word

== Example of Exponential Time ==
Consider a computer program to print all possible permutations of a given word of $n$ letters.
Such a computer program needs to print a letter a total of $n \paren {n!}$ times.
This exceeds $A n^k$ for any fixed $A$ and $k$, as long as $n$ gets sufficiently large.
An algorithm which prints all possible permutations of such a word runs in exponential time.
== Sources ==
* 
* 
Category:Examples of Exponential Time
Exponential Time/Examples/Traveling Salesman Problem

== Example of Exponential Time ==
Consider the traveling salesman problem.
This can be expressed:
:Is there a route shorter in length than some number $C$?
An algorithm which systematically generates and checks all routes while looking for a route shorter than $C$ would run in exponential time.
== Sources ==
* 
* 
Category:Examples of Exponential Time
Category:Traveling Salesman Problem
Exponential is Strictly Convex

== Theorem ==
Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Then:
:The function $f \left({x}\right) = \exp x$ is strictly convex.
== Proof ==
By definition, the exponential function is the inverse of the natural logarithm function.
From Logarithm is Strictly Increasing, $\ln x$ is strictly increasing.
From Logarithm is Strictly Concave, $\ln x$ is strictly concave.
The result follows from Inverse of Strictly Increasing Strictly Concave Real Function is Strictly Convex.
Category:Exponential Function
Exponential is Strictly Increasing

== Theorem ==
Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Then:
:The function $\map f x = \exp x$ is strictly increasing.
== Proof 1 ==
== Proof 2 ==
== Sources ==
* : $\S 14.4$
Category:Exponential is Strictly Increasing
Category:Exponential Function
Category:Examples of Strictly Increasing Real Functions
Exponential is of Exponential Order Real Part of Index

== Theorem ==
Let $\map f t = e^{\psi t}$ be the complex exponential function, where $t \in \R, \psi \in \C$.
Let $a = \map \Re \psi$.
Then $e^{\psi t}$ is of exponential order $a$.
== Proof ==
The result follows from the definition of exponential order with $M = 1$, $K = 2$, and $a = a$.
Category:Exponential Order
Exponential of 2 m i Arccotangent of p

== Theorem ==
:$\map \exp {2 m i \arccot p} \paren {\dfrac {p i + 1} {p i - 1} }^m = 1$
== Proof ==
Let $z = \arccot p$.
Then:
So we have:
Now:
and the result follows.
== Sources ==
* : $1$: Complex Numbers: Supplementary Problems: Miscellaneous Problems: $132$
Category:Arccotangent Function
Exponential of Natural Logarithm

== Theorem ==
Let $x \in \R$ be a real number.
Let $\exp x$ be the exponential of $x$.
Let $\ln x$ be the natural logarithm of $x$.
Then:
: $\forall x > 0: \map \exp {\ln x} = x$
: $\forall x \in \R: \map \ln {\exp x} = x$
== Proof ==
From the definition of the exponential function:
:$e^y = x \iff \ln x = y$
Raising both sides of the equation $\ln x = y$ to the power of $e$:
Category:Exponential Function
Category:Natural Logarithms
Exponential of Negative of Exponential Random Variable has Beta Distribution

== Theorem ==
Let $\beta$ be a positive real number.
Let $X \sim \Exponential \beta$ where $\Exponential \beta$ is the exponential distribution with parameter $\beta$. 
Then:
:$e^{-X} \sim \BetaDist {\dfrac 1 \beta} 1$
== Proof ==
Note that if:
:$Y \sim \BetaDist {\dfrac 1 \beta} 1$
then the probability density function of $Y$, $f_Y$ is given by:
for each $y > 0$. 
Let:
:$Z = e^{-X}$
It suffices to show that $Z$ has the same probability density function as $Y$.
We have: 
By Derivative of Power, the probability density function of $Z$, $f_Z$ is therefore given by: 
:$\map {f_Z} z = \dfrac 1 \beta z^{\frac 1 \beta - 1}$
for each $z > 0$.
So:
:$f_Y = f_Z$
Category:Exponential Distribution
Category:Beta Distribution
Exponential of One

== Theorem ==
Let $\exp x$ be the exponential of $x$.
Then:
:$\exp 1 = e$
where $e$ is Euler's number: $e = 2.718281828\ldots$
== Proof ==
We have that the exponential function is the inverse of the natural logarithm function:
:$\ln e = 1$
Hence the result.
== Sources ==
* : $\S 14.4$
Category:Exponential Function
Exponential of Product

== Theorem ==
Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x y} = \paren {\exp y}^x$
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
Category:Exponential Function
Category:Exponential of Product
Exponential of Product/Proof 1

== Theorem ==
== Proof ==
Let $Y = \exp y$.
From Exponential of Natural Logarithm:
:$\map \ln {\exp y} = y$
From Logarithms of Powers, we have:
:$\ln Y^x = x \ln Y = x \, \map \ln {\exp y} = x y$
Thus:
:$\map \exp {x y} = \map \exp {\ln Y^x} = Y^x = \paren {\exp y}^x$
== Sources ==
* : $\S 14.5 \ (1) \ \text{(ii)}$
Category:Exponential of Product
Exponential of Product/Proof 3

== Theorem ==
== Proof ==
For $n \in \Z_{\ge 0}$:
That is:
:$\forall n \in \Z_{\ge 0}: \map \exp {n y} = \paren {\exp y}^n$
Now let $n \in \Z_{<0}$.
It follows that $-n \in \Z_{>0}$, so:
Thus:
:$(2): \quad \forall m \in \Z: \map \exp {m y} = \paren {\exp y}^m$
Next, for $n \in \Z_{>0}$:
So fix $r \in \Q$.
Let $r = \dfrac m n$, where $m \in \Z$ is an integer and $n \in \Z_{>0}$ is a strictly positive integer.
From the above:
Thus, from the definition of $\paren {\exp y}^x$ as the unique continuous extension of $r \mapsto \paren {\exp y}^r$ from $\Q$ to $\R$:
:$\map \exp {x y} = \paren {\exp y}^x$
Category:Exponential of Product
Exponential of Rational Number is Irrational

== Theorem ==
Let $r$ be a rational number such that $r \ne 0$.
Then:
:$e^r$ is irrational
where $e$ is Euler's number.
== Proof ==
Let $r = \dfrac p q$ be rational such that $r \ne 0$.
 $e^r$ is rational.
Then $\paren {e^r}^q = e^p$ is also rational.
Then if $e^{-p}$ is rational, it follows that $e^p$ is rational.
It is therefore sufficient to derive a contradiction from the supposition that $e^p$ is rational for every $p \in \Z_{>0}$.
Let $e^p = \dfrac a b$ for $a, b \in \Z_{>0}$.
Let $n \in \Z_{>0}$ be a strictly positive integer.
Let $\map f x$ be the function defined as:
Note that:
:$(2): \quad 0 < x < 1 \implies 0 < \map f x < \dfrac 1 {n!}$
We also have:
:$\map f 0 = 0$
:$\map {f^{\paren m} } 0 = 0$ if $m < n$ or $m > 2 n$
and:
:$n \le m \le 2 n \implies \map {f^{\paren m} } 0 = \dfrac {m!} {n!} c_m$
and this number is an integer.
Thus at $x = 0$, $\map f x$ and all its derivatives are integers.
Since $\map f {1 - x} = \map f x$, the same is true for $x = 1$.
Let $\map F x$ be the function defined as:
Because of the properties of $\map f x$ and its derivatives above, $\map F 0$ and $\map F 1$ are integers.
Next we have:
$(4)$ leads to:
which is an integer.
But from $(2)$:
The expression on the tends to $0$ as $n$ tends to $\infty$.
Hence:
:$0 < a \, \map F 1 - b \, \map F 0 < 1$
for sufficiently large $n$.
But there exists no integer strictly between $0$ and $1$.
From this contradiction it follows that our original assumption, that is, that $e^r$ is rational, must have been false.
== Sources ==
* : Chapter $\text {B}.17$: More About Irrational Numbers. $\pi$ is Irrational
Category:Exponential Function
Exponential of Real Number is Strictly Positive

== Theorem ==
Let $x$ be a real number.
Let $\exp$ denote the (real) exponential function.
Then:
:$\forall x \in \R : \exp x > 0$
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Proof 4 ==
== Proof 5 ==
== Also see ==
* Image of Complex Exponential Function
Category:Exponential Function
Category:Exponential of Real Number is Strictly Positive
Exponential of Real Number is Strictly Positive/Proof 1

== Theorem ==
== Proof ==
This proof assumes the series definition of $\exp$.
That is, let:
:$\ds \exp x = \sum_{n \mathop = 0}^\infty \dfrac {x^n} {n!}$
First, suppose $0 < x$.
Then:
So $\exp$ is strictly positive on $\R_{>0}$.
From Exponential of Zero, $\exp 0 = 1$.
Finally, suppose that $x < 0$.
Then:
So $\exp$ is strictly positive on $\R_{<0}$.
Hence the result.
Category:Exponential of Real Number is Strictly Positive
Exponential of Real Number is Strictly Positive/Proof 2

== Theorem ==
== 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:
Category:Exponential of Real Number is Strictly Positive
Exponential of Real Number is Strictly Positive/Proof 4

== Theorem ==
== 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.
Category:Exponential of Real Number is Strictly Positive
Exponential of Real Number is Strictly Positive/Proof 5

== Theorem ==
== 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 ===
 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.
== Sources ==
* : $\S 8.3$: Theorem $6 \ \text {(iii)}$
Category:Exponential of Real Number is Strictly Positive
Exponential of Real Number is Strictly Positive/Proof 5/Lemma

== Theorem ==
Let $x$ be a real number.
Let $\exp$ denote the (real) Exponential Function.
Then:
:$\forall x \in \R: \exp x \ne 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$.
 $\exists \alpha \in \R: \exp \alpha = 0$.
Suppose that $\alpha > 0$.
Let $J = \closedint 0 \alpha$.
From Exponential Function is Continuous, $\exp$ is continuous on $J$.
From Max and Min of Function on Closed Real Interval:
:$\exists K \in \R: \forall x \in J: \size {\exp x} < K$
Then, $\forall n \in \N : \exists c_n \in J$ such that:
So:
:$\forall n \in \N: 1 \le K \dfrac {\alpha^n} {n!}$
That is, dividing both sides by $K$:
:$\forall n \in \N: \dfrac 1 K \le \dfrac {\alpha^n} {n!}$
But from Power over Factorial, $\dfrac {\alpha^n} {n!} \to 0$.
This contradicts our assumption.
The same argument, mutatis mutandis proves the result for $\alpha < 0$.
By hypothesis $(2)$:
Hence the result.
Category:Exponential of Real Number is Strictly Positive
Exponential of Series Equals Infinite Product

== Theorem ==
Let $\sequence {z_n}$ be a sequence of complex numbers.
Suppose $\ds \sum_{n \mathop = 1}^\infty z_n$ converges to $z \in \C$.
Then $\ds \prod_{n \mathop = 1}^\infty \map \exp {z_n}$ converges to $\exp z$.
== Proof ==
Let $S_n$ be the $n$th partial sum of $\ds \sum_{n \mathop = 1}^\infty z_n$.
Let $P_n$ be the $n$th partial product of $\ds \prod_{n \mathop = 1}^\infty \map \exp {z_n}$.
By Exponential of Sum, $\map \exp {S_n} = P_n$ for all $n \in \N$.
By Exponential Function is Continuous, $\ds \lim_{n \mathop \to \infty} \map \exp {S_n} = \exp z$.
By Exponential of Complex Number is Nonzero, $\exp z \ne 0$.
Thus $\ds \lim_{n \mathop \to \infty} P_n = \exp z \ne 0$.
== Also see ==
* Logarithm of Infinite Product of Complex Numbers
Category:Infinite Products
Exponential of Sum/Complex Numbers

== Theorem ==
Let $z_1, z_2 \in \C$ be complex numbers.
Let $\exp z$ be the exponential of $z$.
Then:
:$\map \exp {z_1 + z_2} = \paren {\exp z_1} \paren {\exp z_2}$
=== Corollary ===
=== General Result ===
== Proof ==
This proof is based on the definition of the complex exponential as the unique solution of the differential equation:
:$\dfrac \d {\d z} \exp = \exp$
which satisfies the initial condition $\map \exp 0 = 1$.
Define the complex function $f: \C \to \C$ by:
:$\map f z = \map \exp z \, \map \exp {z_1 + z_2 - z}$
Then find its derivative:
From Zero Derivative implies Constant Complex Function, it follows that $f$ is constant.
Then:
== Sources ==
* : $\S 4.5$. The Functions $e^z$, $\cos z$, $\sin z$: $\text{(i)}$: $(4.12)$
* : $2$: Functions, Limits and Continuity: The Elementary Functions: $3$
* : $\S 1.5$
Category:Exponential of Sum
Exponential of Sum/Complex Numbers/Corollary

== Corollary to Exponential of Sum: Complex Numbers ==
Let $z_1, z_2 \in \C$ be complex numbers.
Let $\exp z$ be the exponential of $z$.
Then:
:$\map \exp {z_1 - z_2} = \dfrac {\exp z_1} {\exp z_2}$
== Proof ==
By Exponential of Sum: Complex Numbers:
:$\map \exp {z_1 - z_2} = \exp z_1 \, \map \exp {-z_2}$
By Reciprocal of Complex Exponential:
:$\dfrac 1 {\exp z_2} = \map \exp {-z_2}$
Combining these two, we obtain the result:
:$\map \exp {z_1 - z_2} = \dfrac {\exp z_1} {\exp z_2}$
== Sources ==
* : $2$: Functions, Limits and Continuity: The Elementary Functions: $3$
Category:Exponential of Sum
Exponential of Sum/Complex Numbers/General Result

== Theorem ==
Let $m \in \N_{>0}$ be a natural number.
Let $z_1, z_2, \ldots, z_m \in \C$ be complex numbers.
Let $\exp z$ be the exponential of $z$.
Then:
:$\ds \map \exp {\sum_{j \mathop = 1}^m z_j} = \prod_{j \mathop = 1}^m \paren {\exp z_j}$
=== Corollary ===
== Proof ==
The proof proceeds by induction.
For all $m \in \N_{>0}$, let $\map P m$ be the proposition:
:$\ds \map \exp {\sum_{j \mathop = 1}^m z_j} = \prod_{j \mathop = 1}^m \paren {\exp z_j}$
$\map P 1$ is the case:
Thus $\map P 1$ is seen to hold.
=== Basis for the Induction ===
$\map P 2$ is the case:
:$\map \exp {z_1 + z_2} = \paren {\exp z_1} \paren {\exp z_2}$
This is proved in Exponential of Sum: Complex Numbers.
Thus $\map P 2$ is seen to hold.
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:
:$\ds \map \exp {\sum_{j \mathop = 1}^k z_j} = \prod_{j \mathop = 1}^k \paren {\exp z_j}$
from which it is to be shown that:
:$\ds \map \exp {\sum_{j \mathop = 1}^{k + 1} z_j} = \prod_{j \mathop = 1}^{k + 1} \paren {\exp z_j}$
=== Induction Step ===
This is the induction step:
So $\map P k \implies \map P {k + 1}$ and the result follows by the Principle of Mathematical Induction.
Therefore:
:$\forall m \in \N_{>0}: \ds \map \exp {\sum_{j \mathop = 1}^m z_j} = \prod_{j \mathop = 1}^m \paren {\exp z_j}$
== Sources ==
* : $\S 2$. Geometrical Representations
Category:Exponential of Sum
Exponential of Sum/Complex Numbers/General Result/Corollary

== Theorem ==
Let $m \in \Z_{>0}$ be a positive integer.
Let $z \in \C$ be a complex number.
Let $\exp z$ be the exponential of $z$.
Then:
: $\ds \exp \paren {m z} = \paren {\exp z}^m$
== Proof ==
From Exponential of Sum: Complex Numbers: General Result:
:$\ds \exp \paren {\sum_{j \mathop = 1}^m z_j} = \prod_{j \mathop = 1}^m \paren {\exp z_j}$
for complex numberst $z_1, z_2, \ldots, z_m \in \C$.
The result follows by setting $z = z_1 = z_2 = \cdots = z_m$.
== Sources ==
* : $\S 2$. Geometrical Representations
Category:Exponential of Sum
Exponential of Sum/Real Numbers

== Theorem ==
Let $x, y \in \R$ be real numbers.
Let $\exp x$ be the exponential of $x$.
Then:
:$\map \exp {x + y} = \paren {\exp x} \paren {\exp y}$
=== Corollary ===
== Lemma ==
== Proof 1 ==
== Proof 2 ==
== Proof 3 ==
== Proof 4 ==
== Proof 5 ==
== Proof 6 ==
Category:Exponential of Sum
Exponential of Sum/Real Numbers/Lemma

== Lemma ==
Let $x, y \in \R$.
Let $n \in \N_{> 0}$ such that $n > -\paren {x + y}$.
Then:
:$1 + \dfrac {x + y} n + \dfrac {x y} {n^2} = \paren {1 + \dfrac {x + y} n} \paren {1 + \dfrac {\paren {\frac {x y} {n + x + y} } } n}$
== Proof ==
As $n \in \N_{> 0}$ we have that $n \ne 0$ and so the fractions in the expressions are defined.
That final step is justified, as we have that $n > -\paren {x + y}$ and so $n + x + y \ne 0$.
== Also see ==
This lemma is used in:
:Proof 2 of (Real) Exponential of Sum
:Proof 3 of (Real) Exponential of Sum
:$\map \exp {x + y} = \paren {\exp x} \paren {\exp y}$
for real $x$ and $y$.
Category:Exponential of Sum
Exponential of Sum/Real Numbers/Proof 1

== Theorem ==
== Proof ==
This proof assumes the definition of $\exp$ as:
:$\exp x = y \iff \ln y = x$
where:
:$\ln y = \ds \int_1^y \dfrac 1 t \rd t$
Let $X = \exp x$ and $Y = \exp y$.
From Sum of Logarithms, we have:
:$\ln X Y = \ln X + \ln Y = x + y$
From the Exponential of Natural Logarithm:
:$\map \exp {\ln x} = x$
Thus:
:$\map \exp {x + y} = \map \exp {\ln X Y} = X Y = \paren {\exp x} \paren {\exp y}$
Alternatively, this may be proved directly by investigating:
:$\map D {\map \exp {x + y} / \exp x}$
== Sources ==
* : $\S 14.5 \ (1) \ \text {(i)}$
Category:Exponential of Sum
Exponential of Sum/Real Numbers/Proof 2

== Theorem ==
== Proof ==
=== Lemma ===
This proof assumes the definition of $\exp$ as defined by a limit of a sequence:
:$\exp x = \ds \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n$
From Powers of Group Elements we can presuppose the Exponent Combination Laws for natural number indices.
First we introduce a lemma:
By definition:
Category:Exponential of Sum
Exponential of Sum/Real Numbers/Proof 3

== Theorem ==
== Proof ==
=== Lemma ===
This proof assumes the definition of $\exp$ as defined by a limit of a sequence:
:$\exp x = \ds \lim_{n \mathop \to +\infty} \paren {1 + \frac x n}^n$
From Powers of Group Elements we can presuppose the Exponent Combination Laws for natural number indices.
By definition:
Intuitively, the $\paren {1 + \dfrac {x + y} n}$ term is the most influential of the terms involved in the limit, and:
:$\paren {1 + \dfrac {x + y} n + \dfrac {x y} {n^2} }^n \to \paren {1 + \dfrac {x + y} n}^n$ as $n \to +\infty$
To formalize this claim:
:$\map \exp {x + y} = \exp x \cdot \exp y \iff \dfrac {\exp x \cdot \exp y} {\map \exp {x + y} } = 1$
Now, as $n \to +\infty$, we use the Combination Theorem for Limits of Real Functions to investigate the behavior of this sequence, term by term.
As $1$ trivially converges to $1$, consider now the other terms of the sequence.
We invoke the Squeeze Theorem for Absolutely Convergent Series.
Hence it will suffice to investigate the limit behaviour of:
:$\ds \sum_{k \mathop = 1}^n \, \size {\binom n k n^{-k} \paren {\frac {x y} {n + x + y} }^k}$
From $\dbinom n k$ is not greater than $n^k$:
Therefore, we may conclude, using Absolute Value is Bounded Below by Zero:
:$\ds 0 \le \sum_{k \mathop = 1}^n \size { {n \choose k} n^{-k} \paren {\frac {x y} {n + x + y} }^k} \le \sum_{k \mathop = 1}^n \size {\frac {x y} {n + x + y} }^k$
From Sum of Infinite Geometric Sequence, the right hand term converges to:
:$0 \to 0$ as $n \to +\infty$, trivially.
This means:
:$\dfrac {\paren {1 + \dfrac {x + y} n + \dfrac {x y} {n^2} }^n} {\paren {1 + \dfrac {x + y} n}^n} \to 1$ as $n \to +\infty$
which is equivalent to our hypothesis:
:$\paren {1 + \dfrac {x + y} n + \dfrac {x y} {n^2} }^n \to \paren {1 + \dfrac {x + y} n}^n$ as $n \to +\infty$
Category:Exponential of Sum
Exponential of Sum/Real Numbers/Proof 4

== Theorem ==
== Proof ==
This proof assumes the definition of $\exp$ as defined by an initial value problem.
That is, suppose $\exp$ satisfies:
:$(1): \quad D_x \exp x = \exp x$
:$(2): \quad \exp 0 = 1$
on $\R$.
Consider the real function $f: \R \to \R$ defined by:
:$\map f x := \dfrac {\map \exp {x + y} } {\map \exp y}$
From Exponential of Real Number is Strictly Positive, $f$ is well-defined.
So:
Thus $f$ satisfies $(1)$.
Further:
So $f$ satisfies $(2)$.
From Exponential Function is Well-Defined:
:$f = \exp$
That is:
== Sources ==
* : $\S 8.3$: Theorem $6 (iv)$
Category:Exponential of Sum