Theorem sq0i

Description: If a number is zero, then 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 )