Theorem zeo3 16297

Description: An integer is even or odd. With this representation of even and odd integers, this variant of zeo 12606 follows immediately from the law of excluded middle, see exmidd 901. (Contributed by AV, 17-Jun-2021.)

Assertion

Ref	Expression
zeo3	⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁))

Proof of Theorem zeo3

Step	Hyp	Ref	Expression
1		exmidd 901	1 ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 853   ∈ wcel 2119   class class class wbr 5072  2c2 12227  ℤcz 12515   ∥ cdvds 16212

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 208  df-or 854

This theorem is referenced by:  zeo5  16316