Theorem pntrlog2bndlem3

Description: Lemma for pntrlog2bnd . Bound on the difference between the Selberg function and its approximation, inside a sum. (Contributed by Mario Carneiro, 31-May-2016)

	Ref	Expression
Hypotheses	pntsval.1	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
	pntrlog2bnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntrlog2bndlem3.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
	pntrlog2bndlem3.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝐴 )
Assertion	pntrlog2bndlem3	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2		pntrlog2bnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
3		pntrlog2bndlem3.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
4		pntrlog2bndlem3.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝐴 )
5		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
6	3	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
7	6	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ )
8		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
9		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
10	9	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
11	10	nnred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
12		elioore	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
13	12	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
14		1rp	⊢ 1 ∈ ℝ+
15	14	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
16		1red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
17		eliooord	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
18	17	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
19	18	simpld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
20	16 13 19	ltled	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
21	13 15 20	rpgecld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
22	21	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
23	10	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
24	14	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ+ )
25	23 24	rpaddcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ∈ ℝ+ )
26	22 25	rpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ+ )
27	2	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
28	27	ffvelrni	⊢ ( ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
29	26 28	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
30	29	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℂ )
31	22 23	rpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
32	27	ffvelrni	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
33	31 32	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
34	33	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
35	30 34	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
36	35	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
37	11 36	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℝ )
38	8 37	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℝ )
39	13 19	rplogcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
40	21 39	rpmulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
41	38 40	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
42		ioossre	⊢ ( 1 (,) +∞ ) ⊆ ℝ
43	3	rpcnd	⊢ ( 𝜑 → 𝐴 ∈ ℂ )
44		o1const	⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 𝐴 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) )
45	42 43 44	sylancr	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 𝐴 ) ∈ 𝑂(1) )
46		chpo1ubb	⊢ ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( ψ ‘ 𝑦 ) ≤ ( 𝑐 · 𝑦 )
47		simpl	⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℝ+ ( ψ ‘ 𝑦 ) ≤ ( 𝑐 · 𝑦 ) ) → 𝑐 ∈ ℝ+ )
48		simpr	⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℝ+ ( ψ ‘ 𝑦 ) ≤ ( 𝑐 · 𝑦 ) ) → ∀ 𝑦 ∈ ℝ+ ( ψ ‘ 𝑦 ) ≤ ( 𝑐 · 𝑦 ) )
49	1 2 47 48	pntrlog2bndlem2	⊢ ( ( 𝑐 ∈ ℝ+ ∧ ∀ 𝑦 ∈ ℝ+ ( ψ ‘ 𝑦 ) ≤ ( 𝑐 · 𝑦 ) ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
50	49	rexlimiva	⊢ ( ∃ 𝑐 ∈ ℝ+ ∀ 𝑦 ∈ ℝ+ ( ψ ‘ 𝑦 ) ≤ ( 𝑐 · 𝑦 ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
51	46 50	mp1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
52	7 41 45 51	o1mul2	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
53	7 41	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
54	34	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
55	30	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
56	54 55	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ∈ ℝ )
57	1	pntsf	⊢ 𝑆 : ℝ ⟶ ℝ
58	57	ffvelrni	⊢ ( 𝑛 ∈ ℝ → ( 𝑆 ‘ 𝑛 ) ∈ ℝ )
59	11 58	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ 𝑛 ) ∈ ℝ )
60		2re	⊢ 2 ∈ ℝ
61	60	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℝ )
62	23	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
63	11 62	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( log ‘ 𝑛 ) ) ∈ ℝ )
64	61 63	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
65	59 64	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
66	56 65	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
67	8 66	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
68	67 40	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
69	68	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
70	69	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
71	53	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ℂ )
72	71	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) ∈ ℝ )
73	67	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℂ )
74	73	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ∈ ℝ )
75	7 38	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ ℝ )
76	66	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℂ )
77	76	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ∈ ℝ )
78	8 77	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ∈ ℝ )
79	8 76	fsumabs	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) )
80	7	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℝ )
81	80 37	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) ∈ ℝ )
82	56	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ∈ ℂ )
83	82	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ) ∈ ℝ )
84	65	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ )
85	84	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ∈ ℝ )
86	80 11	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · 𝑛 ) ∈ ℝ )
87	82	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ) )
88	84	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) )
89	34 30	abs2difabsd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) − ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
90	34 30	abssubd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) − ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) )
91	89 90	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ) ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) )
92	59	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑆 ‘ 𝑛 ) ∈ ℂ )
93	11	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
94	10	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
95	92 93 94	divcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
96		2cnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 2 ∈ ℂ )
97	62	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℂ )
98	96 97	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 2 · ( log ‘ 𝑛 ) ) ∈ ℂ )
99	95 98	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
100	99 93	absmuld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) · 𝑛 ) ) = ( ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) · ( abs ‘ 𝑛 ) ) )
101	95 98 93	subdird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) · 𝑛 ) = ( ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) · 𝑛 ) − ( ( 2 · ( log ‘ 𝑛 ) ) · 𝑛 ) ) )
102	92 93 94	divcan1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) · 𝑛 ) = ( 𝑆 ‘ 𝑛 ) )
103	96 93 97	mul32d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑛 ) · ( log ‘ 𝑛 ) ) = ( ( 2 · ( log ‘ 𝑛 ) ) · 𝑛 ) )
104	96 93 97	mulassd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · 𝑛 ) · ( log ‘ 𝑛 ) ) = ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) )
105	103 104	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 2 · ( log ‘ 𝑛 ) ) · 𝑛 ) = ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) )
106	102 105	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) · 𝑛 ) − ( ( 2 · ( log ‘ 𝑛 ) ) · 𝑛 ) ) = ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) )
107	101 106	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) · 𝑛 ) = ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) )
108	107	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) · 𝑛 ) ) = ( abs ‘ ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) )
109	23	rpge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ 𝑛 )
110	11 109	absidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ 𝑛 ) = 𝑛 )
111	110	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) · ( abs ‘ 𝑛 ) ) = ( ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) · 𝑛 ) )
112	100 108 111	3eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) = ( ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) · 𝑛 ) )
113	99	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
114		fveq2	⊢ ( 𝑦 = 𝑛 → ( 𝑆 ‘ 𝑦 ) = ( 𝑆 ‘ 𝑛 ) )
115		id	⊢ ( 𝑦 = 𝑛 → 𝑦 = 𝑛 )
116	114 115	oveq12d	⊢ ( 𝑦 = 𝑛 → ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) = ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) )
117		fveq2	⊢ ( 𝑦 = 𝑛 → ( log ‘ 𝑦 ) = ( log ‘ 𝑛 ) )
118	117	oveq2d	⊢ ( 𝑦 = 𝑛 → ( 2 · ( log ‘ 𝑦 ) ) = ( 2 · ( log ‘ 𝑛 ) ) )
119	116 118	oveq12d	⊢ ( 𝑦 = 𝑛 → ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) = ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) )
120	119	fveq2d	⊢ ( 𝑦 = 𝑛 → ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) = ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) )
121	120	breq1d	⊢ ( 𝑦 = 𝑛 → ( ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝐴 ↔ ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) ≤ 𝐴 ) )
122	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ( 1 [,) +∞ ) ( abs ‘ ( ( ( 𝑆 ‘ 𝑦 ) / 𝑦 ) − ( 2 · ( log ‘ 𝑦 ) ) ) ) ≤ 𝐴 )
123	10	nnge1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ≤ 𝑛 )
124		1re	⊢ 1 ∈ ℝ
125		elicopnf	⊢ ( 1 ∈ ℝ → ( 𝑛 ∈ ( 1 [,) +∞ ) ↔ ( 𝑛 ∈ ℝ ∧ 1 ≤ 𝑛 ) ) )
126	124 125	ax-mp	⊢ ( 𝑛 ∈ ( 1 [,) +∞ ) ↔ ( 𝑛 ∈ ℝ ∧ 1 ≤ 𝑛 ) )
127	11 123 126	sylanbrc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ( 1 [,) +∞ ) )
128	121 122 127	rspcdva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) ≤ 𝐴 )
129	113 80 11 109 128	lemul1ad	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( ( 𝑆 ‘ 𝑛 ) / 𝑛 ) − ( 2 · ( log ‘ 𝑛 ) ) ) ) · 𝑛 ) ≤ ( 𝐴 · 𝑛 ) )
130	112 129	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ≤ ( 𝐴 · 𝑛 ) )
131	83 36 85 86 87 88 91 130	lemul12ad	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ) · ( abs ‘ ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ≤ ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( 𝐴 · 𝑛 ) ) )
132	82 84	absmuld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) = ( ( abs ‘ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ) · ( abs ‘ ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) )
133	43	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℂ )
134	36	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℂ )
135	133 93 134	mulassd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 · 𝑛 ) · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( 𝐴 · ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
136	133 93	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · 𝑛 ) ∈ ℂ )
137	136 134	mulcomd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 · 𝑛 ) · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) = ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( 𝐴 · 𝑛 ) ) )
138	135 137	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = ( ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) · ( 𝐴 · 𝑛 ) ) )
139	131 132 138	3brtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ≤ ( 𝐴 · ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
140	8 77 81 139	fsumle	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐴 · ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
141	43	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℂ )
142	37	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ )
143	8 141 142	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝐴 · ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
144	140 143	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( abs ‘ ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ≤ ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
145	74 78 75 79 144	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) ≤ ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) )
146	74 75 40 145	lediv1dd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ ( ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
147	40	rpcnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ )
148	40	rpne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ≠ 0 )
149	73 147 148	absdivd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
150	40	rpred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ )
151	40	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 𝑥 · ( log ‘ 𝑥 ) ) )
152	150 151	absidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( 𝑥 · ( log ‘ 𝑥 ) ) )
153	152	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( abs ‘ ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
154	149 153	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
155	38	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℂ )
156	141 155 147 148	divassd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
157	146 154 156	3brtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ≤ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
158	53	leabsd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) )
159	70 53 72 157 158	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) )
160	159	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( 𝐴 · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) )
161	5 52 53 69 160	o1le	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) − ( abs ‘ ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) · ( ( 𝑆 ‘ 𝑛 ) − ( 2 · ( 𝑛 · ( log ‘ 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )