Metamath Proof Explorer

Theorem dvfsumrlim2

Description: Compare a finite sum to an integral (the integral here is given as a function with a known derivative). The statement here says that if x e. S |-> B is a decreasing function with antiderivative A converging to zero, then the difference between sum_ k e. ( M ... ( |_x ) ) B ( k ) and S. u e. ( M , x ) B ( u ) _d u = A ( x ) converges to a constant limit value, with the remainder term bounded by B ( x ) . (Contributed by Mario Carneiro, 18-May-2016)

Ref Expression
Hypotheses dvfsum.s ⊢ 𝑆 = ( 𝑇 (,) +∞ )
dvfsum.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
dvfsum.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
dvfsum.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
dvfsum.md ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
dvfsum.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
dvfsum.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
dvfsum.b1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
dvfsum.b2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
dvfsum.b3 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
dvfsum.c ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
dvfsumrlim.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) ) → 𝐶 ≤ 𝐵 )
dvfsumrlim.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
dvfsumrlim.k ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 )
dvfsumrlim2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dvfsumrlim2.2 ⊢ ( 𝜑 → 𝐷 ≤ 𝑋 )
Assertion dvfsumrlim2 ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )

Proof

Step Hyp Ref Expression
1 dvfsum.s ⊢ 𝑆 = ( 𝑇 (,) +∞ )
2 dvfsum.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 dvfsum.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 dvfsum.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5 dvfsum.md ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
6 dvfsum.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
7 dvfsum.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
8 dvfsum.b1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
9 dvfsum.b2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
10 dvfsum.b3 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
11 dvfsum.c ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
12 dvfsumrlim.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) ) → 𝐶 ≤ 𝐵 )
13 dvfsumrlim.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
14 dvfsumrlim.k ⊢ ( 𝜑 → ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 )
15 dvfsumrlim2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
16 dvfsumrlim2.2 ⊢ ( 𝜑 → 𝐷 ≤ 𝑋 )
17 ioossre ⊢ ( 𝑇 (,) +∞ ) ⊆ ℝ
18 1 17 eqsstri ⊢ 𝑆 ⊆ ℝ
19 18 15 sseldi ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
20 19 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
21 19 renepnfd ⊢ ( 𝜑 → 𝑋 ≠ +∞ )
22 icopnfsup ⊢ ( ( 𝑋 ∈ ℝ* ∧ 𝑋 ≠ +∞ ) → sup ( ( 𝑋 [,) +∞ ) , ℝ* , < ) = +∞ )
23 20 21 22 syl2anc ⊢ ( 𝜑 → sup ( ( 𝑋 [,) +∞ ) , ℝ* , < ) = +∞ )
24 23 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → sup ( ( 𝑋 [,) +∞ ) , ℝ* , < ) = +∞ )
25 1 2 3 4 5 6 7 8 9 10 11 13 dvfsumrlimf ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℝ )
26 25 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝐺 : 𝑆 ⟶ ℝ )
27 15 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑋 ∈ 𝑆 )
28 26 27 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ℝ )
29 28 recnd ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( 𝐺 ‘ 𝑋 ) ∈ ℂ )
30 6 rexrd ⊢ ( 𝜑 → 𝑇 ∈ ℝ* )
31 15 1 eleqtrdi ⊢ ( 𝜑 → 𝑋 ∈ ( 𝑇 (,) +∞ ) )
32 elioopnf ⊢ ( 𝑇 ∈ ℝ* → ( 𝑋 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) ) )
33 30 32 syl ⊢ ( 𝜑 → ( 𝑋 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) ) )
34 31 33 mpbid ⊢ ( 𝜑 → ( 𝑋 ∈ ℝ ∧ 𝑇 < 𝑋 ) )
35 34 simprd ⊢ ( 𝜑 → 𝑇 < 𝑋 )
36 df-ioo ⊢ (,) = ( 𝑢 ∈ ℝ* , 𝑣 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑢 < 𝑤 ∧ 𝑤 < 𝑣 ) } )
37 df-ico ⊢ [,) = ( 𝑢 ∈ ℝ* , 𝑣 ∈ ℝ* ↦ { 𝑤 ∈ ℝ* ∣ ( 𝑢 ≤ 𝑤 ∧ 𝑤 < 𝑣 ) } )
38 xrltletr ⊢ ( ( 𝑇 ∈ ℝ* ∧ 𝑋 ∈ ℝ* ∧ 𝑧 ∈ ℝ* ) → ( ( 𝑇 < 𝑋 ∧ 𝑋 ≤ 𝑧 ) → 𝑇 < 𝑧 ) )
39 36 37 38 ixxss1 ⊢ ( ( 𝑇 ∈ ℝ* ∧ 𝑇 < 𝑋 ) → ( 𝑋 [,) +∞ ) ⊆ ( 𝑇 (,) +∞ ) )
40 30 35 39 syl2anc ⊢ ( 𝜑 → ( 𝑋 [,) +∞ ) ⊆ ( 𝑇 (,) +∞ ) )
41 40 1 sseqtrrdi ⊢ ( 𝜑 → ( 𝑋 [,) +∞ ) ⊆ 𝑆 )
42 41 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝑋 [,) +∞ ) ⊆ 𝑆 )
43 42 sselda ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑦 ∈ 𝑆 )
44 26 43 ffvelrnd ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ℝ )
45 44 recnd ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ℂ )
46 29 45 subcld ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑦 ) ) ∈ ℂ )
47 pnfxr ⊢ +∞ ∈ ℝ*
48 icossre ⊢ ( ( 𝑋 ∈ ℝ ∧ +∞ ∈ ℝ* ) → ( 𝑋 [,) +∞ ) ⊆ ℝ )
49 19 47 48 sylancl ⊢ ( 𝜑 → ( 𝑋 [,) +∞ ) ⊆ ℝ )
50 49 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝑋 [,) +∞ ) ⊆ ℝ )
51 rlimf ⊢ ( 𝐺 ⇝𝑟 𝐿 → 𝐺 : dom 𝐺 ⟶ ℂ )
52 51 adantl ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → 𝐺 : dom 𝐺 ⟶ ℂ )
53 ovex ⊢ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ∈ V
54 53 13 dmmpti ⊢ dom 𝐺 = 𝑆
55 54 feq2i ⊢ ( 𝐺 : dom 𝐺 ⟶ ℂ ↔ 𝐺 : 𝑆 ⟶ ℂ )
56 52 55 sylib ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → 𝐺 : 𝑆 ⟶ ℂ )
57 15 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → 𝑋 ∈ 𝑆 )
58 56 57 ffvelrnd ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝐺 ‘ 𝑋 ) ∈ ℂ )
59 rlimconst ⊢ ( ( ( 𝑋 [,) +∞ ) ⊆ ℝ ∧ ( 𝐺 ‘ 𝑋 ) ∈ ℂ ) → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↦ ( 𝐺 ‘ 𝑋 ) ) ⇝𝑟 ( 𝐺 ‘ 𝑋 ) )
60 50 58 59 syl2anc ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↦ ( 𝐺 ‘ 𝑋 ) ) ⇝𝑟 ( 𝐺 ‘ 𝑋 ) )
61 56 feqmptd ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → 𝐺 = ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑦 ) ) )
62 simpr ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → 𝐺 ⇝𝑟 𝐿 )
63 61 62 eqbrtrrd ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝑦 ∈ 𝑆 ↦ ( 𝐺 ‘ 𝑦 ) ) ⇝𝑟 𝐿 )
64 42 63 rlimres2 ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↦ ( 𝐺 ‘ 𝑦 ) ) ⇝𝑟 𝐿 )
65 29 45 60 64 rlimsub ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↦ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑦 ) ) ) ⇝𝑟 ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) )
66 46 65 rlimabs ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↦ ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑦 ) ) ) ) ⇝𝑟 ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) )
67 18 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
68 67 7 8 10 dvmptrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
69 68 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ )
70 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐵
71 70 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ
72 csbeq1a ⊢ ( 𝑥 = 𝑋 → 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
73 72 eleq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
74 71 73 rspc ⊢ ( 𝑋 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
75 15 69 74 sylc ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ )
76 75 recnd ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ )
77 rlimconst ⊢ ( ( ( 𝑋 [,) +∞ ) ⊆ ℝ ∧ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ ) → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ⇝𝑟 ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
78 49 76 77 syl2anc ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ⇝𝑟 ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
79 78 adantr ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↦ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ⇝𝑟 ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
80 46 abscld ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑦 ) ) ) ∈ ℝ )
81 75 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ )
82 29 45 abssubd ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑦 ) ) ) = ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑋 ) ) ) )
83 3 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑀 ∈ ℤ )
84 4 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝐷 ∈ ℝ )
85 5 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑀 ≤ ( 𝐷 + 1 ) )
86 6 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑇 ∈ ℝ )
87 7 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
88 8 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
89 9 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
90 10 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
91 47 a1i ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → +∞ ∈ ℝ* )
92 3simpa ⊢ ( ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞ ) → ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) )
93 92 12 syl3an3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞ ) ) → 𝐶 ≤ 𝐵 )
94 93 3adant1r ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞ ) ) → 𝐶 ≤ 𝐵 )
95 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dvfsumrlimge0 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 0 ≤ 𝐵 )
96 95 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) ) → 0 ≤ 𝐵 )
97 96 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) ) → 0 ≤ 𝐵 )
98 15 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑋 ∈ 𝑆 )
99 41 sselda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑦 ∈ 𝑆 )
100 16 adantr ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝐷 ≤ 𝑋 )
101 elicopnf ⊢ ( 𝑋 ∈ ℝ → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ) ) )
102 19 101 syl ⊢ ( 𝜑 → ( 𝑦 ∈ ( 𝑋 [,) +∞ ) ↔ ( 𝑦 ∈ ℝ ∧ 𝑋 ≤ 𝑦 ) ) )
103 102 simplbda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑋 ≤ 𝑦 )
104 102 simprbda ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑦 ∈ ℝ )
105 104 rexrd ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑦 ∈ ℝ* )
106 pnfge ⊢ ( 𝑦 ∈ ℝ* → 𝑦 ≤ +∞ )
107 105 106 syl ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → 𝑦 ≤ +∞ )
108 1 2 83 84 85 86 87 88 89 90 11 91 94 13 97 98 99 100 103 107 dvfsumlem4 ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑋 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
109 108 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑋 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
110 82 109 eqbrtrd ⊢ ( ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) ∧ 𝑦 ∈ ( 𝑋 [,) +∞ ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − ( 𝐺 ‘ 𝑦 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
111 24 66 79 80 81 110 rlimle ⊢ ( ( 𝜑 ∧ 𝐺 ⇝𝑟 𝐿 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑋 ) − 𝐿 ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )