exponential function never vanishes

In the entry exponential function (http://planetmath.org/ExponentialFunction) one defines for real variable $x$ the real exponential function  $\exp x$, i.e. $e^x$, as the sum of power series:

$$e^x=\sum _{k=0}^{\mathrm{\infty }}\frac{x^k}{k!}$$

The series form implies immediately that the real exponential function attains only positive values when  $x\geqq 0$.  Also for    the positiveness is easy to see by grouping the series terms pairwise.

In to study the sign of $e^x$ for arbitrary real $x$, we may multiply the series of $e^x$ and $e^{-x}$ using Abel’s multiplication rule for series (http://planetmath.org/AbelsMultiplicationRuleForSeries).  We obtain

$$e^x{e}^{-x}=\sum _{n=0}^{\mathrm{\infty }}\frac{x^n}{n!}\sum _{k=0}^{\mathrm{\infty }}{(-1)}^k\frac{x^k}{k!}=\sum _{n=0}^{\mathrm{\infty }}\sum _{j=0}^n{(-1)}^j\frac{x^n}{j!(n-j)!}=\sum _{n=0}^{\mathrm{\infty }}\frac{x^n}{n!}\sum _{j=0}^n\left(\genfrac{}{}{0pt}{}{n}{j}\right){(-1)}^j=\sum _{n=0}^{\mathrm{\infty }}\frac{x^n}{n!}\cdot 0^n.$$

The last sum equals 1.  So, if  $-x>0$,  then  $e^{-x}>0$,  whence $e^x$ must be positive.

Let us now consider arbitrary complex value  $z=x+iy$  where $x$ and $y$ are real.  Using the addition formula of complex exponential function and the Euler relation, we can write

$$e^z=e^{x+iy}=e^x{e}^{iy}=e^x(\cos y+i\sin y).$$

From this we see that the absolute value of $e^z$ is $e^x$, which we above have proved to be positive.  Accordingly, we may write the

Theorem.  The complex exponential function never vanishes.

Title	exponential function never vanishes
Canonical name	ExponentialFunctionNeverVanishes
Date of creation	2014-11-22 21:23:32
Last modified on	2014-11-22 21:23:32
Owner	pahio (2872)
Last modified by	pahio (2872)
Numerical id	8
Author	pahio (2872)
Entry type	Theorem
Classification	msc 32A05
Classification	msc 30D20
Synonym	real exponential function is positive
Related topic	ExponentialFunction
Related topic	ExponentialFunctionDefinedAsLimitOfPowers
Related topic	PeriodicityOfExponentialFunction