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) = 𝑁)) |