Theorem zeo3 16046

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

Assertion

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

Proof of Theorem zeo3

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 844   ∈ wcel 2106   class class class wbr 5074  2c2 12028  ℤcz 12319   ∥ cdvds 15963

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  16065