Step | Hyp | Ref
| Expression |
1 | | 1red 10713 |
. . 3
⊢ (⊤
→ 1 ∈ ℝ) |
2 | | pntrlog2bnd.r |
. . . . 5
⊢ 𝑅 = (𝑎 ∈ ℝ+ ↦
((ψ‘𝑎) −
𝑎)) |
3 | 2 | selberg34r 26299 |
. . . 4
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) |
4 | | elioore 12844 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
5 | 4 | adantl 485 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) |
6 | | 1rp 12469 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
7 | 6 | a1i 11 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) |
8 | | 1red 10713 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) |
9 | | eliooord 12873 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
10 | 9 | adantl 485 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
11 | 10 | simpld 498 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) |
12 | 8, 5, 11 | ltled 10859 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) |
13 | 5, 7, 12 | rpgecld 12546 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) |
14 | 2 | pntrf 26291 |
. . . . . . . . . . 11
⊢ 𝑅:ℝ+⟶ℝ |
15 | 14 | ffvelrni 6854 |
. . . . . . . . . 10
⊢ (𝑥 ∈ ℝ+
→ (𝑅‘𝑥) ∈
ℝ) |
16 | 13, 15 | syl 17 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℝ) |
17 | 13 | relogcld 25358 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) |
18 | 16, 17 | remulcld 10742 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑅‘𝑥) · (log‘𝑥)) ∈ ℝ) |
19 | | fzfid 13425 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
20 | 13 | adantr 484 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ+) |
21 | | elfznn 13020 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
22 | 21 | adantl 485 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
23 | 22 | nnrpd 12505 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ+) |
24 | 20, 23 | rpdivcld 12524 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈
ℝ+) |
25 | 14 | ffvelrni 6854 |
. . . . . . . . . . . 12
⊢ ((𝑥 / 𝑛) ∈ ℝ+ → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
26 | 24, 25 | syl 17 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℝ) |
27 | | fzfid 13425 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (1...𝑛) ∈ Fin) |
28 | | dvdsssfz1 15756 |
. . . . . . . . . . . . . . 15
⊢ (𝑛 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
29 | 22, 28 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ (1...𝑛)) |
30 | 27, 29 | ssfid 8812 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ∈ Fin) |
31 | | ssrab2 3967 |
. . . . . . . . . . . . . . . 16
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ⊆ ℕ |
32 | | simpr 488 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
33 | 31, 32 | sseldi 3873 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 𝑚 ∈ ℕ) |
34 | | vmacl 25847 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
35 | 33, 34 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘𝑚) ∈ ℝ) |
36 | | dvdsdivcl 15754 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑛 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
37 | 22, 36 | sylan 583 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
38 | 31, 37 | sseldi 3873 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (𝑛 / 𝑚) ∈ ℕ) |
39 | | vmacl 25847 |
. . . . . . . . . . . . . . 15
⊢ ((𝑛 / 𝑚) ∈ ℕ →
(Λ‘(𝑛 / 𝑚)) ∈
ℝ) |
40 | 38, 39 | syl 17 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → (Λ‘(𝑛 / 𝑚)) ∈ ℝ) |
41 | 35, 40 | remulcld 10742 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ) |
42 | 30, 41 | fsumrecl 15177 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℝ) |
43 | | vmacl 25847 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
44 | 22, 43 | syl 17 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
45 | 23 | relogcld 25358 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (log‘𝑛) ∈
ℝ) |
46 | 44, 45 | remulcld 10742 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· (log‘𝑛))
∈ ℝ) |
47 | 42, 46 | resubcld 11139 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))) ∈
ℝ) |
48 | 26, 47 | remulcld 10742 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℝ) |
49 | 19, 48 | fsumrecl 15177 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℝ) |
50 | 5, 11 | rplogcld 25364 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) |
51 | 49, 50 | rerpdivcld 12538 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈
ℝ) |
52 | 18, 51 | resubcld 11139 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℝ) |
53 | 52, 13 | rerpdivcld 12538 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) |
54 | 53 | recnd 10740 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥) ∈ ℂ) |
55 | 54 | lo1o12 14973 |
. . . 4
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ ((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
(abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) ∈
≤𝑂(1))) |
56 | 3, 55 | mpbii 236 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) ∈ ≤𝑂(1)) |
57 | 54 | abscld 14879 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) ∈ ℝ) |
58 | 16 | recnd 10740 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑅‘𝑥) ∈ ℂ) |
59 | 58 | abscld 14879 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(𝑅‘𝑥)) ∈ ℝ) |
60 | 59, 17 | remulcld 10742 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (log‘𝑥)) ∈ ℝ) |
61 | 26 | recnd 10740 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑅‘(𝑥 / 𝑛)) ∈ ℂ) |
62 | 61 | abscld 14879 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘(𝑅‘(𝑥 / 𝑛))) ∈ ℝ) |
63 | 22 | nnred 11724 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℝ) |
64 | | pntsval.1 |
. . . . . . . . . . . 12
⊢ 𝑆 = (𝑎 ∈ ℝ ↦ Σ𝑖 ∈
(1...(⌊‘𝑎))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑎 / 𝑖))))) |
65 | 64 | pntsf 26301 |
. . . . . . . . . . 11
⊢ 𝑆:ℝ⟶ℝ |
66 | 65 | ffvelrni 6854 |
. . . . . . . . . 10
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) ∈ ℝ) |
67 | 63, 66 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) ∈ ℝ) |
68 | | 1red 10713 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℝ) |
69 | 63, 68 | resubcld 11139 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℝ) |
70 | 65 | ffvelrni 6854 |
. . . . . . . . . 10
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) ∈
ℝ) |
71 | 69, 70 | syl 17 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℝ) |
72 | 67, 71 | resubcld 11139 |
. . . . . . . 8
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) ∈
ℝ) |
73 | 62, 72 | remulcld 10742 |
. . . . . . 7
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
74 | 19, 73 | fsumrecl 15177 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) ∈
ℝ) |
75 | 74, 50 | rerpdivcld 12538 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥)) ∈
ℝ) |
76 | 60, 75 | resubcld 11139 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ∈
ℝ) |
77 | 76, 13 | rerpdivcld 12538 |
. . 3
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ∈ ℝ) |
78 | 17 | recnd 10740 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) |
79 | 58, 78 | mulcld 10732 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((𝑅‘𝑥) · (log‘𝑥)) ∈ ℂ) |
80 | 49 | recnd 10740 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℂ) |
81 | 50 | rpne0d 12512 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) |
82 | 80, 78, 81 | divcld 11487 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)) ∈
ℂ) |
83 | 79, 82 | subcld 11068 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℂ) |
84 | 83 | abscld 14879 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) ∈
ℝ) |
85 | 80 | abscld 14879 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
86 | 85, 50 | rerpdivcld 12538 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)) ∈
ℝ) |
87 | 60, 86 | resubcld 11139 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) ∈
ℝ) |
88 | 48 | recnd 10740 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) ∈
ℂ) |
89 | 88 | abscld 14879 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
90 | 19, 89 | fsumrecl 15177 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ∈
ℝ) |
91 | 19, 88 | fsumabs 15242 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) |
92 | 47 | recnd 10740 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))) ∈
ℂ) |
93 | 61, 92 | absmuld 14897 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) = ((abs‘(𝑅‘(𝑥 / 𝑛))) · (abs‘(Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))))) |
94 | 92 | abscld 14879 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
∈ ℝ) |
95 | 61 | absge0d 14887 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(abs‘(𝑅‘(𝑥 / 𝑛)))) |
96 | 42 | recnd 10740 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) ∈ ℂ) |
97 | 46 | recnd 10740 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· (log‘𝑛))
∈ ℂ) |
98 | 96, 97 | abs2dif2d 14901 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
≤ ((abs‘Σ𝑚
∈ {𝑦 ∈ ℕ
∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) +
(abs‘((Λ‘𝑛) · (log‘𝑛))))) |
99 | 71 | recnd 10740 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) ∈ ℂ) |
100 | 96, 97 | addcld 10731 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))) ∈ ℂ) |
101 | 99, 100 | pncan2d 11070 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) − (𝑆‘(𝑛 − 1))) = (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) |
102 | | elfzuz 12987 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
(ℤ≥‘1)) |
103 | 102 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈
(ℤ≥‘1)) |
104 | | elfznn 13020 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ (1...𝑛) → 𝑘 ∈ ℕ) |
105 | 104 | adantl 485 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℕ) |
106 | | vmacl 25847 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 ∈ ℕ →
(Λ‘𝑘) ∈
ℝ) |
107 | 105, 106 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (Λ‘𝑘) ∈ ℝ) |
108 | 105 | nnrpd 12505 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → 𝑘 ∈ ℝ+) |
109 | 108 | relogcld 25358 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (log‘𝑘) ∈ ℝ) |
110 | 107, 109 | remulcld 10742 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → ((Λ‘𝑘) · (log‘𝑘)) ∈ ℝ) |
111 | | fzfid 13425 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (1...𝑘) ∈ Fin) |
112 | | dvdsssfz1 15756 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑘 ∈ ℕ → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) |
113 | 105, 112 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ (1...𝑘)) |
114 | 111, 113 | ssfid 8812 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ∈ Fin) |
115 | | ssrab2 3967 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ⊆ ℕ |
116 | | simpr 488 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
117 | 115, 116 | sseldi 3873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → 𝑚 ∈ ℕ) |
118 | 117, 34 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘𝑚) ∈ ℝ) |
119 | | dvdsdivcl 15754 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ ((𝑘 ∈ ℕ ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
120 | 105, 119 | sylan 583 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) |
121 | 115, 120 | sseldi 3873 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (𝑘 / 𝑚) ∈ ℕ) |
122 | | vmacl 25847 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ ((𝑘 / 𝑚) ∈ ℕ →
(Λ‘(𝑘 / 𝑚)) ∈
ℝ) |
123 | 121, 122 | syl 17 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → (Λ‘(𝑘 / 𝑚)) ∈ ℝ) |
124 | 118, 123 | remulcld 10742 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((((⊤ ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑘 ∈ (1...𝑛)) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘}) → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) ∈ ℝ) |
125 | 114, 124 | fsumrecl 15177 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) ∈ ℝ) |
126 | 110, 125 | readdcld 10741 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) ∈ ℝ) |
127 | 126 | recnd 10740 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑘 ∈ (1...𝑛)) → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) ∈ ℂ) |
128 | | fveq2 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (Λ‘𝑘) = (Λ‘𝑛)) |
129 | | fveq2 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → (log‘𝑘) = (log‘𝑛)) |
130 | 128, 129 | oveq12d 7182 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑛) · (log‘𝑛))) |
131 | | breq2 5031 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑛 → (𝑦 ∥ 𝑘 ↔ 𝑦 ∥ 𝑛)) |
132 | 131 | rabbidv 3380 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑘 = 𝑛 → {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} = {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) |
133 | | fvoveq1 7187 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑘 = 𝑛 → (Λ‘(𝑘 / 𝑚)) = (Λ‘(𝑛 / 𝑚))) |
134 | 133 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑘 = 𝑛 → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
135 | 134 | adantr 484 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑘 = 𝑛 ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
136 | 132, 135 | sumeq12rdv 15150 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑘 = 𝑛 → Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))) = Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
137 | 130, 136 | oveq12d 7182 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑘 = 𝑛 → (((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
138 | 103, 127,
137 | fsumm1 15192 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = (Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) + (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))) |
139 | 64 | pntsval2 26304 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℝ → (𝑆‘𝑛) = Σ𝑘 ∈ (1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
140 | 63, 139 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = Σ𝑘 ∈ (1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
141 | 22 | nnzd 12160 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℤ) |
142 | | flid 13262 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑛 ∈ ℤ →
(⌊‘𝑛) = 𝑛) |
143 | 141, 142 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘𝑛) = 𝑛) |
144 | 143 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘𝑛)) =
(1...𝑛)) |
145 | 144 | sumeq1d 15144 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈
(1...(⌊‘𝑛))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
146 | 140, 145 | eqtrd 2773 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = Σ𝑘 ∈ (1...𝑛)(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
147 | 64 | pntsval2 26304 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 − 1) ∈ ℝ
→ (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈
(1...(⌊‘(𝑛
− 1)))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
148 | 69, 147 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈ (1...(⌊‘(𝑛 −
1)))(((Λ‘𝑘)
· (log‘𝑘)) +
Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
149 | | 1zzd 12087 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ∈
ℤ) |
150 | 141, 149 | zsubcld 12166 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑛 − 1) ∈ ℤ) |
151 | | flid 13262 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ ((𝑛 − 1) ∈ ℤ
→ (⌊‘(𝑛
− 1)) = (𝑛 −
1)) |
152 | 150, 151 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (⌊‘(𝑛 − 1)) = (𝑛 − 1)) |
153 | 152 | oveq2d 7180 |
. . . . . . . . . . . . . . . . . . . 20
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑛
− 1))) = (1...(𝑛
− 1))) |
154 | 153 | sumeq1d 15144 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑘 ∈
(1...(⌊‘(𝑛
− 1)))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) = Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
155 | 148, 154 | eqtrd 2773 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘(𝑛 − 1)) = Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚))))) |
156 | 96, 97 | addcomd 10913 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))) = (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))))) |
157 | 155, 156 | oveq12d 7182 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) = (Σ𝑘 ∈ (1...(𝑛 − 1))(((Λ‘𝑘) · (log‘𝑘)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘} ((Λ‘𝑚) · (Λ‘(𝑘 / 𝑚)))) + (((Λ‘𝑛) · (log‘𝑛)) + Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))))) |
158 | 138, 146,
157 | 3eqtr4d 2783 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑆‘𝑛) = ((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛))))) |
159 | 158 | oveq1d 7179 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) = (((𝑆‘(𝑛 − 1)) + (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) − (𝑆‘(𝑛 − 1)))) |
160 | | vmage0 25850 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑚 ∈ ℕ → 0 ≤
(Λ‘𝑚)) |
161 | 33, 160 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ (Λ‘𝑚)) |
162 | | vmage0 25850 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((𝑛 / 𝑚) ∈ ℕ → 0 ≤
(Λ‘(𝑛 / 𝑚))) |
163 | 38, 162 | syl 17 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ (Λ‘(𝑛 / 𝑚))) |
164 | 35, 40, 161, 163 | mulge0d 11288 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛}) → 0 ≤ ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) |
165 | 30, 41, 164 | fsumge0 15236 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤ Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
166 | 42, 165 | absidd 14865 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) = Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) |
167 | | vmage0 25850 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
168 | 22, 167 | syl 17 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(Λ‘𝑛)) |
169 | 22 | nnge1d 11757 |
. . . . . . . . . . . . . . . . . . 19
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 1 ≤ 𝑛) |
170 | 63, 169 | logge0d 25365 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
(log‘𝑛)) |
171 | 44, 45, 168, 170 | mulge0d 11288 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 0 ≤
((Λ‘𝑛)
· (log‘𝑛))) |
172 | 46, 171 | absidd 14865 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘((Λ‘𝑛) · (log‘𝑛))) = ((Λ‘𝑛) · (log‘𝑛))) |
173 | 166, 172 | oveq12d 7182 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((abs‘Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚)))) +
(abs‘((Λ‘𝑛) · (log‘𝑛)))) = (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) + ((Λ‘𝑛) · (log‘𝑛)))) |
174 | 101, 159,
173 | 3eqtr4d 2783 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))) = ((abs‘Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚)))) + (abs‘((Λ‘𝑛) · (log‘𝑛))))) |
175 | 98, 174 | breqtrrd 5055 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(abs‘(Σ𝑚 ∈
{𝑦 ∈ ℕ ∣
𝑦 ∥ 𝑛} ((Λ‘𝑚) ·
(Λ‘(𝑛 / 𝑚))) −
((Λ‘𝑛)
· (log‘𝑛))))
≤ ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) |
176 | 94, 72, 62, 95, 175 | lemul2ad 11651 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → ((abs‘(𝑅‘(𝑥 / 𝑛))) · (abs‘(Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
177 | 93, 176 | eqbrtrd 5049 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ ((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
178 | 19, 89, 73, 177 | fsumle 15240 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
179 | 85, 90, 74, 91, 178 | letrd 10868 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) ≤ Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1))))) |
180 | 85, 74, 50, 179 | lediv1dd 12565 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)) ≤ (Σ𝑛 ∈
(1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) |
181 | 86, 75, 60, 180 | lesub2dd 11328 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ≤ (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)))) |
182 | 58, 78 | absmuld 14897 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((𝑅‘𝑥) · (log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (abs‘(log‘𝑥)))) |
183 | 5, 12 | logge0d 25365 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ (log‘𝑥)) |
184 | 17, 183 | absidd 14865 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(log‘𝑥)) = (log‘𝑥)) |
185 | 184 | oveq2d 7180 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(𝑅‘𝑥)) · (abs‘(log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (log‘𝑥))) |
186 | 182, 185 | eqtrd 2773 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((𝑅‘𝑥) · (log‘𝑥))) = ((abs‘(𝑅‘𝑥)) · (log‘𝑥))) |
187 | 80, 78, 81 | absdivd 14898 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) /
(abs‘(log‘𝑥)))) |
188 | 184 | oveq2d 7180 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) /
(abs‘(log‘𝑥)))
= ((abs‘Σ𝑛
∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) |
189 | 187, 188 | eqtrd 2773 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) = ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) |
190 | 186, 189 | oveq12d 7182 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘((𝑅‘𝑥) · (log‘𝑥))) − (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) = (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥)))) |
191 | 79, 82 | abs2difd 14900 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘((𝑅‘𝑥) · (log‘𝑥))) − (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
192 | 190, 191 | eqbrtrrd 5051 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − ((abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛))))) / (log‘𝑥))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
193 | 76, 87, 84, 181, 192 | letrd 10868 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) ≤ (abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))))) |
194 | 76, 84, 13, 193 | lediv1dd 12565 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
195 | 52 | recnd 10740 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) ∈
ℂ) |
196 | 5 | recnd 10740 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℂ) |
197 | 13 | rpne0d 12512 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ≠ 0) |
198 | 195, 196,
197 | absdivd 14898 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / (abs‘𝑥))) |
199 | 13 | rpge0d 12511 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 0 ≤ 𝑥) |
200 | 5, 199 | absidd 14865 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘𝑥) = 𝑥) |
201 | 200 | oveq2d 7180 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / (abs‘𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
202 | 198, 201 | eqtrd 2773 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥)) = ((abs‘(((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥)))) / 𝑥)) |
203 | 194, 202 | breqtrrd 5055 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) |
204 | 203 | adantrr 717 |
. . 3
⊢
((⊤ ∧ (𝑥
∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥) ≤ (abs‘((((𝑅‘𝑥) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((𝑅‘(𝑥 / 𝑛)) · (Σ𝑚 ∈ {𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑛} ((Λ‘𝑚) · (Λ‘(𝑛 / 𝑚))) − ((Λ‘𝑛) · (log‘𝑛)))) / (log‘𝑥))) / 𝑥))) |
205 | 1, 56, 57, 77, 204 | lo1le 15094 |
. 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1)) |
206 | 205 | mptru 1549 |
1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((abs‘(𝑅‘𝑥)) · (log‘𝑥)) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((abs‘(𝑅‘(𝑥 / 𝑛))) · ((𝑆‘𝑛) − (𝑆‘(𝑛 − 1)))) / (log‘𝑥))) / 𝑥)) ∈ ≤𝑂(1) |