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 )