Theorem absneg

Description: Absolute value of the negative. (Contributed by NM, 27-Feb-2005)

	Ref	Expression
Assertion	absneg	$$⊢A\in ℂ\to \left|-A\right|=\left|A\right|$$

Proof

Step	Hyp	Ref	Expression
1		cjneg	$$⊢A\in ℂ\to \overline{-A}=-\bar{A}$$
2	1	oveq2d	$$⊢A\in ℂ\to \left(-A\right)\overline{-A}=\left(-A\right)\left(-\bar{A}\right)$$
3		cjcl	$$⊢A\in ℂ\to \bar{A}\in ℂ$$
4		mul2neg	$$⊢\left(A\in ℂ\wedge \bar{A}\in ℂ\right)\to \left(-A\right)\left(-\bar{A}\right)=A\bar{A}$$
5	3 4	mpdan	$$⊢A\in ℂ\to \left(-A\right)\left(-\bar{A}\right)=A\bar{A}$$
6	2 5	eqtrd	$$⊢A\in ℂ\to \left(-A\right)\overline{-A}=A\bar{A}$$
7	6	fveq2d	$$⊢A\in ℂ\to \sqrt{\left(-A\right)\overline{-A}}=\sqrt{A\bar{A}}$$
8		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
9		absval	$$⊢-A\in ℂ\to \left|-A\right|=\sqrt{\left(-A\right)\overline{-A}}$$
10	8 9	syl	$$⊢A\in ℂ\to \left|-A\right|=\sqrt{\left(-A\right)\overline{-A}}$$
11		absval	$$⊢A\in ℂ\to \left|A\right|=\sqrt{A\bar{A}}$$
12	7 10 11	3eqtr4d	$$⊢A\in ℂ\to \left|-A\right|=\left|A\right|$$