absre

Description: Absolute value of a real number. (Contributed by NM, 17-Mar-2005)

		Ref	Expression
	Assertion	absre	$⊢ A \in ℝ \to \|A\| = \sqrt{A^{2}}$

Step	Hyp	Ref	Expression
1		recn	$⊢ A \in ℝ \to A \in ℂ$
2		absval	$⊢ A \in ℂ \to \|A\| = \sqrt{A \overline{A}}$
3	1 2	syl	$⊢ A \in ℝ \to \|A\| = \sqrt{A \overline{A}}$
4	1	sqvald	$⊢ A \in ℝ \to A^{2} = A A$
5		cjre	$⊢ A \in ℝ \to \overline{A} = A$
6	5	oveq2d	$⊢ A \in ℝ \to A \overline{A} = A A$
7	4 6	eqtr4d	$⊢ A \in ℝ \to A^{2} = A \overline{A}$
8	7	fveq2d	$⊢ A \in ℝ \to \sqrt{A^{2}} = \sqrt{A \overline{A}}$
9	3 8	eqtr4d	$⊢ A \in ℝ \to \|A\| = \sqrt{A^{2}}$

Metamath Proof Explorer