Metamath Proof Explorer |
< Previous
Next >
Nearby theorems |
||
Mirrors > Home > MPE Home > Th. List > zeo4 | Structured version Visualization version GIF version |
Description: An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 12521 follows immediately from the principle of double negation, see notnotb 315. (Contributed by AV, 17-Jun-2021.) |
Ref | Expression |
---|---|
zeo4 | ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 315 | . 2 ⊢ (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁) | |
2 | 1 | a1i 11 | 1 ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 205 ∈ wcel 2107 class class class wbr 5104 2c2 12142 ℤcz 12433 ∥ cdvds 16071 |
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 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |