odd2np1

Description: An integer is odd iff it is one plus twice another integer. (Contributed by Scott Fenton, 3-Apr-2014) (Revised by Mario Carneiro, 19-Apr-2014)

		Ref	Expression
	Assertion	odd2np1	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$

Proof

Step	Hyp	Ref	Expression
1		2z	$⊢ 2 \in ℤ$
2		divides	$⊢ (2 \in ℤ \land N \in ℤ) \to (2 ∥ N \leftrightarrow \exists k \in ℤ k \cdot 2 = N)$
3	1 2	mpan	$⊢ N \in ℤ \to (2 ∥ N \leftrightarrow \exists k \in ℤ k \cdot 2 = N)$
4	3	notbid	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \neg \exists k \in ℤ k \cdot 2 = N)$
5		elznn0	$⊢ N \in ℤ \leftrightarrow (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0}))$
6		odd2np1lem	$⊢ N \in ℕ_{0} \to (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N)$
7	6	adantl	$⊢ (N \in ℝ \land N \in ℕ_{0}) \to (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N)$
8		peano2z	$⊢ x \in ℤ \to x + 1 \in ℤ$
9		znegcl	$⊢ x + 1 \in ℤ \to - (x + 1) \in ℤ$
10	8 9	syl	$⊢ x \in ℤ \to - (x + 1) \in ℤ$
11	10	ad2antlr	$⊢ ((N \in ℝ \land x \in ℤ) \land 2 x + 1 = - N) \to - (x + 1) \in ℤ$
12		zcn	$⊢ x \in ℤ \to x \in ℂ$
13		2cn	$⊢ 2 \in ℂ$
14		mulcl	$⊢ (2 \in ℂ \land x \in ℂ) \to 2 x \in ℂ$
15	13 14	mpan	$⊢ x \in ℂ \to 2 x \in ℂ$
16		peano2cn	$⊢ 2 x \in ℂ \to 2 x + 1 \in ℂ$
17	15 16	syl	$⊢ x \in ℂ \to 2 x + 1 \in ℂ$
18	12 17	syl	$⊢ x \in ℤ \to 2 x + 1 \in ℂ$
19	18	adantl	$⊢ (N \in ℝ \land x \in ℤ) \to 2 x + 1 \in ℂ$
20		simpl	$⊢ (N \in ℝ \land x \in ℤ) \to N \in ℝ$
21	20	recnd	$⊢ (N \in ℝ \land x \in ℤ) \to N \in ℂ$
22		negcon2	$⊢ (2 x + 1 \in ℂ \land N \in ℂ) \to (2 x + 1 = - N \leftrightarrow N = - (2 x + 1))$
23	19 21 22	syl2anc	$⊢ (N \in ℝ \land x \in ℤ) \to (2 x + 1 = - N \leftrightarrow N = - (2 x + 1))$
24		eqcom	$⊢ N = - (2 x + 1) \leftrightarrow - (2 x + 1) = N$
25	13 12 14	sylancr	$⊢ x \in ℤ \to 2 x \in ℂ$
26		ax-1cn	$⊢ 1 \in ℂ$
27	13 26	mulcli	$⊢ 2 \cdot 1 \in ℂ$
28		addsubass	$⊢ (2 x \in ℂ \land 2 \cdot 1 \in ℂ \land 1 \in ℂ) \to 2 x + 2 \cdot 1 - 1 = 2 x + 2 \cdot 1 - 1$
29	27 26 28	mp3an23	$⊢ 2 x \in ℂ \to 2 x + 2 \cdot 1 - 1 = 2 x + 2 \cdot 1 - 1$
30	25 29	syl	$⊢ x \in ℤ \to 2 x + 2 \cdot 1 - 1 = 2 x + 2 \cdot 1 - 1$
31		2t1e2	$⊢ 2 \cdot 1 = 2$
32	31	oveq1i	$⊢ 2 \cdot 1 - 1 = 2 - 1$
33		2m1e1	$⊢ 2 - 1 = 1$
34	32 33	eqtri	$⊢ 2 \cdot 1 - 1 = 1$
35	34	oveq2i	$⊢ 2 x + 2 \cdot 1 - 1 = 2 x + 1$
36	30 35	eqtr2di	$⊢ x \in ℤ \to 2 x + 1 = 2 x + 2 \cdot 1 - 1$
37		adddi	$⊢ (2 \in ℂ \land x \in ℂ \land 1 \in ℂ) \to 2 (x + 1) = 2 x + 2 \cdot 1$
38	13 26 37	mp3an13	$⊢ x \in ℂ \to 2 (x + 1) = 2 x + 2 \cdot 1$
39	12 38	syl	$⊢ x \in ℤ \to 2 (x + 1) = 2 x + 2 \cdot 1$
40	39	oveq1d	$⊢ x \in ℤ \to 2 (x + 1) - 1 = 2 x + 2 \cdot 1 - 1$
41	36 40	eqtr4d	$⊢ x \in ℤ \to 2 x + 1 = 2 (x + 1) - 1$
42	41	negeqd	$⊢ x \in ℤ \to - (2 x + 1) = - (2 (x + 1) - 1)$
43	8	zcnd	$⊢ x \in ℤ \to x + 1 \in ℂ$
44		mulneg2	$⊢ (2 \in ℂ \land x + 1 \in ℂ) \to 2 (- (x + 1)) = - 2 (x + 1)$
45	13 43 44	sylancr	$⊢ x \in ℤ \to 2 (- (x + 1)) = - 2 (x + 1)$
46	45	oveq1d	$⊢ x \in ℤ \to 2 (- (x + 1)) + 1 = - 2 (x + 1) + 1$
47		mulcl	$⊢ (2 \in ℂ \land x + 1 \in ℂ) \to 2 (x + 1) \in ℂ$
48	13 43 47	sylancr	$⊢ x \in ℤ \to 2 (x + 1) \in ℂ$
49		negsubdi	$⊢ (2 (x + 1) \in ℂ \land 1 \in ℂ) \to - (2 (x + 1) - 1) = - 2 (x + 1) + 1$
50	48 26 49	sylancl	$⊢ x \in ℤ \to - (2 (x + 1) - 1) = - 2 (x + 1) + 1$
51	46 50	eqtr4d	$⊢ x \in ℤ \to 2 (- (x + 1)) + 1 = - (2 (x + 1) - 1)$
52	42 51	eqtr4d	$⊢ x \in ℤ \to - (2 x + 1) = 2 (- (x + 1)) + 1$
53	52	adantl	$⊢ (N \in ℝ \land x \in ℤ) \to - (2 x + 1) = 2 (- (x + 1)) + 1$
54	53	eqeq1d	$⊢ (N \in ℝ \land x \in ℤ) \to (- (2 x + 1) = N \leftrightarrow 2 (- (x + 1)) + 1 = N)$
55	24 54	syl5bb	$⊢ (N \in ℝ \land x \in ℤ) \to (N = - (2 x + 1) \leftrightarrow 2 (- (x + 1)) + 1 = N)$
56	23 55	bitrd	$⊢ (N \in ℝ \land x \in ℤ) \to (2 x + 1 = - N \leftrightarrow 2 (- (x + 1)) + 1 = N)$
57	56	biimpa	$⊢ ((N \in ℝ \land x \in ℤ) \land 2 x + 1 = - N) \to 2 (- (x + 1)) + 1 = N$
58		oveq2	$⊢ n = - (x + 1) \to 2 n = 2 (- (x + 1))$
59	58	oveq1d	$⊢ n = - (x + 1) \to 2 n + 1 = 2 (- (x + 1)) + 1$
60	59	eqeq1d	$⊢ n = - (x + 1) \to (2 n + 1 = N \leftrightarrow 2 (- (x + 1)) + 1 = N)$
61	60	rspcev	$⊢ (- (x + 1) \in ℤ \land 2 (- (x + 1)) + 1 = N) \to \exists n \in ℤ 2 n + 1 = N$
62	11 57 61	syl2anc	$⊢ ((N \in ℝ \land x \in ℤ) \land 2 x + 1 = - N) \to \exists n \in ℤ 2 n + 1 = N$
63	62	rexlimdva2	$⊢ N \in ℝ \to (\exists x \in ℤ 2 x + 1 = - N \to \exists n \in ℤ 2 n + 1 = N)$
64		znegcl	$⊢ y \in ℤ \to - y \in ℤ$
65	64	ad2antlr	$⊢ ((N \in ℝ \land y \in ℤ) \land y \cdot 2 = - N) \to - y \in ℤ$
66		zcn	$⊢ y \in ℤ \to y \in ℂ$
67		mulcl	$⊢ (y \in ℂ \land 2 \in ℂ) \to y \cdot 2 \in ℂ$
68	66 13 67	sylancl	$⊢ y \in ℤ \to y \cdot 2 \in ℂ$
69		recn	$⊢ N \in ℝ \to N \in ℂ$
70		negcon2	$⊢ (y \cdot 2 \in ℂ \land N \in ℂ) \to (y \cdot 2 = - N \leftrightarrow N = - y \cdot 2)$
71	68 69 70	syl2anr	$⊢ (N \in ℝ \land y \in ℤ) \to (y \cdot 2 = - N \leftrightarrow N = - y \cdot 2)$
72		eqcom	$⊢ N = - y \cdot 2 \leftrightarrow - y \cdot 2 = N$
73		mulneg1	$⊢ (y \in ℂ \land 2 \in ℂ) \to (- y) \cdot 2 = - y \cdot 2$
74	66 13 73	sylancl	$⊢ y \in ℤ \to (- y) \cdot 2 = - y \cdot 2$
75	74	adantl	$⊢ (N \in ℝ \land y \in ℤ) \to (- y) \cdot 2 = - y \cdot 2$
76	75	eqeq1d	$⊢ (N \in ℝ \land y \in ℤ) \to ((- y) \cdot 2 = N \leftrightarrow - y \cdot 2 = N)$
77	72 76	bitr4id	$⊢ (N \in ℝ \land y \in ℤ) \to (N = - y \cdot 2 \leftrightarrow (- y) \cdot 2 = N)$
78	71 77	bitrd	$⊢ (N \in ℝ \land y \in ℤ) \to (y \cdot 2 = - N \leftrightarrow (- y) \cdot 2 = N)$
79	78	biimpa	$⊢ ((N \in ℝ \land y \in ℤ) \land y \cdot 2 = - N) \to (- y) \cdot 2 = N$
80		oveq1	$⊢ k = - y \to k \cdot 2 = (- y) \cdot 2$
81	80	eqeq1d	$⊢ k = - y \to (k \cdot 2 = N \leftrightarrow (- y) \cdot 2 = N)$
82	81	rspcev	$⊢ (- y \in ℤ \land (- y) \cdot 2 = N) \to \exists k \in ℤ k \cdot 2 = N$
83	65 79 82	syl2anc	$⊢ ((N \in ℝ \land y \in ℤ) \land y \cdot 2 = - N) \to \exists k \in ℤ k \cdot 2 = N$
84	83	rexlimdva2	$⊢ N \in ℝ \to (\exists y \in ℤ y \cdot 2 = - N \to \exists k \in ℤ k \cdot 2 = N)$
85	63 84	orim12d	$⊢ N \in ℝ \to ((\exists x \in ℤ 2 x + 1 = - N \lor \exists y \in ℤ y \cdot 2 = - N) \to (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N))$
86		odd2np1lem	$⊢ - N \in ℕ_{0} \to (\exists x \in ℤ 2 x + 1 = - N \lor \exists y \in ℤ y \cdot 2 = - N)$
87	85 86	impel	$⊢ (N \in ℝ \land - N \in ℕ_{0}) \to (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N)$
88	7 87	jaodan	$⊢ (N \in ℝ \land (N \in ℕ_{0} \lor - N \in ℕ_{0})) \to (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N)$
89	5 88	sylbi	$⊢ N \in ℤ \to (\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N)$
90		halfnz	$⊢ \neg \frac{1}{2} \in ℤ$
91		reeanv	$⊢ \exists n \in ℤ \exists k \in ℤ (2 n + 1 = N \land k \cdot 2 = N) \leftrightarrow (\exists n \in ℤ 2 n + 1 = N \land \exists k \in ℤ k \cdot 2 = N)$
92		eqtr3	$⊢ (2 n + 1 = N \land k \cdot 2 = N) \to 2 n + 1 = k \cdot 2$
93		zcn	$⊢ k \in ℤ \to k \in ℂ$
94		mulcom	$⊢ (k \in ℂ \land 2 \in ℂ) \to k \cdot 2 = 2 k$
95	93 13 94	sylancl	$⊢ k \in ℤ \to k \cdot 2 = 2 k$
96	95	eqeq2d	$⊢ k \in ℤ \to (2 n + 1 = k \cdot 2 \leftrightarrow 2 n + 1 = 2 k)$
97	96	adantl	$⊢ (n \in ℤ \land k \in ℤ) \to (2 n + 1 = k \cdot 2 \leftrightarrow 2 n + 1 = 2 k)$
98		mulcl	$⊢ (2 \in ℂ \land k \in ℂ) \to 2 k \in ℂ$
99	13 93 98	sylancr	$⊢ k \in ℤ \to 2 k \in ℂ$
100		zcn	$⊢ n \in ℤ \to n \in ℂ$
101		mulcl	$⊢ (2 \in ℂ \land n \in ℂ) \to 2 n \in ℂ$
102	13 100 101	sylancr	$⊢ n \in ℤ \to 2 n \in ℂ$
103		subadd	$⊢ (2 k \in ℂ \land 2 n \in ℂ \land 1 \in ℂ) \to (2 k - 2 n = 1 \leftrightarrow 2 n + 1 = 2 k)$
104	26 103	mp3an3	$⊢ (2 k \in ℂ \land 2 n \in ℂ) \to (2 k - 2 n = 1 \leftrightarrow 2 n + 1 = 2 k)$
105	99 102 104	syl2anr	$⊢ (n \in ℤ \land k \in ℤ) \to (2 k - 2 n = 1 \leftrightarrow 2 n + 1 = 2 k)$
106		subcl	$⊢ (k \in ℂ \land n \in ℂ) \to k - n \in ℂ$
107		2cnne0	$⊢ (2 \in ℂ \land 2 \neq 0)$
108		eqcom	$⊢ k - n = \frac{1}{2} \leftrightarrow \frac{1}{2} = k - n$
109		divmul	$⊢ (1 \in ℂ \land k - n \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (\frac{1}{2} = k - n \leftrightarrow 2 (k - n) = 1)$
110	108 109	syl5bb	$⊢ (1 \in ℂ \land k - n \in ℂ \land (2 \in ℂ \land 2 \neq 0)) \to (k - n = \frac{1}{2} \leftrightarrow 2 (k - n) = 1)$
111	26 107 110	mp3an13	$⊢ k - n \in ℂ \to (k - n = \frac{1}{2} \leftrightarrow 2 (k - n) = 1)$
112	106 111	syl	$⊢ (k \in ℂ \land n \in ℂ) \to (k - n = \frac{1}{2} \leftrightarrow 2 (k - n) = 1)$
113	112	ancoms	$⊢ (n \in ℂ \land k \in ℂ) \to (k - n = \frac{1}{2} \leftrightarrow 2 (k - n) = 1)$
114		subdi	$⊢ (2 \in ℂ \land k \in ℂ \land n \in ℂ) \to 2 (k - n) = 2 k - 2 n$
115	13 114	mp3an1	$⊢ (k \in ℂ \land n \in ℂ) \to 2 (k - n) = 2 k - 2 n$
116	115	ancoms	$⊢ (n \in ℂ \land k \in ℂ) \to 2 (k - n) = 2 k - 2 n$
117	116	eqeq1d	$⊢ (n \in ℂ \land k \in ℂ) \to (2 (k - n) = 1 \leftrightarrow 2 k - 2 n = 1)$
118	113 117	bitrd	$⊢ (n \in ℂ \land k \in ℂ) \to (k - n = \frac{1}{2} \leftrightarrow 2 k - 2 n = 1)$
119	100 93 118	syl2an	$⊢ (n \in ℤ \land k \in ℤ) \to (k - n = \frac{1}{2} \leftrightarrow 2 k - 2 n = 1)$
120		zsubcl	$⊢ (k \in ℤ \land n \in ℤ) \to k - n \in ℤ$
121		eleq1	$⊢ k - n = \frac{1}{2} \to (k - n \in ℤ \leftrightarrow \frac{1}{2} \in ℤ)$
122	120 121	syl5ibcom	$⊢ (k \in ℤ \land n \in ℤ) \to (k - n = \frac{1}{2} \to \frac{1}{2} \in ℤ)$
123	122	ancoms	$⊢ (n \in ℤ \land k \in ℤ) \to (k - n = \frac{1}{2} \to \frac{1}{2} \in ℤ)$
124	119 123	sylbird	$⊢ (n \in ℤ \land k \in ℤ) \to (2 k - 2 n = 1 \to \frac{1}{2} \in ℤ)$
125	105 124	sylbird	$⊢ (n \in ℤ \land k \in ℤ) \to (2 n + 1 = 2 k \to \frac{1}{2} \in ℤ)$
126	97 125	sylbid	$⊢ (n \in ℤ \land k \in ℤ) \to (2 n + 1 = k \cdot 2 \to \frac{1}{2} \in ℤ)$
127	92 126	syl5	$⊢ (n \in ℤ \land k \in ℤ) \to ((2 n + 1 = N \land k \cdot 2 = N) \to \frac{1}{2} \in ℤ)$
128	127	rexlimivv	$⊢ \exists n \in ℤ \exists k \in ℤ (2 n + 1 = N \land k \cdot 2 = N) \to \frac{1}{2} \in ℤ$
129	91 128	sylbir	$⊢ (\exists n \in ℤ 2 n + 1 = N \land \exists k \in ℤ k \cdot 2 = N) \to \frac{1}{2} \in ℤ$
130	90 129	mto	$⊢ \neg (\exists n \in ℤ 2 n + 1 = N \land \exists k \in ℤ k \cdot 2 = N)$
131		pm5.17	$⊢ ((\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N) \land \neg (\exists n \in ℤ 2 n + 1 = N \land \exists k \in ℤ k \cdot 2 = N)) \leftrightarrow (\exists n \in ℤ 2 n + 1 = N \leftrightarrow \neg \exists k \in ℤ k \cdot 2 = N)$
132		bicom	$⊢ (\exists n \in ℤ 2 n + 1 = N \leftrightarrow \neg \exists k \in ℤ k \cdot 2 = N) \leftrightarrow (\neg \exists k \in ℤ k \cdot 2 = N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
133	131 132	bitri	$⊢ ((\exists n \in ℤ 2 n + 1 = N \lor \exists k \in ℤ k \cdot 2 = N) \land \neg (\exists n \in ℤ 2 n + 1 = N \land \exists k \in ℤ k \cdot 2 = N)) \leftrightarrow (\neg \exists k \in ℤ k \cdot 2 = N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
134	89 130 133	sylanblc	$⊢ N \in ℤ \to (\neg \exists k \in ℤ k \cdot 2 = N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$
135	4 134	bitrd	$⊢ N \in ℤ \to (\neg 2 ∥ N \leftrightarrow \exists n \in ℤ 2 n + 1 = N)$

Metamath Proof Explorer

Theorem odd2np1

Proof