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 ⊢ Z ∈ ℤ → Z ∈ Even ∨ Z ∈ Odd

Proof

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