Step | Hyp | Ref
| Expression |
1 | | chtppilim.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
2 | 1 | rpred 11748 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | recnd 9947 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℂ) |
4 | 3 | sqvald 12867 |
. . . 4
⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
5 | 4 | oveq1d 6564 |
. . 3
⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) = ((𝐴 · 𝐴) · ((π‘𝑁) · (log‘𝑁)))) |
6 | | chtppilim.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (2[,)+∞)) |
7 | | 2re 10967 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
8 | | elicopnf 12140 |
. . . . . . . . . 10
⊢ (2 ∈
ℝ → (𝑁 ∈
(2[,)+∞) ↔ (𝑁
∈ ℝ ∧ 2 ≤ 𝑁))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑁 ∈ (2[,)+∞) ↔
(𝑁 ∈ ℝ ∧ 2
≤ 𝑁)) |
10 | 6, 9 | sylib 207 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 2 ≤ 𝑁)) |
11 | 10 | simpld 474 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
12 | | ppicl 24657 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(π‘𝑁)
∈ ℕ0) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → (π‘𝑁) ∈
ℕ0) |
14 | 13 | nn0red 11229 |
. . . . 5
⊢ (𝜑 → (π‘𝑁) ∈
ℝ) |
15 | 14 | recnd 9947 |
. . . 4
⊢ (𝜑 → (π‘𝑁) ∈
ℂ) |
16 | | 0red 9920 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
17 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) |
18 | | 2pos 10989 |
. . . . . . . . 9
⊢ 0 <
2 |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 < 2) |
20 | 10 | simprd 478 |
. . . . . . . 8
⊢ (𝜑 → 2 ≤ 𝑁) |
21 | 16, 17, 11, 19, 20 | ltletrd 10076 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑁) |
22 | 11, 21 | elrpd 11745 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
23 | 22 | relogcld 24173 |
. . . . 5
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) |
24 | 23 | recnd 9947 |
. . . 4
⊢ (𝜑 → (log‘𝑁) ∈
ℂ) |
25 | 3, 3, 15, 24 | mul4d 10127 |
. . 3
⊢ (𝜑 → ((𝐴 · 𝐴) · ((π‘𝑁) · (log‘𝑁))) = ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁)))) |
26 | 5, 25 | eqtrd 2644 |
. 2
⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) = ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁)))) |
27 | 2, 14 | remulcld 9949 |
. . . 4
⊢ (𝜑 → (𝐴 · (π‘𝑁)) ∈
ℝ) |
28 | 2, 23 | remulcld 9949 |
. . . 4
⊢ (𝜑 → (𝐴 · (log‘𝑁)) ∈ ℝ) |
29 | 27, 28 | remulcld 9949 |
. . 3
⊢ (𝜑 → ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁))) ∈ ℝ) |
30 | 22, 2 | rpcxpcld 24276 |
. . . . . . . 8
⊢ (𝜑 → (𝑁↑𝑐𝐴) ∈
ℝ+) |
31 | 30 | rpred 11748 |
. . . . . . 7
⊢ (𝜑 → (𝑁↑𝑐𝐴) ∈ ℝ) |
32 | | ppicl 24657 |
. . . . . . 7
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ →
(π‘(𝑁↑𝑐𝐴)) ∈
ℕ0) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → (π‘(𝑁↑𝑐𝐴)) ∈
ℕ0) |
34 | 33 | nn0red 11229 |
. . . . 5
⊢ (𝜑 → (π‘(𝑁↑𝑐𝐴)) ∈
ℝ) |
35 | 14, 34 | resubcld 10337 |
. . . 4
⊢ (𝜑 → ((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) ∈ ℝ) |
36 | 35, 28 | remulcld 9949 |
. . 3
⊢ (𝜑 → (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁))) ∈ ℝ) |
37 | | chtcl 24635 |
. . . 4
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) ∈
ℝ) |
38 | 11, 37 | syl 17 |
. . 3
⊢ (𝜑 → (θ‘𝑁) ∈
ℝ) |
39 | | 1red 9934 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
40 | | 1lt2 11071 |
. . . . . . . 8
⊢ 1 <
2 |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 < 2) |
42 | 39, 17, 11, 41, 20 | ltletrd 10076 |
. . . . . 6
⊢ (𝜑 → 1 < 𝑁) |
43 | 11, 42 | rplogcld 24179 |
. . . . 5
⊢ (𝜑 → (log‘𝑁) ∈
ℝ+) |
44 | 1, 43 | rpmulcld 11764 |
. . . 4
⊢ (𝜑 → (𝐴 · (log‘𝑁)) ∈
ℝ+) |
45 | 14, 31 | resubcld 10337 |
. . . . 5
⊢ (𝜑 → ((π‘𝑁) − (𝑁↑𝑐𝐴)) ∈ ℝ) |
46 | | ppinncl 24700 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) →
(π‘𝑁)
∈ ℕ) |
47 | 10, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (π‘𝑁) ∈
ℕ) |
48 | 31, 47 | nndivred 10946 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) ∈ ℝ) |
49 | | chtppilim.4 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) < (1 − 𝐴)) |
50 | 48, 39, 2, 49 | ltsub13d 10512 |
. . . . . . 7
⊢ (𝜑 → 𝐴 < (1 − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
51 | 31 | recnd 9947 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁↑𝑐𝐴) ∈ ℂ) |
52 | 47 | nnrpd 11746 |
. . . . . . . . . 10
⊢ (𝜑 → (π‘𝑁) ∈
ℝ+) |
53 | 52 | rpcnne0d 11757 |
. . . . . . . . 9
⊢ (𝜑 → ((π‘𝑁) ∈ ℂ ∧
(π‘𝑁) ≠
0)) |
54 | | divsubdir 10600 |
. . . . . . . . 9
⊢
(((π‘𝑁) ∈ ℂ ∧ (𝑁↑𝑐𝐴) ∈ ℂ ∧
((π‘𝑁)
∈ ℂ ∧ (π‘𝑁) ≠ 0)) → (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁)) = (((π‘𝑁) / (π‘𝑁)) − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
55 | 15, 51, 53, 54 | syl3anc 1318 |
. . . . . . . 8
⊢ (𝜑 → (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁)) = (((π‘𝑁) / (π‘𝑁)) − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
56 | | divid 10593 |
. . . . . . . . . 10
⊢
(((π‘𝑁) ∈ ℂ ∧
(π‘𝑁) ≠
0) → ((π‘𝑁) / (π‘𝑁)) = 1) |
57 | 53, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((π‘𝑁) / (π‘𝑁)) = 1) |
58 | 57 | oveq1d 6564 |
. . . . . . . 8
⊢ (𝜑 → (((π‘𝑁) / (π‘𝑁)) − ((𝑁↑𝑐𝐴) / (π‘𝑁))) = (1 − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
59 | 55, 58 | eqtrd 2644 |
. . . . . . 7
⊢ (𝜑 → (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁)) = (1 − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
60 | 50, 59 | breqtrrd 4611 |
. . . . . 6
⊢ (𝜑 → 𝐴 < (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁))) |
61 | 2, 45, 52 | ltmuldivd 11795 |
. . . . . 6
⊢ (𝜑 → ((𝐴 · (π‘𝑁)) <
((π‘𝑁)
− (𝑁↑𝑐𝐴)) ↔ 𝐴 < (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁)))) |
62 | 60, 61 | mpbird 246 |
. . . . 5
⊢ (𝜑 → (𝐴 · (π‘𝑁)) <
((π‘𝑁)
− (𝑁↑𝑐𝐴))) |
63 | | ppiltx 24703 |
. . . . . . 7
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ+
→ (π‘(𝑁↑𝑐𝐴)) < (𝑁↑𝑐𝐴)) |
64 | 30, 63 | syl 17 |
. . . . . 6
⊢ (𝜑 → (π‘(𝑁↑𝑐𝐴)) < (𝑁↑𝑐𝐴)) |
65 | 34, 31, 14, 64 | ltsub2dd 10519 |
. . . . 5
⊢ (𝜑 → ((π‘𝑁) − (𝑁↑𝑐𝐴)) < ((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴)))) |
66 | 27, 45, 35, 62, 65 | lttrd 10077 |
. . . 4
⊢ (𝜑 → (𝐴 · (π‘𝑁)) <
((π‘𝑁)
− (π‘(𝑁↑𝑐𝐴)))) |
67 | 27, 35, 44, 66 | ltmul1dd 11803 |
. . 3
⊢ (𝜑 → ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁))) < (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁)))) |
68 | | fzfid 12634 |
. . . . . 6
⊢ (𝜑 → (((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∈ Fin) |
69 | | inss1 3795 |
. . . . . 6
⊢
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
(((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) |
70 | | ssfi 8065 |
. . . . . 6
⊢
(((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∈ Fin ∧ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
(((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁))) → ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
71 | 68, 69, 70 | sylancl 693 |
. . . . 5
⊢ (𝜑 → ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
72 | | inss2 3796 |
. . . . . . . 8
⊢
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
ℙ |
73 | | simpr 476 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) |
74 | 72, 73 | sseldi 3566 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ ℙ) |
75 | | prmnn 15226 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
76 | 75 | nnrpd 11746 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℝ+) |
77 | 74, 76 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
78 | 77 | relogcld 24173 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
79 | 71, 78 | fsumrecl 14312 |
. . . 4
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝) ∈
ℝ) |
80 | 28 | recnd 9947 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · (log‘𝑁)) ∈ ℂ) |
81 | | fsumconst 14364 |
. . . . . . 7
⊢
((((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ∈ Fin ∧ (𝐴 · (log‘𝑁)) ∈ ℂ) →
Σ𝑝 ∈
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(𝐴 · (log‘𝑁)) = ((#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) ·
(𝐴 ·
(log‘𝑁)))) |
82 | 71, 80, 81 | syl2anc 691 |
. . . . . 6
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(𝐴 · (log‘𝑁)) = ((#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) ·
(𝐴 ·
(log‘𝑁)))) |
83 | | ppifl 24686 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ →
(π‘(⌊‘𝑁)) = (π‘𝑁)) |
84 | 11, 83 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(π‘(⌊‘𝑁)) = (π‘𝑁)) |
85 | | ppifl 24686 |
. . . . . . . . . 10
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ →
(π‘(⌊‘(𝑁↑𝑐𝐴))) = (π‘(𝑁↑𝑐𝐴))) |
86 | 31, 85 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(π‘(⌊‘(𝑁↑𝑐𝐴))) = (π‘(𝑁↑𝑐𝐴))) |
87 | 84, 86 | oveq12d 6567 |
. . . . . . . 8
⊢ (𝜑 →
((π‘(⌊‘𝑁)) −
(π‘(⌊‘(𝑁↑𝑐𝐴)))) = ((π‘𝑁) − (π‘(𝑁↑𝑐𝐴)))) |
88 | 39, 11, 42 | ltled 10064 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ≤ 𝑁) |
89 | | chtppilim.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 1) |
90 | | 1re 9918 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
91 | | ltle 10005 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 < 1
→ 𝐴 ≤
1)) |
92 | 2, 90, 91 | sylancl 693 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 < 1 → 𝐴 ≤ 1)) |
93 | 89, 92 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 1) |
94 | 11, 88, 2, 39, 93 | cxplead 24267 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁↑𝑐𝐴) ≤ (𝑁↑𝑐1)) |
95 | 11 | recnd 9947 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
96 | 95 | cxp1d 24252 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁↑𝑐1) = 𝑁) |
97 | 94, 96 | breqtrd 4609 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁↑𝑐𝐴) ≤ 𝑁) |
98 | | flword2 12476 |
. . . . . . . . . 10
⊢ (((𝑁↑𝑐𝐴) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁↑𝑐𝐴) ≤ 𝑁) → (⌊‘𝑁) ∈
(ℤ≥‘(⌊‘(𝑁↑𝑐𝐴)))) |
99 | 31, 11, 97, 98 | syl3anc 1318 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘𝑁) ∈
(ℤ≥‘(⌊‘(𝑁↑𝑐𝐴)))) |
100 | | ppidif 24689 |
. . . . . . . . 9
⊢
((⌊‘𝑁)
∈ (ℤ≥‘(⌊‘(𝑁↑𝑐𝐴))) →
((π‘(⌊‘𝑁)) −
(π‘(⌊‘(𝑁↑𝑐𝐴)))) = (#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩
ℙ))) |
101 | 99, 100 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
((π‘(⌊‘𝑁)) −
(π‘(⌊‘(𝑁↑𝑐𝐴)))) = (#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩
ℙ))) |
102 | 87, 101 | eqtr3d 2646 |
. . . . . . 7
⊢ (𝜑 → ((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) = (#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩
ℙ))) |
103 | 102 | oveq1d 6564 |
. . . . . 6
⊢ (𝜑 → (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁))) = ((#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) ·
(𝐴 ·
(log‘𝑁)))) |
104 | 82, 103 | eqtr4d 2647 |
. . . . 5
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(𝐴 · (log‘𝑁)) = (((π‘𝑁) − (π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁)))) |
105 | 28 | adantr 480 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝐴 · (log‘𝑁)) ∈ ℝ) |
106 | 31 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝑁↑𝑐𝐴) ∈ ℝ) |
107 | | reflcl 12459 |
. . . . . . . . . . 11
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ →
(⌊‘(𝑁↑𝑐𝐴)) ∈ ℝ) |
108 | | peano2re 10088 |
. . . . . . . . . . 11
⊢
((⌊‘(𝑁↑𝑐𝐴)) ∈ ℝ →
((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈ ℝ) |
109 | 31, 107, 108 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈
ℝ) |
110 | 109 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) →
((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈ ℝ) |
111 | 77 | rpred 11748 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ ℝ) |
112 | | fllep1 12464 |
. . . . . . . . . . 11
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ → (𝑁↑𝑐𝐴) ≤ ((⌊‘(𝑁↑𝑐𝐴)) + 1)) |
113 | 31, 112 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁↑𝑐𝐴) ≤ ((⌊‘(𝑁↑𝑐𝐴)) + 1)) |
114 | 113 | adantr 480 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝑁↑𝑐𝐴) ≤ ((⌊‘(𝑁↑𝑐𝐴)) + 1)) |
115 | 69, 73 | sseldi 3566 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ (((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁))) |
116 | | elfzle1 12215 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) → ((⌊‘(𝑁↑𝑐𝐴)) + 1) ≤ 𝑝) |
117 | 115, 116 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) →
((⌊‘(𝑁↑𝑐𝐴)) + 1) ≤ 𝑝) |
118 | 106, 110,
111, 114, 117 | letrd 10073 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝑁↑𝑐𝐴) ≤ 𝑝) |
119 | 22 | rpne0d 11753 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ≠ 0) |
120 | 95, 119, 3 | cxpefd 24258 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁↑𝑐𝐴) = (exp‘(𝐴 · (log‘𝑁)))) |
121 | 120 | eqcomd 2616 |
. . . . . . . . 9
⊢ (𝜑 → (exp‘(𝐴 · (log‘𝑁))) = (𝑁↑𝑐𝐴)) |
122 | 121 | adantr 480 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (exp‘(𝐴 · (log‘𝑁))) = (𝑁↑𝑐𝐴)) |
123 | 77 | reeflogd 24174 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) →
(exp‘(log‘𝑝)) =
𝑝) |
124 | 118, 122,
123 | 3brtr4d 4615 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (exp‘(𝐴 · (log‘𝑁))) ≤
(exp‘(log‘𝑝))) |
125 | | efle 14687 |
. . . . . . . 8
⊢ (((𝐴 · (log‘𝑁)) ∈ ℝ ∧
(log‘𝑝) ∈
ℝ) → ((𝐴
· (log‘𝑁))
≤ (log‘𝑝) ↔
(exp‘(𝐴 ·
(log‘𝑁))) ≤
(exp‘(log‘𝑝)))) |
126 | 105, 78, 125 | syl2anc 691 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → ((𝐴 · (log‘𝑁)) ≤ (log‘𝑝) ↔ (exp‘(𝐴 · (log‘𝑁))) ≤
(exp‘(log‘𝑝)))) |
127 | 124, 126 | mpbird 246 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝐴 · (log‘𝑁)) ≤ (log‘𝑝)) |
128 | 71, 105, 78, 127 | fsumle 14372 |
. . . . 5
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(𝐴 · (log‘𝑁)) ≤ Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝)) |
129 | 104, 128 | eqbrtrrd 4607 |
. . . 4
⊢ (𝜑 → (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁))) ≤ Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝)) |
130 | | fzfid 12634 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘𝑁)) ∈ Fin) |
131 | | inss1 3795 |
. . . . . . 7
⊢
((1...(⌊‘𝑁)) ∩ ℙ) ⊆
(1...(⌊‘𝑁)) |
132 | | ssfi 8065 |
. . . . . . 7
⊢
(((1...(⌊‘𝑁)) ∈ Fin ∧
((1...(⌊‘𝑁))
∩ ℙ) ⊆ (1...(⌊‘𝑁))) → ((1...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
133 | 130, 131,
132 | sylancl 693 |
. . . . . 6
⊢ (𝜑 → ((1...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
134 | | inss2 3796 |
. . . . . . . . . . . . 13
⊢
((1...(⌊‘𝑁)) ∩ ℙ) ⊆
ℙ |
135 | | simpr 476 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
((1...(⌊‘𝑁))
∩ ℙ)) |
136 | 134, 135 | sseldi 3566 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
ℙ) |
137 | | prmuz2 15246 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
(ℤ≥‘2)) |
139 | | eluz2b2 11637 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
140 | 138, 139 | sylib 207 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → (𝑝 ∈ ℕ ∧ 1 <
𝑝)) |
141 | 140 | simpld 474 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
ℕ) |
142 | 141 | nnred 10912 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
ℝ) |
143 | 140 | simprd 478 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 1 <
𝑝) |
144 | 142, 143 | rplogcld 24179 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ+) |
145 | 144 | rpred 11748 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ) |
146 | 144 | rpge0d 11752 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 0 ≤
(log‘𝑝)) |
147 | 30 | rpge0d 11752 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝑁↑𝑐𝐴)) |
148 | | flge0nn0 12483 |
. . . . . . . . . 10
⊢ (((𝑁↑𝑐𝐴) ∈ ℝ ∧ 0 ≤
(𝑁↑𝑐𝐴)) → (⌊‘(𝑁↑𝑐𝐴)) ∈
ℕ0) |
149 | 31, 147, 148 | syl2anc 691 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑁↑𝑐𝐴)) ∈
ℕ0) |
150 | | nn0p1nn 11209 |
. . . . . . . . 9
⊢
((⌊‘(𝑁↑𝑐𝐴)) ∈ ℕ0 →
((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈ ℕ) |
151 | 149, 150 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈
ℕ) |
152 | | nnuz 11599 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
153 | 151, 152 | syl6eleq 2698 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈
(ℤ≥‘1)) |
154 | | fzss1 12251 |
. . . . . . 7
⊢
(((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈
(ℤ≥‘1) → (((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ⊆ (1...(⌊‘𝑁))) |
155 | | ssrin 3800 |
. . . . . . 7
⊢
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ⊆ (1...(⌊‘𝑁)) →
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
((1...(⌊‘𝑁))
∩ ℙ)) |
156 | 153, 154,
155 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
((1...(⌊‘𝑁))
∩ ℙ)) |
157 | 133, 145,
146, 156 | fsumless 14369 |
. . . . 5
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝) ≤ Σ𝑝 ∈ ((1...(⌊‘𝑁)) ∩
ℙ)(log‘𝑝)) |
158 | | chtval 24636 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) =
Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝)) |
159 | 11, 158 | syl 17 |
. . . . . 6
⊢ (𝜑 → (θ‘𝑁) = Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝)) |
160 | | 2eluzge1 11610 |
. . . . . . . 8
⊢ 2 ∈
(ℤ≥‘1) |
161 | | ppisval2 24631 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 2 ∈
(ℤ≥‘1)) → ((0[,]𝑁) ∩ ℙ) =
((1...(⌊‘𝑁))
∩ ℙ)) |
162 | 11, 160, 161 | sylancl 693 |
. . . . . . 7
⊢ (𝜑 → ((0[,]𝑁) ∩ ℙ) =
((1...(⌊‘𝑁))
∩ ℙ)) |
163 | 162 | sumeq1d 14279 |
. . . . . 6
⊢ (𝜑 → Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑁)) ∩
ℙ)(log‘𝑝)) |
164 | 159, 163 | eqtrd 2644 |
. . . . 5
⊢ (𝜑 → (θ‘𝑁) = Σ𝑝 ∈ ((1...(⌊‘𝑁)) ∩
ℙ)(log‘𝑝)) |
165 | 157, 164 | breqtrrd 4611 |
. . . 4
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝) ≤ (θ‘𝑁)) |
166 | 36, 79, 38, 129, 165 | letrd 10073 |
. . 3
⊢ (𝜑 → (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁))) ≤ (θ‘𝑁)) |
167 | 29, 36, 38, 67, 166 | ltletrd 10076 |
. 2
⊢ (𝜑 → ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁))) < (θ‘𝑁)) |
168 | 26, 167 | eqbrtrd 4605 |
1
⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) < (θ‘𝑁)) |