Theorem absvalsq

Description: Square of value of absolute value function. (Contributed by NM, 16-Jan-2006)

	Ref	Expression
Assertion	absvalsq	$$⊢A\in ℂ\to {\left|A\right|}^2=A\bar{A}$$

Proof

Step	Hyp	Ref	Expression
1		absval	$$⊢A\in ℂ\to \left|A\right|=\sqrt{A\bar{A}}$$
2	1	oveq1d	$$⊢A\in ℂ\to {\left|A\right|}^2={\sqrt{A\bar{A}}}^2$$
3		cjmulrcl	$$⊢A\in ℂ\to A\bar{A}\in ℝ$$
4		cjmulge0	$$⊢A\in ℂ\to 0\le A\bar{A}$$
5		resqrtth	$$⊢\left(A\bar{A}\in ℝ\wedge 0\le A\bar{A}\right)\to {\sqrt{A\bar{A}}}^2=A\bar{A}$$
6	3 4 5	syl2anc	$$⊢A\in ℂ\to {\sqrt{A\bar{A}}}^2=A\bar{A}$$
7	2 6	eqtrd	$$⊢A\in ℂ\to {\left|A\right|}^2=A\bar{A}$$