Proof of The Exponential Function Dominates Every Polynomial Function

Write $\iota=\iota_{\mathbb{R}}$ for the canonical map of $\mathbb{R}$ and $S$ for the successor map of Natural Numbers.

Step 1 (a bound valid for $t\ge 1$). By claim 2 of Growth Bound for a Polynomial Function on the Real Line there are $N\in\mathbb{N}$ and $C\in\mathbb{R}$ with $0\le C$ such that $|p(t)|\le C\,t^{N}$ for every $t\in\mathbb{R}$ with $1\le t$, where the powers are the natural number powers of $\mathbb{R}$. Put $\mu=\iota(S(N))$ and $D=C\,\mu^{S(N)}$; by The Exponential Function Dominates Every Power we have $0<\mu$, hence $0\le\mu^{S(N)}$ by claim 5 of Properties of Natural Number Powers in a Field and therefore $0\le D$ by claim 5 of Elementary Arithmetic in an Ordered Field.

Let $t\in\mathbb{R}$ with $1\le t$. Then $0<1\le t$ by claim 6 of Elementary Order Arithmetic in an Ordered Field and claim 2 of that lemma, so $0<t$ and $t^{-1}$ exists with $0<t^{-1}$ by claim 7 of that lemma. By claim 2 of Basic Properties of the Exponential Function we have $0<\exp(-t)$, so multiplying $|p(t)|\le C\,t^{N}$ by $\exp(-t)$ using claim 5 of Elementary Arithmetic in an Ordered Field gives

By The Exponential Function Dominates Every Power, $t^{N}\exp(-t)\le\mu^{S(N)}t^{-1}$; multiplying by the nonnegative element $C$, again by claim 5 of Elementary Arithmetic in an Ordered Field, and using associativity of multiplication,

By transitivity of the order of the ordered field $\mathbb{R}$,

Step 2 (claim 1). Let $\varepsilon\in\mathbb{R}$ with $0<\varepsilon$. Then $\varepsilon^{-1}$ exists and $0<\varepsilon^{-1}$ by claim 7 of Elementary Order Arithmetic in an Ordered Field, so $0\le D\varepsilon^{-1}$ by claim 5 of Elementary Arithmetic in an Ordered Field. Put $M=1+D\varepsilon^{-1}$. Adding $1$ to $0\le D\varepsilon^{-1}$ gives $1\le M$, and adding $D\varepsilon^{-1}$ to $0<1$ gives $D\varepsilon^{-1}<M$, both by claim 1 of Elementary Order Arithmetic in an Ordered Field together with the trivial case of equality.

Let $t\in\mathbb{R}$ with $M\le t$. Then $1\le t$ by transitivity, and $D\varepsilon^{-1}<t$ by claim 2 of Elementary Order Arithmetic in an Ordered Field. Since $0<t$, as in Step 1, and $0<\varepsilon t^{-1}$ by claim 5 of Elementary Order Arithmetic in an Ordered Field, multiplying the strict inequality $D\varepsilon^{-1}<t$ by $\varepsilon t^{-1}$ using claim 10 of that lemma gives

by commutativity and associativity of multiplication and $\varepsilon^{-1}\varepsilon=1=t\,t^{-1}$. Combining with the bound of Step 1 and claim 2 of Elementary Order Arithmetic in an Ordered Field,

which proves claim 1.

Step 3 (claim 2). Let $\varepsilon\in\mathbb{R}$ with $0<\varepsilon$ and let $M$ be as in claim 1, so $1\le M$ and hence $0<M$ by claim 6 and claim 2 of Elementary Order Arithmetic in an Ordered Field. Put $\delta=M^{-1}$; then $0<\delta$ by claim 7 of that lemma.

Let $s\in\mathbb{R}$ with $0<s<\delta$. Then $s^{-1}$ exists and $0<s^{-1}$ by claim 7 of Elementary Order Arithmetic in an Ordered Field, and $0<Ms^{-1}$ by claim 5 of that lemma. Multiplying the strict inequality $s<M^{-1}$ by $Ms^{-1}$ using claim 10 of that lemma gives

by commutativity and associativity of multiplication and $s\,s^{-1}=1=M^{-1}M$. In particular $M\le s^{-1}$, so claim 1 applied to $t=s^{-1}$ gives

which proves claim 2.