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