Theorem dvfsumlem4

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 18-May-2016)

	Ref	Expression
Hypotheses	dvfsum.s	$$⊢S=\left(T,\mathrm{+\infty }\right)$$
	dvfsum.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	dvfsum.m	$$⊢\phi \to M\in \mathbb{Z}$$
	dvfsum.d	$$⊢\phi \to D\in ℝ$$
	dvfsum.md	$$⊢\phi \to M\le D+1$$
	dvfsum.t	$$⊢\phi \to T\in ℝ$$
	dvfsum.a	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℝ$$
	dvfsum.b1	$$⊢\left(\phi \wedge x\in S\right)\to B\in V$$
	dvfsum.b2	$$⊢\left(\phi \wedge x\in Z\right)\to B\in ℝ$$
	dvfsum.b3	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\left(x\in S⟼B\right)$$
	dvfsum.c	$$⊢x=k\to B=C$$
	dvfsum.u	$$⊢\phi \to U\in {ℝ}^{*}$$
	dvfsum.l	$$⊢\left(\phi \wedge \left(x\in S\wedge k\in S\right)\wedge \left(D\le x\wedge x\le k\wedge k\le U\right)\right)\to C\le B$$
	dvfsumlem4.g	$$⊢G=\left(x\in S⟼\sum _{k=M}^{⌊x⌋}C-A\right)$$
	dvfsumlem4.0	$$⊢\left(\phi \wedge \left(x\in S\wedge D\le x\wedge x\le U\right)\right)\to 0\le B$$
	dvfsumlem4.1	$$⊢\phi \to X\in S$$
	dvfsumlem4.2	$$⊢\phi \to Y\in S$$
	dvfsumlem4.3	$$⊢\phi \to D\le X$$
	dvfsumlem4.4	$$⊢\phi \to X\le Y$$
	dvfsumlem4.5	$$⊢\phi \to Y\le U$$
Assertion	dvfsumlem4	$$⊢\phi \to \left|G\left(Y\right)-G\left(X\right)\right|\le ⦋X/x⦌B$$

Proof

Step	Hyp	Ref	Expression
1		dvfsum.s	$$⊢S=\left(T,\mathrm{+\infty }\right)$$
2		dvfsum.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		dvfsum.m	$$⊢\phi \to M\in \mathbb{Z}$$
4		dvfsum.d	$$⊢\phi \to D\in ℝ$$
5		dvfsum.md	$$⊢\phi \to M\le D+1$$
6		dvfsum.t	$$⊢\phi \to T\in ℝ$$
7		dvfsum.a	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℝ$$
8		dvfsum.b1	$$⊢\left(\phi \wedge x\in S\right)\to B\in V$$
9		dvfsum.b2	$$⊢\left(\phi \wedge x\in Z\right)\to B\in ℝ$$
10		dvfsum.b3	$$⊢\phi \to \frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\left(x\in S⟼B\right)$$
11		dvfsum.c	$$⊢x=k\to B=C$$
12		dvfsum.u	$$⊢\phi \to U\in {ℝ}^{*}$$
13		dvfsum.l	$$⊢\left(\phi \wedge \left(x\in S\wedge k\in S\right)\wedge \left(D\le x\wedge x\le k\wedge k\le U\right)\right)\to C\le B$$
14		dvfsumlem4.g	$$⊢G=\left(x\in S⟼\sum _{k=M}^{⌊x⌋}C-A\right)$$
15		dvfsumlem4.0	$$⊢\left(\phi \wedge \left(x\in S\wedge D\le x\wedge x\le U\right)\right)\to 0\le B$$
16		dvfsumlem4.1	$$⊢\phi \to X\in S$$
17		dvfsumlem4.2	$$⊢\phi \to Y\in S$$
18		dvfsumlem4.3	$$⊢\phi \to D\le X$$
19		dvfsumlem4.4	$$⊢\phi \to X\le Y$$
20		dvfsumlem4.5	$$⊢\phi \to Y\le U$$
21		fzfid	$$⊢\phi \to \left(M\dots ⌊Y⌋\right)\in \mathrm{Fin}$$
22	9	ralrimiva	$$⊢\phi \to \forall x\in ZB\in ℝ$$
23		elfzuz	$$⊢k\in \left(M\dots ⌊Y⌋\right)\to k\in {\mathbb{Z}}_{\ge M}$$
24	23 2	eleqtrrdi	$$⊢k\in \left(M\dots ⌊Y⌋\right)\to k\in Z$$
25	11	eleq1d	$$⊢x=k\to \left(B\in ℝ\leftrightarrow C\in ℝ\right)$$
26	25	rspccva	$$⊢\left(\forall x\in ZB\in ℝ\wedge k\in Z\right)\to C\in ℝ$$
27	22 24 26	syl2an	$$⊢\left(\phi \wedge k\in \left(M\dots ⌊Y⌋\right)\right)\to C\in ℝ$$
28	21 27	fsumrecl	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C\in ℝ$$
29	7	ralrimiva	$$⊢\phi \to \forall x\in SA\in ℝ$$
30		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋Y/x⦌A$$
31	30	nfel1	$$⊢Ⅎx⦋Y/x⦌A\in ℝ$$
32		csbeq1a	$$⊢x=Y\to A=⦋Y/x⦌A$$
33	32	eleq1d	$$⊢x=Y\to \left(A\in ℝ\leftrightarrow ⦋Y/x⦌A\in ℝ\right)$$
34	31 33	rspc	$$⊢Y\in S\to \left(\forall x\in SA\in ℝ\to ⦋Y/x⦌A\in ℝ\right)$$
35	17 29 34	sylc	$$⊢\phi \to ⦋Y/x⦌A\in ℝ$$
36	28 35	resubcld	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\in ℝ$$
37		nfcv	$$⊢\underset{\_}{Ⅎ}xY$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}x\sum _{k=M}^{⌊Y⌋}C$$
39		nfcv	$$⊢\underset{\_}{Ⅎ}x-$$
40	38 39 30	nfov	$$⊢\underset{\_}{Ⅎ}x\left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)$$
41		fveq2	$$⊢x=Y\to ⌊x⌋=⌊Y⌋$$
42	41	oveq2d	$$⊢x=Y\to \left(M\dots ⌊x⌋\right)=\left(M\dots ⌊Y⌋\right)$$
43	42	sumeq1d	$$⊢x=Y\to \sum _{k=M}^{⌊x⌋}C=\sum _{k=M}^{⌊Y⌋}C$$
44	43 32	oveq12d	$$⊢x=Y\to \sum _{k=M}^{⌊x⌋}C-A=\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
45	37 40 44 14	fvmptf	$$⊢\left(Y\in S\wedge \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\in ℝ\right)\to G\left(Y\right)=\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
46	17 36 45	syl2anc	$$⊢\phi \to G\left(Y\right)=\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
47		fzfid	$$⊢\phi \to \left(M\dots ⌊X⌋\right)\in \mathrm{Fin}$$
48		elfzuz	$$⊢k\in \left(M\dots ⌊X⌋\right)\to k\in {\mathbb{Z}}_{\ge M}$$
49	48 2	eleqtrrdi	$$⊢k\in \left(M\dots ⌊X⌋\right)\to k\in Z$$
50	22 49 26	syl2an	$$⊢\left(\phi \wedge k\in \left(M\dots ⌊X⌋\right)\right)\to C\in ℝ$$
51	47 50	fsumrecl	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C\in ℝ$$
52		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋X/x⦌A$$
53	52	nfel1	$$⊢Ⅎx⦋X/x⦌A\in ℝ$$
54		csbeq1a	$$⊢x=X\to A=⦋X/x⦌A$$
55	54	eleq1d	$$⊢x=X\to \left(A\in ℝ\leftrightarrow ⦋X/x⦌A\in ℝ\right)$$
56	53 55	rspc	$$⊢X\in S\to \left(\forall x\in SA\in ℝ\to ⦋X/x⦌A\in ℝ\right)$$
57	16 29 56	sylc	$$⊢\phi \to ⦋X/x⦌A\in ℝ$$
58	51 57	resubcld	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\in ℝ$$
59		nfcv	$$⊢\underset{\_}{Ⅎ}xX$$
60		nfcv	$$⊢\underset{\_}{Ⅎ}x\sum _{k=M}^{⌊X⌋}C$$
61	60 39 52	nfov	$$⊢\underset{\_}{Ⅎ}x\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)$$
62		fveq2	$$⊢x=X\to ⌊x⌋=⌊X⌋$$
63	62	oveq2d	$$⊢x=X\to \left(M\dots ⌊x⌋\right)=\left(M\dots ⌊X⌋\right)$$
64	63	sumeq1d	$$⊢x=X\to \sum _{k=M}^{⌊x⌋}C=\sum _{k=M}^{⌊X⌋}C$$
65	64 54	oveq12d	$$⊢x=X\to \sum _{k=M}^{⌊x⌋}C-A=\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
66	59 61 65 14	fvmptf	$$⊢\left(X\in S\wedge \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\in ℝ\right)\to G\left(X\right)=\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
67	16 58 66	syl2anc	$$⊢\phi \to G\left(X\right)=\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
68	46 67	oveq12d	$$⊢\phi \to G\left(Y\right)-G\left(X\right)=\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A-\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)$$
69	68	fveq2d	$$⊢\phi \to \left|G\left(Y\right)-G\left(X\right)\right|=\left|\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A-\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)\right|$$
70		ioossre	$$⊢\left(T,\mathrm{+\infty }\right)\subseteq ℝ$$
71	1 70	eqsstri	$$⊢S\subseteq ℝ$$
72	71	a1i	$$⊢\phi \to S\subseteq ℝ$$
73	72 7 8 10	dvmptrecl	$$⊢\left(\phi \wedge x\in S\right)\to B\in ℝ$$
74	73	ralrimiva	$$⊢\phi \to \forall x\in SB\in ℝ$$
75		nfv	$$⊢ℲmB\in ℝ$$
76		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋m/x⦌B$$
77	76	nfel1	$$⊢Ⅎx⦋m/x⦌B\in ℝ$$
78		csbeq1a	$$⊢x=m\to B=⦋m/x⦌B$$
79	78	eleq1d	$$⊢x=m\to \left(B\in ℝ\leftrightarrow ⦋m/x⦌B\in ℝ\right)$$
80	75 77 79	cbvralw	$$⊢\forall x\in SB\in ℝ\leftrightarrow \forall m\in S⦋m/x⦌B\in ℝ$$
81	74 80	sylib	$$⊢\phi \to \forall m\in S⦋m/x⦌B\in ℝ$$
82		csbeq1	$$⊢m=X\to ⦋m/x⦌B=⦋X/x⦌B$$
83	82	eleq1d	$$⊢m=X\to \left(⦋m/x⦌B\in ℝ\leftrightarrow ⦋X/x⦌B\in ℝ\right)$$
84	83	rspcv	$$⊢X\in S\to \left(\forall m\in S⦋m/x⦌B\in ℝ\to ⦋X/x⦌B\in ℝ\right)$$
85	16 81 84	sylc	$$⊢\phi \to ⦋X/x⦌B\in ℝ$$
86	58 85	resubcld	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A-⦋X/x⦌B\in ℝ$$
87	71 16	sseldi	$$⊢\phi \to X\in ℝ$$
88		reflcl	$$⊢X\in ℝ\to ⌊X⌋\in ℝ$$
89	87 88	syl	$$⊢\phi \to ⌊X⌋\in ℝ$$
90	87 89	resubcld	$$⊢\phi \to X-⌊X⌋\in ℝ$$
91	90 85	remulcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B\in ℝ$$
92	91 58	readdcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\in ℝ$$
93	92 85	resubcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B+\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)-⦋X/x⦌B\in ℝ$$
94		fracge0	$$⊢X\in ℝ\to 0\le X-⌊X⌋$$
95	87 94	syl	$$⊢\phi \to 0\le X-⌊X⌋$$
96	87	rexrd	$$⊢\phi \to X\in {ℝ}^{*}$$
97	71 17	sseldi	$$⊢\phi \to Y\in ℝ$$
98	97	rexrd	$$⊢\phi \to Y\in {ℝ}^{*}$$
99	96 98 12 19 20	xrletrd	$$⊢\phi \to X\le U$$
100	16 18 99	3jca	$$⊢\phi \to \left(X\in S\wedge D\le X\wedge X\le U\right)$$
101		simpr1	$$⊢\left(\phi \wedge \left(X\in S\wedge D\le X\wedge X\le U\right)\right)\to X\in S$$
102		nfv	$$⊢Ⅎx\left(\phi \wedge \left(X\in S\wedge D\le X\wedge X\le U\right)\right)$$
103		nfcv	$$⊢\underset{\_}{Ⅎ}x0$$
104		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
105		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋X/x⦌B$$
106	103 104 105	nfbr	$$⊢Ⅎx0\le ⦋X/x⦌B$$
107	102 106	nfim	$$⊢Ⅎx\left(\left(\phi \wedge \left(X\in S\wedge D\le X\wedge X\le U\right)\right)\to 0\le ⦋X/x⦌B\right)$$
108		eleq1	$$⊢x=X\to \left(x\in S\leftrightarrow X\in S\right)$$
109		breq2	$$⊢x=X\to \left(D\le x\leftrightarrow D\le X\right)$$
110		breq1	$$⊢x=X\to \left(x\le U\leftrightarrow X\le U\right)$$
111	108 109 110	3anbi123d	$$⊢x=X\to \left(\left(x\in S\wedge D\le x\wedge x\le U\right)\leftrightarrow \left(X\in S\wedge D\le X\wedge X\le U\right)\right)$$
112	111	anbi2d	$$⊢x=X\to \left(\left(\phi \wedge \left(x\in S\wedge D\le x\wedge x\le U\right)\right)\leftrightarrow \left(\phi \wedge \left(X\in S\wedge D\le X\wedge X\le U\right)\right)\right)$$
113		csbeq1a	$$⊢x=X\to B=⦋X/x⦌B$$
114	113	breq2d	$$⊢x=X\to \left(0\le B\leftrightarrow 0\le ⦋X/x⦌B\right)$$
115	112 114	imbi12d	$$⊢x=X\to \left(\left(\left(\phi \wedge \left(x\in S\wedge D\le x\wedge x\le U\right)\right)\to 0\le B\right)\leftrightarrow \left(\left(\phi \wedge \left(X\in S\wedge D\le X\wedge X\le U\right)\right)\to 0\le ⦋X/x⦌B\right)\right)$$
116	107 115 15	vtoclg1f	$$⊢X\in S\to \left(\left(\phi \wedge \left(X\in S\wedge D\le X\wedge X\le U\right)\right)\to 0\le ⦋X/x⦌B\right)$$
117	101 116	mpcom	$$⊢\left(\phi \wedge \left(X\in S\wedge D\le X\wedge X\le U\right)\right)\to 0\le ⦋X/x⦌B$$
118	100 117	mpdan	$$⊢\phi \to 0\le ⦋X/x⦌B$$
119	90 85 95 118	mulge0d	$$⊢\phi \to 0\le \left(X-⌊X⌋\right)⦋X/x⦌B$$
120	58 91	addge02d	$$⊢\phi \to \left(0\le \left(X-⌊X⌋\right)⦋X/x⦌B\leftrightarrow \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\le \left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)$$
121	119 120	mpbid	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\le \left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
122	58 92 85 121	lesub1dd	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A-⦋X/x⦌B\le \left(X-⌊X⌋\right)⦋X/x⦌B+\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)-⦋X/x⦌B$$
123		reflcl	$$⊢Y\in ℝ\to ⌊Y⌋\in ℝ$$
124	97 123	syl	$$⊢\phi \to ⌊Y⌋\in ℝ$$
125	97 124	resubcld	$$⊢\phi \to Y-⌊Y⌋\in ℝ$$
126		csbeq1	$$⊢m=Y\to ⦋m/x⦌B=⦋Y/x⦌B$$
127	126	eleq1d	$$⊢m=Y\to \left(⦋m/x⦌B\in ℝ\leftrightarrow ⦋Y/x⦌B\in ℝ\right)$$
128	127	rspcv	$$⊢Y\in S\to \left(\forall m\in S⦋m/x⦌B\in ℝ\to ⦋Y/x⦌B\in ℝ\right)$$
129	17 81 128	sylc	$$⊢\phi \to ⦋Y/x⦌B\in ℝ$$
130	125 129	remulcld	$$⊢\phi \to \left(Y-⌊Y⌋\right)⦋Y/x⦌B\in ℝ$$
131	130 36	readdcld	$$⊢\phi \to \left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\in ℝ$$
132	131 129	resubcld	$$⊢\phi \to \left(Y-⌊Y⌋\right)⦋Y/x⦌B+\left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)-⦋Y/x⦌B\in ℝ$$
133		eqid	$$⊢\left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)=\left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)$$
134	1 2 3 4 5 6 7 8 9 10 11 12 13 133 16 17 18 19 20	dvfsumlem3	$$⊢\phi \to \left(\left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(Y\right)\le \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(X\right)\wedge \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(X\right)-⦋X/x⦌B\le \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(Y\right)-⦋Y/x⦌B\right)$$
135	134	simprd	$$⊢\phi \to \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(X\right)-⦋X/x⦌B\le \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(Y\right)-⦋Y/x⦌B$$
136		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(X-⌊X⌋\right)$$
137		nfcv	$$⊢\underset{\_}{Ⅎ}x\times$$
138	136 137 105	nfov	$$⊢\underset{\_}{Ⅎ}x\left(X-⌊X⌋\right)⦋X/x⦌B$$
139		nfcv	$$⊢\underset{\_}{Ⅎ}x+$$
140	138 139 61	nfov	$$⊢\underset{\_}{Ⅎ}x\left(\left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)$$
141		id	$$⊢x=X\to x=X$$
142	141 62	oveq12d	$$⊢x=X\to x-⌊x⌋=X-⌊X⌋$$
143	142 113	oveq12d	$$⊢x=X\to \left(x-⌊x⌋\right)B=\left(X-⌊X⌋\right)⦋X/x⦌B$$
144	143 65	oveq12d	$$⊢x=X\to \left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A=\left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
145	59 140 144 133	fvmptf	$$⊢\left(X\in S\wedge \left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\in ℝ\right)\to \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(X\right)=\left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
146	16 92 145	syl2anc	$$⊢\phi \to \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(X\right)=\left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
147	146	oveq1d	$$⊢\phi \to \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(X\right)-⦋X/x⦌B=\left(X-⌊X⌋\right)⦋X/x⦌B+\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)-⦋X/x⦌B$$
148		nfcv	$$⊢\underset{\_}{Ⅎ}x\left(Y-⌊Y⌋\right)$$
149		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋Y/x⦌B$$
150	148 137 149	nfov	$$⊢\underset{\_}{Ⅎ}x\left(Y-⌊Y⌋\right)⦋Y/x⦌B$$
151	150 139 40	nfov	$$⊢\underset{\_}{Ⅎ}x\left(\left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)$$
152		id	$$⊢x=Y\to x=Y$$
153	152 41	oveq12d	$$⊢x=Y\to x-⌊x⌋=Y-⌊Y⌋$$
154		csbeq1a	$$⊢x=Y\to B=⦋Y/x⦌B$$
155	153 154	oveq12d	$$⊢x=Y\to \left(x-⌊x⌋\right)B=\left(Y-⌊Y⌋\right)⦋Y/x⦌B$$
156	155 44	oveq12d	$$⊢x=Y\to \left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A=\left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
157	37 151 156 133	fvmptf	$$⊢\left(Y\in S\wedge \left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\in ℝ\right)\to \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(Y\right)=\left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
158	17 131 157	syl2anc	$$⊢\phi \to \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(Y\right)=\left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
159	158	oveq1d	$$⊢\phi \to \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(Y\right)-⦋Y/x⦌B=\left(Y-⌊Y⌋\right)⦋Y/x⦌B+\left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)-⦋Y/x⦌B$$
160	135 147 159	3brtr3d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B+\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)-⦋X/x⦌B\le \left(Y-⌊Y⌋\right)⦋Y/x⦌B+\left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)-⦋Y/x⦌B$$
161	36	recnd	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\in ℂ$$
162	129	recnd	$$⊢\phi \to ⦋Y/x⦌B\in ℂ$$
163	130	recnd	$$⊢\phi \to \left(Y-⌊Y⌋\right)⦋Y/x⦌B\in ℂ$$
164	161 162 163	subsub3d	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A-\left(⦋Y/x⦌B-\left(Y-⌊Y⌋\right)⦋Y/x⦌B\right)=\left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)+\left(Y-⌊Y⌋\right)⦋Y/x⦌B-⦋Y/x⦌B$$
165	161 163	addcomd	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A+\left(Y-⌊Y⌋\right)⦋Y/x⦌B=\left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
166	165	oveq1d	$$⊢\phi \to \left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)+\left(Y-⌊Y⌋\right)⦋Y/x⦌B-⦋Y/x⦌B=\left(Y-⌊Y⌋\right)⦋Y/x⦌B+\left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)-⦋Y/x⦌B$$
167	164 166	eqtrd	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A-\left(⦋Y/x⦌B-\left(Y-⌊Y⌋\right)⦋Y/x⦌B\right)=\left(Y-⌊Y⌋\right)⦋Y/x⦌B+\left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)-⦋Y/x⦌B$$
168		1red	$$⊢\phi \to 1\in ℝ$$
169	4 87 97 18 19	letrd	$$⊢\phi \to D\le Y$$
170	17 169 20	3jca	$$⊢\phi \to \left(Y\in S\wedge D\le Y\wedge Y\le U\right)$$
171		simpr1	$$⊢\left(\phi \wedge \left(Y\in S\wedge D\le Y\wedge Y\le U\right)\right)\to Y\in S$$
172		nfv	$$⊢Ⅎx\left(\phi \wedge \left(Y\in S\wedge D\le Y\wedge Y\le U\right)\right)$$
173	103 104 149	nfbr	$$⊢Ⅎx0\le ⦋Y/x⦌B$$
174	172 173	nfim	$$⊢Ⅎx\left(\left(\phi \wedge \left(Y\in S\wedge D\le Y\wedge Y\le U\right)\right)\to 0\le ⦋Y/x⦌B\right)$$
175		eleq1	$$⊢x=Y\to \left(x\in S\leftrightarrow Y\in S\right)$$
176		breq2	$$⊢x=Y\to \left(D\le x\leftrightarrow D\le Y\right)$$
177		breq1	$$⊢x=Y\to \left(x\le U\leftrightarrow Y\le U\right)$$
178	175 176 177	3anbi123d	$$⊢x=Y\to \left(\left(x\in S\wedge D\le x\wedge x\le U\right)\leftrightarrow \left(Y\in S\wedge D\le Y\wedge Y\le U\right)\right)$$
179	178	anbi2d	$$⊢x=Y\to \left(\left(\phi \wedge \left(x\in S\wedge D\le x\wedge x\le U\right)\right)\leftrightarrow \left(\phi \wedge \left(Y\in S\wedge D\le Y\wedge Y\le U\right)\right)\right)$$
180	154	breq2d	$$⊢x=Y\to \left(0\le B\leftrightarrow 0\le ⦋Y/x⦌B\right)$$
181	179 180	imbi12d	$$⊢x=Y\to \left(\left(\left(\phi \wedge \left(x\in S\wedge D\le x\wedge x\le U\right)\right)\to 0\le B\right)\leftrightarrow \left(\left(\phi \wedge \left(Y\in S\wedge D\le Y\wedge Y\le U\right)\right)\to 0\le ⦋Y/x⦌B\right)\right)$$
182	174 181 15	vtoclg1f	$$⊢Y\in S\to \left(\left(\phi \wedge \left(Y\in S\wedge D\le Y\wedge Y\le U\right)\right)\to 0\le ⦋Y/x⦌B\right)$$
183	171 182	mpcom	$$⊢\left(\phi \wedge \left(Y\in S\wedge D\le Y\wedge Y\le U\right)\right)\to 0\le ⦋Y/x⦌B$$
184	170 183	mpdan	$$⊢\phi \to 0\le ⦋Y/x⦌B$$
185		fracle1	$$⊢Y\in ℝ\to Y-⌊Y⌋\le 1$$
186	97 185	syl	$$⊢\phi \to Y-⌊Y⌋\le 1$$
187	125 168 129 184 186	lemul1ad	$$⊢\phi \to \left(Y-⌊Y⌋\right)⦋Y/x⦌B\le 1⦋Y/x⦌B$$
188	162	mulid2d	$$⊢\phi \to 1⦋Y/x⦌B=⦋Y/x⦌B$$
189	187 188	breqtrd	$$⊢\phi \to \left(Y-⌊Y⌋\right)⦋Y/x⦌B\le ⦋Y/x⦌B$$
190	129 130	subge0d	$$⊢\phi \to \left(0\le ⦋Y/x⦌B-\left(Y-⌊Y⌋\right)⦋Y/x⦌B\leftrightarrow \left(Y-⌊Y⌋\right)⦋Y/x⦌B\le ⦋Y/x⦌B\right)$$
191	189 190	mpbird	$$⊢\phi \to 0\le ⦋Y/x⦌B-\left(Y-⌊Y⌋\right)⦋Y/x⦌B$$
192	129 130	resubcld	$$⊢\phi \to ⦋Y/x⦌B-\left(Y-⌊Y⌋\right)⦋Y/x⦌B\in ℝ$$
193	36 192	subge02d	$$⊢\phi \to \left(0\le ⦋Y/x⦌B-\left(Y-⌊Y⌋\right)⦋Y/x⦌B\leftrightarrow \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A-\left(⦋Y/x⦌B-\left(Y-⌊Y⌋\right)⦋Y/x⦌B\right)\le \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)$$
194	191 193	mpbid	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A-\left(⦋Y/x⦌B-\left(Y-⌊Y⌋\right)⦋Y/x⦌B\right)\le \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
195	167 194	eqbrtrrd	$$⊢\phi \to \left(Y-⌊Y⌋\right)⦋Y/x⦌B+\left(\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)-⦋Y/x⦌B\le \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
196	93 132 36 160 195	letrd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B+\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)-⦋X/x⦌B\le \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
197	86 93 36 122 196	letrd	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A-⦋X/x⦌B\le \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
198	85 58	readdcld	$$⊢\phi \to ⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\in ℝ$$
199		fracge0	$$⊢Y\in ℝ\to 0\le Y-⌊Y⌋$$
200	97 199	syl	$$⊢\phi \to 0\le Y-⌊Y⌋$$
201	125 129 200 184	mulge0d	$$⊢\phi \to 0\le \left(Y-⌊Y⌋\right)⦋Y/x⦌B$$
202	36 130	addge02d	$$⊢\phi \to \left(0\le \left(Y-⌊Y⌋\right)⦋Y/x⦌B\leftrightarrow \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\le \left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\right)$$
203	201 202	mpbid	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\le \left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A$$
204	134	simpld	$$⊢\phi \to \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(Y\right)\le \left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)\left(X\right)$$
205	204 158 146	3brtr3d	$$⊢\phi \to \left(Y-⌊Y⌋\right)⦋Y/x⦌B+\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\le \left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
206	36 131 92 203 205	letrd	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\le \left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
207		fracle1	$$⊢X\in ℝ\to X-⌊X⌋\le 1$$
208	87 207	syl	$$⊢\phi \to X-⌊X⌋\le 1$$
209	90 168 85 118 208	lemul1ad	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B\le 1⦋X/x⦌B$$
210	85	recnd	$$⊢\phi \to ⦋X/x⦌B\in ℂ$$
211	210	mulid2d	$$⊢\phi \to 1⦋X/x⦌B=⦋X/x⦌B$$
212	209 211	breqtrd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B\le ⦋X/x⦌B$$
213	91 85 58 212	leadd1dd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\le ⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
214	36 92 198 206 213	letrd	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\le ⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A$$
215	58	recnd	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\in ℂ$$
216	210 215	addcomd	$$⊢\phi \to ⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A=\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A+⦋X/x⦌B$$
217	214 216	breqtrd	$$⊢\phi \to \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\le \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A+⦋X/x⦌B$$
218	36 58 85	absdifled	$$⊢\phi \to \left(\left|\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A-\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)\right|\le ⦋X/x⦌B\leftrightarrow \left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A-⦋X/x⦌B\le \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\wedge \sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A\le \sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A+⦋X/x⦌B\right)\right)$$
219	197 217 218	mpbir2and	$$⊢\phi \to \left|\sum _{k=M}^{⌊Y⌋}C-⦋Y/x⦌A-\left(\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌A\right)\right|\le ⦋X/x⦌B$$
220	69 219	eqbrtrd	$$⊢\phi \to \left|G\left(Y\right)-G\left(X\right)\right|\le ⦋X/x⦌B$$