This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem abscl

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

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

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