theorem zle02 (a: nat): $ 0 <=Z a <-> ~odd a $;
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | noteq | (a <Z 0 <-> odd a) -> (~a <Z 0 <-> ~odd a) |
|
| 2 | 1 | conv zle | (a <Z 0 <-> odd a) -> (0 <=Z a <-> ~odd a) |
| 3 | zlt01 | a <Z 0 <-> odd a |
|
| 4 | 2, 3 | ax_mp | 0 <=Z a <-> ~odd a |