This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem sqneg

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

Ref Expression
Assertion sqneg ⊢ A ∈ ℂ → − A 2 = A 2

Proof

Step Hyp Ref Expression
1 mul2neg ⊢ A ∈ ℂ ∧ A ∈ ℂ → − A ⁢ − A = A ⁢ A
2 1 anidms ⊢ A ∈ ℂ → − A ⁢ − A = A ⁢ A
3 negcl ⊢ A ∈ ℂ → − A ∈ ℂ
4 sqval ⊢ − A ∈ ℂ → − A 2 = − A ⁢ − A
5 3 4 syl ⊢ A ∈ ℂ → − A 2 = − A ⁢ − A
6 sqval ⊢ A ∈ ℂ → A 2 = A ⁢ A
7 2 5 6 3eqtr4d ⊢ A ∈ ℂ → − A 2 = A 2