Metamath Proof Explorer

Theorem evenm1odd

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

Ref Expression
Assertion evenm1odd ⊢ Z ∈ Even → Z − 1 ∈ Odd

Proof

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