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

Metamath Proof Explorer

Theorem absval2

Description: Value of absolute value function. Definition 10.36 of Gleason p. 133. (Contributed by NM, 17-Mar-2005)

		Ref	Expression
	Assertion	absval2	$⊢ A \in ℂ \to \|A\| = \sqrt{{ℜ (A)}^{2} + {ℑ (A)}^{2}}$

Step	Hyp	Ref	Expression
1		absval	$⊢ A \in ℂ \to \|A\| = \sqrt{A \overline{A}}$
2		cjmulval	$⊢ A \in ℂ \to A \overline{A} = {ℜ (A)}^{2} + {ℑ (A)}^{2}$
3	2	fveq2d	$⊢ A \in ℂ \to \sqrt{A \overline{A}} = \sqrt{{ℜ (A)}^{2} + {ℑ (A)}^{2}}$
4	1 3	eqtrd	$⊢ A \in ℂ \to \|A\| = \sqrt{{ℜ (A)}^{2} + {ℑ (A)}^{2}}$