Theorem abscl

Description: Real closure of absolute value. (Contributed by NM, 3-Oct-1999)

	Ref	Expression
Assertion	abscl	$$⊢A\in ℂ\to \left|A\right|\in ℝ$$

Proof

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