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 | ⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ∨ 2 ∥ ( 𝑁 + 1 ) ) ) |
| Step | Hyp | Ref | Expression |
|---|---|---|---|
| 1 | zeo3 | ⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁 ) ) | |
| 2 | oddp1even | ⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ 2 ∥ ( 𝑁 + 1 ) ) ) | |
| 3 | 2 | bicomd | ⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ ( 𝑁 + 1 ) ↔ ¬ 2 ∥ 𝑁 ) ) |
| 4 | 3 | orbi2d | ⊢ ( 𝑁 ∈ ℤ → ( ( 2 ∥ 𝑁 ∨ 2 ∥ ( 𝑁 + 1 ) ) ↔ ( 2 ∥ 𝑁 ∨ ¬ 2 ∥ 𝑁 ) ) ) |
| 5 | 1 4 | mpbird | ⊢ ( 𝑁 ∈ ℤ → ( 2 ∥ 𝑁 ∨ 2 ∥ ( 𝑁 + 1 ) ) ) |