Step | Hyp | Ref
| Expression |
1 | | 1red 10055 |
. 2
⊢ (𝜑 → 1 ∈
ℝ) |
2 | | ioossre 12235 |
. . . 4
⊢
(1(,)+∞) ⊆ ℝ |
3 | | selberg3lem1.1 |
. . . . 5
⊢ (𝜑 → 𝐴 ∈
ℝ+) |
4 | 3 | rpcnd 11874 |
. . . 4
⊢ (𝜑 → 𝐴 ∈ ℂ) |
5 | | o1const 14350 |
. . . 4
⊢
(((1(,)+∞) ⊆ ℝ ∧ 𝐴 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈
𝑂(1)) |
6 | 2, 4, 5 | sylancr 695 |
. . 3
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ 𝐴) ∈
𝑂(1)) |
7 | | fzfid 12772 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(1...(⌊‘𝑥))
∈ Fin) |
8 | | elfznn 12370 |
. . . . . . . . . 10
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
9 | 8 | adantl 482 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℕ) |
10 | | vmacl 24844 |
. . . . . . . . 9
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
11 | 9, 10 | syl 17 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℝ) |
12 | 11, 9 | nndivred 11069 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℝ) |
13 | 7, 12 | fsumrecl 14465 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℝ) |
14 | | elioore 12205 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
15 | | eliooord 12233 |
. . . . . . . . . 10
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
16 | 15 | simpld 475 |
. . . . . . . . 9
⊢ (𝑥 ∈ (1(,)+∞) → 1
< 𝑥) |
17 | 14, 16 | rplogcld 24375 |
. . . . . . . 8
⊢ (𝑥 ∈ (1(,)+∞) →
(log‘𝑥) ∈
ℝ+) |
18 | | rpdivcl 11856 |
. . . . . . . 8
⊢ ((𝐴 ∈ ℝ+
∧ (log‘𝑥) ∈
ℝ+) → (𝐴 / (log‘𝑥)) ∈
ℝ+) |
19 | 3, 17, 18 | syl2an 494 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈
ℝ+) |
20 | 19 | rpred 11872 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈ ℝ) |
21 | 13, 20 | remulcld 10070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ∈ ℝ) |
22 | 21 | recnd 10068 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ∈ ℂ) |
23 | 4 | adantr 481 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℂ) |
24 | 13 | recnd 10068 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) ∈ ℂ) |
25 | 17 | adantl 482 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ+) |
26 | 25 | rpcnd 11874 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℂ) |
27 | 19 | rpcnd 11874 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 / (log‘𝑥)) ∈ ℂ) |
28 | 24, 26, 27 | subdird 10487 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − ((log‘𝑥) · (𝐴 / (log‘𝑥))))) |
29 | 25 | rpne0d 11877 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ≠
0) |
30 | 23, 26, 29 | divcan2d 10803 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((log‘𝑥) ·
(𝐴 / (log‘𝑥))) = 𝐴) |
31 | 30 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − ((log‘𝑥) · (𝐴 / (log‘𝑥)))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴)) |
32 | 28, 31 | eqtrd 2656 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥))) = ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴)) |
33 | 32 | mpteq2dva 4744 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥)))) = (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴))) |
34 | 25 | rpred 11872 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(log‘𝑥) ∈
ℝ) |
35 | 13, 34 | resubcld 10458 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) ∈ ℝ) |
36 | 14 | adantl 482 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ) |
37 | | 0red 10041 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ∈
ℝ) |
38 | | 1red 10055 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 ∈
ℝ) |
39 | | 0lt1 10550 |
. . . . . . . . . . . 12
⊢ 0 <
1 |
40 | 39 | a1i 11 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 <
1) |
41 | 16 | adantl 482 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 1 < 𝑥) |
42 | 37, 38, 36, 40, 41 | lttrd 10198 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 < 𝑥) |
43 | 36, 42 | elrpd 11869 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℝ+) |
44 | 43 | ex 450 |
. . . . . . . 8
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) → 𝑥 ∈
ℝ+)) |
45 | 44 | ssrdv 3609 |
. . . . . . 7
⊢ (𝜑 → (1(,)+∞) ⊆
ℝ+) |
46 | | vmadivsum 25171 |
. . . . . . . 8
⊢ (𝑥 ∈ ℝ+
↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1) |
47 | 46 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (𝑥 ∈ ℝ+ ↦
(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
48 | 45, 47 | o1res2 14294 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥))) ∈ 𝑂(1)) |
49 | 2 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → (1(,)+∞) ⊆
ℝ) |
50 | | ere 14819 |
. . . . . . . 8
⊢ e ∈
ℝ |
51 | 50 | a1i 11 |
. . . . . . 7
⊢ (𝜑 → e ∈
ℝ) |
52 | 3 | rpred 11872 |
. . . . . . 7
⊢ (𝜑 → 𝐴 ∈ ℝ) |
53 | 19 | adantrr 753 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ∈
ℝ+) |
54 | 53 | rprege0d 11879 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → ((𝐴 / (log‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝐴 / (log‘𝑥)))) |
55 | | absid 14036 |
. . . . . . . . 9
⊢ (((𝐴 / (log‘𝑥)) ∈ ℝ ∧ 0 ≤ (𝐴 / (log‘𝑥))) → (abs‘(𝐴 / (log‘𝑥))) = (𝐴 / (log‘𝑥))) |
56 | 54, 55 | syl 17 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (abs‘(𝐴 / (log‘𝑥))) = (𝐴 / (log‘𝑥))) |
57 | | loge 24333 |
. . . . . . . . . . 11
⊢
(log‘e) = 1 |
58 | | simprr 796 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → e ≤ 𝑥) |
59 | | epr 14936 |
. . . . . . . . . . . . 13
⊢ e ∈
ℝ+ |
60 | 43 | adantrr 753 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝑥 ∈ ℝ+) |
61 | | logleb 24349 |
. . . . . . . . . . . . 13
⊢ ((e
∈ ℝ+ ∧ 𝑥 ∈ ℝ+) → (e ≤
𝑥 ↔ (log‘e) ≤
(log‘𝑥))) |
62 | 59, 60, 61 | sylancr 695 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (e ≤ 𝑥 ↔ (log‘e) ≤
(log‘𝑥))) |
63 | 58, 62 | mpbid 222 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (log‘e) ≤
(log‘𝑥)) |
64 | 57, 63 | syl5eqbrr 4689 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 1 ≤
(log‘𝑥)) |
65 | | 1rp 11836 |
. . . . . . . . . . . 12
⊢ 1 ∈
ℝ+ |
66 | | rpregt0 11846 |
. . . . . . . . . . . 12
⊢ (1 ∈
ℝ+ → (1 ∈ ℝ ∧ 0 < 1)) |
67 | 65, 66 | mp1i 13 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (1 ∈ ℝ
∧ 0 < 1)) |
68 | 25 | adantrr 753 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (log‘𝑥) ∈
ℝ+) |
69 | 68 | rpregt0d 11878 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → ((log‘𝑥) ∈ ℝ ∧ 0 <
(log‘𝑥))) |
70 | 3 | adantr 481 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝐴 ∈
ℝ+) |
71 | 70 | rpregt0d 11878 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 ∈ ℝ ∧ 0 < 𝐴)) |
72 | | lediv2 10913 |
. . . . . . . . . . 11
⊢ (((1
∈ ℝ ∧ 0 < 1) ∧ ((log‘𝑥) ∈ ℝ ∧ 0 <
(log‘𝑥)) ∧ (𝐴 ∈ ℝ ∧ 0 <
𝐴)) → (1 ≤
(log‘𝑥) ↔ (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1))) |
73 | 67, 69, 71, 72 | syl3anc 1326 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (1 ≤
(log‘𝑥) ↔ (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1))) |
74 | 64, 73 | mpbid 222 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ≤ (𝐴 / 1)) |
75 | 4 | adantr 481 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → 𝐴 ∈ ℂ) |
76 | 75 | div1d 10793 |
. . . . . . . . 9
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / 1) = 𝐴) |
77 | 74, 76 | breqtrd 4679 |
. . . . . . . 8
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (𝐴 / (log‘𝑥)) ≤ 𝐴) |
78 | 56, 77 | eqbrtrd 4675 |
. . . . . . 7
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ e ≤ 𝑥)) → (abs‘(𝐴 / (log‘𝑥))) ≤ 𝐴) |
79 | 49, 27, 51, 52, 78 | elo1d 14267 |
. . . . . 6
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (𝐴 / (log‘𝑥))) ∈ 𝑂(1)) |
80 | 35, 20, 48, 79 | o1mul2 14355 |
. . . . 5
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) − (log‘𝑥)) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1)) |
81 | 33, 80 | eqeltrrd 2702 |
. . . 4
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) − 𝐴)) ∈ 𝑂(1)) |
82 | 22, 23, 81 | o1dif 14360 |
. . 3
⊢ (𝜑 → ((𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1) ↔ (𝑥 ∈ (1(,)+∞) ↦
𝐴) ∈
𝑂(1))) |
83 | 6, 82 | mpbird 247 |
. 2
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ 𝑂(1)) |
84 | | 2re 11090 |
. . . . . . 7
⊢ 2 ∈
ℝ |
85 | | rerpdivcl 11861 |
. . . . . . 7
⊢ ((2
∈ ℝ ∧ (log‘𝑥) ∈ ℝ+) → (2 /
(log‘𝑥)) ∈
ℝ) |
86 | 84, 25, 85 | sylancr 695 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 /
(log‘𝑥)) ∈
ℝ) |
87 | | nndivre 11056 |
. . . . . . . . . . 11
⊢ ((𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ) → (𝑥 / 𝑛) ∈ ℝ) |
88 | 36, 8, 87 | syl2an 494 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ) |
89 | | chpcl 24850 |
. . . . . . . . . 10
⊢ ((𝑥 / 𝑛) ∈ ℝ → (ψ‘(𝑥 / 𝑛)) ∈ ℝ) |
90 | 88, 89 | syl 17 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑛)) ∈
ℝ) |
91 | 11, 90 | remulcld 10070 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (ψ‘(𝑥 /
𝑛))) ∈
ℝ) |
92 | 9 | nnrpd 11870 |
. . . . . . . . 9
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℝ+) |
93 | 92 | relogcld 24369 |
. . . . . . . 8
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℝ) |
94 | 91, 93 | remulcld 10070 |
. . . . . . 7
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
· (ψ‘(𝑥 /
𝑛))) ·
(log‘𝑛)) ∈
ℝ) |
95 | 7, 94 | fsumrecl 14465 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℝ) |
96 | 86, 95 | remulcld 10070 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℝ) |
97 | 7, 91 | fsumrecl 14465 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℝ) |
98 | 96, 97 | resubcld 10458 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) ∈ ℝ) |
99 | 98, 43 | rerpdivcld 11903 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℝ) |
100 | 99 | recnd 10068 |
. 2
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) ∈ ℂ) |
101 | 100 | abscld 14175 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ ℝ) |
102 | 22 | abscld 14175 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) ∈ ℝ) |
103 | | 2cnd 11093 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 2 ∈
ℂ) |
104 | 95 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) ∈ ℂ) |
105 | 103, 104 | mulcld 10060 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) ∈ ℂ) |
106 | 97 | recnd 10068 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) ∈ ℂ) |
107 | 106, 26 | mulcld 10060 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) ∈ ℂ) |
108 | 105, 107 | subcld 10392 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) ∈ ℂ) |
109 | 108 | abscld 14175 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ∈ ℝ) |
110 | 42 | gt0ne0d 10592 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ≠ 0) |
111 | 109, 36, 110 | redivcld 10853 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ∈ ℝ) |
112 | 52 | adantr 481 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝐴 ∈
ℝ) |
113 | 13, 112 | remulcld 10070 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ∈ ℝ) |
114 | 11 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑛)
∈ ℂ) |
115 | | fzfid 12772 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑛))) ∈ Fin) |
116 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) |
117 | 116 | adantl 482 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 𝑚 ∈
ℕ) |
118 | | vmacl 24844 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
119 | 117, 118 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
(Λ‘𝑚) ∈
ℝ) |
120 | 117 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) → 𝑚 ∈
ℝ+) |
121 | 120 | relogcld 24369 |
. . . . . . . . . . . . . . . 16
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
(log‘𝑚) ∈
ℝ) |
122 | 119, 121 | remulcld 10070 |
. . . . . . . . . . . . . . 15
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((Λ‘𝑚)
· (log‘𝑚))
∈ ℝ) |
123 | 115, 122 | fsumrecl 14465 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) ∈
ℝ) |
124 | 8 | nnrpd 11870 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℝ+) |
125 | | rpdivcl 11856 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 ∈ ℝ+
∧ 𝑛 ∈
ℝ+) → (𝑥 / 𝑛) ∈
ℝ+) |
126 | 43, 124, 125 | syl2an 494 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℝ+) |
127 | 126 | relogcld 24369 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) ∈
ℝ) |
128 | 90, 127 | remulcld 10070 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑥 /
𝑛)) ·
(log‘(𝑥 / 𝑛))) ∈
ℝ) |
129 | 123, 128 | resubcld 10458 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) ∈ ℝ) |
130 | 129 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) ∈ ℂ) |
131 | 114, 130 | mulcld 10060 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℂ) |
132 | 7, 131 | fsumcl 14464 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℂ) |
133 | 132 | abscld 14175 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ) |
134 | 131 | abscld 14175 |
. . . . . . . . . 10
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ) |
135 | 7, 134 | fsumrecl 14465 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ∈ ℝ) |
136 | 112, 36 | remulcld 10070 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · 𝑥) ∈ ℝ) |
137 | 13, 136 | remulcld 10070 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) ∈ ℝ) |
138 | 7, 131 | fsumabs 14533 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))))) |
139 | 52 | ad2antrr 762 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈
ℝ) |
140 | 36 | adantr 481 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
141 | 139, 140 | remulcld 10070 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 · 𝑥) ∈
ℝ) |
142 | 12, 141 | remulcld 10070 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · (𝐴 · 𝑥)) ∈ ℝ) |
143 | 130 | abscld 14175 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ∈ ℝ) |
144 | 141, 9 | nndivred 11069 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝐴 · 𝑥) / 𝑛) ∈ ℝ) |
145 | | vmage0 24847 |
. . . . . . . . . . . . . 14
⊢ (𝑛 ∈ ℕ → 0 ≤
(Λ‘𝑛)) |
146 | 9, 145 | syl 17 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (Λ‘𝑛)) |
147 | 88 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
ℂ) |
148 | 126 | rpne0d 11877 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ≠ 0) |
149 | 130, 147,
148 | absdivd 14194 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (abs‘(𝑥 / 𝑛)))) |
150 | 126 | rpge0d 11876 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 0 ≤ (𝑥 / 𝑛)) |
151 | 88, 150 | absidd 14161 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(𝑥 /
𝑛)) = (𝑥 / 𝑛)) |
152 | 151 | oveq2d 6666 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (abs‘(𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛))) |
153 | 149, 152 | eqtrd 2656 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) = ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛))) |
154 | 9 | nncnd 11036 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ∈
ℂ) |
155 | 154 | mulid2d 10058 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑛) =
𝑛) |
156 | | fznnfl 12661 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑥 ∈ ℝ → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
157 | 36, 156 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑛 ∈
(1...(⌊‘𝑥))
↔ (𝑛 ∈ ℕ
∧ 𝑛 ≤ 𝑥))) |
158 | 157 | simplbda 654 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≤ 𝑥) |
159 | 155, 158 | eqbrtrd 4675 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (1 · 𝑛) ≤
𝑥) |
160 | | 1red 10055 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ∈ ℝ) |
161 | 160, 140,
92 | lemuldivd 11921 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((1 · 𝑛) ≤
𝑥 ↔ 1 ≤ (𝑥 / 𝑛))) |
162 | 159, 161 | mpbid 222 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 1 ≤ (𝑥 / 𝑛)) |
163 | | 1re 10039 |
. . . . . . . . . . . . . . . . . . 19
⊢ 1 ∈
ℝ |
164 | | elicopnf 12269 |
. . . . . . . . . . . . . . . . . . 19
⊢ (1 ∈
ℝ → ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔
((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛)))) |
165 | 163, 164 | ax-mp 5 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 / 𝑛) ∈ (1[,)+∞) ↔ ((𝑥 / 𝑛) ∈ ℝ ∧ 1 ≤ (𝑥 / 𝑛))) |
166 | 88, 162, 165 | sylanbrc 698 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑛) ∈
(1[,)+∞)) |
167 | | selberg3lem1.2 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝜑 → ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴) |
168 | 167 | ad2antrr 762 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴) |
169 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑚 → (Λ‘𝑘) = (Λ‘𝑚)) |
170 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑘 = 𝑚 → (log‘𝑘) = (log‘𝑚)) |
171 | 169, 170 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑘 = 𝑚 → ((Λ‘𝑘) · (log‘𝑘)) = ((Λ‘𝑚) · (log‘𝑚))) |
172 | 171 | cbvsumv 14426 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢
Σ𝑘 ∈
(1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) |
173 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . . . 25
⊢ (𝑦 = (𝑥 / 𝑛) → (⌊‘𝑦) = (⌊‘(𝑥 / 𝑛))) |
174 | 173 | oveq2d 6666 |
. . . . . . . . . . . . . . . . . . . . . . . 24
⊢ (𝑦 = (𝑥 / 𝑛) → (1...(⌊‘𝑦)) = (1...(⌊‘(𝑥 / 𝑛)))) |
175 | 174 | sumeq1d 14431 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑚 ∈ (1...(⌊‘𝑦))((Λ‘𝑚) · (log‘𝑚)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) |
176 | 172, 175 | syl5eq 2668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑥 / 𝑛) → Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) |
177 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑥 / 𝑛) → (ψ‘𝑦) = (ψ‘(𝑥 / 𝑛))) |
178 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑦 = (𝑥 / 𝑛) → (log‘𝑦) = (log‘(𝑥 / 𝑛))) |
179 | 177, 178 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑦 = (𝑥 / 𝑛) → ((ψ‘𝑦) · (log‘𝑦)) = ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) |
180 | 176, 179 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑥 / 𝑛) → (Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) |
181 | | id 22 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (𝑦 = (𝑥 / 𝑛) → 𝑦 = (𝑥 / 𝑛)) |
182 | 180, 181 | oveq12d 6668 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (𝑦 = (𝑥 / 𝑛) → ((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) |
183 | 182 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑦 = (𝑥 / 𝑛) → (abs‘((Σ𝑘 ∈
(1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) = (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛)))) |
184 | 183 | breq1d 4663 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑦 = (𝑥 / 𝑛) → ((abs‘((Σ𝑘 ∈
(1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴 ↔ (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) ≤ 𝐴)) |
185 | 184 | rspcv 3305 |
. . . . . . . . . . . . . . . . 17
⊢ ((𝑥 / 𝑛) ∈ (1[,)+∞) → (∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑘 ∈ (1...(⌊‘𝑦))((Λ‘𝑘) · (log‘𝑘)) − ((ψ‘𝑦) · (log‘𝑦))) / 𝑦)) ≤ 𝐴 → (abs‘((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) ≤ 𝐴)) |
186 | 166, 168,
185 | sylc 65 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) / (𝑥 / 𝑛))) ≤ 𝐴) |
187 | 153, 186 | eqbrtrrd 4677 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)) ≤ 𝐴) |
188 | 143, 139,
126 | ledivmul2d 11926 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) / (𝑥 / 𝑛)) ≤ 𝐴 ↔ (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ (𝐴 · (𝑥 / 𝑛)))) |
189 | 187, 188 | mpbid 222 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ (𝐴 · (𝑥 / 𝑛))) |
190 | 23 | adantr 481 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝐴 ∈
ℂ) |
191 | 140 | recnd 10068 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℂ) |
192 | 9 | nnne0d 11065 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑛 ≠
0) |
193 | 190, 191,
154, 192 | divassd 10836 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((𝐴 · 𝑥) / 𝑛) = (𝐴 · (𝑥 / 𝑛))) |
194 | 189, 193 | breqtrrd 4681 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Σ𝑚
∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) ≤ ((𝐴 · 𝑥) / 𝑛)) |
195 | 143, 144,
11, 146, 194 | lemul2ad 10964 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (abs‘(Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ ((Λ‘𝑛) · ((𝐴 · 𝑥) / 𝑛))) |
196 | 114, 130 | absmuld 14193 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((abs‘(Λ‘𝑛)) ·
(abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))))) |
197 | 11, 146 | absidd 14161 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘(Λ‘𝑛)) = (Λ‘𝑛)) |
198 | 197 | oveq1d 6665 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((abs‘(Λ‘𝑛)) · (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((Λ‘𝑛) · (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))))) |
199 | 196, 198 | eqtrd 2656 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) = ((Λ‘𝑛) · (abs‘(Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))))) |
200 | 141 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (𝐴 · 𝑥) ∈
ℂ) |
201 | 114, 154,
200, 192 | div32d 10824 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
/ 𝑛) · (𝐴 · 𝑥)) = ((Λ‘𝑛) · ((𝐴 · 𝑥) / 𝑛))) |
202 | 195, 199,
201 | 3brtr4d 4685 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (abs‘((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥))) |
203 | 7, 134, 142, 202 | fsumle 14531 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥))) |
204 | 36 | recnd 10068 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 𝑥 ∈
ℂ) |
205 | 23, 204 | mulcld 10060 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝐴 · 𝑥) ∈ ℂ) |
206 | 114, 154,
192 | divcld 10801 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
/ 𝑛) ∈
ℂ) |
207 | 7, 205, 206 | fsummulc1 14517 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥))) |
208 | 203, 207 | breqtrrd 4681 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(abs‘((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥))) |
209 | 133, 135,
137, 138, 208 | letrd 10194 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥))) |
210 | 123 | recnd 10068 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) ∈
ℂ) |
211 | 90 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑛)) ∈
ℂ) |
212 | 93 | recnd 10068 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑛) ∈
ℂ) |
213 | 211, 212 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑥 /
𝑛)) ·
(log‘𝑛)) ∈
ℂ) |
214 | 210, 213 | addcld 10059 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) ∈ ℂ) |
215 | 114, 214 | mulcld 10060 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) ∈ ℂ) |
216 | 114, 211 | mulcld 10060 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (ψ‘(𝑥 /
𝑛))) ∈
ℂ) |
217 | 26 | adantr 481 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑥) ∈
ℂ) |
218 | 216, 217 | mulcld 10060 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
· (ψ‘(𝑥 /
𝑛))) ·
(log‘𝑥)) ∈
ℂ) |
219 | 7, 215, 218 | fsumsub 14520 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) |
220 | 211, 217 | mulcld 10060 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑥 /
𝑛)) ·
(log‘𝑥)) ∈
ℂ) |
221 | 114, 214,
220 | subdid 10486 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))) |
222 | 43 | adantr 481 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ+) |
223 | 222, 92 | relogdivd 24372 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (log‘(𝑥 /
𝑛)) = ((log‘𝑥) − (log‘𝑛))) |
224 | 223 | oveq2d 6666 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑥 /
𝑛)) ·
(log‘(𝑥 / 𝑛))) = ((ψ‘(𝑥 / 𝑛)) · ((log‘𝑥) − (log‘𝑛)))) |
225 | 211, 217,
212 | subdid 10486 |
. . . . . . . . . . . . . . . 16
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑥 /
𝑛)) ·
((log‘𝑥) −
(log‘𝑛))) =
(((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) |
226 | 224, 225 | eqtrd 2656 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑥 /
𝑛)) ·
(log‘(𝑥 / 𝑛))) = (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) |
227 | 226 | oveq2d 6666 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))) |
228 | 210, 220,
213 | subsub3d 10422 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − (((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))) |
229 | 227, 228 | eqtrd 2656 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))) = ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥)))) |
230 | 229 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = ((Λ‘𝑛) · ((Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))) − ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))) |
231 | 114, 211,
217 | mulassd 10063 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
· (ψ‘(𝑥 /
𝑛))) ·
(log‘𝑥)) =
((Λ‘𝑛)
· ((ψ‘(𝑥 /
𝑛)) ·
(log‘𝑥)))) |
232 | 231 | oveq2d 6666 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
· (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑥))))) |
233 | 221, 230,
232 | 3eqtr4d 2666 |
. . . . . . . . . . 11
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = (((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) |
234 | 233 | sumeq2dv 14433 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) |
235 | | fveq2 6191 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (Λ‘𝑛) = (Λ‘𝑚)) |
236 | | oveq2 6658 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑛 = 𝑚 → (𝑥 / 𝑛) = (𝑥 / 𝑚)) |
237 | 236 | fveq2d 6195 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 = 𝑚 → (ψ‘(𝑥 / 𝑛)) = (ψ‘(𝑥 / 𝑚))) |
238 | 235, 237 | oveq12d 6668 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → ((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) = ((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) |
239 | | fveq2 6191 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 = 𝑚 → (log‘𝑛) = (log‘𝑚)) |
240 | 238, 239 | oveq12d 6668 |
. . . . . . . . . . . . . . . 16
⊢ (𝑛 = 𝑚 → (((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = (((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) |
241 | 240 | cbvsumv 14426 |
. . . . . . . . . . . . . . 15
⊢
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) |
242 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚))) → 𝑛 ∈
ℕ) |
243 | 242 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))) → 𝑛 ∈
ℕ) |
244 | 243, 10 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))) →
(Λ‘𝑛) ∈
ℝ) |
245 | 244 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))) →
(Λ‘𝑛) ∈
ℂ) |
246 | 245 | anasss 679 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚))))) →
(Λ‘𝑛) ∈
ℂ) |
247 | | elfznn 12370 |
. . . . . . . . . . . . . . . . . . . . . . 23
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℕ) |
248 | 247 | adantl 482 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
ℕ) |
249 | 248, 118 | syl 17 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑚)
∈ ℝ) |
250 | 249 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (Λ‘𝑚)
∈ ℂ) |
251 | 248 | nnrpd 11870 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑚 ∈
ℝ+) |
252 | 251 | relogcld 24369 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑚) ∈
ℝ) |
253 | 252 | recnd 10068 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (log‘𝑚) ∈
ℂ) |
254 | 250, 253 | mulcld 10060 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑚)
· (log‘𝑚))
∈ ℂ) |
255 | 254 | adantrr 753 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚))))) →
((Λ‘𝑚)
· (log‘𝑚))
∈ ℂ) |
256 | 246, 255 | mulcld 10060 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ (𝑚 ∈
(1...(⌊‘𝑥))
∧ 𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚))))) →
((Λ‘𝑛)
· ((Λ‘𝑚) · (log‘𝑚))) ∈ ℂ) |
257 | 36, 256 | fsumfldivdiag 24916 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈
(1...(⌊‘𝑥))Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
258 | 36 | adantr 481 |
. . . . . . . . . . . . . . . . . . . . . 22
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ 𝑥 ∈
ℝ) |
259 | 258, 248 | nndivred 11069 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (𝑥 / 𝑚) ∈
ℝ) |
260 | | chpcl 24850 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 / 𝑚) ∈ ℝ → (ψ‘(𝑥 / 𝑚)) ∈ ℝ) |
261 | 259, 260 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑚)) ∈
ℝ) |
262 | 261 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑚)) ∈
ℂ) |
263 | 250, 262,
253 | mul32d 10246 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑚)
· (ψ‘(𝑥 /
𝑚))) ·
(log‘𝑚)) =
(((Λ‘𝑚)
· (log‘𝑚))
· (ψ‘(𝑥 /
𝑚)))) |
264 | 249, 252 | remulcld 10070 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑚)
· (log‘𝑚))
∈ ℝ) |
265 | 264 | recnd 10068 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑚)
· (log‘𝑚))
∈ ℂ) |
266 | 265, 262 | mulcomd 10061 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑚)
· (log‘𝑚))
· (ψ‘(𝑥 /
𝑚))) = ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚)))) |
267 | | chpval 24848 |
. . . . . . . . . . . . . . . . . . . . 21
⊢ ((𝑥 / 𝑚) ∈ ℝ → (ψ‘(𝑥 / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛)) |
268 | 259, 267 | syl 17 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (ψ‘(𝑥 /
𝑚)) = Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))(Λ‘𝑛)) |
269 | 268 | oveq1d 6665 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑥 /
𝑚)) ·
((Λ‘𝑚)
· (log‘𝑚))) =
(Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))(Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚)))) |
270 | | fzfid 12772 |
. . . . . . . . . . . . . . . . . . . 20
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (1...(⌊‘(𝑥 / 𝑚))) ∈ Fin) |
271 | 270, 265,
245 | fsummulc1 14517 |
. . . . . . . . . . . . . . . . . . 19
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))(Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚))) =
Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))((Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚)))) |
272 | 269, 271 | eqtrd 2656 |
. . . . . . . . . . . . . . . . . 18
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ ((ψ‘(𝑥 /
𝑚)) ·
((Λ‘𝑚)
· (log‘𝑚))) =
Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))((Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚)))) |
273 | 263, 266,
272 | 3eqtrd 2660 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑚 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑚)
· (ψ‘(𝑥 /
𝑚))) ·
(log‘𝑚)) =
Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))((Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚)))) |
274 | 273 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈
(1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
275 | 122 | recnd 10068 |
. . . . . . . . . . . . . . . . . 18
⊢ ((((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
∧ 𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))) →
((Λ‘𝑚)
· (log‘𝑚))
∈ ℂ) |
276 | 115, 114,
275 | fsummulc2 14516 |
. . . . . . . . . . . . . . . . 17
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
277 | 276 | sumeq2dv 14433 |
. . . . . . . . . . . . . . . 16
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
278 | 257, 274,
277 | 3eqtr4d 2666 |
. . . . . . . . . . . . . . 15
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑚 ∈
(1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) |
279 | 241, 278 | syl5eq 2668 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) |
280 | 114, 211,
212 | mulassd 10063 |
. . . . . . . . . . . . . . 15
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ (((Λ‘𝑛)
· (ψ‘(𝑥 /
𝑛))) ·
(log‘𝑛)) =
((Λ‘𝑛)
· ((ψ‘(𝑥 /
𝑛)) ·
(log‘𝑛)))) |
281 | 280 | sumeq2dv 14433 |
. . . . . . . . . . . . . 14
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) |
282 | 279, 281 | oveq12d 6668 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))) |
283 | 104 | 2timesd 11275 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)) + Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)))) |
284 | 114, 210 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) ∈
ℂ) |
285 | 114, 213 | mulcld 10060 |
. . . . . . . . . . . . . 14
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· ((ψ‘(𝑥 /
𝑛)) ·
(log‘𝑛))) ∈
ℂ) |
286 | 7, 284, 285 | fsumadd 14470 |
. . . . . . . . . . . . 13
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))) |
287 | 282, 283,
286 | 3eqtr4d 2666 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))) |
288 | 114, 210,
213 | adddid 10064 |
. . . . . . . . . . . . 13
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))) |
289 | 288 | sumeq2dv 14433 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))) |
290 | 287, 289 | eqtr4d 2659 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛))))) |
291 | 91 | recnd 10068 |
. . . . . . . . . . . 12
⊢ (((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) ∧ 𝑛 ∈
(1...(⌊‘𝑥)))
→ ((Λ‘𝑛)
· (ψ‘(𝑥 /
𝑛))) ∈
ℂ) |
292 | 7, 26, 291 | fsummulc1 14517 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) |
293 | 290, 292 | oveq12d 6668 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + ((ψ‘(𝑥 / 𝑛)) · (log‘𝑛)))) − Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) |
294 | 219, 234,
293 | 3eqtr4rd 2667 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛)))))) |
295 | 294 | fveq2d 6195 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) = (abs‘Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) − ((ψ‘(𝑥 / 𝑛)) · (log‘(𝑥 / 𝑛))))))) |
296 | 24, 23, 204 | mulassd 10063 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 · 𝑥))) |
297 | 209, 295,
296 | 3brtr4d 4685 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥)) |
298 | 109, 113,
43 | ledivmul2d 11926 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) ↔ (abs‘((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) · 𝑥))) |
299 | 297, 298 | mpbird 247 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴)) |
300 | 111, 113,
25, 299 | lediv1dd 11930 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) ≤ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥))) |
301 | 109 | recnd 10068 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (abs‘((2
· Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) ∈ ℂ) |
302 | 301, 204,
26, 110, 29 | divdiv1d 10832 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) = ((abs‘((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥)))) |
303 | 108, 26, 204, 29, 110 | divdiv32d 10826 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) / 𝑥) = ((((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / 𝑥) / (log‘𝑥))) |
304 | 105, 107,
26, 29 | divsubdird 10840 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥)))) |
305 | 103, 104,
26, 29 | div23d 10838 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛)))) |
306 | 106, 26, 29 | divcan4d 10807 |
. . . . . . . . . . . 12
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) |
307 | 305, 306 | oveq12d 6668 |
. . . . . . . . . . 11
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) / (log‘𝑥)) − ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)) / (log‘𝑥))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))))) |
308 | 304, 307 | eqtrd 2656 |
. . . . . . . . . 10
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))))) |
309 | 308 | oveq1d 6665 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (log‘𝑥)) / 𝑥) = ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) |
310 | 108, 204,
26, 110, 29 | divdiv1d 10832 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / 𝑥) / (log‘𝑥)) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥)))) |
311 | 303, 309,
310 | 3eqtr3d 2664 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥) = (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥)))) |
312 | 311 | fveq2d 6195 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) = (abs‘(((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥))))) |
313 | 43, 25 | rpmulcld 11888 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ+) |
314 | 313 | rpcnd 11874 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℂ) |
315 | 313 | rpne0d 11877 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0) |
316 | 108, 314,
315 | absdivd 14194 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥))) / (𝑥 · (log‘𝑥)))) = ((abs‘((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (abs‘(𝑥 · (log‘𝑥))))) |
317 | 313 | rpred 11872 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ) |
318 | 313 | rpge0d 11876 |
. . . . . . . . 9
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → 0 ≤ (𝑥 · (log‘𝑥))) |
319 | 317, 318 | absidd 14161 |
. . . . . . . 8
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘(𝑥 ·
(log‘𝑥))) = (𝑥 · (log‘𝑥))) |
320 | 319 | oveq2d 6666 |
. . . . . . 7
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (abs‘(𝑥 · (log‘𝑥)))) = ((abs‘((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥)))) |
321 | 312, 316,
320 | 3eqtrd 2660 |
. . . . . 6
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) = ((abs‘((2 · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / (𝑥 · (log‘𝑥)))) |
322 | 302, 321 | eqtr4d 2659 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(((abs‘((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑥)))) / 𝑥) / (log‘𝑥)) = (abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥))) |
323 | 24, 23, 26, 29 | divassd 10836 |
. . . . 5
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · 𝐴) / (log‘𝑥)) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) |
324 | 300, 322,
323 | 3brtr3d 4684 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥)))) |
325 | 21 | leabsd 14153 |
. . . 4
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) → (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))) ≤ (abs‘(Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))))) |
326 | 101, 21, 102, 324, 325 | letrd 10194 |
. . 3
⊢ ((𝜑 ∧ 𝑥 ∈ (1(,)+∞)) →
(abs‘((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))))) |
327 | 326 | adantrr 753 |
. 2
⊢ ((𝜑 ∧ (𝑥 ∈ (1(,)+∞) ∧ 1 ≤ 𝑥)) → (abs‘((((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ≤ (abs‘(Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) / 𝑛) · (𝐴 / (log‘𝑥))))) |
328 | 1, 83, 21, 100, 327 | o1le 14383 |
1
⊢ (𝜑 → (𝑥 ∈ (1(,)+∞) ↦ ((((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))(((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛))) · (log‘𝑛))) − Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · (ψ‘(𝑥 / 𝑛)))) / 𝑥)) ∈ 𝑂(1)) |