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

Proof

Step Hyp Ref Expression
1 oddz 
 |-  ( Z e. Odd -> Z e. ZZ )
2 peano2zm 
 |-  ( Z e. ZZ -> ( Z - 1 ) e. ZZ )
3 1 2 syl 
 |-  ( Z e. Odd -> ( Z - 1 ) e. ZZ )
4 oddm1div2z 
 |-  ( Z e. Odd -> ( ( Z - 1 ) / 2 ) e. ZZ )
5 iseven 
 |-  ( ( Z - 1 ) e. Even <-> ( ( Z - 1 ) e. ZZ /\ ( ( Z - 1 ) / 2 ) e. ZZ ) )
6 3 4 5 sylanbrc 
 |-  ( Z e. Odd -> ( Z - 1 ) e. Even )