Theorem pntrsumo1

Description: A bound on a sum over R . Equation 10.1.16 of Shapiro, p. 403. (Contributed by Mario Carneiro, 25-May-2016)

	Ref	Expression
Hypothesis	pntrval.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
Assertion	pntrsumo1	⊢ ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ 𝑂(1)

Proof

Step	Hyp	Ref	Expression
1		pntrval.r	⊢ 𝑅 = ( 𝑎 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑎 ) − 𝑎 ) )
2		1re	⊢ 1 ∈ ℝ
3		elicopnf	⊢ ( 1 ∈ ℝ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) ) )
4	2 3	ax-mp	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↔ ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) )
5	4	simplbi	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ )
6		0red	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 0 ∈ ℝ )
7		1red	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 1 ∈ ℝ )
8		0lt1	⊢ 0 < 1
9	8	a1i	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 0 < 1 )
10	4	simprbi	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 1 ≤ 𝑥 )
11	6 7 5 9 10	ltletrd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 0 < 𝑥 )
12	5 11	elrpd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 𝑥 ∈ ℝ+ )
13	12	ssriv	⊢ ( 1 [,) +∞ ) ⊆ ℝ+
14	13	a1i	⊢ ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ+ )
15		rpssre	⊢ ℝ+ ⊆ ℝ
16	14 15	sstrdi	⊢ ( ⊤ → ( 1 [,) +∞ ) ⊆ ℝ )
17	16	resmptd	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ↾ ( 1 [,) +∞ ) ) = ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
18		chpcl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ 𝑥 ) ∈ ℝ )
19	5 18	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
20		peano2re	⊢ ( ( ψ ‘ 𝑥 ) ∈ ℝ → ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℝ )
21	19 20	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℝ )
22	12	rprege0d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
23		flge0nn0	⊢ ( ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
24	22 23	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
25		nn0p1nn	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℕ0 → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
26	24 25	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
27	21 26	nndivred	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ )
28	27	recnd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℂ )
29		ax-1cn	⊢ 1 ∈ ℂ
30		subcl	⊢ ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ∈ ℂ )
31	28 29 30	sylancl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ∈ ℂ )
32		fzfid	⊢ ( 𝑥 ∈ ℝ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
33		elfznn	⊢ ( 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) → 𝑛 ∈ ℕ )
34	33	adantl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
35		nnrp	⊢ ( 𝑛 ∈ ℕ → 𝑛 ∈ ℝ+ )
36	1	pntrf	⊢ 𝑅 : ℝ+ ⟶ ℝ
37	36	ffvelcdmi	⊢ ( 𝑛 ∈ ℝ+ → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
38	35 37	syl	⊢ ( 𝑛 ∈ ℕ → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
39		peano2nn	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 + 1 ) ∈ ℕ )
40		nnmulcl	⊢ ( ( 𝑛 ∈ ℕ ∧ ( 𝑛 + 1 ) ∈ ℕ ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
41	39 40	mpdan	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
42	38 41	nndivred	⊢ ( 𝑛 ∈ ℕ → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
43	34 42	syl	⊢ ( ( 𝑥 ∈ ℝ ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
44	32 43	fsumrecl	⊢ ( 𝑥 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
45	44	recnd	⊢ ( 𝑥 ∈ ℝ → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
46	5 45	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
47		oveq2	⊢ ( 𝑚 = 𝑛 → ( 1 / 𝑚 ) = ( 1 / 𝑛 ) )
48		fvoveq1	⊢ ( 𝑚 = 𝑛 → ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( 𝑛 − 1 ) ) )
49		oveq1	⊢ ( 𝑚 = 𝑛 → ( 𝑚 − 1 ) = ( 𝑛 − 1 ) )
50	48 49	oveq12d	⊢ ( 𝑚 = 𝑛 → ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) − ( 𝑛 − 1 ) ) )
51	47 50	jca	⊢ ( 𝑚 = 𝑛 → ( ( 1 / 𝑚 ) = ( 1 / 𝑛 ) ∧ ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) − ( 𝑛 − 1 ) ) ) )
52		oveq2	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 1 / 𝑚 ) = ( 1 / ( 𝑛 + 1 ) ) )
53		fvoveq1	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) )
54		oveq1	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( 𝑚 − 1 ) = ( ( 𝑛 + 1 ) − 1 ) )
55	53 54	oveq12d	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) )
56	52 55	jca	⊢ ( 𝑚 = ( 𝑛 + 1 ) → ( ( 1 / 𝑚 ) = ( 1 / ( 𝑛 + 1 ) ) ∧ ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) ) )
57		oveq2	⊢ ( 𝑚 = 1 → ( 1 / 𝑚 ) = ( 1 / 1 ) )
58		1div1e1	⊢ ( 1 / 1 ) = 1
59	57 58	eqtrdi	⊢ ( 𝑚 = 1 → ( 1 / 𝑚 ) = 1 )
60		oveq1	⊢ ( 𝑚 = 1 → ( 𝑚 − 1 ) = ( 1 − 1 ) )
61		1m1e0	⊢ ( 1 − 1 ) = 0
62	60 61	eqtrdi	⊢ ( 𝑚 = 1 → ( 𝑚 − 1 ) = 0 )
63	62	fveq2d	⊢ ( 𝑚 = 1 → ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ 0 ) )
64		2pos	⊢ 0 < 2
65		0re	⊢ 0 ∈ ℝ
66		chpeq0	⊢ ( 0 ∈ ℝ → ( ( ψ ‘ 0 ) = 0 ↔ 0 < 2 ) )
67	65 66	ax-mp	⊢ ( ( ψ ‘ 0 ) = 0 ↔ 0 < 2 )
68	64 67	mpbir	⊢ ( ψ ‘ 0 ) = 0
69	63 68	eqtrdi	⊢ ( 𝑚 = 1 → ( ψ ‘ ( 𝑚 − 1 ) ) = 0 )
70	69 62	oveq12d	⊢ ( 𝑚 = 1 → ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = ( 0 − 0 ) )
71		0m0e0	⊢ ( 0 − 0 ) = 0
72	70 71	eqtrdi	⊢ ( 𝑚 = 1 → ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = 0 )
73	59 72	jca	⊢ ( 𝑚 = 1 → ( ( 1 / 𝑚 ) = 1 ∧ ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = 0 ) )
74		oveq2	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 1 / 𝑚 ) = ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
75		fvoveq1	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ψ ‘ ( 𝑚 − 1 ) ) = ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) )
76		oveq1	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( 𝑚 − 1 ) = ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) )
77	75 76	oveq12d	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) )
78	74 77	jca	⊢ ( 𝑚 = ( ( ⌊ ‘ 𝑥 ) + 1 ) → ( ( 1 / 𝑚 ) = ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∧ ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) = ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) )
79		nnuz	⊢ ℕ = ( ℤ≥ ‘ 1 )
80	26 79	eleqtrdi	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ( ℤ≥ ‘ 1 ) )
81		elfznn	⊢ ( 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) → 𝑚 ∈ ℕ )
82	81	adantl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℕ )
83	82	nnrecred	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 1 / 𝑚 ) ∈ ℝ )
84	83	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 1 / 𝑚 ) ∈ ℂ )
85	82	nnred	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 𝑚 ∈ ℝ )
86		peano2rem	⊢ ( 𝑚 ∈ ℝ → ( 𝑚 − 1 ) ∈ ℝ )
87	85 86	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑚 − 1 ) ∈ ℝ )
88		chpcl	⊢ ( ( 𝑚 − 1 ) ∈ ℝ → ( ψ ‘ ( 𝑚 − 1 ) ) ∈ ℝ )
89	87 88	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ψ ‘ ( 𝑚 − 1 ) ) ∈ ℝ )
90	89 87	resubcld	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) ∈ ℝ )
91	90	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑚 ∈ ( 1 ... ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → ( ( ψ ‘ ( 𝑚 − 1 ) ) − ( 𝑚 − 1 ) ) ∈ ℂ )
92	51 56 73 78 80 84 91	fsumparts	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( 1 / 𝑛 ) · ( ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) − ( ( ψ ‘ ( 𝑛 − 1 ) ) − ( 𝑛 − 1 ) ) ) ) = ( ( ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) − ( 1 · 0 ) ) − Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( 1 / ( 𝑛 + 1 ) ) − ( 1 / 𝑛 ) ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) ) ) )
93	5	flcld	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ⌊ ‘ 𝑥 ) ∈ ℤ )
94		fzval3	⊢ ( ( ⌊ ‘ 𝑥 ) ∈ ℤ → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
95	93 94	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) = ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
96	95	eqcomd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) = ( 1 ... ( ⌊ ‘ 𝑥 ) ) )
97	33	adantl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
98	97	nncnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
99		pncan	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
100	98 29 99	sylancl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 1 ) = 𝑛 )
101	97	nnred	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ )
102	100 101	eqeltrd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 1 ) ∈ ℝ )
103		chpcl	⊢ ( ( ( 𝑛 + 1 ) − 1 ) ∈ ℝ → ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) ∈ ℝ )
104	102 103	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) ∈ ℝ )
105	104	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) ∈ ℂ )
106	102	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 1 ) ∈ ℂ )
107		peano2rem	⊢ ( 𝑛 ∈ ℝ → ( 𝑛 − 1 ) ∈ ℝ )
108	101 107	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℝ )
109		chpcl	⊢ ( ( 𝑛 − 1 ) ∈ ℝ → ( ψ ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
110	108 109	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑛 − 1 ) ) ∈ ℝ )
111	110	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( 𝑛 − 1 ) ) ∈ ℂ )
112		1cnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
113	98 112	subcld	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℂ )
114	105 106 111 113	sub4d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) − ( ( ψ ‘ ( 𝑛 − 1 ) ) − ( 𝑛 − 1 ) ) ) = ( ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ψ ‘ ( 𝑛 − 1 ) ) ) − ( ( ( 𝑛 + 1 ) − 1 ) − ( 𝑛 − 1 ) ) ) )
115		vmacl	⊢ ( 𝑛 ∈ ℕ → ( Λ ‘ 𝑛 ) ∈ ℝ )
116	97 115	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
117	116	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
118		nnm1nn0	⊢ ( 𝑛 ∈ ℕ → ( 𝑛 − 1 ) ∈ ℕ0 )
119	97 118	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 − 1 ) ∈ ℕ0 )
120		chpp1	⊢ ( ( 𝑛 − 1 ) ∈ ℕ0 → ( ψ ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) )
121	119 120	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) )
122		npcan	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
123	98 29 122	sylancl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 − 1 ) + 1 ) = 𝑛 )
124	123 100	eqtr4d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 − 1 ) + 1 ) = ( ( 𝑛 + 1 ) − 1 ) )
125	124	fveq2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) )
126	123	fveq2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ ( ( 𝑛 − 1 ) + 1 ) ) = ( Λ ‘ 𝑛 ) )
127	126	oveq2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ ( ( 𝑛 − 1 ) + 1 ) ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ 𝑛 ) ) )
128	121 125 127	3eqtr3d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( ( ψ ‘ ( 𝑛 − 1 ) ) + ( Λ ‘ 𝑛 ) ) )
129	111 117 128	mvrladdd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ψ ‘ ( 𝑛 − 1 ) ) ) = ( Λ ‘ 𝑛 ) )
130		peano2cn	⊢ ( 𝑛 ∈ ℂ → ( 𝑛 + 1 ) ∈ ℂ )
131	98 130	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ∈ ℂ )
132	131 98 112	nnncan2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) − 1 ) − ( 𝑛 − 1 ) ) = ( ( 𝑛 + 1 ) − 𝑛 ) )
133		pncan2	⊢ ( ( 𝑛 ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( 𝑛 + 1 ) − 𝑛 ) = 1 )
134	98 29 133	sylancl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 𝑛 ) = 1 )
135	132 134	eqtrd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) − 1 ) − ( 𝑛 − 1 ) ) = 1 )
136	129 135	oveq12d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ψ ‘ ( 𝑛 − 1 ) ) ) − ( ( ( 𝑛 + 1 ) − 1 ) − ( 𝑛 − 1 ) ) ) = ( ( Λ ‘ 𝑛 ) − 1 ) )
137	114 136	eqtrd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) − ( ( ψ ‘ ( 𝑛 − 1 ) ) − ( 𝑛 − 1 ) ) ) = ( ( Λ ‘ 𝑛 ) − 1 ) )
138	137	oveq2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 / 𝑛 ) · ( ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) − ( ( ψ ‘ ( 𝑛 − 1 ) ) − ( 𝑛 − 1 ) ) ) ) = ( ( 1 / 𝑛 ) · ( ( Λ ‘ 𝑛 ) − 1 ) ) )
139		peano2rem	⊢ ( ( Λ ‘ 𝑛 ) ∈ ℝ → ( ( Λ ‘ 𝑛 ) − 1 ) ∈ ℝ )
140	116 139	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) − 1 ) ∈ ℝ )
141	140	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) − 1 ) ∈ ℂ )
142	97	nnne0d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
143	141 98 142	divrec2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) = ( ( 1 / 𝑛 ) · ( ( Λ ‘ 𝑛 ) − 1 ) ) )
144	138 143	eqtr4d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 / 𝑛 ) · ( ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) − ( ( ψ ‘ ( 𝑛 − 1 ) ) − ( 𝑛 − 1 ) ) ) ) = ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) )
145	96 144	sumeq12rdv	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( 1 / 𝑛 ) · ( ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) − ( ( ψ ‘ ( 𝑛 − 1 ) ) − ( 𝑛 − 1 ) ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) )
146	24	nn0cnd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ⌊ ‘ 𝑥 ) ∈ ℂ )
147		pncan	⊢ ( ( ( ⌊ ‘ 𝑥 ) ∈ ℂ ∧ 1 ∈ ℂ ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑥 ) )
148	146 29 147	sylancl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) = ( ⌊ ‘ 𝑥 ) )
149	148	fveq2d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( ψ ‘ ( ⌊ ‘ 𝑥 ) ) )
150		chpfl	⊢ ( 𝑥 ∈ ℝ → ( ψ ‘ ( ⌊ ‘ 𝑥 ) ) = ( ψ ‘ 𝑥 ) )
151	5 150	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ψ ‘ ( ⌊ ‘ 𝑥 ) ) = ( ψ ‘ 𝑥 ) )
152	149 151	eqtrd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( ψ ‘ 𝑥 ) )
153	152	oveq1d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( ( ψ ‘ 𝑥 ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) )
154	19	recnd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ψ ‘ 𝑥 ) ∈ ℂ )
155	26	nncnd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℂ )
156		1cnd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → 1 ∈ ℂ )
157	154 155 156	subsub3d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ψ ‘ 𝑥 ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( ( ( ψ ‘ 𝑥 ) + 1 ) − ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
158	153 157	eqtrd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) = ( ( ( ψ ‘ 𝑥 ) + 1 ) − ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
159	158	oveq2d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) = ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( ψ ‘ 𝑥 ) + 1 ) − ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
160	26	nnrecred	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ )
161	160	recnd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℂ )
162		peano2cn	⊢ ( ( ψ ‘ 𝑥 ) ∈ ℂ → ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℂ )
163	154 162	syl	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℂ )
164	161 163 155	subdid	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ( ψ ‘ 𝑥 ) + 1 ) − ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ 𝑥 ) + 1 ) ) − ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) )
165	26	nnne0d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ≠ 0 )
166	163 155 165	divrec2d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) = ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ 𝑥 ) + 1 ) ) )
167	166	eqcomd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ 𝑥 ) + 1 ) ) = ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
168	155 165	recid2d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ⌊ ‘ 𝑥 ) + 1 ) ) = 1 )
169	167 168	oveq12d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ 𝑥 ) + 1 ) ) − ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) )
170	159 164 169	3eqtrd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) = ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) )
171	29	mul01i	⊢ ( 1 · 0 ) = 0
172	171	a1i	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( 1 · 0 ) = 0 )
173	170 172	oveq12d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) − ( 1 · 0 ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) − 0 ) )
174	31	subid1d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) − 0 ) = ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) )
175	173 174	eqtrd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) − ( 1 · 0 ) ) = ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) )
176	97 41	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℕ )
177	176	nnrecred	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
178	177	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
179	97 38	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
180	179	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ 𝑛 ) ∈ ℂ )
181	178 180	mulneg1d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( - ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) · ( 𝑅 ‘ 𝑛 ) ) = - ( ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) · ( 𝑅 ‘ 𝑛 ) ) )
182	98 112	mulcld	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · 1 ) ∈ ℂ )
183	98 131	mulcld	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ∈ ℂ )
184	176	nnne0d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · ( 𝑛 + 1 ) ) ≠ 0 )
185	131 182 183 184	divsubdird	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) − ( 𝑛 · 1 ) ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( ( ( 𝑛 + 1 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) − ( ( 𝑛 · 1 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
186	98	mulridd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 · 1 ) = 𝑛 )
187	186	oveq2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − ( 𝑛 · 1 ) ) = ( ( 𝑛 + 1 ) − 𝑛 ) )
188	187 134	eqtrd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − ( 𝑛 · 1 ) ) = 1 )
189	188	oveq1d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) − ( 𝑛 · 1 ) ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
190	131	mulridd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) · 1 ) = ( 𝑛 + 1 ) )
191	131 98	mulcomd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) · 𝑛 ) = ( 𝑛 · ( 𝑛 + 1 ) ) )
192	190 191	oveq12d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) · 1 ) / ( ( 𝑛 + 1 ) · 𝑛 ) ) = ( ( 𝑛 + 1 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
193	97 39	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ∈ ℕ )
194	193	nnne0d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑛 + 1 ) ≠ 0 )
195	112 98 131 142 194	divcan5d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) · 1 ) / ( ( 𝑛 + 1 ) · 𝑛 ) ) = ( 1 / 𝑛 ) )
196	192 195	eqtr3d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( 1 / 𝑛 ) )
197	112 131 98 194 142	divcan5d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 · 1 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( 1 / ( 𝑛 + 1 ) ) )
198	196 197	oveq12d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 𝑛 + 1 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) − ( ( 𝑛 · 1 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = ( ( 1 / 𝑛 ) − ( 1 / ( 𝑛 + 1 ) ) ) )
199	185 189 198	3eqtr3d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( ( 1 / 𝑛 ) − ( 1 / ( 𝑛 + 1 ) ) ) )
200	199	negeqd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → - ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) = - ( ( 1 / 𝑛 ) − ( 1 / ( 𝑛 + 1 ) ) ) )
201	97	nnrecred	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
202	201	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
203	193	nnrecred	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( 𝑛 + 1 ) ) ∈ ℝ )
204	203	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / ( 𝑛 + 1 ) ) ∈ ℂ )
205	202 204	negsubdi2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → - ( ( 1 / 𝑛 ) − ( 1 / ( 𝑛 + 1 ) ) ) = ( ( 1 / ( 𝑛 + 1 ) ) − ( 1 / 𝑛 ) ) )
206	200 205	eqtr2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 1 / ( 𝑛 + 1 ) ) − ( 1 / 𝑛 ) ) = - ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
207	97	nnrpd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℝ+ )
208	100 207	eqeltrd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑛 + 1 ) − 1 ) ∈ ℝ+ )
209	1	pntrval	⊢ ( ( ( 𝑛 + 1 ) − 1 ) ∈ ℝ+ → ( 𝑅 ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) )
210	208 209	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) )
211	100	fveq2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 𝑅 ‘ ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑅 ‘ 𝑛 ) )
212	210 211	eqtr3d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) = ( 𝑅 ‘ 𝑛 ) )
213	206 212	oveq12d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 1 / ( 𝑛 + 1 ) ) − ( 1 / 𝑛 ) ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) ) = ( - ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) · ( 𝑅 ‘ 𝑛 ) ) )
214	180 183 184	divrec2d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = ( ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) · ( 𝑅 ‘ 𝑛 ) ) )
215	214	negeqd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = - ( ( 1 / ( 𝑛 · ( 𝑛 + 1 ) ) ) · ( 𝑅 ‘ 𝑛 ) ) )
216	181 213 215	3eqtr4d	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( 1 / ( 𝑛 + 1 ) ) − ( 1 / 𝑛 ) ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) ) = - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
217	96 216	sumeq12rdv	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( 1 / ( 𝑛 + 1 ) ) − ( 1 / 𝑛 ) ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
218		fzfid	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
219	97 42	syl	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℝ )
220	219	recnd	⊢ ( ( 𝑥 ∈ ( 1 [,) +∞ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ∈ ℂ )
221	218 220	fsumneg	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) - ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) = - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
222	217 221	eqtrd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( 1 / ( 𝑛 + 1 ) ) − ( 1 / 𝑛 ) ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) ) = - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
223	175 222	oveq12d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( ( 1 / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) · ( ( ψ ‘ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) − ( ( ( ⌊ ‘ 𝑥 ) + 1 ) − 1 ) ) ) − ( 1 · 0 ) ) − Σ 𝑛 ∈ ( 1 ..^ ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ( ( ( 1 / ( 𝑛 + 1 ) ) − ( 1 / 𝑛 ) ) · ( ( ψ ‘ ( ( 𝑛 + 1 ) − 1 ) ) − ( ( 𝑛 + 1 ) − 1 ) ) ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) − - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
224	92 145 223	3eqtr3d	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) = ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) − - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
225	31 46	subnegd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) − - Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
226	224 225	eqtrd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) = ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) + Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) )
227	31 46 226	mvrladdd	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) − ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
228	227	mpteq2ia	⊢ ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) − ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ) ) = ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
229		fzfid	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 ... ( ⌊ ‘ 𝑥 ) ) ∈ Fin )
230	33	adantl	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℕ )
231	230 115	syl	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℝ )
232	231 139	syl	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) − 1 ) ∈ ℝ )
233	232 230	nndivred	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) ∈ ℝ )
234	229 233	fsumrecl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) ∈ ℝ )
235		rpre	⊢ ( 𝑥 ∈ ℝ+ → 𝑥 ∈ ℝ )
236	235	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ )
237	236 18	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ψ ‘ 𝑥 ) ∈ ℝ )
238	237 20	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℝ )
239		rprege0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 ≤ 𝑥 ) )
240	239 23	syl	⊢ ( 𝑥 ∈ ℝ+ → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
241	240	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ⌊ ‘ 𝑥 ) ∈ ℕ0 )
242	241 25	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℕ )
243	238 242	nndivred	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ )
244		peano2rem	⊢ ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℝ → ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ∈ ℝ )
245	243 244	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ∈ ℝ )
246		reex	⊢ ℝ ∈ V
247	246 15	ssexi	⊢ ℝ+ ∈ V
248	247	a1i	⊢ ( ⊤ → ℝ+ ∈ V )
249	231 230	nndivred	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℝ )
250	249	recnd	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
251	229 250	fsumcl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) ∈ ℂ )
252		relogcl	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ∈ ℝ )
253	252	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℝ )
254	253	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ∈ ℂ )
255	251 254	subcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
256	230	nnrecred	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℝ )
257	229 256	fsumrecl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ∈ ℝ )
258	257 253	resubcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℝ )
259		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) )
260		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) )
261	248 255 258 259 260	offval2	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ) )
262	256	recnd	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( 1 / 𝑛 ) ∈ ℂ )
263	229 250 262	fsumsub	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( 1 / 𝑛 ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) )
264	231	recnd	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( Λ ‘ 𝑛 ) ∈ ℂ )
265		1cnd	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 1 ∈ ℂ )
266	230	nncnd	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ∈ ℂ )
267	230	nnne0d	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → 𝑛 ≠ 0 )
268	264 265 266 267	divsubdird	⊢ ( ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) ∧ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ) → ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) = ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( 1 / 𝑛 ) ) )
269	268	sumeq2dv	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( 1 / 𝑛 ) ) )
270	257	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ∈ ℂ )
271	251 270 254	nnncan2d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ) )
272	263 269 271	3eqtr4rd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) = Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) )
273	272	mpteq2dva	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) − ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) ) )
274	261 273	eqtrd	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ) = ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) ) )
275		vmadivsum	⊢ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1)
276	15	a1i	⊢ ( ⊤ → ℝ+ ⊆ ℝ )
277	258	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ∈ ℂ )
278		1red	⊢ ( ⊤ → 1 ∈ ℝ )
279		harmoniclbnd	⊢ ( 𝑥 ∈ ℝ+ → ( log ‘ 𝑥 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) )
280	279	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( log ‘ 𝑥 ) ≤ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) )
281	253 257 280	abssubge0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) )
282	281	adantrr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) = ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) )
283	235	ad2antrl	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 𝑥 ∈ ℝ )
284		simprr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → 1 ≤ 𝑥 )
285		harmonicubnd	⊢ ( ( 𝑥 ∈ ℝ ∧ 1 ≤ 𝑥 ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
286	283 284 285	syl2anc	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) )
287		1red	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℝ )
288	257 253 287	lesubadd2d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ≤ 1 ↔ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) ) )
289	288	adantrr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ≤ 1 ↔ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) ≤ ( ( log ‘ 𝑥 ) + 1 ) ) )
290	286 289	mpbird	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ≤ 1 )
291	282 290	eqbrtrd	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ≤ 1 )
292	276 277 278 278 291	elo1d	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) )
293		o1sub	⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
294	275 292 293	sylancr	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( Λ ‘ 𝑛 ) / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ∘f − ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( 1 / 𝑛 ) − ( log ‘ 𝑥 ) ) ) ) ∈ 𝑂(1) )
295	274 294	eqeltrrd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) ) ∈ 𝑂(1) )
296	243	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∈ ℂ )
297		1cnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 1 ∈ ℂ )
298	237	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ψ ‘ 𝑥 ) ∈ ℂ )
299		rpcnne0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
300	299	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) )
301		divdir	⊢ ( ( ( ψ ‘ 𝑥 ) ∈ ℂ ∧ 1 ∈ ℂ ∧ ( 𝑥 ∈ ℂ ∧ 𝑥 ≠ 0 ) ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) = ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) )
302	298 297 300 301	syl3anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) = ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) )
303	302	mpteq2dva	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) )
304		simpr	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ∈ ℝ+ )
305	237 304	rerpdivcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) / 𝑥 ) ∈ ℝ )
306		rpreccl	⊢ ( 𝑥 ∈ ℝ+ → ( 1 / 𝑥 ) ∈ ℝ+ )
307	306	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 1 / 𝑥 ) ∈ ℝ+ )
308		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) )
309		eqidd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) = ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) )
310	248 305 307 308 309	offval2	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ) = ( 𝑥 ∈ ℝ+ ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) )
311		chpo1ub	⊢ ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1)
312		divrcnv	⊢ ( 1 ∈ ℂ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0 )
313	29 312	ax-mp	⊢ ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0
314		rlimo1	⊢ ( ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ⇝𝑟 0 → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ∈ 𝑂(1) )
315	313 314	mp1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ∈ 𝑂(1) )
316		o1add	⊢ ( ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∈ 𝑂(1) ∧ ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ∈ 𝑂(1) ) → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ) ∈ 𝑂(1) )
317	311 315 316	sylancr	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ+ ↦ ( ( ψ ‘ 𝑥 ) / 𝑥 ) ) ∘f + ( 𝑥 ∈ ℝ+ ↦ ( 1 / 𝑥 ) ) ) ∈ 𝑂(1) )
318	310 317	eqeltrrd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ψ ‘ 𝑥 ) / 𝑥 ) + ( 1 / 𝑥 ) ) ) ∈ 𝑂(1) )
319	303 318	eqeltrd	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) ∈ 𝑂(1) )
320	238 304	rerpdivcld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℝ )
321		chpge0	⊢ ( 𝑥 ∈ ℝ → 0 ≤ ( ψ ‘ 𝑥 ) )
322	236 321	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ ( ψ ‘ 𝑥 ) )
323	237 322	ge0p1rpd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℝ+ )
324	323	rprege0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℝ ∧ 0 ≤ ( ( ψ ‘ 𝑥 ) + 1 ) ) )
325	242	nnrpd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ+ )
326	325	rpregt0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ∧ 0 < ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
327		divge0	⊢ ( ( ( ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℝ ∧ 0 ≤ ( ( ψ ‘ 𝑥 ) + 1 ) ) ∧ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ∧ 0 < ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) → 0 ≤ ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
328	324 326 327	syl2anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 0 ≤ ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
329	243 328	absidd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) = ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) )
330	320	recnd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ∈ ℂ )
331	330	abscld	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) ∈ ℝ )
332		fllep1	⊢ ( 𝑥 ∈ ℝ → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
333	236 332	syl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) )
334		rpregt0	⊢ ( 𝑥 ∈ ℝ+ → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
335	334	adantl	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) )
336	323	rpregt0d	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℝ ∧ 0 < ( ( ψ ‘ 𝑥 ) + 1 ) ) )
337		lediv2	⊢ ( ( ( 𝑥 ∈ ℝ ∧ 0 < 𝑥 ) ∧ ( ( ( ⌊ ‘ 𝑥 ) + 1 ) ∈ ℝ ∧ 0 < ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ∧ ( ( ( ψ ‘ 𝑥 ) + 1 ) ∈ ℝ ∧ 0 < ( ( ψ ‘ 𝑥 ) + 1 ) ) ) → ( 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ↔ ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ≤ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
338	335 326 336 337	syl3anc	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( 𝑥 ≤ ( ( ⌊ ‘ 𝑥 ) + 1 ) ↔ ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ≤ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
339	333 338	mpbid	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ≤ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) )
340	320	leabsd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ≤ ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
341	243 320 331 339 340	letrd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ≤ ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
342	329 341	eqbrtrd	⊢ ( ( ⊤ ∧ 𝑥 ∈ ℝ+ ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ≤ ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
343	342	adantrr	⊢ ( ( ⊤ ∧ ( 𝑥 ∈ ℝ+ ∧ 1 ≤ 𝑥 ) ) → ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ≤ ( abs ‘ ( ( ( ψ ‘ 𝑥 ) + 1 ) / 𝑥 ) ) )
344	278 319 320 296 343	o1le	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) ) ∈ 𝑂(1) )
345		o1const	⊢ ( ( ℝ+ ⊆ ℝ ∧ 1 ∈ ℂ ) → ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) )
346	15 29 345	mp2an	⊢ ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1)
347	346	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ 1 ) ∈ 𝑂(1) )
348	296 297 344 347	o1sub2	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ) ∈ 𝑂(1) )
349	234 245 295 348	o1sub2	⊢ ( ⊤ → ( 𝑥 ∈ ℝ+ ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) − ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ) ) ∈ 𝑂(1) )
350	14 349	o1res2	⊢ ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ ( Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( ( Λ ‘ 𝑛 ) − 1 ) / 𝑛 ) − ( ( ( ( ψ ‘ 𝑥 ) + 1 ) / ( ( ⌊ ‘ 𝑥 ) + 1 ) ) − 1 ) ) ) ∈ 𝑂(1) )
351	228 350	eqeltrrid	⊢ ( ⊤ → ( 𝑥 ∈ ( 1 [,) +∞ ) ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ 𝑂(1) )
352	17 351	eqeltrd	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ↾ ( 1 [,) +∞ ) ) ∈ 𝑂(1) )
353		eqid	⊢ ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) = ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) )
354	353 45	fmpti	⊢ ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) : ℝ ⟶ ℂ
355	354	a1i	⊢ ( ⊤ → ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) : ℝ ⟶ ℂ )
356		ssidd	⊢ ( ⊤ → ℝ ⊆ ℝ )
357	355 356 278	o1resb	⊢ ( ⊤ → ( ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ 𝑂(1) ↔ ( ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ↾ ( 1 [,) +∞ ) ) ∈ 𝑂(1) ) )
358	352 357	mpbird	⊢ ( ⊤ → ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ 𝑂(1) )
359	358	mptru	⊢ ( 𝑥 ∈ ℝ ↦ Σ 𝑛 ∈ ( 1 ... ( ⌊ ‘ 𝑥 ) ) ( ( 𝑅 ‘ 𝑛 ) / ( 𝑛 · ( 𝑛 + 1 ) ) ) ) ∈ 𝑂(1)