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 )