Description: If a number is zero, then its square is zero. Deduction form of sq0i . Converse of sqeq0d . (Contributed by David Moews, 28-Feb-2017)
| Ref | Expression | ||
|---|---|---|---|
| Hypothesis | sq0id.1 | |- ( ph -> A = 0 ) |
|
| Assertion | sq0id | |- ( ph -> ( A ^ 2 ) = 0 ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | sq0id.1 | |- ( ph -> A = 0 ) |
|
| 2 | sq0i | |- ( A = 0 -> ( A ^ 2 ) = 0 ) |
|
| 3 | 1 2 | syl | |- ( ph -> ( A ^ 2 ) = 0 ) |