Step | Hyp | Ref
| Expression |
1 | | 1red 10357 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ) |
2 | | pntrlog2bnd.r |
. . . . 5
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
3 | 2 | selberg34r 25673 |
. . . 4
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) |
4 | | elioore 12493 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
5 | 4 | adantl 475 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) |
6 | | 1rp 12116 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) |
8 | | 1red 10357 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) |
9 | | eliooord 12521 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
10 | 9 | adantl 475 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
11 | 10 | simpld 490 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) |
12 | 8, 5, 11 | ltled 10504 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) |
13 | 5, 7, 12 | rpgecld 12195 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) |
14 | 2 | pntrf 25665 |
. . . . . . . . . . 11
⊢ 𝑅:ℝ+⟶ℝ |
15 | 14 | ffvelrni 6607 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
16 | 13, 15 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ) |
17 | 13 | relogcld 24768 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) |
18 | 16, 17 | remulcld 10387 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑅‘𝑥) · (log‘𝑥)) ∈ ℝ) |
19 | | fzfid 13067 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
20 | 13 | adantr 474 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) |
21 | | elfznn 12663 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
22 | 21 | adantl 475 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
23 | 22 | nnrpd 12154 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
24 | 20, 23 | rpdivcld 12173 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
25 | 14 | ffvelrni 6607 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
27 | | fzfid 13067 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...𝑛) ∈ Fin) |
28 | | dvdsssfz1 15417 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
29 | 22, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
30 | | ssfi 8449 |
. . . . . . . . . . . . . 14
⊢
(((1...𝑛) ∈ Fin
∧ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ∈ Fin) |
31 | 27, 29, 30 | syl2anc 579 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ∈ Fin) |
32 | | ssrab2 3912 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ ℕ |
33 | | simpr 479 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
34 | 32, 33 | sseldi 3825 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ ℕ) |
35 | | vmacl 25257 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
36 | 34, 35 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘𝑚) ∈ ℝ) |
37 | | dvdsdivcl 15415 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
38 | 22, 37 | sylan 575 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
39 | 32, 38 | sseldi 3825 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ ℕ) |
40 | | vmacl 25257 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 / 𝑚) ∈ ℕ →
(Λ‘(𝑛 / 𝑚)) ∈
ℝ) |
41 | 39, 40 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘(𝑛 / 𝑚)) ∈ ℝ) |
42 | 36, 41 | remulcld 10387 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ) |
43 | 31, 42 | fsumrecl 14842 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ) |
44 | | vmacl 25257 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
45 | 22, 44 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
46 | 23 | relogcld 24768 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈
ℝ) |
47 | 45, 46 | remulcld 10387 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· (log‘𝑛))
∈ ℝ) |
48 | 43, 47 | resubcld 10782 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))) ∈
ℝ) |
49 | 26, 48 | remulcld 10387 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℝ) |
50 | 19, 49 | fsumrecl 14842 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℝ) |
51 | 5, 11 | rplogcld 24774 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) |
52 | 50, 51 | rerpdivcld 12187 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈
ℝ) |
53 | 18, 52 | resubcld 10782 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℝ) |
54 | 53, 13 | rerpdivcld 12187 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) |
55 | 54 | recnd 10385 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥) ∈ ℂ) |
56 | 55 | lo1o12 14641 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
(abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) ∈
≤𝑂(1))) |
57 | 3, 56 | mpbii 225 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) ∈ ≤𝑂(1)) |
58 | 55 | abscld 14552 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ ℝ) |
59 | 16 | recnd 10385 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ) |
60 | 59 | abscld 14552 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ) |
61 | 60, 17 | remulcld 10387 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ) |
62 | 26 | recnd 10385 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
63 | 62 | abscld 14552 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
64 | 22 | nnred 11367 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ) |
65 | | pntsval.1 |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
66 | 65 | pntsf 25675 |
. . . . . . . . . . 11
⊢ 𝑆:ℝ⟶ℝ |
67 | 66 | ffvelrni 6607 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ) |
68 | 64, 67 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ) |
69 | | 1red 10357 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) |
70 | 64, 69 | resubcld 10782 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ) |
71 | 66 | ffvelrni 6607 |
. . . . . . . . . 10
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) ∈
ℝ) |
72 | 70, 71 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ) |
73 | 68, 72 | resubcld 10782 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℝ) |
74 | 63, 73 | remulcld 10387 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
75 | 19, 74 | fsumrecl 14842 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
76 | 75, 51 | rerpdivcld 12187 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℝ) |
77 | 61, 76 | resubcld 10782 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℝ) |
78 | 77, 13 | rerpdivcld 12187 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) |
79 | 17 | recnd 10385 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) |
80 | 59, 79 | mulcld 10377 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑅‘𝑥) · (log‘𝑥)) ∈ ℂ) |
81 | 50 | recnd 10385 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℂ) |
82 | 51 | rpne0d 12161 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) |
83 | 81, 79, 82 | divcld 11127 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈
ℂ) |
84 | 80, 83 | subcld 10713 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℂ) |
85 | 84 | abscld 14552 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) ∈
ℝ) |
86 | 81 | abscld 14552 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
87 | 86, 51 | rerpdivcld 12187 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)) ∈
ℝ) |
88 | 61, 87 | resubcld 10782 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) ∈
ℝ) |
89 | 49 | recnd 10385 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℂ) |
90 | 89 | abscld 14552 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
91 | 19, 90 | fsumrecl 14842 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
92 | 19, 89 | fsumabs 14907 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) |
93 | 48 | recnd 10385 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))) ∈
ℂ) |
94 | 62, 93 | absmuld 14570 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (abs‘(Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) |
95 | 93 | abscld 14552 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
∈ ℝ) |
96 | 62 | absge0d 14560 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(abs‘(𝑅‘(𝑥 / 𝑛)))) |
97 | 43 | recnd 10385 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℂ) |
98 | 47 | recnd 10385 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· (log‘𝑛))
∈ ℂ) |
99 | 97, 98 | abs2dif2d 14574 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
≤ ((abs‘Σ𝑚
∈ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) +
(abs‘((Λ‘𝑛) · (log‘𝑛))))) |
100 | 72 | recnd 10385 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ) |
101 | 97, 98 | addcld 10376 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))) ∈ ℂ) |
102 | 100, 101 | pncan2d 10715 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) − (𝑆‘(𝑛 − 1))) = (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) |
103 | | elfzuz 12631 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
(ℤ≥‘1)) |
104 | 103 | adantl 475 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈
(ℤ≥‘1)) |
105 | | elfznn 12663 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
106 | 105 | adantl 475 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
107 | | vmacl 25257 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) |
108 | 106, 107 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (Λ‘𝑘) ∈ ℝ) |
109 | 106 | nnrpd 12154 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+) |
110 | 109 | relogcld 24768 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ) |
111 | 108, 110 | remulcld 10387 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → ((Λ‘𝑘) · (log‘𝑘)) ∈ ℝ) |
112 | | fzfid 13067 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (1...𝑘) ∈ Fin) |
113 | | dvdsssfz1 15417 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) |
114 | 106, 113 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) |
115 | | ssfi 8449 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((1...𝑘) ∈ Fin
∧ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ∈ Fin) |
116 | 112, 114,
115 | syl2anc 579 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ∈ Fin) |
117 | | ssrab2 3912 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ |
118 | | simpr 479 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
119 | 117, 118 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑚 ∈ ℕ) |
120 | 119, 35 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘𝑚) ∈ ℝ) |
121 | | dvdsdivcl 15415 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
122 | 106, 121 | sylan 575 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
123 | 117, 122 | sseldi 3825 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ ℕ) |
124 | | vmacl 25257 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 / 𝑚) ∈ ℕ →
(Λ‘(𝑘 / 𝑚)) ∈
ℝ) |
125 | 123, 124 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘(𝑘 / 𝑚)) ∈ ℝ) |
126 | 120, 125 | remulcld 10387 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) ∈ ℝ) |
127 | 116, 126 | fsumrecl 14842 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) ∈ ℝ) |
128 | 111, 127 | readdcld 10386 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) ∈ ℝ) |
129 | 128 | recnd 10385 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) ∈ ℂ) |
130 | | fveq2 6433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (Λ‘𝑘) = (Λ‘𝑛)) |
131 | | fveq2 6433 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (log‘𝑘) = (log‘𝑛)) |
132 | 130, 131 | oveq12d 6923 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑛) · (log‘𝑛))) |
133 | | breq2 4877 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑛 → (𝑦 ∥ 𝑘 ↔ 𝑦 ∥ 𝑛)) |
134 | 133 | rabbidv 3402 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} = {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
135 | | fvoveq1 6928 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑛 → (Λ‘(𝑘 / 𝑚)) = (Λ‘(𝑛 / 𝑚))) |
136 | 135 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑛 → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
137 | 136 | adantr 474 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 = 𝑛 ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
138 | 134, 137 | sumeq12rdv 14815 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
139 | 132, 138 | oveq12d 6923 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
140 | 104, 129,
139 | fsumm1 14857 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = (Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) + (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))) |
141 | 65 | pntsval2 25678 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) = Σ𝑘 ∈ (1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
142 | 64, 141 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = Σ𝑘 ∈ (1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
143 | 22 | nnzd 11809 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℤ) |
144 | | flid 12904 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℤ →
(⌊‘𝑛) = 𝑛) |
145 | 143, 144 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘𝑛) = 𝑛) |
146 | 145 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘𝑛)) =
(1...𝑛)) |
147 | 146 | sumeq1d 14808 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈
(1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
148 | 142, 147 | eqtrd 2861 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
149 | 65 | pntsval2 25678 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈
(1...(⌊‘(𝑛
− 1)))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
150 | 70, 149 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈ (1...(⌊‘(𝑛 −
1)))(((Λ‘𝑘)
· (log‘𝑘)) +
Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
151 | | 1zzd 11736 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℤ) |
152 | 143, 151 | zsubcld 11815 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℤ) |
153 | | flid 12904 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 − 1) ∈ ℤ
→ (⌊‘(𝑛
− 1)) = (𝑛 −
1)) |
154 | 152, 153 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑛 − 1)) = (𝑛 − 1)) |
155 | 154 | oveq2d 6921 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑛
− 1))) = (1...(𝑛
− 1))) |
156 | 155 | sumeq1d 14808 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈
(1...(⌊‘(𝑛
− 1)))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
157 | 150, 156 | eqtrd 2861 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
158 | 97, 98 | addcomd 10557 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))) = (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
159 | 157, 158 | oveq12d 6923 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) = (Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) + (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))) |
160 | 140, 148,
159 | 3eqtr4d 2871 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = ((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))))) |
161 | 160 | oveq1d 6920 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) = (((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) − (𝑆‘(𝑛 − 1)))) |
162 | | vmage0 25260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ → 0 ≤
(Λ‘𝑚)) |
163 | 34, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ (Λ‘𝑚)) |
164 | | vmage0 25260 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 / 𝑚) ∈ ℕ → 0 ≤
(Λ‘(𝑛 / 𝑚))) |
165 | 39, 164 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ (Λ‘(𝑛 / 𝑚))) |
166 | 36, 41, 163, 165 | mulge0d 10929 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) |
167 | 31, 42, 166 | fsumge0 14901 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
168 | 43, 167 | absidd 14538 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
169 | | vmage0 25260 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
170 | 22, 169 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(Λ‘𝑛)) |
171 | 22 | nnge1d 11399 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑛) |
172 | 64, 171 | logge0d 24775 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(log‘𝑛)) |
173 | 45, 46, 170, 172 | mulge0d 10929 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
((Λ‘𝑛)
· (log‘𝑛))) |
174 | 47, 173 | absidd 14538 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Λ‘𝑛) · (log‘𝑛))) = ((Λ‘𝑛) · (log‘𝑛))) |
175 | 168, 174 | oveq12d 6923 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((abs‘Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) +
(abs‘((Λ‘𝑛) · (log‘𝑛)))) = (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) |
176 | 102, 161,
175 | 3eqtr4d 2871 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) = ((abs‘Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) + (abs‘((Λ‘𝑛) · (log‘𝑛))))) |
177 | 99, 176 | breqtrrd 4901 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
≤ ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) |
178 | 95, 73, 63, 96, 177 | lemul2ad 11294 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (abs‘(Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
179 | 94, 178 | eqbrtrd 4895 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
180 | 19, 90, 74, 179 | fsumle 14905 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
181 | 86, 91, 75, 92, 180 | letrd 10513 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
182 | 86, 75, 51, 181 | lediv1dd 12214 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)) ≤ (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) |
183 | 87, 76, 61, 182 | lesub2dd 10969 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ≤ (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)))) |
184 | 59, 79 | absmuld 14570 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((𝑅‘𝑥) · (log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (abs‘(log‘𝑥)))) |
185 | 5, 12 | logge0d 24775 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (log‘𝑥)) |
186 | 17, 185 | absidd 14538 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(log‘𝑥)) = (log‘𝑥)) |
187 | 186 | oveq2d 6921 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (abs‘(log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (log‘𝑥))) |
188 | 184, 187 | eqtrd 2861 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((𝑅‘𝑥) · (log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (log‘𝑥))) |
189 | 81, 79, 82 | absdivd 14571 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) /
(abs‘(log‘𝑥)))) |
190 | 186 | oveq2d 6921 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) /
(abs‘(log‘𝑥)))
= ((abs‘Σ𝑛
∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) |
191 | 189, 190 | eqtrd 2861 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) |
192 | 188, 191 | oveq12d 6923 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘((𝑅‘𝑥) · (log‘𝑥))) − (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)))) |
193 | 80, 83 | abs2difd 14573 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘((𝑅‘𝑥) · (log‘𝑥))) − (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
194 | 192, 193 | eqbrtrrd 4897 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
195 | 77, 88, 85, 183, 194 | letrd 10513 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
196 | 77, 85, 13, 195 | lediv1dd 12214 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
197 | 53 | recnd 10385 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℂ) |
198 | 5 | recnd 10385 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℂ) |
199 | 13 | rpne0d 12161 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ≠ 0) |
200 | 197, 198,
199 | absdivd 14571 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / (abs‘𝑥))) |
201 | 13 | rpge0d 12160 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ 𝑥) |
202 | 5, 201 | absidd 14538 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘𝑥) = 𝑥) |
203 | 202 | oveq2d 6921 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / (abs‘𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
204 | 200, 203 | eqtrd 2861 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
205 | 196, 204 | breqtrrd 4901 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) |
206 | 205 | adantrr 708 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) |
207 | 1, 57, 58, 78, 206 | lo1le 14759 |
. 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)) |
208 | 207 | mptru 1664 |
1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1) |