Theorem absre

Description: Absolute value of a real number. (Contributed by NM, 17-Mar-2005)

	Ref	Expression
Assertion	absre	$$⊢A\in ℝ\to \left|A\right|=\sqrt{A^2}$$

Proof

Step	Hyp	Ref	Expression
1		recn	$$⊢A\in ℝ\to A\in ℂ$$
2		absval	$$⊢A\in ℂ\to \left|A\right|=\sqrt{A\bar{A}}$$
3	1 2	syl	$$⊢A\in ℝ\to \left|A\right|=\sqrt{A\bar{A}}$$
4	1	sqvald	$$⊢A\in ℝ\to A^2=AA$$
5		cjre	$$⊢A\in ℝ\to \bar{A}=A$$
6	5	oveq2d	$$⊢A\in ℝ\to A\bar{A}=AA$$
7	4 6	eqtr4d	$$⊢A\in ℝ\to A^2=A\bar{A}$$
8	7	fveq2d	$$⊢A\in ℝ\to \sqrt{A^2}=\sqrt{A\bar{A}}$$
9	3 8	eqtr4d	$$⊢A\in ℝ\to \left|A\right|=\sqrt{A^2}$$