Theorem abscl

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

	Ref	Expression
Assertion	abscl	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		absval	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) = ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) )
2		cjmulrcl	⊢ ( 𝐴 ∈ ℂ → ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ )
3		cjmulge0	⊢ ( 𝐴 ∈ ℂ → 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) )
4		resqrtcl	⊢ ( ( ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) → ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ )
5	2 3 4	syl2anc	⊢ ( 𝐴 ∈ ℂ → ( √ ‘ ( 𝐴 · ( ∗ ‘ 𝐴 ) ) ) ∈ ℝ )
6	1 5	eqeltrd	⊢ ( 𝐴 ∈ ℂ → ( abs ‘ 𝐴 ) ∈ ℝ )