The Exponential Bump Building Block is Smooth on the Real Line

Let $\mathbb{R}$ be the real numbers, an ordered field with order $\le$, regarded also as the Euclidean space $\mathbb{R}^{1}$, which is an open subset of itself by claim 1 of Polynomial Functions on the Real Line are Smooth. Write $s^{-1}$ for the multiplicative inverse of $s\in\mathbb{R}$ with $s\ne 0$, and let $\exp$ be the exponential function.

Let $\varphi:\mathbb{R}\to\mathbb{R}$ be the function given by

$$\varphi(s)=\exp\bigl(-\bigl(s^{-1}\bigr)\bigr)\ \text{ for }0<s,\qquad \varphi(s)=0\ \text{ for }s\le 0.$$

Then the following hold.

1. (Sign) $0\le\varphi(s)$ for every $s\in\mathbb{R}$; and for $s\in\mathbb{R}$ one has $0<\varphi(s)$ if and only if $0<s$.

2. (Smoothness) $\varphi$ is a smooth map on $\mathbb{R}^{1}$.