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 ‘ ( ( 𝐺 ‘ 𝑌 ) − ( 𝐺 ‘ 𝑋 ) ) ) ≤ ⦋ 𝑋 / 𝑥 ⦌ 𝐵 )