Metamath Proof Explorer

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 ffvelrni ⊢ ( 𝑛 ∈ ℝ+ → ( 𝑅 ‘ 𝑛 ) ∈ ℝ )
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 mulid1d ⊢ ( ( 𝑥 ∈ ( 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 mulid1d ⊢ ( ( 𝑥 ∈ ( 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)