Theorem absge0

Description: Absolute value is nonnegative. (Contributed by NM, 20-Nov-2004) (Revised by Mario Carneiro, 29-May-2016)

	Ref	Expression
Assertion	absge0	$$⊢A\in ℂ\to 0\le \left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		cjmulrcl	$$⊢A\in ℂ\to A\bar{A}\in ℝ$$
2		cjmulge0	$$⊢A\in ℂ\to 0\le A\bar{A}$$
3		sqrtge0	$$⊢\left(A\bar{A}\in ℝ\wedge 0\le A\bar{A}\right)\to 0\le \sqrt{A\bar{A}}$$
4	1 2 3	syl2anc	$$⊢A\in ℂ\to 0\le \sqrt{A\bar{A}}$$
5		absval	$$⊢A\in ℂ\to \left|A\right|=\sqrt{A\bar{A}}$$
6	4 5	breqtrrd	$$⊢A\in ℂ\to 0\le \left|A\right|$$