Metamath Proof Explorer

Theorem oddm1eveni

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

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

Proof

Step Hyp Ref Expression
1 oddz ⊢ Z ∈ Odd → Z ∈ ℤ
2 peano2zm ⊢ Z ∈ ℤ → Z − 1 ∈ ℤ
3 1 2 syl ⊢ Z ∈ Odd → Z − 1 ∈ ℤ
4 oddm1div2z ⊢ Z ∈ Odd → Z − 1 2 ∈ ℤ
5 iseven ⊢ Z − 1 ∈ Even ↔ Z − 1 ∈ ℤ ∧ Z − 1 2 ∈ ℤ
6 3 4 5 sylanbrc ⊢ Z ∈ Odd → Z − 1 ∈ Even