Step |
Hyp |
Ref |
Expression |
1 |
|
2re |
⊢ 2 ∈ ℝ |
2 |
1
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ ) |
3 |
|
elioore |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ ) |
4 |
3
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ ) |
5 |
|
eliooord |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) ) |
6 |
5
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) ) |
7 |
6
|
simpld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 ) |
8 |
4 7
|
rplogcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ ) |
9 |
2 8
|
rerpdivcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ ) |
10 |
|
fzfid |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
11 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ ) |
12 |
11
|
adantl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ ) |
13 |
|
vmacl |
⊢ ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ ) |
14 |
12 13
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ ) |
15 |
4
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ ) |
16 |
15 12
|
nndivred |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑚 ) ∈ ℝ ) |
17 |
|
chpcl |
⊢ ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ ) |
18 |
16 17
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ ) |
19 |
14 18
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ ℝ ) |
20 |
12
|
nnrpd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ ) |
21 |
20
|
relogcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ ) |
22 |
19 21
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ∈ ℝ ) |
23 |
10 22
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ∈ ℝ ) |
24 |
9 23
|
remulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) ∈ ℝ ) |
25 |
10 19
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ ℝ ) |
26 |
24 25
|
resubcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ∈ ℝ ) |
27 |
|
1rp |
⊢ 1 ∈ ℝ+ |
28 |
27
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ ) |
29 |
|
1red |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ ) |
30 |
29 4 7
|
ltled |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 ) |
31 |
4 28 30
|
rpgecld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ ) |
32 |
26 31
|
rerpdivcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℝ ) |
33 |
32
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℂ ) |
34 |
|
chpcl |
⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ ) |
35 |
4 34
|
syl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ ) |
36 |
31
|
relogcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
37 |
35 36
|
remulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ ) |
38 |
37 25
|
readdcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ∈ ℝ ) |
39 |
38 31
|
rerpdivcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℝ ) |
40 |
39
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ∈ ℂ ) |
41 |
2 36
|
remulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℝ ) |
42 |
41
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
43 |
33 40 42
|
addsubassd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) |
44 |
26
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ∈ ℂ ) |
45 |
38
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ∈ ℂ ) |
46 |
4
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ ) |
47 |
31
|
rpne0d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 ) |
48 |
44 45 46 47
|
divdird |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) + ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) / 𝑥 ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) ) |
49 |
24
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ ) |
50 |
25
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ ℂ ) |
51 |
37
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
52 |
49 50 51
|
nppcan3d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) + ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) |
53 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) → 𝑛 ∈ ℕ ) |
54 |
53
|
ad2antll |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → 𝑛 ∈ ℕ ) |
55 |
|
vmacl |
⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
56 |
54 55
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
57 |
14
|
adantrr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ ) |
58 |
20
|
adantrr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → 𝑚 ∈ ℝ+ ) |
59 |
58
|
relogcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ ) |
60 |
57 59
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ ) |
61 |
56 60
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℝ ) |
62 |
61
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ ) |
63 |
4 62
|
fsumfldivdiag |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
64 |
14
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ ) |
65 |
18
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℂ ) |
66 |
21
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ ) |
67 |
64 65 66
|
mul32d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) |
68 |
64 66
|
mulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ ) |
69 |
68 65
|
mulcomd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) = ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
70 |
|
chpval |
⊢ ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) ) |
71 |
16 70
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) ) |
72 |
71
|
oveq1d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
73 |
|
fzfid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ Fin ) |
74 |
56
|
anassrs |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
75 |
74
|
recnd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
76 |
73 68 75
|
fsummulc1 |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
77 |
72 76
|
eqtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
78 |
67 69 77
|
3eqtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
79 |
78
|
sumeq2dv |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
80 |
|
fzfid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin ) |
81 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
82 |
81
|
adantl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ ) |
83 |
82 55
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
84 |
83
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
85 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ ) |
86 |
85
|
adantl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ ) |
87 |
86 13
|
syl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ ) |
88 |
86
|
nnrpd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ ) |
89 |
88
|
relogcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ ) |
90 |
87 89
|
remulcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ ) |
91 |
90
|
recnd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ ) |
92 |
80 84 91
|
fsummulc2 |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
93 |
92
|
sumeq2dv |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
94 |
63 79 93
|
3eqtr4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
95 |
94
|
oveq2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ) |
96 |
95
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) |
97 |
52 96
|
eqtrd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) + ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ) |
98 |
97
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) + ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) / 𝑥 ) = ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) |
99 |
48 98
|
eqtr3d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) = ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ) |
100 |
99
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) |
101 |
43 100
|
eqtr3d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) |
102 |
101
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) |
103 |
39 41
|
resubcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ ) |
104 |
|
selberg3lem2 |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) |
105 |
104
|
a1i |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) ) |
106 |
31
|
ex |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) ) |
107 |
106
|
ssrdv |
⊢ ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ+ ) |
108 |
|
selberg2 |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) |
109 |
108
|
a1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
110 |
107 109
|
o1res2 |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
111 |
32 103 105 110
|
o1add2 |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) − Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) + ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) ) |
112 |
102 111
|
eqeltrrd |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
113 |
80 90
|
fsumrecl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ ) |
114 |
83 113
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℝ ) |
115 |
10 114
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℝ ) |
116 |
9 115
|
remulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ∈ ℝ ) |
117 |
116 37
|
readdcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℝ ) |
118 |
117 31
|
rerpdivcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℝ ) |
119 |
118 41
|
resubcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ ) |
120 |
119
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℂ ) |
121 |
4
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ ) |
122 |
121 82
|
nndivred |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ ) |
123 |
122
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ ) |
124 |
123 86
|
nndivred |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( 𝑥 / 𝑛 ) / 𝑚 ) ∈ ℝ ) |
125 |
|
chpcl |
⊢ ( ( ( 𝑥 / 𝑛 ) / 𝑚 ) ∈ ℝ → ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ∈ ℝ ) |
126 |
124 125
|
syl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ∈ ℝ ) |
127 |
87 126
|
remulcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℝ ) |
128 |
80 127
|
fsumrecl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℝ ) |
129 |
83 128
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ ) |
130 |
10 129
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ ) |
131 |
9 130
|
remulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℝ ) |
132 |
37 131
|
resubcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ∈ ℝ ) |
133 |
132 31
|
rerpdivcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ∈ ℝ ) |
134 |
133
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ∈ ℂ ) |
135 |
116
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ∈ ℂ ) |
136 |
131
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℂ ) |
137 |
51 135 136
|
pnncand |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) = ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) ) ) |
139 |
138
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ ) |
141 |
89
|
recnd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ ) |
142 |
126
|
recnd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ∈ ℂ ) |
143 |
140 141 142
|
adddid |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) = ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) |
144 |
143
|
sumeq2dv |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) |
145 |
127
|
recnd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℂ ) |
146 |
80 91 145
|
fsumadd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) |
147 |
144 146
|
eqtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) |
148 |
147
|
oveq2d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) |
149 |
113
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ ) |
150 |
128
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℂ ) |
151 |
84 149 150
|
adddid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) |
152 |
148 151
|
eqtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) |
153 |
152
|
sumeq2dv |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) |
154 |
114
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ ) |
155 |
129
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℂ ) |
156 |
10 154 155
|
fsumadd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) |
157 |
153 156
|
eqtrd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) |
158 |
157
|
oveq2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) |
159 |
9
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℂ ) |
160 |
115
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ ) |
161 |
130
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℂ ) |
162 |
159 160 161
|
adddid |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) |
163 |
158 162
|
eqtrd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) |
164 |
137 139 163
|
3eqtr4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) |
165 |
164
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) − ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) / 𝑥 ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) |
166 |
117
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ ) |
167 |
51 136
|
subcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ∈ ℂ ) |
168 |
166 167 46 47
|
divsubdird |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ ) |
170 |
89 126
|
readdcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ∈ ℝ ) |
171 |
87 170
|
remulcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ ) |
172 |
80 171
|
fsumrecl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ∈ ℝ ) |
173 |
83 172
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℝ ) |
174 |
10 173
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℝ ) |
175 |
174
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ∈ ℂ ) |
176 |
169 175
|
mulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ∈ ℂ ) |
177 |
36
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
178 |
8
|
rpne0d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 ) |
179 |
176 177 46 178 47
|
divdiv1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( ( log ‘ 𝑥 ) · 𝑥 ) ) ) |
180 |
177 46
|
mulcomd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) · 𝑥 ) = ( 𝑥 · ( log ‘ 𝑥 ) ) ) |
181 |
180
|
oveq2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( ( log ‘ 𝑥 ) · 𝑥 ) ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) |
182 |
179 181
|
eqtrd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) |
183 |
169 175 177 178
|
div23d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) ) |
184 |
183
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) |
185 |
31 8
|
rpmulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ+ ) |
186 |
185
|
rpcnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
187 |
185
|
rpne0d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ≠ 0 ) |
188 |
169 175 186 187
|
divassd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) |
189 |
182 184 188
|
3eqtr3d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) |
190 |
165 168 189
|
3eqtr3d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) = ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) |
191 |
190
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) |
192 |
118
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) ∈ ℂ ) |
193 |
192 42 134
|
sub32d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 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 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ ) |
195 |
194
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℂ ) |
196 |
169 195 177
|
subdid |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) = ( ( 2 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) |
197 |
191 193 196
|
3eqtr4d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) = ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ) |
198 |
197
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ( 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 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ∈ ℝ ) |
200 |
|
ioossre |
⊢ ( 1 (,) +∞ ) ⊆ ℝ |
201 |
|
2cnd |
⊢ ( ⊤ → 2 ∈ ℂ ) |
202 |
|
o1const |
⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) ) |
203 |
200 201 202
|
sylancr |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 2 ) ∈ 𝑂(1) ) |
204 |
|
selbergb |
⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 |
205 |
|
simpl |
⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → 𝑐 ∈ ℝ+ ) |
206 |
|
simpr |
⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) |
207 |
205 206
|
selberg4lem1 |
⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
208 |
207
|
rexlimiva |
⊢ ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑦 / 𝑖 ) ) ) ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝑐 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
209 |
204 208
|
mp1i |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
210 |
2 199 203 209
|
o1mul2 |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 2 · ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ( log ‘ 𝑚 ) + ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
211 |
198 210
|
eqeltrd |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) − ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ) ∈ 𝑂(1) ) |
212 |
120 134 211
|
o1dif |
⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) + ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) ) ) |
213 |
112 212
|
mpbid |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) ) |
214 |
213
|
mptru |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( ( 𝑥 / 𝑛 ) / 𝑚 ) ) ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) |