ftc1anclem6 - Mathbox for Brendan Leahy

	Mathbox for Brendan Leahy		< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > ftc1anclem6		Structured version Visualization version Unicode version

Theorem ftc1anclem6 33490

Description: Lemma for ftc1anc 33493- construction of simple functions within an arbitrary absolute distance of the given function. Similar to Lemma 565Ib of [Fremlin5] p. 218, but without Fremlin's additional step of converting the simple function into a continuous one, which is unnecessary to this lemma's use; also, two simple functions are used to allow for complex-valued

. (Contributed by Brendan Leahy, 31-May-2018.)

**Hypotheses**
Ref	Expression
ftc1anc.g
ftc1anc.a
ftc1anc.b
ftc1anc.le
ftc1anc.s
ftc1anc.d
ftc1anc.i
ftc1anc.f

**Assertion**
Ref	Expression
ftc1anclem6	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem ftc1anclem6 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		rphalfcl 11858	. . 3
2		ftc1anc.g	. . . 4
3		ftc1anc.a	. . . 4
4		ftc1anc.b	. . . 4
5		ftc1anc.le	. . . 4
6		ftc1anc.s	. . . 4
7		ftc1anc.d	. . . 4
8		ftc1anc.i	. . . 4
9		ftc1anc.f	. . . 4
10	2, 3, 4, 5, 6, 7, 8, 9	ftc1anclem5 33489	. . 3 $/\$
11	1, 10	sylan2 491	. 2 $/\$
12		eqid 2622	. . . . 5
13		ax-icn 9995	. . . . . . . 8
14		ine0 10465	. . . . . . . 8
15	13, 14	reccli 10755	. . . . . . 7
16	15	a1i 11	. . . . . 6
17	9	ffvelrnda 6359	. . . . . 6 $/\$
18	9	feqmptd 6249	. . . . . . 7
19	18, 8	eqeltrrd 2702	. . . . . 6
20		divrec2 10702	. . . . . . . . . 10 $/\$ $/\$
21	13, 14, 20	mp3an23 1416	. . . . . . . . 9
22	17, 21	syl 17	. . . . . . . 8 $/\$
23	22	mpteq2dva 4744	. . . . . . 7
24		iblmbf 23534	. . . . . . . . 9 MblFn
25	19, 24	syl 17	. . . . . . . 8 MblFn
26		fveq2 6191	. . . . . . . . . . . . . . . . 17
27	26	fveq2d 6195	. . . . . . . . . . . . . . . 16
28	27	cbvmptv 4750	. . . . . . . . . . . . . . 15
29	28	eleq1i 2692	. . . . . . . . . . . . . 14 MblFn MblFn
30	17	recld 13934	. . . . . . . . . . . . . . . . 17 $/\$
31	30	recnd 10068	. . . . . . . . . . . . . . . 16 $/\$
32	31	adantlr 751	. . . . . . . . . . . . . . 15 $/\$ MblFn $/\$
33	29	biimpri 218	. . . . . . . . . . . . . . . 16 MblFn MblFn
34	33	adantl 482	. . . . . . . . . . . . . . 15 $/\$ MblFn MblFn
35	32, 34	mbfneg 23417	. . . . . . . . . . . . . 14 $/\$ MblFn MblFn
36	29, 35	sylan2b 492	. . . . . . . . . . . . 13 $/\$ MblFn MblFn
37	9	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 $/\$
38	37	recld 13934	. . . . . . . . . . . . . . . . . . 19 $/\$
39	38	recnd 10068	. . . . . . . . . . . . . . . . . 18 $/\$
40	39	negnegd 10383	. . . . . . . . . . . . . . . . 17 $/\$
41	40	mpteq2dva 4744	. . . . . . . . . . . . . . . 16
42	41, 28	syl6eqr 2674	. . . . . . . . . . . . . . 15
43	42	adantr 481	. . . . . . . . . . . . . 14 $/\$ MblFn
44		negex 10279	. . . . . . . . . . . . . . . 16
45	44	a1i 11	. . . . . . . . . . . . . . 15 $/\$ MblFn $/\$
46	27	negeqd 10275	. . . . . . . . . . . . . . . . . . 19
47	46	cbvmptv 4750	. . . . . . . . . . . . . . . . . 18
48	47	eleq1i 2692	. . . . . . . . . . . . . . . . 17 MblFn MblFn
49	48	biimpi 206	. . . . . . . . . . . . . . . 16 MblFn MblFn
50	49	adantl 482	. . . . . . . . . . . . . . 15 $/\$ MblFn MblFn
51	45, 50	mbfneg 23417	. . . . . . . . . . . . . 14 $/\$ MblFn MblFn
52	43, 51	eqeltrrd 2702	. . . . . . . . . . . . 13 $/\$ MblFn MblFn
53	36, 52	impbida 877	. . . . . . . . . . . 12 MblFn MblFn
54		divcl 10691	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
55		imre 13848	. . . . . . . . . . . . . . . . . 18
56	54, 55	syl 17	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
57	13, 14, 56	mp3an23 1416	. . . . . . . . . . . . . . . 16
58	13, 14, 54	mp3an23 1416	. . . . . . . . . . . . . . . . . . 19
59		mulneg1 10466	. . . . . . . . . . . . . . . . . . 19 $/\$
60	13, 58, 59	sylancr 695	. . . . . . . . . . . . . . . . . 18
61		divcan2 10693	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$
62	13, 14, 61	mp3an23 1416	. . . . . . . . . . . . . . . . . . 19
63	62	negeqd 10275	. . . . . . . . . . . . . . . . . 18
64	60, 63	eqtrd 2656	. . . . . . . . . . . . . . . . 17
65	64	fveq2d 6195	. . . . . . . . . . . . . . . 16
66		reneg 13865	. . . . . . . . . . . . . . . 16
67	57, 65, 66	3eqtrd 2660	. . . . . . . . . . . . . . 15
68	17, 67	syl 17	. . . . . . . . . . . . . 14 $/\$
69	68	mpteq2dva 4744	. . . . . . . . . . . . 13
70	69	eleq1d 2686	. . . . . . . . . . . 12 MblFn MblFn
71	53, 70	bitr4d 271	. . . . . . . . . . 11 MblFn MblFn
72		imval 13847	. . . . . . . . . . . . . 14
73	17, 72	syl 17	. . . . . . . . . . . . 13 $/\$
74	73	mpteq2dva 4744	. . . . . . . . . . . 12
75	74	eleq1d 2686	. . . . . . . . . . 11 MblFn MblFn
76	71, 75	anbi12d 747	. . . . . . . . . 10 MblFn $/\$ MblFn MblFn $/\$ MblFn
77		ancom 466	. . . . . . . . . 10 MblFn $/\$ MblFn MblFn $/\$ MblFn
78	76, 77	syl6bb 276	. . . . . . . . 9 MblFn $/\$ MblFn MblFn $/\$ MblFn
79	17	ismbfcn2 23406	. . . . . . . . 9 MblFn MblFn $/\$ MblFn
80	17, 58	syl 17	. . . . . . . . . 10 $/\$
81	80	ismbfcn2 23406	. . . . . . . . 9 MblFn MblFn $/\$ MblFn
82	78, 79, 81	3bitr4d 300	. . . . . . . 8 MblFn MblFn
83	25, 82	mpbid 222	. . . . . . 7 MblFn
84	23, 83	eqeltrrd 2702	. . . . . 6 MblFn
85	16, 17, 19, 84	iblmulc2nc 33475	. . . . 5
86		mulcl 10020	. . . . . . 7 $/\$
87	15, 17, 86	sylancr 695	. . . . . 6 $/\$
88		eqid 2622	. . . . . 6
89	87, 88	fmptd 6385	. . . . 5
90	12, 3, 4, 5, 6, 7, 85, 89	ftc1anclem5 33489	. . . 4 $/\$
91	1, 90	sylan2 491	. . 3 $/\$
92	9	ffvelrnda 6359	. . . . . . . . . . . . 13 $/\$
93		0cnd 10033	. . . . . . . . . . . . 13 $/\$
94	92, 93	ifclda 4120	. . . . . . . . . . . 12
95		imval 13847	. . . . . . . . . . . 12
96	94, 95	syl 17	. . . . . . . . . . 11
97		fveq2 6191	. . . . . . . . . . . . . . . . . 18
98	97	oveq2d 6666	. . . . . . . . . . . . . . . . 17
99		ovex 6678	. . . . . . . . . . . . . . . . 17
100	98, 88, 99	fvmpt 6282	. . . . . . . . . . . . . . . 16
101	100	adantl 482	. . . . . . . . . . . . . . 15 $/\$
102		divrec2 10702	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
103	13, 14, 102	mp3an23 1416	. . . . . . . . . . . . . . . 16
104	92, 103	syl 17	. . . . . . . . . . . . . . 15 $/\$
105	101, 104	eqtr4d 2659	. . . . . . . . . . . . . 14 $/\$
106	105	ifeq1da 4116	. . . . . . . . . . . . 13
107		ovif 6737	. . . . . . . . . . . . . 14
108	13, 14	div0i 10759	. . . . . . . . . . . . . . 15
109		ifeq2 4091	. . . . . . . . . . . . . . 15
110	108, 109	ax-mp 5	. . . . . . . . . . . . . 14
111	107, 110	eqtri 2644	. . . . . . . . . . . . 13
112	106, 111	syl6eqr 2674	. . . . . . . . . . . 12
113	112	fveq2d 6195	. . . . . . . . . . 11
114	96, 113	eqtr4d 2659	. . . . . . . . . 10
115	114	oveq1d 6665	. . . . . . . . 9
116	115	fveq2d 6195	. . . . . . . 8
117	116	mpteq2dv 4745	. . . . . . 7
118	117	fveq2d 6195	. . . . . 6
119	118	breq1d 4663	. . . . 5
120	119	rexbidv 3052	. . . 4
121	120	adantr 481	. . 3 $/\$
122	91, 121	mpbird 247	. 2 $/\$
123		reeanv 3107	. . 3 $/\$ $/\$
124		eleq1w 2684	. . . . . . . . . . . . . . . . 17
125		fveq2 6191	. . . . . . . . . . . . . . . . 17
126	124, 125	ifbieq1d 4109	. . . . . . . . . . . . . . . 16
127	126	fveq2d 6195	. . . . . . . . . . . . . . 15
128		eqid 2622	. . . . . . . . . . . . . . 15
129		fvex 6201	. . . . . . . . . . . . . . 15
130	127, 128, 129	fvmpt 6282	. . . . . . . . . . . . . 14
131	130	oveq1d 6665	. . . . . . . . . . . . 13
132	131	fveq2d 6195	. . . . . . . . . . . 12
133	132	mpteq2ia 4740	. . . . . . . . . . 11
134	133	fveq2i 6194	. . . . . . . . . 10
135		rembl 23308	. . . . . . . . . . . . . . . . 17
136	135	a1i 11	. . . . . . . . . . . . . . . 16
137		0cnd 10033	. . . . . . . . . . . . . . . . . 18 $/\$
138	37, 137	ifclda 4120	. . . . . . . . . . . . . . . . 17
139	138	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
140		eldifn 3733	. . . . . . . . . . . . . . . . . 18 $\$
141	140	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $\$
142	141	iffalsed 4097	. . . . . . . . . . . . . . . 16 $/\$ $\$
143	9	feqmptd 6249	. . . . . . . . . . . . . . . . . 18
144		iftrue 4092	. . . . . . . . . . . . . . . . . . 19
145	144	mpteq2ia 4740	. . . . . . . . . . . . . . . . . 18
146	143, 145	syl6eqr 2674	. . . . . . . . . . . . . . . . 17
147	146, 8	eqeltrrd 2702	. . . . . . . . . . . . . . . 16
148	7, 136, 139, 142, 147	iblss2 23572	. . . . . . . . . . . . . . 15
149	138	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
150	149	iblcn 23565	. . . . . . . . . . . . . . 15 $/\$
151	148, 150	mpbid 222	. . . . . . . . . . . . . 14 $/\$
152	151	simpld 475	. . . . . . . . . . . . 13
153	149	recld 13934	. . . . . . . . . . . . . 14 $/\$
154	153, 128	fmptd 6385	. . . . . . . . . . . . 13
155	152, 154	jca 554	. . . . . . . . . . . 12 $/\$
156		ftc1anclem4 33488	. . . . . . . . . . . . 13 $/\$ $/\$
157	156	3expb 1266	. . . . . . . . . . . 12 $/\$ $/\$
158	155, 157	sylan2 491	. . . . . . . . . . 11 $/\$
159	158	ancoms 469	. . . . . . . . . 10 $/\$
160	134, 159	syl5eqelr 2706	. . . . . . . . 9 $/\$
161	126	fveq2d 6195	. . . . . . . . . . . . . . 15
162		eqid 2622	. . . . . . . . . . . . . . 15
163		fvex 6201	. . . . . . . . . . . . . . 15
164	161, 162, 163	fvmpt 6282	. . . . . . . . . . . . . 14
165	164	oveq1d 6665	. . . . . . . . . . . . 13
166	165	fveq2d 6195	. . . . . . . . . . . 12
167	166	mpteq2ia 4740	. . . . . . . . . . 11
168	167	fveq2i 6194	. . . . . . . . . 10
169	151	simprd 479	. . . . . . . . . . . . 13
170	138	imcld 13935	. . . . . . . . . . . . . . 15
171	170	adantr 481	. . . . . . . . . . . . . 14 $/\$
172	171, 162	fmptd 6385	. . . . . . . . . . . . 13
173	169, 172	jca 554	. . . . . . . . . . . 12 $/\$
174		ftc1anclem4 33488	. . . . . . . . . . . . 13 $/\$ $/\$
175	174	3expb 1266	. . . . . . . . . . . 12 $/\$ $/\$
176	173, 175	sylan2 491	. . . . . . . . . . 11 $/\$
177	176	ancoms 469	. . . . . . . . . 10 $/\$
178	168, 177	syl5eqelr 2706	. . . . . . . . 9 $/\$
179	160, 178	anim12dan 882	. . . . . . . 8 $/\$ $/\$ $/\$
180	1	rpred 11872	. . . . . . . . 9
181	180, 180	jca 554	. . . . . . . 8 $/\$
182		lt2add 10513	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
183	179, 181, 182	syl2an 494	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
184	183	an32s 846	. . . . . 6 $/\$ $/\$ $/\$ $/\$
185	94	recld 13934	. . . . . . . . . . . . . . . . . . 19
186	185	recnd 10068	. . . . . . . . . . . . . . . . . 18
187		i1ff 23443	. . . . . . . . . . . . . . . . . . . 20
188	187	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . 19 $/\$
189	188	recnd 10068	. . . . . . . . . . . . . . . . . 18 $/\$
190		subcl 10280	. . . . . . . . . . . . . . . . . 18 $/\$
191	186, 189, 190	syl2an 494	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
192	191	anassrs 680	. . . . . . . . . . . . . . . 16 $/\$ $/\$
193	192	adantlrr 757	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
194	94	imcld 13935	. . . . . . . . . . . . . . . . . . . 20
195	194	recnd 10068	. . . . . . . . . . . . . . . . . . 19
196		i1ff 23443	. . . . . . . . . . . . . . . . . . . . 21
197	196	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . 20 $/\$
198	197	recnd 10068	. . . . . . . . . . . . . . . . . . 19 $/\$
199		subcl 10280	. . . . . . . . . . . . . . . . . . 19 $/\$
200	195, 198, 199	syl2an 494	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
201	200	anassrs 680	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
202		mulcl 10020	. . . . . . . . . . . . . . . . 17 $/\$
203	13, 201, 202	sylancr 695	. . . . . . . . . . . . . . . 16 $/\$ $/\$
204	203	adantlrl 756	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
205	193, 204	addcld 10059	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
206	205	abscld 14175	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
207	206	rexrd 10089	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
208	205	absge0d 14183	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
209		elxrge0 12281	. . . . . . . . . . . 12 $/\$
210	207, 208, 209	sylanbrc 698	. . . . . . . . . . 11 $/\$ $/\$ $/\$
211		eqid 2622	. . . . . . . . . . 11
212	210, 211	fmptd 6385	. . . . . . . . . 10 $/\$ $/\$
213		icossicc 12260	. . . . . . . . . . . . 13
214		ge0addcl 12284	. . . . . . . . . . . . 13 $/\$
215	213, 214	sseldi 3601	. . . . . . . . . . . 12 $/\$
216	215	adantl 482	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
217	192	abscld 14175	. . . . . . . . . . . . . 14 $/\$ $/\$
218	192	absge0d 14183	. . . . . . . . . . . . . 14 $/\$ $/\$
219		elrege0 12278	. . . . . . . . . . . . . 14 $/\$
220	217, 218, 219	sylanbrc 698	. . . . . . . . . . . . 13 $/\$ $/\$
221		eqid 2622	. . . . . . . . . . . . 13
222	220, 221	fmptd 6385	. . . . . . . . . . . 12 $/\$
223	222	adantrr 753	. . . . . . . . . . 11 $/\$ $/\$
224	201	abscld 14175	. . . . . . . . . . . . . 14 $/\$ $/\$
225	201	absge0d 14183	. . . . . . . . . . . . . 14 $/\$ $/\$
226		elrege0 12278	. . . . . . . . . . . . . 14 $/\$
227	224, 225, 226	sylanbrc 698	. . . . . . . . . . . . 13 $/\$ $/\$
228		eqid 2622	. . . . . . . . . . . . 13
229	227, 228	fmptd 6385	. . . . . . . . . . . 12 $/\$
230	229	adantrl 752	. . . . . . . . . . 11 $/\$ $/\$
231		reex 10027	. . . . . . . . . . . 12
232	231	a1i 11	. . . . . . . . . . 11 $/\$ $/\$
233		inidm 3822	. . . . . . . . . . 11
234	216, 223, 230, 232, 232, 233	off 6912	. . . . . . . . . 10 $/\$ $/\$
235	193, 204	abstrid 14195	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
236	235	ralrimiva 2966	. . . . . . . . . . 11 $/\$ $/\$
237		ovexd 6680	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
238		eqidd 2623	. . . . . . . . . . . 12 $/\$ $/\$
239		fvexd 6203	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
240		fvexd 6203	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
241		eqidd 2623	. . . . . . . . . . . . 13 $/\$ $/\$
242		absmul 14034	. . . . . . . . . . . . . . . . 17 $/\$
243	13, 201, 242	sylancr 695	. . . . . . . . . . . . . . . 16 $/\$ $/\$
244		absi 14026	. . . . . . . . . . . . . . . . . 18
245	244	oveq1i 6660	. . . . . . . . . . . . . . . . 17
246	224	recnd 10068	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
247	246	mulid2d 10058	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
248	245, 247	syl5eq 2668	. . . . . . . . . . . . . . . 16 $/\$ $/\$
249	243, 248	eqtr2d 2657	. . . . . . . . . . . . . . 15 $/\$ $/\$
250	249	mpteq2dva 4744	. . . . . . . . . . . . . 14 $/\$
251	250	adantrl 752	. . . . . . . . . . . . 13 $/\$ $/\$
252	232, 239, 240, 241, 251	offval2 6914	. . . . . . . . . . . 12 $/\$ $/\$
253	232, 206, 237, 238, 252	ofrfval2 6915	. . . . . . . . . . 11 $/\$ $/\$
254	236, 253	mpbird 247	. . . . . . . . . 10 $/\$ $/\$
255		itg2le 23506	. . . . . . . . . 10 $/\$ $/\$
256	212, 234, 254, 255	syl3anc 1326	. . . . . . . . 9 $/\$ $/\$
257		absf 14077	. . . . . . . . . . . . . 14
258	257	a1i 11	. . . . . . . . . . . . 13 $/\$
259	258, 192	cofmpt 6399	. . . . . . . . . . . 12 $/\$
260		resubcl 10345	. . . . . . . . . . . . . . . 16 $/\$
261	185, 188, 260	syl2an 494	. . . . . . . . . . . . . . 15 $/\$ $/\$
262	261	anassrs 680	. . . . . . . . . . . . . 14 $/\$ $/\$
263		eqid 2622	. . . . . . . . . . . . . 14
264	262, 263	fmptd 6385	. . . . . . . . . . . . 13 $/\$
265	135	a1i 11	. . . . . . . . . . . . . 14 $/\$
266		iunin2 4584	. . . . . . . . . . . . . . . . . . 19
267		imaiun 6503	. . . . . . . . . . . . . . . . . . . . 21
268		iunid 4575	. . . . . . . . . . . . . . . . . . . . . 22
269	268	imaeq2i 5464	. . . . . . . . . . . . . . . . . . . . 21
270	267, 269	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . 20
271	270	ineq2i 3811	. . . . . . . . . . . . . . . . . . 19
272	266, 271	eqtri 2644	. . . . . . . . . . . . . . . . . 18
273		cnvimass 5485	. . . . . . . . . . . . . . . . . . . . 21
274		ovex 6678	. . . . . . . . . . . . . . . . . . . . . 22
275	274, 263	dmmpti 6023	. . . . . . . . . . . . . . . . . . . . 21
276	273, 275	sseqtri 3637	. . . . . . . . . . . . . . . . . . . 20
277		cnvimarndm 5486	. . . . . . . . . . . . . . . . . . . . 21
278		fdm 6051	. . . . . . . . . . . . . . . . . . . . . 22
279	187, 278	syl 17	. . . . . . . . . . . . . . . . . . . . 21
280	277, 279	syl5eq 2668	. . . . . . . . . . . . . . . . . . . 20
281	276, 280	syl5sseqr 3654	. . . . . . . . . . . . . . . . . . 19
282		df-ss 3588	. . . . . . . . . . . . . . . . . . 19
283	281, 282	sylib 208	. . . . . . . . . . . . . . . . . 18
284	272, 283	syl5eq 2668	. . . . . . . . . . . . . . . . 17
285	284	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$
286		frn 6053	. . . . . . . . . . . . . . . . . . . . . . 23
287	187, 286	syl 17	. . . . . . . . . . . . . . . . . . . . . 22
288	287	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$
289	288	sselda 3603	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
290	185	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
291		resubcl 10345	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
292	185, 291	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
293	292	adantlr 751	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
294	290, 293	2thd 255	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
295		ltaddsub 10502	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
296	185, 295	syl3an3 1361	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
297	296	3comr 1273	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
298	297	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
299	294, 298	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
300		readdcl 10019	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
301	300	rexrd 10089	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
302	301	adantll 750	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
303		elioopnf 12267	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
304	302, 303	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
305		rexr 10085	. . . . . . . . . . . . . . . . . . . . . . . . . 26
306	305	ad2antlr 763	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
307		elioopnf 12267	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
308	306, 307	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
309	299, 304, 308	3bitr4rd 301	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
310		oveq2 6658	. . . . . . . . . . . . . . . . . . . . . . . . 25
311	310	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . 24
312	311	bibi1d 333	. . . . . . . . . . . . . . . . . . . . . . 23
313	309, 312	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
314	313	pm5.32rd 672	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
315	314	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
316	289, 315	syldan 487	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
317	316	rabbidv 3189	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
318	187	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . . . 23
319	318	cnveqd 5298	. . . . . . . . . . . . . . . . . . . . . 22
320	319	imaeq1d 5465	. . . . . . . . . . . . . . . . . . . . 21
321	320	ineq2d 3814	. . . . . . . . . . . . . . . . . . . 20
322	263	mptpreima 5628	. . . . . . . . . . . . . . . . . . . . . 22
323		vex 3203	. . . . . . . . . . . . . . . . . . . . . . 23
324		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . . 24
325	324	mptiniseg 5629	. . . . . . . . . . . . . . . . . . . . . . 23
326	323, 325	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . 22
327	322, 326	ineq12i 3812	. . . . . . . . . . . . . . . . . . . . 21
328		inrab 3899	. . . . . . . . . . . . . . . . . . . . 21 $/\$
329	327, 328	eqtri 2644	. . . . . . . . . . . . . . . . . . . 20 $/\$
330	321, 329	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 $/\$
331	330	ad3antlr 767	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
332	320	ineq2d 3814	. . . . . . . . . . . . . . . . . . . 20
333		eqid 2622	. . . . . . . . . . . . . . . . . . . . . . 23
334	333	mptpreima 5628	. . . . . . . . . . . . . . . . . . . . . 22
335	334, 326	ineq12i 3812	. . . . . . . . . . . . . . . . . . . . 21
336		inrab 3899	. . . . . . . . . . . . . . . . . . . . 21 $/\$
337	335, 336	eqtri 2644	. . . . . . . . . . . . . . . . . . . 20 $/\$
338	332, 337	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 $/\$
339	338	ad3antlr 767	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
340	317, 331, 339	3eqtr4d 2666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
341	340	iuneq2dv 4542	. . . . . . . . . . . . . . . 16 $/\$ $/\$
342	285, 341	eqtr3d 2658	. . . . . . . . . . . . . . 15 $/\$ $/\$
343		i1frn 23444	. . . . . . . . . . . . . . . . . 18
344	343	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$
345	94	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
346		eldifn 3733	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
347	346	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $\$
348	347	iffalsed 4097	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$
349	9	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . . . . . 25
350		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . . . . 26
351	350	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . . . . . 25
352	349, 351	syl6eqr 2674	. . . . . . . . . . . . . . . . . . . . . . . 24
353		iblmbf 23534	. . . . . . . . . . . . . . . . . . . . . . . . 25 MblFn
354	8, 353	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 MblFn
355	352, 354	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . . . . 23 MblFn
356	7, 136, 345, 348, 355	mbfss 23413	. . . . . . . . . . . . . . . . . . . . . 22 MblFn
357	94	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
358	357	ismbfcn2 23406	. . . . . . . . . . . . . . . . . . . . . 22 MblFn MblFn $/\$ MblFn
359	356, 358	mpbid 222	. . . . . . . . . . . . . . . . . . . . 21 MblFn $/\$ MblFn
360	359	simpld 475	. . . . . . . . . . . . . . . . . . . 20 MblFn
361	185	adantr 481	. . . . . . . . . . . . . . . . . . . . 21 $/\$
362	361, 333	fmptd 6385	. . . . . . . . . . . . . . . . . . . 20
363		mbfima 23399	. . . . . . . . . . . . . . . . . . . 20 MblFn $/\$
364	360, 362, 363	syl2anc 693	. . . . . . . . . . . . . . . . . . 19
365		i1fima 23445	. . . . . . . . . . . . . . . . . . 19
366		inmbl 23310	. . . . . . . . . . . . . . . . . . 19 $/\$
367	364, 365, 366	syl2an 494	. . . . . . . . . . . . . . . . . 18 $/\$
368	367	ralrimivw 2967	. . . . . . . . . . . . . . . . 17 $/\$
369		finiunmbl 23312	. . . . . . . . . . . . . . . . 17 $/\$
370	344, 368, 369	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$
371	370	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$
372	342, 371	eqeltrd 2701	. . . . . . . . . . . . . 14 $/\$ $/\$
373		iunin2 4584	. . . . . . . . . . . . . . . . . . 19
374	270	ineq2i 3811	. . . . . . . . . . . . . . . . . . 19
375	373, 374	eqtri 2644	. . . . . . . . . . . . . . . . . 18
376		cnvimass 5485	. . . . . . . . . . . . . . . . . . . . 21
377	376, 275	sseqtri 3637	. . . . . . . . . . . . . . . . . . . 20
378	377, 280	syl5sseqr 3654	. . . . . . . . . . . . . . . . . . 19
379		df-ss 3588	. . . . . . . . . . . . . . . . . . 19
380	378, 379	sylib 208	. . . . . . . . . . . . . . . . . 18
381	375, 380	syl5eq 2668	. . . . . . . . . . . . . . . . 17
382	381	ad2antlr 763	. . . . . . . . . . . . . . . 16 $/\$ $/\$
383	293, 290	2thd 255	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
384		ltsubadd 10498	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
385	185, 384	syl3an1 1359	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
386	385	3expa 1265	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
387	386	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
388	383, 387	anbi12d 747	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
389		elioomnf 12268	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
390	306, 389	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
391		elioomnf 12268	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
392	302, 391	syl 17	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$
393	388, 390, 392	3bitr4d 300	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
394	310	eleq1d 2686	. . . . . . . . . . . . . . . . . . . . . . . 24
395	394	bibi1d 333	. . . . . . . . . . . . . . . . . . . . . . 23
396	393, 395	syl5ibrcom 237	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
397	396	pm5.32rd 672	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
398	397	adantllr 755	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$ $/\$
399	289, 398	syldan 487	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$ $/\$
400	399	rabbidv 3189	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$ $/\$
401	320	ineq2d 3814	. . . . . . . . . . . . . . . . . . . 20
402	263	mptpreima 5628	. . . . . . . . . . . . . . . . . . . . . 22
403	402, 326	ineq12i 3812	. . . . . . . . . . . . . . . . . . . . 21
404		inrab 3899	. . . . . . . . . . . . . . . . . . . . 21 $/\$
405	403, 404	eqtri 2644	. . . . . . . . . . . . . . . . . . . 20 $/\$
406	401, 405	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 $/\$
407	406	ad3antlr 767	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
408	320	ineq2d 3814	. . . . . . . . . . . . . . . . . . . 20
409	333	mptpreima 5628	. . . . . . . . . . . . . . . . . . . . . 22
410	409, 326	ineq12i 3812	. . . . . . . . . . . . . . . . . . . . 21
411		inrab 3899	. . . . . . . . . . . . . . . . . . . . 21 $/\$
412	410, 411	eqtri 2644	. . . . . . . . . . . . . . . . . . . 20 $/\$
413	408, 412	syl6eq 2672	. . . . . . . . . . . . . . . . . . 19 $/\$
414	413	ad3antlr 767	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$ $/\$
415	400, 407, 414	3eqtr4d 2666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
416	415	iuneq2dv 4542	. . . . . . . . . . . . . . . 16 $/\$ $/\$
417	382, 416	eqtr3d 2658	. . . . . . . . . . . . . . 15 $/\$ $/\$
418		mbfima 23399	. . . . . . . . . . . . . . . . . . . 20 MblFn $/\$
419	360, 362, 418	syl2anc 693	. . . . . . . . . . . . . . . . . . 19
420		inmbl 23310	. . . . . . . . . . . . . . . . . . 19 $/\$
421	419, 365, 420	syl2an 494	. . . . . . . . . . . . . . . . . 18 $/\$
422	421	ralrimivw 2967	. . . . . . . . . . . . . . . . 17 $/\$
423		finiunmbl 23312	. . . . . . . . . . . . . . . . 17 $/\$
424	344, 422, 423	syl2anc 693	. . . . . . . . . . . . . . . 16 $/\$
425	424	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$
426	417, 425	eqeltrd 2701	. . . . . . . . . . . . . 14 $/\$ $/\$
427	264, 265, 372, 426	ismbf2d 23408	. . . . . . . . . . . . 13 $/\$ MblFn
428		ftc1anclem1 33485	. . . . . . . . . . . . 13 $/\$ MblFn MblFn
429	264, 427, 428	syl2anc 693	. . . . . . . . . . . 12 $/\$ MblFn
430	259, 429	eqeltrrd 2702	. . . . . . . . . . 11 $/\$ MblFn
431	430	adantrr 753	. . . . . . . . . 10 $/\$ $/\$ MblFn
432	160	adantrr 753	. . . . . . . . . 10 $/\$ $/\$
433	178	adantrl 752	. . . . . . . . . 10 $/\$ $/\$
434	431, 223, 432, 230, 433	itg2addnc 33464	. . . . . . . . 9 $/\$ $/\$
435	256, 434	breqtrd 4679	. . . . . . . 8 $/\$ $/\$
436	435	adantlr 751	. . . . . . 7 $/\$ $/\$ $/\$
437		itg2cl 23499	. . . . . . . . . 10
438	212, 437	syl 17	. . . . . . . . 9 $/\$ $/\$
439	438	adantlr 751	. . . . . . . 8 $/\$ $/\$ $/\$
440		readdcl 10019	. . . . . . . . . . . 12 $/\$
441	160, 178, 440	syl2an 494	. . . . . . . . . . 11 $/\$ $/\$ $/\$
442	441	anandis 873	. . . . . . . . . 10 $/\$ $/\$
443	442	rexrd 10089	. . . . . . . . 9 $/\$ $/\$
444	443	adantlr 751	. . . . . . . 8 $/\$ $/\$ $/\$
445	1, 1	rpaddcld 11887	. . . . . . . . . 10
446	445	rpxrd 11873	. . . . . . . . 9
447	446	ad2antlr 763	. . . . . . . 8 $/\$ $/\$ $/\$
448		xrlelttr 11987	. . . . . . . 8 $/\$ $/\$ $/\$
449	439, 444, 447, 448	syl3anc 1326	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
450	436, 449	mpand 711	. . . . . 6 $/\$ $/\$ $/\$
451	184, 450	syld 47	. . . . 5 $/\$ $/\$ $/\$ $/\$
452		mulcl 10020	. . . . . . . . . . . . . . 15 $/\$
453	13, 195, 452	sylancr 695	. . . . . . . . . . . . . 14
454	186, 453	jca 554	. . . . . . . . . . . . 13 $/\$
455		mulcl 10020	. . . . . . . . . . . . . . . 16 $/\$
456	13, 198, 455	sylancr 695	. . . . . . . . . . . . . . 15 $/\$
457	189, 456	anim12i 590	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$
458	457	anandirs 874	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
459		addsub4 10324	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
460	454, 458, 459	syl2an 494	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
461	460	anassrs 680	. . . . . . . . . . 11 $/\$ $/\$ $/\$
462	94	replimd 13937	. . . . . . . . . . . . 13
463	462	ad2antrr 762	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
464	463	oveq1d 6665	. . . . . . . . . . 11 $/\$ $/\$ $/\$
465	198	adantll 750	. . . . . . . . . . . . . 14 $/\$ $/\$
466		subdi 10463	. . . . . . . . . . . . . 14 $/\$ $/\$
467	13, 195, 465, 466	mp3an3an 1430	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
468	467	anassrs 680	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
469	468	oveq2d 6666	. . . . . . . . . . 11 $/\$ $/\$ $/\$
470	461, 464, 469	3eqtr4rd 2667	. . . . . . . . . 10 $/\$ $/\$ $/\$
471	470	fveq2d 6195	. . . . . . . . 9 $/\$ $/\$ $/\$
472	471	mpteq2dva 4744	. . . . . . . 8 $/\$ $/\$
473	472	fveq2d 6195	. . . . . . 7 $/\$ $/\$
474	473	adantlr 751	. . . . . 6 $/\$ $/\$ $/\$
475		rpcn 11841	. . . . . . . 8
476	475	2halvesd 11278	. . . . . . 7
477	476	ad2antlr 763	. . . . . 6 $/\$ $/\$ $/\$
478	474, 477	breq12d 4666	. . . . 5 $/\$ $/\$ $/\$
479	451, 478	sylibd 229	. . . 4 $/\$ $/\$ $/\$ $/\$
480	479	reximdvva 3019	. . 3 $/\$ $/\$
481	123, 480	syl5bir 233	. 2 $/\$ $/\$
482	11, 122, 481	mp2and 715	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $/\$ wa 384 $/\$ w3a 1037

wceq 1483

wcel 1990

wne 2794

wral 2912

wrex 2913

crab 2916

cvv 3200 $\$ cdif 3571

cin 3573

wss 3574

cif 4086

csn 4177

ciun 4520 class class class wbr 4653

cmpt 4729

ccnv 5113

cdm 5114

crn 5115

cima 5117

ccom 5118

wf 5884

cfv 5888 (class class class)co 6650

cof 6895

cofr 6896

cfn 7955

cc 9934

cr 9935

cc0 9936

c1 9937

ci 9938

caddc 9939

cmul 9941

cpnf 10071

cmnf 10072

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

cdiv 10684

c2 11070

crp 11832

cioo 12175

cico 12177

cicc 12178

cre 13837

cim 13838

cabs 13974

cvol 23232 MblFncmbf 23383

citg1 23384

citg2 23385

cibl 23386

citg 23387

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1722 ax-4 1737 ax-5 1839 ax-6 1888 ax-7 1935 ax-8 1992 ax-9 1999 ax-10 2019 ax-11 2034 ax-12 2047 ax-13 2246 ax-ext 2602 ax-rep 4771 ax-sep 4781 ax-nul 4789 ax-pow 4843 ax-pr 4906 ax-un 6949 ax-inf2 8538 ax-cnex 9992 ax-resscn 9993 ax-1cn 9994 ax-icn 9995 ax-addcl 9996 ax-addrcl 9997 ax-mulcl 9998 ax-mulrcl 9999 ax-mulcom 10000 ax-addass 10001 ax-mulass 10002 ax-distr 10003 ax-i2m1 10004 ax-1ne0 10005 ax-1rid 10006 ax-rnegex 10007 ax-rrecex 10008 ax-cnre 10009 ax-pre-lttri 10010 ax-pre-lttrn 10011 ax-pre-ltadd 10012 ax-pre-mulgt0 10013 ax-pre-sup 10014 ax-addf 10015

This theorem depends on definitions: df-bi 197 df-or 385 df-an 386 df-3or 1038 df-3an 1039 df-tru 1486 df-fal 1489 df-ex 1705 df-nf 1710 df-sb 1881 df-eu 2474 df-mo 2475 df-clab 2609 df-cleq 2615 df-clel 2618 df-nfc 2753 df-ne 2795 df-nel 2898 df-ral 2917 df-rex 2918 df-reu 2919 df-rmo 2920 df-rab 2921 df-v 3202 df-sbc 3436 df-csb 3534 df-dif 3577 df-un 3579 df-in 3581 df-ss 3588 df-pss 3590 df-nul 3916 df-if 4087 df-pw 4160 df-sn 4178 df-pr 4180 df-tp 4182 df-op 4184 df-uni 4437 df-int 4476 df-iun 4522 df-disj 4621 df-br 4654 df-opab 4713 df-mpt 4730 df-tr 4753 df-id 5024 df-eprel 5029 df-po 5035 df-so 5036 df-fr 5073 df-se 5074 df-we 5075 df-xp 5120 df-rel 5121 df-cnv 5122 df-co 5123 df-dm 5124 df-rn 5125 df-res 5126 df-ima 5127 df-pred 5680 df-ord 5726 df-on 5727 df-lim 5728 df-suc 5729 df-iota 5851 df-fun 5890 df-fn 5891 df-f 5892 df-f1 5893 df-fo 5894 df-f1o 5895 df-fv 5896 df-isom 5897 df-riota 6611 df-ov 6653 df-oprab 6654 df-mpt2 6655 df-of 6897 df-ofr 6898 df-om 7066 df-1st 7168 df-2nd 7169 df-wrecs 7407 df-recs 7468 df-rdg 7506 df-1o 7560 df-2o 7561 df-oadd 7564 df-er 7742 df-map 7859 df-pm 7860 df-en 7956 df-dom 7957 df-sdom 7958 df-fin 7959 df-fi 8317 df-sup 8348 df-inf 8349 df-oi 8415 df-card 8765 df-cda 8990 df-pnf 10076 df-mnf 10077 df-xr 10078 df-ltxr 10079 df-le 10080 df-sub 10268 df-neg 10269 df-div 10685 df-nn 11021 df-2 11079 df-3 11080 df-4 11081 df-n0 11293 df-z 11378 df-uz 11688 df-q 11789 df-rp 11833 df-xneg 11946 df-xadd 11947 df-xmul 11948 df-ioo 12179 df-ico 12181 df-icc 12182 df-fz 12327 df-fzo 12466 df-fl 12593 df-mod 12669 df-seq 12802 df-exp 12861 df-hash 13118 df-cj 13839 df-re 13840 df-im 13841 df-sqrt 13975 df-abs 13976 df-clim 14219 df-sum 14417 df-rest 16083 df-topgen 16104 df-psmet 19738 df-xmet 19739 df-met 19740 df-bl 19741 df-mopn 19742 df-top 20699 df-topon 20716 df-bases 20750 df-cmp 21190 df-ovol 23233 df-vol 23234 df-mbf 23388 df-itg1 23389 df-itg2 23390 df-ibl 23391 df-0p 23437

This theorem is referenced by: ftc1anc 33493

W3C validator