Metamath Proof Explorer

Theorem dvfsum2

Description: The reverse of dvfsumrlim , when comparing a finite sum of increasing terms to an integral. In this case there is no point in stating the limit properties, because the terms of the sum aren't approaching zero, but there is nevertheless still a natural asymptotic statement that can be made. (Contributed by Mario Carneiro, 20-May-2016)

Ref Expression
Hypotheses dvfsum2.s ⊢ 𝑆 = ( 𝑇 (,) +∞ )
dvfsum2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
dvfsum2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
dvfsum2.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
dvfsum2.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
dvfsum2.md ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
dvfsum2.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
dvfsum2.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
dvfsum2.b1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
dvfsum2.b2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
dvfsum2.b3 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
dvfsum2.c ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
dvfsum2.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐵 ≤ 𝐶 )
dvfsum2.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
dvfsum2.0 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 0 ≤ 𝐵 )
dvfsum2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
dvfsum2.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
dvfsum2.3 ⊢ ( 𝜑 → 𝐷 ≤ 𝑋 )
dvfsum2.4 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
dvfsum2.5 ⊢ ( 𝜑 → 𝑌 ≤ 𝑈 )
dvfsum2.e ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐸 )
Assertion dvfsum2 ( 𝜑 → ( abs ‘ ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) ) ≤ 𝐸 )

Proof

Step Hyp Ref Expression
1 dvfsum2.s ⊢ 𝑆 = ( 𝑇 (,) +∞ )
2 dvfsum2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 dvfsum2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
4 dvfsum2.d ⊢ ( 𝜑 → 𝐷 ∈ ℝ )
5 dvfsum2.u ⊢ ( 𝜑 → 𝑈 ∈ ℝ* )
6 dvfsum2.md ⊢ ( 𝜑 → 𝑀 ≤ ( 𝐷 + 1 ) )
7 dvfsum2.t ⊢ ( 𝜑 → 𝑇 ∈ ℝ )
8 dvfsum2.a ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℝ )
9 dvfsum2.b1 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ 𝑉 )
10 dvfsum2.b2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → 𝐵 ∈ ℝ )
11 dvfsum2.b3 ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ 𝐵 ) )
12 dvfsum2.c ⊢ ( 𝑥 = 𝑘 → 𝐵 = 𝐶 )
13 dvfsum2.l ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐵 ≤ 𝐶 )
14 dvfsum2.g ⊢ 𝐺 = ( 𝑥 ∈ 𝑆 ↦ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) )
15 dvfsum2.0 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝐷 ≤ 𝑥 ) ) → 0 ≤ 𝐵 )
16 dvfsum2.1 ⊢ ( 𝜑 → 𝑋 ∈ 𝑆 )
17 dvfsum2.2 ⊢ ( 𝜑 → 𝑌 ∈ 𝑆 )
18 dvfsum2.3 ⊢ ( 𝜑 → 𝐷 ≤ 𝑋 )
19 dvfsum2.4 ⊢ ( 𝜑 → 𝑋 ≤ 𝑌 )
20 dvfsum2.5 ⊢ ( 𝜑 → 𝑌 ≤ 𝑈 )
21 dvfsum2.e ⊢ ( 𝑥 = 𝑌 → 𝐵 = 𝐸 )
22 fzfid ⊢ ( 𝜑 → ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) ∈ Fin )
23 10 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ )
24 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
25 24 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) → 𝑘 ∈ 𝑍 )
26 12 eleq1d ⊢ ( 𝑥 = 𝑘 → ( 𝐵 ∈ ℝ ↔ 𝐶 ∈ ℝ ) )
27 26 rspccva ⊢ ( ( ∀ 𝑥 ∈ 𝑍 𝐵 ∈ ℝ ∧ 𝑘 ∈ 𝑍 ) → 𝐶 ∈ ℝ )
28 23 25 27 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝐶 ∈ ℝ )
29 22 28 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 ∈ ℝ )
30 8 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ )
31 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐴
32 31 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ
33 csbeq1a ⊢ ( 𝑥 = 𝑌 → 𝐴 = ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
34 33 eleq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
35 32 34 rspc ⊢ ( 𝑌 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
36 17 30 35 sylc ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℝ )
37 29 36 resubcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ )
38 nfcv ⊢ Ⅎ 𝑥 𝑌
39 nfcv ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶
40 nfcv ⊢ Ⅎ 𝑥 −
41 39 40 31 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
42 fveq2 ⊢ ( 𝑥 = 𝑌 → ( ⌊ ‘ 𝑥 ) = ( ⌊ ‘ 𝑌 ) )
43 42 oveq2d ⊢ ( 𝑥 = 𝑌 → ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) = ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) )
44 43 sumeq1d ⊢ ( 𝑥 = 𝑌 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 )
45 44 33 oveq12d ⊢ ( 𝑥 = 𝑌 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
46 38 41 45 14 fvmptf ⊢ ( ( 𝑌 ∈ 𝑆 ∧ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑌 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
47 17 37 46 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑌 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
48 fzfid ⊢ ( 𝜑 → ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ∈ Fin )
49 elfzuz ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) → 𝑘 ∈ ( ℤ≥ ‘ 𝑀 ) )
50 49 2 eleqtrrdi ⊢ ( 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) → 𝑘 ∈ 𝑍 )
51 23 50 27 syl2an ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐶 ∈ ℝ )
52 48 51 fsumrecl ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ∈ ℝ )
53 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐴
54 53 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ
55 csbeq1a ⊢ ( 𝑥 = 𝑋 → 𝐴 = ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
56 55 eleq1d ⊢ ( 𝑥 = 𝑋 → ( 𝐴 ∈ ℝ ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
57 54 56 rspc ⊢ ( 𝑋 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐴 ∈ ℝ → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ ) )
58 16 30 57 sylc ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℝ )
59 52 58 resubcld ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℝ )
60 nfcv ⊢ Ⅎ 𝑥 𝑋
61 nfcv ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶
62 61 40 53 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
63 fveq2 ⊢ ( 𝑥 = 𝑋 → ( ⌊ ‘ 𝑥 ) = ( ⌊ ‘ 𝑋 ) )
64 63 oveq2d ⊢ ( 𝑥 = 𝑋 → ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) = ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) )
65 64 sumeq1d ⊢ ( 𝑥 = 𝑋 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 )
66 65 55 oveq12d ⊢ ( 𝑥 = 𝑋 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) 𝐶 − 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
67 60 62 66 14 fvmptf ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℝ ) → ( 𝐺 ‘ 𝑋 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
68 16 59 67 syl2anc ⊢ ( 𝜑 → ( 𝐺 ‘ 𝑋 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
69 47 68 oveq12d ⊢ ( 𝜑 → ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) = ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
70 69 fveq2d ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) ) = ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) )
71 37 recnd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
72 59 recnd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∈ ℂ )
73 71 72 abssubd ⊢ ( 𝜑 → ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) = ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) )
74 70 73 eqtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) ) = ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) )
75 ioossre ⊢ ( 𝑇 (,) +∞ ) ⊆ ℝ
76 1 75 eqsstri ⊢ 𝑆 ⊆ ℝ
77 76 a1i ⊢ ( 𝜑 → 𝑆 ⊆ ℝ )
78 77 8 9 11 dvmptrecl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐵 ∈ ℝ )
79 78 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ )
80 21 eleq1d ⊢ ( 𝑥 = 𝑌 → ( 𝐵 ∈ ℝ ↔ 𝐸 ∈ ℝ ) )
81 80 rspcv ⊢ ( 𝑌 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐸 ∈ ℝ ) )
82 17 79 81 sylc ⊢ ( 𝜑 → 𝐸 ∈ ℝ )
83 37 82 resubcld ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − 𝐸 ) ∈ ℝ )
84 76 16 sselid ⊢ ( 𝜑 → 𝑋 ∈ ℝ )
85 reflcl ⊢ ( 𝑋 ∈ ℝ → ( ⌊ ‘ 𝑋 ) ∈ ℝ )
86 84 85 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑋 ) ∈ ℝ )
87 84 86 resubcld ⊢ ( 𝜑 → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ∈ ℝ )
88 nfv ⊢ Ⅎ 𝑚 𝐵 ∈ ℝ
89 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑚 / 𝑥 ⦌ 𝐵
90 89 nfel1 ⊢ Ⅎ 𝑥 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ
91 csbeq1a ⊢ ( 𝑥 = 𝑚 → 𝐵 = ⦋ 𝑚 / 𝑥 ⦌ 𝐵 )
92 91 eleq1d ⊢ ( 𝑥 = 𝑚 → ( 𝐵 ∈ ℝ ↔ ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
93 88 90 92 cbvralw ⊢ ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ ↔ ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ )
94 79 93 sylib ⊢ ( 𝜑 → ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ )
95 csbeq1 ⊢ ( 𝑚 = 𝑋 → ⦋ 𝑚 / 𝑥 ⦌ 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
96 95 eleq1d ⊢ ( 𝑚 = 𝑋 → ( ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ ↔ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
97 96 rspcv ⊢ ( 𝑋 ∈ 𝑆 → ( ∀ 𝑚 ∈ 𝑆 ⦋ 𝑚 / 𝑥 ⦌ 𝐵 ∈ ℝ → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ ) )
98 16 94 97 sylc ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℝ )
99 87 98 remulcld ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
100 99 59 readdcld ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
101 100 98 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℝ )
102 76 17 sselid ⊢ ( 𝜑 → 𝑌 ∈ ℝ )
103 reflcl ⊢ ( 𝑌 ∈ ℝ → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
104 102 103 syl ⊢ ( 𝜑 → ( ⌊ ‘ 𝑌 ) ∈ ℝ )
105 102 104 resubcld ⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) ∈ ℝ )
106 105 82 remulcld ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) ∈ ℝ )
107 106 37 readdcld ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
108 107 82 resubcld ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − 𝐸 ) ∈ ℝ )
109 fracge0 ⊢ ( 𝑌 ∈ ℝ → 0 ≤ ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) )
110 102 109 syl ⊢ ( 𝜑 → 0 ≤ ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) )
111 15 expr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → ( 𝐷 ≤ 𝑥 → 0 ≤ 𝐵 ) )
112 111 ralrimiva ⊢ ( 𝜑 → ∀ 𝑥 ∈ 𝑆 ( 𝐷 ≤ 𝑥 → 0 ≤ 𝐵 ) )
113 4 84 102 18 19 letrd ⊢ ( 𝜑 → 𝐷 ≤ 𝑌 )
114 breq2 ⊢ ( 𝑥 = 𝑌 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑌 ) )
115 21 breq2d ⊢ ( 𝑥 = 𝑌 → ( 0 ≤ 𝐵 ↔ 0 ≤ 𝐸 ) )
116 114 115 imbi12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝐷 ≤ 𝑥 → 0 ≤ 𝐵 ) ↔ ( 𝐷 ≤ 𝑌 → 0 ≤ 𝐸 ) ) )
117 116 rspcv ⊢ ( 𝑌 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( 𝐷 ≤ 𝑥 → 0 ≤ 𝐵 ) → ( 𝐷 ≤ 𝑌 → 0 ≤ 𝐸 ) ) )
118 17 112 113 117 syl3c ⊢ ( 𝜑 → 0 ≤ 𝐸 )
119 105 82 110 118 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) )
120 37 106 addge02d ⊢ ( 𝜑 → ( 0 ≤ ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) ↔ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) )
121 119 120 mpbid ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
122 37 107 82 121 lesub1dd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − 𝐸 ) ≤ ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − 𝐸 ) )
123 8 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → - 𝐴 ∈ ℝ )
124 78 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → - 𝐵 ∈ ℝ )
125 10 renegcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑍 ) → - 𝐵 ∈ ℝ )
126 reelprrecn ⊢ ℝ ∈ { ℝ , ℂ }
127 126 a1i ⊢ ( 𝜑 → ℝ ∈ { ℝ , ℂ } )
128 8 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝑆 ) → 𝐴 ∈ ℂ )
129 127 128 9 11 dvmptneg ⊢ ( 𝜑 → ( ℝ D ( 𝑥 ∈ 𝑆 ↦ - 𝐴 ) ) = ( 𝑥 ∈ 𝑆 ↦ - 𝐵 ) )
130 12 negeqd ⊢ ( 𝑥 = 𝑘 → - 𝐵 = - 𝐶 )
131 78 adantrr ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ) → 𝐵 ∈ ℝ )
132 131 3adant3 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐵 ∈ ℝ )
133 simp2r ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝑘 ∈ 𝑆 )
134 79 3ad2ant1 ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ )
135 26 rspcv ⊢ ( 𝑘 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 𝐵 ∈ ℝ → 𝐶 ∈ ℝ ) )
136 133 134 135 sylc ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → 𝐶 ∈ ℝ )
137 132 136 lenegd ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → ( 𝐵 ≤ 𝐶 ↔ - 𝐶 ≤ - 𝐵 ) )
138 13 137 mpbid ⊢ ( ( 𝜑 ∧ ( 𝑥 ∈ 𝑆 ∧ 𝑘 ∈ 𝑆 ) ∧ ( 𝐷 ≤ 𝑥 ∧ 𝑥 ≤ 𝑘 ∧ 𝑘 ≤ 𝑈 ) ) → - 𝐶 ≤ - 𝐵 )
139 eqid ⊢ ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) = ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) )
140 1 2 3 4 6 7 123 124 125 129 130 5 138 139 16 17 18 19 20 dvfsumlem3 ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑌 ) ≤ ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑋 ) ∧ ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ - 𝐵 ) ≤ ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ - 𝐵 ) ) )
141 140 simprd ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ - 𝐵 ) ≤ ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ - 𝐵 ) )
142 87 recnd ⊢ ( 𝜑 → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ∈ ℂ )
143 98 recnd ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ∈ ℂ )
144 142 143 mulneg2d ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = - ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
145 52 recnd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ∈ ℂ )
146 58 recnd ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ∈ ℂ )
147 145 146 neg2subd ⊢ ( 𝜑 → ( - Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐴 − Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )
148 51 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) ) → 𝐶 ∈ ℂ )
149 48 148 fsumneg ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 = - Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 )
150 149 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) = ( - Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
151 145 146 negsubdi2d ⊢ ( 𝜑 → - ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐴 − Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 ) )
152 147 150 151 3eqtr4d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) = - ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
153 144 152 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) = ( - ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + - ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
154 99 recnd ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ∈ ℂ )
155 154 72 negdid ⊢ ( 𝜑 → - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) = ( - ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + - ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
156 153 155 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) = - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
157 100 renegcld ⊢ ( 𝜑 → - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
158 156 157 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
159 nfcv ⊢ Ⅎ 𝑥 ( 𝑋 − ( ⌊ ‘ 𝑋 ) )
160 nfcv ⊢ Ⅎ 𝑥 ·
161 nfcsb1v ⊢ Ⅎ 𝑥 ⦋ 𝑋 / 𝑥 ⦌ 𝐵
162 161 nfneg ⊢ Ⅎ 𝑥 - ⦋ 𝑋 / 𝑥 ⦌ 𝐵
163 159 160 162 nfov ⊢ Ⅎ 𝑥 ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
164 nfcv ⊢ Ⅎ 𝑥 +
165 nfcv ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶
166 53 nfneg ⊢ Ⅎ 𝑥 - ⦋ 𝑋 / 𝑥 ⦌ 𝐴
167 165 40 166 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
168 163 164 167 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
169 id ⊢ ( 𝑥 = 𝑋 → 𝑥 = 𝑋 )
170 169 63 oveq12d ⊢ ( 𝑥 = 𝑋 → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) = ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) )
171 csbeq1a ⊢ ( 𝑥 = 𝑋 → 𝐵 = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
172 171 negeqd ⊢ ( 𝑥 = 𝑋 → - 𝐵 = - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
173 170 172 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) = ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
174 64 sumeq1d ⊢ ( 𝑥 = 𝑋 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 )
175 55 negeqd ⊢ ( 𝑥 = 𝑋 → - 𝐴 = - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 )
176 174 175 oveq12d ⊢ ( 𝑥 = 𝑋 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
177 173 176 oveq12d ⊢ ( 𝑥 = 𝑋 → ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
178 60 168 177 139 fvmptf ⊢ ( ( 𝑋 ∈ 𝑆 ∧ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑋 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
179 16 158 178 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑋 ) = ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) - 𝐶 − - ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
180 179 156 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑋 ) = - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
181 csbnegg ⊢ ( 𝑋 ∈ 𝑆 → ⦋ 𝑋 / 𝑥 ⦌ - 𝐵 = - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
182 16 181 syl ⊢ ( 𝜑 → ⦋ 𝑋 / 𝑥 ⦌ - 𝐵 = - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
183 180 182 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑋 ) − ⦋ 𝑋 / 𝑥 ⦌ - 𝐵 ) = ( - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
184 105 recnd ⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) ∈ ℂ )
185 82 recnd ⊢ ( 𝜑 → 𝐸 ∈ ℂ )
186 184 185 mulneg2d ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) = - ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) )
187 29 recnd ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 ∈ ℂ )
188 36 recnd ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ∈ ℂ )
189 187 188 neg2subd ⊢ ( 𝜑 → ( - Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 ) )
190 28 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) ) → 𝐶 ∈ ℂ )
191 22 190 fsumneg ⊢ ( 𝜑 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 = - Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 )
192 191 oveq1d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( - Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
193 187 188 negsubdi2d ⊢ ( 𝜑 → - ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = ( ⦋ 𝑌 / 𝑥 ⦌ 𝐴 − Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 ) )
194 189 192 193 3eqtr4d ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) = - ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
195 186 194 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( - ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + - ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
196 106 recnd ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) ∈ ℂ )
197 196 71 negdid ⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( - ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + - ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
198 195 197 eqtr4d ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
199 107 renegcld ⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
200 198 199 eqeltrd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ )
201 nfcv ⊢ Ⅎ 𝑥 ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 )
202 nfcv ⊢ Ⅎ 𝑥 Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶
203 31 nfneg ⊢ Ⅎ 𝑥 - ⦋ 𝑌 / 𝑥 ⦌ 𝐴
204 202 40 203 nfov ⊢ Ⅎ 𝑥 ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
205 201 164 204 nfov ⊢ Ⅎ 𝑥 ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
206 id ⊢ ( 𝑥 = 𝑌 → 𝑥 = 𝑌 )
207 206 42 oveq12d ⊢ ( 𝑥 = 𝑌 → ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) = ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) )
208 21 negeqd ⊢ ( 𝑥 = 𝑌 → - 𝐵 = - 𝐸 )
209 207 208 oveq12d ⊢ ( 𝑥 = 𝑌 → ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) = ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) )
210 43 sumeq1d ⊢ ( 𝑥 = 𝑌 → Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 = Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 )
211 33 negeqd ⊢ ( 𝑥 = 𝑌 → - 𝐴 = - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 )
212 210 211 oveq12d ⊢ ( 𝑥 = 𝑌 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) = ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) )
213 209 212 oveq12d ⊢ ( 𝑥 = 𝑌 → ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
214 38 205 213 139 fvmptf ⊢ ( ( 𝑌 ∈ 𝑆 ∧ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ ℝ ) → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑌 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
215 17 200 214 syl2anc ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑌 ) = ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · - 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) - 𝐶 − - ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
216 215 198 eqtrd ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑌 ) = - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
217 208 adantl ⊢ ( ( 𝜑 ∧ 𝑥 = 𝑌 ) → - 𝐵 = - 𝐸 )
218 17 217 csbied ⊢ ( 𝜑 → ⦋ 𝑌 / 𝑥 ⦌ - 𝐵 = - 𝐸 )
219 216 218 oveq12d ⊢ ( 𝜑 → ( ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑌 ) − ⦋ 𝑌 / 𝑥 ⦌ - 𝐵 ) = ( - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − - 𝐸 ) )
220 141 183 219 3brtr3d ⊢ ( 𝜑 → ( - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − - 𝐸 ) )
221 100 recnd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ∈ ℂ )
222 221 143 neg2subd ⊢ ( 𝜑 → ( - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − - ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) )
223 107 recnd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ∈ ℂ )
224 223 185 neg2subd ⊢ ( 𝜑 → ( - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − - 𝐸 ) = ( 𝐸 − ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) )
225 220 222 224 3brtr3d ⊢ ( 𝜑 → ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) ≤ ( 𝐸 − ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) )
226 221 143 negsubdi2d ⊢ ( 𝜑 → - ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 − ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) )
227 223 185 negsubdi2d ⊢ ( 𝜑 → - ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − 𝐸 ) = ( 𝐸 − ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) )
228 225 226 227 3brtr4d ⊢ ( 𝜑 → - ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ - ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − 𝐸 ) )
229 108 101 lenegd ⊢ ( 𝜑 → ( ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − 𝐸 ) ≤ ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ↔ - ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ - ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − 𝐸 ) ) )
230 228 229 mpbird ⊢ ( 𝜑 → ( ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) − 𝐸 ) ≤ ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
231 83 108 101 122 230 letrd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − 𝐸 ) ≤ ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
232 1red ⊢ ( 𝜑 → 1 ∈ ℝ )
233 nfv ⊢ Ⅎ 𝑥 𝐷 ≤ 𝑋
234 nfcv ⊢ Ⅎ 𝑥 0
235 nfcv ⊢ Ⅎ 𝑥 ≤
236 234 235 161 nfbr ⊢ Ⅎ 𝑥 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵
237 233 236 nfim ⊢ Ⅎ 𝑥 ( 𝐷 ≤ 𝑋 → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
238 breq2 ⊢ ( 𝑥 = 𝑋 → ( 𝐷 ≤ 𝑥 ↔ 𝐷 ≤ 𝑋 ) )
239 171 breq2d ⊢ ( 𝑥 = 𝑋 → ( 0 ≤ 𝐵 ↔ 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
240 238 239 imbi12d ⊢ ( 𝑥 = 𝑋 → ( ( 𝐷 ≤ 𝑥 → 0 ≤ 𝐵 ) ↔ ( 𝐷 ≤ 𝑋 → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
241 237 240 rspc ⊢ ( 𝑋 ∈ 𝑆 → ( ∀ 𝑥 ∈ 𝑆 ( 𝐷 ≤ 𝑥 → 0 ≤ 𝐵 ) → ( 𝐷 ≤ 𝑋 → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ) )
242 16 112 18 241 syl3c ⊢ ( 𝜑 → 0 ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
243 fracle1 ⊢ ( 𝑋 ∈ ℝ → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 )
244 84 243 syl ⊢ ( 𝜑 → ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) ≤ 1 )
245 87 232 98 242 244 lemul1ad ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
246 143 mullidd ⊢ ( 𝜑 → ( 1 · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) = ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
247 245 246 breqtrd ⊢ ( 𝜑 → ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )
248 99 98 59 247 leadd1dd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ≤ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
249 100 98 59 lesubadd2d ⊢ ( 𝜑 → ( ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ↔ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ≤ ( ⦋ 𝑋 / 𝑥 ⦌ 𝐵 + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) )
250 248 249 mpbird ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) − ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
251 83 101 59 231 250 letrd ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − 𝐸 ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) )
252 37 82 readdcld ⊢ ( 𝜑 → ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + 𝐸 ) ∈ ℝ )
253 fracge0 ⊢ ( 𝑋 ∈ ℝ → 0 ≤ ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) )
254 84 253 syl ⊢ ( 𝜑 → 0 ≤ ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) )
255 87 98 254 242 mulge0d ⊢ ( 𝜑 → 0 ≤ ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) )
256 59 99 addge02d ⊢ ( 𝜑 → ( 0 ≤ ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) ↔ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) )
257 255 256 mpbid ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
258 140 simpld ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑌 ) ≤ ( ( 𝑥 ∈ 𝑆 ↦ ( ( ( 𝑥 − ( ⌊ ‘ 𝑥 ) ) · - 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑥 ) ) - 𝐶 − - 𝐴 ) ) ) ‘ 𝑋 ) )
259 258 216 180 3brtr3d ⊢ ( 𝜑 → - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ≤ - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) )
260 100 107 lenegd ⊢ ( 𝜑 → ( ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ↔ - ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ≤ - ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ) )
261 259 260 mpbird ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ≤ ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
262 fracle1 ⊢ ( 𝑌 ∈ ℝ → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) ≤ 1 )
263 102 262 syl ⊢ ( 𝜑 → ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) ≤ 1 )
264 105 232 82 118 263 lemul1ad ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) ≤ ( 1 · 𝐸 ) )
265 185 mullidd ⊢ ( 𝜑 → ( 1 · 𝐸 ) = 𝐸 )
266 264 265 breqtrd ⊢ ( 𝜑 → ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) ≤ 𝐸 )
267 106 82 37 266 leadd1dd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ≤ ( 𝐸 + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) )
268 185 71 addcomd ⊢ ( 𝜑 → ( 𝐸 + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) = ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + 𝐸 ) )
269 267 268 breqtrd ⊢ ( 𝜑 → ( ( ( 𝑌 − ( ⌊ ‘ 𝑌 ) ) · 𝐸 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ≤ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + 𝐸 ) )
270 100 107 252 261 269 letrd ⊢ ( 𝜑 → ( ( ( 𝑋 − ( ⌊ ‘ 𝑋 ) ) · ⦋ 𝑋 / 𝑥 ⦌ 𝐵 ) + ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ) ≤ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + 𝐸 ) )
271 59 100 252 257 270 letrd ⊢ ( 𝜑 → ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + 𝐸 ) )
272 59 37 82 absdifled ⊢ ( 𝜑 → ( ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) ≤ 𝐸 ↔ ( ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) − 𝐸 ) ≤ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ∧ ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) ≤ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) + 𝐸 ) ) ) )
273 251 271 272 mpbir2and ⊢ ( 𝜑 → ( abs ‘ ( ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑋 ) ) 𝐶 − ⦋ 𝑋 / 𝑥 ⦌ 𝐴 ) − ( Σ 𝑘 ∈ ( 𝑀 ... ( ⌊ ‘ 𝑌 ) ) 𝐶 − ⦋ 𝑌 / 𝑥 ⦌ 𝐴 ) ) ) ≤ 𝐸 )
274 74 273 eqbrtrd ⊢ ( 𝜑 → ( abs ‘ ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) ) ≤ 𝐸 )