zeo2

Description: An integer is even or odd but not both. (Contributed by Mario Carneiro, 12-Sep-2015)

		Ref	Expression
	Assertion	zeo2	$⊢ N \in ℤ \to (\frac{N}{2} \in ℤ \leftrightarrow \neg \frac{N + 1}{2} \in ℤ)$

Step	Hyp	Ref	Expression
1		zcn	$⊢ N \in ℤ \to N \in ℂ$
2		peano2cn	$⊢ N \in ℂ \to N + 1 \in ℂ$
3	1 2	syl	$⊢ N \in ℤ \to N + 1 \in ℂ$
4		2cnd	$⊢ N \in ℤ \to 2 \in ℂ$
5		2ne0	$⊢ 2 \neq 0$
6	5	a1i	$⊢ N \in ℤ \to 2 \neq 0$
7	3 4 6	divcan2d	$⊢ N \in ℤ \to 2 (\frac{N + 1}{2}) = N + 1$
8	1 4 6	divcan2d	$⊢ N \in ℤ \to 2 (\frac{N}{2}) = N$
9	8	oveq1d	$⊢ N \in ℤ \to 2 (\frac{N}{2}) + 1 = N + 1$
10	7 9	eqtr4d	$⊢ N \in ℤ \to 2 (\frac{N + 1}{2}) = 2 (\frac{N}{2}) + 1$
11		zneo	$⊢ (\frac{N + 1}{2} \in ℤ \land \frac{N}{2} \in ℤ) \to 2 (\frac{N + 1}{2}) \neq 2 (\frac{N}{2}) + 1$
12	11	expcom	$⊢ \frac{N}{2} \in ℤ \to (\frac{N + 1}{2} \in ℤ \to 2 (\frac{N + 1}{2}) \neq 2 (\frac{N}{2}) + 1)$
13	12	necon2bd	$⊢ \frac{N}{2} \in ℤ \to (2 (\frac{N + 1}{2}) = 2 (\frac{N}{2}) + 1 \to \neg \frac{N + 1}{2} \in ℤ)$
14	10 13	syl5com	$⊢ N \in ℤ \to (\frac{N}{2} \in ℤ \to \neg \frac{N + 1}{2} \in ℤ)$
15		zeo	$⊢ N \in ℤ \to (\frac{N}{2} \in ℤ \lor \frac{N + 1}{2} \in ℤ)$
16	15	ord	$⊢ N \in ℤ \to (\neg \frac{N}{2} \in ℤ \to \frac{N + 1}{2} \in ℤ)$
17	16	con1d	$⊢ N \in ℤ \to (\neg \frac{N + 1}{2} \in ℤ \to \frac{N}{2} \in ℤ)$
18	14 17	impbid	$⊢ N \in ℤ \to (\frac{N}{2} \in ℤ \leftrightarrow \neg \frac{N + 1}{2} \in ℤ)$

Metamath Proof Explorer