Proof of The Exponential Function Dominates Every Power

Write $\iota=\iota_{\mathbb{R}}$ and $n^{\ast}=S(m)$.

Step 0 (two elementary facts). (i) If $y,z\in\mathbb{R}$ with $y\ne0$ and $yz=1$, then $z=y^{-1}$, because $z=(y^{-1}y)z=y^{-1}(yz)=y^{-1}$. (ii) If $a,b\in\mathbb{R}$ with $0<a$ and $a\le b$, then $b^{-1}\le a^{-1}$: by claim 2 of Elementary Order Arithmetic in an Ordered Field we have $0<b$, so $a^{-1}$ and $b^{-1}$ exist and are positive by claim 7 of that lemma, hence $0<a^{-1}b^{-1}$ by claim 5 of that lemma; multiplying $a\le b$ by $a^{-1}b^{-1}$ using claim 5 of Elementary Arithmetic in an Ordered Field gives $a\,a^{-1}b^{-1}\le b\,a^{-1}b^{-1}$, that is, $b^{-1}\le a^{-1}$.

Step 1 (positivity of $\mu$). By claim 3 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field, $0<\iota(n^{\ast})=\mu$, so $\mu^{-1}$ exists and $0<\mu^{-1}$ by claim 7 of Elementary Order Arithmetic in an Ordered Field. Moreover $0\le\mu^{n^{\ast}}$ by claim 5 of Properties of Natural Number Powers in a Field and $\mu^{n^{\ast}}\ne0$ by claim 4 of that lemma, so $0<\mu^{n^{\ast}}$.

Step 2 (the exponential of a natural multiple). For all $n\in\mathbb{N}$ and $u\in\mathbb{R}$,

Let $E$ be the set of $n\in\mathbb{N}$ for which this holds for every $u$. By claim 1 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field, $\iota(1)=1$, and $\exp(u)^{1}=\exp(u)$ by claim 1 of Properties of Natural Number Powers in a Field, so $1\in E$. Let $n\in E$. By claim 1 of Arithmetic of Addition on the Natural Numbers we have $S(n)=n+1$, so $\iota(S(n))=\iota(n)+1$ by claim 1 of Properties of the Canonical Map from the Natural Numbers to an Ordered Field, whence $\iota(S(n))u=\iota(n)u+u$ by distributivity. By claim 1 of Basic Properties of the Exponential Function and claim 1 of Properties of Natural Number Powers in a Field,

so $S(n)\in E$. By Principle of Induction for the Natural Numbers, $E=\mathbb{N}$.

Step 3 (the substitution). Let $t\in\mathbb{R}$ with $0<t$ and put $u=t\mu^{-1}$. Then $0<u$ by claim 5 of Elementary Order Arithmetic in an Ordered Field, and by commutativity and associativity of multiplication

so Step 2 gives $\exp(t)=\exp(u)^{n^{\ast}}$.

Step 4 (the lower bound for $\exp(t)$). Since $0<1$ by claim 6 of Elementary Order Arithmetic in an Ordered Field, claim 1 of that lemma gives $u=0+u<1+u$, hence $u\le 1+u$; and $1+u\le\exp(u)$ by claim 4 of Basic Properties of the Exponential Function, which applies because $0\le u$. Hence $u\le\exp(u)$, and claim 5 of Properties of Natural Number Powers in a Field gives

Moreover $0<u^{n^{\ast}}$, by claims 5 and 4 of Properties of Natural Number Powers in a Field as in Step 1. By claim 3 of Properties of Natural Number Powers in a Field, $u^{n^{\ast}}=\bigl(t\mu^{-1}\bigr)^{n^{\ast}}=t^{n^{\ast}}\bigl(\mu^{-1}\bigr)^{n^{\ast}}$; and by claims 3 and 2 of that lemma,

so $\bigl(\mu^{-1}\bigr)^{n^{\ast}}=\bigl(\mu^{n^{\ast}}\bigr)^{-1}$ by Step 0(i) and Step 1. Thus, writing $A=u^{n^{\ast}}=t^{n^{\ast}}\bigl(\mu^{n^{\ast}}\bigr)^{-1}$, we have $0<A\le\exp(t)$.

Step 5 (conclusion). By claim 2 of Basic Properties of the Exponential Function, $0<\exp(t)$ and $\exp(-t)=\exp(t)^{-1}$. By Step 0(ii) applied to $0<A\le\exp(t)$,

As in Step 1, $0<t^{m}$ and $0<t^{n^{\ast}}$, so multiplying by $t^{m}$ using claim 5 of Elementary Arithmetic in an Ordered Field gives $t^{m}\exp(-t)\le t^{m}A^{-1}$.

It remains to identify $t^{m}A^{-1}$. First,

so $A^{-1}=\mu^{n^{\ast}}\bigl(t^{n^{\ast}}\bigr)^{-1}$ by Step 0(i). Second, $t^{n^{\ast}}=t^{S(m)}=t^{m}t$ by claim 1 of Properties of Natural Number Powers in a Field, so

whence $t^{m}\bigl(t^{n^{\ast}}\bigr)^{-1}=t^{-1}$ by Step 0(i). Combining, and using commutativity and associativity of multiplication,

so $t^{m}\exp(-t)\le\mu^{S(m)}t^{-1}$, as claimed.