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 11340 follows immediatly from the principle of double negation, see notnotb 303. (Contributed by AV, 17-Jun-2021.) |
Ref | Expression |
---|---|
zeo4 | ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)) |
Step | Hyp | Ref | Expression |
---|---|---|---|
1 | notnotb 303 | . 2 ⊢ (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁) | |
2 | 1 | a1i 11 | 1 ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)) |
Colors of variables: wff setvar class |
Syntax hints: ¬ wn 3 → wi 4 ↔ wb 195 ∈ wcel 1977 class class class wbr 4583 2c2 10947 ℤcz 11254 ∥ cdvds 14821 |
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 196 |
This theorem is referenced by: (None) |
Copyright terms: Public domain | W3C validator |