Metamath Proof Explorer

Theorem mulogsum

Description: Asymptotic formula for sum_ n <_ x , ( mmu ( n ) / n ) log ( x / n ) = O(1) . Equation 10.2.6 of Shapiro, p. 406. (Contributed by Mario Carneiro, 14-May-2016)

Ref Expression
Assertion mulogsum ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 rpssre ⊢ ℝ+ ⊆ ℝ
2 ax-1cn ⊢ 1 ∈ ℂ
3 o1const ⊢ ( ( ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) )
4 1 2 3 mp2an ⊢ ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1)
5 1cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
6 fzfid ⊢ ( 𝑥 ∈ ℝ+ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
7 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
8 7 adantl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
9 mucl ⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ )
10 8 9 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
11 10 zred ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
12 11 8 nndivred ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
13 7 nnrpd ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
14 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
15 13 14 sylan2 ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
16 15 relogcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
17 12 16 remulcld ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
18 17 recnd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
19 6 18 fsumcl ⊢ ( 𝑥 ∈ ℝ+ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
20 19 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
21 mulogsumlem ⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1)
22 sumex ⊢ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ V
23 22 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ V )
24 21 a1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) )
25 23 24 o1mptrcl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
26 5 20 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
27 1red ⊢ ( ⊤ → 1 ∈ ℝ )
28 fz1ssnn ⊢ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ℕ
29 28 a1i ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ⊆ ℕ )
30 29 sselda ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
31 30 9 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
32 31 zred ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
33 32 30 nndivred ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
34 33 recnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
35 fzfid ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin )
36 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ )
37 36 adantl ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ )
38 37 nnrpd ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ )
39 38 rpcnne0d ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) )
40 reccl ⊢ ( ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) → ( 1 / 𝑚 ) ∈ ℂ )
41 39 40 syl ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 1 / 𝑚 ) ∈ ℂ )
42 35 41 fsumcl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ∈ ℂ )
43 simpl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 𝑥 ∈ ℝ+ )
44 43 13 14 syl2an ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
45 44 relogcld ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
46 45 recnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
47 34 42 46 subdid ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
48 47 sumeq2dv ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
49 fzfid ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
50 34 42 mulcld ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) ∈ ℂ )
51 18 adantlr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
52 49 50 51 fsumsub ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
53 oveq2 ⊢ ( 𝑘 = ( 𝑛 · 𝑚 ) → ( 1 / 𝑘 ) = ( 1 / ( 𝑛 · 𝑚 ) ) )
54 53 oveq2d ⊢ ( 𝑘 = ( 𝑛 · 𝑚 ) → ( ( μ ‘ 𝑛 ) · ( 1 / 𝑘 ) ) = ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) )
55 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
56 55 adantr ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 𝑥 ∈ ℝ )
57 ssrab2 ⊢ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ⊆ ℕ
58 simprr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } )
59 57 58 sselid ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → 𝑛 ∈ ℕ )
60 59 9 syl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
61 60 zcnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
62 elfznn ⊢ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑘 ∈ ℕ )
63 62 adantl ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑘 ∈ ℕ )
64 63 nnrecred ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑘 ) ∈ ℝ )
65 64 recnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑘 ) ∈ ℂ )
66 65 adantrr ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( 1 / 𝑘 ) ∈ ℂ )
67 61 66 mulcld ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ ( 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∧ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ) ) → ( ( μ ‘ 𝑛 ) · ( 1 / 𝑘 ) ) ∈ ℂ )
68 54 56 67 dvdsflsumcom ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( μ ‘ 𝑛 ) · ( 1 / 𝑘 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) )
69 oveq2 ⊢ ( 𝑘 = 1 → ( 1 / 𝑘 ) = ( 1 / 1 ) )
70 1div1e1 ⊢ ( 1 / 1 ) = 1
71 69 70 eqtrdi ⊢ ( 𝑘 = 1 → ( 1 / 𝑘 ) = 1 )
72 flge1nn ⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
73 55 72 sylan ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ )
74 nnuz ⊢ ℕ = ( ℤ≥ ‘ 1 )
75 73 74 eleqtrdi ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) )
76 eluzfz1 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ( ℤ≥ ‘ 1 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
77 75 76 syl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → 1 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
78 71 49 29 77 65 musumsum ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑘 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑛 ∈ { 𝑦 ∈ ℕ ∣ 𝑦 ∥ 𝑘 } ( ( μ ‘ 𝑛 ) · ( 1 / 𝑘 ) ) = 1 )
79 31 zcnd ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
80 79 adantr ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
81 30 adantr ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑛 ∈ ℕ )
82 81 nnrpd ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑛 ∈ ℝ+ )
83 82 rpcnne0d ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
84 divdiv1 ⊢ ( ( ( μ ‘ 𝑛 ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ∧ ( 𝑚 ∈ ℂ ∧ 𝑚 ≠ 0 ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) / 𝑚 ) = ( ( μ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) )
85 80 83 39 84 syl3anc ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) / 𝑚 ) = ( ( μ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) )
86 34 adantr ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( μ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
87 37 nncnd ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℂ )
88 37 nnne0d ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ≠ 0 )
89 86 87 88 divrecd ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) / 𝑚 ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) )
90 nnmulcl ⊢ ( ( 𝑛 ∈ ℕ ∧ 𝑚 ∈ ℕ ) → ( 𝑛 · 𝑚 ) ∈ ℕ )
91 30 36 90 syl2an ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 · 𝑚 ) ∈ ℕ )
92 91 nncnd ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 · 𝑚 ) ∈ ℂ )
93 91 nnne0d ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( 𝑛 · 𝑚 ) ≠ 0 )
94 80 92 93 divrecd ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( μ ‘ 𝑛 ) / ( 𝑛 · 𝑚 ) ) = ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) )
95 85 89 94 3eqtr3rd ⊢ ( ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) )
96 95 sumeq2dv ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) )
97 35 34 41 fsummulc2 ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( 1 / 𝑚 ) ) )
98 96 97 eqtr4d ⊢ ( ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) = ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) )
99 98 sumeq2dv ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( 1 / ( 𝑛 · 𝑚 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) )
100 68 78 99 3eqtr3rd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) = 1 )
101 100 oveq1d ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
102 48 52 101 3eqtrd ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
103 102 adantl ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) )
104 25 26 27 103 o1eq ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( 1 / 𝑚 ) − ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) ) )
105 21 104 mpbii ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ 𝑂(1) )
106 5 20 105 o1dif ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) ↔ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1) ) )
107 4 106 mpbii ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1) )
108 107 mptru ⊢ ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) / 𝑛 ) · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ 𝑂(1)