Theorem pntrlog2bndlem2

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

Proof

Step	Hyp	Ref	Expression
1		pntsval.1	⊢ 𝑆 = ( 𝑎 ∈ ℝ ↦ Σ 𝑖 ∈ ( 1 ... ( ⌊ ‘ 𝑎 ) ) ( ( Λ ‘ 𝑖 ) · ( ( log ‘ 𝑖 ) + ( ψ ‘ ( 𝑎 / 𝑖 ) ) ) ) )
2		pntrlog2bnd.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
3		pntrlog2bndlem2.1	⊢ ( 𝜑 → 𝐴 ∈ ℝ+ )
4		pntrlog2bndlem2.2	⊢ ( 𝜑 → ∀ 𝑦 ∈ ℝ+ ( ψ ‘ 𝑦 ) ≤ ( 𝐴 · 𝑦 ) )
5		1red	⊢ ( 𝜑 → 1 ∈ ℝ )
6		elioore	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ )
7	6	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ )
8		chpcl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
9	7 8	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
10	9	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ψ ‘ 𝑥 ) ∈ ℂ )
11		fzfid	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
12	7	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ )
13		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
14	13	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
15	14	peano2nnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
16	12 15	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ )
17		chpcl	⊢ ( ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ → ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
18	16 17	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
19	18 16	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
20	11 19	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
21	20	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℂ )
22	7	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℂ )
23		eliooord	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
24	23	adantl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 < 𝑥 ∧ 𝑥 < +∞ ) )
25	24	simpld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 𝑥 )
26	7 25	rplogcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ+ )
27	26	rpcnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℂ )
28	22 27	mulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℂ )
29		1rp	⊢ 1 ∈ ℝ+
30	29	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ+ )
31		1red	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℝ )
32	31 7 25	ltled	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ≤ 𝑥 )
33	7 30 32	rpgecld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ∈ ℝ+ )
34	33	rpne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 ≠ 0 )
35	26	rpne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ≠ 0 )
36	22 27 34 35	mulne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ≠ 0 )
37	10 21 28 36	divdird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( ( ψ ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
38	37	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) )
39	33 26	rpmulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 · ( log ‘ 𝑥 ) ) ∈ ℝ+ )
40	9 39	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
41	20 39	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
42	10 22 27 34 35	divdiv1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( ( ψ ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
43	9 33	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
44	43	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℂ )
45	44 27 35	divrecd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( 1 / ( log ‘ 𝑥 ) ) ) )
46	42 45	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) = ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( 1 / ( log ‘ 𝑥 ) ) ) )
47	46	mpteq2dva	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) )
48	26	rprecred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 / ( log ‘ 𝑥 ) ) ∈ ℝ )
49	33	ex	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) → 𝑥 ∈ ℝ+ ) )
50	49	ssrdv	⊢ ( 𝜑 → ( 1 (,) +∞ ) ⊆ ℝ+ )
51		chpo1ub	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)
52	51	a1i	⊢ ( 𝜑 → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
53	50 52	o1res2	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) )
54		divlogrlim	⊢ ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0
55		rlimo1	⊢ ( ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ⇝𝑟 0 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
56	54 55	mp1i	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 / ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
57	43 48 53 56	o1mul2	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) · ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
58	47 57	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ψ ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
59	3	rpred	⊢ ( 𝜑 → 𝐴 ∈ ℝ )
60	59 5	readdcld	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℝ )
61	60	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 + 1 ) ∈ ℝ )
62	31 48	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ∈ ℝ )
63		ioossre	⊢ ( 1 (,) +∞ ) ⊆ ℝ
64	60	recnd	⊢ ( 𝜑 → ( 𝐴 + 1 ) ∈ ℂ )
65		o1const	⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ ( 𝐴 + 1 ) ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 𝐴 + 1 ) ) ∈ 𝑂(1) )
66	63 64 65	sylancr	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 𝐴 + 1 ) ) ∈ 𝑂(1) )
67		1cnd	⊢ ( 𝜑 → 1 ∈ ℂ )
68		o1const	⊢ ( ( ( 1 (,) +∞ ) ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) )
69	63 67 68	sylancr	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ 1 ) ∈ 𝑂(1) )
70	31 48 69 56	o1add2	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
71	61 62 66 70	o1mul2	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
72	61 62	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
73	41	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
74		chpge0	⊢ ( ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ → 0 ≤ ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) )
75	16 74	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) )
76	14	nnrpd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
77	29	a1i	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ+ )
78	76 77	rpaddcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ∈ ℝ+ )
79	33	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℝ+ )
80	79	rpge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ 𝑥 )
81	12 78 80	divge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( 𝑥 / ( 𝑛 + 1 ) ) )
82	18 16 75 81	addge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
83	11 19 82	fsumge0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
84	20 39 83	divge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
85	41 84	absidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
86	72	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ∈ ℂ )
87	86	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ) ∈ ℝ )
88	20 33	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / 𝑥 ) ∈ ℝ )
89	33	relogcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( log ‘ 𝑥 ) ∈ ℝ )
90	89 31	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℝ )
91	61 90	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) ∈ ℝ )
92	61 7	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 + 1 ) · 𝑥 ) ∈ ℝ )
93	14	nnrecred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
94	11 93	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ∈ ℝ )
95	92 94	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) ∈ ℝ )
96	92 90	remulcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( ( log ‘ 𝑥 ) + 1 ) ) ∈ ℝ )
97	59	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℝ )
98		1red	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℝ )
99	97 98	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 + 1 ) ∈ ℝ )
100	99 12	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 + 1 ) · 𝑥 ) ∈ ℝ )
101	100 93	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( 1 / 𝑛 ) ) ∈ ℝ )
102	100 15	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) / ( 𝑛 + 1 ) ) ∈ ℝ )
103	100 14	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) / 𝑛 ) ∈ ℝ )
104	97 16	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
105		fveq2	⊢ ( 𝑦 = ( 𝑥 / ( 𝑛 + 1 ) ) → ( ψ ‘ 𝑦 ) = ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) )
106		oveq2	⊢ ( 𝑦 = ( 𝑥 / ( 𝑛 + 1 ) ) → ( 𝐴 · 𝑦 ) = ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) )
107	105 106	breq12d	⊢ ( 𝑦 = ( 𝑥 / ( 𝑛 + 1 ) ) → ( ( ψ ‘ 𝑦 ) ≤ ( 𝐴 · 𝑦 ) ↔ ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
108	4	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ∀ 𝑦 ∈ ℝ+ ( ψ ‘ 𝑦 ) ≤ ( 𝐴 · 𝑦 ) )
109	79 78	rpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ+ )
110	107 108 109	rspcdva	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) )
111	18 104 16 110	leadd1dd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
112	64	ad2antrr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝐴 + 1 ) ∈ ℂ )
113	22	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑥 ∈ ℂ )
114	14	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
115		1cnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
116	114 115	addcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ∈ ℂ )
117	15	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ≠ 0 )
118	112 113 116 117	divassd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) / ( 𝑛 + 1 ) ) = ( ( 𝐴 + 1 ) · ( 𝑥 / ( 𝑛 + 1 ) ) ) )
119	97	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝐴 ∈ ℂ )
120	113 116 117	divcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℂ )
121	119 115 120	adddird	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 + 1 ) · ( 𝑥 / ( 𝑛 + 1 ) ) ) = ( ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 1 · ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
122	120	mullidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · ( 𝑥 / ( 𝑛 + 1 ) ) ) = ( 𝑥 / ( 𝑛 + 1 ) ) )
123	122	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 1 · ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = ( ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
124	118 121 123	3eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) / ( 𝑛 + 1 ) ) = ( ( 𝐴 · ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
125	111 124	breqtrrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐴 + 1 ) · 𝑥 ) / ( 𝑛 + 1 ) ) )
126	59	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ )
127	3	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝐴 ∈ ℝ+ )
128	127	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 𝐴 )
129	30	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 1 )
130	126 31 128 129	addge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( 𝐴 + 1 ) )
131	33	rpge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ 𝑥 )
132	61 7 130 131	mulge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( ( 𝐴 + 1 ) · 𝑥 ) )
133	132	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( ( 𝐴 + 1 ) · 𝑥 ) )
134	14	nnred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
135	134	lep1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≤ ( 𝑛 + 1 ) )
136	76 78 100 133 135	lediv2ad	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) / ( 𝑛 + 1 ) ) ≤ ( ( ( 𝐴 + 1 ) · 𝑥 ) / 𝑛 ) )
137	19 102 103 125 136	letrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐴 + 1 ) · 𝑥 ) / 𝑛 ) )
138	100	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝐴 + 1 ) · 𝑥 ) ∈ ℂ )
139	14	nnne0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
140	138 114 139	divrecd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) / 𝑛 ) = ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( 1 / 𝑛 ) ) )
141	137 140	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( 1 / 𝑛 ) ) )
142	11 19 101 141	fsumle	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( 1 / 𝑛 ) ) )
143	92	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 + 1 ) · 𝑥 ) ∈ ℂ )
144	114 139	reccld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
145	11 143 144	fsummulc2	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( 1 / 𝑛 ) ) )
146	142 145	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐴 + 1 ) · 𝑥 ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) )
147		harmonicubnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
148	7 32 147	syl2anc	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
149	94 90 92 132 148	lemul2ad	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) · Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) ≤ ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( ( log ‘ 𝑥 ) + 1 ) ) )
150	20 95 96 146 149	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( ( log ‘ 𝑥 ) + 1 ) ) )
151	64	adantr	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝐴 + 1 ) ∈ ℂ )
152	90	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℂ )
153	151 22 152	mul32d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝐴 + 1 ) · 𝑥 ) · ( ( log ‘ 𝑥 ) + 1 ) ) = ( ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) · 𝑥 ) )
154	150 153	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) · 𝑥 ) )
155	20 91 33	ledivmul2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / 𝑥 ) ≤ ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) ↔ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) · 𝑥 ) ) )
156	154 155	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / 𝑥 ) ≤ ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) )
157	88 91 26 156	lediv1dd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) ≤ ( ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) / ( log ‘ 𝑥 ) ) )
158	21 22 27 34 35	divdiv1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / 𝑥 ) / ( log ‘ 𝑥 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
159		1cnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 ∈ ℂ )
160	27 159	addcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) + 1 ) ∈ ℂ )
161	151 160 27 35	divassd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) / ( log ‘ 𝑥 ) ) = ( ( 𝐴 + 1 ) · ( ( ( log ‘ 𝑥 ) + 1 ) / ( log ‘ 𝑥 ) ) ) )
162	27 159 27 35	divdird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) + 1 ) / ( log ‘ 𝑥 ) ) = ( ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) + ( 1 / ( log ‘ 𝑥 ) ) ) )
163	27 35	dividd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) = 1 )
164	163	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( log ‘ 𝑥 ) / ( log ‘ 𝑥 ) ) + ( 1 / ( log ‘ 𝑥 ) ) ) = ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) )
165	162 164	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) = ( ( ( log ‘ 𝑥 ) + 1 ) / ( log ‘ 𝑥 ) ) )
166	165	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) = ( ( 𝐴 + 1 ) · ( ( ( log ‘ 𝑥 ) + 1 ) / ( log ‘ 𝑥 ) ) ) )
167	161 166	eqtr4d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( 𝐴 + 1 ) · ( ( log ‘ 𝑥 ) + 1 ) ) / ( log ‘ 𝑥 ) ) = ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) )
168	157 158 167	3brtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) )
169	72	leabsd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ) )
170	41 72 87 168 169	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ) )
171	85 170	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ) )
172	171	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( ( 𝐴 + 1 ) · ( 1 + ( 1 / ( log ‘ 𝑥 ) ) ) ) ) )
173	5 71 72 73 172	o1le	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
174	40 41 58 173	o1add2	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) + ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ) ∈ 𝑂(1) )
175	38 174	eqeltrd	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
176	9 20	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
177	176 39	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
178	2	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
179	178	ffvelcdmi	⊢ ( ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
180	109 179	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℝ )
181	180	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℂ )
182	79 76	rpdivcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ+ )
183	178	ffvelcdmi	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
184	182 183	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
185	184	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
186	181 185	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
187	186	abscld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ∈ ℝ )
188	134 187	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℝ )
189	11 188	fsumrecl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ∈ ℝ )
190	189 39	rerpdivcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℝ )
191	190	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
192	76	rpge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ 𝑛 )
193	186	absge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) )
194	134 187 192 193	mulge0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 0 ≤ ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
195	11 188 194	fsumge0	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) )
196	189 39 195	divge0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 0 ≤ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
197	190 196	absidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
198	10 21	addcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ∈ ℂ )
199	198 28 36	divcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ∈ ℂ )
200	199	abscld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ ℝ )
201	12 14	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℝ )
202		chpcl	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
203	201 202	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℝ )
204	203 201	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) ∈ ℝ )
205	204 19	resubcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ∈ ℝ )
206	134 205	remulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ∈ ℝ )
207	2	pntrval	⊢ ( ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) = ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑥 / ( 𝑛 + 1 ) ) ) )
208	109 207	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) = ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑥 / ( 𝑛 + 1 ) ) ) )
209	2	pntrval	⊢ ( ( 𝑥 / 𝑛 ) ∈ ℝ+ → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) − ( 𝑥 / 𝑛 ) ) )
210	182 209	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) − ( 𝑥 / 𝑛 ) ) )
211	208 210	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) − ( 𝑥 / 𝑛 ) ) ) )
212	18	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℂ )
213	203	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑛 ) ) ∈ ℂ )
214	113 114 139	divcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / 𝑛 ) ∈ ℂ )
215	212 120 213 214	sub4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) − ( 𝑥 / 𝑛 ) ) ) = ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) − ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) )
216	211 215	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) = ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) − ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) )
217	216	fveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( abs ‘ ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) − ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) ) )
218	212 213	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ∈ ℂ )
219	120 214	subcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ∈ ℂ )
220	218 219	abs2dif2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) − ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) ) ≤ ( ( abs ‘ ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) + ( abs ‘ ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) ) )
221	217 220	eqbrtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ ( ( abs ‘ ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) + ( abs ‘ ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) ) )
222	76 78 12 80 135	lediv2ad	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑥 / ( 𝑛 + 1 ) ) ≤ ( 𝑥 / 𝑛 ) )
223		chpwordi	⊢ ( ( ( 𝑥 / ( 𝑛 + 1 ) ) ∈ ℝ ∧ ( 𝑥 / 𝑛 ) ∈ ℝ ∧ ( 𝑥 / ( 𝑛 + 1 ) ) ≤ ( 𝑥 / 𝑛 ) ) → ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ψ ‘ ( 𝑥 / 𝑛 ) ) )
224	16 201 222 223	syl3anc	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ≤ ( ψ ‘ ( 𝑥 / 𝑛 ) ) )
225	18 203 224	abssuble0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) − ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
226	16 201 222	abssuble0d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) = ( ( 𝑥 / 𝑛 ) − ( 𝑥 / ( 𝑛 + 1 ) ) ) )
227	225 226	oveq12d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) + ( abs ‘ ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) − ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) + ( ( 𝑥 / 𝑛 ) − ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
228	213 214 212 120	addsub4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) − ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) ) + ( ( 𝑥 / 𝑛 ) − ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
229	227 228	eqtr4d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( abs ‘ ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ψ ‘ ( 𝑥 / 𝑛 ) ) ) ) + ( abs ‘ ( ( 𝑥 / ( 𝑛 + 1 ) ) − ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
230	221 229	breqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ≤ ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
231	187 205 134 192 230	lemul2ad	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
232	11 188 206 231	fsumle	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
233	205	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ∈ ℂ )
234	114 233	mulcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ∈ ℂ )
235	11 234	fsumcl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) ∈ ℂ )
236	10 21	negdi2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → - ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = ( - ( ψ ‘ 𝑥 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
237	33	rprege0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
238		flge0nn0	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
239		nn0p1nn	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
240	237 238 239	3syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
241	7 240	nndivred	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ )
242		2re	⊢ 2 ∈ ℝ
243	242	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 2 ∈ ℝ )
244		flltp1	⊢ ( 𝑥 ∈ ℝ → 𝑥 < ( ( ⌊ ‘ 𝑥 ) + 1 ) )
245	7 244	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 < ( ( ⌊ ‘ 𝑥 ) + 1 ) )
246	240	nncnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℂ )
247	246	mulridd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · 1 ) = ( ( ⌊ ‘ 𝑥 ) + 1 ) )
248	245 247	breqtrrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 𝑥 < ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · 1 ) )
249	240	nnrpd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ+ )
250	7 31 249	ltdivmuld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 1 ↔ 𝑥 < ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · 1 ) ) )
251	248 250	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 1 )
252		1lt2	⊢ 1 < 2
253	252	a1i	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → 1 < 2 )
254	241 31 243 251 253	lttrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 2 )
255		chpeq0	⊢ ( ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ → ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = 0 ↔ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 2 ) )
256	241 255	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = 0 ↔ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) < 2 ) )
257	254 256	mpbird	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = 0 )
258	257	oveq1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( 0 + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
259	241	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℂ )
260	259	addlidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 0 + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
261	258 260	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
262	261	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) = ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
263	240	nnne0d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ≠ 0 )
264	22 246 263	divcan2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = 𝑥 )
265	262 264	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) = 𝑥 )
266	22	div1d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 𝑥 / 1 ) = 𝑥 )
267	266	fveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ψ ‘ ( 𝑥 / 1 ) ) = ( ψ ‘ 𝑥 ) )
268	267 266	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) = ( ( ψ ‘ 𝑥 ) + 𝑥 ) )
269	268	oveq2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 · ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) ) = ( 1 · ( ( ψ ‘ 𝑥 ) + 𝑥 ) ) )
270	9 7	readdcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) + 𝑥 ) ∈ ℝ )
271	270	recnd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ψ ‘ 𝑥 ) + 𝑥 ) ∈ ℂ )
272	271	mullidd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 · ( ( ψ ‘ 𝑥 ) + 𝑥 ) ) = ( ( ψ ‘ 𝑥 ) + 𝑥 ) )
273	269 272	eqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 · ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) ) = ( ( ψ ‘ 𝑥 ) + 𝑥 ) )
274	265 273	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) − ( 1 · ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) ) ) = ( 𝑥 − ( ( ψ ‘ 𝑥 ) + 𝑥 ) ) )
275	271 22	negsubdi2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → - ( ( ( ψ ‘ 𝑥 ) + 𝑥 ) − 𝑥 ) = ( 𝑥 − ( ( ψ ‘ 𝑥 ) + 𝑥 ) ) )
276	10 22	pncand	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) + 𝑥 ) − 𝑥 ) = ( ψ ‘ 𝑥 ) )
277	276	negeqd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → - ( ( ( ψ ‘ 𝑥 ) + 𝑥 ) − 𝑥 ) = - ( ψ ‘ 𝑥 ) )
278	274 275 277	3eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) − ( 1 · ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) ) ) = - ( ψ ‘ 𝑥 ) )
279	7	flcld	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
280		fzval3	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℤ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
281	279 280	syl	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
282	281	eqcomd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) = ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
283	114 115	pncan2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 𝑛 ) = 1 )
284	283	oveq1d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) − 𝑛 ) · ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = ( 1 · ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
285	19	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℂ )
286	285	mullidd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 · ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
287	284 286	eqtrd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) − 𝑛 ) · ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
288	282 287	sumeq12rdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( 𝑛 + 1 ) − 𝑛 ) · ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
289	278 288	oveq12d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) − ( 1 · ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) ) ) − Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( 𝑛 + 1 ) − 𝑛 ) · ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = ( - ( ψ ‘ 𝑥 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
290		oveq2	⊢ ( 𝑚 = 𝑛 → ( 𝑥 / 𝑚 ) = ( 𝑥 / 𝑛 ) )
291	290	fveq2d	⊢ ( 𝑚 = 𝑛 → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = ( ψ ‘ ( 𝑥 / 𝑛 ) ) )
292	291 290	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) )
293	292	ancli	⊢ ( 𝑚 = 𝑛 → ( 𝑚 = 𝑛 ∧ ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) = ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) ) )
294		oveq2	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑥 / 𝑚 ) = ( 𝑥 / ( 𝑛 + 1 ) ) )
295	294	fveq2d	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) )
296	295 294	oveq12d	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) = ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) )
297	296	ancli	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 = ( 𝑛 + 1 ) ∧ ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) = ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
298		oveq2	⊢ ( 𝑚 = 1 → ( 𝑥 / 𝑚 ) = ( 𝑥 / 1 ) )
299	298	fveq2d	⊢ ( 𝑚 = 1 → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = ( ψ ‘ ( 𝑥 / 1 ) ) )
300	299 298	oveq12d	⊢ ( 𝑚 = 1 → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) = ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) )
301	300	ancli	⊢ ( 𝑚 = 1 → ( 𝑚 = 1 ∧ ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) = ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) ) )
302		oveq2	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑥 / 𝑚 ) = ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
303	302	fveq2d	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) = ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
304	303 302	oveq12d	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) = ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
305	304	ancli	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) ∧ ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) = ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) )
306		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
307	240 306	eleqtrdi	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
308		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → 𝑚 ∈ ℕ )
309	308	adantl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℕ )
310	309	nncnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℂ )
311	7	adantr	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑥 ∈ ℝ )
312	311 309	nndivred	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑥 / 𝑚 ) ∈ ℝ )
313		chpcl	⊢ ( ( 𝑥 / 𝑚 ) ∈ ℝ → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ )
314	312 313	syl	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ψ ‘ ( 𝑥 / 𝑚 ) ) ∈ ℝ )
315	314 312	readdcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) ∈ ℝ )
316	315	recnd	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑚 ) ) + ( 𝑥 / 𝑚 ) ) ∈ ℂ )
317	293 297 301 305 307 310 316	fsumparts	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) ) ) = ( ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) − ( 1 · ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) ) ) − Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( 𝑛 + 1 ) − 𝑛 ) · ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
318	213 214	addcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) ∈ ℂ )
319	212 120	addcld	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ∈ ℂ )
320	318 319	negsubdi2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → - ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) ) )
321	320	oveq2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · - ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) ) ) )
322	114 233	mulneg2d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · - ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = - ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
323	321 322	eqtr3d	⊢ ( ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) ) ) = - ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
324	282 323	sumeq12rdv	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) - ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
325	317 324	eqtr3d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ( ( ⌊ ‘ 𝑥 ) + 1 ) · ( ( ψ ‘ ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) + ( 𝑥 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ) − ( 1 · ( ( ψ ‘ ( 𝑥 / 1 ) ) + ( 𝑥 / 1 ) ) ) ) − Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( 𝑛 + 1 ) − 𝑛 ) · ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) - ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
326	236 289 325	3eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → - ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) - ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
327	11 234	fsumneg	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) - ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) )
328	326 327	eqtr2d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = - ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
329	235 198 328	neg11d	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( ( ( ψ ‘ ( 𝑥 / 𝑛 ) ) + ( 𝑥 / 𝑛 ) ) − ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) ) = ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
330	232 329	breqtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) ≤ ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) )
331	189 176 39 330	lediv1dd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) )
332	177	leabsd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
333	190 177 200 331 332	letrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ≤ ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
334	197 333	eqbrtrd	⊢ ( ( 𝜑 ∧ 𝑥 ∈ ( 1 (,) +∞ ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
335	334	adantrr	⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ ( 1 (,) +∞ ) ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ≤ ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ψ ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) + ( 𝑥 / ( 𝑛 + 1 ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) )
336	5 175 177 191 335	o1le	⊢ ( 𝜑 → ( 𝑥 ∈ ( 1 (,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 𝑛 · ( abs ‘ ( ( 𝑅 ‘ ( 𝑥 / ( 𝑛 + 1 ) ) ) − ( 𝑅 ‘ ( 𝑥 / 𝑛 ) ) ) ) ) / ( 𝑥 · ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )