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 + 1 2 ∈ ℤ
2 zeo2 ⊢ Z ∈ ℤ → Z 2 ∈ ℤ ↔ ¬ Z + 1 2 ∈ ℤ
3 2 biimpd ⊢ Z ∈ ℤ → Z 2 ∈ ℤ → ¬ Z + 1 2 ∈ ℤ
4 3 con2d ⊢ Z ∈ ℤ → Z + 1 2 ∈ ℤ → ¬ Z 2 ∈ ℤ
5 4 imp ⊢ Z ∈ ℤ ∧ Z + 1 2 ∈ ℤ → ¬ Z 2 ∈ ℤ
6 1 5 sylbi ⊢ Z ∈ Odd → ¬ Z 2 ∈ ℤ
7 6 olcd ⊢ Z ∈ Odd → ¬ Z ∈ ℤ ∨ ¬ Z 2 ∈ ℤ
8 ianor ⊢ ¬ Z ∈ ℤ ∧ Z 2 ∈ ℤ ↔ ¬ Z ∈ ℤ ∨ ¬ Z 2 ∈ ℤ
9 iseven ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ Z 2 ∈ ℤ
10 8 9 xchnxbir ⊢ ¬ Z ∈ Even ↔ ¬ Z ∈ ℤ ∨ ¬ Z 2 ∈ ℤ
11 7 10 sylibr ⊢ Z ∈ Odd → ¬ Z ∈ Even