Metamath Proof Explorer


Theorem sq0i

Description: If a number is zero, then its square is zero. (Contributed by FL, 10-Dec-2006)

Ref Expression
Assertion sq0i ⊢ A = 0 → A 2 = 0

Proof

Step Hyp Ref Expression
1 oveq1 ⊢ A = 0 → A 2 = 0 2
2 sq0 ⊢ 0 2 = 0
3 1 2 eqtrdi ⊢ A = 0 → A 2 = 0