Step | Hyp | Ref
| Expression |
1 | | 2re 11904 |
. . . . . . . . . . . . 13
⊢ 2 ∈
ℝ |
2 | 1 | a1i 11 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℝ) |
3 | | elioore 12965 |
. . . . . . . . . . . . . 14
⊢ (𝑥 ∈ (1(,)+∞) →
𝑥 ∈
ℝ) |
4 | 3 | adantl 485 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ) |
5 | | eliooord 12994 |
. . . . . . . . . . . . . . 15
⊢ (𝑥 ∈ (1(,)+∞) → (1
< 𝑥 ∧ 𝑥 <
+∞)) |
6 | 5 | adantl 485 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1 < 𝑥 ∧ 𝑥 < +∞)) |
7 | 6 | simpld 498 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 < 𝑥) |
8 | 4, 7 | rplogcld 25517 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈
ℝ+) |
9 | 2, 8 | rerpdivcld 12659 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℝ) |
10 | | fzfid 13546 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (1...(⌊‘𝑥)) ∈ Fin) |
11 | | elfznn 13141 |
. . . . . . . . . . . . . . . 16
⊢ (𝑚 ∈
(1...(⌊‘𝑥))
→ 𝑚 ∈
ℕ) |
12 | 11 | adantl 485 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℕ) |
13 | | vmacl 26000 |
. . . . . . . . . . . . . . 15
⊢ (𝑚 ∈ ℕ →
(Λ‘𝑚) ∈
ℝ) |
14 | 12, 13 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈
ℝ) |
15 | 4 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ) |
16 | 15, 12 | nndivred 11884 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑚) ∈ ℝ) |
17 | | chpcl 26006 |
. . . . . . . . . . . . . . 15
⊢ ((𝑥 / 𝑚) ∈ ℝ → (ψ‘(𝑥 / 𝑚)) ∈ ℝ) |
18 | 16, 17 | syl 17 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) ∈ ℝ) |
19 | 14, 18 | remulcld 10863 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑚)
· (ψ‘(𝑥 /
𝑚))) ∈
ℝ) |
20 | 12 | nnrpd 12626 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → 𝑚 ∈ ℝ+) |
21 | 20 | relogcld 25511 |
. . . . . . . . . . . . 13
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈
ℝ) |
22 | 19, 21 | remulcld 10863 |
. . . . . . . . . . . 12
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑚)
· (ψ‘(𝑥 /
𝑚))) ·
(log‘𝑚)) ∈
ℝ) |
23 | 10, 22 | fsumrecl 15298 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) ∈ ℝ) |
24 | 9, 23 | remulcld 10863 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) ∈ ℝ) |
25 | 10, 19 | fsumrecl 15298 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) ∈ ℝ) |
26 | 24, 25 | resubcld 11260 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) ∈ ℝ) |
27 | | 1rp 12590 |
. . . . . . . . . . 11
⊢ 1 ∈
ℝ+ |
28 | 27 | a1i 11 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ+) |
29 | | 1red 10834 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ∈ ℝ) |
30 | 29, 4, 7 | ltled 10980 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 1 ≤ 𝑥) |
31 | 4, 28, 30 | rpgecld 12667 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℝ+) |
32 | 26, 31 | rerpdivcld 12659 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) ∈ ℝ) |
33 | 32 | recnd 10861 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) ∈ ℂ) |
34 | | chpcl 26006 |
. . . . . . . . . . . 12
⊢ (𝑥 ∈ ℝ →
(ψ‘𝑥) ∈
ℝ) |
35 | 4, 34 | syl 17 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (ψ‘𝑥) ∈ ℝ) |
36 | 31 | relogcld 25511 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℝ) |
37 | 35, 36 | remulcld 10863 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℝ) |
38 | 37, 25 | readdcld 10862 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) ∈ ℝ) |
39 | 38, 31 | rerpdivcld 12659 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) ∈ ℝ) |
40 | 39 | recnd 10861 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) ∈ ℂ) |
41 | 2, 36 | remulcld 10863 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℝ) |
42 | 41 | recnd 10861 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · (log‘𝑥)) ∈ ℂ) |
43 | 33, 40, 42 | addsubassd 11209 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) + ((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥)) − (2 · (log‘𝑥))) = (((((2 / (log‘𝑥)) · Σ𝑚 ∈
(1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) + (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) − (2 · (log‘𝑥))))) |
44 | 26 | recnd 10861 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) ∈ ℂ) |
45 | 38 | recnd 10861 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) ∈ ℂ) |
46 | 4 | recnd 10861 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ∈ ℂ) |
47 | 31 | rpne0d 12633 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 𝑥 ≠ 0) |
48 | 44, 45, 46, 47 | divdird 11646 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) + (((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))))) / 𝑥) = (((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) + ((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥))) |
49 | 24 | recnd 10861 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) ∈ ℂ) |
50 | 25 | recnd 10861 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) ∈ ℂ) |
51 | 37 | recnd 10861 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((ψ‘𝑥) · (log‘𝑥)) ∈ ℂ) |
52 | 49, 50, 51 | nppcan3d 11216 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) + (((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))))) = (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) + ((ψ‘𝑥) · (log‘𝑥)))) |
53 | | elfznn 13141 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚))) → 𝑛 ∈
ℕ) |
54 | 53 | ad2antll 729 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → 𝑛 ∈ ℕ) |
55 | | vmacl 26000 |
. . . . . . . . . . . . . . . . 17
⊢ (𝑛 ∈ ℕ →
(Λ‘𝑛) ∈
ℝ) |
56 | 54, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → (Λ‘𝑛) ∈
ℝ) |
57 | 14 | adantrr 717 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → (Λ‘𝑚) ∈
ℝ) |
58 | 20 | adantrr 717 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → 𝑚 ∈ ℝ+) |
59 | 58 | relogcld 25511 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → (log‘𝑚) ∈ ℝ) |
60 | 57, 59 | remulcld 10863 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → ((Λ‘𝑚) · (log‘𝑚)) ∈
ℝ) |
61 | 56, 60 | remulcld 10863 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → ((Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚)))
∈ ℝ) |
62 | 61 | recnd 10861 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ (𝑚 ∈ (1...(⌊‘𝑥)) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚))))) → ((Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚)))
∈ ℂ) |
63 | 4, 62 | fsumfldivdiag 26072 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
64 | 14 | recnd 10861 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑚) ∈
ℂ) |
65 | 18 | recnd 10861 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) ∈ ℂ) |
66 | 21 | recnd 10861 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (log‘𝑚) ∈
ℂ) |
67 | 64, 65, 66 | mul32d 11042 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑚)
· (ψ‘(𝑥 /
𝑚))) ·
(log‘𝑚)) =
(((Λ‘𝑚)
· (log‘𝑚))
· (ψ‘(𝑥 /
𝑚)))) |
68 | 64, 66 | mulcld 10853 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑚)
· (log‘𝑚))
∈ ℂ) |
69 | 68, 65 | mulcomd 10854 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑚)
· (log‘𝑚))
· (ψ‘(𝑥 /
𝑚))) = ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚)))) |
70 | | chpval 26004 |
. . . . . . . . . . . . . . . . . 18
⊢ ((𝑥 / 𝑚) ∈ ℝ → (ψ‘(𝑥 / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛)) |
71 | 16, 70 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (ψ‘(𝑥 / 𝑚)) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛)) |
72 | 71 | oveq1d 7228 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚))) = (Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))(Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
73 | | fzfid 13546 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑥 /
𝑚))) ∈
Fin) |
74 | 56 | anassrs 471 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑛) ∈
ℝ) |
75 | 74 | recnd 10861 |
. . . . . . . . . . . . . . . . 17
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) ∧ 𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))) → (Λ‘𝑛) ∈
ℂ) |
76 | 73, 68, 75 | fsummulc1 15349 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → (Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))(Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚))) =
Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))((Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚)))) |
77 | 72, 76 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) → ((ψ‘(𝑥 / 𝑚)) · ((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
78 | 67, 69, 77 | 3eqtrd 2781 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑚 ∈ (1...(⌊‘𝑥))) →
(((Λ‘𝑚)
· (ψ‘(𝑥 /
𝑚))) ·
(log‘𝑚)) =
Σ𝑛 ∈
(1...(⌊‘(𝑥 /
𝑚)))((Λ‘𝑛) ·
((Λ‘𝑚)
· (log‘𝑚)))) |
79 | 78 | sumeq2dv 15267 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑚 ∈ (1...(⌊‘𝑥))Σ𝑛 ∈ (1...(⌊‘(𝑥 / 𝑚)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
80 | | fzfid 13546 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
(1...(⌊‘(𝑥 /
𝑛))) ∈
Fin) |
81 | | elfznn 13141 |
. . . . . . . . . . . . . . . . . 18
⊢ (𝑛 ∈
(1...(⌊‘𝑥))
→ 𝑛 ∈
ℕ) |
82 | 81 | adantl 485 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑛 ∈ ℕ) |
83 | 82, 55 | syl 17 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℝ) |
84 | 83 | recnd 10861 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (Λ‘𝑛) ∈
ℂ) |
85 | | elfznn 13141 |
. . . . . . . . . . . . . . . . . . 19
⊢ (𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛))) → 𝑚 ∈
ℕ) |
86 | 85 | adantl 485 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℕ) |
87 | 86, 13 | syl 17 |
. . . . . . . . . . . . . . . . 17
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈
ℝ) |
88 | 86 | nnrpd 12626 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → 𝑚 ∈ ℝ+) |
89 | 88 | relogcld 25511 |
. . . . . . . . . . . . . . . . 17
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℝ) |
90 | 87, 89 | remulcld 10863 |
. . . . . . . . . . . . . . . 16
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (log‘𝑚)) ∈
ℝ) |
91 | 90 | recnd 10861 |
. . . . . . . . . . . . . . 15
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (log‘𝑚)) ∈
ℂ) |
92 | 80, 84, 91 | fsummulc2 15348 |
. . . . . . . . . . . . . 14
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
93 | 92 | sumeq2dv 15267 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) = Σ𝑛 ∈ (1...(⌊‘𝑥))Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑛) · ((Λ‘𝑚) · (log‘𝑚)))) |
94 | 63, 79, 93 | 3eqtr4d 2787 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚)) = Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) |
95 | 94 | oveq2d 7229 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))))) |
96 | 95 | oveq1d 7228 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) + ((ψ‘𝑥) · (log‘𝑥))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥)))) |
97 | 52, 96 | eqtrd 2777 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) + (((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥)))) |
98 | 97 | oveq1d 7228 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) + (((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))))) / 𝑥) = ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
99 | 48, 98 | eqtr3d 2779 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) + ((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥)) = ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥)) |
100 | 99 | oveq1d 7228 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) + ((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥)) − (2 · (log‘𝑥))) = (((((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥)))) |
101 | 43, 100 | eqtr3d 2779 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) + (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) − (2 · (log‘𝑥)))) = (((((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥)))) |
102 | 101 | mpteq2dva 5150 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) + (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) − (2 · (log‘𝑥))))) = (𝑥 ∈ (1(,)+∞) ↦ (((((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥))))) |
103 | 39, 41 | resubcld 11260 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) − (2 · (log‘𝑥))) ∈
ℝ) |
104 | | selberg3lem2 26439 |
. . . . . 6
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((2 / (log‘𝑥))
· Σ𝑚 ∈
(1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥)) ∈ 𝑂(1) |
105 | 104 | a1i 11 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥)) ∈ 𝑂(1)) |
106 | 31 | ex 416 |
. . . . . . 7
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) → 𝑥
∈ ℝ+)) |
107 | 106 | ssrdv 3907 |
. . . . . 6
⊢ (⊤
→ (1(,)+∞) ⊆ ℝ+) |
108 | | selberg2 26432 |
. . . . . . 7
⊢ (𝑥 ∈ ℝ+
↦ (((((ψ‘𝑥)
· (log‘𝑥)) +
Σ𝑚 ∈
(1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1) |
109 | 108 | a1i 11 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
ℝ+ ↦ (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
110 | 107, 109 | o1res2 15124 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
111 | 32, 103, 105, 110 | o1add2 15185 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((((2 / (log‘𝑥)) · Σ𝑚 ∈ (1...(⌊‘𝑥))(((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚))) · (log‘𝑚))) − Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) + (((((ψ‘𝑥) · (log‘𝑥)) + Σ𝑚 ∈ (1...(⌊‘𝑥))((Λ‘𝑚) · (ψ‘(𝑥 / 𝑚)))) / 𝑥) − (2 · (log‘𝑥))))) ∈
𝑂(1)) |
112 | 102, 111 | eqeltrrd 2839 |
. . 3
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥)))) ∈
𝑂(1)) |
113 | 80, 90 | fsumrecl 15298 |
. . . . . . . . . . 11
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) ∈
ℝ) |
114 | 83, 113 | remulcld 10863 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) ∈
ℝ) |
115 | 10, 114 | fsumrecl 15298 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) ∈
ℝ) |
116 | 9, 115 | remulcld 10863 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) ∈
ℝ) |
117 | 116, 37 | readdcld 10862 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) ∈
ℝ) |
118 | 117, 31 | rerpdivcld 12659 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) ∈ ℝ) |
119 | 118, 41 | resubcld 11260 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥))) ∈
ℝ) |
120 | 119 | recnd 10861 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥))) ∈
ℂ) |
121 | 4 | adantr 484 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → 𝑥 ∈ ℝ) |
122 | 121, 82 | nndivred 11884 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → (𝑥 / 𝑛) ∈ ℝ) |
123 | 122 | adantr 484 |
. . . . . . . . . . . . . 14
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (𝑥 / 𝑛) ∈ ℝ) |
124 | 123, 86 | nndivred 11884 |
. . . . . . . . . . . . 13
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((𝑥 / 𝑛) / 𝑚) ∈ ℝ) |
125 | | chpcl 26006 |
. . . . . . . . . . . . 13
⊢ (((𝑥 / 𝑛) / 𝑚) ∈ ℝ → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ) |
126 | 124, 125 | syl 17 |
. . . . . . . . . . . 12
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℝ) |
127 | 87, 126 | remulcld 10863 |
. . . . . . . . . . 11
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℝ) |
128 | 80, 127 | fsumrecl 15298 |
. . . . . . . . . 10
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℝ) |
129 | 83, 128 | remulcld 10863 |
. . . . . . . . 9
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ) |
130 | 10, 129 | fsumrecl 15298 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ) |
131 | 9, 130 | remulcld 10863 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ) |
132 | 37, 131 | resubcld 11260 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) ∈ ℝ) |
133 | 132, 31 | rerpdivcld 12659 |
. . . . 5
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) ∈ ℝ) |
134 | 133 | recnd 10861 |
. . . 4
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) ∈ ℂ) |
135 | 116 | recnd 10861 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) ∈
ℂ) |
136 | 131 | recnd 10861 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℂ) |
137 | 51, 135, 136 | pnncand 11228 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((ψ‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))))) −
(((ψ‘𝑥) ·
(log‘𝑥)) − ((2
/ (log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) |
138 | 135, 51 | addcomd 11034 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) = (((ψ‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)))))) |
139 | 138 | oveq1d 7228 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) − (((ψ‘𝑥) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) = ((((ψ‘𝑥) · (log‘𝑥)) + ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))))) −
(((ψ‘𝑥) ·
(log‘𝑥)) − ((2
/ (log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))))) |
140 | 87 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (Λ‘𝑚) ∈
ℂ) |
141 | 89 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (log‘𝑚) ∈ ℂ) |
142 | 126 | recnd 10861 |
. . . . . . . . . . . . . . . . . . . 20
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → (ψ‘((𝑥 / 𝑛) / 𝑚)) ∈ ℂ) |
143 | 140, 141,
142 | adddid 10857 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) = (((Λ‘𝑚) · (log‘𝑚)) + ((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) |
144 | 143 | sumeq2dv 15267 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) = Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))(((Λ‘𝑚) · (log‘𝑚)) + ((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) |
145 | 127 | recnd 10861 |
. . . . . . . . . . . . . . . . . . 19
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℂ) |
146 | 80, 91, 145 | fsumadd 15304 |
. . . . . . . . . . . . . . . . . 18
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))(((Λ‘𝑚) · (log‘𝑚)) + ((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) |
147 | 144, 146 | eqtrd 2777 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) = (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) |
148 | 147 | oveq2d 7229 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) = ((Λ‘𝑛) · (Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚)) + Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) |
149 | 113 | recnd 10861 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) ∈
ℂ) |
150 | 128 | recnd 10861 |
. . . . . . . . . . . . . . . . 17
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℂ) |
151 | 84, 149, 150 | adddid 10857 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· (Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)) + Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) = (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) |
152 | 148, 151 | eqtrd 2777 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) = (((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) |
153 | 152 | sumeq2dv 15267 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) = Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) |
154 | 114 | recnd 10861 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) ∈
ℂ) |
155 | 129 | recnd 10861 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℂ) |
156 | 10, 154, 155 | fsumadd 15304 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))(((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + ((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) |
157 | 153, 156 | eqtrd 2777 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) = (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) |
158 | 157 | oveq2d 7229 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) = ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) |
159 | 9 | recnd 10861 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 / (log‘𝑥)) ∈ ℂ) |
160 | 115 | recnd 10861 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) ∈
ℂ) |
161 | 130 | recnd 10861 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℂ) |
162 | 159, 160,
161 | adddid 10857 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚))) + Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) |
163 | 158, 162 | eqtrd 2777 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) |
164 | 137, 139,
163 | 3eqtr4d 2787 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) − (((ψ‘𝑥) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))))) |
165 | 164 | oveq1d 7228 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) − (((ψ‘𝑥) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) / 𝑥) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) |
166 | 117 | recnd 10861 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) ∈
ℂ) |
167 | 51, 136 | subcld 11189 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) ∈ ℂ) |
168 | 166, 167,
46, 47 | divsubdird 11647 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) − (((ψ‘𝑥) · (log‘𝑥)) − ((2 /
(log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚))))))) / 𝑥) = (((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥))) |
169 | | 2cnd 11908 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → 2 ∈ ℂ) |
170 | 89, 126 | readdcld 10862 |
. . . . . . . . . . . . . . . . . 18
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))) ∈ ℝ) |
171 | 87, 170 | remulcld 10863 |
. . . . . . . . . . . . . . . . 17
⊢
((((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) ∧ 𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))) → ((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ) |
172 | 80, 171 | fsumrecl 15298 |
. . . . . . . . . . . . . . . 16
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) → Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))) ∈ ℝ) |
173 | 83, 172 | remulcld 10863 |
. . . . . . . . . . . . . . 15
⊢
(((⊤ ∧ 𝑥
∈ (1(,)+∞)) ∧ 𝑛 ∈ (1...(⌊‘𝑥))) →
((Λ‘𝑛)
· Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ) |
174 | 10, 173 | fsumrecl 15298 |
. . . . . . . . . . . . . 14
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℝ) |
175 | 174 | recnd 10861 |
. . . . . . . . . . . . 13
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) ∈ ℂ) |
176 | 169, 175 | mulcld 10853 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) ∈ ℂ) |
177 | 36 | recnd 10861 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ∈ ℂ) |
178 | 8 | rpne0d 12633 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (log‘𝑥) ≠ 0) |
179 | 176, 177,
46, 178, 47 | divdiv1d 11639 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / (log‘𝑥)) / 𝑥) = ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / ((log‘𝑥) · 𝑥))) |
180 | 177, 46 | mulcomd 10854 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((log‘𝑥) · 𝑥) = (𝑥 · (log‘𝑥))) |
181 | 180 | oveq2d 7229 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / ((log‘𝑥) · 𝑥)) = ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / (𝑥 · (log‘𝑥)))) |
182 | 179, 181 | eqtrd 2777 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / (log‘𝑥)) / 𝑥) = ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / (𝑥 · (log‘𝑥)))) |
183 | 169, 175,
177, 178 | div23d 11645 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / (log‘𝑥)) = ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))))) |
184 | 183 | oveq1d 7228 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / (log‘𝑥)) / 𝑥) = (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) |
185 | 31, 8 | rpmulcld 12644 |
. . . . . . . . . . . 12
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈
ℝ+) |
186 | 185 | rpcnd 12630 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ∈ ℂ) |
187 | 185 | rpne0d 12633 |
. . . . . . . . . . 11
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (𝑥 · (log‘𝑥)) ≠ 0) |
188 | 169, 175,
186, 187 | divassd 11643 |
. . . . . . . . . 10
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((2 · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / (𝑥 · (log‘𝑥))) = (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))))) |
189 | 182, 184,
188 | 3eqtr3d 2785 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥) = (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))))) |
190 | 165, 168,
189 | 3eqtr3d 2785 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) = (2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))))) |
191 | 190 | oveq1d 7228 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) − (2 · (log‘𝑥))) = ((2 · (Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥)))) − (2 · (log‘𝑥)))) |
192 | 118 | recnd 10861 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) ∈ ℂ) |
193 | 192, 42, 134 | sub32d 11221 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥))) −
((((ψ‘𝑥) ·
(log‘𝑥)) − ((2
/ (log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) = ((((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) − (2 · (log‘𝑥)))) |
194 | 174, 185 | rerpdivcld 12659 |
. . . . . . . . 9
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) ∈ ℝ) |
195 | 194 | recnd 10861 |
. . . . . . . 8
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) ∈ ℂ) |
196 | 169, 195,
177 | subdid 11288 |
. . . . . . 7
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) = ((2 · (Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥)))) − (2 · (log‘𝑥)))) |
197 | 191, 193,
196 | 3eqtr4d 2787 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥))) −
((((ψ‘𝑥) ·
(log‘𝑥)) − ((2
/ (log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) = (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)))) |
198 | 197 | mpteq2dva 5150 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥))) −
((((ψ‘𝑥) ·
(log‘𝑥)) − ((2
/ (log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥))) = (𝑥 ∈ (1(,)+∞) ↦ (2 ·
((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))))) |
199 | 194, 36 | resubcld 11260 |
. . . . . 6
⊢
((⊤ ∧ 𝑥
∈ (1(,)+∞)) → ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)) ∈ ℝ) |
200 | | ioossre 12996 |
. . . . . . 7
⊢
(1(,)+∞) ⊆ ℝ |
201 | | 2cnd 11908 |
. . . . . . 7
⊢ (⊤
→ 2 ∈ ℂ) |
202 | | o1const 15181 |
. . . . . . 7
⊢
(((1(,)+∞) ⊆ ℝ ∧ 2 ∈ ℂ) → (𝑥 ∈ (1(,)+∞) ↦
2) ∈ 𝑂(1)) |
203 | 200, 201,
202 | sylancr 590 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ 2) ∈ 𝑂(1)) |
204 | | selbergb 26430 |
. . . . . . 7
⊢
∃𝑐 ∈
ℝ+ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 |
205 | | simpl 486 |
. . . . . . . . 9
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → 𝑐 ∈ ℝ+) |
206 | | simpr 488 |
. . . . . . . . 9
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) |
207 | 205, 206 | selberg4lem1 26441 |
. . . . . . . 8
⊢ ((𝑐 ∈ ℝ+
∧ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐) → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1)) |
208 | 207 | rexlimiva 3200 |
. . . . . . 7
⊢
(∃𝑐 ∈
ℝ+ ∀𝑦 ∈
(1[,)+∞)(abs‘((Σ𝑖 ∈ (1...(⌊‘𝑦))((Λ‘𝑖) · ((log‘𝑖) + (ψ‘(𝑦 / 𝑖)))) / 𝑦) − (2 · (log‘𝑦)))) ≤ 𝑐 → (𝑥 ∈ (1(,)+∞) ↦ ((Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1)) |
209 | 204, 208 | mp1i 13 |
. . . . . 6
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥))) ∈ 𝑂(1)) |
210 | 2, 199, 203, 209 | o1mul2 15186 |
. . . . 5
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ (2 · ((Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · ((log‘𝑚) + (ψ‘((𝑥 / 𝑛) / 𝑚))))) / (𝑥 · (log‘𝑥))) − (log‘𝑥)))) ∈ 𝑂(1)) |
211 | 198, 210 | eqeltrd 2838 |
. . . 4
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥))) −
((((ψ‘𝑥) ·
(log‘𝑥)) − ((2
/ (log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥))) ∈ 𝑂(1)) |
212 | 120, 134,
211 | o1dif 15191 |
. . 3
⊢ (⊤
→ ((𝑥 ∈
(1(,)+∞) ↦ (((((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (log‘𝑚)))) + ((ψ‘𝑥) · (log‘𝑥))) / 𝑥) − (2 · (log‘𝑥)))) ∈ 𝑂(1) ↔
(𝑥 ∈ (1(,)+∞)
↦ ((((ψ‘𝑥)
· (log‘𝑥))
− ((2 / (log‘𝑥)) · Σ𝑛 ∈ (1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈
(1...(⌊‘(𝑥 /
𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1))) |
213 | 112, 212 | mpbid 235 |
. 2
⊢ (⊤
→ (𝑥 ∈
(1(,)+∞) ↦ ((((ψ‘𝑥) · (log‘𝑥)) − ((2 / (log‘𝑥)) · Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1)) |
214 | 213 | mptru 1550 |
1
⊢ (𝑥 ∈ (1(,)+∞) ↦
((((ψ‘𝑥) ·
(log‘𝑥)) − ((2
/ (log‘𝑥)) ·
Σ𝑛 ∈
(1...(⌊‘𝑥))((Λ‘𝑛) · Σ𝑚 ∈ (1...(⌊‘(𝑥 / 𝑛)))((Λ‘𝑚) · (ψ‘((𝑥 / 𝑛) / 𝑚)))))) / 𝑥)) ∈ 𝑂(1) |