Theorem odd2np1 11832

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.)

Assertion

Ref	Expression
odd2np1	⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))

Distinct variable group:   𝑛,𝑁

Proof of Theorem odd2np1

Dummy variables 𝑘 𝑥 𝑦 are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		2z 9240	. . . 4 ⊢ 2 ∈ ℤ
2		divides 11751	. . . 4 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
3	1, 2	mpan 422	. . 3 ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
4	3	notbid 662	. 2 ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
5		elznn0 9227	. . . 4 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
6		odd2np1lem 11831	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
7	6	adantl 275	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
8		odd2np1lem 11831	. . . . . . 7 ⊢ (-𝑁 ∈ ℕ0 → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁))
9		peano2z 9248	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℤ)
10		znegcl 9243	. . . . . . . . . . . . 13 ⊢ ((𝑥 + 1) ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
11	9, 10	syl 14	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
12	11	ad2antlr 486	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → -(𝑥 + 1) ∈ ℤ)
13		zcn 9217	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
14		2cn 8949	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
15		mulcl 7901	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
16	14, 15	mpan 422	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
17		peano2cn 8054	. . . . . . . . . . . . . . . . 17 ⊢ ((2 · 𝑥) ∈ ℂ → ((2 · 𝑥) + 1) ∈ ℂ)
18	16, 17	syl 14	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℂ → ((2 · 𝑥) + 1) ∈ ℂ)
19	13, 18	syl 14	. . . . . . . . . . . . . . 15 ⊢ (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) ∈ ℂ)
20	19	adantl 275	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((2 · 𝑥) + 1) ∈ ℂ)
21		simpl 108	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℝ)
22	21	recnd 7948	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℂ)
23		negcon2 8172	. . . . . . . . . . . . . 14 ⊢ ((((2 · 𝑥) + 1) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 · 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1)))
24	20, 22, 23	syl2anc 409	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1)))
25		eqcom 2172	. . . . . . . . . . . . . 14 ⊢ (𝑁 = -((2 · 𝑥) + 1) ↔ -((2 · 𝑥) + 1) = 𝑁)
26	14, 13, 15	sylancr 412	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℤ → (2 · 𝑥) ∈ ℂ)
27		ax-1cn 7867	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
28	14, 27	mulcli 7925	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 · 1) ∈ ℂ
29		addsubass 8129	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2 · 𝑥) ∈ ℂ ∧ (2 · 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
30	28, 27, 29	mp3an23 1324	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 · 𝑥) ∈ ℂ → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
31	26, 30	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
32		2t1e2 9031	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 · 1) = 2
33	32	oveq1i 5863	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 · 1) − 1) = (2 − 1)
34		2m1e1 8996	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 − 1) = 1
35	33, 34	eqtri 2191	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 · 1) − 1) = 1
36	35	oveq2i 5864	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝑥) + ((2 · 1) − 1)) = ((2 · 𝑥) + 1)
37	31, 36	eqtr2di 2220	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = (((2 · 𝑥) + (2 · 1)) − 1))
38		adddi 7906	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
39	14, 27, 38	mp3an13 1323	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
40	13, 39	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
41	40	oveq1d 5868	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → ((2 · (𝑥 + 1)) − 1) = (((2 · 𝑥) + (2 · 1)) − 1))
42	37, 41	eqtr4d 2206	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = ((2 · (𝑥 + 1)) − 1))
43	42	negeqd 8114	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = -((2 · (𝑥 + 1)) − 1))
44	9	zcnd 9335	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℂ)
45		mulneg2 8315	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
46	14, 44, 45	sylancr 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
47	46	oveq1d 5868	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = (-(2 · (𝑥 + 1)) + 1))
48		mulcl 7901	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · (𝑥 + 1)) ∈ ℂ)
49	14, 44, 48	sylancr 412	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) ∈ ℂ)
50		negsubdi 8175	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2 · (𝑥 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
51	49, 27, 50	sylancl 411	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
52	47, 51	eqtr4d 2206	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = -((2 · (𝑥 + 1)) − 1))
53	43, 52	eqtr4d 2206	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
54	53	adantl 275	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
55	54	eqeq1d 2179	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-((2 · 𝑥) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
56	25, 55	syl5bb 191	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑁 = -((2 · 𝑥) + 1) ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
57	24, 56	bitrd 187	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
58	57	biimpa 294	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → ((2 · -(𝑥 + 1)) + 1) = 𝑁)
59		oveq2 5861	. . . . . . . . . . . . . 14 ⊢ (𝑛 = -(𝑥 + 1) → (2 · 𝑛) = (2 · -(𝑥 + 1)))
60	59	oveq1d 5868	. . . . . . . . . . . . 13 ⊢ (𝑛 = -(𝑥 + 1) → ((2 · 𝑛) + 1) = ((2 · -(𝑥 + 1)) + 1))
61	60	eqeq1d 2179	. . . . . . . . . . . 12 ⊢ (𝑛 = -(𝑥 + 1) → (((2 · 𝑛) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
62	61	rspcev 2834	. . . . . . . . . . 11 ⊢ ((-(𝑥 + 1) ∈ ℤ ∧ ((2 · -(𝑥 + 1)) + 1) = 𝑁) → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)
63	12, 58, 62	syl2anc 409	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)
64	63	ex 114	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
65	64	rexlimdva 2587	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
66		znegcl 9243	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℤ → -𝑦 ∈ ℤ)
67	66	ad2antlr 486	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → -𝑦 ∈ ℤ)
68		zcn 9217	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
69		mulcl 7901	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑦 · 2) ∈ ℂ)
70	68, 14, 69	sylancl 411	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℤ → (𝑦 · 2) ∈ ℂ)
71		recn 7907	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℝ → 𝑁 ∈ ℂ)
72		negcon2 8172	. . . . . . . . . . . . . 14 ⊢ (((𝑦 · 2) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑦 · 2) = -𝑁 ↔ 𝑁 = -(𝑦 · 2)))
73	70, 71, 72	syl2anr 288	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ 𝑁 = -(𝑦 · 2)))
74		eqcom 2172	. . . . . . . . . . . . . 14 ⊢ (𝑁 = -(𝑦 · 2) ↔ -(𝑦 · 2) = 𝑁)
75		mulneg1 8314	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (-𝑦 · 2) = -(𝑦 · 2))
76	68, 14, 75	sylancl 411	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℤ → (-𝑦 · 2) = -(𝑦 · 2))
77	76	adantl 275	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (-𝑦 · 2) = -(𝑦 · 2))
78	77	eqeq1d 2179	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((-𝑦 · 2) = 𝑁 ↔ -(𝑦 · 2) = 𝑁))
79	74, 78	bitr4id 198	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑁 = -(𝑦 · 2) ↔ (-𝑦 · 2) = 𝑁))
80	73, 79	bitrd 187	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ (-𝑦 · 2) = 𝑁))
81	80	biimpa 294	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → (-𝑦 · 2) = 𝑁)
82		oveq1 5860	. . . . . . . . . . . . 13 ⊢ (𝑘 = -𝑦 → (𝑘 · 2) = (-𝑦 · 2))
83	82	eqeq1d 2179	. . . . . . . . . . . 12 ⊢ (𝑘 = -𝑦 → ((𝑘 · 2) = 𝑁 ↔ (-𝑦 · 2) = 𝑁))
84	83	rspcev 2834	. . . . . . . . . . 11 ⊢ ((-𝑦 ∈ ℤ ∧ (-𝑦 · 2) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
85	67, 81, 84	syl2anc 409	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
86	85	ex 114	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
87	86	rexlimdva 2587	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
88	65, 87	orim12d 781	. . . . . . 7 ⊢ (𝑁 ∈ ℝ → ((∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
89	8, 88	syl5 32	. . . . . 6 ⊢ (𝑁 ∈ ℝ → (-𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
90	89	imp 123	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
91	7, 90	jaodan 792	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
92	5, 91	sylbi 120	. . 3 ⊢ (𝑁 ∈ ℤ → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
93		halfnz 9308	. . . 4 ⊢ ¬ (1 / 2) ∈ ℤ
94		reeanv 2639	. . . . 5 ⊢ (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
95		eqtr3 2190	. . . . . . 7 ⊢ ((((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → ((2 · 𝑛) + 1) = (𝑘 · 2))
96		zcn 9217	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
97		mulcom 7903	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑘 · 2) = (2 · 𝑘))
98	96, 14, 97	sylancl 411	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ → (𝑘 · 2) = (2 · 𝑘))
99	98	eqeq2d 2182	. . . . . . . . 9 ⊢ (𝑘 ∈ ℤ → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
100	99	adantl 275	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
101		mulcl 7901	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
102	14, 96, 101	sylancr 412	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ → (2 · 𝑘) ∈ ℂ)
103		zcn 9217	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
104		mulcl 7901	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
105	14, 103, 104	sylancr 412	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ → (2 · 𝑛) ∈ ℂ)
106		subadd 8122	. . . . . . . . . . 11 ⊢ (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
107	27, 106	mp3an3 1321	. . . . . . . . . 10 ⊢ (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
108	102, 105, 107	syl2anr 288	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
109		subcl 8118	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑘 − 𝑛) ∈ ℂ)
110		2ap0 8971	. . . . . . . . . . . . . . . 16 ⊢ 2 # 0
111	14, 110	pm3.2i 270	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 # 0)
112		eqcom 2172	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 − 𝑛) = (1 / 2) ↔ (1 / 2) = (𝑘 − 𝑛))
113		divmulap 8592	. . . . . . . . . . . . . . . 16 ⊢ ((1 ∈ ℂ ∧ (𝑘 − 𝑛) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((1 / 2) = (𝑘 − 𝑛) ↔ (2 · (𝑘 − 𝑛)) = 1))
114	112, 113	syl5bb 191	. . . . . . . . . . . . . . 15 ⊢ ((1 ∈ ℂ ∧ (𝑘 − 𝑛) ∈ ℂ ∧ (2 ∈ ℂ ∧ 2 # 0)) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1))
115	27, 111, 114	mp3an13 1323	. . . . . . . . . . . . . 14 ⊢ ((𝑘 − 𝑛) ∈ ℂ → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1))
116	109, 115	syl 14	. . . . . . . . . . . . 13 ⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1))
117	116	ancoms 266	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1))
118		subdi 8304	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
119	14, 118	mp3an1 1319	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
120	119	ancoms 266	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
121	120	eqeq1d 2179	. . . . . . . . . . . 12 ⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((2 · (𝑘 − 𝑛)) = 1 ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
122	117, 121	bitrd 187	. . . . . . . . . . 11 ⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
123	103, 96, 122	syl2an 287	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1))
124		zsubcl 9253	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘 − 𝑛) ∈ ℤ)
125		eleq1 2233	. . . . . . . . . . . 12 ⊢ ((𝑘 − 𝑛) = (1 / 2) → ((𝑘 − 𝑛) ∈ ℤ ↔ (1 / 2) ∈ ℤ))
126	124, 125	syl5ibcom 154	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) → (1 / 2) ∈ ℤ))
127	126	ancoms 266	. . . . . . . . . 10 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) → (1 / 2) ∈ ℤ))
128	123, 127	sylbird 169	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 → (1 / 2) ∈ ℤ))
129	108, 128	sylbird 169	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (2 · 𝑘) → (1 / 2) ∈ ℤ))
130	100, 129	sylbid 149	. . . . . . 7 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (𝑘 · 2) → (1 / 2) ∈ ℤ))
131	95, 130	syl5 32	. . . . . 6 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ))
132	131	rexlimivv 2593	. . . . 5 ⊢ (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
133	94, 132	sylbir 134	. . . 4 ⊢ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
134	93, 133	mto 657	. . 3 ⊢ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
135		df-xor 1371	. . . . 5 ⊢ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ⊻ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ↔ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
136		xorbin 1379	. . . . 5 ⊢ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ⊻ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
137	135, 136	sylbir 134	. . . 4 ⊢ (((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
138	137	bicomd 140	. . 3 ⊢ (((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) → (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
139	92, 134, 138	sylancl 411	. 2 ⊢ (𝑁 ∈ ℤ → (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
140	4, 139	bitrd 187	1 ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 703   ∧ w3a 973   = wceq 1348   ⊻ wxo 1370   ∈ wcel 2141  ∃wrex 2449   class class class wbr 3989  (class class class)co 5853  ℂcc 7772  ℝcr 7773  0cc0 7774  1c1 7775   + caddc 7777   · cmul 7779   − cmin 8090  -cneg 8091   # cap 8500   / cdiv 8589  2c2 8929  ℕ₀cn0 9135  ℤcz 9212   ∥ cdvds 11749

This theorem was proved from axioms:  ax-mp 5  ax-1 6  ax-2 7  ax-ia1 105  ax-ia2 106  ax-ia3 107  ax-in1 609  ax-in2 610  ax-io 704  ax-5 1440  ax-7 1441  ax-gen 1442  ax-ie1 1486  ax-ie2 1487  ax-8 1497  ax-10 1498  ax-11 1499  ax-i12 1500  ax-bndl 1502  ax-4 1503  ax-17 1519  ax-i9 1523  ax-ial 1527  ax-i5r 1528  ax-13 2143  ax-14 2144  ax-ext 2152  ax-sep 4107  ax-pow 4160  ax-pr 4194  ax-un 4418  ax-setind 4521  ax-cnex 7865  ax-resscn 7866  ax-1cn 7867  ax-1re 7868  ax-icn 7869  ax-addcl 7870  ax-addrcl 7871  ax-mulcl 7872  ax-mulrcl 7873  ax-addcom 7874  ax-mulcom 7875  ax-addass 7876  ax-mulass 7877  ax-distr 7878  ax-i2m1 7879  ax-0lt1 7880  ax-1rid 7881  ax-0id 7882  ax-rnegex 7883  ax-precex 7884  ax-cnre 7885  ax-pre-ltirr 7886  ax-pre-ltwlin 7887  ax-pre-lttrn 7888  ax-pre-apti 7889  ax-pre-ltadd 7890  ax-pre-mulgt0 7891  ax-pre-mulext 7892

This theorem depends on definitions:  df-bi 116  df-3or 974  df-3an 975  df-tru 1351  df-fal 1354  df-xor 1371  df-nf 1454  df-sb 1756  df-eu 2022  df-mo 2023  df-clab 2157  df-cleq 2163  df-clel 2166  df-nfc 2301  df-ne 2341  df-nel 2436  df-ral 2453  df-rex 2454  df-reu 2455  df-rmo 2456  df-rab 2457  df-v 2732  df-sbc 2956  df-dif 3123  df-un 3125  df-in 3127  df-ss 3134  df-pw 3568  df-sn 3589  df-pr 3590  df-op 3592  df-uni 3797  df-int 3832  df-br 3990  df-opab 4051  df-id 4278  df-po 4281  df-iso 4282  df-xp 4617  df-rel 4618  df-cnv 4619  df-co 4620  df-dm 4621  df-iota 5160  df-fun 5200  df-fv 5206  df-riota 5809  df-ov 5856  df-oprab 5857  df-mpo 5858  df-pnf 7956  df-mnf 7957  df-xr 7958  df-ltxr 7959  df-le 7960  df-sub 8092  df-neg 8093  df-reap 8494  df-ap 8501  df-div 8590  df-inn 8879  df-2 8937  df-n0 9136  df-z 9213  df-dvds 11750

This theorem is referenced by:  oddm1even  11834  oexpneg  11836  oddnn02np1  11839  2tp1odd  11843  sqoddm1div8z  11845  ltoddhalfle  11852  halfleoddlt  11853  opoe  11854  omoe  11855  opeo  11856  omeo  11857  m1expo  11859  m1exp1  11860  flodddiv4  11893