Theorem odd2np1 11758

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 9190	. . . 4 ⊢ 2 ∈ ℤ
2		divides 11680	. . . 4 ⊢ ((2 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
3	1, 2	mpan 421	. . 3 ⊢ (𝑁 ∈ ℤ → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
4	3	notbid 657	. 2 ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
5		elznn0 9177	. . . 4 ⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)))
6		odd2np1lem 11757	. . . . . 6 ⊢ (𝑁 ∈ ℕ0 → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
7	6	adantl 275	. . . . 5 ⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
8		odd2np1lem 11757	. . . . . . 7 ⊢ (-𝑁 ∈ ℕ0 → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁))
9		peano2z 9198	. . . . . . . . . . . . 13 ⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℤ)
10		znegcl 9193	. . . . . . . . . . . . 13 ⊢ ((𝑥 + 1) ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
11	9, 10	syl 14	. . . . . . . . . . . 12 ⊢ (𝑥 ∈ ℤ → -(𝑥 + 1) ∈ ℤ)
12	11	ad2antlr 481	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2 · 𝑥) + 1) = -𝑁) → -(𝑥 + 1) ∈ ℤ)
13		zcn 9167	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ → 𝑥 ∈ ℂ)
14		2cn 8899	. . . . . . . . . . . . . . . . . 18 ⊢ 2 ∈ ℂ
15		mulcl 7854	. . . . . . . . . . . . . . . . . 18 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ) → (2 · 𝑥) ∈ ℂ)
16	14, 15	mpan 421	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℂ → (2 · 𝑥) ∈ ℂ)
17		peano2cn 8005	. . . . . . . . . . . . . . . . 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 7901	. . . . . . . . . . . . . 14 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈ ℂ)
23		negcon2 8123	. . . . . . . . . . . . . 14 ⊢ ((((2 · 𝑥) + 1) ∈ ℂ ∧ 𝑁 ∈ ℂ) → (((2 · 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1)))
24	20, 22, 23	syl2anc 409	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2 · 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1)))
25		eqcom 2159	. . . . . . . . . . . . . 14 ⊢ (𝑁 = -((2 · 𝑥) + 1) ↔ -((2 · 𝑥) + 1) = 𝑁)
26	14, 13, 15	sylancr 411	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℤ → (2 · 𝑥) ∈ ℂ)
27		ax-1cn 7820	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ 1 ∈ ℂ
28	14, 27	mulcli 7878	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 · 1) ∈ ℂ
29		addsubass 8080	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (((2 · 𝑥) ∈ ℂ ∧ (2 · 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑥) + (2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) − 1)))
30	28, 27, 29	mp3an23 1311	. . . . . . . . . . . . . . . . . . . . 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 8981	. . . . . . . . . . . . . . . . . . . . . . 23 ⊢ (2 · 1) = 2
33	32	oveq1i 5831	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 · 1) − 1) = (2 − 1)
34		2m1e1 8946	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ (2 − 1) = 1
35	33, 34	eqtri 2178	. . . . . . . . . . . . . . . . . . . . 21 ⊢ ((2 · 1) − 1) = 1
36	35	oveq2i 5832	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 · 𝑥) + ((2 · 1) − 1)) = ((2 · 𝑥) + 1)
37	31, 36	eqtr2di 2207	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = (((2 · 𝑥) + (2 · 1)) − 1))
38		adddi 7859	. . . . . . . . . . . . . . . . . . . . . 22 ⊢ ((2 ∈ ℂ ∧ 𝑥 ∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
39	14, 27, 38	mp3an13 1310	. . . . . . . . . . . . . . . . . . . . 21 ⊢ (𝑥 ∈ ℂ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
40	13, 39	syl 14	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1)))
41	40	oveq1d 5836	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → ((2 · (𝑥 + 1)) − 1) = (((2 · 𝑥) + (2 · 1)) − 1))
42	37, 41	eqtr4d 2193	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → ((2 · 𝑥) + 1) = ((2 · (𝑥 + 1)) − 1))
43	42	negeqd 8065	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = -((2 · (𝑥 + 1)) − 1))
44	9	zcnd 9282	. . . . . . . . . . . . . . . . . . . 20 ⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈ ℂ)
45		mulneg2 8266	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
46	14, 44, 45	sylancr 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1)))
47	46	oveq1d 5836	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = (-(2 · (𝑥 + 1)) + 1))
48		mulcl 7854	. . . . . . . . . . . . . . . . . . . 20 ⊢ ((2 ∈ ℂ ∧ (𝑥 + 1) ∈ ℂ) → (2 · (𝑥 + 1)) ∈ ℂ)
49	14, 44, 48	sylancr 411	. . . . . . . . . . . . . . . . . . 19 ⊢ (𝑥 ∈ ℤ → (2 · (𝑥 + 1)) ∈ ℂ)
50		negsubdi 8126	. . . . . . . . . . . . . . . . . . 19 ⊢ (((2 · (𝑥 + 1)) ∈ ℂ ∧ 1 ∈ ℂ) → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
51	49, 27, 50	sylancl 410	. . . . . . . . . . . . . . . . . 18 ⊢ (𝑥 ∈ ℤ → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1))
52	47, 51	eqtr4d 2193	. . . . . . . . . . . . . . . . 17 ⊢ (𝑥 ∈ ℤ → ((2 · -(𝑥 + 1)) + 1) = -((2 · (𝑥 + 1)) − 1))
53	43, 52	eqtr4d 2193	. . . . . . . . . . . . . . . 16 ⊢ (𝑥 ∈ ℤ → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
54	53	adantl 275	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → -((2 · 𝑥) + 1) = ((2 · -(𝑥 + 1)) + 1))
55	54	eqeq1d 2166	. . . . . . . . . . . . . 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 5829	. . . . . . . . . . . . . 14 ⊢ (𝑛 = -(𝑥 + 1) → (2 · 𝑛) = (2 · -(𝑥 + 1)))
60	59	oveq1d 5836	. . . . . . . . . . . . 13 ⊢ (𝑛 = -(𝑥 + 1) → ((2 · 𝑛) + 1) = ((2 · -(𝑥 + 1)) + 1))
61	60	eqeq1d 2166	. . . . . . . . . . . 12 ⊢ (𝑛 = -(𝑥 + 1) → (((2 · 𝑛) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁))
62	61	rspcev 2816	. . . . . . . . . . 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 2574	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (∃𝑥 ∈ ℤ ((2 · 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
66		znegcl 9193	. . . . . . . . . . . 12 ⊢ (𝑦 ∈ ℤ → -𝑦 ∈ ℤ)
67	66	ad2antlr 481	. . . . . . . . . . 11 ⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → -𝑦 ∈ ℤ)
68		zcn 9167	. . . . . . . . . . . . . . 15 ⊢ (𝑦 ∈ ℤ → 𝑦 ∈ ℂ)
69		mulcl 7854	. . . . . . . . . . . . . . 15 ⊢ ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑦 · 2) ∈ ℂ)
70	68, 14, 69	sylancl 410	. . . . . . . . . . . . . 14 ⊢ (𝑦 ∈ ℤ → (𝑦 · 2) ∈ ℂ)
71		recn 7860	. . . . . . . . . . . . . 14 ⊢ (𝑁 ∈ ℝ → 𝑁 ∈ ℂ)
72		negcon2 8123	. . . . . . . . . . . . . 14 ⊢ (((𝑦 · 2) ∈ ℂ ∧ 𝑁 ∈ ℂ) → ((𝑦 · 2) = -𝑁 ↔ 𝑁 = -(𝑦 · 2)))
73	70, 71, 72	syl2anr 288	. . . . . . . . . . . . 13 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ 𝑁 = -(𝑦 · 2)))
74		eqcom 2159	. . . . . . . . . . . . . 14 ⊢ (𝑁 = -(𝑦 · 2) ↔ -(𝑦 · 2) = 𝑁)
75		mulneg1 8265	. . . . . . . . . . . . . . . . 17 ⊢ ((𝑦 ∈ ℂ ∧ 2 ∈ ℂ) → (-𝑦 · 2) = -(𝑦 · 2))
76	68, 14, 75	sylancl 410	. . . . . . . . . . . . . . . 16 ⊢ (𝑦 ∈ ℤ → (-𝑦 · 2) = -(𝑦 · 2))
77	76	adantl 275	. . . . . . . . . . . . . . 15 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (-𝑦 · 2) = -(𝑦 · 2))
78	77	eqeq1d 2166	. . . . . . . . . . . . . 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 5828	. . . . . . . . . . . . 13 ⊢ (𝑘 = -𝑦 → (𝑘 · 2) = (-𝑦 · 2))
83	82	eqeq1d 2166	. . . . . . . . . . . 12 ⊢ (𝑘 = -𝑦 → ((𝑘 · 2) = 𝑁 ↔ (-𝑦 · 2) = 𝑁))
84	83	rspcev 2816	. . . . . . . . . . 11 ⊢ ((-𝑦 ∈ ℤ ∧ (-𝑦 · 2) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
85	67, 81, 84	syl2anc 409	. . . . . . . . . 10 ⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
86	85	ex 114	. . . . . . . . 9 ⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
87	86	rexlimdva 2574	. . . . . . . 8 ⊢ (𝑁 ∈ ℝ → (∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
88	65, 87	orim12d 776	. . . . . . 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 787	. . . 4 ⊢ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨ -𝑁 ∈ ℕ0)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
92	5, 91	sylbi 120	. . 3 ⊢ (𝑁 ∈ ℤ → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
93		halfnz 9255	. . . 4 ⊢ ¬ (1 / 2) ∈ ℤ
94		reeanv 2626	. . . . 5 ⊢ (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))
95		eqtr3 2177	. . . . . . 7 ⊢ ((((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → ((2 · 𝑛) + 1) = (𝑘 · 2))
96		zcn 9167	. . . . . . . . . . 11 ⊢ (𝑘 ∈ ℤ → 𝑘 ∈ ℂ)
97		mulcom 7856	. . . . . . . . . . 11 ⊢ ((𝑘 ∈ ℂ ∧ 2 ∈ ℂ) → (𝑘 · 2) = (2 · 𝑘))
98	96, 14, 97	sylancl 410	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ → (𝑘 · 2) = (2 · 𝑘))
99	98	eqeq2d 2169	. . . . . . . . 9 ⊢ (𝑘 ∈ ℤ → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
100	99	adantl 275	. . . . . . . 8 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑛) + 1) = (𝑘 · 2) ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
101		mulcl 7854	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · 𝑘) ∈ ℂ)
102	14, 96, 101	sylancr 411	. . . . . . . . . 10 ⊢ (𝑘 ∈ ℤ → (2 · 𝑘) ∈ ℂ)
103		zcn 9167	. . . . . . . . . . 11 ⊢ (𝑛 ∈ ℤ → 𝑛 ∈ ℂ)
104		mulcl 7854	. . . . . . . . . . 11 ⊢ ((2 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · 𝑛) ∈ ℂ)
105	14, 103, 104	sylancr 411	. . . . . . . . . 10 ⊢ (𝑛 ∈ ℤ → (2 · 𝑛) ∈ ℂ)
106		subadd 8073	. . . . . . . . . . 11 ⊢ (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
107	27, 106	mp3an3 1308	. . . . . . . . . 10 ⊢ (((2 · 𝑘) ∈ ℂ ∧ (2 · 𝑛) ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
108	102, 105, 107	syl2anr 288	. . . . . . . . 9 ⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘)))
109		subcl 8069	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑘 − 𝑛) ∈ ℂ)
110		2ap0 8921	. . . . . . . . . . . . . . . 16 ⊢ 2 # 0
111	14, 110	pm3.2i 270	. . . . . . . . . . . . . . 15 ⊢ (2 ∈ ℂ ∧ 2 # 0)
112		eqcom 2159	. . . . . . . . . . . . . . . 16 ⊢ ((𝑘 − 𝑛) = (1 / 2) ↔ (1 / 2) = (𝑘 − 𝑛))
113		divmulap 8543	. . . . . . . . . . . . . . . 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 1310	. . . . . . . . . . . . . 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 8255	. . . . . . . . . . . . . . 15 ⊢ ((2 ∈ ℂ ∧ 𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
119	14, 118	mp3an1 1306	. . . . . . . . . . . . . 14 ⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
120	119	ancoms 266	. . . . . . . . . . . . 13 ⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛)))
121	120	eqeq1d 2166	. . . . . . . . . . . 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 9203	. . . . . . . . . . . 12 ⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘 − 𝑛) ∈ ℤ)
125		eleq1 2220	. . . . . . . . . . . 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 2580	. . . . 5 ⊢ (∃𝑛 ∈ ℤ ∃𝑘 ∈ ℤ (((2 · 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
133	94, 132	sylbir 134	. . . 4 ⊢ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (1 / 2) ∈ ℤ)
134	93, 133	mto 652	. . 3 ⊢ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)
135		df-xor 1358	. . . . 5 ⊢ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ⊻ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ↔ ((∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)))
136		xorbin 1366	. . . . 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 410	. 2 ⊢ (𝑁 ∈ ℤ → (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))
140	4, 139	bitrd 187	1 ⊢ (𝑁 ∈ ℤ → (¬ 2 ∥ 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁))

Syntax hints:  ¬ wn 3   → wi 4   ∧ wa 103   ↔ wb 104   ∨ wo 698   ∧ w3a 963   = wceq 1335   ⊻ wxo 1357   ∈ wcel 2128  ∃wrex 2436   class class class wbr 3965  (class class class)co 5821  ℂcc 7725  ℝcr 7726  0cc0 7727  1c1 7728   + caddc 7730   · cmul 7732   − cmin 8041  -cneg 8042   # cap 8451   / cdiv 8540  2c2 8879  ℕ₀cn0 9085  ℤcz 9162   ∥ cdvds 11678

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 604  ax-in2 605  ax-io 699  ax-5 1427  ax-7 1428  ax-gen 1429  ax-ie1 1473  ax-ie2 1474  ax-8 1484  ax-10 1485  ax-11 1486  ax-i12 1487  ax-bndl 1489  ax-4 1490  ax-17 1506  ax-i9 1510  ax-ial 1514  ax-i5r 1515  ax-13 2130  ax-14 2131  ax-ext 2139  ax-sep 4082  ax-pow 4135  ax-pr 4169  ax-un 4393  ax-setind 4495  ax-cnex 7818  ax-resscn 7819  ax-1cn 7820  ax-1re 7821  ax-icn 7822  ax-addcl 7823  ax-addrcl 7824  ax-mulcl 7825  ax-mulrcl 7826  ax-addcom 7827  ax-mulcom 7828  ax-addass 7829  ax-mulass 7830  ax-distr 7831  ax-i2m1 7832  ax-0lt1 7833  ax-1rid 7834  ax-0id 7835  ax-rnegex 7836  ax-precex 7837  ax-cnre 7838  ax-pre-ltirr 7839  ax-pre-ltwlin 7840  ax-pre-lttrn 7841  ax-pre-apti 7842  ax-pre-ltadd 7843  ax-pre-mulgt0 7844  ax-pre-mulext 7845

This theorem depends on definitions:  df-bi 116  df-3or 964  df-3an 965  df-tru 1338  df-fal 1341  df-xor 1358  df-nf 1441  df-sb 1743  df-eu 2009  df-mo 2010  df-clab 2144  df-cleq 2150  df-clel 2153  df-nfc 2288  df-ne 2328  df-nel 2423  df-ral 2440  df-rex 2441  df-reu 2442  df-rmo 2443  df-rab 2444  df-v 2714  df-sbc 2938  df-dif 3104  df-un 3106  df-in 3108  df-ss 3115  df-pw 3545  df-sn 3566  df-pr 3567  df-op 3569  df-uni 3773  df-int 3808  df-br 3966  df-opab 4026  df-id 4253  df-po 4256  df-iso 4257  df-xp 4591  df-rel 4592  df-cnv 4593  df-co 4594  df-dm 4595  df-iota 5134  df-fun 5171  df-fv 5177  df-riota 5777  df-ov 5824  df-oprab 5825  df-mpo 5826  df-pnf 7909  df-mnf 7910  df-xr 7911  df-ltxr 7912  df-le 7913  df-sub 8043  df-neg 8044  df-reap 8445  df-ap 8452  df-div 8541  df-inn 8829  df-2 8887  df-n0 9086  df-z 9163  df-dvds 11679

This theorem is referenced by:  oddm1even  11760  oexpneg  11762  oddnn02np1  11765  2tp1odd  11769  sqoddm1div8z  11771  ltoddhalfle  11778  halfleoddlt  11779  opoe  11780  omoe  11781  opeo  11782  omeo  11783  m1expo  11785  m1exp1  11786  flodddiv4  11819