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

Metamath Proof Explorer

Theorem evenp1odd

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

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

Proof

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