Metamath Proof Explorer

Theorem oddp1eveni

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

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

Proof

Step Hyp Ref Expression
1 oddz ⊢ Z ∈ Odd → Z ∈ ℤ
2 1 peano2zd ⊢ Z ∈ Odd → Z + 1 ∈ ℤ
3 oddp1div2z ⊢ Z ∈ Odd → Z + 1 2 ∈ ℤ
4 iseven ⊢ Z + 1 ∈ Even ↔ Z + 1 ∈ ℤ ∧ Z + 1 2 ∈ ℤ
5 2 3 4 sylanbrc ⊢ Z ∈ Odd → Z + 1 ∈ Even