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

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

Proof of Theorem zeo3
StepHypRef 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 5141  2c2 12271  cz 12562  cdvds 16204
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  16306
  Copyright terms: Public domain W3C validator