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 )