Description: 0 is an even number. (Contributed by AV, 11-Feb-2020) (Revised by AV, 17-Jun-2020)
| Ref | Expression | ||
|---|---|---|---|
| Assertion | 0evenALTV | ⊢ 0 ∈ Even |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | 0z | ⊢ 0 ∈ ℤ | |
| 2 | 2cn | ⊢ 2 ∈ ℂ | |
| 3 | 2ne0 | ⊢ 2 ≠ 0 | |
| 4 | 2 3 | div0i | ⊢ ( 0 / 2 ) = 0 |
| 5 | 4 1 | eqeltri | ⊢ ( 0 / 2 ) ∈ ℤ |
| 6 | iseven | ⊢ ( 0 ∈ Even ↔ ( 0 ∈ ℤ ∧ ( 0 / 2 ) ∈ ℤ ) ) | |
| 7 | 1 5 6 | mpbir2an | ⊢ 0 ∈ Even |