Description: An integer is even or odd. With this representation of even and odd integers, this variant of zeo follows immediately from the law of excluded middle, see exmidd . (Contributed by AV, 17-Jun-2021)
Ref | Expression | ||
---|---|---|---|
Assertion | zeo3 | ⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁 ) ) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exmidd | ⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁 ) ) |