Metamath Proof Explorer

Theorem oddneven

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

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

Proof

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