指数関数の微分

段 1（左の不等式）。rem-dex-premises の 1 で $n=m$ とすると $\bigl(1+\frac1m\bigr)^m< e$ である。
段 2（右の不等式）。rem-dex-premises の 1 で $n=m-1$（$m\ge2$ なので正の整数）とすると
$$ e<\Bigl(1+\frac1{m-1}\Bigr)^{(m-1)+1}=\Bigl(1+\frac1{m-1}\Bigr)^m $$
である。
段 3（$m$ 乗根をとる）。段 1・段 2 から $\bigl(1+\frac1m\bigr)^m< e<\bigl(1+\frac1{m-1}\bigr)^m$ である。3 つの数はどれも正であり、$t\mapsto t^{1/m}$ は狭義単調増加なので（rem-dex-premises の 2）、$\frac1m$ 乗しても不等号の向きは変わらない。$\bigl((1+\frac1m)^m\bigr)^{1/m}=1+\frac1m$ などに注意すると、主張を得る。$\square$

方針：$h>0$ のときは $h$ を $\frac1{m+1}$ と $\frac1m$ の間に挟み、lem-dex-root で上下から評価する。$h<0$ のときは $h>0$ の場合に帰着する。
段 1（$m$ の選び方）。$0< h\le\frac12$ とする。$\frac1h\ge2$ なので、$m\le\frac1h< m+1$ を満たす整数 $m\ge2$ がただ 1 つある（$\frac1h$ の整数部分）。逆数をとると $\frac1{m+1}< h\le\frac1m$ である。また $m>\frac1h-1$ なので、$h\to+0$ のとき $m\to\infty$ である。
段 2（$e^h$ を挟む）。$e>1$ なので $x\mapsto e^x$ は狭義単調増加であり（rem-dex-premises の 2）、段 1 から
$$ e^{\frac1{m+1}}< e^h\le e^{\frac1m} $$
である。
段 3（上からの評価）。段 2 の右側と lem-dex-root から $e^h-1\le e^{\frac1m}-1<\frac1{m-1}$ である。また段 1 から $\frac1h< m+1$ である。どちらも正の数なので掛け合わせて
$$ \frac{e^h-1}h=(e^h-1)\cdot\frac1h<\frac1{m-1}\cdot(m+1)=\frac{m+1}{m-1} $$
である。
段 4（下からの評価）。段 2 の左側と lem-dex-root（$m$ の代わりに $m+1$ を使う）から $e^h-1>e^{\frac1{m+1}}-1>\frac1{m+1}$ である。また段 1 から $\frac1h\ge m$ である。掛け合わせて
$$ \frac{e^h-1}h>\frac1{m+1}\cdot m=\frac m{m+1} $$
である。
段 5（右からの極限）。$\frac m{m+1}=1-\frac1{m+1}$、$\frac{m+1}{m-1}=1+\frac2{m-1}$ は、$m\to\infty$ でどちらも $1$ に近づく。段 1 より $h\to+0$ のとき $m\to\infty$ なので、はさみうちにより $\frac{e^h-1}h\to1$（$h\to+0$）である。同じく段 2 と lem-dex-root から $1< e^h<1+\frac1{m-1}$ なので、$e^h\to1$（$h\to+0$）もわかる。
段 6（左からの極限）。$h=-t$（$t>0$）とおく。指数法則から $e^{-t}e^t=e^0=1$ なので $e^{-t}=\frac1{e^t}$ であり、
$$ \frac{e^{-t}-1}{-t}=\frac{1-e^{-t}}t=\frac{e^{-t}(e^t-1)}t=e^{-t}\cdot\frac{e^t-1}t $$
である（3 つ目の等号では $1=e^{-t}e^t$ を使った）。$t\to+0$ のとき、段 5 から $e^t\to1$ なので $e^{-t}=\frac1{e^t}\to1$ であり、$\frac{e^t-1}t\to1$ である。よってこの値も $1$ に近づく。
段 7（導関数）。任意の実数 $x$ について、指数法則 $e^{x+h}=e^xe^h$ から
$$ \frac{e^{x+h}-e^x}h=e^x\cdot\frac{e^h-1}h\to e^x\cdot1=e^x\qquad(h\to0) $$
である。$\square$

方針：$a^x$ を $e^{cx}$ の形に書き直し、thm-dex-derivative-at-zero と合成関数の微分法を使う。
段 1（底の取り替え）。$c:=\log a$ とおく。$\log$ は $e^x$ の逆関数なので $e^c=a$ である。指数法則 $(e^c)^x=e^{cx}$ から
$$ a^x=(e^c)^x=e^{cx} $$
である。
段 2（微分）。$g(x)=cx$ とおくと $g'(x)=c$ であり、thm-dex-derivative-at-zero より $(e^u)'=e^u$ である。合成関数の微分法から
$$ (a^x)'=(e^{g(x)})'=e^{g(x)}\cdot g'(x)=c\,e^{cx}=(\log a)\,a^x $$
である。
段 3（底の一意性）。すべての $x$ で $(a^x)'=a^x$ とする。段 2 から $(\log a)\,a^x=a^x$ であり、$a^x>0$ なので両辺を $a^x$ で割って $\log a=1$ である。$e^x$ は単射で $e^1=e$ なので、$\log a=1$ は $a=e$ を意味する。逆に $a=e$ なら $\log e=1$ なので、段 2 から $(e^x)'=e^x$ である。$\square$

方針：$\log(x+h)-\log x$ を $u$ とおき、$h$ を $u$ で表して thm-dex-derivative-at-zero に帰着する。
段 1（置き換え）。$x>0$ を固定し、$h\ne0$、$x+h>0$ とする。$u:=\log(x+h)-\log x$ とおく。$\log$ は単射なので、$x+h\ne x$ から $u\ne0$ である。また $\log(x+h)=\log x+u$ の両辺を $e$ の肩に乗せると、指数法則により $x+h=x\,e^u$、すなわち $h=x(e^u-1)$ である。
段 2（差分商の書き直し）。段 1 から
$$ \frac{\log(x+h)-\log x}h=\frac u{x(e^u-1)}=\frac1x\cdot\frac1{\frac{e^u-1}u} $$
である。
段 3（極限）。$\log$ は連続なので（rem-dex-premises の 3）、$h\to0$ のとき $u=\log(x+h)-\log x\to0$ である。$u\ne0$ なので thm-dex-derivative-at-zero から $\frac{e^u-1}u\to1$ であり、段 2 の値は $\frac1x\cdot\frac11=\frac1x$ に近づく。$\square$

方針：$f$ を $e^x$ で割った関数の導関数が $0$ になることを示す。
段 1（$e^{-x}$ の導関数）。合成関数の微分法と thm-dex-derivative-at-zero から $(e^{-x})'=e^{-x}\cdot(-1)=-e^{-x}$ である。
段 2（割った関数の導関数）。$g(x):=f(x)e^{-x}$ とおく。積の微分法と段 1、仮定 $f'=f$ から
$$ g'(x)=f'(x)e^{-x}+f(x)\cdot(-e^{-x})=f(x)e^{-x}-f(x)e^{-x}=0 $$
である。
段 3（定数になる）。$\mathbb{R}$ は区間なので、rem-dex-premises の 4 により $g$ は定数である。$g(0)=f(0)e^0=f(0)$ なので、すべての $x$ で $f(x)e^{-x}=f(0)$ である。両辺に $e^x$ を掛けると、$e^{-x}e^x=1$ より $f(x)=f(0)e^x$ である。$\square$