ftc1anclem5 - Mathbox for Brendan Leahy

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

Theorem ftc1anclem5 33489

Description: Lemma for ftc1anc 33493, the existence of a simple function the integral of whose pointwise difference from the function is less than a given positive real. (Contributed by Brendan Leahy, 17-Jun-2018.)

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

**Assertion**
Ref	Expression
ftc1anclem5	$/\$

Distinct variable groups:

Allowed substitution hints:

(

)

Proof of Theorem ftc1anclem5 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		iftrue 4092	. . . . . . . . 9
2	1	mpteq2ia 4740	. . . . . . . 8
3	2	fveq2i 6194	. . . . . . 7
4		ftc1anc.f	. . . . . . . . . . . . . 14
5	4	ffvelrnda 6359	. . . . . . . . . . . . 13 $/\$
6		0cnd 10033	. . . . . . . . . . . . 13 $/\$
7	5, 6	ifclda 4120	. . . . . . . . . . . 12
8	7	recld 13934	. . . . . . . . . . 11
9	8	adantr 481	. . . . . . . . . 10 $/\$
10		ftc1anc.d	. . . . . . . . . . 11
11		rembl 23308	. . . . . . . . . . . 12
12	11	a1i 11	. . . . . . . . . . 11
13	8	adantr 481	. . . . . . . . . . 11 $/\$
14		eldifn 3733	. . . . . . . . . . . . 13 $\$
15	14	adantl 482	. . . . . . . . . . . 12 $/\$ $\$
16		iffalse 4095	. . . . . . . . . . . . . 14
17	16	fveq2d 6195	. . . . . . . . . . . . 13
18		re0 13892	. . . . . . . . . . . . 13
19	17, 18	syl6eq 2672	. . . . . . . . . . . 12
20	15, 19	syl 17	. . . . . . . . . . 11 $/\$ $\$
21		iftrue 4092	. . . . . . . . . . . . . 14
22	21	fveq2d 6195	. . . . . . . . . . . . 13
23	22	mpteq2ia 4740	. . . . . . . . . . . 12
24	4	feqmptd 6249	. . . . . . . . . . . . . . 15
25		ftc1anc.i	. . . . . . . . . . . . . . 15
26	24, 25	eqeltrrd 2702	. . . . . . . . . . . . . 14
27	5	iblcn 23565	. . . . . . . . . . . . . 14 $/\$
28	26, 27	mpbid 222	. . . . . . . . . . . . 13 $/\$
29	28	simpld 475	. . . . . . . . . . . 12
30	23, 29	syl5eqel 2705	. . . . . . . . . . 11
31	10, 12, 13, 20, 30	iblss2 23572	. . . . . . . . . 10
32	8	recnd 10068	. . . . . . . . . . . . 13
33	32	adantr 481	. . . . . . . . . . . 12 $/\$
34		eqidd 2623	. . . . . . . . . . . 12
35		absf 14077	. . . . . . . . . . . . . 14
36	35	a1i 11	. . . . . . . . . . . . 13
37	36	feqmptd 6249	. . . . . . . . . . . 12
38		fveq2 6191	. . . . . . . . . . . 12
39	33, 34, 37, 38	fmptco 6396	. . . . . . . . . . 11
40		eqid 2622	. . . . . . . . . . . . 13
41	9, 40	fmptd 6385	. . . . . . . . . . . 12
42		iblmbf 23534	. . . . . . . . . . . . . . . . . 18 MblFn
43	25, 42	syl 17	. . . . . . . . . . . . . . . . 17 MblFn
44	24, 43	eqeltrrd 2702	. . . . . . . . . . . . . . . 16 MblFn
45	5	ismbfcn2 23406	. . . . . . . . . . . . . . . 16 MblFn MblFn $/\$ MblFn
46	44, 45	mpbid 222	. . . . . . . . . . . . . . 15 MblFn $/\$ MblFn
47	46	simpld 475	. . . . . . . . . . . . . 14 MblFn
48	23, 47	syl5eqel 2705	. . . . . . . . . . . . 13 MblFn
49	10, 12, 13, 20, 48	mbfss 23413	. . . . . . . . . . . 12 MblFn
50		ftc1anclem1 33485	. . . . . . . . . . . 12 $/\$ MblFn MblFn
51	41, 49, 50	syl2anc 693	. . . . . . . . . . 11 MblFn
52	39, 51	eqeltrrd 2702	. . . . . . . . . 10 MblFn
53	9, 31, 52	iblabsnc 33474	. . . . . . . . 9
54	32	abscld 14175	. . . . . . . . . . 11
55	54	adantr 481	. . . . . . . . . 10 $/\$
56	32	absge0d 14183	. . . . . . . . . . 11
57	56	adantr 481	. . . . . . . . . 10 $/\$
58	55, 57	iblpos 23559	. . . . . . . . 9 MblFn $/\$
59	53, 58	mpbid 222	. . . . . . . 8 MblFn $/\$
60	59	simprd 479	. . . . . . 7
61	3, 60	syl5eqelr 2706	. . . . . 6
62		ltsubrp 11866	. . . . . 6 $/\$
63	61, 62	sylan 488	. . . . 5 $/\$
64		rpre 11839	. . . . . . 7
65		resubcl 10345	. . . . . . 7 $/\$
66	61, 64, 65	syl2an 494	. . . . . 6 $/\$
67	61	adantr 481	. . . . . 6 $/\$
68	66, 67	ltnled 10184	. . . . 5 $/\$
69	63, 68	mpbid 222	. . . 4 $/\$
70	54	rexrd 10089	. . . . . . . . 9
71		elxrge0 12281	. . . . . . . . 9 $/\$
72	70, 56, 71	sylanbrc 698	. . . . . . . 8
73	72	adantr 481	. . . . . . 7 $/\$
74		eqid 2622	. . . . . . 7
75	73, 74	fmptd 6385	. . . . . 6
76	75	adantr 481	. . . . 5 $/\$
77	66	rexrd 10089	. . . . 5 $/\$
78		itg2leub 23501	. . . . 5 $/\$
79	76, 77, 78	syl2anc 693	. . . 4 $/\$
80	69, 79	mtbid 314	. . 3 $/\$
81		rexanali 2998	. . 3 $/\$
82	80, 81	sylibr 224	. 2 $/\$ $/\$
83	66	ad2antrr 762	. . . . . . . 8 $/\$ $/\$ $/\$
84		itg1cl 23452	. . . . . . . . 9
85	84	ad2antlr 763	. . . . . . . 8 $/\$ $/\$ $/\$
86		eqid 2622	. . . . . . . . . . . 12
87	86	i1fpos 23473	. . . . . . . . . . 11
88		0re 10040	. . . . . . . . . . . . . 14
89		i1ff 23443	. . . . . . . . . . . . . . 15
90	89	ffvelrnda 6359	. . . . . . . . . . . . . 14 $/\$
91		max1 12016	. . . . . . . . . . . . . 14 $/\$
92	88, 90, 91	sylancr 695	. . . . . . . . . . . . 13 $/\$
93	92	ralrimiva 2966	. . . . . . . . . . . 12
94		ax-resscn 9993	. . . . . . . . . . . . . . 15
95	94	a1i 11	. . . . . . . . . . . . . 14
96		fvex 6201	. . . . . . . . . . . . . . . . 17
97		c0ex 10034	. . . . . . . . . . . . . . . . 17
98	96, 97	ifex 4156	. . . . . . . . . . . . . . . 16
99	98, 86	fnmpti 6022	. . . . . . . . . . . . . . 15
100	99	a1i 11	. . . . . . . . . . . . . 14
101	95, 100	0pledm 23440	. . . . . . . . . . . . 13
102		reex 10027	. . . . . . . . . . . . . . 15
103	102	a1i 11	. . . . . . . . . . . . . 14
104	97	a1i 11	. . . . . . . . . . . . . 14 $/\$
105		ifcl 4130	. . . . . . . . . . . . . . 15 $/\$
106	90, 88, 105	sylancl 694	. . . . . . . . . . . . . 14 $/\$
107		fconstmpt 5163	. . . . . . . . . . . . . . 15
108	107	a1i 11	. . . . . . . . . . . . . 14
109		eqidd 2623	. . . . . . . . . . . . . 14
110	103, 104, 106, 108, 109	ofrfval2 6915	. . . . . . . . . . . . 13
111	101, 110	bitrd 268	. . . . . . . . . . . 12
112	93, 111	mpbird 247	. . . . . . . . . . 11
113		itg2itg1 23503	. . . . . . . . . . 11 $/\$
114	87, 112, 113	syl2anc 693	. . . . . . . . . 10
115		itg1cl 23452	. . . . . . . . . . 11
116	87, 115	syl 17	. . . . . . . . . 10
117	114, 116	eqeltrd 2701	. . . . . . . . 9
118	117	ad2antlr 763	. . . . . . . 8 $/\$ $/\$ $/\$
119		ltnle 10117	. . . . . . . . . 10 $/\$
120	66, 84, 119	syl2an 494	. . . . . . . . 9 $/\$ $/\$
121	120	biimpar 502	. . . . . . . 8 $/\$ $/\$ $/\$
122		max2 12018	. . . . . . . . . . . . . 14 $/\$
123	88, 90, 122	sylancr 695	. . . . . . . . . . . . 13 $/\$
124	123	ralrimiva 2966	. . . . . . . . . . . 12
125	89	feqmptd 6249	. . . . . . . . . . . . 13
126	103, 90, 106, 125, 109	ofrfval2 6915	. . . . . . . . . . . 12
127	124, 126	mpbird 247	. . . . . . . . . . 11
128		itg1le 23480	. . . . . . . . . . 11 $/\$ $/\$
129	87, 127, 128	mpd3an23 1426	. . . . . . . . . 10
130	129, 114	breqtrrd 4681	. . . . . . . . 9
131	130	ad2antlr 763	. . . . . . . 8 $/\$ $/\$ $/\$
132	83, 85, 118, 121, 131	ltletrd 10197	. . . . . . 7 $/\$ $/\$ $/\$
133	132	adantrl 752	. . . . . 6 $/\$ $/\$ $/\$ $/\$
134		i1fmbf 23442	. . . . . . . . . . . . . . . 16 MblFn
135	87, 134	syl 17	. . . . . . . . . . . . . . 15 MblFn
136	135	adantl 482	. . . . . . . . . . . . . 14 $/\$ MblFn
137		elrege0 12278	. . . . . . . . . . . . . . . . 17 $/\$
138	106, 92, 137	sylanbrc 698	. . . . . . . . . . . . . . . 16 $/\$
139	138, 86	fmptd 6385	. . . . . . . . . . . . . . 15
140	139	adantl 482	. . . . . . . . . . . . . 14 $/\$
141	117	adantl 482	. . . . . . . . . . . . . 14 $/\$
142	106	recnd 10068	. . . . . . . . . . . . . . . . . . . 20 $/\$
143	142	negcld 10379	. . . . . . . . . . . . . . . . . . . 20 $/\$
144	142, 143	ifcld 4131	. . . . . . . . . . . . . . . . . . 19 $/\$
145		subcl 10280	. . . . . . . . . . . . . . . . . . 19 $/\$
146	32, 144, 145	syl2an 494	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
147	146	anassrs 680	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
148	147	abscld 14175	. . . . . . . . . . . . . . . 16 $/\$ $/\$
149	147	absge0d 14183	. . . . . . . . . . . . . . . 16 $/\$ $/\$
150		elrege0 12278	. . . . . . . . . . . . . . . 16 $/\$
151	148, 149, 150	sylanbrc 698	. . . . . . . . . . . . . . 15 $/\$ $/\$
152		eqid 2622	. . . . . . . . . . . . . . 15
153	151, 152	fmptd 6385	. . . . . . . . . . . . . 14 $/\$
154		eleq1 2689	. . . . . . . . . . . . . . . . . . . . . 22
155		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . 22
156	154, 155	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . 21
157	156	fveq2d 6195	. . . . . . . . . . . . . . . . . . . 20
158		eqid 2622	. . . . . . . . . . . . . . . . . . . 20
159		fvex 6201	. . . . . . . . . . . . . . . . . . . 20
160	157, 158, 159	fvmpt 6282	. . . . . . . . . . . . . . . . . . 19
161	157	breq2d 4665	. . . . . . . . . . . . . . . . . . . . 21
162		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . 23
163	162	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . 22
164	163, 162	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . 21
165	164	negeqd 10275	. . . . . . . . . . . . . . . . . . . . 21
166	161, 164, 165	ifbieq12d 4113	. . . . . . . . . . . . . . . . . . . 20
167		eqid 2622	. . . . . . . . . . . . . . . . . . . 20
168		negex 10279	. . . . . . . . . . . . . . . . . . . . 21
169	98, 168	ifex 4156	. . . . . . . . . . . . . . . . . . . 20
170	166, 167, 169	fvmpt 6282	. . . . . . . . . . . . . . . . . . 19
171	160, 170	oveq12d 6668	. . . . . . . . . . . . . . . . . 18
172	171	fveq2d 6195	. . . . . . . . . . . . . . . . 17
173	172	mpteq2ia 4740	. . . . . . . . . . . . . . . 16
174	173	fveq2i 6194	. . . . . . . . . . . . . . 15
175	102	a1i 11	. . . . . . . . . . . . . . . . . . 19
176		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22
177	176, 97	ifex 4156	. . . . . . . . . . . . . . . . . . . . 21
178	177, 97	ifex 4156	. . . . . . . . . . . . . . . . . . . 20
179	178	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
180		ovex 6678	. . . . . . . . . . . . . . . . . . . . 21
181	97, 180	ifex 4156	. . . . . . . . . . . . . . . . . . . 20
182	181	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
183		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
184		frn 6053	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
185		ref 13852	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
186		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
187	185, 186	ax-mp 5	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
188		fnco 5999	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
189	187, 188	mp3an1 1411	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
190	183, 184, 189	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . . . . 26
191		elpreima 6337	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
192	4, 190, 191	3syl 18	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
193		fco 6058	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31 $/\$
194	185, 4, 193	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30
195	194	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
196	195	biantrurd 529	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$ $/\$
197		elrege0 12278	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
198	196, 197	syl6bbr 278	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
199		fvco3 6275	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
200	4, 199	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
201	200	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
202	198, 201	bitr3d 270	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
203	202	pm5.32da 673	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
204	192, 203	bitrd 268	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
205	204	adantr 481	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
206		0le0 11110	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
207	206, 18	breqtrri 4680	. . . . . . . . . . . . . . . . . . . . . . . . . 26
208	207	biantru 526	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
209		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $\$ $/\$
210	209	baibr 945	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$
211	208, 210	syl5rbbr 275	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $/\$
212	211	adantl 482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $\$ $/\$
213	205, 212	orbi12d 746	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\/$ $\$ $/\$ $\/$ $/\$
214		elun 3753	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\/$ $\$
215		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
216	215	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . 23
217		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . 24
218	217	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . 23
219	216, 218	elimif 4122	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $\/$ $/\$
220	213, 214, 219	3bitr4g 303	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $\$
221	220	ifbid 4108	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$
222	221	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 $\$
223	220	ifbid 4108	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$
224	223	mpteq2dva 4744	. . . . . . . . . . . . . . . . . . 19 $\$
225	175, 179, 182, 222, 224	offval2 6914	. . . . . . . . . . . . . . . . . 18 $\$ $\$
226		ovif12 6739	. . . . . . . . . . . . . . . . . . . 20
227	89	ffvelrnda 6359	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
228	227	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
229		0cn 10032	. . . . . . . . . . . . . . . . . . . . . . 23
230		ifcl 4130	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
231	228, 229, 230	sylancl 694	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
232	231	addid1d 10236	. . . . . . . . . . . . . . . . . . . . 21 $/\$
233	231	mulm1d 10482	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
234	233	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
235	231	negcld 10379	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
236	235	addid2d 10237	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
237	234, 236	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
238	232, 237	ifeq12d 4106	. . . . . . . . . . . . . . . . . . . 20 $/\$
239	226, 238	syl5eq 2668	. . . . . . . . . . . . . . . . . . 19 $/\$
240	239	mpteq2dva 4744	. . . . . . . . . . . . . . . . . 18
241	225, 240	sylan9eq 2676	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$
242		0xr 10086	. . . . . . . . . . . . . . . . . . . . . . 23
243		pnfxr 10092	. . . . . . . . . . . . . . . . . . . . . . 23
244		0ltpnf 11956	. . . . . . . . . . . . . . . . . . . . . . 23
245		snunioo 12298	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
246	242, 243, 244, 245	mp3an 1424	. . . . . . . . . . . . . . . . . . . . . 22
247	246	imaeq2i 5464	. . . . . . . . . . . . . . . . . . . . 21
248		imaundi 5545	. . . . . . . . . . . . . . . . . . . . 21
249	247, 248	eqtr3i 2646	. . . . . . . . . . . . . . . . . . . 20
250		ismbfcn 23398	. . . . . . . . . . . . . . . . . . . . . . . 24 MblFn MblFn $/\$ MblFn
251	4, 250	syl 17	. . . . . . . . . . . . . . . . . . . . . . 23 MblFn MblFn $/\$ MblFn
252	43, 251	mpbid 222	. . . . . . . . . . . . . . . . . . . . . 22 MblFn $/\$ MblFn
253	252	simpld 475	. . . . . . . . . . . . . . . . . . . . 21 MblFn
254		mbfimasn 23401	. . . . . . . . . . . . . . . . . . . . . . 23 MblFn $/\$ $/\$
255	88, 254	mp3an3 1413	. . . . . . . . . . . . . . . . . . . . . 22 MblFn $/\$
256		mbfima 23399	. . . . . . . . . . . . . . . . . . . . . 22 MblFn $/\$
257		unmbl 23305	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
258	255, 256, 257	syl2anc 693	. . . . . . . . . . . . . . . . . . . . 21 MblFn $/\$
259	253, 194, 258	syl2anc 693	. . . . . . . . . . . . . . . . . . . 20
260	249, 259	syl5eqel 2705	. . . . . . . . . . . . . . . . . . 19
261		fdm 6051	. . . . . . . . . . . . . . . . . . . . . 22
262	4, 261	syl 17	. . . . . . . . . . . . . . . . . . . . 21
263		mbfdm 23395	. . . . . . . . . . . . . . . . . . . . . 22 MblFn
264	43, 263	syl 17	. . . . . . . . . . . . . . . . . . . . 21
265	262, 264	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . 20
266		difmbl 23311	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$
267	11, 265, 266	sylancr 695	. . . . . . . . . . . . . . . . . . 19 $\$
268		unmbl 23305	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $\$
269	260, 267, 268	syl2anc 693	. . . . . . . . . . . . . . . . . 18 $\$
270		fveq2 6191	. . . . . . . . . . . . . . . . . . . . . . . . . 26
271	270	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . 25
272	271, 270	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . . 24
273	272, 86, 177	fvmpt 6282	. . . . . . . . . . . . . . . . . . . . . . 23
274	273	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . 22
275	274	ifeq1d 4104	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$
276	275	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$
277	276	i1fres 23472	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $\$
278		id 22	. . . . . . . . . . . . . . . . . . . . 21
279		neg1rr 11125	. . . . . . . . . . . . . . . . . . . . . 22
280	279	a1i 11	. . . . . . . . . . . . . . . . . . . . 21
281	278, 280	i1fmulc 23470	. . . . . . . . . . . . . . . . . . . 20
282		cmmbl 23302	. . . . . . . . . . . . . . . . . . . 20 $\$ $\$ $\$
283		ifnot 4133	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$
284		eldif 3584	. . . . . . . . . . . . . . . . . . . . . . . . 25 $\$ $\$ $/\$ $\$
285	284	baibr 945	. . . . . . . . . . . . . . . . . . . . . . . 24 $\$ $\$ $\$
286		tru 1487	. . . . . . . . . . . . . . . . . . . . . . . . . 26
287		negex 10279	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29
288	287	fconst 6091	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
289		ffn 6045	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
290	288, 289	mp1i 13	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
291	99	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
292	102	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
293		inidm 3822	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
294	287	fvconst2 6469	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
295	294	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
296	273	adantl 482	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
297	290, 291, 292, 292, 293, 295, 296	ofval 6906	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
298	286, 297	mpan 706	. . . . . . . . . . . . . . . . . . . . . . . . 25
299	298	eqcomd 2628	. . . . . . . . . . . . . . . . . . . . . . . 24
300	285, 299	ifbieq1d 4109	. . . . . . . . . . . . . . . . . . . . . . 23 $\$ $\$ $\$
301	283, 300	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . 22 $\$ $\$ $\$
302	301	mpteq2ia 4740	. . . . . . . . . . . . . . . . . . . . 21 $\$ $\$ $\$
303	302	i1fres 23472	. . . . . . . . . . . . . . . . . . . 20 $/\$ $\$ $\$ $\$
304	281, 282, 303	syl2an 494	. . . . . . . . . . . . . . . . . . 19 $/\$ $\$ $\$
305	277, 304	i1fadd 23462	. . . . . . . . . . . . . . . . . 18 $/\$ $\$ $\$ $\$
306	87, 269, 305	syl2anr 495	. . . . . . . . . . . . . . . . 17 $/\$ $\$ $\$
307	241, 306	eqeltrrd 2702	. . . . . . . . . . . . . . . 16 $/\$
308	157	cbvmptv 4750	. . . . . . . . . . . . . . . . . . 19
309	308, 31	syl5eqel 2705	. . . . . . . . . . . . . . . . . 18
310	9, 308	fmptd 6385	. . . . . . . . . . . . . . . . . 18
311	309, 310	jca 554	. . . . . . . . . . . . . . . . 17 $/\$
312	311	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
313		ftc1anclem4 33488	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
314	313	3expb 1266	. . . . . . . . . . . . . . . 16 $/\$ $/\$
315	307, 312, 314	syl2anc 693	. . . . . . . . . . . . . . 15 $/\$
316	174, 315	syl5eqelr 2706	. . . . . . . . . . . . . 14 $/\$
317	136, 140, 141, 153, 316	itg2addnc 33464	. . . . . . . . . . . . 13 $/\$
318	102	a1i 11	. . . . . . . . . . . . . . 15 $/\$
319	98	a1i 11	. . . . . . . . . . . . . . 15 $/\$ $/\$
320		eqidd 2623	. . . . . . . . . . . . . . 15 $/\$
321		eqidd 2623	. . . . . . . . . . . . . . 15 $/\$
322	318, 319, 148, 320, 321	offval2 6914	. . . . . . . . . . . . . 14 $/\$
323	322	fveq2d 6195	. . . . . . . . . . . . 13 $/\$
324	317, 323	eqtr3d 2658	. . . . . . . . . . . 12 $/\$
325	324	adantr 481	. . . . . . . . . . 11 $/\$ $/\$
326		nfv 1843	. . . . . . . . . . . . . 14 $/\$
327		nfcv 2764	. . . . . . . . . . . . . . 15
328		nfcv 2764	. . . . . . . . . . . . . . 15
329		nfmpt1 4747	. . . . . . . . . . . . . . 15
330	327, 328, 329	nfbr 4699	. . . . . . . . . . . . . 14
331	326, 330	nfan 1828	. . . . . . . . . . . . 13 $/\$ $/\$
332		anass 681	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$
333		ffn 6045	. . . . . . . . . . . . . . . . . . . . 21
334	89, 333	syl 17	. . . . . . . . . . . . . . . . . . . 20
335		fvex 6201	. . . . . . . . . . . . . . . . . . . . . 22
336	335, 74	fnmpti 6022	. . . . . . . . . . . . . . . . . . . . 21
337	336	a1i 11	. . . . . . . . . . . . . . . . . . . 20
338		eqidd 2623	. . . . . . . . . . . . . . . . . . . 20 $/\$
339	74	fvmpt2 6291	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
340	335, 339	mpan2 707	. . . . . . . . . . . . . . . . . . . . 21
341	340	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$
342	334, 337, 103, 103, 293, 338, 341	ofrval 6907	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$
343	342	3com23 1271	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
344	343	3expa 1265	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
345	344	adantll 750	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
346		resubcl 10345	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
347	8, 106, 346	syl2an 494	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
348	347	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
349		absid 14036	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
350	8, 349	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$
351	350	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$
352	351	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$
353	352	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
354	353	adantllr 755	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
355		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . 24
356		breq1 4656	. . . . . . . . . . . . . . . . . . . . . . . 24
357	355, 356	ifboth 4124	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
358	354, 357	sylancom 701	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
359		subge0 10541	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
360	8, 106, 359	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
361	360	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
362	358, 361	mpbird 247	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
363	348, 362	absidd 14161	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
364		iftrue 4092	. . . . . . . . . . . . . . . . . . . . . . 23
365	364	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22
366	365	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
367	366	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
368	8	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$
369	349	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 $/\$
370	368, 369	sylan 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
371	363, 367, 370	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
372	106	renegcld 10457	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
373		resubcl 10345	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
374	8, 372, 373	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$
375	374	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
376	90	ad3antlr 767	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
377	8	ad3antrrr 766	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
378	8	adantr 481	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
379		ltnle 10117	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
380	88, 379	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
381		ltle 10126	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 33 $/\$
382	88, 381	mpan2 707	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 32
383	380, 382	sylbird 250	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . . 31
384	383	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
385		absnid 14038	. . . . . . . . . . . . . . . . . . . . . . . . . . . . . 30 $/\$
386	384, 385	syldan 487	. . . . . . . . . . . . . . . . . . . . . . . . . . . . 29 $/\$
387	386	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28 $/\$
388	387	biimpa 501	. . . . . . . . . . . . . . . . . . . . . . . . . . 27 $/\$ $/\$
389	388	an32s 846	. . . . . . . . . . . . . . . . . . . . . . . . . 26 $/\$ $/\$
390	378, 389	sylanl1 682	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$ $/\$
391	376, 377, 390	lenegcon2d 10610	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
392		simpll 790	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$ $/\$ $/\$
393	88	a1i 11	. . . . . . . . . . . . . . . . . . . . . . . . . . . 28
394	8, 393	ltnled 10184	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
395	8, 88, 381	sylancl 694	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
396	394, 395	sylbird 250	. . . . . . . . . . . . . . . . . . . . . . . . . 26
397	396	imp 445	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
398	392, 397	sylan 488	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$ $/\$ $/\$
399		negeq 10273	. . . . . . . . . . . . . . . . . . . . . . . . . 26
400	399	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . 25
401		neg0 10327	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
402		negeq 10273	. . . . . . . . . . . . . . . . . . . . . . . . . . 27
403	401, 402	syl5eqr 2670	. . . . . . . . . . . . . . . . . . . . . . . . . 26
404	403	breq2d 4665	. . . . . . . . . . . . . . . . . . . . . . . . 25
405	400, 404	ifboth 4124	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
406	391, 398, 405	syl2anc 693	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
407		suble0 10542	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
408	8, 372, 407	syl2an 494	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$ $/\$
409	408	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$ $/\$ $/\$ $/\$
410	406, 409	mpbird 247	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$ $/\$ $/\$
411	375, 410	absnidd 14152	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
412		subneg 10330	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
413	412	negeqd 10275	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
414		negdi2 10339	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
415	413, 414	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
416	32, 142, 415	syl2an 494	. . . . . . . . . . . . . . . . . . . . . 22 $/\$ $/\$
417	416	ad2antrr 762	. . . . . . . . . . . . . . . . . . . . 21 $/\$ $/\$ $/\$ $/\$
418	411, 417	eqtrd 2656	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
419		iffalse 4095	. . . . . . . . . . . . . . . . . . . . . . 23
420	419	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . . 22
421	420	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . 21
422	421	adantl 482	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
423	8, 385	sylan 488	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
424	397, 423	syldan 487	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
425	424	oveq1d 6665	. . . . . . . . . . . . . . . . . . . . 21 $/\$
426	392, 425	sylan 488	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
427	418, 422, 426	3eqtr4d 2666	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$ $/\$
428	371, 427	pm2.61dan 832	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
429	428	oveq2d 6666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
430	54	recnd 10068	. . . . . . . . . . . . . . . . . . 19
431		pncan3 10289	. . . . . . . . . . . . . . . . . . 19 $/\$
432	142, 430, 431	syl2anr 495	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
433	432	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
434	429, 433	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
435	345, 434	syldan 487	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
436	332, 435	sylanb 489	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
437	436	an32s 846	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
438	331, 437	mpteq2da 4743	. . . . . . . . . . . 12 $/\$ $/\$
439	438	fveq2d 6195	. . . . . . . . . . 11 $/\$ $/\$
440	325, 439	eqtrd 2656	. . . . . . . . . 10 $/\$ $/\$
441	440	breq1d 4663	. . . . . . . . 9 $/\$ $/\$
442	441	adantllr 755	. . . . . . . 8 $/\$ $/\$ $/\$
443	316	adantlr 751	. . . . . . . . . 10 $/\$ $/\$
444	64	ad2antlr 763	. . . . . . . . . 10 $/\$ $/\$
445	117	adantl 482	. . . . . . . . . 10 $/\$ $/\$
446	443, 444, 445	ltadd2d 10193	. . . . . . . . 9 $/\$ $/\$
447	446	adantr 481	. . . . . . . 8 $/\$ $/\$ $/\$
448		ltsubadd 10498	. . . . . . . . . . 11 $/\$ $/\$
449	61, 64, 117, 448	syl3an 1368	. . . . . . . . . 10 $/\$ $/\$
450	449	3expa 1265	. . . . . . . . 9 $/\$ $/\$
451	450	adantr 481	. . . . . . . 8 $/\$ $/\$ $/\$
452	442, 447, 451	3bitr4d 300	. . . . . . 7 $/\$ $/\$ $/\$
453	452	adantrr 753	. . . . . 6 $/\$ $/\$ $/\$ $/\$
454	133, 453	mpbird 247	. . . . 5 $/\$ $/\$ $/\$ $/\$
455	454	ex 450	. . . 4 $/\$ $/\$ $/\$
456	455	reximdva 3017	. . 3 $/\$ $/\$
457		fveq1 6190	. . . . . . . . . . . . . 14
458	457, 170	sylan9eq 2676	. . . . . . . . . . . . 13 $/\$
459	458	oveq2d 6666	. . . . . . . . . . . 12 $/\$
460	459	fveq2d 6195	. . . . . . . . . . 11 $/\$
461	460	mpteq2dva 4744	. . . . . . . . . 10
462	461	fveq2d 6195	. . . . . . . . 9
463	462	breq1d 4663	. . . . . . . 8
464	463	rspcev 3309	. . . . . . 7 $/\$
465	464	ex 450	. . . . . 6
466	307, 465	syl 17	. . . . 5 $/\$
467	466	rexlimdva 3031	. . . 4
468	467	adantr 481	. . 3 $/\$
469	456, 468	syld 47	. 2 $/\$ $/\$
470	82, 469	mpd 15	1 $/\$

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 196 $\/$ wo 383 $/\$ wa 384

wceq 1483

wtru 1484

wcel 1990

wral 2912

wrex 2913

cvv 3200 $\$ cdif 3571

cun 3572

wss 3574

cif 4086

csn 4177 class class class wbr 4653

cmpt 4729

cxp 5112

ccnv 5113

cdm 5114

crn 5115

cima 5117

ccom 5118

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cof 6895

cofr 6896

cc 9934

cr 9935

cc0 9936

c1 9937

caddc 9939

cmul 9941

cpnf 10071

cxr 10073

clt 10074

cle 10075

cmin 10266

cneg 10267

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

c0p 23436

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: ftc1anclem6 33490

W3C validator