Is this proof correct, $\lvert x \rvert=0$ iff $x=0$?

Question

I looking for comments and corrections on my proof. I'm also unsure if the second case is correct.

For $x\in \mathbb{R}$ we have:

$\lvert x\rvert \geq 0$, and $\lvert x \rvert=0$ if and only if $x=0$.

I have three cases:

1. For $x>0$, the absolute value $\lvert x\rvert=x$ is greater than zero, so $x \neq 0$. This case not true according to the theorem.

2. For $x<0$, we have $\lvert x\rvert =-x>0$, which is less than zero, so $x<0$. This case not true according to the theorem.

3. For $x=0$, we have $\lvert x\rvert=0$, according to the theorem. Therefore the theorem is true only for $x=0$.

Thanks!

Answer 1

If the absolute value is defined as

$$|x|:=\begin{cases}x>0\to x\\x=0\to0\\x<0\to-x\end{cases},$$

you can say $$|x|\ge0\iff (x>0\land x\ge0)\lor(x=0\land 0\ge0)\lor(x<0\land-x\ge0)\\\iff x>0\lor x=0\lor x<0\iff\text{true}.$$ $$|x|=0\iff (x>0\land x=0)\lor(x=0\land 0=0)\lor(x<0\land-x=0)\\\iff x=0\lor x=0\lor x=0\iff x=0.$$

If it is defined as

$$|x|:=\begin{cases}x\ge0\to x\\x\le0\to-x\end{cases},$$

you can say

$$|x|\ge0\iff (x\ge0\land x\ge0)\lor(x\le0\land-x\ge0)\iff x\ge0\lor x\le 0\iff\text{true}.$$ $$|x|=0\iff (x\ge0\land x=0)\lor(x\le0\land-x=0)\\\iff x=0\lor x=0\iff x=0.$$

If it is defined as

$$|x|:=\sqrt{x^2},$$ then

$$\sqrt{x^2}\ge0$$ by definition of the square root, and by squaring, then solving the quadratic equation

$$\sqrt{x^2}=0\iff x^2=0^2=0\iff x=0.$$

Answer 2

The theorem should be interpreted as

For $x\in \mathbb{R}$ we have: $(\lvert x\rvert \geq 0$) and ($\lvert x \rvert=0$ if and only if $x=0$).

With this in mind, the theorem should be straightforward to prove using your casework.