Theorem oddneven

Description: An odd number is not an even number. (Contributed by AV, 16-Jun-2020)

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

Proof

Step	Hyp	Ref	Expression
1		isodd	|- ( Z e. Odd <-> ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) )
2		zeo2	|- ( Z e. ZZ -> ( ( Z / 2 ) e. ZZ <-> -. ( ( Z + 1 ) / 2 ) e. ZZ ) )
3	2	biimpd	|- ( Z e. ZZ -> ( ( Z / 2 ) e. ZZ -> -. ( ( Z + 1 ) / 2 ) e. ZZ ) )
4	3	con2d	|- ( Z e. ZZ -> ( ( ( Z + 1 ) / 2 ) e. ZZ -> -. ( Z / 2 ) e. ZZ ) )
5	4	imp	|- ( ( Z e. ZZ /\ ( ( Z + 1 ) / 2 ) e. ZZ ) -> -. ( Z / 2 ) e. ZZ )
6	1 5	sylbi	|- ( Z e. Odd -> -. ( Z / 2 ) e. ZZ )
7	6	olcd	|- ( Z e. Odd -> ( -. Z e. ZZ \/ -. ( Z / 2 ) e. ZZ ) )
8		ianor	|- ( -. ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) <-> ( -. Z e. ZZ \/ -. ( Z / 2 ) e. ZZ ) )
9		iseven	|- ( Z e. Even <-> ( Z e. ZZ /\ ( Z / 2 ) e. ZZ ) )
10	8 9	xchnxbir	|- ( -. Z e. Even <-> ( -. Z e. ZZ \/ -. ( Z / 2 ) e. ZZ ) )
11	7 10	sylibr	|- ( Z e. Odd -> -. Z e. Even )