Step |
Hyp |
Ref |
Expression |
1 |
|
selberg3lem1.1 |
⊢ ( 𝜑 → 𝐴 ∈ ℝ+ ) |
2 |
|
selberg3lem1.2 |
⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝐴 ) |
3 |
|
1red |
⊢ ( 𝜑 → 1 ∈ ℝ ) |
4 |
|
ioossre |
⊢ ( 1 (,) +∞ ) ⊆ ℝ |
5 |
1
|
rpcnd |
⊢ ( 𝜑 → 𝐴 ∈ ℂ ) |
6 |
|
o1const |
⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) ) |
7 |
4 5 6
|
sylancr |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) ) |
8 |
|
fzfid |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
9 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
10 |
9
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ ) |
11 |
|
vmacl |
⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
12 |
10 11
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
13 |
12 10
|
nndivred |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
14 |
8 13
|
fsumrecl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
15 |
|
elioore |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ ) |
16 |
|
eliooord |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) ) |
17 |
16
|
simpld |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 1 < 𝑥 ) |
18 |
15 17
|
rplogcld |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( log ‘ 𝑥 ) ∈ ℝ+ ) |
19 |
|
rpdivcl |
⊢ ( ( 𝐴 ∈ ℝ+ ∧ ( log ‘ 𝑥 ) ∈ ℝ+ ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ+ ) |
20 |
1 18 19
|
syl2an |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ+ ) |
21 |
20
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ ) |
22 |
14 21
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ∈ ℝ ) |
23 |
22
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ∈ ℂ ) |
24 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℂ ) |
25 |
14
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
26 |
18
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ ) |
27 |
26
|
rpcnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
28 |
20
|
rpcnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℂ ) |
29 |
25 27 28
|
subdird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − ( ( log ‘ 𝑥 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ) |
30 |
26
|
rpne0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 ) |
31 |
24 27 30
|
divcan2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) = 𝐴 ) |
32 |
31
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − ( ( log ‘ 𝑥 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − 𝐴 ) ) |
33 |
29 32
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − 𝐴 ) ) |
34 |
33
|
mpteq2dva |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − 𝐴 ) ) ) |
35 |
26
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
36 |
14 35
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℝ ) |
37 |
15
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ ) |
38 |
|
0red |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ∈ ℝ ) |
39 |
|
1red |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ ) |
40 |
|
0lt1 |
⊢ 0 < 1 |
41 |
40
|
a1i |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 < 1 ) |
42 |
17
|
adantl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 ) |
43 |
38 39 37 41 42
|
lttrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 < 𝑥 ) |
44 |
37 43
|
elrpd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ ) |
45 |
44
|
ex |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) ) |
46 |
45
|
ssrdv |
⊢ ( 𝜑 → ( 1 (,) +∞ ) ⊆ ℝ+ ) |
47 |
|
vmadivsum |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) |
48 |
47
|
a1i |
⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
49 |
46 48
|
o1res2 |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
50 |
4
|
a1i |
⊢ ( 𝜑 → ( 1 (,) +∞ ) ⊆ ℝ ) |
51 |
|
ere |
⊢ e ∈ ℝ |
52 |
51
|
a1i |
⊢ ( 𝜑 → e ∈ ℝ ) |
53 |
1
|
rpred |
⊢ ( 𝜑 → 𝐴 ∈ ℝ ) |
54 |
20
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ+ ) |
55 |
54
|
rprege0d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) |
56 |
|
absid |
⊢ ( ( ( 𝐴 / ( log ‘ 𝑥 ) ) ∈ ℝ ∧ 0 ≤ ( 𝐴 / ( log ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝐴 / ( log ‘ 𝑥 ) ) ) = ( 𝐴 / ( log ‘ 𝑥 ) ) ) |
57 |
55 56
|
syl |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( abs ‘ ( 𝐴 / ( log ‘ 𝑥 ) ) ) = ( 𝐴 / ( log ‘ 𝑥 ) ) ) |
58 |
|
loge |
⊢ ( log ‘ e ) = 1 |
59 |
|
simprr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → e ≤ 𝑥 ) |
60 |
|
epr |
⊢ e ∈ ℝ+ |
61 |
44
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → 𝑥 ∈ ℝ+ ) |
62 |
|
logleb |
⊢ ( ( e ∈ ℝ+ ∧ 𝑥 ∈ ℝ+ ) → ( e ≤ 𝑥 ↔ ( log ‘ e ) ≤ ( log ‘ 𝑥 ) ) ) |
63 |
60 61 62
|
sylancr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( e ≤ 𝑥 ↔ ( log ‘ e ) ≤ ( log ‘ 𝑥 ) ) ) |
64 |
59 63
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( log ‘ e ) ≤ ( log ‘ 𝑥 ) ) |
65 |
58 64
|
eqbrtrrid |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → 1 ≤ ( log ‘ 𝑥 ) ) |
66 |
|
1rp |
⊢ 1 ∈ ℝ+ |
67 |
|
rpregt0 |
⊢ ( 1 ∈ ℝ+ → ( 1 ∈ ℝ ∧ 0 < 1 ) ) |
68 |
66 67
|
mp1i |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 1 ∈ ℝ ∧ 0 < 1 ) ) |
69 |
26
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ ) |
70 |
69
|
rpregt0d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( ( log ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( log ‘ 𝑥 ) ) ) |
71 |
1
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → 𝐴 ∈ ℝ+ ) |
72 |
71
|
rpregt0d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) |
73 |
|
lediv2 |
⊢ ( ( ( 1 ∈ ℝ ∧ 0 < 1 ) ∧ ( ( log ‘ 𝑥 ) ∈ ℝ ∧ 0 < ( log ‘ 𝑥 ) ) ∧ ( 𝐴 ∈ ℝ ∧ 0 < 𝐴 ) ) → ( 1 ≤ ( log ‘ 𝑥 ) ↔ ( 𝐴 / ( log ‘ 𝑥 ) ) ≤ ( 𝐴 / 1 ) ) ) |
74 |
68 70 72 73
|
syl3anc |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 1 ≤ ( log ‘ 𝑥 ) ↔ ( 𝐴 / ( log ‘ 𝑥 ) ) ≤ ( 𝐴 / 1 ) ) ) |
75 |
65 74
|
mpbid |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ≤ ( 𝐴 / 1 ) ) |
76 |
5
|
adantr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → 𝐴 ∈ ℂ ) |
77 |
76
|
div1d |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 / 1 ) = 𝐴 ) |
78 |
75 77
|
breqtrd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( 𝐴 / ( log ‘ 𝑥 ) ) ≤ 𝐴 ) |
79 |
57 78
|
eqbrtrd |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ e ≤ 𝑥 ) ) → ( abs ‘ ( 𝐴 / ( log ‘ 𝑥 ) ) ) ≤ 𝐴 ) |
80 |
50 28 52 53 79
|
elo1d |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 𝐴 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
81 |
36 21 49 80
|
o1mul2 |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
82 |
34 81
|
eqeltrrd |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) − 𝐴 ) ) ∈ 𝑂(1) ) |
83 |
23 24 82
|
o1dif |
⊢ ( 𝜑 → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) ) ) |
84 |
7 83
|
mpbird |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
85 |
|
2re |
⊢ 2 ∈ ℝ |
86 |
|
rerpdivcl |
⊢ ( ( 2 ∈ ℝ ∧ ( log ‘ 𝑥 ) ∈ ℝ+ ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ ) |
87 |
85 26 86
|
sylancr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ ) |
88 |
|
nndivre |
⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℕ ) → ( 𝑥 / 𝑛 ) ∈ ℝ ) |
89 |
37 9 88
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ ) |
90 |
|
chpcl |
⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
91 |
89 90
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
92 |
12 91
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
93 |
10
|
nnrpd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ ) |
94 |
93
|
relogcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ ) |
95 |
92 94
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ ) |
96 |
8 95
|
fsumrecl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ ) |
97 |
87 96
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ ) |
98 |
8 92
|
fsumrecl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
99 |
97 98
|
resubcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ ) |
100 |
99 44
|
rerpdivcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ ) |
101 |
100
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ∈ ℂ ) |
102 |
101
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ℝ ) |
103 |
23
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ∈ ℝ ) |
104 |
|
2cnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ ) |
105 |
96
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ ) |
106 |
104 105
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ ) |
107 |
98
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) |
108 |
107 27
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
109 |
106 108
|
subcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ∈ ℂ ) |
110 |
109
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ ) |
111 |
43
|
gt0ne0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 ) |
112 |
110 37 111
|
redivcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) ∈ ℝ ) |
113 |
53
|
adantr |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ ) |
114 |
14 113
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) ∈ ℝ ) |
115 |
12
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
116 |
|
fzfid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin ) |
117 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ ) |
118 |
117
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ ) |
119 |
|
vmacl |
⊢ ( 𝑚 ∈ ℕ → ( Λ ‘ 𝑚 ) ∈ ℝ ) |
120 |
118 119
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ ) |
121 |
118
|
nnrpd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ ) |
122 |
121
|
relogcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ ) |
123 |
120 122
|
remulcld |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ ) |
124 |
116 123
|
fsumrecl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ ) |
125 |
9
|
nnrpd |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ ) |
126 |
|
rpdivcl |
⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ ) |
127 |
44 125 126
|
syl2an |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ ) |
128 |
127
|
relogcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
129 |
91 128
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
130 |
124 129
|
resubcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ ) |
131 |
130
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ ) |
132 |
115 131
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ) |
133 |
8 132
|
fsumcl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ) |
134 |
133
|
abscld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ ℝ ) |
135 |
132
|
abscld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ ℝ ) |
136 |
8 135
|
fsumrecl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ ℝ ) |
137 |
113 37
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · 𝑥 ) ∈ ℝ ) |
138 |
14 137
|
remulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ∈ ℝ ) |
139 |
8 132
|
fsumabs |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
140 |
53
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℝ ) |
141 |
37
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ ) |
142 |
140 141
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · 𝑥 ) ∈ ℝ ) |
143 |
13 142
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ∈ ℝ ) |
144 |
131
|
abscld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℝ ) |
145 |
142 10
|
nndivred |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 · 𝑥 ) / 𝑛 ) ∈ ℝ ) |
146 |
|
vmage0 |
⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) ) |
147 |
10 146
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) ) |
148 |
89
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℂ ) |
149 |
127
|
rpne0d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ≠ 0 ) |
150 |
131 148 149
|
absdivd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( abs ‘ ( 𝑥 / 𝑛 ) ) ) ) |
151 |
127
|
rpge0d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( 𝑥 / 𝑛 ) ) |
152 |
89 151
|
absidd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑥 / 𝑛 ) ) = ( 𝑥 / 𝑛 ) ) |
153 |
152
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( abs ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) |
154 |
150 153
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) |
155 |
|
fveq2 |
⊢ ( 𝑘 = 𝑚 → ( Λ ‘ 𝑘 ) = ( Λ ‘ 𝑚 ) ) |
156 |
|
fveq2 |
⊢ ( 𝑘 = 𝑚 → ( log ‘ 𝑘 ) = ( log ‘ 𝑚 ) ) |
157 |
155 156
|
oveq12d |
⊢ ( 𝑘 = 𝑚 → ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) |
158 |
157
|
cbvsumv |
⊢ Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) |
159 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ⌊ ‘ 𝑦 ) = ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) |
160 |
159
|
oveq2d |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( 1 ... ( ⌊ ‘ 𝑦 ) ) = ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) |
161 |
160
|
sumeq1d |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) |
162 |
158 161
|
syl5eq |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) |
163 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ψ ‘ 𝑦 ) = ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) |
164 |
|
fveq2 |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( log ‘ 𝑦 ) = ( log ‘ ( 𝑥 / 𝑛 ) ) ) |
165 |
163 164
|
oveq12d |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) |
166 |
162 165
|
oveq12d |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
167 |
|
id |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → 𝑦 = ( 𝑥 / 𝑛 ) ) |
168 |
166 167
|
oveq12d |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) |
169 |
168
|
fveq2d |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) = ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) ) |
170 |
169
|
breq1d |
⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝐴 ↔ ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) ≤ 𝐴 ) ) |
171 |
2
|
ad2antrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑦 ) ) ( ( Λ ‘ 𝑘 ) · ( log ‘ 𝑘 ) ) − ( ( ψ ‘ 𝑦 ) · ( log ‘ 𝑦 ) ) ) / 𝑦 ) ) ≤ 𝐴 ) |
172 |
10
|
nncnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ ) |
173 |
172
|
mulid2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) = 𝑛 ) |
174 |
|
fznnfl |
⊢ ( 𝑥 ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥 ) ) ) |
175 |
37 174
|
syl |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥 ) ) ) |
176 |
175
|
simplbda |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≤ 𝑥 ) |
177 |
173 176
|
eqbrtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) ≤ 𝑥 ) |
178 |
|
1red |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ ) |
179 |
178 141 93
|
lemuldivd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 · 𝑛 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑛 ) ) ) |
180 |
177 179
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ ( 𝑥 / 𝑛 ) ) |
181 |
|
1re |
⊢ 1 ∈ ℝ |
182 |
|
elicopnf |
⊢ ( 1 ∈ ℝ → ( ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) ↔ ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑛 ) ) ) ) |
183 |
181 182
|
ax-mp |
⊢ ( ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) ↔ ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑛 ) ) ) |
184 |
89 180 183
|
sylanbrc |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ( 1 [,) +∞ ) ) |
185 |
170 171 184
|
rspcdva |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( 𝑥 / 𝑛 ) ) ) ≤ 𝐴 ) |
186 |
154 185
|
eqbrtrrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 / 𝑛 ) ) ≤ 𝐴 ) |
187 |
144 140 127
|
ledivmul2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 / 𝑛 ) ) ≤ 𝐴 ↔ ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ ( 𝐴 · ( 𝑥 / 𝑛 ) ) ) ) |
188 |
186 187
|
mpbid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ ( 𝐴 · ( 𝑥 / 𝑛 ) ) ) |
189 |
24
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℂ ) |
190 |
141
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ ) |
191 |
10
|
nnne0d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 ) |
192 |
189 190 172 191
|
divassd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 · 𝑥 ) / 𝑛 ) = ( 𝐴 · ( 𝑥 / 𝑛 ) ) ) |
193 |
188 192
|
breqtrrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ ( ( 𝐴 · 𝑥 ) / 𝑛 ) ) |
194 |
144 145 12 147 193
|
lemul2ad |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ ( ( Λ ‘ 𝑛 ) · ( ( 𝐴 · 𝑥 ) / 𝑛 ) ) ) |
195 |
115 131
|
absmuld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( abs ‘ ( Λ ‘ 𝑛 ) ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
196 |
12 147
|
absidd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Λ ‘ 𝑛 ) ) = ( Λ ‘ 𝑛 ) ) |
197 |
196
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( Λ ‘ 𝑛 ) ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
198 |
195 197
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
199 |
142
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ ) |
200 |
115 172 199 191
|
div32d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) = ( ( Λ ‘ 𝑛 ) · ( ( 𝐴 · 𝑥 ) / 𝑛 ) ) ) |
201 |
194 198 200
|
3brtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ) |
202 |
8 135 143 201
|
fsumle |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ) |
203 |
37
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ ) |
204 |
24 203
|
mulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · 𝑥 ) ∈ ℂ ) |
205 |
115 172 191
|
divcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
206 |
8 204 205
|
fsummulc1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ) |
207 |
202 206
|
breqtrrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ) |
208 |
134 136 138 139 207
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ) |
209 |
124
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ ) |
210 |
91
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ ) |
211 |
94
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ ) |
212 |
210 211
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ ) |
213 |
209 212
|
addcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ ) |
214 |
115 213
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ ) |
215 |
115 210
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) |
216 |
27
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
217 |
215 216
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
218 |
8 214 217
|
fsumsub |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) |
219 |
210 216
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
220 |
115 213 219
|
subdid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) ) |
221 |
44
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ ) |
222 |
221 93
|
relogdivd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) = ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) ) |
223 |
222
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) ) ) |
224 |
210 216 211
|
subdid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) ) = ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) |
225 |
223 224
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) |
226 |
225
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ) |
227 |
209 219 212
|
subsub3d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) |
228 |
226 227
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) |
229 |
228
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( Λ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) ) |
230 |
115 210 216
|
mulassd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) = ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) |
231 |
230
|
oveq2d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑥 ) ) ) ) ) |
232 |
220 229 231
|
3eqtr4d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) |
233 |
232
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) |
234 |
|
fveq2 |
⊢ ( 𝑛 = 𝑚 → ( Λ ‘ 𝑛 ) = ( Λ ‘ 𝑚 ) ) |
235 |
|
oveq2 |
⊢ ( 𝑛 = 𝑚 → ( 𝑥 / 𝑛 ) = ( 𝑥 / 𝑚 ) ) |
236 |
235
|
fveq2d |
⊢ ( 𝑛 = 𝑚 → ( ψ ‘ ( 𝑥 / 𝑛 ) ) = ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) |
237 |
234 236
|
oveq12d |
⊢ ( 𝑛 = 𝑚 → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) |
238 |
|
fveq2 |
⊢ ( 𝑛 = 𝑚 → ( log ‘ 𝑛 ) = ( log ‘ 𝑚 ) ) |
239 |
237 238
|
oveq12d |
⊢ ( 𝑛 = 𝑚 → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) ) |
240 |
239
|
cbvsumv |
⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) |
241 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) → 𝑛 ∈ ℕ ) |
242 |
241
|
adantl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → 𝑛 ∈ ℕ ) |
243 |
242 11
|
syl |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
244 |
243
|
recnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
245 |
244
|
anasss |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
246 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑚 ∈ ℕ ) |
247 |
246
|
adantl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℕ ) |
248 |
247 119
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℝ ) |
249 |
248
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑚 ) ∈ ℂ ) |
250 |
247
|
nnrpd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑚 ∈ ℝ+ ) |
251 |
250
|
relogcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ ) |
252 |
251
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑚 ) ∈ ℂ ) |
253 |
249 252
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ ) |
254 |
253
|
adantrr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ ) |
255 |
245 254
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ ) |
256 |
37 255
|
fsumfldivdiag |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
257 |
37
|
adantr |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ ) |
258 |
257 247
|
nndivred |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑚 ) ∈ ℝ ) |
259 |
|
chpcl |
⊢ ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ ) |
260 |
258 259
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ ) |
261 |
260
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℂ ) |
262 |
249 261 252
|
mul32d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) ) |
263 |
248 251
|
remulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℝ ) |
264 |
263
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ ) |
265 |
264 261
|
mulcomd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) = ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
266 |
|
chpval |
⊢ ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) ) |
267 |
258 266
|
syl |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) ) |
268 |
267
|
oveq1d |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
269 |
|
fzfid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ∈ Fin ) |
270 |
269 264 244
|
fsummulc1 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
271 |
268 270
|
eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
272 |
262 265 271
|
3eqtrd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
273 |
272
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑚 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
274 |
123
|
recnd |
⊢ ( ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ∈ ℂ ) |
275 |
116 115 274
|
fsummulc2 |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
276 |
275
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) · ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
277 |
256 273 276
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑚 ) · ( ψ ‘ ( 𝑥 / 𝑚 ) ) ) · ( log ‘ 𝑚 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
278 |
240 277
|
syl5eq |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ) |
279 |
115 210 211
|
mulassd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) |
280 |
279
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) |
281 |
278 280
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ) |
282 |
105
|
2timesd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) |
283 |
115 209
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) ∈ ℂ ) |
284 |
115 212
|
mulcld |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ ) |
285 |
8 283 284
|
fsumadd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ) |
286 |
281 282 285
|
3eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ) |
287 |
115 209 212
|
adddid |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ) |
288 |
287
|
sumeq2dv |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) ) + ( ( Λ ‘ 𝑛 ) · ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ) |
289 |
286 288
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) ) |
290 |
92
|
recnd |
⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) |
291 |
8 27 290
|
fsummulc1 |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) |
292 |
289 291
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) + ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ 𝑛 ) ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) |
293 |
218 233 292
|
3eqtr4rd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) |
294 |
293
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) = ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑚 ) · ( log ‘ 𝑚 ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) |
295 |
25 24 203
|
mulassd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) · 𝑥 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 · 𝑥 ) ) ) |
296 |
208 294 295
|
3brtr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) · 𝑥 ) ) |
297 |
110 114 44
|
ledivmul2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) ↔ ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) · 𝑥 ) ) ) |
298 |
296 297
|
mpbird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) ) |
299 |
112 114 26 298
|
lediv1dd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) / ( log ‘ 𝑥 ) ) ) |
300 |
110
|
recnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) ∈ ℂ ) |
301 |
300 203 27 111 30
|
divdiv1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) |
302 |
109 27 203 30 111
|
divdiv32d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) ) |
303 |
106 108 27 30
|
divsubdird |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) ) ) |
304 |
104 105 27 30
|
div23d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) |
305 |
107 27 30
|
divcan4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) |
306 |
304 305
|
oveq12d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
307 |
303 306
|
eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
308 |
307
|
oveq1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( log ‘ 𝑥 ) ) / 𝑥 ) = ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) |
309 |
109 203 27 111 30
|
divdiv1d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) |
310 |
302 308 309
|
3eqtr3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) = ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) |
311 |
310
|
fveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) = ( abs ‘ ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) |
312 |
44 26
|
rpmulcld |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ+ ) |
313 |
312
|
rpcnd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ ) |
314 |
312
|
rpne0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ≠ 0 ) |
315 |
109 313 314
|
absdivd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) |
316 |
312
|
rpred |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ ) |
317 |
312
|
rpge0d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 𝑥 · ( log ‘ 𝑥 ) ) ) |
318 |
316 317
|
absidd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( 𝑥 · ( log ‘ 𝑥 ) ) ) |
319 |
318
|
oveq2d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) |
320 |
311 315 319
|
3eqtrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) = ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) |
321 |
301 320
|
eqtr4d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( ( 2 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ) |
322 |
25 24 27 30
|
divassd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 𝐴 ) / ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) |
323 |
299 321 322
|
3brtr3d |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) |
324 |
22
|
leabsd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ) |
325 |
102 22 103 323 324
|
letrd |
⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ≤ ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ) |
326 |
325
|
adantrr |
⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ≤ ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 𝐴 / ( log ‘ 𝑥 ) ) ) ) ) |
327 |
3 84 22 101 326
|
o1le |
⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) · ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) / 𝑥 ) ) ∈ 𝑂(1) ) |