nneo

Description: A positive integer is even or odd but not both. (Contributed by NM, 1-Jan-2006) (Proof shortened by Mario Carneiro, 18-May-2014)

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

Proof

Step	Hyp	Ref	Expression
1		peano2nn	$⊢ N \in ℕ \to N + 1 \in ℕ$
2	1	nncnd	$⊢ N \in ℕ \to N + 1 \in ℂ$
3		2cn	$⊢ 2 \in ℂ$
4	3	a1i	$⊢ N \in ℕ \to 2 \in ℂ$
5		2ne0	$⊢ 2 \neq 0$
6	5	a1i	$⊢ N \in ℕ \to 2 \neq 0$
7	2 4 6	divcan2d	$⊢ N \in ℕ \to 2 (\frac{N + 1}{2}) = N + 1$
8		nncn	$⊢ N \in ℕ \to N \in ℂ$
9	8 4 6	divcan2d	$⊢ N \in ℕ \to 2 (\frac{N}{2}) = N$
10	9	oveq1d	$⊢ N \in ℕ \to 2 (\frac{N}{2}) + 1 = N + 1$
11	7 10	eqtr4d	$⊢ N \in ℕ \to 2 (\frac{N + 1}{2}) = 2 (\frac{N}{2}) + 1$
12		nnz	$⊢ \frac{N + 1}{2} \in ℕ \to \frac{N + 1}{2} \in ℤ$
13		nnz	$⊢ \frac{N}{2} \in ℕ \to \frac{N}{2} \in ℤ$
14		zneo	$⊢ (\frac{N + 1}{2} \in ℤ \land \frac{N}{2} \in ℤ) \to 2 (\frac{N + 1}{2}) \neq 2 (\frac{N}{2}) + 1$
15	12 13 14	syl2an	$⊢ (\frac{N + 1}{2} \in ℕ \land \frac{N}{2} \in ℕ) \to 2 (\frac{N + 1}{2}) \neq 2 (\frac{N}{2}) + 1$
16	15	expcom	$⊢ \frac{N}{2} \in ℕ \to (\frac{N + 1}{2} \in ℕ \to 2 (\frac{N + 1}{2}) \neq 2 (\frac{N}{2}) + 1)$
17	16	necon2bd	$⊢ \frac{N}{2} \in ℕ \to (2 (\frac{N + 1}{2}) = 2 (\frac{N}{2}) + 1 \to \neg \frac{N + 1}{2} \in ℕ)$
18	11 17	syl5com	$⊢ N \in ℕ \to (\frac{N}{2} \in ℕ \to \neg \frac{N + 1}{2} \in ℕ)$
19		oveq1	$⊢ j = 1 \to j + 1 = 1 + 1$
20	19	oveq1d	$⊢ j = 1 \to \frac{j + 1}{2} = \frac{1 + 1}{2}$
21	20	eleq1d	$⊢ j = 1 \to (\frac{j + 1}{2} \in ℕ \leftrightarrow \frac{1 + 1}{2} \in ℕ)$
22		oveq1	$⊢ j = 1 \to \frac{j}{2} = \frac{1}{2}$
23	22	eleq1d	$⊢ j = 1 \to (\frac{j}{2} \in ℕ \leftrightarrow \frac{1}{2} \in ℕ)$
24	21 23	orbi12d	$⊢ j = 1 \to ((\frac{j + 1}{2} \in ℕ \lor \frac{j}{2} \in ℕ) \leftrightarrow (\frac{1 + 1}{2} \in ℕ \lor \frac{1}{2} \in ℕ))$
25		oveq1	$⊢ j = k \to j + 1 = k + 1$
26	25	oveq1d	$⊢ j = k \to \frac{j + 1}{2} = \frac{k + 1}{2}$
27	26	eleq1d	$⊢ j = k \to (\frac{j + 1}{2} \in ℕ \leftrightarrow \frac{k + 1}{2} \in ℕ)$
28		oveq1	$⊢ j = k \to \frac{j}{2} = \frac{k}{2}$
29	28	eleq1d	$⊢ j = k \to (\frac{j}{2} \in ℕ \leftrightarrow \frac{k}{2} \in ℕ)$
30	27 29	orbi12d	$⊢ j = k \to ((\frac{j + 1}{2} \in ℕ \lor \frac{j}{2} \in ℕ) \leftrightarrow (\frac{k + 1}{2} \in ℕ \lor \frac{k}{2} \in ℕ))$
31		oveq1	$⊢ j = k + 1 \to j + 1 = k + 1 + 1$
32	31	oveq1d	$⊢ j = k + 1 \to \frac{j + 1}{2} = \frac{k + 1 + 1}{2}$
33	32	eleq1d	$⊢ j = k + 1 \to (\frac{j + 1}{2} \in ℕ \leftrightarrow \frac{k + 1 + 1}{2} \in ℕ)$
34		oveq1	$⊢ j = k + 1 \to \frac{j}{2} = \frac{k + 1}{2}$
35	34	eleq1d	$⊢ j = k + 1 \to (\frac{j}{2} \in ℕ \leftrightarrow \frac{k + 1}{2} \in ℕ)$
36	33 35	orbi12d	$⊢ j = k + 1 \to ((\frac{j + 1}{2} \in ℕ \lor \frac{j}{2} \in ℕ) \leftrightarrow (\frac{k + 1 + 1}{2} \in ℕ \lor \frac{k + 1}{2} \in ℕ))$
37		oveq1	$⊢ j = N \to j + 1 = N + 1$
38	37	oveq1d	$⊢ j = N \to \frac{j + 1}{2} = \frac{N + 1}{2}$
39	38	eleq1d	$⊢ j = N \to (\frac{j + 1}{2} \in ℕ \leftrightarrow \frac{N + 1}{2} \in ℕ)$
40		oveq1	$⊢ j = N \to \frac{j}{2} = \frac{N}{2}$
41	40	eleq1d	$⊢ j = N \to (\frac{j}{2} \in ℕ \leftrightarrow \frac{N}{2} \in ℕ)$
42	39 41	orbi12d	$⊢ j = N \to ((\frac{j + 1}{2} \in ℕ \lor \frac{j}{2} \in ℕ) \leftrightarrow (\frac{N + 1}{2} \in ℕ \lor \frac{N}{2} \in ℕ))$
43		df-2	$⊢ 2 = 1 + 1$
44	43	oveq1i	$⊢ \frac{2}{2} = \frac{1 + 1}{2}$
45		2div2e1	$⊢ \frac{2}{2} = 1$
46	44 45	eqtr3i	$⊢ \frac{1 + 1}{2} = 1$
47		1nn	$⊢ 1 \in ℕ$
48	46 47	eqeltri	$⊢ \frac{1 + 1}{2} \in ℕ$
49	48	orci	$⊢ (\frac{1 + 1}{2} \in ℕ \lor \frac{1}{2} \in ℕ)$
50		peano2nn	$⊢ \frac{k}{2} \in ℕ \to (\frac{k}{2}) + 1 \in ℕ$
51		nncn	$⊢ k \in ℕ \to k \in ℂ$
52		add1p1	$⊢ k \in ℂ \to k + 1 + 1 = k + 2$
53	52	oveq1d	$⊢ k \in ℂ \to \frac{k + 1 + 1}{2} = \frac{k + 2}{2}$
54		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
55		divdir	$⊢ (k \in ℂ \land 2 \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to \frac{k + 2}{2} = (\frac{k}{2}) + (\frac{2}{2})$
56	3 54 55	mp3an23	$⊢ k \in ℂ \to \frac{k + 2}{2} = (\frac{k}{2}) + (\frac{2}{2})$
57	45	oveq2i	$⊢ (\frac{k}{2}) + (\frac{2}{2}) = (\frac{k}{2}) + 1$
58	56 57	eqtrdi	$⊢ k \in ℂ \to \frac{k + 2}{2} = (\frac{k}{2}) + 1$
59	53 58	eqtrd	$⊢ k \in ℂ \to \frac{k + 1 + 1}{2} = (\frac{k}{2}) + 1$
60	51 59	syl	$⊢ k \in ℕ \to \frac{k + 1 + 1}{2} = (\frac{k}{2}) + 1$
61	60	eleq1d	$⊢ k \in ℕ \to (\frac{k + 1 + 1}{2} \in ℕ \leftrightarrow (\frac{k}{2}) + 1 \in ℕ)$
62	50 61	imbitrrid	$⊢ k \in ℕ \to (\frac{k}{2} \in ℕ \to \frac{k + 1 + 1}{2} \in ℕ)$
63	62	orim2d	$⊢ k \in ℕ \to ((\frac{k + 1}{2} \in ℕ \lor \frac{k}{2} \in ℕ) \to (\frac{k + 1}{2} \in ℕ \lor \frac{k + 1 + 1}{2} \in ℕ))$
64		orcom	$⊢ (\frac{k + 1}{2} \in ℕ \lor \frac{k + 1 + 1}{2} \in ℕ) \leftrightarrow (\frac{k + 1 + 1}{2} \in ℕ \lor \frac{k + 1}{2} \in ℕ)$
65	63 64	imbitrdi	$⊢ k \in ℕ \to ((\frac{k + 1}{2} \in ℕ \lor \frac{k}{2} \in ℕ) \to (\frac{k + 1 + 1}{2} \in ℕ \lor \frac{k + 1}{2} \in ℕ))$
66	24 30 36 42 49 65	nnind	$⊢ N \in ℕ \to (\frac{N + 1}{2} \in ℕ \lor \frac{N}{2} \in ℕ)$
67	66	ord	$⊢ N \in ℕ \to (\neg \frac{N + 1}{2} \in ℕ \to \frac{N}{2} \in ℕ)$
68	18 67	impbid	$⊢ N \in ℕ \to (\frac{N}{2} \in ℕ \leftrightarrow \neg \frac{N + 1}{2} \in ℕ)$

Metamath Proof Explorer

Theorem nneo

Proof