Metamath Proof Explorer

Theorem evenp1odd

Description: The successor of an even number is odd. (Contributed by AV, 16-Jun-2020)

Ref Expression
Assertion evenp1odd ⊢ Z ∈ Even → Z + 1 ∈ Odd

Proof

Step Hyp Ref Expression
1 evenz ⊢ Z ∈ Even → Z ∈ ℤ
2 1 peano2zd ⊢ Z ∈ Even → Z + 1 ∈ ℤ
3 iseven ⊢ Z ∈ Even ↔ Z ∈ ℤ ∧ Z 2 ∈ ℤ
4 zcn ⊢ Z ∈ ℤ → Z ∈ ℂ
5 pncan1 ⊢ Z ∈ ℂ → Z + 1 - 1 = Z
6 4 5 syl ⊢ Z ∈ ℤ → Z + 1 - 1 = Z
7 6 eqcomd ⊢ Z ∈ ℤ → Z = Z + 1 - 1
8 7 oveq1d ⊢ Z ∈ ℤ → Z 2 = Z + 1 - 1 2
9 8 eleq1d ⊢ Z ∈ ℤ → Z 2 ∈ ℤ ↔ Z + 1 - 1 2 ∈ ℤ
10 9 biimpa ⊢ Z ∈ ℤ ∧ Z 2 ∈ ℤ → Z + 1 - 1 2 ∈ ℤ
11 3 10 sylbi ⊢ Z ∈ Even → Z + 1 - 1 2 ∈ ℤ
12 isodd2 ⊢ Z + 1 ∈ Odd ↔ Z + 1 ∈ ℤ ∧ Z + 1 - 1 2 ∈ ℤ
13 2 11 12 sylanbrc ⊢ Z ∈ Even → Z + 1 ∈ Odd