Database
SUPPLEMENTARY MATERIAL (USERS' MATHBOXES)
Mathbox for Igor Ieskov
sqnegd
Next ⟩
negexpidd
Metamath Proof Explorer
Ascii
Unicode
Theorem
sqnegd
Description:
The square of the negative of a number.
(Contributed by
Igor Ieskov
, 21-Jan-2024)
Ref
Expression
Hypothesis
sqnegd.1
⊢
φ
→
A
∈
ℂ
Assertion
sqnegd
⊢
φ
→
−
A
2
=
A
2
Proof
Step
Hyp
Ref
Expression
1
sqnegd.1
⊢
φ
→
A
∈
ℂ
2
sqneg
⊢
A
∈
ℂ
→
−
A
2
=
A
2
3
1
2
syl
⊢
φ
→
−
A
2
=
A
2