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