Theorem sqneg

Description: The square of the negative of a number. (Contributed by NM, 15-Jan-2006)

	Ref	Expression
Assertion	sqneg	$$⊢A\in ℂ\to {\left(-A\right)}^2=A^2$$

Proof

Step	Hyp	Ref	Expression
1		mul2neg	$$⊢\left(A\in ℂ\wedge A\in ℂ\right)\to \left(-A\right)\left(-A\right)=AA$$
2	1	anidms	$$⊢A\in ℂ\to \left(-A\right)\left(-A\right)=AA$$
3		negcl	$$⊢A\in ℂ\to -A\in ℂ$$
4		sqval	$$⊢-A\in ℂ\to {\left(-A\right)}^2=\left(-A\right)\left(-A\right)$$
5	3 4	syl	$$⊢A\in ℂ\to {\left(-A\right)}^2=\left(-A\right)\left(-A\right)$$
6		sqval	$$⊢A\in ℂ\to A^2=AA$$
7	2 5 6	3eqtr4d	$$⊢A\in ℂ\to {\left(-A\right)}^2=A^2$$