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

Metamath Proof Explorer

Theorem absresq

Description: Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006)

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

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