Metamath Proof Explorer

Theorem zeo5

Description: An integer is either even or odd, version of zeo3 avoiding the negation of the representation of an odd number. (Proposed by BJ, 21-Jun-2021.) (Contributed by AV, 26-Jun-2020)

Ref Expression
Assertion zeo5 ⊢ N ∈ ℤ → 2 ∥ N ∨ 2 ∥ N + 1

Proof

Step Hyp Ref Expression
1 zeo3 ⊢ N ∈ ℤ → 2 ∥ N ∨ ¬ 2 ∥ N
2 oddp1even ⊢ N ∈ ℤ → ¬ 2 ∥ N ↔ 2 ∥ N + 1
3 2 bicomd ⊢ N ∈ ℤ → 2 ∥ N + 1 ↔ ¬ 2 ∥ N
4 3 orbi2d ⊢ N ∈ ℤ → 2 ∥ N ∨ 2 ∥ N + 1 ↔ 2 ∥ N ∨ ¬ 2 ∥ N
5 1 4 mpbird ⊢ N ∈ ℤ → 2 ∥ N ∨ 2 ∥ N + 1