Description: 0 is an even number. (Contributed by AV, 11-Feb-2020) (Revised by AV, 17-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0evenALTV | |- 0 e. Even |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0z | |- 0 e. ZZ |
|
| 2 | 2cn | |- 2 e. CC |
|
| 3 | 2ne0 | |- 2 =/= 0 |
|
| 4 | 2 3 | div0i | |- ( 0 / 2 ) = 0 |
| 5 | 4 1 | eqeltri | |- ( 0 / 2 ) e. ZZ |
| 6 | iseven | |- ( 0 e. Even <-> ( 0 e. ZZ /\ ( 0 / 2 ) e. ZZ ) ) |
|
| 7 | 1 5 6 | mpbir2an | |- 0 e. Even |