absvalsq

Description: Square of value of absolute value function. (Contributed by NM, 16-Jan-2006)

		Ref	Expression
	Assertion	absvalsq	$⊢ A \in ℂ \to {\|A\|}^{2} = A \overline{A}$

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

Metamath Proof Explorer