指数関数

定義の冪級数の収束半径は $\infty$ なので、冪級数 の記事の定理「項別微分」により、$\exp$ は $\mathbb{R}$ 上で微分可能で
$$ \exp'x=\sum_{n=1}^{\infty}\frac{nx^{n-1}}{n!}=\sum_{n=1}^{\infty}\frac{x^{n-1}}{(n-1)!}=\sum_{m=0}^{\infty}\frac{x^m}{m!}=\exp x $$
である。$x=0$ では $n\geq1$ の項が $0$ なので $\exp0=1$ である。$\exp'=\exp$ を繰り返し使えば、何回でも微分できる。

$h(x):=\exp x\exp(-x)$ とおく。連鎖律 の記事の定理「連鎖律」により $\frac{d}{dx}\exp(-x)=\exp'(-x)\cdot(-1)=-\exp(-x)$ であり、積の微分公式（導関数 の記事の定理「和・積・商の微分法」、Leb Proposition 4.1.8、p. 158）により
$$ h'(x)=\exp x\exp(-x)+\exp x\cdot\bigl(-\exp(-x)\bigr)=0 $$
である。平均値の定理 の記事の系「導関数が0なら定数」により $h$ は定数であり、$h(0)=\exp0\cdot\exp0=1$ なので $h=1$ である。

$g(x):=f(x)\exp(-kx)$ とおく。連鎖律により $\frac{d}{dx}\exp(-kx)=-k\exp(-kx)$ なので、積の微分公式により
$$ g'(x)=f'(x)\exp(-kx)-kf(x)\exp(-kx)=\bigl(f'(x)-kf(x)\bigr)\exp(-kx)=0 $$
である。$I$ は区間なので、平均値の定理 の記事の系「導関数が0なら定数」により $g$ は定数で、$g(x)=g(0)=f(0)$ である。cor-expf-inverse により $\exp(-kx)\exp(kx)=1$ なので、$f(x)=g(x)\exp(kx)=f(0)\exp(kx)$ である。後半は $k=1$、$I=\mathbb{R}$ の場合であり、thm-expf-derivative により $\exp$ 自身がこの条件を満たす。

$y$ を固定し、$f(x):=\exp(x+y)$ とおく。連鎖律により $f'(x)=\exp'(x+y)=\exp(x+y)=f(x)$ であり、$f(0)=\exp y$ である。thm-expf-uniqueness（$k=1$、$I=\mathbb{R}$）により、$f(x)=f(0)\exp x=\exp y\exp x$ である。

$m\geq0$ については $m$ についての帰納法で示す。$m=0$ では両辺 $1$ であり、$m$ で成り立てば thm-expf-addition により $\exp((m+1)x)=\exp(mx)\exp x=(\exp x)^{m+1}$ である。$m<0$ なら $-m>0$ なので、cor-expf-inverse により $\exp(mx)=1/\exp(-mx)=1/(\exp x)^{-m}=(\exp x)^m$ である。$x=1$ とおけば後半を得る。

$x=y=0$ とおくと $f(0)=f(0)^2$ なので $f(0)=0$ か $f(0)=1$ である。$f(0)=0$ なら、すべての $x$ で $f(x)=f(x+0)=f(x)f(0)=0$ である。$f(0)=1$ とする。任意の $x$ と $h\ne0$ について
$$ \frac{f(x+h)-f(x)}{h}=f(x)\,\frac{f(h)-f(0)}{h} $$
であり、$h\to0$ で右辺は $f(x)f'(0)$ に収束する。よって $f$ はすべての点で微分可能で $f'=kf$ である。thm-expf-uniqueness により $f(x)=f(0)\exp(kx)=\exp(kx)$ である。

1：thm-expf-addition により $\exp x=\exp(x/2)^2\geq0$ であり、cor-expf-inverse により $\exp x\ne0$ なので $\exp x>0$ である。
2：$\exp'=\exp>0$ なので、平均値の定理 の記事の系「導関数の符号と増減」により狭義単調増加である。
3：$g(x):=\exp x-1-x$ とおくと $g'(x)=\exp x-1$ である。2 により $x<0$ で $g'(x)<\exp0-1=0$、$x>0$ で $g'(x)>0$ である。$x\ne0$ とすると、平均値の定理 により $g(x)-g(0)=g'(\xi)x$ となる $0$ と $x$ の間の $\xi$ があり、$\xi$ は $x$ と同符号なので $g'(\xi)$ も $x$ と同符号である。したがって $g'(\xi)x>0$ であり、$g(x)=g(0)+g'(\xi)x=g'(\xi)x>0$ である。
4：3 により $x>0$ で $\exp x\geq1+x$ なので $\exp x\to\infty$（$x\to\infty$）である。cor-expf-inverse により $\exp(-x)=1/\exp x\to0$（$x\to\infty$）である。
5：2 により単射であり、1 により値は $(0,\infty)$ に入る。$y>0$ とすると、4 により $\exp a< y<\exp b$ となる $a< b$ がとれる。$\exp$ は微分可能なので連続であり、中間値の定理 の記事の定理「中間値の定理」により $\exp x=y$ となる $x\in(a,b)$ がある。

$x>0$ なら定義の級数の項はすべて正なので、$m+1$ 次の項 1 つだけを残して $\exp x>\dfrac{x^{m+1}}{(m+1)!}$ である。よって
$$ \frac{\exp x}{x^m}>\frac{x}{(m+1)!}\to\infty\qquad(x\to\infty) $$
である。後半は cor-expf-inverse により $x^m\exp(-x)=\bigl(\exp x/x^m\bigr)^{-1}$ だから従う。

1：cor-expf-integer により $\exp(m\log a)=(\exp\log a)^m=a^m$ であり、右辺は整数乗の通常の意味（$m<0$ なら $1/a^{-m}$）である。
2：$b:=a^{1/q}=\exp\bigl(\frac1q\log a\bigr)>0$ とおくと、cor-expf-integer により $b^q=\exp(\log a)=a$ である。$t\mapsto t^q$ は $(0,\infty)$ 上で狭義単調増加なので、$t^q=a$ となる正の実数 $t$ は $b$ だけである（存在だけなら 中間値の定理 の記事の命題「正の数の冪根の存在」にもある）。
3：cor-expf-integer により $\exp\bigl(p\cdot\frac1q\log a\bigr)=\Bigl(\exp\bigl(\frac1q\log a\bigr)\Bigr)^p$ である。
4：$\log e=1$ なので $e^x=\exp(x\cdot1)=\exp x$ である。

$x=0$ なら両辺とも $1$ である。$x\ne0$ とし、$n>|x|$ の範囲で考えると $1+x/n>0$ なので、prop-expf-rational-power の 1 により $\bigl(1+\frac xn\bigr)^n=\exp\bigl(n\log(1+\frac xn)\bigr)$ である。
$\exp$ は $\mathbb{R}$ 上で連続かつ狭義単調増加で、$\exp'(0)=\exp0=1\ne0$ なので、連鎖律 の記事の系「逆関数の微分公式」により逆関数 $\log$ は $\exp0=1$ で微分可能で、微分係数は $1/\exp'(0)=1$ である。すなわち $t\to0$（$t\ne0$）で $\frac{\log(1+t)-\log1}{t}\to1$ であり、$\log1=0$ なので $\frac{\log(1+t)}t\to1$ である。$t_n:=x/n$ は $0$ でなく $0$ に収束するので
$$ n\log\Bigl(1+\frac xn\Bigr)=x\cdot\frac{\log(1+t_n)}{t_n}\to x\qquad(n\to\infty) $$
である。$\exp$ は $x$ で連続なので、$\exp\bigl(n\log(1+\frac xn)\bigr)\to\exp x$ である。