Step | Hyp | Ref
| Expression |
1 | | 4nn 11064 |
. . . . . 6
⊢ 4 ∈
ℕ |
2 | | eluznn 11634 |
. . . . . . . 8
⊢ ((4
∈ ℕ ∧ 𝑁
∈ (ℤ≥‘4)) → 𝑁 ∈ ℕ) |
3 | 1, 2 | mpan 702 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈ ℕ) |
4 | 3 | nnnn0d 11228 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈
ℕ0) |
5 | | nnexpcl 12735 |
. . . . . 6
⊢ ((4
∈ ℕ ∧ 𝑁
∈ ℕ0) → (4↑𝑁) ∈ ℕ) |
6 | 1, 4, 5 | sylancr 694 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (4↑𝑁) ∈ ℕ) |
7 | 6 | nnrpd 11746 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (4↑𝑁) ∈
ℝ+) |
8 | 3 | nnrpd 11746 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈
ℝ+) |
9 | 7, 8 | rpdivcld 11765 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((4↑𝑁) / 𝑁) ∈
ℝ+) |
10 | 9 | relogcld 24173 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) ∈ ℝ) |
11 | | fzctr 12320 |
. . . . . 6
⊢ (𝑁 ∈ ℕ0
→ 𝑁 ∈ (0...(2
· 𝑁))) |
12 | 4, 11 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈ (0...(2 · 𝑁))) |
13 | | bccl2 12972 |
. . . . 5
⊢ (𝑁 ∈ (0...(2 · 𝑁)) → ((2 · 𝑁)C𝑁) ∈ ℕ) |
14 | 12, 13 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℕ) |
15 | 14 | nnrpd 11746 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈
ℝ+) |
16 | 15 | relogcld 24173 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ∈ ℝ) |
17 | | 2z 11286 |
. . . . . . 7
⊢ 2 ∈
ℤ |
18 | | eluzelz 11573 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈ ℤ) |
19 | | zmulcl 11303 |
. . . . . . 7
⊢ ((2
∈ ℤ ∧ 𝑁
∈ ℤ) → (2 · 𝑁) ∈ ℤ) |
20 | 17, 18, 19 | sylancr 694 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 𝑁) ∈ ℤ) |
21 | 20 | zred 11358 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 𝑁) ∈ ℝ) |
22 | | ppicl 24657 |
. . . . 5
⊢ ((2
· 𝑁) ∈ ℝ
→ (π‘(2 · 𝑁)) ∈
ℕ0) |
23 | 21, 22 | syl 17 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘(2 · 𝑁)) ∈
ℕ0) |
24 | 23 | nn0red 11229 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘(2 · 𝑁)) ∈
ℝ) |
25 | | 2nn 11062 |
. . . . . 6
⊢ 2 ∈
ℕ |
26 | | nnmulcl 10920 |
. . . . . 6
⊢ ((2
∈ ℕ ∧ 𝑁
∈ ℕ) → (2 · 𝑁) ∈ ℕ) |
27 | 25, 3, 26 | sylancr 694 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 𝑁) ∈ ℕ) |
28 | 27 | nnrpd 11746 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 𝑁) ∈
ℝ+) |
29 | 28 | relogcld 24173 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘(2 · 𝑁)) ∈
ℝ) |
30 | 24, 29 | remulcld 9949 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘(2 · 𝑁)) · (log‘(2
· 𝑁))) ∈
ℝ) |
31 | | bclbnd 24805 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁)) |
32 | | logltb 24150 |
. . . 4
⊢
((((4↑𝑁) /
𝑁) ∈
ℝ+ ∧ ((2 · 𝑁)C𝑁) ∈ ℝ+) →
(((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁) ↔ (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁)))) |
33 | 9, 15, 32 | syl2anc 691 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → (((4↑𝑁) / 𝑁) < ((2 · 𝑁)C𝑁) ↔ (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁)))) |
34 | 31, 33 | mpbid 221 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < (log‘((2 · 𝑁)C𝑁))) |
35 | | chebbnd1lem1.1 |
. . . . . . . 8
⊢ 𝐾 = if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) |
36 | 27, 14 | ifcld 4081 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ∈ ℕ) |
37 | 35, 36 | syl5eqel 2692 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ∈ ℕ) |
38 | 37 | nnred 10912 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ∈ ℝ) |
39 | | ppicl 24657 |
. . . . . 6
⊢ (𝐾 ∈ ℝ →
(π‘𝐾)
∈ ℕ0) |
40 | 38, 39 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘𝐾) ∈
ℕ0) |
41 | 40 | nn0red 11229 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘𝐾) ∈ ℝ) |
42 | 41, 29 | remulcld 9949 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ∈
ℝ) |
43 | | fzfid 12634 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → (1...𝐾) ∈ Fin) |
44 | | inss1 3795 |
. . . . . 6
⊢
((1...𝐾) ∩
ℙ) ⊆ (1...𝐾) |
45 | | ssfi 8065 |
. . . . . 6
⊢
(((1...𝐾) ∈ Fin
∧ ((1...𝐾) ∩
ℙ) ⊆ (1...𝐾))
→ ((1...𝐾) ∩
ℙ) ∈ Fin) |
46 | 43, 44, 45 | sylancl 693 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → ((1...𝐾) ∩ ℙ) ∈
Fin) |
47 | 37 | nnzd 11357 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ∈ ℤ) |
48 | 14 | nnzd 11357 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℤ) |
49 | 14 | nnred 10912 |
. . . . . . . . . . . 12
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ ℝ) |
50 | | min2 11895 |
. . . . . . . . . . . 12
⊢ (((2
· 𝑁) ∈ ℝ
∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → if((2
· 𝑁) ≤ ((2
· 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ ((2 · 𝑁)C𝑁)) |
51 | 21, 49, 50 | syl2anc 691 |
. . . . . . . . . . 11
⊢ (𝑁 ∈
(ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ ((2 · 𝑁)C𝑁)) |
52 | 35, 51 | syl5eqbr 4618 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ≤ ((2 · 𝑁)C𝑁)) |
53 | | eluz2 11569 |
. . . . . . . . . 10
⊢ (((2
· 𝑁)C𝑁) ∈
(ℤ≥‘𝐾) ↔ (𝐾 ∈ ℤ ∧ ((2 · 𝑁)C𝑁) ∈ ℤ ∧ 𝐾 ≤ ((2 · 𝑁)C𝑁))) |
54 | 47, 48, 52, 53 | syl3anbrc 1239 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘4) → ((2 · 𝑁)C𝑁) ∈ (ℤ≥‘𝐾)) |
55 | | fzss2 12252 |
. . . . . . . . 9
⊢ (((2
· 𝑁)C𝑁) ∈
(ℤ≥‘𝐾) → (1...𝐾) ⊆ (1...((2 · 𝑁)C𝑁))) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘4) → (1...𝐾) ⊆ (1...((2 · 𝑁)C𝑁))) |
57 | | ssrin 3800 |
. . . . . . . 8
⊢
((1...𝐾) ⊆
(1...((2 · 𝑁)C𝑁)) → ((1...𝐾) ∩ ℙ) ⊆
((1...((2 · 𝑁)C𝑁)) ∩
ℙ)) |
58 | 56, 57 | syl 17 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → ((1...𝐾) ∩ ℙ) ⊆ ((1...((2 ·
𝑁)C𝑁)) ∩ ℙ)) |
59 | 58 | sselda 3568 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) |
60 | | inss1 3795 |
. . . . . . . . . . 11
⊢ ((1...((2
· 𝑁)C𝑁)) ∩ ℙ) ⊆
(1...((2 · 𝑁)C𝑁)) |
61 | | simpr 476 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) |
62 | 60, 61 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁))) |
63 | | elfznn 12241 |
. . . . . . . . . 10
⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ∈ ℕ) |
64 | 62, 63 | syl 17 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℕ) |
65 | | inss2 3796 |
. . . . . . . . . . 11
⊢ ((1...((2
· 𝑁)C𝑁)) ∩ ℙ) ⊆
ℙ |
66 | 65, 61 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℙ) |
67 | 14 | adantr 480 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → ((2 · 𝑁)C𝑁) ∈ ℕ) |
68 | 66, 67 | pccld 15393 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
69 | 64, 68 | nnexpcld 12892 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ) |
70 | 69 | nnrpd 11746 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈
ℝ+) |
71 | 70 | relogcld 24173 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ) |
72 | 59, 71 | syldan 486 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ) |
73 | 29 | adantr 480 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(2
· 𝑁)) ∈
ℝ) |
74 | | elin 3758 |
. . . . . . . . 9
⊢ (𝑘 ∈ ((1...𝐾) ∩ ℙ) ↔ (𝑘 ∈ (1...𝐾) ∧ 𝑘 ∈ ℙ)) |
75 | 74 | simprbi 479 |
. . . . . . . 8
⊢ (𝑘 ∈ ((1...𝐾) ∩ ℙ) → 𝑘 ∈ ℙ) |
76 | | bposlem1 24809 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℕ ∧ 𝑘 ∈ ℙ) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
77 | 3, 75, 76 | syl2an 493 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
78 | 59, 70 | syldan 486 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈
ℝ+) |
79 | 78 | reeflogd 24174 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) →
(exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) = (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) |
80 | 28 | adantr 480 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (2 · 𝑁) ∈
ℝ+) |
81 | 80 | reeflogd 24174 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) →
(exp‘(log‘(2 · 𝑁))) = (2 · 𝑁)) |
82 | 77, 79, 81 | 3brtr4d 4615 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) →
(exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 ·
𝑁)))) |
83 | | efle 14687 |
. . . . . . 7
⊢
(((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℝ ∧ (log‘(2
· 𝑁)) ∈
ℝ) → ((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁)) ↔
(exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 ·
𝑁))))) |
84 | 72, 73, 83 | syl2anc 691 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → ((log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁)) ↔
(exp‘(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) ≤ (exp‘(log‘(2 ·
𝑁))))) |
85 | 82, 84 | mpbird 246 |
. . . . 5
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ (log‘(2 · 𝑁))) |
86 | 46, 72, 73, 85 | fsumle 14372 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ≤ Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁))) |
87 | 71 | recnd 9947 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ) |
88 | 59, 87 | syldan 486 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...𝐾) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) ∈ ℂ) |
89 | | eldifn 3695 |
. . . . . . . . . . . . 13
⊢ (𝑘 ∈ (((1...((2 ·
𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) → ¬
𝑘 ∈ ((1...𝐾) ∩
ℙ)) |
90 | 89 | adantl 481 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬
𝑘 ∈ ((1...𝐾) ∩
ℙ)) |
91 | | simpr 476 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ (((1...((2 ·
𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩
ℙ))) |
92 | 91 | eldifad 3552 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) |
93 | 60, 92 | sseldi 3566 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈ (1...((2 · 𝑁)C𝑁))) |
94 | 93, 63 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈
ℕ) |
95 | 94 | adantrr 749 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈
ℕ) |
96 | 95 | nnred 10912 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈
ℝ) |
97 | 92, 69 | syldan 486 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℕ) |
98 | 97 | nnred 10912 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ) |
99 | 98 | adantrr 749 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ∈ ℝ) |
100 | 21 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (2 · 𝑁) ∈
ℝ) |
101 | 95 | nncnd 10913 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈
ℂ) |
102 | 101 | exp1d 12865 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) = 𝑘) |
103 | 95 | nnge1d 10940 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 1 ≤ 𝑘) |
104 | | simprr 792 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ) |
105 | | nnuz 11599 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ℕ =
(ℤ≥‘1) |
106 | 104, 105 | syl6eleq 2698 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈
(ℤ≥‘1)) |
107 | 96, 103, 106 | leexp2ad 12903 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑1) ≤ (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) |
108 | 102, 107 | eqbrtrrd 4607 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) |
109 | 3 | adantr 480 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑁 ∈ ℕ) |
110 | 65, 92 | sseldi 3566 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈
ℙ) |
111 | 110 | adantrr 749 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈
ℙ) |
112 | 109, 111,
76 | syl2anc 691 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) ≤ (2 · 𝑁)) |
113 | 96, 99, 100, 108, 112 | letrd 10073 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ (2 · 𝑁)) |
114 | | elfzle2 12216 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 ∈ (1...((2 · 𝑁)C𝑁)) → 𝑘 ≤ ((2 · 𝑁)C𝑁)) |
115 | 93, 114 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ≤ ((2 · 𝑁)C𝑁)) |
116 | 115 | adantrr 749 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ ((2 · 𝑁)C𝑁)) |
117 | 49 | adantr 480 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → ((2 ·
𝑁)C𝑁) ∈ ℝ) |
118 | | lemin 11897 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑘 ∈ ℝ ∧ (2
· 𝑁) ∈ ℝ
∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁)))) |
119 | 96, 100, 117, 118 | syl3anc 1318 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ↔ (𝑘 ≤ (2 · 𝑁) ∧ 𝑘 ≤ ((2 · 𝑁)C𝑁)))) |
120 | 113, 116,
119 | mpbir2and 959 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁))) |
121 | 120, 35 | syl6breqr 4625 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ≤ 𝐾) |
122 | 37 | adantr 480 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℕ) |
123 | 122 | nnzd 11357 |
. . . . . . . . . . . . . . . 16
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝐾 ∈ ℤ) |
124 | | fznn 12278 |
. . . . . . . . . . . . . . . 16
⊢ (𝐾 ∈ ℤ → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾))) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . 15
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → (𝑘 ∈ (1...𝐾) ↔ (𝑘 ∈ ℕ ∧ 𝑘 ≤ 𝐾))) |
126 | 95, 121, 125 | mpbir2and 959 |
. . . . . . . . . . . . . 14
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ (1...𝐾)) |
127 | 126, 111 | elind 3760 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ (𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ)) ∧ (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ)) → 𝑘 ∈ ((1...𝐾) ∩ ℙ)) |
128 | 127 | expr 641 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) →
((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ → 𝑘 ∈ ((1...𝐾) ∩ ℙ))) |
129 | 90, 128 | mtod 188 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → ¬
(𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ) |
130 | 92, 68 | syldan 486 |
. . . . . . . . . . . . 13
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈
ℕ0) |
131 | | elnn0 11171 |
. . . . . . . . . . . . 13
⊢ ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ0 ↔ ((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ ∨ (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0)) |
132 | 130, 131 | sylib 207 |
. . . . . . . . . . . 12
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) →
((𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ ∨ (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0)) |
133 | 132 | ord 391 |
. . . . . . . . . . 11
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (¬
(𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℕ → (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0)) |
134 | 129, 133 | mpd 15 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) = 0) |
135 | 134 | oveq2d 6565 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = (𝑘↑0)) |
136 | 94 | nncnd 10913 |
. . . . . . . . . 10
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → 𝑘 ∈
ℂ) |
137 | 136 | exp0d 12864 |
. . . . . . . . 9
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑0) = 1) |
138 | 135, 137 | eqtrd 2644 |
. . . . . . . 8
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) → (𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))) = 1) |
139 | 138 | fveq2d 6107 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) →
(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘1)) |
140 | | log1 24136 |
. . . . . . 7
⊢
(log‘1) = 0 |
141 | 139, 140 | syl6eq 2660 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ (((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∖ ((1...𝐾) ∩ ℙ))) →
(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = 0) |
142 | | fzfid 12634 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → (1...((2 · 𝑁)C𝑁)) ∈ Fin) |
143 | | ssfi 8065 |
. . . . . . 7
⊢
(((1...((2 · 𝑁)C𝑁)) ∈ Fin ∧ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ⊆ (1...((2 ·
𝑁)C𝑁))) → ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∈
Fin) |
144 | 142, 60, 143 | sylancl 693 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → ((1...((2 · 𝑁)C𝑁)) ∩ ℙ) ∈
Fin) |
145 | 58, 88, 141, 144 | fsumss 14303 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁))))) |
146 | 64 | nnrpd 11746 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → 𝑘 ∈ ℝ+) |
147 | 68 | nn0zd 11356 |
. . . . . . 7
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (𝑘 pCnt ((2 · 𝑁)C𝑁)) ∈ ℤ) |
148 | | relogexp 24146 |
. . . . . . 7
⊢ ((𝑘 ∈ ℝ+
∧ (𝑘 pCnt ((2 ·
𝑁)C𝑁)) ∈ ℤ) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = ((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘))) |
149 | 146, 147,
148 | syl2anc 691 |
. . . . . 6
⊢ ((𝑁 ∈
(ℤ≥‘4) ∧ 𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)) → (log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = ((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘))) |
150 | 149 | sumeq2dv 14281 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘))) |
151 | | pclogsum 24740 |
. . . . . 6
⊢ (((2
· 𝑁)C𝑁) ∈ ℕ →
Σ𝑘 ∈ ((1...((2
· 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)) = (log‘((2 · 𝑁)C𝑁))) |
152 | 14, 151 | syl 17 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...((2 · 𝑁)C𝑁)) ∩ ℙ)((𝑘 pCnt ((2 · 𝑁)C𝑁)) · (log‘𝑘)) = (log‘((2 · 𝑁)C𝑁))) |
153 | 145, 150,
152 | 3eqtrd 2648 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(𝑘↑(𝑘 pCnt ((2 · 𝑁)C𝑁)))) = (log‘((2 · 𝑁)C𝑁))) |
154 | 29 | recnd 9947 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘(2 · 𝑁)) ∈
ℂ) |
155 | | fsumconst 14364 |
. . . . . 6
⊢
((((1...𝐾) ∩
ℙ) ∈ Fin ∧ (log‘(2 · 𝑁)) ∈ ℂ) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((#‘((1...𝐾) ∩ ℙ)) ·
(log‘(2 · 𝑁)))) |
156 | 46, 154, 155 | syl2anc 691 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((#‘((1...𝐾) ∩ ℙ)) ·
(log‘(2 · 𝑁)))) |
157 | | 2eluzge1 11610 |
. . . . . . 7
⊢ 2 ∈
(ℤ≥‘1) |
158 | | ppival2g 24655 |
. . . . . . 7
⊢ ((𝐾 ∈ ℤ ∧ 2 ∈
(ℤ≥‘1)) → (π‘𝐾) = (#‘((1...𝐾) ∩ ℙ))) |
159 | 47, 157, 158 | sylancl 693 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘𝐾) = (#‘((1...𝐾) ∩ ℙ))) |
160 | 159 | oveq1d 6564 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) = ((#‘((1...𝐾) ∩ ℙ)) ·
(log‘(2 · 𝑁)))) |
161 | 156, 160 | eqtr4d 2647 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → Σ𝑘 ∈ ((1...𝐾) ∩ ℙ)(log‘(2 · 𝑁)) = ((π‘𝐾) · (log‘(2
· 𝑁)))) |
162 | 86, 153, 161 | 3brtr3d 4614 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘𝐾) · (log‘(2
· 𝑁)))) |
163 | | min1 11894 |
. . . . . . 7
⊢ (((2
· 𝑁) ∈ ℝ
∧ ((2 · 𝑁)C𝑁) ∈ ℝ) → if((2
· 𝑁) ≤ ((2
· 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ (2 · 𝑁)) |
164 | 21, 49, 163 | syl2anc 691 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → if((2 · 𝑁) ≤ ((2 · 𝑁)C𝑁), (2 · 𝑁), ((2 · 𝑁)C𝑁)) ≤ (2 · 𝑁)) |
165 | 35, 164 | syl5eqbr 4618 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝐾 ≤ (2 · 𝑁)) |
166 | | ppiwordi 24688 |
. . . . 5
⊢ ((𝐾 ∈ ℝ ∧ (2
· 𝑁) ∈ ℝ
∧ 𝐾 ≤ (2 ·
𝑁)) →
(π‘𝐾) ≤
(π‘(2 · 𝑁))) |
167 | 38, 21, 165, 166 | syl3anc 1318 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → (π‘𝐾) ≤ (π‘(2 · 𝑁))) |
168 | | 1red 9934 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 1 ∈ ℝ) |
169 | | 2re 10967 |
. . . . . . . 8
⊢ 2 ∈
ℝ |
170 | 169 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 2 ∈ ℝ) |
171 | | 1lt2 11071 |
. . . . . . . 8
⊢ 1 <
2 |
172 | 171 | a1i 11 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 1 < 2) |
173 | | 2t1e2 11053 |
. . . . . . . 8
⊢ (2
· 1) = 2 |
174 | 3 | nnge1d 10940 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘4) → 1 ≤ 𝑁) |
175 | | eluzelre 11574 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → 𝑁 ∈ ℝ) |
176 | | 2pos 10989 |
. . . . . . . . . . . 12
⊢ 0 <
2 |
177 | 169, 176 | pm3.2i 470 |
. . . . . . . . . . 11
⊢ (2 ∈
ℝ ∧ 0 < 2) |
178 | 177 | a1i 11 |
. . . . . . . . . 10
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 ∈ ℝ ∧ 0 <
2)) |
179 | | lemul2 10755 |
. . . . . . . . . 10
⊢ ((1
∈ ℝ ∧ 𝑁
∈ ℝ ∧ (2 ∈ ℝ ∧ 0 < 2)) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2
· 𝑁))) |
180 | 168, 175,
178, 179 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝑁 ∈
(ℤ≥‘4) → (1 ≤ 𝑁 ↔ (2 · 1) ≤ (2 ·
𝑁))) |
181 | 174, 180 | mpbid 221 |
. . . . . . . 8
⊢ (𝑁 ∈
(ℤ≥‘4) → (2 · 1) ≤ (2 · 𝑁)) |
182 | 173, 181 | syl5eqbrr 4619 |
. . . . . . 7
⊢ (𝑁 ∈
(ℤ≥‘4) → 2 ≤ (2 · 𝑁)) |
183 | 168, 170,
21, 172, 182 | ltletrd 10076 |
. . . . . 6
⊢ (𝑁 ∈
(ℤ≥‘4) → 1 < (2 · 𝑁)) |
184 | 21, 183 | rplogcld 24179 |
. . . . 5
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘(2 · 𝑁)) ∈
ℝ+) |
185 | 41, 24, 184 | lemul1d 11791 |
. . . 4
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘𝐾) ≤ (π‘(2 · 𝑁)) ↔
((π‘𝐾)
· (log‘(2 · 𝑁))) ≤ ((π‘(2 ·
𝑁)) · (log‘(2
· 𝑁))))) |
186 | 167, 185 | mpbid 221 |
. . 3
⊢ (𝑁 ∈
(ℤ≥‘4) → ((π‘𝐾) · (log‘(2 · 𝑁))) ≤ ((π‘(2
· 𝑁)) ·
(log‘(2 · 𝑁)))) |
187 | 16, 42, 30, 162, 186 | letrd 10073 |
. 2
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((2 · 𝑁)C𝑁)) ≤ ((π‘(2 ·
𝑁)) · (log‘(2
· 𝑁)))) |
188 | 10, 16, 30, 34, 187 | ltletrd 10076 |
1
⊢ (𝑁 ∈
(ℤ≥‘4) → (log‘((4↑𝑁) / 𝑁)) < ((π‘(2 ·
𝑁)) · (log‘(2
· 𝑁)))) |