| Step | Hyp | Ref
| Expression |
| 1 | | 4nn 12349 |
. . . . . 6
⊢ 4 ∈
ℕ |
| 2 | | eluznn 12960 |
. . . . . . . 8
⊢ ((4
∈ ℕ ∧ 𝑁
∈ (ℤ≥‘4)) → 𝑁 ∈ ℕ) |
| 3 | 1, 2 | mpan 690 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈ ℕ) |
| 4 | 3 | nnnn0d 12587 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈
ℕ0) |
| 5 | | nnexpcl 14115 |
. . . . . 6
⊢ ((4
∈ ℕ ∧ 𝑁
∈ ℕ0) → (4↑𝑁) ∈ ℕ) |
| 6 | 1, 4, 5 | sylancr 587 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (4↑𝑁) ∈ ℕ) |
| 7 | 6 | nnrpd 13075 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (4↑𝑁) ∈
ℝ+) |
| 8 | 3 | nnrpd 13075 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈
ℝ+) |
| 9 | 7, 8 | rpdivcld 13094 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((4↑𝑁) / 𝑁) ∈
ℝ+) |
| 10 | 9 | relogcld 26665 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) ∈ ℝ) |
| 11 | | fzctr 13680 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...(2
· 𝑁))) |
| 12 | 4, 11 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈ (0...(2 · 𝑁))) |
| 13 | | bccl2 14362 |
. . . . 5
⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ) |
| 14 | 12, 13 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℕ) |
| 15 | 14 | nnrpd 13075 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈
ℝ+) |
| 16 | 15 | relogcld 26665 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ∈ ℝ) |
| 17 | | 2z 12649 |
. . . . . . 7
⊢ 2 ∈
ℤ |
| 18 | | eluzelz 12888 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈ ℤ) |
| 19 | | zmulcl 12666 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 · 𝑁) ∈ ℤ) |
| 20 | 17, 18, 19 | sylancr 587 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 𝑁) ∈ ℤ) |
| 21 | 20 | zred 12722 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 𝑁) ∈ ℝ) |
| 22 | | ppicl 27174 |
. . . . 5
⊢ ((2
· 𝑁) ∈ ℝ
→ (π‘(2 · 𝑁)) ∈
ℕ0) |
| 23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘(2 · 𝑁)) ∈
ℕ0) |
| 24 | 23 | nn0red 12588 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘(2 · 𝑁)) ∈
ℝ) |
| 25 | | 2nn 12339 |
. . . . . 6
⊢ 2 ∈
ℕ |
| 26 | | nnmulcl 12290 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
| 27 | 25, 3, 26 | sylancr 587 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 𝑁) ∈ ℕ) |
| 28 | 27 | nnrpd 13075 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 𝑁) ∈
ℝ+) |
| 29 | 28 | relogcld 26665 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘(2 · 𝑁)) ∈
ℝ) |
| 30 | 24, 29 | remulcld 11291 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘(2 · 𝑁)) · (log‘(2
· 𝑁))) ∈
ℝ) |
| 31 | | bclbnd 27324 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) |
| 32 | | logltb 26642 |
. . . 4
⊢
((((4↑𝑁) /
𝑁) ∈
ℝ+ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ+) →
(((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁) ↔ (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁)))) |
| 33 | 9, 15, 32 | syl2anc 584 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → (((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁) ↔ (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁)))) |
| 34 | 31, 33 | mpbid 232 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁))) |
| 35 | | chebbnd1lem1.1 |
. . . . . . . 8
⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) |
| 36 | 27, 14 | ifcld 4572 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ∈ ℕ) |
| 37 | 35, 36 | eqeltrid 2845 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ∈ ℕ) |
| 38 | 37 | nnred 12281 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ∈ ℝ) |
| 39 | | ppicl 27174 |
. . . . . 6
⊢ (𝐾 ∈ ℝ →
(π‘𝐾)
∈ ℕ0) |
| 40 | 38, 39 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘𝐾) ∈
ℕ0) |
| 41 | 40 | nn0red 12588 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘𝐾) ∈ ℝ) |
| 42 | 41, 29 | remulcld 11291 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ∈
ℝ) |
| 43 | | fzfid 14014 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → (1...𝐾) ∈ Fin) |
| 44 | | inss1 4237 |
. . . . . 6
⊢
((1...𝐾) ∩
ℙ) ⊆ (1...𝐾) |
| 45 | | ssfi 9213 |
. . . . . 6
⊢
(((1...𝐾) ∈ Fin
∧ ((1...𝐾) ∩
ℙ) ⊆ (1...𝐾))
→ ((1...𝐾) ∩
ℙ) ∈ Fin) |
| 46 | 43, 44, 45 | sylancl 586 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → ((1...𝐾) ∩ ℙ) ∈
Fin) |
| 47 | 37 | nnzd 12640 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ∈ ℤ) |
| 48 | 14 | nnzd 12640 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℤ) |
| 49 | 14 | nnred 12281 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℝ) |
| 50 | | min2 13232 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑁) ∈ ℝ
∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → if((2
· 𝑁) ≤ ((2
· 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ ((2 · 𝑁)C𝑁)) |
| 51 | 21, 49, 50 | syl2anc 584 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ ((2 · 𝑁)C𝑁)) |
| 52 | 35, 51 | eqbrtrid 5178 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ≤ ((2 · 𝑁)C𝑁)) |
| 53 | | eluz2 12884 |
. . . . . . . . . 10
⊢ (((2
· 𝑁)C𝑁) ∈
(ℤ≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ ((2 · 𝑁)C𝑁) ∈ ℤ ∧ 𝐾 ≤ ((2 · 𝑁)C𝑁))) |
| 54 | 47, 48, 52, 53 | syl3anbrc 1344 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ (ℤ≥‘𝐾)) |
| 55 | | fzss2 13604 |
. . . . . . . . 9
⊢ (((2
· 𝑁)C𝑁) ∈
(ℤ≥‘𝐾) → (1...𝐾) ⊆ (1...((2 · 𝑁)C𝑁))) |
| 56 | 54, 55 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘4) → (1...𝐾) ⊆ (1...((2 · 𝑁)C𝑁))) |
| 57 | 56 | ssrind 4244 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → ((1...𝐾) ∩ ℙ) ⊆ ((1...((2 ·
𝑁)C𝑁)) ∩ ℙ)) |
| 58 | 57 | sselda 3983 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) |
| 59 | | simpr 484 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) |
| 60 | 59 | elin1d 4204 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁))) |
| 61 | | elfznn 13593 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ∈ ℕ) |
| 62 | 60, 61 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℕ) |
| 63 | 59 | elin2d 4205 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℙ) |
| 64 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → ((2 · 𝑁)C𝑁) ∈ ℕ) |
| 65 | 63, 64 | pccld 16888 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
| 66 | 62, 65 | nnexpcld 14284 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ) |
| 67 | 66 | nnrpd 13075 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈
ℝ+) |
| 68 | 67 | relogcld 26665 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ) |
| 69 | 58, 68 | syldan 591 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ) |
| 70 | 29 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(2
· 𝑁)) ∈
ℝ) |
| 71 | | elinel2 4202 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝐾) ∩ ℙ) → 𝑘 ∈ ℙ) |
| 72 | | bposlem1 27328 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℙ) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
| 73 | 3, 71, 72 | syl2an 596 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
| 74 | 58, 67 | syldan 591 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈
ℝ+) |
| 75 | 74 | reeflogd 26666 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) →
(exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) = (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) |
| 76 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (2 · 𝑁) ∈
ℝ+) |
| 77 | 76 | reeflogd 26666 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) →
(exp‘(log‘(2 · 𝑁))) = (2 · 𝑁)) |
| 78 | 73, 75, 77 | 3brtr4d 5175 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) →
(exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 ·
𝑁)))) |
| 79 | | efle 16154 |
. . . . . . 7
⊢
(((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ ∧ (log‘(2
· 𝑁)) ∈
ℝ) → ((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁)) ↔
(exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 ·
𝑁))))) |
| 80 | 69, 70, 79 | syl2anc 584 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → ((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁)) ↔
(exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 ·
𝑁))))) |
| 81 | 78, 80 | mpbird 257 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁))) |
| 82 | 46, 69, 70, 81 | fsumle 15835 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁))) |
| 83 | 68 | recnd 11289 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ) |
| 84 | 58, 83 | syldan 591 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ) |
| 85 | | eldifn 4132 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (((1...((2 ·
𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) → ¬
𝑘 ∈ ((1...𝐾) ∩
ℙ)) |
| 86 | 85 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬
𝑘 ∈ ((1...𝐾) ∩
ℙ)) |
| 87 | | simpr 484 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ (((1...((2 ·
𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩
ℙ))) |
| 88 | 87 | eldifad 3963 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) |
| 89 | 88 | elin1d 4204 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁))) |
| 90 | 89, 61 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈
ℕ) |
| 91 | 90 | adantrr 717 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈
ℕ) |
| 92 | 91 | nnred 12281 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈
ℝ) |
| 93 | 88, 66 | syldan 591 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ) |
| 94 | 93 | nnred 12281 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ) |
| 95 | 94 | adantrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ) |
| 96 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (2 · 𝑁) ∈
ℝ) |
| 97 | 91 | nncnd 12282 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈
ℂ) |
| 98 | 97 | exp1d 14181 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) = 𝑘) |
| 99 | 91 | nnge1d 12314 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 1 ≤ 𝑘) |
| 100 | | simprr 773 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ) |
| 101 | | nnuz 12921 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ =
(ℤ≥‘1) |
| 102 | 100, 101 | eleqtrdi 2851 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈
(ℤ≥‘1)) |
| 103 | 92, 99, 102 | leexp2ad 14293 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) ≤ (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) |
| 104 | 98, 103 | eqbrtrrd 5167 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) |
| 105 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑁 ∈ ℕ) |
| 106 | 88 | elin2d 4205 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈
ℙ) |
| 107 | 106 | adantrr 717 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈
ℙ) |
| 108 | 105, 107,
72 | syl2anc 584 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
| 109 | 92, 95, 96, 104, 108 | letrd 11418 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (2 · 𝑁)) |
| 110 | | elfzle2 13568 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ≤ ((2 · 𝑁)C𝑁)) |
| 111 | 89, 110 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ≤ ((2 · 𝑁)C𝑁)) |
| 112 | 111 | adantrr 717 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ ((2 · 𝑁)C𝑁)) |
| 113 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → ((2 ·
𝑁)C𝑁) ∈ ℝ) |
| 114 | | lemin 13234 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℝ ∧ (2
· 𝑁) ∈ ℝ
∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁)))) |
| 115 | 92, 96, 113, 114 | syl3anc 1373 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁)))) |
| 116 | 109, 112,
115 | mpbir2and 713 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁))) |
| 117 | 116, 35 | breqtrrdi 5185 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ 𝐾) |
| 118 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℕ) |
| 119 | 118 | nnzd 12640 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℤ) |
| 120 | | fznn 13632 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℤ → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾))) |
| 121 | 119, 120 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾))) |
| 122 | 91, 117, 121 | mpbir2and 713 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ (1...𝐾)) |
| 123 | 122, 107 | elind 4200 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ((1...𝐾) ∩ ℙ)) |
| 124 | 123 | expr 456 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) →
((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ → 𝑘 ∈ ((1...𝐾) ∩ ℙ))) |
| 125 | 86, 124 | mtod 198 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬
(𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ) |
| 126 | 88, 65 | syldan 591 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
| 127 | | elnn0 12528 |
. . . . . . . . . . . . 13
⊢ ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0 ↔ ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ ∨ (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0)) |
| 128 | 126, 127 | sylib 218 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) →
((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ ∨ (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0)) |
| 129 | 128 | ord 865 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (¬
(𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ → (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0)) |
| 130 | 125, 129 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0) |
| 131 | 130 | oveq2d 7447 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = (𝑘↑0)) |
| 132 | 90 | nncnd 12282 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈
ℂ) |
| 133 | 132 | exp0d 14180 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑0) = 1) |
| 134 | 131, 133 | eqtrd 2777 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = 1) |
| 135 | 134 | fveq2d 6910 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) →
(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘1)) |
| 136 | | log1 26627 |
. . . . . . 7
⊢
(log‘1) = 0 |
| 137 | 135, 136 | eqtrdi 2793 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) →
(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = 0) |
| 138 | | fzfid 14014 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → (1...((2 · 𝑁)C𝑁)) ∈ Fin) |
| 139 | | inss1 4237 |
. . . . . . 7
⊢ ((1...((2
· 𝑁)C𝑁)) ∩ ℙ) ⊆
(1...((2 · 𝑁)C𝑁)) |
| 140 | | ssfi 9213 |
. . . . . . 7
⊢
(((1...((2 · 𝑁)C𝑁)) ∈ Fin ∧ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ⊆ (1...((2 ·
𝑁)C𝑁))) → ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∈
Fin) |
| 141 | 138, 139,
140 | sylancl 586 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∈
Fin) |
| 142 | 57, 84, 137, 141 | fsumss 15761 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) |
| 143 | 62 | nnrpd 13075 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℝ+) |
| 144 | 65 | nn0zd 12639 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ) |
| 145 | | relogexp 26638 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ+
∧ (𝑘 pCnt ((2 ·
𝑁)C𝑁)) ∈ ℤ) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = ((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘))) |
| 146 | 143, 144,
145 | syl2anc 584 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = ((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘))) |
| 147 | 146 | sumeq2dv 15738 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘))) |
| 148 | | pclogsum 27259 |
. . . . . 6
⊢ (((2
· 𝑁)C𝑁) ∈ ℕ →
Σ𝑘 ∈ ((1...((2
· 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)) = (log‘((2 · 𝑁)C𝑁))) |
| 149 | 14, 148 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)) = (log‘((2 · 𝑁)C𝑁))) |
| 150 | 142, 147,
149 | 3eqtrd 2781 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘((2 · 𝑁)C𝑁))) |
| 151 | 29 | recnd 11289 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘(2 · 𝑁)) ∈
ℂ) |
| 152 | | fsumconst 15826 |
. . . . . 6
⊢
((((1...𝐾) ∩
ℙ) ∈ Fin ∧ (log‘(2 · 𝑁)) ∈ ℂ) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((♯‘((1...𝐾) ∩ ℙ)) ·
(log‘(2 · 𝑁)))) |
| 153 | 46, 151, 152 | syl2anc 584 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((♯‘((1...𝐾) ∩ ℙ)) ·
(log‘(2 · 𝑁)))) |
| 154 | | 2eluzge1 12936 |
. . . . . . 7
⊢ 2 ∈
(ℤ≥‘1) |
| 155 | | ppival2g 27172 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 2 ∈
(ℤ≥‘1)) → (π‘𝐾) = (♯‘((1...𝐾) ∩ ℙ))) |
| 156 | 47, 154, 155 | sylancl 586 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘𝐾) = (♯‘((1...𝐾) ∩ ℙ))) |
| 157 | 156 | oveq1d 7446 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) =
((♯‘((1...𝐾)
∩ ℙ)) · (log‘(2 · 𝑁)))) |
| 158 | 153, 157 | eqtr4d 2780 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((π‘𝐾) · (log‘(2
· 𝑁)))) |
| 159 | 82, 150, 158 | 3brtr3d 5174 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘𝐾) · (log‘(2
· 𝑁)))) |
| 160 | | min1 13231 |
. . . . . . 7
⊢ (((2
· 𝑁) ∈ ℝ
∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → if((2
· 𝑁) ≤ ((2
· 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ (2 · 𝑁)) |
| 161 | 21, 49, 160 | syl2anc 584 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ (2 · 𝑁)) |
| 162 | 35, 161 | eqbrtrid 5178 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ≤ (2 · 𝑁)) |
| 163 | | ppiwordi 27205 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ (2
· 𝑁) ∈ ℝ
∧ 𝐾 ≤ (2 ·
𝑁)) →
(π‘𝐾) ≤
(π‘(2 · 𝑁))) |
| 164 | 38, 21, 162, 163 | syl3anc 1373 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘𝐾) ≤ (π‘(2 · 𝑁))) |
| 165 | | 1red 11262 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 1 ∈ ℝ) |
| 166 | | 2re 12340 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
| 167 | 166 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 2 ∈ ℝ) |
| 168 | | 1lt2 12437 |
. . . . . . . 8
⊢ 1 <
2 |
| 169 | 168 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 1 < 2) |
| 170 | | 2t1e2 12429 |
. . . . . . . 8
⊢ (2
· 1) = 2 |
| 171 | 3 | nnge1d 12314 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘4) → 1 ≤ 𝑁) |
| 172 | | eluzelre 12889 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈ ℝ) |
| 173 | | 2pos 12369 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
| 174 | 166, 173 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ ∧ 0 < 2) |
| 175 | 174 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 ∈ ℝ ∧ 0 <
2)) |
| 176 | | lemul2 12120 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2
· 𝑁))) |
| 177 | 165, 172,
175, 176 | syl3anc 1373 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘4) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 ·
𝑁))) |
| 178 | 171, 177 | mpbid 232 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 1) ≤ (2 · 𝑁)) |
| 179 | 170, 178 | eqbrtrrid 5179 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 2 ≤ (2 · 𝑁)) |
| 180 | 165, 167,
21, 169, 179 | ltletrd 11421 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → 1 < (2 · 𝑁)) |
| 181 | 21, 180 | rplogcld 26671 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘(2 · 𝑁)) ∈
ℝ+) |
| 182 | 41, 24, 181 | lemul1d 13120 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘𝐾) ≤ (π‘(2 · 𝑁)) ↔
((π‘𝐾)
· (log‘(2 · 𝑁))) ≤ ((π‘(2 ·
𝑁)) · (log‘(2
· 𝑁))))) |
| 183 | 164, 182 | mpbid 232 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ≤ ((π‘(2
· 𝑁)) ·
(log‘(2 · 𝑁)))) |
| 184 | 16, 42, 30, 159, 183 | letrd 11418 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘(2 ·
𝑁)) · (log‘(2
· 𝑁)))) |
| 185 | 10, 16, 30, 34, 184 | ltletrd 11421 |
1
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 ·
𝑁)) · (log‘(2
· 𝑁)))) |