Step | Hyp | Ref
| Expression |
1 | | 2z 11409 |
. . . 4
⊢ 2 ∈
ℤ |
2 | | divides 14985 |
. . . 4
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 ∥ 𝑁 ↔ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
3 | 1, 2 | mpan 706 |
. . 3
⊢ (𝑁 ∈ ℤ → (2
∥ 𝑁 ↔
∃𝑘 ∈ ℤ
(𝑘 · 2) = 𝑁)) |
4 | 3 | notbid 308 |
. 2
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔ ¬
∃𝑘 ∈ ℤ
(𝑘 · 2) = 𝑁)) |
5 | | elznn0 11392 |
. . . 4
⊢ (𝑁 ∈ ℤ ↔ (𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0))) |
6 | | odd2np1lem 15064 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
7 | 6 | adantl 482 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ 𝑁 ∈ ℕ0)
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
8 | | odd2np1lem 15064 |
. . . . . . 7
⊢ (-𝑁 ∈ ℕ0
→ (∃𝑥 ∈
ℤ ((2 · 𝑥) +
1) = -𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁)) |
9 | | peano2z 11418 |
. . . . . . . . . . . . 13
⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈
ℤ) |
10 | | znegcl 11412 |
. . . . . . . . . . . . 13
⊢ ((𝑥 + 1) ∈ ℤ →
-(𝑥 + 1) ∈
ℤ) |
11 | 9, 10 | syl 17 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℤ → -(𝑥 + 1) ∈
ℤ) |
12 | 11 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2
· 𝑥) + 1) = -𝑁) → -(𝑥 + 1) ∈ ℤ) |
13 | | zcn 11382 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → 𝑥 ∈
ℂ) |
14 | | 2cn 11091 |
. . . . . . . . . . . . . . . . . 18
⊢ 2 ∈
ℂ |
15 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . 18
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ) → (2 · 𝑥) ∈ ℂ) |
16 | 14, 15 | mpan 706 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℂ → (2
· 𝑥) ∈
ℂ) |
17 | | peano2cn 10208 |
. . . . . . . . . . . . . . . . 17
⊢ ((2
· 𝑥) ∈ ℂ
→ ((2 · 𝑥) + 1)
∈ ℂ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℂ → ((2
· 𝑥) + 1) ∈
ℂ) |
19 | 13, 18 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) + 1) ∈
ℂ) |
20 | 19 | adantl 482 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → ((2
· 𝑥) + 1) ∈
ℂ) |
21 | | simpl 473 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈
ℝ) |
22 | 21 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → 𝑁 ∈
ℂ) |
23 | | negcon2 10334 |
. . . . . . . . . . . . . 14
⊢ ((((2
· 𝑥) + 1) ∈
ℂ ∧ 𝑁 ∈
ℂ) → (((2 · 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1))) |
24 | 20, 22, 23 | syl2anc 693 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2
· 𝑥) + 1) = -𝑁 ↔ 𝑁 = -((2 · 𝑥) + 1))) |
25 | | eqcom 2629 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = -((2 · 𝑥) + 1) ↔ -((2 ·
𝑥) + 1) = 𝑁) |
26 | 14, 13, 15 | sylancr 695 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℤ → (2
· 𝑥) ∈
ℂ) |
27 | | ax-1cn 9994 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ 1 ∈
ℂ |
28 | 14, 27 | mulcli 10045 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
· 1) ∈ ℂ |
29 | | addsubass 10291 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((2
· 𝑥) ∈ ℂ
∧ (2 · 1) ∈ ℂ ∧ 1 ∈ ℂ) → (((2
· 𝑥) + (2 ·
1)) − 1) = ((2 · 𝑥) + ((2 · 1) −
1))) |
30 | 28, 27, 29 | mp3an23 1416 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
· 𝑥) ∈ ℂ
→ (((2 · 𝑥) +
(2 · 1)) − 1) = ((2 · 𝑥) + ((2 · 1) −
1))) |
31 | 26, 30 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → (((2
· 𝑥) + (2 ·
1)) − 1) = ((2 · 𝑥) + ((2 · 1) −
1))) |
32 | | 2t1e2 11176 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (2
· 1) = 2 |
33 | 32 | oveq1i 6660 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
· 1) − 1) = (2 − 1) |
34 | | 2m1e1 11135 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (2
− 1) = 1 |
35 | 33, 34 | eqtri 2644 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((2
· 1) − 1) = 1 |
36 | 35 | oveq2i 6661 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
· 𝑥) + ((2 ·
1) − 1)) = ((2 · 𝑥) + 1) |
37 | 31, 36 | syl6req 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) + 1) = (((2
· 𝑥) + (2 ·
1)) − 1)) |
38 | | adddi 10025 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((2
∈ ℂ ∧ 𝑥
∈ ℂ ∧ 1 ∈ ℂ) → (2 · (𝑥 + 1)) = ((2 · 𝑥) + (2 · 1))) |
39 | 14, 27, 38 | mp3an13 1415 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑥 ∈ ℂ → (2
· (𝑥 + 1)) = ((2
· 𝑥) + (2 ·
1))) |
40 | 13, 39 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → (2
· (𝑥 + 1)) = ((2
· 𝑥) + (2 ·
1))) |
41 | 40 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → ((2
· (𝑥 + 1)) −
1) = (((2 · 𝑥) + (2
· 1)) − 1)) |
42 | 37, 41 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → ((2
· 𝑥) + 1) = ((2
· (𝑥 + 1)) −
1)) |
43 | 42 | negeqd 10275 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → -((2
· 𝑥) + 1) = -((2
· (𝑥 + 1)) −
1)) |
44 | 9 | zcnd 11483 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑥 ∈ ℤ → (𝑥 + 1) ∈
ℂ) |
45 | | mulneg2 10467 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℂ ∧ (𝑥 +
1) ∈ ℂ) → (2 · -(𝑥 + 1)) = -(2 · (𝑥 + 1))) |
46 | 14, 44, 45 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → (2
· -(𝑥 + 1)) = -(2
· (𝑥 +
1))) |
47 | 46 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → ((2
· -(𝑥 + 1)) + 1) =
(-(2 · (𝑥 + 1)) +
1)) |
48 | | mulcl 10020 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((2
∈ ℂ ∧ (𝑥 +
1) ∈ ℂ) → (2 · (𝑥 + 1)) ∈ ℂ) |
49 | 14, 44, 48 | sylancr 695 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ ℤ → (2
· (𝑥 + 1)) ∈
ℂ) |
50 | | negsubdi 10337 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((2
· (𝑥 + 1)) ∈
ℂ ∧ 1 ∈ ℂ) → -((2 · (𝑥 + 1)) − 1) = (-(2 · (𝑥 + 1)) + 1)) |
51 | 49, 27, 50 | sylancl 694 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ ℤ → -((2
· (𝑥 + 1)) −
1) = (-(2 · (𝑥 + 1))
+ 1)) |
52 | 47, 51 | eqtr4d 2659 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ ℤ → ((2
· -(𝑥 + 1)) + 1) =
-((2 · (𝑥 + 1))
− 1)) |
53 | 43, 52 | eqtr4d 2659 |
. . . . . . . . . . . . . . . 16
⊢ (𝑥 ∈ ℤ → -((2
· 𝑥) + 1) = ((2
· -(𝑥 + 1)) +
1)) |
54 | 53 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → -((2
· 𝑥) + 1) = ((2
· -(𝑥 + 1)) +
1)) |
55 | 54 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (-((2
· 𝑥) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁)) |
56 | 25, 55 | syl5bb 272 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (𝑁 = -((2 · 𝑥) + 1) ↔ ((2 ·
-(𝑥 + 1)) + 1) = 𝑁)) |
57 | 24, 56 | bitrd 268 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2
· 𝑥) + 1) = -𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁)) |
58 | 57 | biimpa 501 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2
· 𝑥) + 1) = -𝑁) → ((2 · -(𝑥 + 1)) + 1) = 𝑁) |
59 | | oveq2 6658 |
. . . . . . . . . . . . . 14
⊢ (𝑛 = -(𝑥 + 1) → (2 · 𝑛) = (2 · -(𝑥 + 1))) |
60 | 59 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (𝑛 = -(𝑥 + 1) → ((2 · 𝑛) + 1) = ((2 · -(𝑥 + 1)) + 1)) |
61 | 60 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑛 = -(𝑥 + 1) → (((2 · 𝑛) + 1) = 𝑁 ↔ ((2 · -(𝑥 + 1)) + 1) = 𝑁)) |
62 | 61 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((-(𝑥 + 1) ∈ ℤ ∧ ((2
· -(𝑥 + 1)) + 1) =
𝑁) → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁) |
63 | 12, 58, 62 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) ∧ ((2
· 𝑥) + 1) = -𝑁) → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁) |
64 | 63 | ex 450 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 𝑥 ∈ ℤ) → (((2
· 𝑥) + 1) = -𝑁 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
65 | 64 | rexlimdva 3031 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ →
(∃𝑥 ∈ ℤ
((2 · 𝑥) + 1) =
-𝑁 → ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
66 | | znegcl 11412 |
. . . . . . . . . . . 12
⊢ (𝑦 ∈ ℤ → -𝑦 ∈
ℤ) |
67 | 66 | ad2antlr 763 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → -𝑦 ∈ ℤ) |
68 | | zcn 11382 |
. . . . . . . . . . . . . . 15
⊢ (𝑦 ∈ ℤ → 𝑦 ∈
ℂ) |
69 | | mulcl 10020 |
. . . . . . . . . . . . . . 15
⊢ ((𝑦 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑦 ·
2) ∈ ℂ) |
70 | 68, 14, 69 | sylancl 694 |
. . . . . . . . . . . . . 14
⊢ (𝑦 ∈ ℤ → (𝑦 · 2) ∈
ℂ) |
71 | | recn 10026 |
. . . . . . . . . . . . . 14
⊢ (𝑁 ∈ ℝ → 𝑁 ∈
ℂ) |
72 | | negcon2 10334 |
. . . . . . . . . . . . . 14
⊢ (((𝑦 · 2) ∈ ℂ
∧ 𝑁 ∈ ℂ)
→ ((𝑦 · 2) =
-𝑁 ↔ 𝑁 = -(𝑦 · 2))) |
73 | 70, 71, 72 | syl2anr 495 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ 𝑁 = -(𝑦 · 2))) |
74 | | mulneg1 10466 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑦 ∈ ℂ ∧ 2 ∈
ℂ) → (-𝑦
· 2) = -(𝑦 ·
2)) |
75 | 68, 14, 74 | sylancl 694 |
. . . . . . . . . . . . . . . 16
⊢ (𝑦 ∈ ℤ → (-𝑦 · 2) = -(𝑦 · 2)) |
76 | 75 | adantl 482 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (-𝑦 · 2) = -(𝑦 · 2)) |
77 | 76 | eqeq1d 2624 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((-𝑦 · 2) = 𝑁 ↔ -(𝑦 · 2) = 𝑁)) |
78 | | eqcom 2629 |
. . . . . . . . . . . . . 14
⊢ (𝑁 = -(𝑦 · 2) ↔ -(𝑦 · 2) = 𝑁) |
79 | 77, 78 | syl6rbbr 279 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → (𝑁 = -(𝑦 · 2) ↔ (-𝑦 · 2) = 𝑁)) |
80 | 73, 79 | bitrd 268 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 ↔ (-𝑦 · 2) = 𝑁)) |
81 | 80 | biimpa 501 |
. . . . . . . . . . 11
⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → (-𝑦 · 2) = 𝑁) |
82 | | oveq1 6657 |
. . . . . . . . . . . . 13
⊢ (𝑘 = -𝑦 → (𝑘 · 2) = (-𝑦 · 2)) |
83 | 82 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ (𝑘 = -𝑦 → ((𝑘 · 2) = 𝑁 ↔ (-𝑦 · 2) = 𝑁)) |
84 | 83 | rspcev 3309 |
. . . . . . . . . . 11
⊢ ((-𝑦 ∈ ℤ ∧ (-𝑦 · 2) = 𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) |
85 | 67, 81, 84 | syl2anc 693 |
. . . . . . . . . 10
⊢ (((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) ∧ (𝑦 · 2) = -𝑁) → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) |
86 | 85 | ex 450 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℝ ∧ 𝑦 ∈ ℤ) → ((𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
87 | 86 | rexlimdva 3031 |
. . . . . . . 8
⊢ (𝑁 ∈ ℝ →
(∃𝑦 ∈ ℤ
(𝑦 · 2) = -𝑁 → ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
88 | 65, 87 | orim12d 883 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
((∃𝑥 ∈ ℤ
((2 · 𝑥) + 1) =
-𝑁 ∨ ∃𝑦 ∈ ℤ (𝑦 · 2) = -𝑁) → (∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))) |
89 | 8, 88 | syl5 34 |
. . . . . 6
⊢ (𝑁 ∈ ℝ → (-𝑁 ∈ ℕ0
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁))) |
90 | 89 | imp 445 |
. . . . 5
⊢ ((𝑁 ∈ ℝ ∧ -𝑁 ∈ ℕ0)
→ (∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
91 | 7, 90 | jaodan 826 |
. . . 4
⊢ ((𝑁 ∈ ℝ ∧ (𝑁 ∈ ℕ0 ∨
-𝑁 ∈
ℕ0)) → (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
92 | 5, 91 | sylbi 207 |
. . 3
⊢ (𝑁 ∈ ℤ →
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
93 | | halfnz 11455 |
. . . 4
⊢ ¬ (1
/ 2) ∈ ℤ |
94 | | reeanv 3107 |
. . . . 5
⊢
(∃𝑛 ∈
ℤ ∃𝑘 ∈
ℤ (((2 · 𝑛) +
1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
95 | | eqtr3 2643 |
. . . . . . 7
⊢ ((((2
· 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → ((2 · 𝑛) + 1) = (𝑘 · 2)) |
96 | | zcn 11382 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℤ → 𝑘 ∈
ℂ) |
97 | | mulcom 10022 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℂ ∧ 2 ∈
ℂ) → (𝑘 ·
2) = (2 · 𝑘)) |
98 | 96, 14, 97 | sylancl 694 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (𝑘 · 2) = (2 · 𝑘)) |
99 | 98 | eqeq2d 2632 |
. . . . . . . . 9
⊢ (𝑘 ∈ ℤ → (((2
· 𝑛) + 1) = (𝑘 · 2) ↔ ((2 ·
𝑛) + 1) = (2 · 𝑘))) |
100 | 99 | adantl 482 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑛) + 1) = (𝑘 · 2) ↔ ((2 ·
𝑛) + 1) = (2 · 𝑘))) |
101 | | mulcl 10020 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑘
∈ ℂ) → (2 · 𝑘) ∈ ℂ) |
102 | 14, 96, 101 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℤ → (2
· 𝑘) ∈
ℂ) |
103 | | zcn 11382 |
. . . . . . . . . . 11
⊢ (𝑛 ∈ ℤ → 𝑛 ∈
ℂ) |
104 | | mulcl 10020 |
. . . . . . . . . . 11
⊢ ((2
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · 𝑛) ∈ ℂ) |
105 | 14, 103, 104 | sylancr 695 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℤ → (2
· 𝑛) ∈
ℂ) |
106 | | subadd 10284 |
. . . . . . . . . . 11
⊢ (((2
· 𝑘) ∈ ℂ
∧ (2 · 𝑛) ∈
ℂ ∧ 1 ∈ ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘))) |
107 | 27, 106 | mp3an3 1413 |
. . . . . . . . . 10
⊢ (((2
· 𝑘) ∈ ℂ
∧ (2 · 𝑛) ∈
ℂ) → (((2 · 𝑘) − (2 · 𝑛)) = 1 ↔ ((2 · 𝑛) + 1) = (2 · 𝑘))) |
108 | 102, 105,
107 | syl2anr 495 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑘) − (2
· 𝑛)) = 1 ↔ ((2
· 𝑛) + 1) = (2
· 𝑘))) |
109 | | subcl 10280 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (𝑘 − 𝑛) ∈ ℂ) |
110 | | 2cnne0 11242 |
. . . . . . . . . . . . . . 15
⊢ (2 ∈
ℂ ∧ 2 ≠ 0) |
111 | | eqcom 2629 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑘 − 𝑛) = (1 / 2) ↔ (1 / 2) = (𝑘 − 𝑛)) |
112 | | divmul 10688 |
. . . . . . . . . . . . . . . 16
⊢ ((1
∈ ℂ ∧ (𝑘
− 𝑛) ∈ ℂ
∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((1 / 2) = (𝑘 − 𝑛) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
113 | 111, 112 | syl5bb 272 |
. . . . . . . . . . . . . . 15
⊢ ((1
∈ ℂ ∧ (𝑘
− 𝑛) ∈ ℂ
∧ (2 ∈ ℂ ∧ 2 ≠ 0)) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
114 | 27, 110, 113 | mp3an13 1415 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 − 𝑛) ∈ ℂ → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
115 | 109, 114 | syl 17 |
. . . . . . . . . . . . 13
⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
116 | 115 | ancoms 469 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ (2 · (𝑘 − 𝑛)) = 1)) |
117 | | subdi 10463 |
. . . . . . . . . . . . . . 15
⊢ ((2
∈ ℂ ∧ 𝑘
∈ ℂ ∧ 𝑛
∈ ℂ) → (2 · (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛))) |
118 | 14, 117 | mp3an1 1411 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℂ ∧ 𝑛 ∈ ℂ) → (2
· (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛))) |
119 | 118 | ancoms 469 |
. . . . . . . . . . . . 13
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → (2
· (𝑘 − 𝑛)) = ((2 · 𝑘) − (2 · 𝑛))) |
120 | 119 | eqeq1d 2624 |
. . . . . . . . . . . 12
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((2
· (𝑘 − 𝑛)) = 1 ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1)) |
121 | 116, 120 | bitrd 268 |
. . . . . . . . . . 11
⊢ ((𝑛 ∈ ℂ ∧ 𝑘 ∈ ℂ) → ((𝑘 − 𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1)) |
122 | 103, 96, 121 | syl2an 494 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) ↔ ((2 · 𝑘) − (2 · 𝑛)) = 1)) |
123 | | zsubcl 11419 |
. . . . . . . . . . . 12
⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → (𝑘 − 𝑛) ∈ ℤ) |
124 | | eleq1 2689 |
. . . . . . . . . . . 12
⊢ ((𝑘 − 𝑛) = (1 / 2) → ((𝑘 − 𝑛) ∈ ℤ ↔ (1 / 2) ∈
ℤ)) |
125 | 123, 124 | syl5ibcom 235 |
. . . . . . . . . . 11
⊢ ((𝑘 ∈ ℤ ∧ 𝑛 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) → (1 / 2) ∈
ℤ)) |
126 | 125 | ancoms 469 |
. . . . . . . . . 10
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((𝑘 − 𝑛) = (1 / 2) → (1 / 2) ∈
ℤ)) |
127 | 122, 126 | sylbird 250 |
. . . . . . . . 9
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑘) − (2
· 𝑛)) = 1 → (1
/ 2) ∈ ℤ)) |
128 | 108, 127 | sylbird 250 |
. . . . . . . 8
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑛) + 1) = (2
· 𝑘) → (1 / 2)
∈ ℤ)) |
129 | 100, 128 | sylbid 230 |
. . . . . . 7
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → (((2
· 𝑛) + 1) = (𝑘 · 2) → (1 / 2)
∈ ℤ)) |
130 | 95, 129 | syl5 34 |
. . . . . 6
⊢ ((𝑛 ∈ ℤ ∧ 𝑘 ∈ ℤ) → ((((2
· 𝑛) + 1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈
ℤ)) |
131 | 130 | rexlimivv 3036 |
. . . . 5
⊢
(∃𝑛 ∈
ℤ ∃𝑘 ∈
ℤ (((2 · 𝑛) +
1) = 𝑁 ∧ (𝑘 · 2) = 𝑁) → (1 / 2) ∈
ℤ) |
132 | 94, 131 | sylbir 225 |
. . . 4
⊢
((∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) → (1 / 2) ∈
ℤ) |
133 | 93, 132 | mto 188 |
. . 3
⊢ ¬
(∃𝑛 ∈ ℤ
((2 · 𝑛) + 1) =
𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) |
134 | | pm5.17 932 |
. . . 4
⊢
(((∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) ↔ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ↔ ¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) |
135 | | bicom 212 |
. . . 4
⊢
((∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ↔ ¬
∃𝑘 ∈ ℤ
(𝑘 · 2) = 𝑁) ↔ (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) |
136 | 134, 135 | bitri 264 |
. . 3
⊢
(((∃𝑛 ∈
ℤ ((2 · 𝑛) +
1) = 𝑁 ∨ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁) ∧ ¬ (∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁 ∧ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁)) ↔ (¬ ∃𝑘 ∈ ℤ (𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 · 𝑛) + 1) = 𝑁)) |
137 | 92, 133, 136 | sylanblc 696 |
. 2
⊢ (𝑁 ∈ ℤ → (¬
∃𝑘 ∈ ℤ
(𝑘 · 2) = 𝑁 ↔ ∃𝑛 ∈ ℤ ((2 ·
𝑛) + 1) = 𝑁)) |
138 | 4, 137 | bitrd 268 |
1
⊢ (𝑁 ∈ ℤ → (¬ 2
∥ 𝑁 ↔
∃𝑛 ∈ ℤ ((2
· 𝑛) + 1) = 𝑁)) |