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