Step |
Hyp |
Ref |
Expression |
1 |
|
fzfid |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ) |
2 |
|
elfznn |
⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ ℕ ) |
3 |
2
|
adantl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℕ ) |
4 |
3
|
nnrpd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℝ+ ) |
5 |
4
|
relogcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑘 ) ∈ ℝ ) |
6 |
5 3
|
nndivred |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ 𝑘 ) / 𝑘 ) ∈ ℝ ) |
7 |
1 6
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) ∈ ℝ ) |
8 |
7
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) ∈ ℂ ) |
9 |
|
elioore |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ ) |
10 |
9
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ ) |
11 |
|
1rp |
⊢ 1 ∈ ℝ+ |
12 |
11
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ ) |
13 |
|
1red |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ ) |
14 |
|
eliooord |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) ) |
15 |
14
|
adantl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) ) |
16 |
15
|
simpld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 ) |
17 |
13 10 16
|
ltled |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 ) |
18 |
10 12 17
|
rpgecld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ ) |
19 |
18
|
relogcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ ) |
20 |
19
|
resqcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) ↑ 2 ) ∈ ℝ ) |
21 |
20
|
rehalfcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ∈ ℝ ) |
22 |
21
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ∈ ℂ ) |
23 |
19
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
24 |
10 16
|
rplogcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ ) |
25 |
24
|
rpne0d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 ) |
26 |
8 22 23 25
|
divsubdird |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) / ( log ‘ 𝑥 ) ) = ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) / ( log ‘ 𝑥 ) ) ) ) |
27 |
7 21
|
resubcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ∈ ℝ ) |
28 |
27
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ∈ ℂ ) |
29 |
28 23 25
|
divrecd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) / ( log ‘ 𝑥 ) ) = ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) |
30 |
20
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) ↑ 2 ) ∈ ℂ ) |
31 |
|
2cnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ ) |
32 |
|
2ne0 |
⊢ 2 ≠ 0 |
33 |
32
|
a1i |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ≠ 0 ) |
34 |
30 31 23 33 25
|
divdiv32d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) / ( log ‘ 𝑥 ) ) = ( ( ( ( log ‘ 𝑥 ) ↑ 2 ) / ( log ‘ 𝑥 ) ) / 2 ) ) |
35 |
23
|
sqvald |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) ↑ 2 ) = ( ( log ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) ) |
36 |
35
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) ↑ 2 ) / ( log ‘ 𝑥 ) ) = ( ( ( log ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) ) |
37 |
23 23 25
|
divcan3d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = ( log ‘ 𝑥 ) ) |
38 |
36 37
|
eqtrd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) ↑ 2 ) / ( log ‘ 𝑥 ) ) = ( log ‘ 𝑥 ) ) |
39 |
38
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 2 ) / ( log ‘ 𝑥 ) ) / 2 ) = ( ( log ‘ 𝑥 ) / 2 ) ) |
40 |
34 39
|
eqtrd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) / ( log ‘ 𝑥 ) ) = ( ( log ‘ 𝑥 ) / 2 ) ) |
41 |
40
|
oveq2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) |
42 |
26 29 41
|
3eqtr3rd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) = ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) |
43 |
42
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) ) |
44 |
24
|
rprecred |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℝ ) |
45 |
18
|
ex |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) ) |
46 |
45
|
ssrdv |
⊢ ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ+ ) |
47 |
|
eqid |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) |
48 |
47
|
logdivsum |
⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) : ℝ+ ⟶ ℝ ∧ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) ∈ dom ⇝𝑟 ∧ ( ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) ⇝𝑟 1 ∧ 1 ∈ ℝ+ ∧ e ≤ 1 ) → ( abs ‘ ( ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) ‘ 1 ) − 1 ) ) ≤ ( ( log ‘ 1 ) / 1 ) ) ) |
49 |
48
|
simp2i |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) ∈ dom ⇝𝑟 |
50 |
|
rlimdmo1 |
⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) ∈ dom ⇝𝑟 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) ∈ 𝑂(1) ) |
51 |
49 50
|
mp1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) ∈ 𝑂(1) ) |
52 |
46 51
|
o1res2 |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) ) ∈ 𝑂(1) ) |
53 |
|
divlogrlim |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 |
54 |
|
rlimo1 |
⊢ ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
55 |
53 54
|
mp1i |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
56 |
27 44 52 55
|
o1mul2 |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − ( ( ( log ‘ 𝑥 ) ↑ 2 ) / 2 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
57 |
43 56
|
eqeltrd |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) ) |
58 |
8 23 25
|
divcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) ∈ ℂ ) |
59 |
23
|
halfcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℂ ) |
60 |
58 59
|
subcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ∈ ℂ ) |
61 |
|
elfznn |
⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ ) |
62 |
61
|
adantl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ ) |
63 |
|
vmacl |
⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
64 |
62 63
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
65 |
64 62
|
nndivred |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
66 |
18
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ ) |
67 |
62
|
nnrpd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ ) |
68 |
66 67
|
rpdivcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ ) |
69 |
68
|
relogcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) |
70 |
65 69
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
71 |
1 70
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
72 |
71
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) |
73 |
24
|
rpcnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ ) |
74 |
72 73 25
|
divcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ ) |
75 |
73
|
halfcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℂ ) |
76 |
74 75
|
subcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ∈ ℂ ) |
77 |
58 74 59
|
nnncan2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) ) |
78 |
8 72 23 25
|
divsubdird |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) = ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) ) ) |
79 |
|
fzfid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin ) |
80 |
64
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
81 |
62
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑛 ∈ ℕ ) |
82 |
|
elfznn |
⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ ) |
83 |
82
|
adantl |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ ) |
84 |
81 83
|
nnmulcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 · 𝑚 ) ∈ ℕ ) |
85 |
80 84
|
nndivred |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) ∈ ℝ ) |
86 |
79 85
|
fsumrecl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) ∈ ℝ ) |
87 |
86
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) ∈ ℂ ) |
88 |
70
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ ) |
89 |
1 87 88
|
fsumsub |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
90 |
64
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
91 |
62
|
nncnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ ) |
92 |
62
|
nnne0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 ) |
93 |
90 91 92
|
divcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
94 |
83
|
nnrecred |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 1 / 𝑚 ) ∈ ℝ ) |
95 |
79 94
|
fsumrecl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ∈ ℝ ) |
96 |
95
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ∈ ℂ ) |
97 |
69
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ ) |
98 |
93 96 97
|
subdid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
99 |
90
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
100 |
91
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑛 ∈ ℂ ) |
101 |
83
|
nncnd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℂ ) |
102 |
92
|
adantr |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑛 ≠ 0 ) |
103 |
83
|
nnne0d |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ≠ 0 ) |
104 |
99 100 101 102 103
|
divdiv1d |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) / 𝑚 ) = ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) ) |
105 |
99 100 102
|
divcld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
106 |
105 101 103
|
divrecd |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) / 𝑚 ) = ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) ) |
107 |
104 106
|
eqtr3d |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) = ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) ) |
108 |
107
|
sumeq2dv |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) ) |
109 |
101 103
|
reccld |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 1 / 𝑚 ) ∈ ℂ ) |
110 |
79 93 109
|
fsummulc2 |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) ) |
111 |
108 110
|
eqtr4d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) = ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) ) |
112 |
111
|
oveq1d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
113 |
98 112
|
eqtr4d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
114 |
113
|
sumeq2dv |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
115 |
|
vmasum |
⊢ ( 𝑘 ∈ ℕ → Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( Λ ‘ 𝑛 ) = ( log ‘ 𝑘 ) ) |
116 |
3 115
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( Λ ‘ 𝑛 ) = ( log ‘ 𝑘 ) ) |
117 |
116
|
oveq1d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( Λ ‘ 𝑛 ) / 𝑘 ) = ( ( log ‘ 𝑘 ) / 𝑘 ) ) |
118 |
|
fzfid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... 𝑘 ) ∈ Fin ) |
119 |
|
dvdsssfz1 |
⊢ ( 𝑘 ∈ ℕ → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ( 1 ... 𝑘 ) ) |
120 |
3 119
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ( 1 ... 𝑘 ) ) |
121 |
118 120
|
ssfid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ∈ Fin ) |
122 |
3
|
nncnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℂ ) |
123 |
|
ssrab2 |
⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ℕ |
124 |
|
simprr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) |
125 |
123 124
|
sseldi |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑛 ∈ ℕ ) |
126 |
125 63
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ ) |
127 |
126
|
recnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
128 |
127
|
anassrs |
⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) → ( Λ ‘ 𝑛 ) ∈ ℂ ) |
129 |
3
|
nnne0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ≠ 0 ) |
130 |
121 122 128 129
|
fsumdivc |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( Λ ‘ 𝑛 ) / 𝑘 ) = Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑛 ) / 𝑘 ) ) |
131 |
117 130
|
eqtr3d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ 𝑘 ) / 𝑘 ) = Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑛 ) / 𝑘 ) ) |
132 |
131
|
sumeq2dv |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) = Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑛 ) / 𝑘 ) ) |
133 |
|
oveq2 |
⊢ ( 𝑘 = ( 𝑛 · 𝑚 ) → ( ( Λ ‘ 𝑛 ) / 𝑘 ) = ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) ) |
134 |
2
|
ad2antrl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑘 ∈ ℕ ) |
135 |
134
|
nncnd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑘 ∈ ℂ ) |
136 |
134
|
nnne0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑘 ≠ 0 ) |
137 |
127 135 136
|
divcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( ( Λ ‘ 𝑛 ) / 𝑘 ) ∈ ℂ ) |
138 |
133 10 137
|
dvdsflsumcom |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( Λ ‘ 𝑛 ) / 𝑘 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) ) |
139 |
132 138
|
eqtrd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) ) |
140 |
139
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( Λ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
141 |
89 114 140
|
3eqtr4rd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
142 |
141
|
oveq1d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) |
143 |
77 78 142
|
3eqtr2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) |
144 |
143
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ) |
145 |
|
1red |
⊢ ( ⊤ → 1 ∈ ℝ ) |
146 |
1 65
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ ) |
147 |
146 24
|
rerpdivcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ∈ ℝ ) |
148 |
|
ioossre |
⊢ ( 1 (,) +∞ ) ⊆ ℝ |
149 |
|
ax-1cn |
⊢ 1 ∈ ℂ |
150 |
|
o1const |
⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) ) |
151 |
148 149 150
|
mp2an |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) |
152 |
151
|
a1i |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) ) |
153 |
147
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ∈ ℂ ) |
154 |
12
|
rpcnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℂ ) |
155 |
146
|
recnd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ ) |
156 |
155 23 23 25
|
divsubdird |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) ) ) |
157 |
155 23
|
subcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℂ ) |
158 |
157 23 25
|
divrecd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) |
159 |
23 25
|
dividd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) = 1 ) |
160 |
159
|
oveq2d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − 1 ) ) |
161 |
156 158 160
|
3eqtr3rd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − 1 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) |
162 |
161
|
mpteq2dva |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − 1 ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) ) |
163 |
146 19
|
resubcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℝ ) |
164 |
|
vmadivsum |
⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) |
165 |
164
|
a1i |
⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
166 |
46 165
|
o1res2 |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
167 |
163 44 166 55
|
o1mul2 |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) |
168 |
162 167
|
eqeltrd |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) − 1 ) ) ∈ 𝑂(1) ) |
169 |
153 154 168
|
o1dif |
⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) ) ) |
170 |
152 169
|
mpbird |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
171 |
147 170
|
o1lo1d |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) ∈ ≤𝑂(1) ) |
172 |
95 69
|
resubcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) |
173 |
65 172
|
remulcld |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ ) |
174 |
1 173
|
fsumrecl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ ) |
175 |
174 24
|
rerpdivcld |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ ) |
176 |
|
1red |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ ) |
177 |
|
vmage0 |
⊢ ( 𝑛 ∈ ℕ → 0 ≤ ( Λ ‘ 𝑛 ) ) |
178 |
62 177
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Λ ‘ 𝑛 ) ) |
179 |
64 67 178
|
divge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) |
180 |
68
|
rpred |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ ) |
181 |
91
|
mulid2d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) = 𝑛 ) |
182 |
|
fznnfl |
⊢ ( 𝑥 ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥 ) ) ) |
183 |
10 182
|
syl |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥 ) ) ) |
184 |
183
|
simplbda |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≤ 𝑥 ) |
185 |
181 184
|
eqbrtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) ≤ 𝑥 ) |
186 |
10
|
adantr |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ ) |
187 |
176 186 67
|
lemuldivd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 · 𝑛 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑛 ) ) ) |
188 |
185 187
|
mpbid |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ ( 𝑥 / 𝑛 ) ) |
189 |
|
harmonicubnd |
⊢ ( ( ( 𝑥 / 𝑛 ) ∈ ℝ ∧ 1 ≤ ( 𝑥 / 𝑛 ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( 𝑥 / 𝑛 ) ) + 1 ) ) |
190 |
180 188 189
|
syl2anc |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( 𝑥 / 𝑛 ) ) + 1 ) ) |
191 |
95 69 176
|
lesubadd2d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ≤ 1 ↔ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ≤ ( ( log ‘ ( 𝑥 / 𝑛 ) ) + 1 ) ) ) |
192 |
190 191
|
mpbird |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ≤ 1 ) |
193 |
172 176 65 179 192
|
lemul2ad |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 1 ) ) |
194 |
93
|
mulid1d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · 1 ) = ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) |
195 |
193 194
|
breqtrd |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) |
196 |
1 173 65 195
|
fsumle |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ) |
197 |
174 146 24 196
|
lediv1dd |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) |
198 |
197
|
adantrr |
⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) / ( log ‘ 𝑥 ) ) ) |
199 |
145 171 147 175 198
|
lo1le |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ≤𝑂(1) ) |
200 |
|
0red |
⊢ ( ⊤ → 0 ∈ ℝ ) |
201 |
|
harmoniclbnd |
⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( log ‘ ( 𝑥 / 𝑛 ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) |
202 |
68 201
|
syl |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) |
203 |
95 69
|
subge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 0 ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ↔ ( log ‘ ( 𝑥 / 𝑛 ) ) ≤ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) ) |
204 |
202 203
|
mpbird |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) |
205 |
65 172 179 204
|
mulge0d |
⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
206 |
1 173 205
|
fsumge0 |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) |
207 |
174 24 206
|
divge0d |
⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) |
208 |
175 200 207
|
o1lo12 |
⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ ≤𝑂(1) ) ) |
209 |
199 208
|
mpbird |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) |
210 |
144 209
|
eqeltrd |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ) ∈ 𝑂(1) ) |
211 |
60 76 210
|
o1dif |
⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ 𝑘 ) / 𝑘 ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) ) ) |
212 |
57 211
|
mpbid |
⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) ) |
213 |
212
|
mptru |
⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) |