Theorem absresq

Description: Square of the absolute value of a real number. (Contributed by NM, 16-Jan-2006)

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

Proof

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