Theorem zeo3 16308

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

Assertion

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

Proof of Theorem zeo3

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 846   ∈ wcel 2099   class class class wbr 5143  2c2 12292  ℤcz 12583   ∥ cdvds 16225

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 847

This theorem is referenced by:  zeo5  16327