Theorem pntrlog2bndlem6

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	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
	pntrlog2bnd.t	⊢ 𝑇 = ( 𝑎 ∈ ℝ ↦ if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) )
	pntrlog2bndlem5.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
	pntrlog2bndlem5.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 )
	pntrlog2bndlem6.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
	pntrlog2bndlem6.2	⊢ ( 𝜑 → 1 ≤ 𝐴 )
Assertion	pntrlog2bndlem6	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2		pntrlog2bnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
3		pntrlog2bnd.t	⊢ 𝑇 = ( 𝑎 ∈ ℝ ↦ if ( 𝑎 ∈ ℝ+ , ( 𝑎 · ( log ‘ 𝑎 ) ) , 0 ) )
4		pntrlog2bndlem5.1	⊢ ( 𝜑 → 𝐵 ∈ ℝ+ )
5		pntrlog2bndlem5.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 )
6		pntrlog2bndlem6.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
7		pntrlog2bndlem6.2	⊢ ( 𝜑 → 1 ≤ 𝐴 )
8		elioore	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
9	8	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
10		1rp	⊢ 1 ∈ ℝ+
11	10	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
12		1red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
13		eliooord	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
14	13	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
15	14	simpld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
16	12 9 15	ltled	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
17	9 11 16	rpgecld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
18	2	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
19	18	ffvelrni	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
20	17 19	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℝ )
21	20	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑅 ‘ 𝑥 ) ∈ ℂ )
22	21	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) ∈ ℝ )
23	17	relogcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
24	22 23	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) ∈ ℝ )
25		2re	⊢ 2 ∈ ℝ
26	25	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ )
27	9 15	rplogcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
28	26 27	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℝ )
29		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
30	17	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
31		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
32	31	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
33	32	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
34	30 33	rpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
35	18	ffvelrni	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
36	34 35	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
37	36	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
38	37	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
39	33	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
40	38 39	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
41	29 40	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
42	28 41	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
43	24 42	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℝ )
44	43	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) ∈ ℂ )
45		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
46		ssun2	⊢ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) )
47	1 2 3 4 5 6 7	pntrlog2bndlem6a	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) )
48	46 47	sseqtrrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
49	48	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
50	49 40	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
51	45 50	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
52	28 51	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℝ )
53	52	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
54	9	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
55	17	rpne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
56	44 53 54 55	divdird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) = ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ) )
57	24	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) ∈ ℂ )
58	42	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ∈ ℂ )
59	57 58 53	subsubd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
60	28	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 / ( log ‘ 𝑥 ) ) ∈ ℂ )
61	41	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
62	51	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
63	60 61 62	subdid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
64		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∈ Fin )
65		ssun1	⊢ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ⊆ ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∪ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) )
66	65 47	sseqtrrid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ⊆ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
67	66	sselda	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ) → 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
68	67 40	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
69	64 68	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℝ )
70	69	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
71	10	a1i	⊢ ( 𝜑 → 1 ∈ ℝ+ )
72	6 71 7	rpgecld	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
73	72	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ+ )
74	9 73	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 𝐴 ) ∈ ℝ )
75		reflcl	⊢ ( ( 𝑥 / 𝐴 ) ∈ ℝ → ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ∈ ℝ )
76	74 75	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ∈ ℝ )
77	76	ltp1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) < ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) )
78		fzdisj	⊢ ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) < ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) → ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) = ∅ )
79	77 78	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ∩ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) = ∅ )
80	40	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
81	79 47 29 80	fsumsplit	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
82	70 62 81	mvrraddd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) )
83	82	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) − Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
84	63 83	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) )
85	84	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
86	59 85	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) = ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) )
87	86	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) + ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) )
88	56 87	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ) = ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) )
89	88	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) )
90	43 17	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ∈ ℝ )
91	52 17	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ∈ ℝ )
92	1 2 3 4 5	pntrlog2bndlem5	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )
93		ioossre	⊢ ( 1 (,) +∞ ) ⊆ ℝ
94	93	a1i	⊢ ( 𝜑 → ( 1 (,) +∞ ) ⊆ ℝ )
95		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
96	25	a1i	⊢ ( 𝜑 → 2 ∈ ℝ )
97	4	rpred	⊢ ( 𝜑 → 𝐵 ∈ ℝ )
98	72	relogcld	⊢ ( 𝜑 → ( log ‘ 𝐴 ) ∈ ℝ )
99	98 95	readdcld	⊢ ( 𝜑 → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℝ )
100	97 99	remulcld	⊢ ( 𝜑 → ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ∈ ℝ )
101	96 100	remulcld	⊢ ( 𝜑 → ( 2 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ∈ ℝ )
102	51 27	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
103	97	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐵 ∈ ℝ )
104	73	relogcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝐴 ) ∈ ℝ )
105	104 12	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℝ )
106	103 105	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ∈ ℝ )
107	9 106	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ∈ ℝ )
108		2rp	⊢ 2 ∈ ℝ+
109	108	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ+ )
110	109	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 2 )
111	103 9	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐵 · 𝑥 ) ∈ ℝ )
112	49 31	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
113	112	nnrecred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
114	45 113	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ∈ ℝ )
115	111 114	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐵 · 𝑥 ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) ∈ ℝ )
116	27	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
117	50 116	rerpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ∈ ℝ )
118	103	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐵 ∈ ℝ )
119	9	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
120	118 119	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐵 · 𝑥 ) ∈ ℝ )
121	120 113	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐵 · 𝑥 ) · ( 1 / 𝑛 ) ) ∈ ℝ )
122	49 38	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℝ )
123	119 112	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
124	118 123	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐵 · ( 𝑥 / 𝑛 ) ) ∈ ℝ )
125	49 33	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
126	125	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ∈ ℝ )
127	17	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
128	127	relogcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
129	49 37	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
130	129	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) )
131		elfzle2	⊢ ( 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ≤ ( ⌊ ‘ 𝑥 ) )
132	131	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≤ ( ⌊ ‘ 𝑥 ) )
133	112	nnzd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℤ )
134		flge	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ℤ ) → ( 𝑛 ≤ 𝑥 ↔ 𝑛 ≤ ( ⌊ ‘ 𝑥 ) ) )
135	119 133 134	syl2anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ≤ 𝑥 ↔ 𝑛 ≤ ( ⌊ ‘ 𝑥 ) ) )
136	132 135	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≤ 𝑥 )
137	125 127	logled	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 ≤ 𝑥 ↔ ( log ‘ 𝑛 ) ≤ ( log ‘ 𝑥 ) ) )
138	136 137	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( log ‘ 𝑛 ) ≤ ( log ‘ 𝑥 ) )
139	126 128 122 130 138	lemul2ad	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ≤ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) )
140	50 122 116	ledivmul2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ≤ ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ↔ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ≤ ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑥 ) ) ) )
141	139 140	mpbird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ≤ ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) )
142	123	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℂ )
143	49 34	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
144	143	rpne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ≠ 0 )
145	129 142 144	absdivd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( abs ‘ ( 𝑥 / 𝑛 ) ) ) )
146	17	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 𝑥 )
147	146	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ 𝑥 )
148	119 125 147	divge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( 𝑥 / 𝑛 ) )
149	123 148	absidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑥 / 𝑛 ) ) = ( 𝑥 / 𝑛 ) )
150	149	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( abs ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( 𝑥 / 𝑛 ) ) )
151	145 150	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) = ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( 𝑥 / 𝑛 ) ) )
152		fveq2	⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( 𝑅 ‘ 𝑦 ) = ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) )
153		id	⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → 𝑦 = ( 𝑥 / 𝑛 ) )
154	152 153	oveq12d	⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) = ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) )
155	154	fveq2d	⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) = ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) )
156	155	breq1d	⊢ ( 𝑦 = ( 𝑥 / 𝑛 ) → ( ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 ↔ ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) ≤ 𝐵 ) )
157	5	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ℝ+ ( abs ‘ ( ( 𝑅 ‘ 𝑦 ) / 𝑦 ) ) ≤ 𝐵 )
158	156 157 143	rspcdva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) / ( 𝑥 / 𝑛 ) ) ) ≤ 𝐵 )
159	151 158	eqbrtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( 𝑥 / 𝑛 ) ) ≤ 𝐵 )
160	122 118 143	ledivmul2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) / ( 𝑥 / 𝑛 ) ) ≤ 𝐵 ↔ ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ≤ ( 𝐵 · ( 𝑥 / 𝑛 ) ) ) )
161	159 160	mpbid	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ≤ ( 𝐵 · ( 𝑥 / 𝑛 ) ) )
162	117 122 124 141 161	letrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ≤ ( 𝐵 · ( 𝑥 / 𝑛 ) ) )
163	118	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐵 ∈ ℂ )
164	54	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
165	112	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
166	112	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
167	163 164 165 166	divassd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐵 · 𝑥 ) / 𝑛 ) = ( 𝐵 · ( 𝑥 / 𝑛 ) ) )
168	163 164	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐵 · 𝑥 ) ∈ ℂ )
169	168 165 166	divrecd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐵 · 𝑥 ) / 𝑛 ) = ( ( 𝐵 · 𝑥 ) · ( 1 / 𝑛 ) ) )
170	167 169	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐵 · ( 𝑥 / 𝑛 ) ) = ( ( 𝐵 · 𝑥 ) · ( 1 / 𝑛 ) ) )
171	162 170	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ≤ ( ( 𝐵 · 𝑥 ) · ( 1 / 𝑛 ) ) )
172	45 117 121 171	fsumle	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ≤ Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐵 · 𝑥 ) · ( 1 / 𝑛 ) ) )
173	23	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
174	49 80	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ∈ ℂ )
175	27	rpne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
176	45 173 174 175	fsumdivc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) )
177	103	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐵 ∈ ℂ )
178	177 54	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐵 · 𝑥 ) ∈ ℂ )
179	113	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
180	45 178 179	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐵 · 𝑥 ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝐵 · 𝑥 ) · ( 1 / 𝑛 ) ) )
181	172 176 180	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ≤ ( ( 𝐵 · 𝑥 ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) )
182	4	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐵 ∈ ℝ+ )
183	182	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 𝐵 )
184	103 9 183 146	mulge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 𝐵 · 𝑥 ) )
185	32	nnrecred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
186	29 185	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ∈ ℝ )
187	23 104	resubcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) − ( log ‘ 𝐴 ) ) ∈ ℝ )
188	23 12	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℝ )
189	67 185	syldan	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
190	64 189	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) ∈ ℝ )
191		harmonicubnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
192	9 16 191	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
193	17 73	relogdivd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ ( 𝑥 / 𝐴 ) ) = ( ( log ‘ 𝑥 ) − ( log ‘ 𝐴 ) ) )
194	17 73	rpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 𝐴 ) ∈ ℝ+ )
195		harmoniclbnd	⊢ ( ( 𝑥 / 𝐴 ) ∈ ℝ+ → ( log ‘ ( 𝑥 / 𝐴 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) )
196	194 195	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ ( 𝑥 / 𝐴 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) )
197	193 196	eqbrtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) − ( log ‘ 𝐴 ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) )
198	186 187 188 190 192 197	le2subd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) ) ≤ ( ( ( log ‘ 𝑥 ) + 1 ) − ( ( log ‘ 𝑥 ) − ( log ‘ 𝐴 ) ) ) )
199	67 31	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ) → 𝑛 ∈ ℕ )
200	199	nnrecred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
201	64 200	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) ∈ ℝ )
202	201	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) ∈ ℂ )
203	114	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ∈ ℂ )
204	32	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
205	32	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
206	204 205	reccld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
207	79 47 29 206	fsumsplit	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) + Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) )
208	202 203 207	mvrladdd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( 1 / 𝑛 ) ) = Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) )
209		1cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℂ )
210	104	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝐴 ) ∈ ℂ )
211	173 209 210	pnncand	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) + 1 ) − ( ( log ‘ 𝑥 ) − ( log ‘ 𝐴 ) ) ) = ( 1 + ( log ‘ 𝐴 ) ) )
212	209 210 211	comraddd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) + 1 ) − ( ( log ‘ 𝑥 ) − ( log ‘ 𝐴 ) ) ) = ( ( log ‘ 𝐴 ) + 1 ) )
213	198 208 212	3brtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝐴 ) + 1 ) )
214	114 105 111 184 213	lemul2ad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐵 · 𝑥 ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) ≤ ( ( 𝐵 · 𝑥 ) · ( ( log ‘ 𝐴 ) + 1 ) ) )
215	105	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℂ )
216	177 54 215	mulassd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐵 · 𝑥 ) · ( ( log ‘ 𝐴 ) + 1 ) ) = ( 𝐵 · ( 𝑥 · ( ( log ‘ 𝐴 ) + 1 ) ) ) )
217	177 54 215	mul12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐵 · ( 𝑥 · ( ( log ‘ 𝐴 ) + 1 ) ) ) = ( 𝑥 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) )
218	216 217	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐵 · 𝑥 ) · ( ( log ‘ 𝐴 ) + 1 ) ) = ( 𝑥 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) )
219	214 218	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐵 · 𝑥 ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) ≤ ( 𝑥 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) )
220	102 115 107 181 219	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ≤ ( 𝑥 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) )
221	102 107 26 110 220	lemul2ad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) ≤ ( 2 · ( 𝑥 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ) )
222		2cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℂ )
223	222 173 62 175	div32d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) = ( 2 · ( Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) / ( log ‘ 𝑥 ) ) ) )
224	210 209	addcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝐴 ) + 1 ) ∈ ℂ )
225	177 224	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ∈ ℂ )
226	54 222 225	mul12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( 2 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ) = ( 2 · ( 𝑥 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ) )
227	221 223 226	3brtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ≤ ( 𝑥 · ( 2 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ) )
228	101	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 2 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ∈ ℝ )
229	52 228 17	ledivmuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ≤ ( 2 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ↔ ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ≤ ( 𝑥 · ( 2 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) ) ) )
230	227 229	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ≤ ( 2 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) )
231	230	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ≤ ( 2 · ( 𝐵 · ( ( log ‘ 𝐴 ) + 1 ) ) ) )
232	94 91 95 101 231	ello1d	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )
233	90 91 92 232	lo1add	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) + ( ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( ( ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) + 1 ) ... ( ⌊ ‘ 𝑥 ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) / 𝑥 ) ) ) ∈ ≤𝑂(1) )
234	89 233	eqeltrrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ( abs ‘ ( 𝑅 ‘ 𝑥 ) ) · ( log ‘ 𝑥 ) ) − ( ( 2 / ( log ‘ 𝑥 ) ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ ( 𝑥 / 𝐴 ) ) ) ( ( abs ‘ ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) · ( log ‘ 𝑛 ) ) ) ) / 𝑥 ) ) ∈ ≤𝑂(1) )