Theorem zeo3 16306

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

Assertion

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

Proof of Theorem zeo3

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

Syntax hints:  ¬ wn 3   → wi 4   ∨ wo 848   ∈ wcel 2114   class class class wbr 5085  2c2 12236  ℤcz 12524   ∥ cdvds 16221

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 207  df-or 849

This theorem is referenced by:  zeo5  16325