Metamath Proof Explorer

Theorem zeoALTV

Description: An integer is even or odd. (Contributed by NM, 1-Jan-2006) (Revised by AV, 16-Jun-2020)

Ref Expression
Assertion zeoALTV ( 𝑍 ∈ ℤ → ( 𝑍 ∈ Even ∨ 𝑍 ∈ Odd ) )

Proof

Step Hyp Ref Expression
1 zeo ⊢ ( 𝑍 ∈ ℤ → ( ( 𝑍 / 2 ) ∈ ℤ ∨ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) )
2 1 ancli ⊢ ( 𝑍 ∈ ℤ → ( 𝑍 ∈ ℤ ∧ ( ( 𝑍 / 2 ) ∈ ℤ ∨ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) ) )
3 andi ⊢ ( ( 𝑍 ∈ ℤ ∧ ( ( 𝑍 / 2 ) ∈ ℤ ∨ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) ) ↔ ( ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) ∨ ( 𝑍 ∈ ℤ ∧ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) ) )
4 2 3 sylib ⊢ ( 𝑍 ∈ ℤ → ( ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) ∨ ( 𝑍 ∈ ℤ ∧ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) ) )
5 iseven ⊢ ( 𝑍 ∈ Even ↔ ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) )
6 isodd ⊢ ( 𝑍 ∈ Odd ↔ ( 𝑍 ∈ ℤ ∧ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) )
7 5 6 orbi12i ⊢ ( ( 𝑍 ∈ Even ∨ 𝑍 ∈ Odd ) ↔ ( ( 𝑍 ∈ ℤ ∧ ( 𝑍 / 2 ) ∈ ℤ ) ∨ ( 𝑍 ∈ ℤ ∧ ( ( 𝑍 + 1 ) / 2 ) ∈ ℤ ) ) )
8 4 7 sylibr ⊢ ( 𝑍 ∈ ℤ → ( 𝑍 ∈ Even ∨ 𝑍 ∈ Odd ) )