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∈ℤ→Z2∈ℤ∨Z+12∈ℤ
2 1 ancli ⊢Z∈ℤ→Z∈ℤ∧Z2∈ℤ∨Z+12∈ℤ
3 andi ⊢Z∈ℤ∧Z2∈ℤ∨Z+12∈ℤ↔Z∈ℤ∧Z2∈ℤ∨Z∈ℤ∧Z+12∈ℤ
4 2 3 sylib ⊢Z∈ℤ→Z∈ℤ∧Z2∈ℤ∨Z∈ℤ∧Z+12∈ℤ
5 iseven ⊢Z∈Even↔Z∈ℤ∧Z2∈ℤ
6 isodd ⊢Z∈Odd↔Z∈ℤ∧Z+12∈ℤ
7 5 6 orbi12i ⊢Z∈Even∨Z∈Odd↔Z∈ℤ∧Z2∈ℤ∨Z∈ℤ∧Z+12∈ℤ
8 4 7 sylibr ⊢Z∈ℤ→Z∈Even∨Z∈Odd