Theorem absval

Description: The absolute value (modulus) of a complex number. Proposition 10-3.7(a) of Gleason p. 133. (Contributed by NM, 27-Jul-1999) (Revised by Mario Carneiro, 7-Nov-2013)

	Ref	Expression
Assertion	absval	$$⊢A\in ℂ\to \left|A\right|=\sqrt{A\bar{A}}$$

Proof

Step	Hyp	Ref	Expression
1		fveq2	$$⊢x=A\to \bar{x}=\bar{A}$$
2		oveq12	$$⊢\left(x=A\wedge \bar{x}=\bar{A}\right)\to x\bar{x}=A\bar{A}$$
3	1 2	mpdan	$$⊢x=A\to x\bar{x}=A\bar{A}$$
4	3	fveq2d	$$⊢x=A\to \sqrt{x\bar{x}}=\sqrt{A\bar{A}}$$
5		df-abs	$$⊢\mathrm{abs}=\left(x\in ℂ⟼\sqrt{x\bar{x}}\right)$$
6		fvex	$$⊢\sqrt{A\bar{A}}\in \mathrm{V}$$
7	4 5 6	fvmpt	$$⊢A\in ℂ\to \left|A\right|=\sqrt{A\bar{A}}$$