Metamath Proof Explorer

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) )