Metamath Proof Explorer


Theorem sqnegd

Description: The square of the negative of a number. (Contributed by Igor Ieskov, 21-Jan-2024)

Ref Expression
Hypothesis sqnegd.1 ( 𝜑𝐴 ∈ ℂ )
Assertion sqnegd ( 𝜑 → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )

Proof

Step Hyp Ref Expression
1 sqnegd.1 ( 𝜑𝐴 ∈ ℂ )
2 sqneg ( 𝐴 ∈ ℂ → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )
3 1 2 syl ( 𝜑 → ( - 𝐴 ↑ 2 ) = ( 𝐴 ↑ 2 ) )