Theorem zeo3 16507

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

Assertion

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

Proof of Theorem zeo3

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ∨ wo 861   ∈ wcel 2145   class class class wbr 5103  2c2 12397  ℤcz 12693   ∥ cdvds 16422

This proof depends on axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-3 8

This proof depends on definitions:  df-bi 210  df-or 862

This theorem is used by:  zeo5  16526