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 ‘ ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) ) ≤ 𝐸 )