Metamath Proof Explorer

Theorem vmalogdivsum

Description: The sum sum_ n <_ x , Lam ( n ) log n / n is asymptotic to log ^ 2 ( x ) / 2 + O ( log x ) . Exercise 9.1.7 of Shapiro, p. 336. (Contributed by Mario Carneiro, 30-May-2016)

Ref Expression
Assertion vmalogdivsum ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 elioore ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
2 1 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
3 1rp ⊢ 1 ∈ ℝ+
4 3 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
5 1red ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
6 eliooord ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
7 6 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
8 7 simpld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
9 5 2 8 ltled ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
10 2 4 9 rpgecld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
11 10 ex ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) )
12 11 ssrdv ⊢ ( ⊤ → ( 1 (,) +∞ ) ⊆ ℝ+ )
13 vmadivsum ⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)
14 13 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
15 12 14 o1res2 ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
16 fzfid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
17 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
18 17 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
19 vmacl ⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
20 18 19 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
21 20 18 nndivred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
22 21 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
23 16 22 fsumcl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
24 10 relogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
25 24 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
26 23 25 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
27 18 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
28 27 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
29 21 28 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
30 16 29 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
31 2 8 rplogcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
32 30 31 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
33 24 rehalfcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℝ )
34 32 33 resubcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ∈ ℝ )
35 34 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ∈ ℂ )
36 33 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / 2 ) ∈ ℂ )
37 23 36 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ 𝑥 ) / 2 ) ) ∈ ℂ )
38 32 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ∈ ℂ )
39 37 38 36 nnncan2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) )
40 23 36 36 subsub4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( ( log ‘ 𝑥 ) / 2 ) + ( ( log ‘ 𝑥 ) / 2 ) ) ) )
41 25 2halvesd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) / 2 ) + ( ( log ‘ 𝑥 ) / 2 ) ) = ( log ‘ 𝑥 ) )
42 41 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( ( log ‘ 𝑥 ) / 2 ) + ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) )
43 40 42 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) )
44 43 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) )
45 23 36 38 sub32d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) )
46 10 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
47 46 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
48 21 47 remulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
49 48 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
50 29 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
51 16 49 50 fsumsub ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
52 46 27 relogdivd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) = ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) )
53 52 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) ) )
54 25 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
55 28 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
56 22 54 55 subdid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( ( log ‘ 𝑥 ) − ( log ‘ 𝑛 ) ) ) = ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
57 53 56 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
58 57 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
59 20 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
60 18 nncnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
61 18 nnne0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
62 59 60 61 divcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
63 16 25 62 fsummulc1 ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) )
64 63 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
65 51 58 64 3eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) )
66 65 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) )
67 23 25 mulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
68 30 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
69 31 rpne0d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
70 67 68 25 69 divsubdird ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) = ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) )
71 23 25 69 divcan4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) )
72 71 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑥 ) ) / ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) )
73 66 70 72 3eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) )
74 73 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) )
75 45 74 eqtr4d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( ( log ‘ 𝑥 ) / 2 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) )
76 39 44 75 3eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) )
77 76 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) )
78 vmalogdivsum2 ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1)
79 77 78 eqeltrdi ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ) ∈ 𝑂(1) )
80 26 35 79 o1dif ⊢ ( ⊤ → ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) ) )
81 15 80 mpbid ⊢ ( ⊤ → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1) )
82 81 mptru ⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) − ( ( log ‘ 𝑥 ) / 2 ) ) ) ∈ 𝑂(1)