Step | Hyp | Ref
| Expression |
1 | | chtppilim.1 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
2 | 1 | rpred 11872 |
. . . . . 6
⊢ (𝜑 → 𝐴 ∈ ℝ) |
3 | 2 | recnd 10068 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈ ℂ) |
4 | 3 | sqvald 13005 |
. . . 4
⊢ (𝜑 → (𝐴↑2) = (𝐴 · 𝐴)) |
5 | 4 | oveq1d 6665 |
. . 3
⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) = ((𝐴 · 𝐴) · ((π‘𝑁) · (log‘𝑁)))) |
6 | | chtppilim.3 |
. . . . . . . . 9
⊢ (𝜑 → 𝑁 ∈ (2[,)+∞)) |
7 | | 2re 11090 |
. . . . . . . . . 10
⊢ 2 ∈
ℝ |
8 | | elicopnf 12269 |
. . . . . . . . . 10
⊢ (2 ∈
ℝ → (𝑁 ∈
(2[,)+∞) ↔ (𝑁
∈ ℝ ∧ 2 ≤ 𝑁))) |
9 | 7, 8 | ax-mp 5 |
. . . . . . . . 9
⊢ (𝑁 ∈ (2[,)+∞) ↔
(𝑁 ∈ ℝ ∧ 2
≤ 𝑁)) |
10 | 6, 9 | sylib 208 |
. . . . . . . 8
⊢ (𝜑 → (𝑁 ∈ ℝ ∧ 2 ≤ 𝑁)) |
11 | 10 | simpld 475 |
. . . . . . 7
⊢ (𝜑 → 𝑁 ∈ ℝ) |
12 | | ppicl 24857 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(π‘𝑁)
∈ ℕ0) |
13 | 11, 12 | syl 17 |
. . . . . 6
⊢ (𝜑 → (π‘𝑁) ∈
ℕ0) |
14 | 13 | nn0red 11352 |
. . . . 5
⊢ (𝜑 → (π‘𝑁) ∈
ℝ) |
15 | 14 | recnd 10068 |
. . . 4
⊢ (𝜑 → (π‘𝑁) ∈
ℂ) |
16 | | 0red 10041 |
. . . . . . . 8
⊢ (𝜑 → 0 ∈
ℝ) |
17 | 7 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 2 ∈
ℝ) |
18 | | 2pos 11112 |
. . . . . . . . 9
⊢ 0 <
2 |
19 | 18 | a1i 11 |
. . . . . . . 8
⊢ (𝜑 → 0 < 2) |
20 | 10 | simprd 479 |
. . . . . . . 8
⊢ (𝜑 → 2 ≤ 𝑁) |
21 | 16, 17, 11, 19, 20 | ltletrd 10197 |
. . . . . . 7
⊢ (𝜑 → 0 < 𝑁) |
22 | 11, 21 | elrpd 11869 |
. . . . . 6
⊢ (𝜑 → 𝑁 ∈
ℝ+) |
23 | 22 | relogcld 24369 |
. . . . 5
⊢ (𝜑 → (log‘𝑁) ∈
ℝ) |
24 | 23 | recnd 10068 |
. . . 4
⊢ (𝜑 → (log‘𝑁) ∈
ℂ) |
25 | 3, 3, 15, 24 | mul4d 10248 |
. . 3
⊢ (𝜑 → ((𝐴 · 𝐴) · ((π‘𝑁) · (log‘𝑁))) = ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁)))) |
26 | 5, 25 | eqtrd 2656 |
. 2
⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) = ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁)))) |
27 | 2, 14 | remulcld 10070 |
. . . 4
⊢ (𝜑 → (𝐴 · (π‘𝑁)) ∈
ℝ) |
28 | 2, 23 | remulcld 10070 |
. . . 4
⊢ (𝜑 → (𝐴 · (log‘𝑁)) ∈ ℝ) |
29 | 27, 28 | remulcld 10070 |
. . 3
⊢ (𝜑 → ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁))) ∈ ℝ) |
30 | 22, 2 | rpcxpcld 24476 |
. . . . . . . 8
⊢ (𝜑 → (𝑁↑𝑐𝐴) ∈
ℝ+) |
31 | 30 | rpred 11872 |
. . . . . . 7
⊢ (𝜑 → (𝑁↑𝑐𝐴) ∈ ℝ) |
32 | | ppicl 24857 |
. . . . . . 7
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ →
(π‘(𝑁↑𝑐𝐴)) ∈
ℕ0) |
33 | 31, 32 | syl 17 |
. . . . . 6
⊢ (𝜑 → (π‘(𝑁↑𝑐𝐴)) ∈
ℕ0) |
34 | 33 | nn0red 11352 |
. . . . 5
⊢ (𝜑 → (π‘(𝑁↑𝑐𝐴)) ∈
ℝ) |
35 | 14, 34 | resubcld 10458 |
. . . 4
⊢ (𝜑 → ((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) ∈ ℝ) |
36 | 35, 28 | remulcld 10070 |
. . 3
⊢ (𝜑 → (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁))) ∈ ℝ) |
37 | | chtcl 24835 |
. . . 4
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) ∈
ℝ) |
38 | 11, 37 | syl 17 |
. . 3
⊢ (𝜑 → (θ‘𝑁) ∈
ℝ) |
39 | | 1red 10055 |
. . . . . . 7
⊢ (𝜑 → 1 ∈
ℝ) |
40 | | 1lt2 11194 |
. . . . . . . 8
⊢ 1 <
2 |
41 | 40 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → 1 < 2) |
42 | 39, 17, 11, 41, 20 | ltletrd 10197 |
. . . . . 6
⊢ (𝜑 → 1 < 𝑁) |
43 | 11, 42 | rplogcld 24375 |
. . . . 5
⊢ (𝜑 → (log‘𝑁) ∈
ℝ+) |
44 | 1, 43 | rpmulcld 11888 |
. . . 4
⊢ (𝜑 → (𝐴 · (log‘𝑁)) ∈
ℝ+) |
45 | 14, 31 | resubcld 10458 |
. . . . 5
⊢ (𝜑 → ((π‘𝑁) − (𝑁↑𝑐𝐴)) ∈ ℝ) |
46 | | ppinncl 24900 |
. . . . . . . . . 10
⊢ ((𝑁 ∈ ℝ ∧ 2 ≤
𝑁) →
(π‘𝑁)
∈ ℕ) |
47 | 10, 46 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → (π‘𝑁) ∈
ℕ) |
48 | 31, 47 | nndivred 11069 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) ∈ ℝ) |
49 | | chtppilim.4 |
. . . . . . . 8
⊢ (𝜑 → ((𝑁↑𝑐𝐴) / (π‘𝑁)) < (1 − 𝐴)) |
50 | 48, 39, 2, 49 | ltsub13d 10633 |
. . . . . . 7
⊢ (𝜑 → 𝐴 < (1 − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
51 | 31 | recnd 10068 |
. . . . . . . . 9
⊢ (𝜑 → (𝑁↑𝑐𝐴) ∈ ℂ) |
52 | 47 | nnrpd 11870 |
. . . . . . . . . 10
⊢ (𝜑 → (π‘𝑁) ∈
ℝ+) |
53 | 52 | rpcnne0d 11881 |
. . . . . . . . 9
⊢ (𝜑 → ((π‘𝑁) ∈ ℂ ∧
(π‘𝑁) ≠
0)) |
54 | | divsubdir 10721 |
. . . . . . . . 9
⊢
(((π‘𝑁) ∈ ℂ ∧ (𝑁↑𝑐𝐴) ∈ ℂ ∧
((π‘𝑁)
∈ ℂ ∧ (π‘𝑁) ≠ 0)) → (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁)) = (((π‘𝑁) / (π‘𝑁)) − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
55 | 15, 51, 53, 54 | syl3anc 1326 |
. . . . . . . 8
⊢ (𝜑 → (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁)) = (((π‘𝑁) / (π‘𝑁)) − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
56 | | divid 10714 |
. . . . . . . . . 10
⊢
(((π‘𝑁) ∈ ℂ ∧
(π‘𝑁) ≠
0) → ((π‘𝑁) / (π‘𝑁)) = 1) |
57 | 53, 56 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 → ((π‘𝑁) / (π‘𝑁)) = 1) |
58 | 57 | oveq1d 6665 |
. . . . . . . 8
⊢ (𝜑 → (((π‘𝑁) / (π‘𝑁)) − ((𝑁↑𝑐𝐴) / (π‘𝑁))) = (1 − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
59 | 55, 58 | eqtrd 2656 |
. . . . . . 7
⊢ (𝜑 → (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁)) = (1 − ((𝑁↑𝑐𝐴) / (π‘𝑁)))) |
60 | 50, 59 | breqtrrd 4681 |
. . . . . 6
⊢ (𝜑 → 𝐴 < (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁))) |
61 | 2, 45, 52 | ltmuldivd 11919 |
. . . . . 6
⊢ (𝜑 → ((𝐴 · (π‘𝑁)) <
((π‘𝑁)
− (𝑁↑𝑐𝐴)) ↔ 𝐴 < (((π‘𝑁) − (𝑁↑𝑐𝐴)) / (π‘𝑁)))) |
62 | 60, 61 | mpbird 247 |
. . . . 5
⊢ (𝜑 → (𝐴 · (π‘𝑁)) <
((π‘𝑁)
− (𝑁↑𝑐𝐴))) |
63 | | ppiltx 24903 |
. . . . . . 7
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ+
→ (π‘(𝑁↑𝑐𝐴)) < (𝑁↑𝑐𝐴)) |
64 | 30, 63 | syl 17 |
. . . . . 6
⊢ (𝜑 → (π‘(𝑁↑𝑐𝐴)) < (𝑁↑𝑐𝐴)) |
65 | 34, 31, 14, 64 | ltsub2dd 10640 |
. . . . 5
⊢ (𝜑 → ((π‘𝑁) − (𝑁↑𝑐𝐴)) < ((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴)))) |
66 | 27, 45, 35, 62, 65 | lttrd 10198 |
. . . 4
⊢ (𝜑 → (𝐴 · (π‘𝑁)) <
((π‘𝑁)
− (π‘(𝑁↑𝑐𝐴)))) |
67 | 27, 35, 44, 66 | ltmul1dd 11927 |
. . 3
⊢ (𝜑 → ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁))) < (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁)))) |
68 | | fzfid 12772 |
. . . . . 6
⊢ (𝜑 → (((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∈ Fin) |
69 | | inss1 3833 |
. . . . . 6
⊢
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
(((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) |
70 | | ssfi 8180 |
. . . . . 6
⊢
(((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∈ Fin ∧ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
(((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁))) → ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
71 | 68, 69, 70 | sylancl 694 |
. . . . 5
⊢ (𝜑 → ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
72 | | inss2 3834 |
. . . . . . . 8
⊢
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
ℙ |
73 | | simpr 477 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) |
74 | 72, 73 | sseldi 3601 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ ℙ) |
75 | | prmnn 15388 |
. . . . . . . 8
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℕ) |
76 | 75 | nnrpd 11870 |
. . . . . . 7
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
ℝ+) |
77 | 74, 76 | syl 17 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ ℝ+) |
78 | 77 | relogcld 24369 |
. . . . 5
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (log‘𝑝) ∈
ℝ) |
79 | 71, 78 | fsumrecl 14465 |
. . . 4
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝) ∈
ℝ) |
80 | 28 | recnd 10068 |
. . . . . . 7
⊢ (𝜑 → (𝐴 · (log‘𝑁)) ∈ ℂ) |
81 | | fsumconst 14522 |
. . . . . . 7
⊢
((((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ∈ Fin ∧ (𝐴 · (log‘𝑁)) ∈ ℂ) →
Σ𝑝 ∈
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(𝐴 · (log‘𝑁)) = ((#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) ·
(𝐴 ·
(log‘𝑁)))) |
82 | 71, 80, 81 | syl2anc 693 |
. . . . . 6
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(𝐴 · (log‘𝑁)) = ((#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) ·
(𝐴 ·
(log‘𝑁)))) |
83 | | ppifl 24886 |
. . . . . . . . . 10
⊢ (𝑁 ∈ ℝ →
(π‘(⌊‘𝑁)) = (π‘𝑁)) |
84 | 11, 83 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(π‘(⌊‘𝑁)) = (π‘𝑁)) |
85 | | ppifl 24886 |
. . . . . . . . . 10
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ →
(π‘(⌊‘(𝑁↑𝑐𝐴))) = (π‘(𝑁↑𝑐𝐴))) |
86 | 31, 85 | syl 17 |
. . . . . . . . 9
⊢ (𝜑 →
(π‘(⌊‘(𝑁↑𝑐𝐴))) = (π‘(𝑁↑𝑐𝐴))) |
87 | 84, 86 | oveq12d 6668 |
. . . . . . . 8
⊢ (𝜑 →
((π‘(⌊‘𝑁)) −
(π‘(⌊‘(𝑁↑𝑐𝐴)))) = ((π‘𝑁) − (π‘(𝑁↑𝑐𝐴)))) |
88 | 39, 11, 42 | ltled 10185 |
. . . . . . . . . . . 12
⊢ (𝜑 → 1 ≤ 𝑁) |
89 | | chtppilim.2 |
. . . . . . . . . . . . 13
⊢ (𝜑 → 𝐴 < 1) |
90 | | 1re 10039 |
. . . . . . . . . . . . . 14
⊢ 1 ∈
ℝ |
91 | | ltle 10126 |
. . . . . . . . . . . . . 14
⊢ ((𝐴 ∈ ℝ ∧ 1 ∈
ℝ) → (𝐴 < 1
→ 𝐴 ≤
1)) |
92 | 2, 90, 91 | sylancl 694 |
. . . . . . . . . . . . 13
⊢ (𝜑 → (𝐴 < 1 → 𝐴 ≤ 1)) |
93 | 89, 92 | mpd 15 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝐴 ≤ 1) |
94 | 11, 88, 2, 39, 93 | cxplead 24467 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁↑𝑐𝐴) ≤ (𝑁↑𝑐1)) |
95 | 11 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (𝜑 → 𝑁 ∈ ℂ) |
96 | 95 | cxp1d 24452 |
. . . . . . . . . . 11
⊢ (𝜑 → (𝑁↑𝑐1) = 𝑁) |
97 | 94, 96 | breqtrd 4679 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁↑𝑐𝐴) ≤ 𝑁) |
98 | | flword2 12614 |
. . . . . . . . . 10
⊢ (((𝑁↑𝑐𝐴) ∈ ℝ ∧ 𝑁 ∈ ℝ ∧ (𝑁↑𝑐𝐴) ≤ 𝑁) → (⌊‘𝑁) ∈
(ℤ≥‘(⌊‘(𝑁↑𝑐𝐴)))) |
99 | 31, 11, 97, 98 | syl3anc 1326 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘𝑁) ∈
(ℤ≥‘(⌊‘(𝑁↑𝑐𝐴)))) |
100 | | ppidif 24889 |
. . . . . . . . 9
⊢
((⌊‘𝑁)
∈ (ℤ≥‘(⌊‘(𝑁↑𝑐𝐴))) →
((π‘(⌊‘𝑁)) −
(π‘(⌊‘(𝑁↑𝑐𝐴)))) = (#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩
ℙ))) |
101 | 99, 100 | syl 17 |
. . . . . . . 8
⊢ (𝜑 →
((π‘(⌊‘𝑁)) −
(π‘(⌊‘(𝑁↑𝑐𝐴)))) = (#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩
ℙ))) |
102 | 87, 101 | eqtr3d 2658 |
. . . . . . 7
⊢ (𝜑 → ((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) = (#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩
ℙ))) |
103 | 102 | oveq1d 6665 |
. . . . . 6
⊢ (𝜑 → (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁))) = ((#‘((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) ·
(𝐴 ·
(log‘𝑁)))) |
104 | 82, 103 | eqtr4d 2659 |
. . . . 5
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(𝐴 · (log‘𝑁)) = (((π‘𝑁) − (π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁)))) |
105 | 28 | adantr 481 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝐴 · (log‘𝑁)) ∈ ℝ) |
106 | 31 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝑁↑𝑐𝐴) ∈ ℝ) |
107 | | reflcl 12597 |
. . . . . . . . . . 11
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ →
(⌊‘(𝑁↑𝑐𝐴)) ∈ ℝ) |
108 | | peano2re 10209 |
. . . . . . . . . . 11
⊢
((⌊‘(𝑁↑𝑐𝐴)) ∈ ℝ →
((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈ ℝ) |
109 | 31, 107, 108 | 3syl 18 |
. . . . . . . . . 10
⊢ (𝜑 → ((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈
ℝ) |
110 | 109 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) →
((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈ ℝ) |
111 | 77 | rpred 11872 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ ℝ) |
112 | | fllep1 12602 |
. . . . . . . . . . 11
⊢ ((𝑁↑𝑐𝐴) ∈ ℝ → (𝑁↑𝑐𝐴) ≤ ((⌊‘(𝑁↑𝑐𝐴)) + 1)) |
113 | 31, 112 | syl 17 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁↑𝑐𝐴) ≤ ((⌊‘(𝑁↑𝑐𝐴)) + 1)) |
114 | 113 | adantr 481 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝑁↑𝑐𝐴) ≤ ((⌊‘(𝑁↑𝑐𝐴)) + 1)) |
115 | 69, 73 | sseldi 3601 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈ (((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁))) |
116 | | elfzle1 12344 |
. . . . . . . . . 10
⊢ (𝑝 ∈ (((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) → ((⌊‘(𝑁↑𝑐𝐴)) + 1) ≤ 𝑝) |
117 | 115, 116 | syl 17 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) →
((⌊‘(𝑁↑𝑐𝐴)) + 1) ≤ 𝑝) |
118 | 106, 110,
111, 114, 117 | letrd 10194 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝑁↑𝑐𝐴) ≤ 𝑝) |
119 | 22 | rpne0d 11877 |
. . . . . . . . . . 11
⊢ (𝜑 → 𝑁 ≠ 0) |
120 | 95, 119, 3 | cxpefd 24458 |
. . . . . . . . . 10
⊢ (𝜑 → (𝑁↑𝑐𝐴) = (exp‘(𝐴 · (log‘𝑁)))) |
121 | 120 | eqcomd 2628 |
. . . . . . . . 9
⊢ (𝜑 → (exp‘(𝐴 · (log‘𝑁))) = (𝑁↑𝑐𝐴)) |
122 | 121 | adantr 481 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (exp‘(𝐴 · (log‘𝑁))) = (𝑁↑𝑐𝐴)) |
123 | 77 | reeflogd 24370 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) →
(exp‘(log‘𝑝)) =
𝑝) |
124 | 118, 122,
123 | 3brtr4d 4685 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (exp‘(𝐴 · (log‘𝑁))) ≤
(exp‘(log‘𝑝))) |
125 | | efle 14848 |
. . . . . . . 8
⊢ (((𝐴 · (log‘𝑁)) ∈ ℝ ∧
(log‘𝑝) ∈
ℝ) → ((𝐴
· (log‘𝑁))
≤ (log‘𝑝) ↔
(exp‘(𝐴 ·
(log‘𝑁))) ≤
(exp‘(log‘𝑝)))) |
126 | 105, 78, 125 | syl2anc 693 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → ((𝐴 · (log‘𝑁)) ≤ (log‘𝑝) ↔ (exp‘(𝐴 · (log‘𝑁))) ≤
(exp‘(log‘𝑝)))) |
127 | 124, 126 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)) → (𝐴 · (log‘𝑁)) ≤ (log‘𝑝)) |
128 | 71, 105, 78, 127 | fsumle 14531 |
. . . . 5
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(𝐴 · (log‘𝑁)) ≤ Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝)) |
129 | 104, 128 | eqbrtrrd 4677 |
. . . 4
⊢ (𝜑 → (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁))) ≤ Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝)) |
130 | | fzfid 12772 |
. . . . . . 7
⊢ (𝜑 → (1...(⌊‘𝑁)) ∈ Fin) |
131 | | inss1 3833 |
. . . . . . 7
⊢
((1...(⌊‘𝑁)) ∩ ℙ) ⊆
(1...(⌊‘𝑁)) |
132 | | ssfi 8180 |
. . . . . . 7
⊢
(((1...(⌊‘𝑁)) ∈ Fin ∧
((1...(⌊‘𝑁))
∩ ℙ) ⊆ (1...(⌊‘𝑁))) → ((1...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
133 | 130, 131,
132 | sylancl 694 |
. . . . . 6
⊢ (𝜑 → ((1...(⌊‘𝑁)) ∩ ℙ) ∈
Fin) |
134 | | inss2 3834 |
. . . . . . . . . . . . 13
⊢
((1...(⌊‘𝑁)) ∩ ℙ) ⊆
ℙ |
135 | | simpr 477 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
((1...(⌊‘𝑁))
∩ ℙ)) |
136 | 134, 135 | sseldi 3601 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
ℙ) |
137 | | prmuz2 15408 |
. . . . . . . . . . . 12
⊢ (𝑝 ∈ ℙ → 𝑝 ∈
(ℤ≥‘2)) |
138 | 136, 137 | syl 17 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
(ℤ≥‘2)) |
139 | | eluz2b2 11761 |
. . . . . . . . . . 11
⊢ (𝑝 ∈
(ℤ≥‘2) ↔ (𝑝 ∈ ℕ ∧ 1 < 𝑝)) |
140 | 138, 139 | sylib 208 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → (𝑝 ∈ ℕ ∧ 1 <
𝑝)) |
141 | 140 | simpld 475 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
ℕ) |
142 | 141 | nnred 11035 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 𝑝 ∈
ℝ) |
143 | 140 | simprd 479 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 1 <
𝑝) |
144 | 142, 143 | rplogcld 24375 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ+) |
145 | 144 | rpred 11872 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) →
(log‘𝑝) ∈
ℝ) |
146 | 144 | rpge0d 11876 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑝 ∈ ((1...(⌊‘𝑁)) ∩ ℙ)) → 0 ≤
(log‘𝑝)) |
147 | 30 | rpge0d 11876 |
. . . . . . . . . 10
⊢ (𝜑 → 0 ≤ (𝑁↑𝑐𝐴)) |
148 | | flge0nn0 12621 |
. . . . . . . . . 10
⊢ (((𝑁↑𝑐𝐴) ∈ ℝ ∧ 0 ≤
(𝑁↑𝑐𝐴)) → (⌊‘(𝑁↑𝑐𝐴)) ∈
ℕ0) |
149 | 31, 147, 148 | syl2anc 693 |
. . . . . . . . 9
⊢ (𝜑 → (⌊‘(𝑁↑𝑐𝐴)) ∈
ℕ0) |
150 | | nn0p1nn 11332 |
. . . . . . . . 9
⊢
((⌊‘(𝑁↑𝑐𝐴)) ∈ ℕ0 →
((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈ ℕ) |
151 | 149, 150 | syl 17 |
. . . . . . . 8
⊢ (𝜑 → ((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈
ℕ) |
152 | | nnuz 11723 |
. . . . . . . 8
⊢ ℕ =
(ℤ≥‘1) |
153 | 151, 152 | syl6eleq 2711 |
. . . . . . 7
⊢ (𝜑 → ((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈
(ℤ≥‘1)) |
154 | | fzss1 12380 |
. . . . . . 7
⊢
(((⌊‘(𝑁↑𝑐𝐴)) + 1) ∈
(ℤ≥‘1) → (((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ⊆ (1...(⌊‘𝑁))) |
155 | | ssrin 3838 |
. . . . . . 7
⊢
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ⊆ (1...(⌊‘𝑁)) →
((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
((1...(⌊‘𝑁))
∩ ℙ)) |
156 | 153, 154,
155 | 3syl 18 |
. . . . . 6
⊢ (𝜑 → ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ) ⊆
((1...(⌊‘𝑁))
∩ ℙ)) |
157 | 133, 145,
146, 156 | fsumless 14528 |
. . . . 5
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝) ≤ Σ𝑝 ∈ ((1...(⌊‘𝑁)) ∩
ℙ)(log‘𝑝)) |
158 | | chtval 24836 |
. . . . . . 7
⊢ (𝑁 ∈ ℝ →
(θ‘𝑁) =
Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝)) |
159 | 11, 158 | syl 17 |
. . . . . 6
⊢ (𝜑 → (θ‘𝑁) = Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝)) |
160 | | 2eluzge1 11734 |
. . . . . . . 8
⊢ 2 ∈
(ℤ≥‘1) |
161 | | ppisval2 24831 |
. . . . . . . 8
⊢ ((𝑁 ∈ ℝ ∧ 2 ∈
(ℤ≥‘1)) → ((0[,]𝑁) ∩ ℙ) =
((1...(⌊‘𝑁))
∩ ℙ)) |
162 | 11, 160, 161 | sylancl 694 |
. . . . . . 7
⊢ (𝜑 → ((0[,]𝑁) ∩ ℙ) =
((1...(⌊‘𝑁))
∩ ℙ)) |
163 | 162 | sumeq1d 14431 |
. . . . . 6
⊢ (𝜑 → Σ𝑝 ∈ ((0[,]𝑁) ∩ ℙ)(log‘𝑝) = Σ𝑝 ∈ ((1...(⌊‘𝑁)) ∩
ℙ)(log‘𝑝)) |
164 | 159, 163 | eqtrd 2656 |
. . . . 5
⊢ (𝜑 → (θ‘𝑁) = Σ𝑝 ∈ ((1...(⌊‘𝑁)) ∩
ℙ)(log‘𝑝)) |
165 | 157, 164 | breqtrrd 4681 |
. . . 4
⊢ (𝜑 → Σ𝑝 ∈ ((((⌊‘(𝑁↑𝑐𝐴)) + 1)...(⌊‘𝑁)) ∩ ℙ)(log‘𝑝) ≤ (θ‘𝑁)) |
166 | 36, 79, 38, 129, 165 | letrd 10194 |
. . 3
⊢ (𝜑 → (((π‘𝑁) −
(π‘(𝑁↑𝑐𝐴))) · (𝐴 · (log‘𝑁))) ≤ (θ‘𝑁)) |
167 | 29, 36, 38, 67, 166 | ltletrd 10197 |
. 2
⊢ (𝜑 → ((𝐴 · (π‘𝑁)) · (𝐴 · (log‘𝑁))) < (θ‘𝑁)) |
168 | 26, 167 | eqbrtrd 4675 |
1
⊢ (𝜑 → ((𝐴↑2) · ((π‘𝑁) · (log‘𝑁))) < (θ‘𝑁)) |