![]() |
Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
|
Mirrors > Home > MPE Home > Th. List > zeo3 | Structured version Visualization version GIF version |
Description: An integer is even or odd. With this representation of even and odd integers, this variant of zeo 12646 follows immediately from the law of excluded middle, see exmidd 892. (Contributed by AV, 17-Jun-2021.) |
Ref | Expression |
---|---|
zeo3 | ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | exmidd 892 | 1 ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ∨ wo 844 ∈ wcel 2098 class class class wbr 5139 2c2 12265 ℤcz 12556 ∥ cdvds 16196 |
This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 |
This theorem depends on definitions: df-bi 206 df-or 845 |
This theorem is referenced by: zeo5 16298 |
Copyright terms: Public domain | W3C validator |