ThmDex – An index of mathematical definitions, results, and conjectures.
Result R3416 on D412: Absolute value function
Absolute value bounds for a basic real number
Formulation 0
Let $t \mapsto |t|$ be the D412: Absolute value function.
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}