Metamath Proof Explorer


Theorem sq0i

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

Ref Expression
Assertion sq0i ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = 0 )

Proof

Step Hyp Ref Expression
1 oveq1 ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = ( 0 ↑ 2 ) )
2 sq0 ( 0 ↑ 2 ) = 0
3 1 2 eqtrdi ( 𝐴 = 0 → ( 𝐴 ↑ 2 ) = 0 )