This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem evenm1odd

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

Ref Expression
Assertion evenm1odd 
|- ( Z e. Even -> ( Z - 1 ) e. Odd )

Proof

Step Hyp Ref Expression
1 evenz 
 |-  ( Z e. Even -> Z e. ZZ )
2 peano2zm 
 |-  ( Z e. ZZ -> ( Z - 1 ) e. ZZ )
3 1 2 syl 
 |-  ( Z e. Even -> ( Z - 1 ) e. ZZ )
4 iseven 
 |-  ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )
5 zcn 
 |-  ( Z e. ZZ -> Z e. CC )
6 npcan1 
 |-  ( Z e. CC -> ( ( Z - 1 ) + 1 ) = Z )
7 5 6 syl 
 |-  ( Z e. ZZ -> ( ( Z - 1 ) + 1 ) = Z )
8 7 eqcomd 
 |-  ( Z e. ZZ -> Z = ( ( Z - 1 ) + 1 ) )
9 8 oveq1d 
 |-  ( Z e. ZZ -> ( Z / 2 ) = ( ( ( Z - 1 ) + 1 ) / 2 ) )
10 9 eleq1d 
 |-  ( Z e. ZZ -> ( ( Z / 2 ) e. ZZ <-> ( ( ( Z - 1 ) + 1 ) / 2 ) e. ZZ ) )
11 10 biimpa 
 |-  ( ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) -> ( ( ( Z - 1 ) + 1 ) / 2 ) e. ZZ )
12 4 11 sylbi 
 |-  ( Z e. Even -> ( ( ( Z - 1 ) + 1 ) / 2 ) e. ZZ )
13 isodd 
 |-  ( ( Z - 1 ) e. Odd <-> ( ( Z - 1 ) e. ZZ /\ ( ( ( Z - 1 ) + 1 ) / 2 ) e. ZZ ) )
14 3 12 13 sylanbrc 
 |-  ( Z e. Even -> ( Z - 1 ) e. Odd )