theorem zdvd02 (a: nat): $ a |Z 0 $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zdvdeq2 | b0 0 = 0 -> (a |Z b0 0 <-> a |Z 0) |
|
| 2 | b00 | b0 0 = 0 |
|
| 3 | 1, 2 | ax_mp | a |Z b0 0 <-> a |Z 0 |
| 4 | zdvdb02 | a |Z b0 0 <-> zabs a || 0 |
|
| 5 | dvd02 | zabs a || 0 |
|
| 6 | 4, 5 | mpbir | a |Z b0 0 |
| 7 | 3, 6 | mpbi | a |Z 0 |