This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem dvfsumlem4

Description: Lemma for dvfsumrlim . (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 ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
dvfsum.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
dvfsum.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 )
dvfsumlem4.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
dvfsumlem4.0 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈 ) ) → 0 ≤ 𝐵 )
dvfsumlem4.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dvfsumlem4.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
dvfsumlem4.3 ⊢ ( 𝜑 → 𝐷 ≤ 𝑋 )
dvfsumlem4.4 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
dvfsumlem4.5 ⊢ ( 𝜑 → 𝑌 ≤ 𝑈 )
Assertion dvfsumlem4 ( 𝜑 → ( 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 dvfsum.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
13 dvfsum.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ≤ 𝐵 )
14 dvfsumlem4.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
15 dvfsumlem4.0 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈 ) ) → 0 ≤ 𝐵 )
16 dvfsumlem4.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
17 dvfsumlem4.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
18 dvfsumlem4.3 ⊢ ( 𝜑 → 𝐷 ≤ 𝑋 )
19 dvfsumlem4.4 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
20 dvfsumlem4.5 ⊢ ( 𝜑 → 𝑌 ≤ 𝑈 )
21 fzfid ⊢ ( 𝜑 → ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) ∈ Fin )
22 9 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ )
23 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
24 23 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) → 𝑘 ∈ 𝑍 )
25 11 eleq1d ⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
26 25 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℝ )
27 22 24 26 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝐶 ∈ ℝ )
28 21 27 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 ∈ ℝ )
29 7 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ )
30 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐴
31 30 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ
32 csbeq1a ⊢ ( 𝑥 = 𝑌 → 𝐴 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
33 32 eleq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
34 31 33 rspc ⊢ ( 𝑌 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
35 17 29 34 sylc ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ )
36 28 35 resubcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ )
37 nfcv ⊢ Ⅎ 𝑥 𝑌
38 nfcv ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶
39 nfcv ⊢ Ⅎ 𝑥 −
40 38 39 30 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
41 fveq2 ⊢ ( 𝑥 = 𝑌 → ( ⌊ ‘ 𝑥 ) = ( ⌊ ‘ 𝑌 ) )
42 41 oveq2d ⊢ ( 𝑥 = 𝑌 → ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) = ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) )
43 42 sumeq1d ⊢ ( 𝑥 = 𝑌 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 )
44 43 32 oveq12d ⊢ ( 𝑥 = 𝑌 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
45 37 40 44 14 fvmptf ⊢ ( ( 𝑌 ∈ 𝑆 ∧ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑌 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
46 17 36 45 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
47 fzfid ⊢ ( 𝜑 → ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ∈ Fin )
48 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
49 48 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) → 𝑘 ∈ 𝑍 )
50 22 49 26 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐶 ∈ ℝ )
51 47 50 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ∈ ℝ )
52 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐴
53 52 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ
54 csbeq1a ⊢ ( 𝑥 = 𝑋 → 𝐴 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
55 54 eleq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
56 53 55 rspc ⊢ ( 𝑋 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
57 16 29 56 sylc ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ )
58 51 57 resubcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℝ )
59 nfcv ⊢ Ⅎ 𝑥 𝑋
60 nfcv ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶
61 60 39 52 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
62 fveq2 ⊢ ( 𝑥 = 𝑋 → ( ⌊ ‘ 𝑥 ) = ( ⌊ ‘ 𝑋 ) )
63 62 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) = ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) )
64 63 sumeq1d ⊢ ( 𝑥 = 𝑋 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 )
65 64 54 oveq12d ⊢ ( 𝑥 = 𝑋 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
66 59 61 65 14 fvmptf ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑋 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
67 16 58 66 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
68 46 67 oveq12d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
69 68 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) ) = ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) )
70 ioossre ⊢ ( 𝑇 (,) +∞ ) ⊆ ℝ
71 1 70 eqsstri ⊢ 𝑆 ⊆ ℝ
72 71 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
73 72 7 8 10 dvmptrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
74 73 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ )
75 nfv ⊢ Ⅎ 𝑚 𝐵 ∈ ℝ
76 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑚 / 𝑥 ⦌ 𝐵
77 76 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ
78 csbeq1a ⊢ ( 𝑥 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑥 ⦌ 𝐵 )
79 78 eleq1d ⊢ ( 𝑥 = 𝑚 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
80 75 77 79 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ ↔ ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ )
81 74 80 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ )
82 csbeq1 ⊢ ( 𝑚 = 𝑋 → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
83 82 eleq1d ⊢ ( 𝑚 = 𝑋 → ( ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
84 83 rspcv ⊢ ( 𝑋 ∈ 𝑆 → ( ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
85 16 81 84 sylc ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ )
86 58 85 resubcld ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
87 71 16 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
88 reflcl ⊢ ( 𝑋 ∈ ℝ → ( ⌊ ‘ 𝑋 ) ∈ ℝ )
89 87 88 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ∈ ℝ )
90 87 89 resubcld ⊢ ( 𝜑 → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ∈ ℝ )
91 90 85 remulcld ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
92 91 58 readdcld ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
93 92 85 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
94 fracge0 ⊢ ( 𝑋 ∈ ℝ → 0 ≤ ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) )
95 87 94 syl ⊢ ( 𝜑 → 0 ≤ ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) )
96 87 rexrd ⊢ ( 𝜑 → 𝑋 ∈ ℝ* )
97 71 17 sselid ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
98 97 rexrd ⊢ ( 𝜑 → 𝑌 ∈ ℝ* )
99 96 98 12 19 20 xrletrd ⊢ ( 𝜑 → 𝑋 ≤ 𝑈 )
100 16 18 99 3jca ⊢ ( 𝜑 → ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) )
101 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) ) → 𝑋 ∈ 𝑆 )
102 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) )
103 nfcv ⊢ Ⅎ 𝑥 0
104 nfcv ⊢ Ⅎ 𝑥 ≤
105 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐵
106 103 104 105 nfbr ⊢ Ⅎ 𝑥 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵
107 102 106 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) ) → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
108 eleq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ∈ 𝑆 ↔ 𝑋 ∈ 𝑆 ) )
109 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋 ) )
110 breq1 ⊢ ( 𝑥 = 𝑋 → ( 𝑥 ≤ 𝑈 ↔ 𝑋 ≤ 𝑈 ) )
111 108 109 110 3anbi123d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈 ) ↔ ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) ) )
112 111 anbi2d ⊢ ( 𝑥 = 𝑋 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) ) ) )
113 csbeq1a ⊢ ( 𝑥 = 𝑋 → 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
114 113 breq2d ⊢ ( 𝑥 = 𝑋 → ( 0 ≤ 𝐵 ↔ 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
115 112 114 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈 ) ) → 0 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) ) → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
116 107 115 15 vtoclg1f ⊢ ( 𝑋 ∈ 𝑆 → ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) ) → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
117 101 116 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑋 ∈ 𝑆 ∧ 𝐷 ≤ 𝑋 ∧ 𝑋 ≤ 𝑈 ) ) → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
118 100 117 mpdan ⊢ ( 𝜑 → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
119 90 85 95 118 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
120 58 91 addge02d ⊢ ( 𝜑 → ( 0 ≤ ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ↔ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) )
121 119 120 mpbid ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
122 58 92 85 121 lesub1dd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
123 reflcl ⊢ ( 𝑌 ∈ ℝ → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
124 97 123 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
125 97 124 resubcld ⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) ∈ ℝ )
126 csbeq1 ⊢ ( 𝑚 = 𝑌 → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
127 126 eleq1d ⊢ ( 𝑚 = 𝑌 → ( ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
128 127 rspcv ⊢ ( 𝑌 ∈ 𝑆 → ( ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
129 17 81 128 sylc ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℝ )
130 125 129 remulcld ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
131 130 36 readdcld ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
132 131 129 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
133 eqid ⊢ ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) )
134 1 2 3 4 5 6 7 8 9 10 11 12 13 133 16 17 18 19 20 dvfsumlem3 ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑌 ) ≤ ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑋 ) ∧ ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
135 134 simprd ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
136 nfcv ⊢ Ⅎ 𝑥 ( 𝑋 − ( ⌊ ‘ 𝑋 ) )
137 nfcv ⊢ Ⅎ 𝑥 ·
138 136 137 105 nfov ⊢ Ⅎ 𝑥 ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
139 nfcv ⊢ Ⅎ 𝑥 +
140 138 139 61 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
141 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
142 141 62 oveq12d ⊢ ( 𝑥 = 𝑋 → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) = ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) )
143 142 113 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) = ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
144 143 65 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
145 59 140 144 133 fvmptf ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑋 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
146 16 92 145 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑋 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
147 146 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
148 nfcv ⊢ Ⅎ 𝑥 ( 𝑌 − ( ⌊ ‘ 𝑌 ) )
149 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐵
150 148 137 149 nfov ⊢ Ⅎ 𝑥 ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
151 150 139 40 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
152 id ⊢ ( 𝑥 = 𝑌 → 𝑥 = 𝑌 )
153 152 41 oveq12d ⊢ ( 𝑥 = 𝑌 → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) = ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) )
154 csbeq1a ⊢ ( 𝑥 = 𝑌 → 𝐵 = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
155 153 154 oveq12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) = ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
156 155 44 oveq12d ⊢ ( 𝑥 = 𝑌 → ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
157 37 151 156 133 fvmptf ⊢ ( ( 𝑌 ∈ 𝑆 ∧ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑌 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
158 17 131 157 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑌 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
159 158 oveq1d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
160 135 147 159 3brtr3d ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
161 36 recnd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
162 129 recnd ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ∈ ℂ )
163 130 recnd ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
164 161 162 163 subsub3d ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 − ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ) = ( ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
165 161 163 addcomd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
166 165 oveq1d ⊢ ( 𝜑 → ( ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
167 164 166 eqtrd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 − ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ) = ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
168 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
169 4 87 97 18 19 letrd ⊢ ( 𝜑 → 𝐷 ≤ 𝑌 )
170 17 169 20 3jca ⊢ ( 𝜑 → ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) )
171 simpr1 ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → 𝑌 ∈ 𝑆 )
172 nfv ⊢ Ⅎ 𝑥 ( 𝜑 ∧ ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) )
173 103 104 149 nfbr ⊢ Ⅎ 𝑥 0 ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵
174 172 173 nfim ⊢ Ⅎ 𝑥 ( ( 𝜑 ∧ ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → 0 ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
175 eleq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ∈ 𝑆 ↔ 𝑌 ∈ 𝑆 ) )
176 breq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑌 ) )
177 breq1 ⊢ ( 𝑥 = 𝑌 → ( 𝑥 ≤ 𝑈 ↔ 𝑌 ≤ 𝑈 ) )
178 175 176 177 3anbi123d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈 ) ↔ ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) )
179 178 anbi2d ⊢ ( 𝑥 = 𝑌 → ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈 ) ) ↔ ( 𝜑 ∧ ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) ) )
180 154 breq2d ⊢ ( 𝑥 = 𝑌 → ( 0 ≤ 𝐵 ↔ 0 ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
181 179 180 imbi12d ⊢ ( 𝑥 = 𝑌 → ( ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑈 ) ) → 0 ≤ 𝐵 ) ↔ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → 0 ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
182 174 181 15 vtoclg1f ⊢ ( 𝑌 ∈ 𝑆 → ( ( 𝜑 ∧ ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → 0 ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
183 171 182 mpcom ⊢ ( ( 𝜑 ∧ ( 𝑌 ∈ 𝑆 ∧ 𝐷 ≤ 𝑌 ∧ 𝑌 ≤ 𝑈 ) ) → 0 ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
184 170 183 mpdan ⊢ ( 𝜑 → 0 ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
185 fracle1 ⊢ ( 𝑌 ∈ ℝ → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) ≤ 1 )
186 97 185 syl ⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) ≤ 1 )
187 125 168 129 184 186 lemul1ad ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
188 162 mullidd ⊢ ( 𝜑 → ( 1 · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
189 187 188 breqtrd ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 )
190 129 130 subge0d ⊢ ( 𝜑 → ( 0 ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 − ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ↔ ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
191 189 190 mpbird ⊢ ( 𝜑 → 0 ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 − ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) )
192 129 130 resubcld ⊢ ( 𝜑 → ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 − ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ∈ ℝ )
193 36 192 subge02d ⊢ ( 𝜑 → ( 0 ≤ ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 − ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ↔ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 − ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
194 191 193 mpbid ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( ⦋ 𝑌 / 𝑥 ⦌ 𝐵 − ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ) ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
195 167 194 eqbrtrrd ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
196 93 132 36 160 195 letrd ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
197 86 93 36 122 196 letrd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
198 85 58 readdcld ⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
199 fracge0 ⊢ ( 𝑌 ∈ ℝ → 0 ≤ ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) )
200 97 199 syl ⊢ ( 𝜑 → 0 ≤ ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) )
201 125 129 200 184 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) )
202 36 130 addge02d ⊢ ( 𝜑 → ( 0 ≤ ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) ↔ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) )
203 201 202 mpbid ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
204 134 simpld ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑌 ) ≤ ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) ) ) ‘ 𝑋 ) )
205 204 158 146 3brtr3d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · ⦋ 𝑌 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
206 36 131 92 203 205 letrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
207 fracle1 ⊢ ( 𝑋 ∈ ℝ → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 )
208 87 207 syl ⊢ ( 𝜑 → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 )
209 90 168 85 118 208 lemul1ad ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
210 85 recnd ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ )
211 210 mullidd ⊢ ( 𝜑 → ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
212 209 211 breqtrd ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
213 91 85 58 212 leadd1dd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ≤ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
214 36 92 198 206 213 letrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
215 58 recnd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
216 210 215 addcomd ⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) = ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
217 214 216 breqtrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
218 36 58 85 absdifled ⊢ ( 𝜑 → ( ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ↔ ( ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∧ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) + ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) ) )
219 197 217 218 mpbir2and ⊢ ( 𝜑 → ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
220 69 219 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )