Metamath Proof Explorer

Theorem dvfsumrlim

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 A ( x ) = S. u e. ( M , x ) B ( u ) _d u 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 )
Assertion dvfsumrlim ( 𝜑 → 𝐺 ∈ dom ⇝𝑟 )

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 ioossre ⊢ ( 𝑇 (,) +∞ ) ⊆ ℝ
16 1 15 eqsstri ⊢ 𝑆 ⊆ ℝ
17 16 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
18 1 2 3 4 5 6 7 8 9 10 11 13 dvfsumrlimf ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℝ )
19 ax-resscn ⊢ ℝ ⊆ ℂ
20 fss ⊢ ( ( 𝐺 : 𝑆 ⟶ ℝ ∧ ℝ ⊆ ℂ ) → 𝐺 : 𝑆 ⟶ ℂ )
21 18 19 20 sylancl ⊢ ( 𝜑 → 𝐺 : 𝑆 ⟶ ℂ )
22 1 supeq1i ⊢ sup ( 𝑆 , ℝ* , < ) = sup ( ( 𝑇 (,) +∞ ) , ℝ* , < )
23 ressxr ⊢ ℝ ⊆ ℝ*
24 23 6 sseldi ⊢ ( 𝜑 → 𝑇 ∈ ℝ* )
25 6 renepnfd ⊢ ( 𝜑 → 𝑇 ≠ +∞ )
26 ioopnfsup ⊢ ( ( 𝑇 ∈ ℝ* ∧ 𝑇 ≠ +∞ ) → sup ( ( 𝑇 (,) +∞ ) , ℝ* , < ) = +∞ )
27 24 25 26 syl2anc ⊢ ( 𝜑 → sup ( ( 𝑇 (,) +∞ ) , ℝ* , < ) = +∞ )
28 22 27 syl5eq ⊢ ( 𝜑 → sup ( 𝑆 , ℝ* , < ) = +∞ )
29 8 14 rlimmptrcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℂ )
30 29 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℂ )
31 30 17 rlim0 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) ⇝𝑟 0 ↔ ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) ) )
32 14 31 mpbid ⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) )
33 16 a1i ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → 𝑆 ⊆ ℝ )
34 peano2re ⊢ ( 𝑇 ∈ ℝ → ( 𝑇 + 1 ) ∈ ℝ )
35 6 34 syl ⊢ ( 𝜑 → ( 𝑇 + 1 ) ∈ ℝ )
36 35 4 ifcld ⊢ ( 𝜑 → if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ∈ ℝ )
37 36 adantr ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ∈ ℝ )
38 rexico ⊢ ( ( 𝑆 ⊆ ℝ ∧ if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ∈ ℝ ) → ( ∃ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) ) )
39 33 37 38 syl2anc ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) ↔ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) ) )
40 elicopnf ⊢ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ∈ ℝ → ( 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ↔ ( 𝑐 ∈ ℝ ∧ if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ≤ 𝑐 ) ) )
41 36 40 syl ⊢ ( 𝜑 → ( 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ↔ ( 𝑐 ∈ ℝ ∧ if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ≤ 𝑐 ) ) )
42 41 simprbda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝑐 ∈ ℝ )
43 6 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝑇 ∈ ℝ )
44 43 34 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → ( 𝑇 + 1 ) ∈ ℝ )
45 43 ltp1d ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝑇 < ( 𝑇 + 1 ) )
46 41 simplbda ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ≤ 𝑐 )
47 4 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝐷 ∈ ℝ )
48 maxle ⊢ ( ( 𝐷 ∈ ℝ ∧ ( 𝑇 + 1 ) ∈ ℝ ∧ 𝑐 ∈ ℝ ) → ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ≤ 𝑐 ↔ ( 𝐷 ≤ 𝑐 ∧ ( 𝑇 + 1 ) ≤ 𝑐 ) ) )
49 47 44 42 48 syl3anc ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) ≤ 𝑐 ↔ ( 𝐷 ≤ 𝑐 ∧ ( 𝑇 + 1 ) ≤ 𝑐 ) ) )
50 46 49 mpbid ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → ( 𝐷 ≤ 𝑐 ∧ ( 𝑇 + 1 ) ≤ 𝑐 ) )
51 50 simprd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → ( 𝑇 + 1 ) ≤ 𝑐 )
52 43 44 42 45 51 ltletrd ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝑇 < 𝑐 )
53 24 adantr ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝑇 ∈ ℝ* )
54 elioopnf ⊢ ( 𝑇 ∈ ℝ* → ( 𝑐 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑐 ∈ ℝ ∧ 𝑇 < 𝑐 ) ) )
55 53 54 syl ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → ( 𝑐 ∈ ( 𝑇 (,) +∞ ) ↔ ( 𝑐 ∈ ℝ ∧ 𝑇 < 𝑐 ) ) )
56 42 52 55 mpbir2and ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝑐 ∈ ( 𝑇 (,) +∞ ) )
57 56 1 eleqtrrdi ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝑐 ∈ 𝑆 )
58 50 simpld ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → 𝐷 ≤ 𝑐 )
59 57 58 jca ⊢ ( ( 𝜑 ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) )
60 59 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) )
61 simprrl ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ) → 𝑐 ∈ 𝑆 )
62 61 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑐 ∈ 𝑆 )
63 16 62 sseldi ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑐 ∈ ℝ )
64 63 leidd ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑐 ≤ 𝑐 )
65 nfv ⊢ Ⅎ 𝑥 𝑐 ≤ 𝑐
66 nfcv ⊢ Ⅎ 𝑥 abs
67 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑐 / 𝑥 ⦌ 𝐵
68 66 67 nffv ⊢ Ⅎ 𝑥 ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 )
69 nfcv ⊢ Ⅎ 𝑥 <
70 nfcv ⊢ Ⅎ 𝑥 𝑒
71 68 69 70 nfbr ⊢ Ⅎ 𝑥 ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒
72 65 71 nfim ⊢ Ⅎ 𝑥 ( 𝑐 ≤ 𝑐 → ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒 )
73 breq2 ⊢ ( 𝑥 = 𝑐 → ( 𝑐 ≤ 𝑥 ↔ 𝑐 ≤ 𝑐 ) )
74 csbeq1a ⊢ ( 𝑥 = 𝑐 → 𝐵 = ⦋ 𝑐 / 𝑥 ⦌ 𝐵 )
75 74 fveq2d ⊢ ( 𝑥 = 𝑐 → ( abs ‘ 𝐵 ) = ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) )
76 75 breq1d ⊢ ( 𝑥 = 𝑐 → ( ( abs ‘ 𝐵 ) < 𝑒 ↔ ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒 ) )
77 73 76 imbi12d ⊢ ( 𝑥 = 𝑐 → ( ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) ↔ ( 𝑐 ≤ 𝑐 → ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒 ) ) )
78 72 77 rspc ⊢ ( 𝑐 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( 𝑐 ≤ 𝑐 → ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒 ) ) )
79 62 78 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( 𝑐 ≤ 𝑐 → ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒 ) ) )
80 64 79 mpid ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒 ) )
81 17 7 8 10 dvmptrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
82 81 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 ∈ ℝ )
83 1 2 3 4 5 6 7 8 9 10 11 12 13 14 dvfsumrlimge0 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 0 ≤ 𝐵 )
84 elrege0 ⊢ ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( 𝐵 ∈ ℝ ∧ 0 ≤ 𝐵 ) )
85 82 83 84 sylanbrc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 𝐵 ∈ ( 0 [,) +∞ ) )
86 85 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐷 ≤ 𝑥 → 𝐵 ∈ ( 0 [,) +∞ ) ) )
87 86 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝐷 ≤ 𝑥 → 𝐵 ∈ ( 0 [,) +∞ ) ) )
88 87 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ∀ 𝑥 ∈ 𝑆 ( 𝐷 ≤ 𝑥 → 𝐵 ∈ ( 0 [,) +∞ ) ) )
89 simprrr ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ) → 𝐷 ≤ 𝑐 )
90 89 adantrr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝐷 ≤ 𝑐 )
91 nfv ⊢ Ⅎ 𝑥 𝐷 ≤ 𝑐
92 67 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ )
93 91 92 nfim ⊢ Ⅎ 𝑥 ( 𝐷 ≤ 𝑐 → ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) )
94 breq2 ⊢ ( 𝑥 = 𝑐 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑐 ) )
95 74 eleq1d ⊢ ( 𝑥 = 𝑐 → ( 𝐵 ∈ ( 0 [,) +∞ ) ↔ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ) )
96 94 95 imbi12d ⊢ ( 𝑥 = 𝑐 → ( ( 𝐷 ≤ 𝑥 → 𝐵 ∈ ( 0 [,) +∞ ) ) ↔ ( 𝐷 ≤ 𝑐 → ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ) ) )
97 93 96 rspc ⊢ ( 𝑐 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( 𝐷 ≤ 𝑥 → 𝐵 ∈ ( 0 [,) +∞ ) ) → ( 𝐷 ≤ 𝑐 → ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ) ) )
98 62 88 90 97 syl3c ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) )
99 elrege0 ⊢ ( ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ( 0 [,) +∞ ) ↔ ( ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 0 ≤ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) )
100 98 99 sylib ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 0 ≤ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) )
101 absid ⊢ ( ( ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 0 ≤ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) → ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑐 / 𝑥 ⦌ 𝐵 )
102 100 101 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑐 / 𝑥 ⦌ 𝐵 )
103 102 breq1d ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒 ↔ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 < 𝑒 ) )
104 3 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑀 ∈ ℤ )
105 4 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝐷 ∈ ℝ )
106 5 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑀 ≤ ( 𝐷 + 1 ) )
107 6 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑇 ∈ ℝ )
108 7 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
109 8 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
110 9 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
111 10 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
112 pnfxr ⊢ +∞ ∈ ℝ*
113 112 a1i ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → +∞ ∈ ℝ* )
114 3simpa ⊢ ( ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞ ) → ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ) )
115 114 12 syl3an3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞ ) ) → 𝐶 ≤ 𝐵 )
116 115 3adant1r ⊢ ( ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ +∞ ) ) → 𝐶 ≤ 𝐵 )
117 83 3adantr3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) ) → 0 ≤ 𝐵 )
118 117 adantlr ⊢ ( ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ +∞ ) ) → 0 ≤ 𝐵 )
119 simprrl ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑦 ∈ 𝑆 )
120 simprrr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑐 ≤ 𝑦 )
121 16 23 sstri ⊢ 𝑆 ⊆ ℝ*
122 121 119 sseldi ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑦 ∈ ℝ* )
123 pnfge ⊢ ( 𝑦 ∈ ℝ* → 𝑦 ≤ +∞ )
124 122 123 syl ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑦 ≤ +∞ )
125 1 2 104 105 106 107 108 109 110 111 11 113 116 13 118 62 119 90 120 124 dvfsumlem4 ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) ≤ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 )
126 21 adantr ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝐺 : 𝑆 ⟶ ℂ )
127 126 119 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( 𝐺 ‘ 𝑦 ) ∈ ℂ )
128 126 62 ffvelrnd ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( 𝐺 ‘ 𝑐 ) ∈ ℂ )
129 127 128 subcld ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ∈ ℂ )
130 129 abscld ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) ∈ ℝ )
131 100 simpld ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ℝ )
132 simprll ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑒 ∈ ℝ+ )
133 132 rpred ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → 𝑒 ∈ ℝ )
134 lelttr ⊢ ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) ∈ ℝ ∧ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∈ ℝ ∧ 𝑒 ∈ ℝ ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) ≤ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∧ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 < 𝑒 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) )
135 130 131 133 134 syl3anc ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ( ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) ≤ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ∧ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 < 𝑒 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) )
136 125 135 mpand ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ⦋ 𝑐 / 𝑥 ⦌ 𝐵 < 𝑒 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) )
137 103 136 sylbid ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ( abs ‘ ⦋ 𝑐 / 𝑥 ⦌ 𝐵 ) < 𝑒 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) )
138 80 137 syld ⊢ ( ( 𝜑 ∧ ( ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) )
139 138 anassrs ⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ) ∧ ( 𝑦 ∈ 𝑆 ∧ 𝑐 ≤ 𝑦 ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) )
140 139 expr ⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ) ∧ 𝑦 ∈ 𝑆 ) → ( 𝑐 ≤ 𝑦 → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) )
141 140 com23 ⊢ ( ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ) ∧ 𝑦 ∈ 𝑆 ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) )
142 141 ralrimdva ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) )
143 142 61 jctild ⊢ ( ( 𝜑 ∧ ( 𝑒 ∈ ℝ+ ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( 𝑐 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) ) )
144 143 anassrs ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ ( 𝑐 ∈ 𝑆 ∧ 𝐷 ≤ 𝑐 ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( 𝑐 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) ) )
145 60 144 syldan ⊢ ( ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) ∧ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ) → ( ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ( 𝑐 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) ) )
146 145 expimpd ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ( 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ∧ ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) ) → ( 𝑐 ∈ 𝑆 ∧ ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) ) )
147 146 reximdv2 ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑐 ∈ ( if ( 𝐷 ≤ ( 𝑇 + 1 ) , ( 𝑇 + 1 ) , 𝐷 ) [,) +∞ ) ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ∃ 𝑐 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) )
148 39 147 sylbird ⊢ ( ( 𝜑 ∧ 𝑒 ∈ ℝ+ ) → ( ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ∃ 𝑐 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) )
149 148 ralimdva ⊢ ( 𝜑 → ( ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ ℝ ∀ 𝑥 ∈ 𝑆 ( 𝑐 ≤ 𝑥 → ( abs ‘ 𝐵 ) < 𝑒 ) → ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) ) )
150 32 149 mpd ⊢ ( 𝜑 → ∀ 𝑒 ∈ ℝ+ ∃ 𝑐 ∈ 𝑆 ∀ 𝑦 ∈ 𝑆 ( 𝑐 ≤ 𝑦 → ( abs ‘ ( ( 𝐺 ‘ 𝑦 ) − ( 𝐺 ‘ 𝑐 ) ) ) < 𝑒 ) )
151 17 21 28 150 caucvgr ⊢ ( 𝜑 → 𝐺 ∈ dom ⇝𝑟 )