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 e. Odd -> ( Z + 1 ) e. Even )

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( Z e. Odd -> Z e. ZZ )
2 1 peano2zd 
 |-  ( Z e. Odd -> ( Z + 1 ) e. ZZ )
3 oddp1div2z 
 |-  ( Z e. Odd -> ( ( Z + 1 ) / 2 ) e. ZZ )
4 iseven 
 |-  ( ( Z + 1 ) e. Even <-> ( ( Z + 1 ) e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) )
5 2 3 4 sylanbrc 
 |-  ( Z e. Odd -> ( Z + 1 ) e. Even )