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 \left|A\right|=\sqrt{{\Re \left(A\right)}^2+{\Im \left(A\right)}^2}$$

Proof

Step	Hyp	Ref	Expression
1		absval	$$⊢A\in ℂ\to \left|A\right|=\sqrt{A\bar{A}}$$
2		cjmulval	$$⊢A\in ℂ\to A\bar{A}={\Re \left(A\right)}^2+{\Im \left(A\right)}^2$$
3	2	fveq2d	$$⊢A\in ℂ\to \sqrt{A\bar{A}}=\sqrt{{\Re \left(A\right)}^2+{\Im \left(A\right)}^2}$$
4	1 3	eqtrd	$$⊢A\in ℂ\to \left|A\right|=\sqrt{{\Re \left(A\right)}^2+{\Im \left(A\right)}^2}$$