Metamath Proof Explorer

Theorem selberglem2

Description: Lemma for selberg . (Contributed by Mario Carneiro, 23-May-2016)

Ref Expression
Hypothesis selberglem1.t ⊢ 𝑇 = ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 )
Assertion selberglem2 ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)

Proof

Step Hyp Ref Expression
1 selberglem1.t ⊢ 𝑇 = ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 )
2 reex ⊢ ℝ ∈ V
3 rpssre ⊢ ℝ+ ⊆ ℝ
4 2 3 ssexi ⊢ ℝ+ ∈ V
5 4 a1i ⊢ ( ⊤ → ℝ+ ∈ V )
6 fzfid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
7 elfznn ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
8 7 adantl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
9 mucl ⊢ ( 𝑛 ∈ ℕ → ( μ ‘ 𝑛 ) ∈ ℤ )
10 8 9 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℤ )
11 10 zred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
12 11 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( μ ‘ 𝑛 ) ∈ ℂ )
13 fzfid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ Fin )
14 elfznn ⊢ ( 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) → 𝑚 ∈ ℕ )
15 14 adantl ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℕ )
16 15 nnrpd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → 𝑚 ∈ ℝ+ )
17 16 relogcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( log ‘ 𝑚 ) ∈ ℝ )
18 17 resqcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( log ‘ 𝑚 ) ↑ 2 ) ∈ ℝ )
19 13 18 fsumrecl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) ∈ ℝ )
20 simplr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
21 19 20 rerpdivcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ∈ ℝ )
22 21 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ∈ ℂ )
23 simpr ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
24 7 nnrpd ⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℝ+ )
25 rpdivcl ⊢ ( ( 𝑥 ∈ ℝ+ ∧ 𝑛 ∈ ℝ+ ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
26 23 24 25 syl2an ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
27 26 relogcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
28 27 resqcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ∈ ℝ )
29 2re ⊢ 2 ∈ ℝ
30 remulcl ⊢ ( ( 2 ∈ ℝ ∧ ( log ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ ) → ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
31 29 27 30 sylancr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
32 resubcl ⊢ ( ( 2 ∈ ℝ ∧ ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ ) → ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
33 29 31 32 sylancr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
34 28 33 readdcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℝ )
35 34 8 nndivred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) ∈ ℝ )
36 1 35 eqeltrid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑇 ∈ ℝ )
37 36 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑇 ∈ ℂ )
38 22 37 subcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ∈ ℂ )
39 12 38 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ∈ ℂ )
40 6 39 fsumcl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ∈ ℂ )
41 12 37 mulcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · 𝑇 ) ∈ ℂ )
42 6 41 fsumcl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) ∈ ℂ )
43 2cn ⊢ 2 ∈ ℂ
44 relogcl ⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
45 44 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
46 45 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
47 mulcl ⊢ ( ( 2 ∈ ℂ ∧ ( log ‘ 𝑥 ) ∈ ℂ ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ )
48 43 46 47 sylancr ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 2 · ( log ‘ 𝑥 ) ) ∈ ℂ )
49 42 48 subcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
50 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) )
51 eqidd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
52 5 40 49 50 51 offval2 ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) )
53 40 42 48 addsubassd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
54 rpcnne0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
55 54 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
56 55 simpld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℂ )
57 11 adantr ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( μ ‘ 𝑛 ) ∈ ℝ )
58 57 18 remulcld ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) ∈ ℝ )
59 13 58 fsumrecl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) ∈ ℝ )
60 59 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) ∈ ℂ )
61 55 simprd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≠ 0 )
62 6 56 60 61 fsumdivc ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) )
63 18 recnd ⊢ ( ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) ∧ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ) → ( ( log ‘ 𝑚 ) ↑ 2 ) ∈ ℂ )
64 13 63 fsumcl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) ∈ ℂ )
65 55 adantr ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
66 divass ⊢ ( ( ( μ ‘ 𝑛 ) ∈ ℂ ∧ Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( μ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) = ( ( μ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ) )
67 12 64 65 66 syl3anc ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) = ( ( μ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ) )
68 13 12 63 fsummulc2 ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) )
69 68 oveq1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( μ ‘ 𝑛 ) · Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) )
70 22 37 npcand ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) + 𝑇 ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) )
71 70 oveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) + 𝑇 ) ) = ( ( μ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ) )
72 12 38 37 adddid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · ( ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) + 𝑇 ) ) = ( ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( ( μ ‘ 𝑛 ) · 𝑇 ) ) )
73 71 72 eqtr3d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( μ ‘ 𝑛 ) · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ) = ( ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( ( μ ‘ 𝑛 ) · 𝑇 ) ) )
74 67 69 73 3eqtr3d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) = ( ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( ( μ ‘ 𝑛 ) · 𝑇 ) ) )
75 74 sumeq2dv ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( ( μ ‘ 𝑛 ) · 𝑇 ) ) )
76 6 39 41 fsumadd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( ( μ ‘ 𝑛 ) · 𝑇 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) ) )
77 62 75 76 3eqtrrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) )
78 77 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) ) − ( 2 · ( log ‘ 𝑥 ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
79 53 78 eqtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) )
80 79 mpteq2dva ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
81 52 80 eqtrd ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) )
82 1red ⊢ ( ⊤ → 1 ∈ ℝ )
83 6 28 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ∈ ℝ )
84 83 23 rerpdivcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) ∈ ℝ )
85 84 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) ∈ ℂ )
86 2cnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℂ )
87 2nn0 ⊢ 2 ∈ ℕ0
88 logexprlim ⊢ ( 2 ∈ ℕ0 → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) ) ⇝𝑟 ( ! ‘ 2 ) )
89 87 88 mp1i ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) ) ⇝𝑟 ( ! ‘ 2 ) )
90 2cnd ⊢ ( ⊤ → 2 ∈ ℂ )
91 rlimconst ⊢ ( ( ℝ+ ⊆ ℝ ∧ 2 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 2 ) ⇝𝑟 2 )
92 3 90 91 sylancr ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ 2 ) ⇝𝑟 2 )
93 85 86 89 92 rlimadd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ) ⇝𝑟 ( ( ! ‘ 2 ) + 2 ) )
94 rlimo1 ⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ) ⇝𝑟 ( ( ! ‘ 2 ) + 2 ) → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ) ∈ 𝑂(1) )
95 93 94 syl ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ) ∈ 𝑂(1) )
96 readdcl ⊢ ( ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ∈ ℝ )
97 84 29 96 sylancl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ∈ ℝ )
98 40 abscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∈ ℝ )
99 97 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ∈ ℂ )
100 99 abscld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ) ∈ ℝ )
101 39 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∈ ℝ )
102 6 101 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∈ ℝ )
103 6 39 fsumabs ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) )
104 readdcl ⊢ ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ∈ ℝ ∧ 2 ∈ ℝ ) → ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) ∈ ℝ )
105 28 29 104 sylancl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) ∈ ℝ )
106 105 20 rerpdivcld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) ∈ ℝ )
107 6 106 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) ∈ ℝ )
108 38 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ∈ ℝ )
109 12 38 absmuld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) = ( ( abs ‘ ( μ ‘ 𝑛 ) ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) )
110 12 abscld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑛 ) ) ∈ ℝ )
111 1red ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
112 38 absge0d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) )
113 mule1 ⊢ ( 𝑛 ∈ ℕ → ( abs ‘ ( μ ‘ 𝑛 ) ) ≤ 1 )
114 8 113 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( μ ‘ 𝑛 ) ) ≤ 1 )
115 110 111 108 112 114 lemul1ad ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑛 ) ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( 1 · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) )
116 108 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ∈ ℂ )
117 116 mullidd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) = ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) )
118 115 117 breqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( μ ‘ 𝑛 ) ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) )
119 109 118 eqbrtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) )
120 65 simpld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
121 120 38 absmuld ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑥 · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) = ( ( abs ‘ 𝑥 ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) )
122 120 22 37 subdid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) = ( ( 𝑥 · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ) − ( 𝑥 · 𝑇 ) ) )
123 65 simprd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ≠ 0 )
124 64 120 123 divcan2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ) = Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) )
125 34 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ )
126 8 nnrpd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
127 rpcnne0 ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
128 126 127 syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) )
129 divass ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑥 · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) / 𝑛 ) = ( 𝑥 · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) ) )
130 1 oveq2i ⊢ ( 𝑥 · 𝑇 ) = ( 𝑥 · ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / 𝑛 ) )
131 129 130 eqtr4di ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑥 · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) / 𝑛 ) = ( 𝑥 · 𝑇 ) )
132 div23 ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( ( 𝑥 · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) / 𝑛 ) = ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
133 131 132 eqtr3d ⊢ ( ( 𝑥 ∈ ℂ ∧ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ ∧ ( 𝑛 ∈ ℂ ∧ 𝑛 ≠ 0 ) ) → ( 𝑥 · 𝑇 ) = ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
134 120 125 128 133 syl3anc ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · 𝑇 ) = ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
135 124 134 oveq12d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 · ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) ) − ( 𝑥 · 𝑇 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) − ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) )
136 122 135 eqtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) = ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) − ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) )
137 136 fveq2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑥 · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) = ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) − ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) ) )
138 rprege0 ⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
139 absid ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( abs ‘ 𝑥 ) = 𝑥 )
140 20 138 139 3syl ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ 𝑥 ) = 𝑥 )
141 140 oveq1d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ 𝑥 ) · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) = ( 𝑥 · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) )
142 121 137 141 3eqtr3d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) − ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) ) = ( 𝑥 · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) )
143 8 nncnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
144 143 mullidd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) = 𝑛 )
145 rpre ⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
146 145 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
147 fznnfl ⊢ ( 𝑥 ∈ ℝ → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥 ) ) )
148 146 147 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ↔ ( 𝑛 ∈ ℕ ∧ 𝑛 ≤ 𝑥 ) ) )
149 148 simplbda ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≤ 𝑥 )
150 144 149 eqbrtrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · 𝑛 ) ≤ 𝑥 )
151 20 rpred ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
152 111 151 126 lemuldivd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 · 𝑛 ) ≤ 𝑥 ↔ 1 ≤ ( 𝑥 / 𝑛 ) ) )
153 150 152 mpbid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ ( 𝑥 / 𝑛 ) )
154 log2sumbnd ⊢ ( ( ( 𝑥 / 𝑛 ) ∈ ℝ+ ∧ 1 ≤ ( 𝑥 / 𝑛 ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) − ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) ) ≤ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) )
155 26 153 154 syl2anc ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) − ( ( 𝑥 / 𝑛 ) · ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 2 − ( 2 · ( log ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ) ) ≤ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) )
156 142 155 eqbrtrrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) )
157 108 105 20 lemuldiv2d ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 · ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) ↔ ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ≤ ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) ) )
158 156 157 mpbid ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ≤ ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) )
159 101 108 106 119 158 letrd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) )
160 6 101 106 159 fsumle ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) )
161 6 105 fsumrecl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) ∈ ℝ )
162 remulcl ⊢ ( ( 𝑥 ∈ ℝ ∧ 2 ∈ ℝ ) → ( 𝑥 · 2 ) ∈ ℝ )
163 146 29 162 sylancl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · 2 ) ∈ ℝ )
164 83 163 readdcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 𝑥 · 2 ) ) ∈ ℝ )
165 28 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ∈ ℂ )
166 2cnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ )
167 6 165 166 fsumadd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 2 ) )
168 fsumconst ⊢ ( ( ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin ∧ 2 ∈ ℂ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 2 = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · 2 ) )
169 6 43 168 sylancl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 2 = ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · 2 ) )
170 138 adantl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
171 flge0nn0 ⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
172 hashfz1 ⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
173 170 171 172 3syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) = ( ⌊ ‘ 𝑥 ) )
174 173 oveq1d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ♯ ‘ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) · 2 ) = ( ( ⌊ ‘ 𝑥 ) · 2 ) )
175 169 174 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 2 = ( ( ⌊ ‘ 𝑥 ) · 2 ) )
176 175 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) 2 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( ( ⌊ ‘ 𝑥 ) · 2 ) ) )
177 167 176 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( ( ⌊ ‘ 𝑥 ) · 2 ) ) )
178 reflcl ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
179 146 178 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ∈ ℝ )
180 29 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 2 ∈ ℝ )
181 179 180 remulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) · 2 ) ∈ ℝ )
182 flle ⊢ ( 𝑥 ∈ ℝ → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
183 146 182 syl ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ≤ 𝑥 )
184 2pos ⊢ 0 < 2
185 29 184 pm3.2i ⊢ ( 2 ∈ ℝ ∧ 0 < 2 )
186 185 a1i ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 2 ∈ ℝ ∧ 0 < 2 ) )
187 lemul1 ⊢ ( ( ( ⌊ ‘ 𝑥 ) ∈ ℝ ∧ 𝑥 ∈ ℝ ∧ ( 2 ∈ ℝ ∧ 0 < 2 ) ) → ( ( ⌊ ‘ 𝑥 ) ≤ 𝑥 ↔ ( ( ⌊ ‘ 𝑥 ) · 2 ) ≤ ( 𝑥 · 2 ) ) )
188 179 146 186 187 syl3anc ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) ≤ 𝑥 ↔ ( ( ⌊ ‘ 𝑥 ) · 2 ) ≤ ( 𝑥 · 2 ) ) )
189 183 188 mpbid ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) · 2 ) ≤ ( 𝑥 · 2 ) )
190 181 163 83 189 leadd2dd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( ( ⌊ ‘ 𝑥 ) · 2 ) ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 𝑥 · 2 ) ) )
191 177 190 eqbrtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 𝑥 · 2 ) ) )
192 161 164 23 191 lediv1dd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 𝑥 · 2 ) ) / 𝑥 ) )
193 105 recnd ⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) ∈ ℂ )
194 6 56 193 61 fsumdivc ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) )
195 83 recnd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ∈ ℂ )
196 56 86 mulcld ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 · 2 ) ∈ ℂ )
197 divdir ⊢ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) ∈ ℂ ∧ ( 𝑥 · 2 ) ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 𝑥 · 2 ) ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + ( ( 𝑥 · 2 ) / 𝑥 ) ) )
198 195 196 55 197 syl3anc ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 𝑥 · 2 ) ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + ( ( 𝑥 · 2 ) / 𝑥 ) ) )
199 86 56 61 divcan3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( 𝑥 · 2 ) / 𝑥 ) = 2 )
200 199 oveq2d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + ( ( 𝑥 · 2 ) / 𝑥 ) ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) )
201 198 200 eqtrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + ( 𝑥 · 2 ) ) / 𝑥 ) = ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) )
202 192 194 201 3brtr3d ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) + 2 ) / 𝑥 ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) )
203 102 107 97 160 202 letrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) )
204 98 102 97 103 203 letrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) )
205 97 leabsd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ≤ ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ) )
206 98 97 100 204 205 letrd ⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ) )
207 206 adantrr ⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ≤ ( abs ‘ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( log ‘ ( 𝑥 / 𝑛 ) ) ↑ 2 ) / 𝑥 ) + 2 ) ) )
208 82 95 97 40 207 o1le ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∈ 𝑂(1) )
209 1 selberglem1 ⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)
210 o1add ⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
211 208 209 210 sylancl ⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · ( ( Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( log ‘ 𝑚 ) ↑ 2 ) / 𝑥 ) − 𝑇 ) ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( μ ‘ 𝑛 ) · 𝑇 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
212 81 211 eqeltrrd ⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
213 212 mptru ⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) Σ 𝑚 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝑛 ) ) ) ( ( μ ‘ 𝑛 ) · ( ( log ‘ 𝑚 ) ↑ 2 ) ) / 𝑥 ) − ( 2 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1)