Let $t \mapsto |t|$ be the D412: Absolute value function.
Let $x \in \mathbb{R}$ be a D993: Real number.
Let $x \in \mathbb{R}$ be a D993: Real number.
Then
(1) | \begin{equation} - |x| \leq x \leq |x| \end{equation} |
(2) | \begin{equation} - |x| = x = |x| \quad \iff \quad x = 0 \end{equation} |