Step | Hyp | Ref
| Expression |
1 | | 2z 11737 |
. . . 4
⊢ 2 ∈
ℤ |
2 | | divides 15359 |
. . . 4
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
3 | 1, 2 | mpan 683 |
. . 3
⊢ (𝑁 ∈ ℤ → (2
∥ 𝑁 ↔
∃𝑘 ∈ ℤ
(𝑘 · 2) = 𝑁)) |
4 | 3 | notbid 310 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔ ¬
∃𝑘 ∈ ℤ
(𝑘 · 2) = 𝑁)) |
5 | | elznn0 11719 |
. . . 4
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0))) |
6 | | odd2np1lem 15438 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
7 | 6 | adantl 475 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0)
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
8 | | odd2np1lem 15438 |
. . . . . . 7
⊢ (-𝑁 ∈ ℕ0
→ (∃𝑥 ∈
ℤ ((2 · 𝑥) +
1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁)) |
9 | | peano2z 11746 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈
ℤ) |
10 | | znegcl 11740 |
. . . . . . . . . . . 12
⊢ ((𝑥 + 1) ∈ ℤ →
-(𝑥 + 1) ∈
ℤ) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ℤ → -(𝑥 + 1) ∈
ℤ) |
12 | 11 | ad2antlr 720 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2
· 𝑥) + 1) = -𝑁) → -(𝑥 + 1) ∈ ℤ) |
13 | | zcn 11709 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
14 | | 2cn 11426 |
. . . . . . . . . . . . . . . . 17
⊢ 2 ∈
ℂ |
15 | | mulcl 10336 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
16 | 14, 15 | mpan 683 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
17 | | peano2cn 10527 |
. . . . . . . . . . . . . . . 16
⊢ ((2
· 𝑥) ∈ ℂ
→ ((2 · 𝑥) + 1)
∈ ℂ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℂ → ((2
· 𝑥) + 1) ∈
ℂ) |
19 | 13, 18 | syl 17 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) + 1) ∈
ℂ) |
20 | 19 | adantl 475 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((2
· 𝑥) + 1) ∈
ℂ) |
21 | | simpl 476 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈
ℝ) |
22 | 21 | recnd 10385 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈
ℂ) |
23 | | negcon2 10655 |
. . . . . . . . . . . . 13
⊢ ((((2
· 𝑥) + 1) ∈
ℂ ∧ 𝑁 ∈
ℂ) → (((2 · 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1))) |
24 | 20, 22, 23 | syl2anc 581 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2
· 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1))) |
25 | | eqcom 2832 |
. . . . . . . . . . . . 13
⊢ (𝑁 = -((2 · 𝑥) + 1) ↔ -((2 ·
𝑥) + 1) = 𝑁) |
26 | 14, 13, 15 | sylancr 583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℂ) |
27 | | ax-1cn 10310 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ 1 ∈
ℂ |
28 | 14, 27 | mulcli 10364 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
· 1) ∈ ℂ |
29 | | addsubass 10612 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((2
· 𝑥) ∈ ℂ
∧ (2 · 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((2
· 𝑥) + (2 ·
1)) − 1) = ((2 · 𝑥) + ((2 · 1) −
1))) |
30 | 28, 27, 29 | mp3an23 1583 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 𝑥) ∈ ℂ
→ (((2 · 𝑥) +
(2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) −
1))) |
31 | 26, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + (2 ·
1)) − 1) = ((2 · 𝑥) + ((2 · 1) −
1))) |
32 | | 2t1e2 11521 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
· 1) = 2 |
33 | 32 | oveq1i 6915 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
· 1) − 1) = (2 − 1) |
34 | | 2m1e1 11484 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (2
− 1) = 1 |
35 | 33, 34 | eqtri 2849 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 1) − 1) = 1 |
36 | 35 | oveq2i 6916 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
· 𝑥) + ((2 ·
1) − 1)) = ((2 · 𝑥) + 1) |
37 | 31, 36 | syl6req 2878 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) + 1) = (((2
· 𝑥) + (2 ·
1)) − 1)) |
38 | | adddi 10341 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1))) |
39 | 14, 27, 38 | mp3an13 1582 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℂ → (2
· (𝑥 + 1)) = ((2
· 𝑥) + (2 ·
1))) |
40 | 13, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → (2
· (𝑥 + 1)) = ((2
· 𝑥) + (2 ·
1))) |
41 | 40 | oveq1d 6920 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → ((2
· (𝑥 + 1)) −
1) = (((2 · 𝑥) + (2
· 1)) − 1)) |
42 | 37, 41 | eqtr4d 2864 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) + 1) = ((2
· (𝑥 + 1)) −
1)) |
43 | 42 | negeqd 10595 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → -((2
· 𝑥) + 1) = -((2
· (𝑥 + 1)) −
1)) |
44 | 9 | zcnd 11811 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈
ℂ) |
45 | | mulneg2 10791 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℂ ∧ (𝑥 +
1) ∈ ℂ) → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1))) |
46 | 14, 44, 45 | sylancr 583 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → (2
· -(𝑥 + 1)) = -(2
· (𝑥 +
1))) |
47 | 46 | oveq1d 6920 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → ((2
· -(𝑥 + 1)) + 1) =
(-(2 · (𝑥 + 1)) +
1)) |
48 | | mulcl 10336 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((2
∈ ℂ ∧ (𝑥 +
1) ∈ ℂ) → (2 · (𝑥 + 1)) ∈ ℂ) |
49 | 14, 44, 48 | sylancr 583 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → (2
· (𝑥 + 1)) ∈
ℂ) |
50 | | negsubdi 10658 |
. . . . . . . . . . . . . . . . . 18
⊢ (((2
· (𝑥 + 1)) ∈
ℂ ∧ 1 ∈ ℂ) → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1)) |
51 | 49, 27, 50 | sylancl 582 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → -((2
· (𝑥 + 1)) −
1) = (-(2 · (𝑥 + 1))
+ 1)) |
52 | 47, 51 | eqtr4d 2864 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → ((2
· -(𝑥 + 1)) + 1) =
-((2 · (𝑥 + 1))
− 1)) |
53 | 43, 52 | eqtr4d 2864 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → -((2
· 𝑥) + 1) = ((2
· -(𝑥 + 1)) +
1)) |
54 | 53 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → -((2
· 𝑥) + 1) = ((2
· -(𝑥 + 1)) +
1)) |
55 | 54 | eqeq1d 2827 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-((2
· 𝑥) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁)) |
56 | 25, 55 | syl5bb 275 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑁 = -((2 · 𝑥) + 1) ↔ ((2 ·
-(𝑥 + 1)) + 1) = 𝑁)) |
57 | 24, 56 | bitrd 271 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2
· 𝑥) + 1) = -𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁)) |
58 | 57 | biimpa 470 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2
· 𝑥) + 1) = -𝑁) → ((2 · -(𝑥 + 1)) + 1) = 𝑁) |
59 | | oveq2 6913 |
. . . . . . . . . . . . 13
⊢ (𝑛 = -(𝑥 + 1) → (2 · 𝑛) = (2 · -(𝑥 + 1))) |
60 | 59 | oveq1d 6920 |
. . . . . . . . . . . 12
⊢ (𝑛 = -(𝑥 + 1) → ((2 · 𝑛) + 1) = ((2 · -(𝑥 + 1)) + 1)) |
61 | 60 | eqeq1d 2827 |
. . . . . . . . . . 11
⊢ (𝑛 = -(𝑥 + 1) → (((2 · 𝑛) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁)) |
62 | 61 | rspcev 3526 |
. . . . . . . . . 10
⊢ ((-(𝑥 + 1) ∈ ℤ ∧ ((2
· -(𝑥 + 1)) + 1) =
𝑁) → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁) |
63 | 12, 58, 62 | syl2anc 581 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2
· 𝑥) + 1) = -𝑁) → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁) |
64 | 63 | rexlimdva2 3243 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ →
(∃𝑥 ∈ ℤ
((2 · 𝑥) + 1) =
-𝑁 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
65 | | znegcl 11740 |
. . . . . . . . . . 11
⊢ (𝑦 ∈ ℤ → -𝑦 ∈
ℤ) |
66 | 65 | ad2antlr 720 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → -𝑦 ∈ ℤ) |
67 | | zcn 11709 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
68 | | mulcl 10336 |
. . . . . . . . . . . . . 14
⊢ ((𝑦 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑦 ·
2) ∈ ℂ) |
69 | 67, 14, 68 | sylancl 582 |
. . . . . . . . . . . . 13
⊢ (𝑦 ∈ ℤ → (𝑦 · 2) ∈
ℂ) |
70 | | recn 10342 |
. . . . . . . . . . . . 13
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℂ) |
71 | | negcon2 10655 |
. . . . . . . . . . . . 13
⊢ (((𝑦 · 2) ∈ ℂ
∧ 𝑁 ∈ ℂ)
→ ((𝑦 · 2) =
-𝑁 ↔ 𝑁 = -(𝑦 · 2))) |
72 | 69, 70, 71 | syl2anr 592 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ 𝑁 = -(𝑦 · 2))) |
73 | | mulneg1 10790 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑦 ∈ ℂ ∧ 2 ∈
ℂ) → (-𝑦
· 2) = -(𝑦 ·
2)) |
74 | 67, 14, 73 | sylancl 582 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℤ → (-𝑦 · 2) = -(𝑦 · 2)) |
75 | 74 | adantl 475 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (-𝑦 · 2) = -(𝑦 · 2)) |
76 | 75 | eqeq1d 2827 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((-𝑦 · 2) = 𝑁 ↔ -(𝑦 · 2) = 𝑁)) |
77 | | eqcom 2832 |
. . . . . . . . . . . . 13
⊢ (𝑁 = -(𝑦 · 2) ↔ -(𝑦 · 2) = 𝑁) |
78 | 76, 77 | syl6rbbr 282 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑁 = -(𝑦 · 2) ↔ (-𝑦 · 2) = 𝑁)) |
79 | 72, 78 | bitrd 271 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ (-𝑦 · 2) = 𝑁)) |
80 | 79 | biimpa 470 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → (-𝑦 · 2) = 𝑁) |
81 | | oveq1 6912 |
. . . . . . . . . . . 12
⊢ (𝑘 = -𝑦 → (𝑘 · 2) = (-𝑦 · 2)) |
82 | 81 | eqeq1d 2827 |
. . . . . . . . . . 11
⊢ (𝑘 = -𝑦 → ((𝑘 · 2) = 𝑁 ↔ (-𝑦 · 2) = 𝑁)) |
83 | 82 | rspcev 3526 |
. . . . . . . . . 10
⊢ ((-𝑦 ∈ ℤ ∧ (-𝑦 · 2) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) |
84 | 66, 80, 83 | syl2anc 581 |
. . . . . . . . 9
⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) |
85 | 84 | rexlimdva2 3243 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ →
(∃𝑦 ∈ ℤ
(𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
86 | 64, 85 | orim12d 994 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
((∃𝑥 ∈ ℤ
((2 · 𝑥) + 1) =
-𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁) → (∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))) |
87 | 8, 86 | syl5 34 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (-𝑁 ∈ ℕ0
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))) |
88 | 87 | imp 397 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0)
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
89 | 7, 88 | jaodan 987 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
90 | 5, 89 | sylbi 209 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
91 | | halfnz 11783 |
. . . 4
⊢ ¬ (1
/ 2) ∈ ℤ |
92 | | reeanv 3317 |
. . . . 5
⊢
(∃𝑛 ∈
ℤ ∃𝑘 ∈
ℤ (((2 · 𝑛) +
1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
93 | | eqtr3 2848 |
. . . . . . 7
⊢ ((((2
· 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → ((2 · 𝑛) + 1) = (𝑘 · 2)) |
94 | | zcn 11709 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
95 | | mulcom 10338 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑘 ·
2) = (2 · 𝑘)) |
96 | 94, 14, 95 | sylancl 582 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (𝑘 · 2) = (2 · 𝑘)) |
97 | 96 | eqeq2d 2835 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℤ → (((2
· 𝑛) + 1) = (𝑘 · 2) ↔ ((2 ·
𝑛) + 1) = (2 · 𝑘))) |
98 | 97 | adantl 475 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑛) + 1) = (𝑘 · 2) ↔ ((2 ·
𝑛) + 1) = (2 · 𝑘))) |
99 | | mulcl 10336 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑘
∈ ℂ) → (2 · 𝑘) ∈ ℂ) |
100 | 14, 94, 99 | sylancr 583 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (2
· 𝑘) ∈
ℂ) |
101 | | zcn 11709 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
102 | | mulcl 10336 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · 𝑛) ∈ ℂ) |
103 | 14, 101, 102 | sylancr 583 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℂ) |
104 | | subadd 10604 |
. . . . . . . . . . 11
⊢ (((2
· 𝑘) ∈ ℂ
∧ (2 · 𝑛) ∈
ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘))) |
105 | 27, 104 | mp3an3 1580 |
. . . . . . . . . 10
⊢ (((2
· 𝑘) ∈ ℂ
∧ (2 · 𝑛) ∈
ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘))) |
106 | 100, 103,
105 | syl2anr 592 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑘) − (2
· 𝑛)) = 1 ↔ ((2
· 𝑛) + 1) = (2
· 𝑘))) |
107 | | subcl 10600 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑘 − 𝑛) ∈ ℂ) |
108 | | 2cnne0 11568 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
109 | | eqcom 2832 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 − 𝑛) = (1 / 2) ↔ (1 / 2) = (𝑘 − 𝑛)) |
110 | | divmul 11013 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝑘
− 𝑛) ∈ ℂ
∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) = (𝑘 − 𝑛) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
111 | 109, 110 | syl5bb 275 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ (𝑘
− 𝑛) ∈ ℂ
∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
112 | 27, 108, 111 | mp3an13 1582 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 − 𝑛) ∈ ℂ → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
113 | 107, 112 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
114 | 113 | ancoms 452 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
115 | | subdi 10787 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑘
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛))) |
116 | 14, 115 | mp3an1 1578 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2
· (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛))) |
117 | 116 | ancoms 452 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2
· (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛))) |
118 | 117 | eqeq1d 2827 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((2
· (𝑘 − 𝑛)) = 1 ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1)) |
119 | 114, 118 | bitrd 271 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1)) |
120 | 101, 94, 119 | syl2an 591 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1)) |
121 | | zsubcl 11747 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘 − 𝑛) ∈ ℤ) |
122 | | eleq1 2894 |
. . . . . . . . . . . 12
⊢ ((𝑘 − 𝑛) = (1 / 2) → ((𝑘 − 𝑛) ∈ ℤ ↔ (1 / 2) ∈
ℤ)) |
123 | 121, 122 | syl5ibcom 237 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) → (1 / 2) ∈
ℤ)) |
124 | 123 | ancoms 452 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) → (1 / 2) ∈
ℤ)) |
125 | 120, 124 | sylbird 252 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑘) − (2
· 𝑛)) = 1 → (1
/ 2) ∈ ℤ)) |
126 | 106, 125 | sylbird 252 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑛) + 1) = (2
· 𝑘) → (1 / 2)
∈ ℤ)) |
127 | 98, 126 | sylbid 232 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑛) + 1) = (𝑘 · 2) → (1 / 2)
∈ ℤ)) |
128 | 93, 127 | syl5 34 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((((2
· 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈
ℤ)) |
129 | 128 | rexlimivv 3246 |
. . . . 5
⊢
(∃𝑛 ∈
ℤ ∃𝑘 ∈
ℤ (((2 · 𝑛) +
1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈
ℤ) |
130 | 92, 129 | sylbir 227 |
. . . 4
⊢
((∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (1 / 2) ∈
ℤ) |
131 | 91, 130 | mto 189 |
. . 3
⊢ ¬
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) |
132 | | pm5.17 1042 |
. . . 4
⊢
(((∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
133 | | bicom 214 |
. . . 4
⊢
((∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ↔ ¬
∃𝑘 ∈ ℤ
(𝑘 · 2) = 𝑁) ↔ (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) |
134 | 132, 133 | bitri 267 |
. . 3
⊢
(((∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) ↔ (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) |
135 | 90, 131, 134 | sylanblc 585 |
. 2
⊢ (𝑁 ∈ ℤ → (¬
∃𝑘 ∈ ℤ
(𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
136 | 4, 135 | bitrd 271 |
1
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |