Step | Hyp | Ref
| Expression |
1 | | prmrec.3 |
. . . 4
⊢ (𝜑 → 𝑁 ∈ ℕ) |
2 | 1 | nnred 10912 |
. . 3
⊢ (𝜑 → 𝑁 ∈ ℝ) |
3 | 2 | rehalfcld 11156 |
. 2
⊢ (𝜑 → (𝑁 / 2) ∈ ℝ) |
4 | | fzfi 12633 |
. . . . . 6
⊢
(1...𝑁) ∈
Fin |
5 | | prmrec.4 |
. . . . . . 7
⊢ 𝑀 = {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} |
6 | | ssrab2 3650 |
. . . . . . 7
⊢ {𝑛 ∈ (1...𝑁) ∣ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛} ⊆ (1...𝑁) |
7 | 5, 6 | eqsstri 3598 |
. . . . . 6
⊢ 𝑀 ⊆ (1...𝑁) |
8 | | ssfi 8065 |
. . . . . 6
⊢
(((1...𝑁) ∈ Fin
∧ 𝑀 ⊆ (1...𝑁)) → 𝑀 ∈ Fin) |
9 | 4, 7, 8 | mp2an 704 |
. . . . 5
⊢ 𝑀 ∈ Fin |
10 | | hashcl 13009 |
. . . . 5
⊢ (𝑀 ∈ Fin →
(#‘𝑀) ∈
ℕ0) |
11 | 9, 10 | ax-mp 5 |
. . . 4
⊢
(#‘𝑀) ∈
ℕ0 |
12 | 11 | nn0rei 11180 |
. . 3
⊢
(#‘𝑀) ∈
ℝ |
13 | 12 | a1i 11 |
. 2
⊢ (𝜑 → (#‘𝑀) ∈ ℝ) |
14 | | 2nn 11062 |
. . . . 5
⊢ 2 ∈
ℕ |
15 | | prmrec.2 |
. . . . . 6
⊢ (𝜑 → 𝐾 ∈ ℕ) |
16 | 15 | nnnn0d 11228 |
. . . . 5
⊢ (𝜑 → 𝐾 ∈
ℕ0) |
17 | | nnexpcl 12735 |
. . . . 5
⊢ ((2
∈ ℕ ∧ 𝐾
∈ ℕ0) → (2↑𝐾) ∈ ℕ) |
18 | 14, 16, 17 | sylancr 694 |
. . . 4
⊢ (𝜑 → (2↑𝐾) ∈ ℕ) |
19 | 18 | nnred 10912 |
. . 3
⊢ (𝜑 → (2↑𝐾) ∈ ℝ) |
20 | 1 | nnrpd 11746 |
. . . . 5
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
21 | 20 | rpsqrtcld 13998 |
. . . 4
⊢ (𝜑 → (√‘𝑁) ∈
ℝ+) |
22 | 21 | rpred 11748 |
. . 3
⊢ (𝜑 → (√‘𝑁) ∈
ℝ) |
23 | 19, 22 | remulcld 9949 |
. 2
⊢ (𝜑 → ((2↑𝐾) · (√‘𝑁)) ∈ ℝ) |
24 | 2 | recnd 9947 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈ ℂ) |
25 | 24 | 2halvesd 11155 |
. . . . 5
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = 𝑁) |
26 | 7 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → 𝑀 ⊆ (1...𝑁)) |
27 | 15 | peano2nnd 10914 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐾 + 1) ∈ ℕ) |
28 | | elfzuz 12209 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ((𝐾 + 1)...𝑁) → 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) |
29 | | eluznn 11634 |
. . . . . . . . . . . . 13
⊢ (((𝐾 + 1) ∈ ℕ ∧ 𝑘 ∈
(ℤ≥‘(𝐾 + 1))) → 𝑘 ∈ ℕ) |
30 | 27, 28, 29 | syl2an 493 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ) |
31 | | eleq1 2676 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
32 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑛 ↔ 𝑘 ∥ 𝑛)) |
33 | 31, 32 | anbi12d 743 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑘 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛))) |
34 | 33 | rabbidv 3164 |
. . . . . . . . . . . . . . 15
⊢ (𝑝 = 𝑘 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
35 | | prmrec.7 |
. . . . . . . . . . . . . . 15
⊢ 𝑊 = (𝑝 ∈ ℕ ↦ {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)}) |
36 | | ovex 6577 |
. . . . . . . . . . . . . . . 16
⊢
(1...𝑁) ∈
V |
37 | 36 | rabex 4740 |
. . . . . . . . . . . . . . 15
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ∈ V |
38 | 34, 35, 37 | fvmpt 6191 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
39 | 38 | adantl 481 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
40 | | ssrab2 3650 |
. . . . . . . . . . . . 13
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ⊆ (1...𝑁) |
41 | 39, 40 | syl6eqss 3618 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
42 | 30, 41 | syldan 486 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) ⊆ (1...𝑁)) |
43 | 42 | ralrimiva 2949 |
. . . . . . . . . 10
⊢ (𝜑 → ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
44 | | iunss 4497 |
. . . . . . . . . 10
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁) ↔ ∀𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
45 | 43, 44 | sylibr 223 |
. . . . . . . . 9
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) |
46 | 26, 45 | unssd 3751 |
. . . . . . . 8
⊢ (𝜑 → (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ⊆ (1...𝑁)) |
47 | | breq1 4586 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 𝑞 → (𝑝 ∥ 𝑛 ↔ 𝑞 ∥ 𝑛)) |
48 | 47 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑞 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑛)) |
49 | 48 | cbvralv 3147 |
. . . . . . . . . . . . . . . 16
⊢
(∀𝑝 ∈
(ℙ ∖ (1...𝐾))
¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖
(1...𝐾)) ¬ 𝑞 ∥ 𝑛) |
50 | | breq2 4587 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑥 → (𝑞 ∥ 𝑛 ↔ 𝑞 ∥ 𝑥)) |
51 | 50 | notbid 307 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑥 → (¬ 𝑞 ∥ 𝑛 ↔ ¬ 𝑞 ∥ 𝑥)) |
52 | 51 | ralbidv 2969 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
53 | 49, 52 | syl5bb 271 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
54 | 53, 5 | elrab2 3333 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥)) |
55 | | elun1 3742 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ 𝑀 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
56 | 54, 55 | sylbir 224 |
. . . . . . . . . . . . 13
⊢ ((𝑥 ∈ (1...𝑁) ∧ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
57 | 56 | ex 449 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1...𝑁) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
58 | 57 | adantl 481 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
59 | | dfrex2 2979 |
. . . . . . . . . . . 12
⊢
(∃𝑞 ∈
(ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 ↔ ¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥) |
60 | | eldifn 3695 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑞 ∈ (ℙ ∖
(1...𝐾)) → ¬ 𝑞 ∈ (1...𝐾)) |
61 | 60 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ∈ (1...𝐾)) |
62 | | eldifi 3694 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑞 ∈ (ℙ ∖
(1...𝐾)) → 𝑞 ∈
ℙ) |
63 | 62 | ad2antrl 760 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℙ) |
64 | | prmnn 15226 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℕ) |
65 | 63, 64 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℕ) |
66 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ =
(ℤ≥‘1) |
67 | 65, 66 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈
(ℤ≥‘1)) |
68 | 15 | nnzd 11357 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → 𝐾 ∈ ℤ) |
69 | 68 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℤ) |
70 | | elfz5 12205 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑞 ∈
(ℤ≥‘1) ∧ 𝐾 ∈ ℤ) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾)) |
71 | 67, 69, 70 | syl2anc 691 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ (1...𝐾) ↔ 𝑞 ≤ 𝐾)) |
72 | 61, 71 | mtbid 313 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → ¬ 𝑞 ≤ 𝐾) |
73 | 15 | nnred 10912 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝜑 → 𝐾 ∈ ℝ) |
74 | 73 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 ∈ ℝ) |
75 | 65 | nnred 10912 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℝ) |
76 | 74, 75 | ltnled 10063 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ ¬ 𝑞 ≤ 𝐾)) |
77 | 72, 76 | mpbird 246 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝐾 < 𝑞) |
78 | | prmz 15227 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑞 ∈ ℙ → 𝑞 ∈
ℤ) |
79 | 63, 78 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ℤ) |
80 | | zltp1le 11304 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝐾 ∈ ℤ ∧ 𝑞 ∈ ℤ) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞)) |
81 | 69, 79, 80 | syl2anc 691 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 < 𝑞 ↔ (𝐾 + 1) ≤ 𝑞)) |
82 | 77, 81 | mpbid 221 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ≤ 𝑞) |
83 | | elfznn 12241 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ∈ ℕ) |
84 | 83 | ad2antlr 759 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℕ) |
85 | 84 | nnred 10912 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ℝ) |
86 | 2 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℝ) |
87 | | simprr 792 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∥ 𝑥) |
88 | | dvdsle 14870 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑞 ∈ ℤ ∧ 𝑥 ∈ ℕ) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
89 | 79, 84, 88 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∥ 𝑥 → 𝑞 ≤ 𝑥)) |
90 | 87, 89 | mpd 15 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑥) |
91 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ (1...𝑁) → 𝑥 ≤ 𝑁) |
92 | 91 | ad2antlr 759 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ≤ 𝑁) |
93 | 75, 85, 86, 90, 92 | letrd 10073 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ≤ 𝑁) |
94 | 68 | peano2zd 11361 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → (𝐾 + 1) ∈ ℤ) |
95 | 94 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝐾 + 1) ∈ ℤ) |
96 | 1 | nnzd 11357 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → 𝑁 ∈ ℤ) |
97 | 96 | ad2antrr 758 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑁 ∈ ℤ) |
98 | | elfz 12203 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑞 ∈ ℤ ∧ (𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞 ∧ 𝑞 ≤ 𝑁))) |
99 | 79, 95, 97, 98 | syl3anc 1318 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ ((𝐾 + 1)...𝑁) ↔ ((𝐾 + 1) ≤ 𝑞 ∧ 𝑞 ≤ 𝑁))) |
100 | 82, 93, 99 | mpbir2and 959 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑞 ∈ ((𝐾 + 1)...𝑁)) |
101 | | simplr 788 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (1...𝑁)) |
102 | 63, 87 | jca 553 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥)) |
103 | 50 | anbi2d 736 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑥 → ((𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥))) |
104 | 103 | elrab 3331 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑥))) |
105 | 101, 102,
104 | sylanbrc 695 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
106 | | eleq1 2676 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑝 = 𝑞 → (𝑝 ∈ ℙ ↔ 𝑞 ∈ ℙ)) |
107 | 106, 47 | anbi12d 743 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑝 = 𝑞 → ((𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛) ↔ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛))) |
108 | 107 | rabbidv 3164 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑝 = 𝑞 → {𝑛 ∈ (1...𝑁) ∣ (𝑝 ∈ ℙ ∧ 𝑝 ∥ 𝑛)} = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
109 | 36 | rabex 4740 |
. . . . . . . . . . . . . . . . . 18
⊢ {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)} ∈ V |
110 | 108, 35, 109 | fvmpt 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑞 ∈ ℕ → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
111 | 65, 110 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → (𝑊‘𝑞) = {𝑛 ∈ (1...𝑁) ∣ (𝑞 ∈ ℙ ∧ 𝑞 ∥ 𝑛)}) |
112 | 105, 111 | eleqtrrd 2691 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑊‘𝑞)) |
113 | | fveq2 6103 |
. . . . . . . . . . . . . . . 16
⊢ (𝑘 = 𝑞 → (𝑊‘𝑘) = (𝑊‘𝑞)) |
114 | 113 | eliuni 4462 |
. . . . . . . . . . . . . . 15
⊢ ((𝑞 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑥 ∈ (𝑊‘𝑞)) → 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
115 | 100, 112,
114 | syl2anc 691 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
116 | | elun2 3743 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
117 | 115, 116 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1...𝑁)) ∧ (𝑞 ∈ (ℙ ∖ (1...𝐾)) ∧ 𝑞 ∥ 𝑥)) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
118 | 117 | rexlimdvaa 3014 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (∃𝑞 ∈ (ℙ ∖ (1...𝐾))𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
119 | 59, 118 | syl5bir 232 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → (¬ ∀𝑞 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑞 ∥ 𝑥 → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
120 | 58, 119 | pm2.61d 169 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1...𝑁)) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
121 | 120 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ (1...𝑁) → 𝑥 ∈ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
122 | 121 | ssrdv 3574 |
. . . . . . . 8
⊢ (𝜑 → (1...𝑁) ⊆ (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
123 | 46, 122 | eqssd 3585 |
. . . . . . 7
⊢ (𝜑 → (𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (1...𝑁)) |
124 | 123 | fveq2d 6107 |
. . . . . 6
⊢ (𝜑 → (#‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = (#‘(1...𝑁))) |
125 | 1 | nnnn0d 11228 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈
ℕ0) |
126 | | hashfz1 12996 |
. . . . . . 7
⊢ (𝑁 ∈ ℕ0
→ (#‘(1...𝑁)) =
𝑁) |
127 | 125, 126 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘(1...𝑁)) = 𝑁) |
128 | 124, 127 | eqtr2d 2645 |
. . . . 5
⊢ (𝜑 → 𝑁 = (#‘(𝑀 ∪ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
129 | 9 | a1i 11 |
. . . . . 6
⊢ (𝜑 → 𝑀 ∈ Fin) |
130 | | ssfi 8065 |
. . . . . . 7
⊢
(((1...𝑁) ∈ Fin
∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ⊆ (1...𝑁)) → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin) |
131 | 4, 45, 130 | sylancr 694 |
. . . . . 6
⊢ (𝜑 → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin) |
132 | | breq1 4586 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑝 = 𝑘 → (𝑝 ∥ 𝑥 ↔ 𝑘 ∥ 𝑥)) |
133 | 132 | notbid 307 |
. . . . . . . . . . . . . . . 16
⊢ (𝑝 = 𝑘 → (¬ 𝑝 ∥ 𝑥 ↔ ¬ 𝑘 ∥ 𝑥)) |
134 | | breq2 4587 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 = 𝑥 → (𝑝 ∥ 𝑛 ↔ 𝑝 ∥ 𝑥)) |
135 | 134 | notbid 307 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑛 = 𝑥 → (¬ 𝑝 ∥ 𝑛 ↔ ¬ 𝑝 ∥ 𝑥)) |
136 | 135 | ralbidv 2969 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑥 → (∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑛 ↔ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)) |
137 | 136, 5 | elrab2 3333 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑥 ∈ 𝑀 ↔ (𝑥 ∈ (1...𝑁) ∧ ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥)) |
138 | 137 | simprbi 479 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑥 ∈ 𝑀 → ∀𝑝 ∈ (ℙ ∖ (1...𝐾)) ¬ 𝑝 ∥ 𝑥) |
139 | 138 | ad2antlr 759 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ∀𝑝 ∈ (ℙ ∖
(1...𝐾)) ¬ 𝑝 ∥ 𝑥) |
140 | | simprr 792 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ℙ) |
141 | | noel 3878 |
. . . . . . . . . . . . . . . . . 18
⊢ ¬
𝑘 ∈
∅ |
142 | | simprl 790 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ ((𝐾 + 1)...𝑁)) |
143 | 142 | biantrud 527 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)))) |
144 | | elin 3758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁))) |
145 | 143, 144 | syl6bbr 277 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)))) |
146 | 73 | ltp1d 10833 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝜑 → 𝐾 < (𝐾 + 1)) |
147 | | fzdisj 12239 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝐾 < (𝐾 + 1) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
148 | 146, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝜑 → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
149 | 148 | ad2antrr 758 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) = ∅) |
150 | 149 | eleq2d 2673 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ ((1...𝐾) ∩ ((𝐾 + 1)...𝑁)) ↔ 𝑘 ∈ ∅)) |
151 | 145, 150 | bitrd 267 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → (𝑘 ∈ (1...𝐾) ↔ 𝑘 ∈ ∅)) |
152 | 141, 151 | mtbiri 316 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∈ (1...𝐾)) |
153 | 140, 152 | eldifd 3551 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → 𝑘 ∈ (ℙ ∖ (1...𝐾))) |
154 | 133, 139,
153 | rspcdva 3288 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ (𝑘 ∈ ((𝐾 + 1)...𝑁) ∧ 𝑘 ∈ ℙ)) → ¬ 𝑘 ∥ 𝑥) |
155 | 154 | expr 641 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑘 ∈ ℙ → ¬ 𝑘 ∥ 𝑥)) |
156 | | imnan 437 |
. . . . . . . . . . . . . 14
⊢ ((𝑘 ∈ ℙ → ¬
𝑘 ∥ 𝑥) ↔ ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
157 | 155, 156 | sylib 207 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
158 | 30 | adantlr 747 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → 𝑘 ∈ ℕ) |
159 | 158, 38 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑊‘𝑘) = {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)}) |
160 | 159 | eleq2d 2673 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) ↔ 𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)})) |
161 | | breq2 4587 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑥 → (𝑘 ∥ 𝑛 ↔ 𝑘 ∥ 𝑥)) |
162 | 161 | anbi2d 736 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑥 → ((𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛) ↔ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
163 | 162 | elrab 3331 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} ↔ (𝑥 ∈ (1...𝑁) ∧ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
164 | 163 | simprbi 479 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ {𝑛 ∈ (1...𝑁) ∣ (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑛)} → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥)) |
165 | 160, 164 | syl6bi 242 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → (𝑥 ∈ (𝑊‘𝑘) → (𝑘 ∈ ℙ ∧ 𝑘 ∥ 𝑥))) |
166 | 157, 165 | mtod 188 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ 𝑀) ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → ¬ 𝑥 ∈ (𝑊‘𝑘)) |
167 | 166 | nrexdv 2984 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘)) |
168 | | eliun 4460 |
. . . . . . . . . . 11
⊢ (𝑥 ∈ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ↔ ∃𝑘 ∈ ((𝐾 + 1)...𝑁)𝑥 ∈ (𝑊‘𝑘)) |
169 | 167, 168 | sylnibr 318 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ 𝑀) → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) |
170 | 169 | ex 449 |
. . . . . . . . 9
⊢ (𝜑 → (𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
171 | | imnan 437 |
. . . . . . . . 9
⊢ ((𝑥 ∈ 𝑀 → ¬ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
172 | 170, 171 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → ¬ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
173 | | elin 3758 |
. . . . . . . 8
⊢ (𝑥 ∈ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ↔ (𝑥 ∈ 𝑀 ∧ 𝑥 ∈ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
174 | 172, 173 | sylnibr 318 |
. . . . . . 7
⊢ (𝜑 → ¬ 𝑥 ∈ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) |
175 | 174 | eq0rdv 3931 |
. . . . . 6
⊢ (𝜑 → (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) |
176 | | hashun 13032 |
. . . . . 6
⊢ ((𝑀 ∈ Fin ∧ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin ∧ (𝑀 ∩ ∪
𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = ∅) → (#‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((#‘𝑀) + (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
177 | 129, 131,
175, 176 | syl3anc 1318 |
. . . . 5
⊢ (𝜑 → (#‘(𝑀 ∪ ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) = ((#‘𝑀) + (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
178 | 25, 128, 177 | 3eqtrd 2648 |
. . . 4
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) = ((#‘𝑀) + (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)))) |
179 | | hashcl 13009 |
. . . . . . 7
⊢ (∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) ∈ Fin → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈
ℕ0) |
180 | 131, 179 | syl 17 |
. . . . . 6
⊢ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈
ℕ0) |
181 | 180 | nn0red 11229 |
. . . . 5
⊢ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ∈ ℝ) |
182 | | fzfid 12634 |
. . . . . . . 8
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ∈ Fin) |
183 | 27, 29 | sylan 487 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 𝑘 ∈
ℕ) |
184 | | nnrecre 10934 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ) |
185 | | 0re 9919 |
. . . . . . . . . . 11
⊢ 0 ∈
ℝ |
186 | | ifcl 4080 |
. . . . . . . . . . 11
⊢ (((1 /
𝑘) ∈ ℝ ∧ 0
∈ ℝ) → if(𝑘
∈ ℙ, (1 / 𝑘), 0)
∈ ℝ) |
187 | 184, 185,
186 | sylancl 693 |
. . . . . . . . . 10
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) |
188 | 183, 187 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℝ) |
189 | 28, 188 | sylan2 490 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑘 ∈ ((𝐾 + 1)...𝑁)) → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
190 | 182, 189 | fsumrecl 14312 |
. . . . . . 7
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
191 | 2, 190 | remulcld 9949 |
. . . . . 6
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ∈ ℝ) |
192 | | prmrec.1 |
. . . . . . . 8
⊢ 𝐹 = (𝑛 ∈ ℕ ↦ if(𝑛 ∈ ℙ, (1 / 𝑛), 0)) |
193 | | prmrec.5 |
. . . . . . . 8
⊢ (𝜑 → seq1( + , 𝐹) ∈ dom ⇝
) |
194 | | prmrec.6 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2)) |
195 | 192, 15, 1, 5, 193, 194, 35 | prmreclem4 15461 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
196 | | eluz 11577 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℤ ∧ 𝐾 ∈ ℤ) → (𝐾 ∈
(ℤ≥‘𝑁) ↔ 𝑁 ≤ 𝐾)) |
197 | 96, 68, 196 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) ↔ 𝑁 ≤ 𝐾)) |
198 | | nnleltp1 11309 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℕ ∧ 𝐾 ∈ ℕ) → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1))) |
199 | 1, 15, 198 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 ≤ 𝐾 ↔ 𝑁 < (𝐾 + 1))) |
200 | | fzn 12228 |
. . . . . . . . . 10
⊢ (((𝐾 + 1) ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
201 | 94, 96, 200 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁 < (𝐾 + 1) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
202 | 197, 199,
201 | 3bitrd 293 |
. . . . . . . 8
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) ↔ ((𝐾 + 1)...𝑁) = ∅)) |
203 | | 0le0 10987 |
. . . . . . . . . 10
⊢ 0 ≤
0 |
204 | 24 | mul01d 10114 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁 · 0) = 0) |
205 | 203, 204 | syl5breqr 4621 |
. . . . . . . . 9
⊢ (𝜑 → 0 ≤ (𝑁 · 0)) |
206 | | iuneq1 4470 |
. . . . . . . . . . . . 13
⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∪ 𝑘 ∈ ∅ (𝑊‘𝑘)) |
207 | | 0iun 4513 |
. . . . . . . . . . . . 13
⊢ ∪ 𝑘 ∈ ∅ (𝑊‘𝑘) = ∅ |
208 | 206, 207 | syl6eq 2660 |
. . . . . . . . . . . 12
⊢ (((𝐾 + 1)...𝑁) = ∅ → ∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘) = ∅) |
209 | 208 | fveq2d 6107 |
. . . . . . . . . . 11
⊢ (((𝐾 + 1)...𝑁) = ∅ → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = (#‘∅)) |
210 | | hash0 13019 |
. . . . . . . . . . 11
⊢
(#‘∅) = 0 |
211 | 209, 210 | syl6eq 2660 |
. . . . . . . . . 10
⊢ (((𝐾 + 1)...𝑁) = ∅ → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) = 0) |
212 | | sumeq1 14267 |
. . . . . . . . . . . 12
⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = Σ𝑘 ∈ ∅ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
213 | | sum0 14299 |
. . . . . . . . . . . 12
⊢
Σ𝑘 ∈
∅ if(𝑘 ∈
ℙ, (1 / 𝑘), 0) =
0 |
214 | 212, 213 | syl6eq 2660 |
. . . . . . . . . . 11
⊢ (((𝐾 + 1)...𝑁) = ∅ → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) = 0) |
215 | 214 | oveq2d 6565 |
. . . . . . . . . 10
⊢ (((𝐾 + 1)...𝑁) = ∅ → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) = (𝑁 · 0)) |
216 | 211, 215 | breq12d 4596 |
. . . . . . . . 9
⊢ (((𝐾 + 1)...𝑁) = ∅ → ((#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) ↔ 0 ≤ (𝑁 · 0))) |
217 | 205, 216 | syl5ibrcom 236 |
. . . . . . . 8
⊢ (𝜑 → (((𝐾 + 1)...𝑁) = ∅ → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
218 | 202, 217 | sylbid 229 |
. . . . . . 7
⊢ (𝜑 → (𝐾 ∈ (ℤ≥‘𝑁) → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)))) |
219 | | uztric 11585 |
. . . . . . . 8
⊢ ((𝐾 ∈ ℤ ∧ 𝑁 ∈ ℤ) → (𝑁 ∈
(ℤ≥‘𝐾) ∨ 𝐾 ∈ (ℤ≥‘𝑁))) |
220 | 68, 96, 219 | syl2anc 691 |
. . . . . . 7
⊢ (𝜑 → (𝑁 ∈ (ℤ≥‘𝐾) ∨ 𝐾 ∈ (ℤ≥‘𝑁))) |
221 | 195, 218,
220 | mpjaod 395 |
. . . . . 6
⊢ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) ≤ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
222 | | eqid 2610 |
. . . . . . . . . 10
⊢
(ℤ≥‘(𝐾 + 1)) =
(ℤ≥‘(𝐾 + 1)) |
223 | | eleq1 2676 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (𝑛 ∈ ℙ ↔ 𝑘 ∈ ℙ)) |
224 | | oveq2 6557 |
. . . . . . . . . . . . 13
⊢ (𝑛 = 𝑘 → (1 / 𝑛) = (1 / 𝑘)) |
225 | 223, 224 | ifbieq1d 4059 |
. . . . . . . . . . . 12
⊢ (𝑛 = 𝑘 → if(𝑛 ∈ ℙ, (1 / 𝑛), 0) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
226 | | ovex 6577 |
. . . . . . . . . . . . 13
⊢ (1 /
𝑘) ∈
V |
227 | | c0ex 9913 |
. . . . . . . . . . . . 13
⊢ 0 ∈
V |
228 | 226, 227 | ifex 4106 |
. . . . . . . . . . . 12
⊢ if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ V |
229 | 225, 192,
228 | fvmpt 6191 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
230 | 183, 229 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → (𝐹‘𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
231 | 187 | recnd 9947 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈
ℂ) |
232 | 229, 231 | eqeltrd 2688 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (𝐹‘𝑘) ∈ ℂ) |
233 | 232 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑘 ∈ ℕ) → (𝐹‘𝑘) ∈ ℂ) |
234 | 66, 27, 233 | iserex 14235 |
. . . . . . . . . . 11
⊢ (𝜑 → (seq1( + , 𝐹) ∈ dom ⇝ ↔
seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝
)) |
235 | 193, 234 | mpbid 221 |
. . . . . . . . . 10
⊢ (𝜑 → seq(𝐾 + 1)( + , 𝐹) ∈ dom ⇝ ) |
236 | 222, 94, 230, 188, 235 | isumrecl 14338 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ) |
237 | | halfre 11123 |
. . . . . . . . . 10
⊢ (1 / 2)
∈ ℝ |
238 | 237 | a1i 11 |
. . . . . . . . 9
⊢ (𝜑 → (1 / 2) ∈
ℝ) |
239 | | fzssuz 12253 |
. . . . . . . . . . 11
⊢ ((𝐾 + 1)...𝑁) ⊆
(ℤ≥‘(𝐾 + 1)) |
240 | 239 | a1i 11 |
. . . . . . . . . 10
⊢ (𝜑 → ((𝐾 + 1)...𝑁) ⊆
(ℤ≥‘(𝐾 + 1))) |
241 | | nnrp 11718 |
. . . . . . . . . . . . . 14
⊢ (𝑘 ∈ ℕ → 𝑘 ∈
ℝ+) |
242 | 241 | rpreccld 11758 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ ℕ → (1 /
𝑘) ∈
ℝ+) |
243 | 242 | rpge0d 11752 |
. . . . . . . . . . . 12
⊢ (𝑘 ∈ ℕ → 0 ≤ (1
/ 𝑘)) |
244 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ ((1 /
𝑘) = if(𝑘 ∈ ℙ, (1 / 𝑘), 0) → (0 ≤ (1 / 𝑘) ↔ 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0))) |
245 | | breq2 4587 |
. . . . . . . . . . . . 13
⊢ (0 =
if(𝑘 ∈ ℙ, (1 /
𝑘), 0) → (0 ≤ 0
↔ 0 ≤ if(𝑘 ∈
ℙ, (1 / 𝑘),
0))) |
246 | 244, 245 | ifboth 4074 |
. . . . . . . . . . . 12
⊢ ((0 ≤
(1 / 𝑘) ∧ 0 ≤ 0)
→ 0 ≤ if(𝑘 ∈
ℙ, (1 / 𝑘),
0)) |
247 | 243, 203,
246 | sylancl 693 |
. . . . . . . . . . 11
⊢ (𝑘 ∈ ℕ → 0 ≤
if(𝑘 ∈ ℙ, (1 /
𝑘), 0)) |
248 | 183, 247 | syl 17 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑘 ∈ (ℤ≥‘(𝐾 + 1))) → 0 ≤ if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
249 | 222, 94, 182, 240, 230, 188, 248, 235 | isumless 14416 |
. . . . . . . . 9
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ≤ Σ𝑘 ∈ (ℤ≥‘(𝐾 + 1))if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) |
250 | 190, 236,
238, 249, 194 | lelttrd 10074 |
. . . . . . . 8
⊢ (𝜑 → Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2)) |
251 | 1 | nngt0d 10941 |
. . . . . . . . 9
⊢ (𝜑 → 0 < 𝑁) |
252 | | ltmul2 10753 |
. . . . . . . . 9
⊢
((Σ𝑘 ∈
((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) ∈ ℝ ∧ (1 / 2) ∈
ℝ ∧ (𝑁 ∈
ℝ ∧ 0 < 𝑁))
→ (Σ𝑘 ∈
((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))) |
253 | 190, 238,
2, 251, 252 | syl112anc 1322 |
. . . . . . . 8
⊢ (𝜑 → (Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0) < (1 / 2) ↔ (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2)))) |
254 | 250, 253 | mpbid 221 |
. . . . . . 7
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 · (1 / 2))) |
255 | | 2cn 10968 |
. . . . . . . . 9
⊢ 2 ∈
ℂ |
256 | | 2ne0 10990 |
. . . . . . . . 9
⊢ 2 ≠
0 |
257 | | divrec 10580 |
. . . . . . . . 9
⊢ ((𝑁 ∈ ℂ ∧ 2 ∈
ℂ ∧ 2 ≠ 0) → (𝑁 / 2) = (𝑁 · (1 / 2))) |
258 | 255, 256,
257 | mp3an23 1408 |
. . . . . . . 8
⊢ (𝑁 ∈ ℂ → (𝑁 / 2) = (𝑁 · (1 / 2))) |
259 | 24, 258 | syl 17 |
. . . . . . 7
⊢ (𝜑 → (𝑁 / 2) = (𝑁 · (1 / 2))) |
260 | 254, 259 | breqtrrd 4611 |
. . . . . 6
⊢ (𝜑 → (𝑁 · Σ𝑘 ∈ ((𝐾 + 1)...𝑁)if(𝑘 ∈ ℙ, (1 / 𝑘), 0)) < (𝑁 / 2)) |
261 | 181, 191,
3, 221, 260 | lelttrd 10074 |
. . . . 5
⊢ (𝜑 → (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘)) < (𝑁 / 2)) |
262 | 181, 3, 13, 261 | ltadd2dd 10075 |
. . . 4
⊢ (𝜑 → ((#‘𝑀) + (#‘∪ 𝑘 ∈ ((𝐾 + 1)...𝑁)(𝑊‘𝑘))) < ((#‘𝑀) + (𝑁 / 2))) |
263 | 178, 262 | eqbrtrd 4605 |
. . 3
⊢ (𝜑 → ((𝑁 / 2) + (𝑁 / 2)) < ((#‘𝑀) + (𝑁 / 2))) |
264 | 3, 13, 3 | ltadd1d 10499 |
. . 3
⊢ (𝜑 → ((𝑁 / 2) < (#‘𝑀) ↔ ((𝑁 / 2) + (𝑁 / 2)) < ((#‘𝑀) + (𝑁 / 2)))) |
265 | 263, 264 | mpbird 246 |
. 2
⊢ (𝜑 → (𝑁 / 2) < (#‘𝑀)) |
266 | | oveq1 6556 |
. . . . . . . 8
⊢ (𝑘 = 𝑟 → (𝑘↑2) = (𝑟↑2)) |
267 | 266 | breq1d 4593 |
. . . . . . 7
⊢ (𝑘 = 𝑟 → ((𝑘↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑥)) |
268 | 267 | cbvrabv 3172 |
. . . . . 6
⊢ {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} |
269 | | breq2 4587 |
. . . . . . 7
⊢ (𝑥 = 𝑛 → ((𝑟↑2) ∥ 𝑥 ↔ (𝑟↑2) ∥ 𝑛)) |
270 | 269 | rabbidv 3164 |
. . . . . 6
⊢ (𝑥 = 𝑛 → {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}) |
271 | 268, 270 | syl5eq 2656 |
. . . . 5
⊢ (𝑥 = 𝑛 → {𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥} = {𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}) |
272 | 271 | supeq1d 8235 |
. . . 4
⊢ (𝑥 = 𝑛 → sup({𝑘 ∈ ℕ ∣ (𝑘↑2) ∥ 𝑥}, ℝ, < ) = sup({𝑟 ∈ ℕ ∣ (𝑟↑2) ∥ 𝑛}, ℝ, < )) |
273 | 272 | cbvmptv 4678 |
. . 3
⊢ (𝑥 ∈ ℕ ↦
sup({𝑘 ∈ ℕ
∣ (𝑘↑2) ∥
𝑥}, ℝ, < )) =
(𝑛 ∈ ℕ ↦
sup({𝑟 ∈ ℕ
∣ (𝑟↑2) ∥
𝑛}, ℝ, <
)) |
274 | 192, 15, 1, 5, 273 | prmreclem3 15460 |
. 2
⊢ (𝜑 → (#‘𝑀) ≤ ((2↑𝐾) · (√‘𝑁))) |
275 | 3, 13, 23, 265, 274 | ltletrd 10076 |
1
⊢ (𝜑 → (𝑁 / 2) < ((2↑𝐾) · (√‘𝑁))) |