Theorem odd2np1 11570

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 9082	. . . 4 ⊢ 2 ∈ ℤ
2		divides 11495	. . . 4 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
3	1, 2	mpan 420	. . 3 ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
4	3	notbid 656	. 2 ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
5		elznn0 9069	. . . 4 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
6		odd2np1lem 11569	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
7	6	adantl 275	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
8		odd2np1lem 11569	. . . . . . 7 ⊢ (-𝑁 ∈ ℕ0 → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁))
9		peano2z 9090	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℤ)
10		znegcl 9085	. . . . . . . . . . . . 13 ⊢ ((𝑥 + 1) ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
11	9, 10	syl 14	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
12	11	ad2antlr 480	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → -(𝑥 + 1) ∈ ℤ)
13		zcn 9059	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
14		2cn 8791	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
15		mulcl 7747	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
16	14, 15	mpan 420	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
17		peano2cn 7897	. . . . . . . . . . . . . . . . 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 7794	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℂ)
23		negcon2 8015	. . . . . . . . . . . . . 14 ⊢ ((((2 · 𝑥) + 1) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 · 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1)))
24	20, 22, 23	syl2anc 408	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1)))
25		eqcom 2141	. . . . . . . . . . . . . 14 ⊢ (𝑁 = -((2 · 𝑥) + 1) ↔ -((2 · 𝑥) + 1) = 𝑁)
26	14, 13, 15	sylancr 410	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℤ → (2 · 𝑥) ∈ ℂ)
27		ax-1cn 7713	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
28	14, 27	mulcli 7771	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 · 1) ∈ ℂ
29		addsubass 7972	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2 · 𝑥) ∈ ℂ ∧ (2 · 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
30	28, 27, 29	mp3an23 1307	. . . . . . . . . . . . . . . . . . . . 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 8873	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 · 1) = 2
33	32	oveq1i 5784	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 · 1) − 1) = (2 − 1)
34		2m1e1 8838	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 − 1) = 1
35	33, 34	eqtri 2160	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 · 1) − 1) = 1
36	35	oveq2i 5785	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝑥) + ((2 · 1) − 1)) = ((2 · 𝑥) + 1)
37	31, 36	syl6req 2189	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = (((2 · 𝑥) + (2 · 1)) − 1))
38		adddi 7752	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
39	14, 27, 38	mp3an13 1306	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
40	13, 39	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
41	40	oveq1d 5789	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → ((2 · (𝑥 + 1)) − 1) = (((2 · 𝑥) + (2 · 1)) − 1))
42	37, 41	eqtr4d 2175	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = ((2 · (𝑥 + 1)) − 1))
43	42	negeqd 7957	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = -((2 · (𝑥 + 1)) − 1))
44	9	zcnd 9174	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℂ)
45		mulneg2 8158	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
46	14, 44, 45	sylancr 410	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
47	46	oveq1d 5789	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = (-(2 · (𝑥 + 1)) + 1))
48		mulcl 7747	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · (𝑥 + 1)) ∈ ℂ)
49	14, 44, 48	sylancr 410	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) ∈ ℂ)
50		negsubdi 8018	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2 · (𝑥 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
51	49, 27, 50	sylancl 409	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
52	47, 51	eqtr4d 2175	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = -((2 · (𝑥 + 1)) − 1))
53	43, 52	eqtr4d 2175	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
54	53	adantl 275	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
55	54	eqeq1d 2148	. . . . . . . . . . . . . 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 5782	. . . . . . . . . . . . . 14 ⊢ (𝑛 = -(𝑥 + 1) → (2 · 𝑛) = (2 · -(𝑥 + 1)))
60	59	oveq1d 5789	. . . . . . . . . . . . 13 ⊢ (𝑛 = -(𝑥 + 1) → ((2 · 𝑛) + 1) = ((2 · -(𝑥 + 1)) + 1))
61	60	eqeq1d 2148	. . . . . . . . . . . 12 ⊢ (𝑛 = -(𝑥 + 1) → (((2 · 𝑛) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
62	61	rspcev 2789	. . . . . . . . . . 11 ⊢ ((-(𝑥 + 1) ∈ ℤ ∧ ((2 · -(𝑥 + 1)) + 1) = 𝑁) → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)
63	12, 58, 62	syl2anc 408	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)
64	63	ex 114	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
65	64	rexlimdva 2549	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
66		znegcl 9085	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℤ → -𝑦 ∈ ℤ)
67	66	ad2antlr 480	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → -𝑦 ∈ ℤ)
68		zcn 9059	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
69		mulcl 7747	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑦 · 2) ∈ ℂ)
70	68, 14, 69	sylancl 409	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℤ → (𝑦 · 2) ∈ ℂ)
71		recn 7753	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℝ → 𝑁 ∈ ℂ)
72		negcon2 8015	. . . . . . . . . . . . . 14 ⊢ (((𝑦 · 2) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑦 · 2) = -𝑁 ↔ 𝑁 = -(𝑦 · 2)))
73	70, 71, 72	syl2anr 288	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ 𝑁 = -(𝑦 · 2)))
74		mulneg1 8157	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (-𝑦 · 2) = -(𝑦 · 2))
75	68, 14, 74	sylancl 409	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℤ → (-𝑦 · 2) = -(𝑦 · 2))
76	75	adantl 275	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (-𝑦 · 2) = -(𝑦 · 2))
77	76	eqeq1d 2148	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((-𝑦 · 2) = 𝑁 ↔ -(𝑦 · 2) = 𝑁))
78		eqcom 2141	. . . . . . . . . . . . . 14 ⊢ (𝑁 = -(𝑦 · 2) ↔ -(𝑦 · 2) = 𝑁)
79	77, 78	syl6rbbr 198	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑁 = -(𝑦 · 2) ↔ (-𝑦 · 2) = 𝑁))
80	73, 79	bitrd 187	. . . . . . . . . . . 12 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ (-𝑦 · 2) = 𝑁))
81	80	biimpa 294	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → (-𝑦 · 2) = 𝑁)
82		oveq1 5781	. . . . . . . . . . . . 13 ⊢ (𝑘 = -𝑦 → (𝑘 · 2) = (-𝑦 · 2))
83	82	eqeq1d 2148	. . . . . . . . . . . 12 ⊢ (𝑘 = -𝑦 → ((𝑘 · 2) = 𝑁 ↔ (-𝑦 · 2) = 𝑁))
84	83	rspcev 2789	. . . . . . . . . . 11 ⊢ ((-𝑦 ∈ ℤ ∧ (-𝑦 · 2) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
85	67, 81, 84	syl2anc 408	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
86	85	ex 114	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
87	86	rexlimdva 2549	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
88	65, 87	orim12d 775	. . . . . . 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 786	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
92	5, 91	sylbi 120	. . 3 ⊢ (𝑁 ∈ ℤ → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
93		halfnz 9147	. . . 4 ⊢ ¬ (1 / 2) ∈ ℤ
94		reeanv 2600	. . . . 5 ⊢ (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
95		eqtr3 2159	. . . . . . 7 ⊢ ((((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → ((2 · 𝑛) + 1) = (𝑘 · 2))
96		zcn 9059	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
97		mulcom 7749	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑘 · 2) = (2 · 𝑘))
98	96, 14, 97	sylancl 409	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ → (𝑘 · 2) = (2 · 𝑘))
99	98	eqeq2d 2151	. . . . . . . . 9 ⊢ (𝑘 ∈ ℤ → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
100	99	adantl 275	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
101		mulcl 7747	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
102	14, 96, 101	sylancr 410	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ → (2 · 𝑘) ∈ ℂ)
103		zcn 9059	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
104		mulcl 7747	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
105	14, 103, 104	sylancr 410	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ → (2 · 𝑛) ∈ ℂ)
106		subadd 7965	. . . . . . . . . . 11 ⊢ (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
107	27, 106	mp3an3 1304	. . . . . . . . . 10 ⊢ (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
108	102, 105, 107	syl2anr 288	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
109		subcl 7961	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑘 − 𝑛) ∈ ℂ)
110		2ap0 8813	. . . . . . . . . . . . . . . 16 ⊢ 2 # 0
111	14, 110	pm3.2i 270	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 # 0)
112		eqcom 2141	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 − 𝑛) = (1 / 2) ↔ (1 / 2) = (𝑘 − 𝑛))
113		divmulap 8435	. . . . . . . . . . . . . . . 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 1306	. . . . . . . . . . . . . 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 8147	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
119	14, 118	mp3an1 1302	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
120	119	ancoms 266	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
121	120	eqeq1d 2148	. . . . . . . . . . . 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 9095	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘 − 𝑛) ∈ ℤ)
125		eleq1 2202	. . . . . . . . . . . 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 2555	. . . . 5 ⊢ (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
133	94, 132	sylbir 134	. . . 4 ⊢ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
134	93, 133	mto 651	. . 3 ⊢ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
135		df-xor 1354	. . . . 5 ⊢ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ⊻ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ↔ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
136		xorbin 1362	. . . . 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 409	. 2 ⊢ (𝑁 ∈ ℤ → (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
140	4, 139	bitrd 187	1 ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 697   ∧ w3a 962   = wceq 1331   ⊻ wxo 1353   ∈ wcel 1480  ∃wrex 2417   class class class wbr 3929  (class class class)co 5774  ℂcc 7618  ℝcr 7619  0cc0 7620  1c1 7621   + caddc 7623   · cmul 7625   − cmin 7933  -cneg 7934   # cap 8343   / cdiv 8432  2c2 8771  ℕ₀cn0 8977  ℤcz 9054   ∥ cdvds 11493

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 603  ax-in2 604  ax-io 698  ax-5 1423  ax-7 1424  ax-gen 1425  ax-ie1 1469  ax-ie2 1470  ax-8 1482  ax-10 1483  ax-11 1484  ax-i12 1485  ax-bndl 1486  ax-4 1487  ax-13 1491  ax-14 1492  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-ext 2121  ax-sep 4046  ax-pow 4098  ax-pr 4131  ax-un 4355  ax-setind 4452  ax-cnex 7711  ax-resscn 7712  ax-1cn 7713  ax-1re 7714  ax-icn 7715  ax-addcl 7716  ax-addrcl 7717  ax-mulcl 7718  ax-mulrcl 7719  ax-addcom 7720  ax-mulcom 7721  ax-addass 7722  ax-mulass 7723  ax-distr 7724  ax-i2m1 7725  ax-0lt1 7726  ax-1rid 7727  ax-0id 7728  ax-rnegex 7729  ax-precex 7730  ax-cnre 7731  ax-pre-ltirr 7732  ax-pre-ltwlin 7733  ax-pre-lttrn 7734  ax-pre-apti 7735  ax-pre-ltadd 7736  ax-pre-mulgt0 7737  ax-pre-mulext 7738

This theorem depends on definitions:  df-bi 116  df-3or 963  df-3an 964  df-tru 1334  df-fal 1337  df-xor 1354  df-nf 1437  df-sb 1736  df-eu 2002  df-mo 2003  df-clab 2126  df-cleq 2132  df-clel 2135  df-nfc 2270  df-ne 2309  df-nel 2404  df-ral 2421  df-rex 2422  df-reu 2423  df-rmo 2424  df-rab 2425  df-v 2688  df-sbc 2910  df-dif 3073  df-un 3075  df-in 3077  df-ss 3084  df-pw 3512  df-sn 3533  df-pr 3534  df-op 3536  df-uni 3737  df-int 3772  df-br 3930  df-opab 3990  df-id 4215  df-po 4218  df-iso 4219  df-xp 4545  df-rel 4546  df-cnv 4547  df-co 4548  df-dm 4549  df-iota 5088  df-fun 5125  df-fv 5131  df-riota 5730  df-ov 5777  df-oprab 5778  df-mpo 5779  df-pnf 7802  df-mnf 7803  df-xr 7804  df-ltxr 7805  df-le 7806  df-sub 7935  df-neg 7936  df-reap 8337  df-ap 8344  df-div 8433  df-inn 8721  df-2 8779  df-n0 8978  df-z 9055  df-dvds 11494

This theorem is referenced by:  oddm1even  11572  oexpneg  11574  oddnn02np1  11577  2tp1odd  11581  sqoddm1div8z  11583  ltoddhalfle  11590  halfleoddlt  11591  opoe  11592  omoe  11593  opeo  11594  omeo  11595  m1expo  11597  m1exp1  11598  flodddiv4  11631