Metamath Proof Explorer

Theorem evennodd

Description: An even number is not an odd number. (Contributed by AV, 16-Jun-2020)

Ref Expression
Assertion evennodd ⊢Z∈Even→¬Z∈Odd

Proof

Step Hyp Ref Expression
1 iseven ⊢Z∈Even↔Z∈ℤ∧Z2∈ℤ
2 zeo2 ⊢Z∈ℤ→Z2∈ℤ↔¬Z+12∈ℤ
3 2 biimpd ⊢Z∈ℤ→Z2∈ℤ→¬Z+12∈ℤ
4 3 imp ⊢Z∈ℤ∧Z2∈ℤ→¬Z+12∈ℤ
5 1 4 sylbi ⊢Z∈Even→¬Z+12∈ℤ
6 5 olcd ⊢Z∈Even→¬Z∈ℤ∨¬Z+12∈ℤ
7 isodd ⊢Z∈Odd↔Z∈ℤ∧Z+12∈ℤ
8 7 notbii ⊢¬Z∈Odd↔¬Z∈ℤ∧Z+12∈ℤ
9 ianor ⊢¬Z∈ℤ∧Z+12∈ℤ↔¬Z∈ℤ∨¬Z+12∈ℤ
10 8 9 bitri ⊢¬Z∈Odd↔¬Z∈ℤ∨¬Z+12∈ℤ
11 6 10 sylibr ⊢Z∈Even→¬Z∈Odd