Theorem absgt0

Description: The absolute value of a nonzero number is positive. (Contributed by NM, 1-Oct-1999) (Proof shortened by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	absgt0	$$⊢A\in ℂ\to \left(A\ne 0\leftrightarrow 0<\left|A\right|\right)$$

Proof

Step	Hyp	Ref	Expression
1		0red	$$⊢A\in ℂ\to 0\in ℝ$$
2		abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$
3		absge0	$$⊢A\in ℂ\to 0\le \left|A\right|$$
4	1 2 3	leltned	$$⊢A\in ℂ\to \left(0<\left|A\right|\leftrightarrow \left|A\right|\ne 0\right)$$
5		abs00	$$⊢A\in ℂ\to \left(\left|A\right|=0\leftrightarrow A=0\right)$$
6	5	necon3bid	$$⊢A\in ℂ\to \left(\left|A\right|\ne 0\leftrightarrow A\ne 0\right)$$
7	4 6	bitr2d	$$⊢A\in ℂ\to \left(A\ne 0\leftrightarrow 0<\left|A\right|\right)$$