Theorem dvfsumlem2

Description: Lemma for dvfsumrlim . (Contributed by Mario Carneiro, 17-May-2016) Avoid ax-mulf . (Revised by GG, 16-Mar-2025)

	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	sselid	$$⊢\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	mpomulcn	$$⊢\left(u\in ℂ,v\in ℂ⟼uv\right)\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		csbeq1	$$⊢z=Y\to ⦋z/x⦌B=⦋Y/x⦌B$$
85	84	eleq1d	$$⊢z=Y\to \left(⦋z/x⦌B\in ℝ\leftrightarrow ⦋Y/x⦌B\in ℝ\right)$$
86		nfcv	$$⊢\underset{\_}{Ⅎ}zB$$
87		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋z/x⦌B$$
88		csbeq1a	$$⊢x=z\to B=⦋z/x⦌B$$
89	86 87 88	cbvmpt	$$⊢\left(x\in S⟼B\right)=\left(z\in S⟼⦋z/x⦌B\right)$$
90	89	fmpt	$$⊢\forall z\in S⦋z/x⦌B\in ℝ\leftrightarrow \left(x\in S⟼B\right):S⟶ℝ$$
91	37 90	sylibr	$$⊢\phi \to \forall z\in S⦋z/x⦌B\in ℝ$$
92	85 91 16	rspcdva	$$⊢\phi \to ⦋Y/x⦌B\in ℝ$$
93		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
94	93	a1i	$$⊢\phi \to \mathrm{+\infty }\in {ℝ}^{*}$$
95	28	simprd	$$⊢\phi \to T<X$$
96	23	ltpnfd	$$⊢\phi \to Y<\mathrm{+\infty }$$
97		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)$$
98	25 94 95 96 97	syl22anc	$$⊢\phi \to \left[X,Y\right]\subseteq \left(T,\mathrm{+\infty }\right)$$
99	98 21	sstrdi	$$⊢\phi \to \left[X,Y\right]\subseteq ℝ$$
100		ax-resscn	$$⊢ℝ\subseteq ℂ$$
101	99 100	sstrdi	$$⊢\phi \to \left[X,Y\right]\subseteq ℂ$$
102	100	a1i	$$⊢\phi \to ℝ\subseteq ℂ$$
103		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}{⟶}ℝ$$
104	92 101 102 103	syl3anc	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋Y/x⦌B\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
105		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}{⟶}ℝ$$
106	99 100 105	sylancl	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
107		remulcl	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋Y/x⦌By\in ℝ$$
108		simpl	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋Y/x⦌B\in ℝ$$
109	108	recnd	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋Y/x⦌B\in ℂ$$
110		simpr	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to y\in ℝ$$
111	110	recnd	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to y\in ℂ$$
112	109 111	jca	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to \left(⦋Y/x⦌B\in ℂ\wedge y\in ℂ\right)$$
113		ovmpot	$$⊢\left(⦋Y/x⦌B\in ℂ\wedge y\in ℂ\right)\to ⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y=⦋Y/x⦌By$$
114	113	eqcomd	$$⊢\left(⦋Y/x⦌B\in ℂ\wedge y\in ℂ\right)\to ⦋Y/x⦌By=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y$$
115	112 114	syl	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋Y/x⦌By=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y$$
116	115	eleq1d	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to \left(⦋Y/x⦌By\in ℝ\leftrightarrow ⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\in ℝ\right)$$
117	116	biimpd	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to \left(⦋Y/x⦌By\in ℝ\to ⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\in ℝ\right)$$
118	107 117	mpd	$$⊢\left(⦋Y/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\in ℝ$$
119	82 83 104 106 100 118	cncfmpt2ss	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
120		df-mpt	$$⊢\left(y\in \left[X,Y\right]⟼⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}$$
121	120	eleq1i	$$⊢\left(y\in \left[X,Y\right]⟼⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\leftrightarrow \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ$$
122	121	biimpi	$$⊢\left(y\in \left[X,Y\right]⟼⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ$$
123	119 122	syl	$$⊢\phi \to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ$$
124		idd	$$⊢\phi \to \left(y\in \left[X,Y\right]\to y\in \left[X,Y\right]\right)$$
125	124	a1dd	$$⊢\phi \to \left(y\in \left[X,Y\right]\to \left(w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\to y\in \left[X,Y\right]\right)\right)$$
126	125	impd	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\to y\in \left[X,Y\right]\right)$$
127		csbeq1	$$⊢m=Y\to ⦋m/x⦌B=⦋Y/x⦌B$$
128	127	eleq1d	$$⊢m=Y\to \left(⦋m/x⦌B\in ℝ\leftrightarrow ⦋Y/x⦌B\in ℝ\right)$$
129		nfcv	$$⊢\underset{\_}{Ⅎ}mB$$
130		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋m/x⦌B$$
131		csbeq1a	$$⊢x=m\to B=⦋m/x⦌B$$
132	129 130 131	cbvmpt	$$⊢\left(x\in S⟼B\right)=\left(m\in S⟼⦋m/x⦌B\right)$$
133	132	fmpt	$$⊢\forall m\in S⦋m/x⦌B\in ℝ\leftrightarrow \left(x\in S⟼B\right):S⟶ℝ$$
134	37 133	sylibr	$$⊢\phi \to \forall m\in S⦋m/x⦌B\in ℝ$$
135	128 134 16	rspcdva	$$⊢\phi \to ⦋Y/x⦌B\in ℝ$$
136	135	recnd	$$⊢\phi \to ⦋Y/x⦌B\in ℂ$$
137	136	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋Y/x⦌B\in ℂ$$
138		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)$$
139	29 23 138	syl2anc	$$⊢\phi \to \left(y\in \left[X,Y\right]\leftrightarrow \left(y\in ℝ\wedge X\le y\wedge y\le Y\right)\right)$$
140	139	biimpa	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(y\in ℝ\wedge X\le y\wedge y\le Y\right)$$
141	140	simp1d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\in ℝ$$
142	141	recnd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\in ℂ$$
143	137 142	jca	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(⦋Y/x⦌B\in ℂ\wedge y\in ℂ\right)$$
144	143 113	syl	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y=⦋Y/x⦌By$$
145	144	eqeq2d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\leftrightarrow w=⦋Y/x⦌By\right)$$
146	145	biimpd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\to w=⦋Y/x⦌By\right)$$
147	146	ex	$$⊢\phi \to \left(y\in \left[X,Y\right]\to \left(w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\to w=⦋Y/x⦌By\right)\right)$$
148	147	impd	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\to w=⦋Y/x⦌By\right)$$
149	126 148	jcad	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\to \left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\right)$$
150	124	a1dd	$$⊢\phi \to \left(y\in \left[X,Y\right]\to \left(w=⦋Y/x⦌By\to y\in \left[X,Y\right]\right)\right)$$
151	150	impd	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\to y\in \left[X,Y\right]\right)$$
152		csbeq1	$$⊢k=Y\to ⦋k/x⦌B=⦋Y/x⦌B$$
153	152	eleq1d	$$⊢k=Y\to \left(⦋k/x⦌B\in ℝ\leftrightarrow ⦋Y/x⦌B\in ℝ\right)$$
154		nfcv	$$⊢\underset{\_}{Ⅎ}kB$$
155		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋k/x⦌B$$
156		csbeq1a	$$⊢x=k\to B=⦋k/x⦌B$$
157	154 155 156	cbvmpt	$$⊢\left(x\in S⟼B\right)=\left(k\in S⟼⦋k/x⦌B\right)$$
158	157	fmpt	$$⊢\forall k\in S⦋k/x⦌B\in ℝ\leftrightarrow \left(x\in S⟼B\right):S⟶ℝ$$
159	37 158	sylibr	$$⊢\phi \to \forall k\in S⦋k/x⦌B\in ℝ$$
160	153 159 16	rspcdva	$$⊢\phi \to ⦋Y/x⦌B\in ℝ$$
161	160	recnd	$$⊢\phi \to ⦋Y/x⦌B\in ℂ$$
162	161	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋Y/x⦌B\in ℂ$$
163	162 142	jca	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(⦋Y/x⦌B\in ℂ\wedge y\in ℂ\right)$$
164	163 114	syl	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋Y/x⦌By=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y$$
165	164	eqeq2d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(w=⦋Y/x⦌By\leftrightarrow w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)$$
166	165	biimpd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(w=⦋Y/x⦌By\to w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)$$
167	166	ex	$$⊢\phi \to \left(y\in \left[X,Y\right]\to \left(w=⦋Y/x⦌By\to w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right)$$
168	167	impd	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\to w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)$$
169	151 168	jcad	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\to \left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right)$$
170	149 169	impbid	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\leftrightarrow \left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\right)$$
171	170	opabbidv	$$⊢\phi \to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\right\}$$
172		df-mpt	$$⊢\left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right)=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\right\}$$
173	172	eqcomi	$$⊢\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\right\}=\left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right)$$
174	173	eqeq2i	$$⊢\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\right\}\leftrightarrow \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right)$$
175	174	biimpi	$$⊢\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌By\right)\right\}\to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right)$$
176	171 175	syl	$$⊢\phi \to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right)$$
177	176	eleq1d	$$⊢\phi \to \left(\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ\leftrightarrow \left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\right)$$
178	177	biimpd	$$⊢\phi \to \left(\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋Y/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ\to \left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\right)$$
179	123 178	mpd	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋Y/x⦌By\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
180		reelprrecn	$$⊢ℝ\in \left\{ℝ,ℂ\right\}$$
181	180	a1i	$$⊢\phi \to ℝ\in \left\{ℝ,ℂ\right\}$$
182		ioossicc	$$⊢\left(X,Y\right)\subseteq \left[X,Y\right]$$
183	182 99	sstrid	$$⊢\phi \to \left(X,Y\right)\subseteq ℝ$$
184	183	sselda	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to y\in ℝ$$
185	184	recnd	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to y\in ℂ$$
186		1cnd	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to 1\in ℂ$$
187		simpr	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\in ℝ$$
188	187	recnd	$$⊢\left(\phi \wedge y\in ℝ\right)\to y\in ℂ$$
189		1cnd	$$⊢\left(\phi \wedge y\in ℝ\right)\to 1\in ℂ$$
190	181	dvmptid	$$⊢\phi \to \frac{d\left(y\in ℝ⟼y\right)}{d_{ℝ}y}=\left(y\in ℝ⟼1\right)$$
191		tgioo4	$$⊢\mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)=\mathrm{TopOpen}\left({ℂ}_{\mathrm{fld}}\right){\upharpoonright }_{𝑡}ℝ$$
192		iooretop	$$⊢\left(X,Y\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
193	192	a1i	$$⊢\phi \to \left(X,Y\right)\in \mathrm{topGen}\left(\mathrm{ran}\left(.\right)\right)$$
194	181 188 189 190 183 191 82 193	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)$$
195	181 185 186 194 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)$$
196	78	mulridd	$$⊢\phi \to ⦋Y/x⦌B\cdot 1=⦋Y/x⦌B$$
197	196	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)$$
198	195 197	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)$$
199	98 1	sseqtrrdi	$$⊢\phi \to \left[X,Y\right]\subseteq S$$
200	199	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)$$
201	7	recnd	$$⊢\left(\phi \wedge x\in S\right)\to A\in ℂ$$
202	201	fmpttd	$$⊢\phi \to \left(x\in S⟼A\right):S⟶ℂ$$
203	10	dmeqd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\mathrm{dom}\left(x\in S⟼B\right)$$
204	8	ralrimiva	$$⊢\phi \to \forall x\in SB\in V$$
205		dmmptg	$$⊢\forall x\in SB\in V\to \mathrm{dom}\left(x\in S⟼B\right)=S$$
206	204 205	syl	$$⊢\phi \to \mathrm{dom}\left(x\in S⟼B\right)=S$$
207	203 206	eqtrd	$$⊢\phi \to \mathrm{dom}\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=S$$
208		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}{⟶}ℂ$$
209	102 202 35 207 208	syl31anc	$$⊢\phi \to \left(x\in S⟼A\right):S\underset{cn}{⟶}ℂ$$
210		cncfcdm	$$⊢\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)$$
211	100 209 210	sylancr	$$⊢\phi \to \left(\left(x\in S⟼A\right):S\underset{cn}{⟶}ℝ\leftrightarrow \left(x\in S⟼A\right):S⟶ℝ\right)$$
212	48 211	mpbird	$$⊢\phi \to \left(x\in S⟼A\right):S\underset{cn}{⟶}ℝ$$
213	52 212	eqeltrrid	$$⊢\phi \to \left(y\in S⟼⦋y/x⦌A\right):S\underset{cn}{⟶}ℝ$$
214		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)$$
215	199 213 214	sylc	$$⊢\phi \to \left({\left(y\in S⟼⦋y/x⦌A\right)\upharpoonright }_{\left[X,Y\right]}\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
216	200 215	eqeltrrd	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋y/x⦌A\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
217	54	r19.21bi	$$⊢\left(\phi \wedge y\in S\right)\to ⦋y/x⦌A\in ℝ$$
218	217	recnd	$$⊢\left(\phi \wedge y\in S\right)\to ⦋y/x⦌A\in ℂ$$
219	43	r19.21bi	$$⊢\left(\phi \wedge y\in S\right)\to ⦋y/x⦌B\in ℝ$$
220	52	oveq2i	$$⊢\frac{d\left(x\in S⟼A\right)}{d_{ℝ}x}=\frac{d\left(y\in S⟼⦋y/x⦌A\right)}{d_{ℝ}y}$$
221	10 220 41	3eqtr3g	$$⊢\phi \to \frac{d\left(y\in S⟼⦋y/x⦌A\right)}{d_{ℝ}y}=\left(y\in S⟼⦋y/x⦌B\right)$$
222	182 199	sstrid	$$⊢\phi \to \left(X,Y\right)\subseteq S$$
223	181 218 219 221 222 191 82 193	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)$$
224	182	sseli	$$⊢y\in \left(X,Y\right)\to y\in \left[X,Y\right]$$
225		simpl	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \phi$$
226	199	sselda	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\in S$$
227	16	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to Y\in S$$
228	4	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to D\in ℝ$$
229	29	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to X\in ℝ$$
230	17	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to D\le X$$
231	140	simp2d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to X\le y$$
232	228 229 141 230 231	letrd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to D\le y$$
233	140	simp3d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\le Y$$
234	19	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to Y\le U$$
235		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$$
236		eleq1	$$⊢k=Y\to \left(k\in S\leftrightarrow Y\in S\right)$$
237	236	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)$$
238		breq2	$$⊢k=Y\to \left(y\le k\leftrightarrow y\le Y\right)$$
239		breq1	$$⊢k=Y\to \left(k\le U\leftrightarrow Y\le U\right)$$
240	238 239	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)$$
241	237 240	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)$$
242		vex	$$⊢k\in \mathrm{V}$$
243	242 11	csbie	$$⊢⦋k/x⦌B=C$$
244	243 152	eqtr3id	$$⊢k=Y\to C=⦋Y/x⦌B$$
245	244	breq1d	$$⊢k=Y\to \left(C\le ⦋y/x⦌B\leftrightarrow ⦋Y/x⦌B\le ⦋y/x⦌B\right)$$
246	241 245	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)$$
247		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)$$
248		nfcv	$$⊢\underset{\_}{Ⅎ}xC$$
249		nfcv	$$⊢\underset{\_}{Ⅎ}x\le$$
250	248 249 39	nfbr	$$⊢ℲxC\le ⦋y/x⦌B$$
251	247 250	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)$$
252		eleq1	$$⊢x=y\to \left(x\in S\leftrightarrow y\in S\right)$$
253	252	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)$$
254		breq2	$$⊢x=y\to \left(D\le x\leftrightarrow D\le y\right)$$
255		breq1	$$⊢x=y\to \left(x\le k\leftrightarrow y\le k\right)$$
256	254 255	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)$$
257	253 256	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)$$
258	40	breq2d	$$⊢x=y\to \left(C\le B\leftrightarrow C\le ⦋y/x⦌B\right)$$
259	257 258	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)$$
260	251 259 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$$
261	246 260	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)$$
262	235 261	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$$
263	225 226 227 232 233 234 262	syl123anc	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋Y/x⦌B\le ⦋y/x⦌B$$
264	224 263	sylan2	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to ⦋Y/x⦌B\le ⦋y/x⦌B$$
265	29	rexrd	$$⊢\phi \to X\in {ℝ}^{*}$$
266	23	rexrd	$$⊢\phi \to Y\in {ℝ}^{*}$$
267		lbicc2	$$⊢\left(X\in {ℝ}^{*}\wedge Y\in {ℝ}^{*}\wedge X\le Y\right)\to X\in \left[X,Y\right]$$
268	265 266 18 267	syl3anc	$$⊢\phi \to X\in \left[X,Y\right]$$
269		ubicc2	$$⊢\left(X\in {ℝ}^{*}\wedge Y\in {ℝ}^{*}\wedge X\le Y\right)\to Y\in \left[X,Y\right]$$
270	265 266 18 269	syl3anc	$$⊢\phi \to Y\in \left[X,Y\right]$$
271		oveq2	$$⊢y=X\to ⦋Y/x⦌By=⦋Y/x⦌BX$$
272		oveq2	$$⊢y=Y\to ⦋Y/x⦌By=⦋Y/x⦌BY$$
273	29 23 179 198 216 223 264 268 270 18 271 62 272 46	dvle	$$⊢\phi \to ⦋Y/x⦌BY-⦋Y/x⦌BX\le ⦋Y/x⦌A-⦋X/x⦌A$$
274	81 273	eqbrtrd	$$⊢\phi \to ⦋Y/x⦌B\left(Y-X\right)\le ⦋Y/x⦌A-⦋X/x⦌A$$
275	77 55 64 274	lesubd	$$⊢\phi \to ⦋X/x⦌A\le ⦋Y/x⦌A-⦋Y/x⦌B\left(Y-X\right)$$
276	74	recnd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B\in ℂ$$
277	45	recnd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B\in ℂ$$
278	55	recnd	$$⊢\phi \to ⦋Y/x⦌A\in ℂ$$
279	276 277 278	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$$
280	277 276	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$$
281	31	recnd	$$⊢\phi \to ⌊X⌋\in ℂ$$
282	79 80 281	nnncan2d	$$⊢\phi \to Y-⌊X⌋-\left(X-⌊X⌋\right)=Y-X$$
283	282	oveq1d	$$⊢\phi \to \left(Y-⌊X⌋-\left(X-⌊X⌋\right)\right)⦋Y/x⦌B=\left(Y-X\right)⦋Y/x⦌B$$
284	32	recnd	$$⊢\phi \to Y-⌊X⌋\in ℂ$$
285	57	recnd	$$⊢\phi \to X-⌊X⌋\in ℂ$$
286	284 285 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$$
287	76	recnd	$$⊢\phi \to Y-X\in ℂ$$
288	287 78	mulcomd	$$⊢\phi \to \left(Y-X\right)⦋Y/x⦌B=⦋Y/x⦌B\left(Y-X\right)$$
289	283 286 288	3eqtr3d	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-\left(X-⌊X⌋\right)⦋Y/x⦌B=⦋Y/x⦌B\left(Y-X\right)$$
290	289	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)$$
291	280 290	eqtr3d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-\left(Y-⌊X⌋\right)⦋Y/x⦌B=-⦋Y/x⦌B\left(Y-X\right)$$
292	291	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$$
293	77	recnd	$$⊢\phi \to ⦋Y/x⦌B\left(Y-X\right)\in ℂ$$
294	293 278	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$$
295	292 294	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)$$
296	293 278	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)$$
297	279 295 296	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)$$
298	275 297	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)$$
299	64 74 56 298	lesubd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\le \left(X-⌊X⌋\right)⦋Y/x⦌B-⦋X/x⦌A$$
300		flle	$$⊢X\in ℝ\to ⌊X⌋\le X$$
301	29 300	syl	$$⊢\phi \to ⌊X⌋\le X$$
302	29 31	subge0d	$$⊢\phi \to \left(0\le X-⌊X⌋\leftrightarrow ⌊X⌋\le X\right)$$
303	301 302	mpbird	$$⊢\phi \to 0\le X-⌊X⌋$$
304	58	breq2d	$$⊢y=X\to \left(⦋Y/x⦌B\le ⦋y/x⦌B\leftrightarrow ⦋Y/x⦌B\le ⦋X/x⦌B\right)$$
305	263	ralrimiva	$$⊢\phi \to \forall y\in \left[X,Y\right]⦋Y/x⦌B\le ⦋y/x⦌B$$
306	304 305 268	rspcdva	$$⊢\phi \to ⦋Y/x⦌B\le ⦋X/x⦌B$$
307	44 60 57 303 306	lemul2ad	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B\le \left(X-⌊X⌋\right)⦋X/x⦌B$$
308	74 61 64 307	lesub1dd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋Y/x⦌B-⦋X/x⦌A\le \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A$$
309	56 75 65 299 308	letrd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\le \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A$$
310	56 65 73 309	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$$
311	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$$
312	29	leidd	$$⊢\phi \to X\le X$$
313	265 266 12 18 19	xrletrd	$$⊢\phi \to X\le U$$
314		fllep1	$$⊢X\in ℝ\to X\le ⌊X⌋+1$$
315	29 314	syl	$$⊢\phi \to X\le ⌊X⌋+1$$
316	1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 15 17 312 313 315	dvfsumlem1	$$⊢\phi \to H\left(X\right)=\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A+\sum _{k=M}^{⌊X⌋}C$$
317	310 311 316	3brtr4d	$$⊢\phi \to H\left(Y\right)\le H\left(X\right)$$
318	65 60	resubcld	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A-⦋X/x⦌B\in ℝ$$
319	56 44	resubcld	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A-⦋Y/x⦌B\in ℝ$$
320		peano2rem	$$⊢X-⌊X⌋\in ℝ\to X-⌊X⌋-1\in ℝ$$
321	57 320	syl	$$⊢\phi \to X-⌊X⌋-1\in ℝ$$
322	321 60	remulcld	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B\in ℝ$$
323	322 64	resubcld	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-⦋X/x⦌A\in ℝ$$
324		peano2rem	$$⊢Y-⌊X⌋\in ℝ\to Y-⌊X⌋-1\in ℝ$$
325	32 324	syl	$$⊢\phi \to Y-⌊X⌋-1\in ℝ$$
326	325 60	remulcld	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B\in ℝ$$
327	326 55	resubcld	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B-⦋Y/x⦌A\in ℝ$$
328	325 44	remulcld	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B\in ℝ$$
329	328 55	resubcld	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B-⦋Y/x⦌A\in ℝ$$
330	322	recnd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B\in ℂ$$
331	326	recnd	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B\in ℂ$$
332	330 331	subcld	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B-\left(Y-⌊X⌋-1\right)⦋X/x⦌B\in ℂ$$
333	332 278	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$$
334	330 331 278	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$$
335	278 331 330	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$$
336	333 334 335	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)$$
337		1cnd	$$⊢\phi \to 1\in ℂ$$
338	284 285 337	nnncan2d	$$⊢\phi \to \left(Y-⌊X⌋\right)-1-\left(X-⌊X⌋-1\right)=Y-⌊X⌋-\left(X-⌊X⌋\right)$$
339	338 282	eqtrd	$$⊢\phi \to \left(Y-⌊X⌋\right)-1-\left(X-⌊X⌋-1\right)=Y-X$$
340	339	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$$
341	325	recnd	$$⊢\phi \to Y-⌊X⌋-1\in ℂ$$
342	321	recnd	$$⊢\phi \to X-⌊X⌋-1\in ℂ$$
343	60	recnd	$$⊢\phi \to ⦋X/x⦌B\in ℂ$$
344	341 342 343	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$$
345	287 343	mulcomd	$$⊢\phi \to \left(Y-X\right)⦋X/x⦌B=⦋X/x⦌B\left(Y-X\right)$$
346	340 344 345	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)$$
347	346	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)$$
348	336 347	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)$$
349	60 76	remulcld	$$⊢\phi \to ⦋X/x⦌B\left(Y-X\right)\in ℝ$$
350		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}{⟶}ℝ$$
351	60 101 102 350	syl3anc	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋X/x⦌B\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
352		remulcl	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋X/x⦌By\in ℝ$$
353		simpl	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋X/x⦌B\in ℝ$$
354	353	recnd	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋X/x⦌B\in ℂ$$
355		simpr	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to y\in ℝ$$
356	355	recnd	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to y\in ℂ$$
357	354 356	jca	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to \left(⦋X/x⦌B\in ℂ\wedge y\in ℂ\right)$$
358		ovmpot	$$⊢\left(⦋X/x⦌B\in ℂ\wedge y\in ℂ\right)\to ⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y=⦋X/x⦌By$$
359	358	eqcomd	$$⊢\left(⦋X/x⦌B\in ℂ\wedge y\in ℂ\right)\to ⦋X/x⦌By=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y$$
360	357 359	syl	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋X/x⦌By=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y$$
361	360	eleq1d	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to \left(⦋X/x⦌By\in ℝ\leftrightarrow ⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\in ℝ\right)$$
362	361	biimpd	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to \left(⦋X/x⦌By\in ℝ\to ⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\in ℝ\right)$$
363	352 362	mpd	$$⊢\left(⦋X/x⦌B\in ℝ\wedge y\in ℝ\right)\to ⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\in ℝ$$
364	82 83 351 106 100 363	cncfmpt2ss	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
365		df-mpt	$$⊢\left(y\in \left[X,Y\right]⟼⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}$$
366	365	eleq1i	$$⊢\left(y\in \left[X,Y\right]⟼⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\leftrightarrow \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ$$
367	366	biimpi	$$⊢\left(y\in \left[X,Y\right]⟼⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ$$
368	364 367	syl	$$⊢\phi \to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ$$
369	124	a1dd	$$⊢\phi \to \left(y\in \left[X,Y\right]\to \left(w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\to y\in \left[X,Y\right]\right)\right)$$
370	369	impd	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\to y\in \left[X,Y\right]\right)$$
371	343	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋X/x⦌B\in ℂ$$
372	371 142	jca	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(⦋X/x⦌B\in ℂ\wedge y\in ℂ\right)$$
373	372 358	syl	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y=⦋X/x⦌By$$
374	373	eqeq2d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\leftrightarrow w=⦋X/x⦌By\right)$$
375	374	biimpd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\to w=⦋X/x⦌By\right)$$
376	375	ex	$$⊢\phi \to \left(y\in \left[X,Y\right]\to \left(w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\to w=⦋X/x⦌By\right)\right)$$
377	376	impd	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\to w=⦋X/x⦌By\right)$$
378	370 377	jcad	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\to \left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\right)$$
379	124	a1dd	$$⊢\phi \to \left(y\in \left[X,Y\right]\to \left(w=⦋X/x⦌By\to y\in \left[X,Y\right]\right)\right)$$
380	379	impd	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\to y\in \left[X,Y\right]\right)$$
381	372 359	syl	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋X/x⦌By=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y$$
382	381	eqeq2d	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(w=⦋X/x⦌By\leftrightarrow w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)$$
383	382	biimpd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to \left(w=⦋X/x⦌By\to w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)$$
384	383	ex	$$⊢\phi \to \left(y\in \left[X,Y\right]\to \left(w=⦋X/x⦌By\to w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right)$$
385	384	impd	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\to w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)$$
386	380 385	jcad	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\to \left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right)$$
387	378 386	impbid	$$⊢\phi \to \left(\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\leftrightarrow \left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\right)$$
388	387	opabbidv	$$⊢\phi \to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\right\}$$
389		df-mpt	$$⊢\left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right)=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\right\}$$
390	389	eqcomi	$$⊢\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\right\}=\left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right)$$
391	390	eqeq2i	$$⊢\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\right\}\leftrightarrow \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right)$$
392	391	biimpi	$$⊢\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌By\right)\right\}\to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right)$$
393	388 392	syl	$$⊢\phi \to \left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}=\left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right)$$
394	393	eleq1d	$$⊢\phi \to \left(\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ\leftrightarrow \left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\right)$$
395	394	biimpd	$$⊢\phi \to \left(\left\{⟨y,w⟩|\left(y\in \left[X,Y\right]\wedge w=⦋X/x⦌B\left(u\in ℂ,v\in ℂ⟼uv\right)y\right)\right\}:\left[X,Y\right]\underset{cn}{⟶}ℝ\to \left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right):\left[X,Y\right]\underset{cn}{⟶}ℝ\right)$$
396	368 395	mpd	$$⊢\phi \to \left(y\in \left[X,Y\right]⟼⦋X/x⦌By\right):\left[X,Y\right]\underset{cn}{⟶}ℝ$$
397	181 185 186 194 343	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)$$
398	343	mulridd	$$⊢\phi \to ⦋X/x⦌B\cdot 1=⦋X/x⦌B$$
399	398	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)$$
400	397 399	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)$$
401	15	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to X\in S$$
402	141	rexrd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\in {ℝ}^{*}$$
403	266	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to Y\in {ℝ}^{*}$$
404	12	adantr	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to U\in {ℝ}^{*}$$
405	402 403 404 233 234	xrletrd	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to y\le U$$
406		vex	$$⊢y\in \mathrm{V}$$
407		eleq1	$$⊢k=y\to \left(k\in S\leftrightarrow y\in S\right)$$
408	407	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)$$
409		breq2	$$⊢k=y\to \left(X\le k\leftrightarrow X\le y\right)$$
410		breq1	$$⊢k=y\to \left(k\le U\leftrightarrow y\le U\right)$$
411	409 410	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)$$
412	408 411	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)$$
413		csbeq1	$$⊢k=y\to ⦋k/x⦌B=⦋y/x⦌B$$
414	243 413	eqtr3id	$$⊢k=y\to C=⦋y/x⦌B$$
415	414	breq1d	$$⊢k=y\to \left(C\le ⦋X/x⦌B\leftrightarrow ⦋y/x⦌B\le ⦋X/x⦌B\right)$$
416	412 415	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)$$
417		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$$
418		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)$$
419		nfcsb1v	$$⊢\underset{\_}{Ⅎ}x⦋X/x⦌B$$
420	248 249 419	nfbr	$$⊢ℲxC\le ⦋X/x⦌B$$
421	418 420	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)$$
422		eleq1	$$⊢x=X\to \left(x\in S\leftrightarrow X\in S\right)$$
423	422	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)$$
424		breq2	$$⊢x=X\to \left(D\le x\leftrightarrow D\le X\right)$$
425		breq1	$$⊢x=X\to \left(x\le k\leftrightarrow X\le k\right)$$
426	424 425	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)$$
427	423 426	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)$$
428		csbeq1a	$$⊢x=X\to B=⦋X/x⦌B$$
429	428	breq2d	$$⊢x=X\to \left(C\le B\leftrightarrow C\le ⦋X/x⦌B\right)$$
430	427 429	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)$$
431	421 430 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)$$
432	417 431	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$$
433	406 416 432	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$$
434	225 401 226 230 231 405 433	syl123anc	$$⊢\left(\phi \wedge y\in \left[X,Y\right]\right)\to ⦋y/x⦌B\le ⦋X/x⦌B$$
435	224 434	sylan2	$$⊢\left(\phi \wedge y\in \left(X,Y\right)\right)\to ⦋y/x⦌B\le ⦋X/x⦌B$$
436		oveq2	$$⊢y=X\to ⦋X/x⦌By=⦋X/x⦌BX$$
437		oveq2	$$⊢y=Y\to ⦋X/x⦌By=⦋X/x⦌BY$$
438	29 23 216 223 396 400 435 268 270 18 62 436 46 437	dvle	$$⊢\phi \to ⦋Y/x⦌A-⦋X/x⦌A\le ⦋X/x⦌BY-⦋X/x⦌BX$$
439	343 79 80	subdid	$$⊢\phi \to ⦋X/x⦌B\left(Y-X\right)=⦋X/x⦌BY-⦋X/x⦌BX$$
440	438 439	breqtrrd	$$⊢\phi \to ⦋Y/x⦌A-⦋X/x⦌A\le ⦋X/x⦌B\left(Y-X\right)$$
441	55 64 349 440	subled	$$⊢\phi \to ⦋Y/x⦌A-⦋X/x⦌B\left(Y-X\right)\le ⦋X/x⦌A$$
442	348 441	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$$
443	322 327 64 442	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$$
444	325	renegcld	$$⊢\phi \to -\left(Y-⌊X⌋-1\right)\in ℝ$$
445		1red	$$⊢\phi \to 1\in ℝ$$
446	23 31 445	lesubadd2d	$$⊢\phi \to \left(Y-⌊X⌋\le 1\leftrightarrow Y\le ⌊X⌋+1\right)$$
447	20 446	mpbird	$$⊢\phi \to Y-⌊X⌋\le 1$$
448	32 445	suble0d	$$⊢\phi \to \left(Y-⌊X⌋-1\le 0\leftrightarrow Y-⌊X⌋\le 1\right)$$
449	447 448	mpbird	$$⊢\phi \to Y-⌊X⌋-1\le 0$$
450	325	le0neg1d	$$⊢\phi \to \left(Y-⌊X⌋-1\le 0\leftrightarrow 0\le -\left(Y-⌊X⌋-1\right)\right)$$
451	449 450	mpbid	$$⊢\phi \to 0\le -\left(Y-⌊X⌋-1\right)$$
452	44 60 444 451 306	lemul2ad	$$⊢\phi \to \left(-\left(Y-⌊X⌋-1\right)\right)⦋Y/x⦌B\le \left(-\left(Y-⌊X⌋-1\right)\right)⦋X/x⦌B$$
453	341 78	mulneg1d	$$⊢\phi \to \left(-\left(Y-⌊X⌋-1\right)\right)⦋Y/x⦌B=-\left(Y-⌊X⌋-1\right)⦋Y/x⦌B$$
454	341 343	mulneg1d	$$⊢\phi \to \left(-\left(Y-⌊X⌋-1\right)\right)⦋X/x⦌B=-\left(Y-⌊X⌋-1\right)⦋X/x⦌B$$
455	452 453 454	3brtr3d	$$⊢\phi \to -\left(Y-⌊X⌋-1\right)⦋Y/x⦌B\le -\left(Y-⌊X⌋-1\right)⦋X/x⦌B$$
456	326 328	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)$$
457	455 456	mpbird	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋X/x⦌B\le \left(Y-⌊X⌋-1\right)⦋Y/x⦌B$$
458	326 328 55 457	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$$
459	323 327 329 443 458	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$$
460	285 337 343	subdird	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B=\left(X-⌊X⌋\right)⦋X/x⦌B-1⦋X/x⦌B$$
461	343	mullidd	$$⊢\phi \to 1⦋X/x⦌B=⦋X/x⦌B$$
462	461	oveq2d	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-1⦋X/x⦌B=\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌B$$
463	460 462	eqtrd	$$⊢\phi \to \left(X-⌊X⌋-1\right)⦋X/x⦌B=\left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌B$$
464	463	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$$
465	284 337 78	subdird	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B=\left(Y-⌊X⌋\right)⦋Y/x⦌B-1⦋Y/x⦌B$$
466	78	mullidd	$$⊢\phi \to 1⦋Y/x⦌B=⦋Y/x⦌B$$
467	466	oveq2d	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-1⦋Y/x⦌B=\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌B$$
468	465 467	eqtrd	$$⊢\phi \to \left(Y-⌊X⌋-1\right)⦋Y/x⦌B=\left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌B$$
469	468	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$$
470	459 464 469	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$$
471	61	recnd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B\in ℂ$$
472	64	recnd	$$⊢\phi \to ⦋X/x⦌A\in ℂ$$
473	471 472 343	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$$
474	277 278 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$$
475	470 473 474	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$$
476	318 319 73 475	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$$
477	65	recnd	$$⊢\phi \to \left(X-⌊X⌋\right)⦋X/x⦌B-⦋X/x⦌A\in ℂ$$
478	73	recnd	$$⊢\phi \to \sum _{k=M}^{⌊X⌋}C\in ℂ$$
479	477 478 343	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$$
480	56	recnd	$$⊢\phi \to \left(Y-⌊X⌋\right)⦋Y/x⦌B-⦋Y/x⦌A\in ℂ$$
481	480 478 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$$
482	476 479 481	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$$
483	316	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$$
484	311	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$$
485	482 483 484	3brtr4d	$$⊢\phi \to H\left(X\right)-⦋X/x⦌B\le H\left(Y\right)-⦋Y/x⦌B$$
486	317 485	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)$$