Theorem zeo4 16508

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

Assertion

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

Proof of Theorem zeo4

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

This proof depends on syntax axioms:  ¬ wn 3   → wi 4   ↔ wb 209   ∈ 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

This theorem is used by: (None)