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

Metamath Proof Explorer

Theorem absvalsqi

Description: Square of value of absolute value function. (Contributed by NM, 2-Oct-1999)

		Ref	Expression
	Hypothesis	absvalsqi.1	$⊢ A \in ℂ$
	Assertion	absvalsqi	$⊢ {\|A\|}^{2} = A \overline{A}$

Step	Hyp	Ref	Expression
1		absvalsqi.1	$⊢ A \in ℂ$
2		absvalsq	$⊢ A \in ℂ \to {\|A\|}^{2} = A \overline{A}$
3	1 2	ax-mp	$⊢ {\|A\|}^{2} = A \overline{A}$