Theorem dvfsumlem2

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-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$$
	dvfsum.h	$$⊢H=\left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)$$
	dvfsumlem1.1	$$⊢\phi \to X\in S$$
	dvfsumlem1.2	$$⊢\phi \to Y\in S$$
	dvfsumlem1.3	$$⊢\phi \to D\le X$$
	dvfsumlem1.4	$$⊢\phi \to X\le Y$$
	dvfsumlem1.5	$$⊢\phi \to Y\le U$$
	dvfsumlem1.6	$$⊢\phi \to Y\le ⌊X⌋+1$$
Assertion	dvfsumlem2	$$⊢\phi \to \left(H\left(Y\right)\le H\left(X\right)\wedge H\left(X\right)-⦋X/x⦌B\le H\left(Y\right)-⦋Y/x⦌B\right)$$

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		dvfsum.h	$$⊢H=\left(x\in S⟼\left(x-⌊x⌋\right)B+\sum _{k=M}^{⌊x⌋}C-A\right)$$
15		dvfsumlem1.1	$$⊢\phi \to X\in S$$
16		dvfsumlem1.2	$$⊢\phi \to Y\in S$$
17		dvfsumlem1.3	$$⊢\phi \to D\le X$$
18		dvfsumlem1.4	$$⊢\phi \to X\le Y$$
19		dvfsumlem1.5	$$⊢\phi \to Y\le U$$
20		dvfsumlem1.6	$$⊢\phi \to Y\le ⌊X⌋+1$$
21		ioossre	$$⊢\left(T,\mathrm{+\infty }\right)\subseteq ℝ$$
22	1 21	eqsstri	$$⊢S\subseteq ℝ$$
23	22 16	sseldi	$$⊢\phi \to Y\in ℝ$$
24	15 1	eleqtrdi	$$⊢\phi \to X\in \left(T,\mathrm{+\infty }\right)$$
25	6	rexrd	$$⊢\phi \to T\in {ℝ}^{*}$$
26		elioopnf	$$⊢T\in {ℝ}^{*}\to \left(X\in \left(T,\mathrm{+\infty }\right)\leftrightarrow \left(X\in ℝ\wedge T<X\right)\right)$$
27	25 26	syl	$$⊢\phi \to \left(X\in \left(T,\mathrm{+\infty }\right)\leftrightarrow \left(X\in ℝ\wedge T<X\right)\right)$$
28	24 27	mpbid	$$⊢\phi \to \left(X\in ℝ\wedge T<X\right)$$
29	28	simpld	$$⊢\phi \to X\in ℝ$$
30		reflcl	$$⊢X\in ℝ\to ⌊X⌋\in ℝ$$
31	29 30	syl	$$⊢\phi \to ⌊X⌋\in ℝ$$
32	23 31	resubcld	$$⊢\phi \to Y-⌊X⌋\in ℝ$$
33		csbeq1	$$⊢y=Y\to ⦋y/x⦌B=⦋Y/x⦌B$$
34	33	eleq1d	$$⊢y=Y\to \left(⦋y/x⦌B\in ℝ\leftrightarrow ⦋Y/x⦌B\in ℝ\right)$$
35	22	a1i	$$⊢\phi \to S\subseteq ℝ$$
36	35 7 8 10	dvmptrecl	$$⊢\left(\phi \wedge x\in S\right)\to B\in ℝ$$
37	36	fmpttd	$$⊢\phi \to \left(x\in S⟼B\right):S⟶ℝ$$
38		nfcv	$$⊢\underset{\_}{Ⅎ}yB$$
39		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌B$$
40		csbeq1a	$$⊢x=y\to B=⦋y/x⦌B$$
41	38 39 40	cbvmpt	$$⊢\left(x\in S⟼B\right)=\left(y\in S⟼⦋y/x⦌B\right)$$
42	41	fmpt	$$⊢\forall y\in S⦋y/x⦌B\in ℝ\leftrightarrow \left(x\in S⟼B\right):S⟶ℝ$$
43	37 42	sylibr	$$⊢\phi \to \forall y\in S⦋y/x⦌B\in ℝ$$
44	34 43 16	rspcdva	$$⊢\phi \to ⦋Y/x⦌B\in ℝ$$
45	32 44	remulcld	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B\in ℝ$$
46		csbeq1	$$⊢y=Y\to ⦋y/x⦌A=⦋Y/x⦌A$$
47	46	eleq1d	$$⊢y=Y\to \left(⦋y/x⦌A\in ℝ\leftrightarrow ⦋Y/x⦌A\in ℝ\right)$$
48	7	fmpttd	$$⊢\phi \to \left(x\in S⟼A\right):S⟶ℝ$$
49		nfcv	$$⊢\underset{\_}{Ⅎ}yA$$
50		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋y/x⦌A$$
51		csbeq1a	$$⊢x=y\to A=⦋y/x⦌A$$
52	49 50 51	cbvmpt	$$⊢\left(x\in S⟼A\right)=\left(y\in S⟼⦋y/x⦌A\right)$$
53	52	fmpt	$$⊢\forall y\in S⦋y/x⦌A\in ℝ\leftrightarrow \left(x\in S⟼A\right):S⟶ℝ$$
54	48 53	sylibr	$$⊢\phi \to \forall y\in S⦋y/x⦌A\in ℝ$$
55	47 54 16	rspcdva	$$⊢\phi \to ⦋Y/x⦌A\in ℝ$$
56	45 55	resubcld	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\in ℝ$$
57	29 31	resubcld	$$⊢\phi \to X-⌊X⌋\in ℝ$$
58		csbeq1	$$⊢y=X\to ⦋y/x⦌B=⦋X/x⦌B$$
59	58	eleq1d	$$⊢y=X\to \left(⦋y/x⦌B\in ℝ\leftrightarrow ⦋X/x⦌B\in ℝ\right)$$
60	59 43 15	rspcdva	$$⊢\phi \to ⦋X/x⦌B\in ℝ$$
61	57 60	remulcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B\in ℝ$$
62		csbeq1	$$⊢y=X\to ⦋y/x⦌A=⦋X/x⦌A$$
63	62	eleq1d	$$⊢y=X\to \left(⦋y/x⦌A\in ℝ\leftrightarrow ⦋X/x⦌A\in ℝ\right)$$
64	63 54 15	rspcdva	$$⊢\phi \to ⦋X/x⦌A\in ℝ$$
65	61 64	resubcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A\in ℝ$$
66		fzfid	$$⊢\phi \to \left(M\dots ⌊X⌋\right)\in \mathrm{Fin}$$
67	9	ralrimiva	$$⊢\phi \to \forall x\in ZB\in ℝ$$
68		elfzuz	$$⊢k\in \left(M\dots ⌊X⌋\right)\to k\in {\mathbb{Z}}_{\ge M}$$
69	68 2	eleqtrrdi	$$⊢k\in \left(M\dots ⌊X⌋\right)\to k\in Z$$
70	11	eleq1d	$$⊢x=k\to \left(B\in ℝ\leftrightarrow C\in ℝ\right)$$
71	70	rspccva	$$⊢\left(\forall x\in ZB\in ℝ\wedge k\in Z\right)\to C\in ℝ$$
72	67 69 71	syl2an	$$⊢\left(\phi \wedge k\in \left(M\dots ⌊X⌋\right)\right)\to C\in ℝ$$
73	66 72	fsumrecl	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C\in ℝ$$
74	57 44	remulcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B\in ℝ$$
75	74 64	resubcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-⦋X/x⦌A\in ℝ$$
76	23 29	resubcld	$$⊢\phi \to Y-X\in ℝ$$
77	44 76	remulcld	$$⊢\phi \to ⦋Y/x⦌B\left(Y-X\right)\in ℝ$$
78	44	recnd	$$⊢\phi \to ⦋Y/x⦌B\in ℂ$$
79	23	recnd	$$⊢\phi \to Y\in ℂ$$
80	29	recnd	$$⊢\phi \to X\in ℂ$$
81	78 79 80	subdid	$$⊢\phi \to ⦋Y/x⦌B\left(Y-X\right)=⦋Y/x⦌BY-⦋Y/x⦌BX$$
82		eqid	$$⊢\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)$$
83	82	mulcn	$$⊢\times \in \left(\left(\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\times }_t\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)\mathrm{Cn}\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right)\right)$$
84		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
85	84	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
86	28	simprd	$$⊢\phi \to T<X$$
87	23	ltpnfd	$$⊢\phi \to Y<\mathrm{+\infty }$$
88		iccssioo	$$⊢\left(\left(T\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\wedge \left(T<X\wedge Y<\mathrm{+\infty }\right)\right)\to \left[X,Y\right]\subseteq \left(T,\mathrm{+\infty }\right)$$
89	25 85 86 87 88	syl22anc	$$⊢\phi \to \left[X,Y\right]\subseteq \left(T,\mathrm{+\infty }\right)$$
90	89 21	sstrdi	$$⊢\phi \to \left[X,Y\right]\subseteq ℝ$$
91		ax-resscn	$$⊢ℝ\subseteq ℂ$$
92	90 91	sstrdi	$$⊢\phi \to \left[X,Y\right]\subseteq ℂ$$
93	91	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
94		cncfmptc	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge \left[X,Y\right]\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to \left(y\in \left[X,Y\right]⟼⦋Y/x⦌B\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
95	44 92 93 94	syl3anc	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋Y/x⦌B\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
96		cncfmptid	$$⊢\left(\left[X,Y\right]\subseteq ℝ\wedge ℝ\subseteq ℂ\right)\to \left(y\in \left[X,Y\right]⟼y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
97	90 91 96	sylancl	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
98		remulcl	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋Y/x⦌By\in ℝ$$
99	82 83 95 97 91 98	cncfmpt2ss	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
100		reelprrecn	$$⊢ℝ\in \left\{ℝ,ℂ\right\}$$
101	100	a1i	$$⊢\phi \to ℝ\in \left\{ℝ,ℂ\right\}$$
102		ioossicc	$$⊢\left(X,Y\right)\subseteq \left[X,Y\right]$$
103	102 90	sstrid	$$⊢\phi \to \left(X,Y\right)\subseteq ℝ$$
104	103	sselda	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to y\in ℝ$$
105	104	recnd	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to y\in ℂ$$
106		1cnd	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to 1\in ℂ$$
107		simpr	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\in ℝ$$
108	107	recnd	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\in ℂ$$
109		1cnd	$$⊢\left(\phi \wedge y\in ℝ\right)\to 1\in ℂ$$
110	101	dvmptid	$$⊢\phi \to \frac{d\left(y\in ℝ⟼y\right)}{d_{ℝ}y}=\left(y\in ℝ⟼1\right)$$
111	82	tgioo2	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
112		iooretop	$$⊢\left(X,Y\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
113	112	a1i	$$⊢\phi \to \left(X,Y\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
114	101 108 109 110 103 111 82 113	dvmptres	$$⊢\phi \to \frac{d\left(y\in \left(X,Y\right)⟼y\right)}{d_{ℝ}y}=\left(y\in \left(X,Y\right)⟼1\right)$$
115	101 105 106 114 78	dvmptcmul	$$⊢\phi \to \frac{d\left(y\in \left(X,Y\right)⟼⦋Y/x⦌By\right)}{d_{ℝ}y}=\left(y\in \left(X,Y\right)⟼⦋Y/x⦌B\cdot 1\right)$$
116	78	mulid1d	$$⊢\phi \to ⦋Y/x⦌B\cdot 1=⦋Y/x⦌B$$
117	116	mpteq2dv	$$⊢\phi \to \left(y\in \left(X,Y\right)⟼⦋Y/x⦌B\cdot 1\right)=\left(y\in \left(X,Y\right)⟼⦋Y/x⦌B\right)$$
118	115 117	eqtrd	$$⊢\phi \to \frac{d\left(y\in \left(X,Y\right)⟼⦋Y/x⦌By\right)}{d_{ℝ}y}=\left(y\in \left(X,Y\right)⟼⦋Y/x⦌B\right)$$
119	89 1	sseqtrrdi	$$⊢\phi \to \left[X,Y\right]\subseteq S$$
120	119	resmptd	$$⊢\phi \to {\left(y\in S⟼⦋y/x⦌A\right)\upharpoonright }_{\left[X,Y\right]}=\left(y\in \left[X,Y\right]⟼⦋y/x⦌A\right)$$
121	7	recnd	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℂ$$
122	121	fmpttd	$$⊢\phi \to \left(x\in S⟼A\right):S⟶ℂ$$
123	10	dmeqd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\mathrm{dom}\left(x\in S⟼B\right)$$
124	8	ralrimiva	$$⊢\phi \to \forall x\in SB\in V$$
125		dmmptg	$$⊢\forall x\in SB\in V\to \mathrm{dom}\left(x\in S⟼B\right)=S$$
126	124 125	syl	$$⊢\phi \to \mathrm{dom}\left(x\in S⟼B\right)=S$$
127	123 126	eqtrd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=S$$
128		dvcn	$$⊢\left(\left(ℝ\subseteq ℂ\wedge \left(x\in S⟼A\right):S⟶ℂ\wedge S\subseteq ℝ\right)\wedge \mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=S\right)\to \left(x\in S⟼A\right):S\underset{cn}{⟶}ℂ$$
129	93 122 35 127 128	syl31anc	$$⊢\phi \to \left(x\in S⟼A\right):S\underset{cn}{⟶}ℂ$$
130		cncffvrn	$$⊢\left(ℝ\subseteq ℂ\wedge \left(x\in S⟼A\right):S\underset{cn}{⟶}ℂ\right)\to \left(\left(x\in S⟼A\right):S\underset{cn}{⟶}ℝ\leftrightarrow \left(x\in S⟼A\right):S⟶ℝ\right)$$
131	91 129 130	sylancr	$$⊢\phi \to \left(\left(x\in S⟼A\right):S\underset{cn}{⟶}ℝ\leftrightarrow \left(x\in S⟼A\right):S⟶ℝ\right)$$
132	48 131	mpbird	$$⊢\phi \to \left(x\in S⟼A\right):S\underset{cn}{⟶}ℝ$$
133	52 132	eqeltrrid	$$⊢\phi \to \left(y\in S⟼⦋y/x⦌A\right):S\underset{cn}{⟶}ℝ$$
134		rescncf	$$⊢\left[X,Y\right]\subseteq S\to \left(\left(y\in S⟼⦋y/x⦌A\right):S\underset{cn}{⟶}ℝ\to \left({\left(y\in S⟼⦋y/x⦌A\right)\upharpoonright }_{\left[X,Y\right]}\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\right)$$
135	119 133 134	sylc	$$⊢\phi \to \left({\left(y\in S⟼⦋y/x⦌A\right)\upharpoonright }_{\left[X,Y\right]}\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
136	120 135	eqeltrrd	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋y/x⦌A\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
137	54	r19.21bi	$$⊢\left(\phi \wedge y\in S\right)\to ⦋y/x⦌A\in ℝ$$
138	137	recnd	$$⊢\left(\phi \wedge y\in S\right)\to ⦋y/x⦌A\in ℂ$$
139	43	r19.21bi	$$⊢\left(\phi \wedge y\in S\right)\to ⦋y/x⦌B\in ℝ$$
140	52	oveq2i	$$⊢\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\frac{d\left(y\in S⟼⦋y/x⦌A\right)}{d_{ℝ}y}$$
141	10 140 41	3eqtr3g	$$⊢\phi \to \frac{d\left(y\in S⟼⦋y/x⦌A\right)}{d_{ℝ}y}=\left(y\in S⟼⦋y/x⦌B\right)$$
142	102 119	sstrid	$$⊢\phi \to \left(X,Y\right)\subseteq S$$
143	101 138 139 141 142 111 82 113	dvmptres	$$⊢\phi \to \frac{d\left(y\in \left(X,Y\right)⟼⦋y/x⦌A\right)}{d_{ℝ}y}=\left(y\in \left(X,Y\right)⟼⦋y/x⦌B\right)$$
144	102	sseli	$$⊢y\in \left(X,Y\right)\to y\in \left[X,Y\right]$$
145		simpl	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \phi$$
146	119	sselda	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\in S$$
147	16	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to Y\in S$$
148	4	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to D\in ℝ$$
149	29	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to X\in ℝ$$
150		elicc2	$$⊢\left(X\in ℝ\wedge Y\in ℝ\right)\to \left(y\in \left[X,Y\right]\leftrightarrow \left(y\in ℝ\wedge X\le y\wedge y\le Y\right)\right)$$
151	29 23 150	syl2anc	$$⊢\phi \to \left(y\in \left[X,Y\right]\leftrightarrow \left(y\in ℝ\wedge X\le y\wedge y\le Y\right)\right)$$
152	151	biimpa	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(y\in ℝ\wedge X\le y\wedge y\le Y\right)$$
153	152	simp1d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\in ℝ$$
154	17	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to D\le X$$
155	152	simp2d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to X\le y$$
156	148 149 153 154 155	letrd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to D\le y$$
157	152	simp3d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\le Y$$
158	19	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to Y\le U$$
159		simp2r	$$⊢\left(\phi \wedge \left(y\in S\wedge Y\in S\right)\wedge \left(D\le y\wedge y\le Y\wedge Y\le U\right)\right)\to Y\in S$$
160		eleq1	$$⊢k=Y\to \left(k\in S\leftrightarrow Y\in S\right)$$
161	160	anbi2d	$$⊢k=Y\to \left(\left(y\in S\wedge k\in S\right)\leftrightarrow \left(y\in S\wedge Y\in S\right)\right)$$
162		breq2	$$⊢k=Y\to \left(y\le k\leftrightarrow y\le Y\right)$$
163		breq1	$$⊢k=Y\to \left(k\le U\leftrightarrow Y\le U\right)$$
164	162 163	3anbi23d	$$⊢k=Y\to \left(\left(D\le y\wedge y\le k\wedge k\le U\right)\leftrightarrow \left(D\le y\wedge y\le Y\wedge Y\le U\right)\right)$$
165	161 164	3anbi23d	$$⊢k=Y\to \left(\left(\phi \wedge \left(y\in S\wedge k\in S\right)\wedge \left(D\le y\wedge y\le k\wedge k\le U\right)\right)\leftrightarrow \left(\phi \wedge \left(y\in S\wedge Y\in S\right)\wedge \left(D\le y\wedge y\le Y\wedge Y\le U\right)\right)\right)$$
166		vex	$$⊢k\in \mathrm{V}$$
167	166 11	csbie	$$⊢⦋k/x⦌B=C$$
168		csbeq1	$$⊢k=Y\to ⦋k/x⦌B=⦋Y/x⦌B$$
169	167 168	syl5eqr	$$⊢k=Y\to C=⦋Y/x⦌B$$
170	169	breq1d	$$⊢k=Y\to \left(C\le ⦋y/x⦌B\leftrightarrow ⦋Y/x⦌B\le ⦋y/x⦌B\right)$$
171	165 170	imbi12d	$$⊢k=Y\to \left(\left(\left(\phi \wedge \left(y\in S\wedge k\in S\right)\wedge \left(D\le y\wedge y\le k\wedge k\le U\right)\right)\to C\le ⦋y/x⦌B\right)\leftrightarrow \left(\left(\phi \wedge \left(y\in S\wedge Y\in S\right)\wedge \left(D\le y\wedge y\le Y\wedge Y\le U\right)\right)\to ⦋Y/x⦌B\le ⦋y/x⦌B\right)\right)$$
172		nfv	$$⊢Ⅎx\left(\phi \wedge \left(y\in S\wedge k\in S\right)\wedge \left(D\le y\wedge y\le k\wedge k\le U\right)\right)$$
173		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
174		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
175	173 174 39	nfbr	$$⊢ℲxC\le ⦋y/x⦌B$$
176	172 175	nfim	$$⊢Ⅎx\left(\left(\phi \wedge \left(y\in S\wedge k\in S\right)\wedge \left(D\le y\wedge y\le k\wedge k\le U\right)\right)\to C\le ⦋y/x⦌B\right)$$
177		eleq1	$$⊢x=y\to \left(x\in S\leftrightarrow y\in S\right)$$
178	177	anbi1d	$$⊢x=y\to \left(\left(x\in S\wedge k\in S\right)\leftrightarrow \left(y\in S\wedge k\in S\right)\right)$$
179		breq2	$$⊢x=y\to \left(D\le x\leftrightarrow D\le y\right)$$
180		breq1	$$⊢x=y\to \left(x\le k\leftrightarrow y\le k\right)$$
181	179 180	3anbi12d	$$⊢x=y\to \left(\left(D\le x\wedge x\le k\wedge k\le U\right)\leftrightarrow \left(D\le y\wedge y\le k\wedge k\le U\right)\right)$$
182	178 181	3anbi23d	$$⊢x=y\to \left(\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)\leftrightarrow \left(\phi \wedge \left(y\in S\wedge k\in S\right)\wedge \left(D\le y\wedge y\le k\wedge k\le U\right)\right)\right)$$
183	40	breq2d	$$⊢x=y\to \left(C\le B\leftrightarrow C\le ⦋y/x⦌B\right)$$
184	182 183	imbi12d	$$⊢x=y\to \left(\left(\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\right)\leftrightarrow \left(\left(\phi \wedge \left(y\in S\wedge k\in S\right)\wedge \left(D\le y\wedge y\le k\wedge k\le U\right)\right)\to C\le ⦋y/x⦌B\right)\right)$$
185	176 184 13	chvarfv	$$⊢\left(\phi \wedge \left(y\in S\wedge k\in S\right)\wedge \left(D\le y\wedge y\le k\wedge k\le U\right)\right)\to C\le ⦋y/x⦌B$$
186	171 185	vtoclg	$$⊢Y\in S\to \left(\left(\phi \wedge \left(y\in S\wedge Y\in S\right)\wedge \left(D\le y\wedge y\le Y\wedge Y\le U\right)\right)\to ⦋Y/x⦌B\le ⦋y/x⦌B\right)$$
187	159 186	mpcom	$$⊢\left(\phi \wedge \left(y\in S\wedge Y\in S\right)\wedge \left(D\le y\wedge y\le Y\wedge Y\le U\right)\right)\to ⦋Y/x⦌B\le ⦋y/x⦌B$$
188	145 146 147 156 157 158 187	syl123anc	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋Y/x⦌B\le ⦋y/x⦌B$$
189	144 188	sylan2	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to ⦋Y/x⦌B\le ⦋y/x⦌B$$
190	29	rexrd	$$⊢\phi \to X\in {ℝ}^{*}$$
191	23	rexrd	$$⊢\phi \to Y\in {ℝ}^{*}$$
192		lbicc2	$$⊢\left(X\in {ℝ}^{*}\wedge Y\in {ℝ}^{*}\wedge X\le Y\right)\to X\in \left[X,Y\right]$$
193	190 191 18 192	syl3anc	$$⊢\phi \to X\in \left[X,Y\right]$$
194		ubicc2	$$⊢\left(X\in {ℝ}^{*}\wedge Y\in {ℝ}^{*}\wedge X\le Y\right)\to Y\in \left[X,Y\right]$$
195	190 191 18 194	syl3anc	$$⊢\phi \to Y\in \left[X,Y\right]$$
196		oveq2	$$⊢y=X\to ⦋Y/x⦌By=⦋Y/x⦌BX$$
197		oveq2	$$⊢y=Y\to ⦋Y/x⦌By=⦋Y/x⦌BY$$
198	29 23 99 118 136 143 189 193 195 18 196 62 197 46	dvle	$$⊢\phi \to ⦋Y/x⦌BY-⦋Y/x⦌BX\le ⦋Y/x⦌A-⦋X/x⦌A$$
199	81 198	eqbrtrd	$$⊢\phi \to ⦋Y/x⦌B\left(Y-X\right)\le ⦋Y/x⦌A-⦋X/x⦌A$$
200	77 55 64 199	lesubd	$$⊢\phi \to ⦋X/x⦌A\le ⦋Y/x⦌A-⦋Y/x⦌B\left(Y-X\right)$$
201	74	recnd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B\in ℂ$$
202	45	recnd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B\in ℂ$$
203	55	recnd	$$⊢\phi \to ⦋Y/x⦌A\in ℂ$$
204	201 202 203	subsubd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-\left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\right)=\left(X-⌊X⌋\right)⦋Y/x⦌B-\left(Y-⌊X⌋\right)⦋Y/x⦌B+⦋Y/x⦌A$$
205	202 201	negsubdi2d	$$⊢\phi \to -\left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-\left(X-⌊X⌋\right)⦋Y/x⦌B\right)=\left(X-⌊X⌋\right)⦋Y/x⦌B-\left(Y-⌊X⌋\right)⦋Y/x⦌B$$
206	31	recnd	$$⊢\phi \to ⌊X⌋\in ℂ$$
207	79 80 206	nnncan2d	$$⊢\phi \to Y-⌊X⌋-\left(X-⌊X⌋\right)=Y-X$$
208	207	oveq1d	$$⊢\phi \to \left(Y-⌊X⌋-\left(X-⌊X⌋\right)\right)⦋Y/x⦌B=\left(Y-X\right)⦋Y/x⦌B$$
209	32	recnd	$$⊢\phi \to Y-⌊X⌋\in ℂ$$
210	57	recnd	$$⊢\phi \to X-⌊X⌋\in ℂ$$
211	209 210 78	subdird	$$⊢\phi \to \left(Y-⌊X⌋-\left(X-⌊X⌋\right)\right)⦋Y/x⦌B=\left(Y-⌊X⌋\right)⦋Y/x⦌B-\left(X-⌊X⌋\right)⦋Y/x⦌B$$
212	76	recnd	$$⊢\phi \to Y-X\in ℂ$$
213	212 78	mulcomd	$$⊢\phi \to \left(Y-X\right)⦋Y/x⦌B=⦋Y/x⦌B\left(Y-X\right)$$
214	208 211 213	3eqtr3d	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-\left(X-⌊X⌋\right)⦋Y/x⦌B=⦋Y/x⦌B\left(Y-X\right)$$
215	214	negeqd	$$⊢\phi \to -\left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-\left(X-⌊X⌋\right)⦋Y/x⦌B\right)=-⦋Y/x⦌B\left(Y-X\right)$$
216	205 215	eqtr3d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-\left(Y-⌊X⌋\right)⦋Y/x⦌B=-⦋Y/x⦌B\left(Y-X\right)$$
217	216	oveq1d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-\left(Y-⌊X⌋\right)⦋Y/x⦌B+⦋Y/x⦌A=-⦋Y/x⦌B\left(Y-X\right)+⦋Y/x⦌A$$
218	77	recnd	$$⊢\phi \to ⦋Y/x⦌B\left(Y-X\right)\in ℂ$$
219	218 203	negsubdid	$$⊢\phi \to -\left(⦋Y/x⦌B\left(Y-X\right)-⦋Y/x⦌A\right)=-⦋Y/x⦌B\left(Y-X\right)+⦋Y/x⦌A$$
220	217 219	eqtr4d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-\left(Y-⌊X⌋\right)⦋Y/x⦌B+⦋Y/x⦌A=-\left(⦋Y/x⦌B\left(Y-X\right)-⦋Y/x⦌A\right)$$
221	218 203	negsubdi2d	$$⊢\phi \to -\left(⦋Y/x⦌B\left(Y-X\right)-⦋Y/x⦌A\right)=⦋Y/x⦌A-⦋Y/x⦌B\left(Y-X\right)$$
222	204 220 221	3eqtrd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-\left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\right)=⦋Y/x⦌A-⦋Y/x⦌B\left(Y-X\right)$$
223	200 222	breqtrrd	$$⊢\phi \to ⦋X/x⦌A\le \left(X-⌊X⌋\right)⦋Y/x⦌B-\left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\right)$$
224	64 74 56 223	lesubd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\le \left(X-⌊X⌋\right)⦋Y/x⦌B-⦋X/x⦌A$$
225		flle	$$⊢X\in ℝ\to ⌊X⌋\le X$$
226	29 225	syl	$$⊢\phi \to ⌊X⌋\le X$$
227	29 31	subge0d	$$⊢\phi \to \left(0\le X-⌊X⌋\leftrightarrow ⌊X⌋\le X\right)$$
228	226 227	mpbird	$$⊢\phi \to 0\le X-⌊X⌋$$
229	58	breq2d	$$⊢y=X\to \left(⦋Y/x⦌B\le ⦋y/x⦌B\leftrightarrow ⦋Y/x⦌B\le ⦋X/x⦌B\right)$$
230	188	ralrimiva	$$⊢\phi \to \forall y\in \left[X,Y\right]⦋Y/x⦌B\le ⦋y/x⦌B$$
231	229 230 193	rspcdva	$$⊢\phi \to ⦋Y/x⦌B\le ⦋X/x⦌B$$
232	44 60 57 228 231	lemul2ad	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B\le \left(X-⌊X⌋\right)⦋X/x⦌B$$
233	74 61 64 232	lesub1dd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-⦋X/x⦌A\le \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A$$
234	56 75 65 224 233	letrd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\le \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A$$
235	56 65 73 234	leadd1dd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A+\sum _{k=M}^{⌊X⌋}C\le \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A+\sum _{k=M}^{⌊X⌋}C$$
236	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20	dvfsumlem1	$$⊢\phi \to H\left(Y\right)=\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A+\sum _{k=M}^{⌊X⌋}C$$
237	29	leidd	$$⊢\phi \to X\le X$$
238	190 191 12 18 19	xrletrd	$$⊢\phi \to X\le U$$
239		fllep1	$$⊢X\in ℝ\to X\le ⌊X⌋+1$$
240	29 239	syl	$$⊢\phi \to X\le ⌊X⌋+1$$
241	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 237 238 240	dvfsumlem1	$$⊢\phi \to H\left(X\right)=\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A+\sum _{k=M}^{⌊X⌋}C$$
242	235 236 241	3brtr4d	$$⊢\phi \to H\left(Y\right)\le H\left(X\right)$$
243	65 60	resubcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A-⦋X/x⦌B\in ℝ$$
244	56 44	resubcld	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A-⦋Y/x⦌B\in ℝ$$
245		peano2rem	$$⊢X-⌊X⌋\in ℝ\to X-⌊X⌋-1\in ℝ$$
246	57 245	syl	$$⊢\phi \to X-⌊X⌋-1\in ℝ$$
247	246 60	remulcld	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B\in ℝ$$
248	247 64	resubcld	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-⦋X/x⦌A\in ℝ$$
249		peano2rem	$$⊢Y-⌊X⌋\in ℝ\to Y-⌊X⌋-1\in ℝ$$
250	32 249	syl	$$⊢\phi \to Y-⌊X⌋-1\in ℝ$$
251	250 60	remulcld	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B\in ℝ$$
252	251 55	resubcld	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B-⦋Y/x⦌A\in ℝ$$
253	250 44	remulcld	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B\in ℝ$$
254	253 55	resubcld	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B-⦋Y/x⦌A\in ℝ$$
255	247	recnd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B\in ℂ$$
256	251	recnd	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B\in ℂ$$
257	255 256	subcld	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(Y-⌊X⌋-1\right)⦋X/x⦌B\in ℂ$$
258	257 203	addcomd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(Y-⌊X⌋-1\right)⦋X/x⦌B+⦋Y/x⦌A=⦋Y/x⦌A+\left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(Y-⌊X⌋-1\right)⦋X/x⦌B$$
259	255 256 203	subsubd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(\left(Y-⌊X⌋-1\right)⦋X/x⦌B-⦋Y/x⦌A\right)=\left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(Y-⌊X⌋-1\right)⦋X/x⦌B+⦋Y/x⦌A$$
260	203 256 255	subsub2d	$$⊢\phi \to ⦋Y/x⦌A-\left(\left(Y-⌊X⌋-1\right)⦋X/x⦌B-\left(X-⌊X⌋-1\right)⦋X/x⦌B\right)=⦋Y/x⦌A+\left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(Y-⌊X⌋-1\right)⦋X/x⦌B$$
261	258 259 260	3eqtr4d	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(\left(Y-⌊X⌋-1\right)⦋X/x⦌B-⦋Y/x⦌A\right)=⦋Y/x⦌A-\left(\left(Y-⌊X⌋-1\right)⦋X/x⦌B-\left(X-⌊X⌋-1\right)⦋X/x⦌B\right)$$
262		1cnd	$$⊢\phi \to 1\in ℂ$$
263	209 210 262	nnncan2d	$$⊢\phi \to \left(Y-⌊X⌋\right)-1-\left(X-⌊X⌋-1\right)=Y-⌊X⌋-\left(X-⌊X⌋\right)$$
264	263 207	eqtrd	$$⊢\phi \to \left(Y-⌊X⌋\right)-1-\left(X-⌊X⌋-1\right)=Y-X$$
265	264	oveq1d	$$⊢\phi \to \left(\left(Y-⌊X⌋\right)-1-\left(X-⌊X⌋-1\right)\right)⦋X/x⦌B=\left(Y-X\right)⦋X/x⦌B$$
266	250	recnd	$$⊢\phi \to Y-⌊X⌋-1\in ℂ$$
267	246	recnd	$$⊢\phi \to X-⌊X⌋-1\in ℂ$$
268	60	recnd	$$⊢\phi \to ⦋X/x⦌B\in ℂ$$
269	266 267 268	subdird	$$⊢\phi \to \left(\left(Y-⌊X⌋\right)-1-\left(X-⌊X⌋-1\right)\right)⦋X/x⦌B=\left(Y-⌊X⌋-1\right)⦋X/x⦌B-\left(X-⌊X⌋-1\right)⦋X/x⦌B$$
270	212 268	mulcomd	$$⊢\phi \to \left(Y-X\right)⦋X/x⦌B=⦋X/x⦌B\left(Y-X\right)$$
271	265 269 270	3eqtr3d	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B-\left(X-⌊X⌋-1\right)⦋X/x⦌B=⦋X/x⦌B\left(Y-X\right)$$
272	271	oveq2d	$$⊢\phi \to ⦋Y/x⦌A-\left(\left(Y-⌊X⌋-1\right)⦋X/x⦌B-\left(X-⌊X⌋-1\right)⦋X/x⦌B\right)=⦋Y/x⦌A-⦋X/x⦌B\left(Y-X\right)$$
273	261 272	eqtrd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(\left(Y-⌊X⌋-1\right)⦋X/x⦌B-⦋Y/x⦌A\right)=⦋Y/x⦌A-⦋X/x⦌B\left(Y-X\right)$$
274	60 76	remulcld	$$⊢\phi \to ⦋X/x⦌B\left(Y-X\right)\in ℝ$$
275		cncfmptc	$$⊢\left(⦋X/x⦌B\in ℝ\wedge \left[X,Y\right]\subseteq ℂ\wedge ℝ\subseteq ℂ\right)\to \left(y\in \left[X,Y\right]⟼⦋X/x⦌B\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
276	60 92 93 275	syl3anc	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋X/x⦌B\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
277		remulcl	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋X/x⦌By\in ℝ$$
278	82 83 276 97 91 277	cncfmpt2ss	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
279	101 105 106 114 268	dvmptcmul	$$⊢\phi \to \frac{d\left(y\in \left(X,Y\right)⟼⦋X/x⦌By\right)}{d_{ℝ}y}=\left(y\in \left(X,Y\right)⟼⦋X/x⦌B\cdot 1\right)$$
280	268	mulid1d	$$⊢\phi \to ⦋X/x⦌B\cdot 1=⦋X/x⦌B$$
281	280	mpteq2dv	$$⊢\phi \to \left(y\in \left(X,Y\right)⟼⦋X/x⦌B\cdot 1\right)=\left(y\in \left(X,Y\right)⟼⦋X/x⦌B\right)$$
282	279 281	eqtrd	$$⊢\phi \to \frac{d\left(y\in \left(X,Y\right)⟼⦋X/x⦌By\right)}{d_{ℝ}y}=\left(y\in \left(X,Y\right)⟼⦋X/x⦌B\right)$$
283	15	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to X\in S$$
284	153	rexrd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\in {ℝ}^{*}$$
285	191	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to Y\in {ℝ}^{*}$$
286	12	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to U\in {ℝ}^{*}$$
287	284 285 286 157 158	xrletrd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\le U$$
288		vex	$$⊢y\in \mathrm{V}$$
289		eleq1	$$⊢k=y\to \left(k\in S\leftrightarrow y\in S\right)$$
290	289	anbi2d	$$⊢k=y\to \left(\left(X\in S\wedge k\in S\right)\leftrightarrow \left(X\in S\wedge y\in S\right)\right)$$
291		breq2	$$⊢k=y\to \left(X\le k\leftrightarrow X\le y\right)$$
292		breq1	$$⊢k=y\to \left(k\le U\leftrightarrow y\le U\right)$$
293	291 292	3anbi23d	$$⊢k=y\to \left(\left(D\le X\wedge X\le k\wedge k\le U\right)\leftrightarrow \left(D\le X\wedge X\le y\wedge y\le U\right)\right)$$
294	290 293	3anbi23d	$$⊢k=y\to \left(\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)\leftrightarrow \left(\phi \wedge \left(X\in S\wedge y\in S\right)\wedge \left(D\le X\wedge X\le y\wedge y\le U\right)\right)\right)$$
295		csbeq1	$$⊢k=y\to ⦋k/x⦌B=⦋y/x⦌B$$
296	167 295	syl5eqr	$$⊢k=y\to C=⦋y/x⦌B$$
297	296	breq1d	$$⊢k=y\to \left(C\le ⦋X/x⦌B\leftrightarrow ⦋y/x⦌B\le ⦋X/x⦌B\right)$$
298	294 297	imbi12d	$$⊢k=y\to \left(\left(\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 ⦋X/x⦌B\right)\leftrightarrow \left(\left(\phi \wedge \left(X\in S\wedge y\in S\right)\wedge \left(D\le X\wedge X\le y\wedge y\le U\right)\right)\to ⦋y/x⦌B\le ⦋X/x⦌B\right)\right)$$
299		simp2l	$$⊢\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 X\in S$$
300		nfv	$$⊢Ⅎx\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)$$
301		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋X/x⦌B$$
302	173 174 301	nfbr	$$⊢ℲxC\le ⦋X/x⦌B$$
303	300 302	nfim	$$⊢Ⅎx\left(\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 ⦋X/x⦌B\right)$$
304		eleq1	$$⊢x=X\to \left(x\in S\leftrightarrow X\in S\right)$$
305	304	anbi1d	$$⊢x=X\to \left(\left(x\in S\wedge k\in S\right)\leftrightarrow \left(X\in S\wedge k\in S\right)\right)$$
306		breq2	$$⊢x=X\to \left(D\le x\leftrightarrow D\le X\right)$$
307		breq1	$$⊢x=X\to \left(x\le k\leftrightarrow X\le k\right)$$
308	306 307	3anbi12d	$$⊢x=X\to \left(\left(D\le x\wedge x\le k\wedge k\le U\right)\leftrightarrow \left(D\le X\wedge X\le k\wedge k\le U\right)\right)$$
309	305 308	3anbi23d	$$⊢x=X\to \left(\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)\leftrightarrow \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)\right)$$
310		csbeq1a	$$⊢x=X\to B=⦋X/x⦌B$$
311	310	breq2d	$$⊢x=X\to \left(C\le B\leftrightarrow C\le ⦋X/x⦌B\right)$$
312	309 311	imbi12d	$$⊢x=X\to \left(\left(\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\right)\leftrightarrow \left(\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 ⦋X/x⦌B\right)\right)$$
313	303 312 13	vtoclg1f	$$⊢X\in S\to \left(\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 ⦋X/x⦌B\right)$$
314	299 313	mpcom	$$⊢\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 ⦋X/x⦌B$$
315	288 298 314	vtocl	$$⊢\left(\phi \wedge \left(X\in S\wedge y\in S\right)\wedge \left(D\le X\wedge X\le y\wedge y\le U\right)\right)\to ⦋y/x⦌B\le ⦋X/x⦌B$$
316	145 283 146 154 155 287 315	syl123anc	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋y/x⦌B\le ⦋X/x⦌B$$
317	144 316	sylan2	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to ⦋y/x⦌B\le ⦋X/x⦌B$$
318		oveq2	$$⊢y=X\to ⦋X/x⦌By=⦋X/x⦌BX$$
319		oveq2	$$⊢y=Y\to ⦋X/x⦌By=⦋X/x⦌BY$$
320	29 23 136 143 278 282 317 193 195 18 62 318 46 319	dvle	$$⊢\phi \to ⦋Y/x⦌A-⦋X/x⦌A\le ⦋X/x⦌BY-⦋X/x⦌BX$$
321	268 79 80	subdid	$$⊢\phi \to ⦋X/x⦌B\left(Y-X\right)=⦋X/x⦌BY-⦋X/x⦌BX$$
322	320 321	breqtrrd	$$⊢\phi \to ⦋Y/x⦌A-⦋X/x⦌A\le ⦋X/x⦌B\left(Y-X\right)$$
323	55 64 274 322	subled	$$⊢\phi \to ⦋Y/x⦌A-⦋X/x⦌B\left(Y-X\right)\le ⦋X/x⦌A$$
324	273 323	eqbrtrd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(\left(Y-⌊X⌋-1\right)⦋X/x⦌B-⦋Y/x⦌A\right)\le ⦋X/x⦌A$$
325	247 252 64 324	subled	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-⦋X/x⦌A\le \left(Y-⌊X⌋-1\right)⦋X/x⦌B-⦋Y/x⦌A$$
326	250	renegcld	$$⊢\phi \to -\left(Y-⌊X⌋-1\right)\in ℝ$$
327		1red	$$⊢\phi \to 1\in ℝ$$
328	23 31 327	lesubadd2d	$$⊢\phi \to \left(Y-⌊X⌋\le 1\leftrightarrow Y\le ⌊X⌋+1\right)$$
329	20 328	mpbird	$$⊢\phi \to Y-⌊X⌋\le 1$$
330	32 327	suble0d	$$⊢\phi \to \left(Y-⌊X⌋-1\le 0\leftrightarrow Y-⌊X⌋\le 1\right)$$
331	329 330	mpbird	$$⊢\phi \to Y-⌊X⌋-1\le 0$$
332	250	le0neg1d	$$⊢\phi \to \left(Y-⌊X⌋-1\le 0\leftrightarrow 0\le -\left(Y-⌊X⌋-1\right)\right)$$
333	331 332	mpbid	$$⊢\phi \to 0\le -\left(Y-⌊X⌋-1\right)$$
334	44 60 326 333 231	lemul2ad	$$⊢\phi \to \left(-\left(Y-⌊X⌋-1\right)\right)⦋Y/x⦌B\le \left(-\left(Y-⌊X⌋-1\right)\right)⦋X/x⦌B$$
335	266 78	mulneg1d	$$⊢\phi \to \left(-\left(Y-⌊X⌋-1\right)\right)⦋Y/x⦌B=-\left(Y-⌊X⌋-1\right)⦋Y/x⦌B$$
336	266 268	mulneg1d	$$⊢\phi \to \left(-\left(Y-⌊X⌋-1\right)\right)⦋X/x⦌B=-\left(Y-⌊X⌋-1\right)⦋X/x⦌B$$
337	334 335 336	3brtr3d	$$⊢\phi \to -\left(Y-⌊X⌋-1\right)⦋Y/x⦌B\le -\left(Y-⌊X⌋-1\right)⦋X/x⦌B$$
338	251 253	lenegd	$$⊢\phi \to \left(\left(Y-⌊X⌋-1\right)⦋X/x⦌B\le \left(Y-⌊X⌋-1\right)⦋Y/x⦌B\leftrightarrow -\left(Y-⌊X⌋-1\right)⦋Y/x⦌B\le -\left(Y-⌊X⌋-1\right)⦋X/x⦌B\right)$$
339	337 338	mpbird	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B\le \left(Y-⌊X⌋-1\right)⦋Y/x⦌B$$
340	251 253 55 339	lesub1dd	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B-⦋Y/x⦌A\le \left(Y-⌊X⌋-1\right)⦋Y/x⦌B-⦋Y/x⦌A$$
341	248 252 254 325 340	letrd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-⦋X/x⦌A\le \left(Y-⌊X⌋-1\right)⦋Y/x⦌B-⦋Y/x⦌A$$
342	210 262 268	subdird	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B=\left(X-⌊X⌋\right)⦋X/x⦌B-1⦋X/x⦌B$$
343	268	mulid2d	$$⊢\phi \to 1⦋X/x⦌B=⦋X/x⦌B$$
344	343	oveq2d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-1⦋X/x⦌B=\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌B$$
345	342 344	eqtrd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B=\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌B$$
346	345	oveq1d	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-⦋X/x⦌A=\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌B-⦋X/x⦌A$$
347	209 262 78	subdird	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B=\left(Y-⌊X⌋\right)⦋Y/x⦌B-1⦋Y/x⦌B$$
348	78	mulid2d	$$⊢\phi \to 1⦋Y/x⦌B=⦋Y/x⦌B$$
349	348	oveq2d	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-1⦋Y/x⦌B=\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌B$$
350	347 349	eqtrd	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B=\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌B$$
351	350	oveq1d	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B-⦋Y/x⦌A=\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌B-⦋Y/x⦌A$$
352	341 346 351	3brtr3d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌B-⦋X/x⦌A\le \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌B-⦋Y/x⦌A$$
353	61	recnd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B\in ℂ$$
354	64	recnd	$$⊢\phi \to ⦋X/x⦌A\in ℂ$$
355	353 354 268	sub32d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A-⦋X/x⦌B=\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌B-⦋X/x⦌A$$
356	202 203 78	sub32d	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A-⦋Y/x⦌B=\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌B-⦋Y/x⦌A$$
357	352 355 356	3brtr4d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A-⦋X/x⦌B\le \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A-⦋Y/x⦌B$$
358	243 244 73 357	leadd1dd	$$⊢\phi \to \left(\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A\right)-⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C\le \left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\right)-⦋Y/x⦌B+\sum _{k=M}^{⌊X⌋}C$$
359	65	recnd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A\in ℂ$$
360	73	recnd	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C\in ℂ$$
361	359 360 268	addsubd	$$⊢\phi \to \left(\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A\right)+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌B=\left(\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A\right)-⦋X/x⦌B+\sum _{k=M}^{⌊X⌋}C$$
362	56	recnd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\in ℂ$$
363	362 360 78	addsubd	$$⊢\phi \to \left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\right)+\sum _{k=M}^{⌊X⌋}C-⦋Y/x⦌B=\left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\right)-⦋Y/x⦌B+\sum _{k=M}^{⌊X⌋}C$$
364	358 361 363	3brtr4d	$$⊢\phi \to \left(\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A\right)+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌B\le \left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\right)+\sum _{k=M}^{⌊X⌋}C-⦋Y/x⦌B$$
365	241	oveq1d	$$⊢\phi \to H\left(X\right)-⦋X/x⦌B=\left(\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A\right)+\sum _{k=M}^{⌊X⌋}C-⦋X/x⦌B$$
366	236	oveq1d	$$⊢\phi \to H\left(Y\right)-⦋Y/x⦌B=\left(\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\right)+\sum _{k=M}^{⌊X⌋}C-⦋Y/x⦌B$$
367	364 365 366	3brtr4d	$$⊢\phi \to H\left(X\right)-⦋X/x⦌B\le H\left(Y\right)-⦋Y/x⦌B$$
368	242 367	jca	$$⊢\phi \to \left(H\left(Y\right)\le H\left(X\right)\wedge H\left(X\right)-⦋X/x⦌B\le H\left(Y\right)-⦋Y/x⦌B\right)$$