Theorem 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	⊢ ( 𝑁 ∈ ℤ → ( ¬ 2 ∥ 𝑁 ↔ ∃ 𝑛 ∈ ℤ ( ( 2 · 𝑛 ) + 1 ) = 𝑁 ) )

Proof

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