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)