Theorem zeo4 15681

Description: An integer is even or odd but not both. With this representation of even and odd integers, this variant of zeo2 12063 follows immediately from the principle of double negation, see notnotb 317. (Contributed by AV, 17-Jun-2021.)

Assertion

Ref	Expression
zeo4	⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁))

Proof of Theorem zeo4

Step	Hyp	Ref	Expression
1		notnotb 317	. 2 ⊢ (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁)
2	1	a1i 11	1 ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ¬ ¬ 2 ∥ 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ↔ wb 208   ∈ wcel 2110   class class class wbr 5058  2c2 11686  ℤcz 11975   ∥ cdvds 15601

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 209

This theorem is referenced by: (None)