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 )