| Step |
Hyp |
Ref |
Expression |
| 1 |
|
1re |
⊢ 1 ∈ ℝ |
| 2 |
|
elicopnf |
⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ) |
| 3 |
1 2
|
mp1i |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) ) |
| 4 |
3
|
simprbda |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ ) |
| 5 |
4
|
ex |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ ) ) |
| 6 |
5
|
ssrdv |
⊢ ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ ) |
| 7 |
1
|
a1i |
⊢ ( ⊤ → 1 ∈ ℝ ) |
| 8 |
|
chpcl |
⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ ) |
| 9 |
4 8
|
syl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ ) |
| 10 |
|
1rp |
⊢ 1 ∈ ℝ+ |
| 11 |
10
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ∈ ℝ+ ) |
| 12 |
3
|
simplbda |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 1 ≤ 𝑥 ) |
| 13 |
4 11 12
|
rpgecld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 𝑥 ∈ ℝ+ ) |
| 14 |
13
|
relogcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
| 15 |
9 14
|
remulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ ) |
| 16 |
|
fzfid |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
| 17 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
| 18 |
17
|
adantl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ ) |
| 19 |
|
vmacl |
⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
| 20 |
18 19
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
| 21 |
4
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ ) |
| 22 |
21 18
|
nndivred |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ ) |
| 23 |
|
chpcl |
⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
| 24 |
22 23
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
| 25 |
20 24
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
| 26 |
16 25
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
| 27 |
15 26
|
readdcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ ) |
| 28 |
27 13
|
rerpdivcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ ) |
| 29 |
|
2re |
⊢ 2 ∈ ℝ |
| 30 |
29
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 2 ∈ ℝ ) |
| 31 |
30 14
|
remulcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℝ ) |
| 32 |
28 31
|
resubcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ ) |
| 33 |
32
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℂ ) |
| 34 |
13
|
ex |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ+ ) ) |
| 35 |
34
|
ssrdv |
⊢ ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ+ ) |
| 36 |
|
selberg2 |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) |
| 37 |
36
|
a1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
| 38 |
35 37
|
o1res2 |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
| 39 |
|
chpcl |
⊢ ( 𝑦 ∈ ℝ → ( ψ ‘ 𝑦 ) ∈ ℝ ) |
| 40 |
39
|
ad2antrl |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( ψ ‘ 𝑦 ) ∈ ℝ ) |
| 41 |
|
simprl |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 𝑦 ∈ ℝ ) |
| 42 |
10
|
a1i |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 1 ∈ ℝ+ ) |
| 43 |
|
simprr |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 1 ≤ 𝑦 ) |
| 44 |
41 42 43
|
rpgecld |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 𝑦 ∈ ℝ+ ) |
| 45 |
44
|
relogcld |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( log ‘ 𝑦 ) ∈ ℝ ) |
| 46 |
40 45
|
remulcld |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ∈ ℝ ) |
| 47 |
|
fzfid |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) ∈ Fin ) |
| 48 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) → 𝑛 ∈ ℕ ) |
| 49 |
48
|
adantl |
⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℕ ) |
| 50 |
49 19
|
syl |
⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
| 51 |
41
|
adantr |
⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑦 ∈ ℝ ) |
| 52 |
51 49
|
nndivred |
⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( 𝑦 / 𝑛 ) ∈ ℝ ) |
| 53 |
|
chpcl |
⊢ ( ( 𝑦 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑦 / 𝑛 ) ) ∈ ℝ ) |
| 54 |
52 53
|
syl |
⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ψ ‘ ( 𝑦 / 𝑛 ) ) ∈ ℝ ) |
| 55 |
50 54
|
remulcld |
⊢ ( ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ∈ ℝ ) |
| 56 |
47 55
|
fsumrecl |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ∈ ℝ ) |
| 57 |
46 56
|
readdcld |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ∈ ℝ ) |
| 58 |
29
|
a1i |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → 2 ∈ ℝ ) |
| 59 |
58 45
|
remulcld |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( 2 · ( log ‘ 𝑦 ) ) ∈ ℝ ) |
| 60 |
57 59
|
readdcld |
⊢ ( ( ⊤ ∧ ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ) → ( ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) + ( 2 · ( log ‘ 𝑦 ) ) ) ∈ ℝ ) |
| 61 |
32
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ ) |
| 62 |
61
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℂ ) |
| 63 |
62
|
abscld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ ) |
| 64 |
28
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ ) |
| 65 |
64
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℂ ) |
| 66 |
65
|
abscld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ℝ ) |
| 67 |
31
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℝ ) |
| 68 |
67
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
| 69 |
68
|
abscld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℝ ) |
| 70 |
66 69
|
readdcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( abs ‘ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) + ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ ) |
| 71 |
60
|
ad2ant2r |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) + ( 2 · ( log ‘ 𝑦 ) ) ) ∈ ℝ ) |
| 72 |
65 68
|
abs2dif2d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( abs ‘ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) + ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) ) ) |
| 73 |
|
simprll |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℝ ) |
| 74 |
73 39
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ψ ‘ 𝑦 ) ∈ ℝ ) |
| 75 |
13
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℝ+ ) |
| 76 |
4
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ∈ ℝ ) |
| 77 |
|
simprr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 < 𝑦 ) |
| 78 |
76 73 77
|
ltled |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑥 ≤ 𝑦 ) |
| 79 |
73 75 78
|
rpgecld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 𝑦 ∈ ℝ+ ) |
| 80 |
79
|
relogcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑦 ) ∈ ℝ ) |
| 81 |
74 80
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ∈ ℝ ) |
| 82 |
56
|
ad2ant2r |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ∈ ℝ ) |
| 83 |
81 82
|
readdcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ∈ ℝ ) |
| 84 |
29
|
a1i |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 2 ∈ ℝ ) |
| 85 |
84 80
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 · ( log ‘ 𝑦 ) ) ∈ ℝ ) |
| 86 |
76 8
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ ) |
| 87 |
75
|
relogcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
| 88 |
86 87
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ∈ ℝ ) |
| 89 |
26
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
| 90 |
88 89
|
readdcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ ) |
| 91 |
|
chpge0 |
⊢ ( 𝑥 ∈ ℝ → 0 ≤ ( ψ ‘ 𝑥 ) ) |
| 92 |
76 91
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( ψ ‘ 𝑥 ) ) |
| 93 |
12
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 1 ≤ 𝑥 ) |
| 94 |
76 93
|
logge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( log ‘ 𝑥 ) ) |
| 95 |
86 87 92 94
|
mulge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) |
| 96 |
|
vmage0 |
⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) ) |
| 97 |
18 96
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) ) |
| 98 |
|
chpge0 |
⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → 0 ≤ ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) |
| 99 |
22 98
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) |
| 100 |
20 24 97 99
|
mulge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) |
| 101 |
16 25 100
|
fsumge0 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) |
| 102 |
101
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) |
| 103 |
88 89 95 102
|
addge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
| 104 |
90 75 103
|
divge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) |
| 105 |
64 104
|
absidd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) = ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) |
| 106 |
10
|
a1i |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 1 ∈ ℝ+ ) |
| 107 |
|
chpwordi |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) → ( ψ ‘ 𝑥 ) ≤ ( ψ ‘ 𝑦 ) ) |
| 108 |
76 73 78 107
|
syl3anc |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ψ ‘ 𝑥 ) ≤ ( ψ ‘ 𝑦 ) ) |
| 109 |
75 79
|
logled |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 𝑥 ≤ 𝑦 ↔ ( log ‘ 𝑥 ) ≤ ( log ‘ 𝑦 ) ) ) |
| 110 |
78 109
|
mpbid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( log ‘ 𝑥 ) ≤ ( log ‘ 𝑦 ) ) |
| 111 |
86 74 87 80 92 94 108 110
|
lemul12ad |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ≤ ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) |
| 112 |
|
fzfid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) ∈ Fin ) |
| 113 |
48
|
adantl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℕ ) |
| 114 |
113 19
|
syl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
| 115 |
76
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑥 ∈ ℝ ) |
| 116 |
115 113
|
nndivred |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ ) |
| 117 |
116 23
|
syl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
| 118 |
114 117
|
remulcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
| 119 |
112 118
|
fsumrecl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
| 120 |
113 96
|
syl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) ) |
| 121 |
116 98
|
syl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) |
| 122 |
114 117 120 121
|
mulge0d |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) |
| 123 |
|
flword2 |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑦 ∈ ℝ ∧ 𝑥 ≤ 𝑦 ) → ( ⌊ ‘ 𝑦 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) ) |
| 124 |
76 73 78 123
|
syl3anc |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ⌊ ‘ 𝑦 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) ) |
| 125 |
|
fzss2 |
⊢ ( ( ⌊ ‘ 𝑦 ) ∈ ( ℤ≥ ‘ ( ⌊ ‘ 𝑥 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) |
| 126 |
124 125
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) |
| 127 |
112 118 122 126
|
fsumless |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) |
| 128 |
73
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑦 ∈ ℝ ) |
| 129 |
128 113
|
nndivred |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( 𝑦 / 𝑛 ) ∈ ℝ ) |
| 130 |
129 53
|
syl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ψ ‘ ( 𝑦 / 𝑛 ) ) ∈ ℝ ) |
| 131 |
114 130
|
remulcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ∈ ℝ ) |
| 132 |
113
|
nnrpd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑛 ∈ ℝ+ ) |
| 133 |
78
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → 𝑥 ≤ 𝑦 ) |
| 134 |
115 128 132 133
|
lediv1dd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( 𝑥 / 𝑛 ) ≤ ( 𝑦 / 𝑛 ) ) |
| 135 |
|
chpwordi |
⊢ ( ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ ( 𝑦 / 𝑛 ) ∈ ℝ ∧ ( 𝑥 / 𝑛 ) ≤ ( 𝑦 / 𝑛 ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) |
| 136 |
116 129 134 135
|
syl3anc |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ≤ ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) |
| 137 |
117 130 114 120 136
|
lemul2ad |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) |
| 138 |
112 118 131 137
|
fsumle |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) |
| 139 |
89 119 82 127 138
|
letrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) |
| 140 |
88 89 81 82 111 139
|
le2addd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ) |
| 141 |
90 83 106 76 103 140 93
|
lediv12ad |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ≤ ( ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) / 1 ) ) |
| 142 |
83
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ∈ ℂ ) |
| 143 |
142
|
div1d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) / 1 ) = ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ) |
| 144 |
141 143
|
breqtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ≤ ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ) |
| 145 |
105 144
|
eqbrtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ≤ ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) ) |
| 146 |
|
2rp |
⊢ 2 ∈ ℝ+ |
| 147 |
|
rpge0 |
⊢ ( 2 ∈ ℝ+ → 0 ≤ 2 ) |
| 148 |
146 147
|
mp1i |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ 2 ) |
| 149 |
84 87 148 94
|
mulge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → 0 ≤ ( 2 · ( log ‘ 𝑥 ) ) ) |
| 150 |
67 149
|
absidd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) = ( 2 · ( log ‘ 𝑥 ) ) ) |
| 151 |
87 80 84 148 110
|
lemul2ad |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( 2 · ( log ‘ 𝑥 ) ) ≤ ( 2 · ( log ‘ 𝑦 ) ) ) |
| 152 |
150 151
|
eqbrtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) ≤ ( 2 · ( log ‘ 𝑦 ) ) ) |
| 153 |
66 69 83 85 145 152
|
le2addd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( ( abs ‘ ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) + ( abs ‘ ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) + ( 2 · ( log ‘ 𝑦 ) ) ) ) |
| 154 |
63 70 71 72 153
|
letrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 [,) +∞ ) ) ∧ ( ( 𝑦 ∈ ℝ ∧ 1 ≤ 𝑦 ) ∧ 𝑥 < 𝑦 ) ) → ( abs ‘ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑦 / 𝑛 ) ) ) ) + ( 2 · ( log ‘ 𝑦 ) ) ) ) |
| 155 |
6 7 33 38 60 154
|
o1bddrp |
⊢ ( ⊤ → ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 ) |
| 156 |
155
|
mptru |
⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑥 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( ( ( ψ ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ≤ 𝑐 |