MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  zeo4 Structured version   Visualization version   GIF version

Theorem zeo4 16372
Description: An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 12703 follows immediately from the principle of double negation, see notnotb 315. (Contributed by AV, 17-Jun-2021.)
Assertion
Ref Expression
zeo4 (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁))

Proof of Theorem zeo4
StepHypRef Expression
1 notnotb 315 . 2 (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)
21a1i 11 1 (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁))
Colors of variables: wff setvar class
Syntax hints:  ¬ wn 3  wi 4  wb 206  wcel 2106   class class class wbr 5148  2c2 12319  cz 12611  cdvds 16287
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 207
This theorem is referenced by: (None)
  Copyright terms: Public domain W3C validator