ftc1anclem8 - Mathbox for Brendan Leahy

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

Theorem ftc1anclem8 33492

Description: Lemma for ftc1anc 33493. (Contributed by Brendan Leahy, 29-May-2018.)

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

**Assertion**
Ref	Expression
ftc1anclem8	$/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$

Distinct variable groups:

Allowed substitution hints:

(

)

**Proof of Theorem ftc1anclem8**
Step	Hyp	Ref	Expression
1		ftc1anc.g	. . 3
2		ftc1anc.a	. . 3
3		ftc1anc.b	. . 3
4		ftc1anc.le	. . 3
5		ftc1anc.s	. . 3
6		ftc1anc.d	. . 3
7		ftc1anc.i	. . 3
8		ftc1anc.f	. . 3
9	1, 2, 3, 4, 5, 6, 7, 8	ftc1anclem7 33491	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
10		simplll 798	. . . 4 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
11		3simpa 1058	. . . 4 $/\$ $/\$ $/\$
12		ioossre 12235	. . . . . . . . 9
13	12	a1i 11	. . . . . . . 8 $/\$ $/\$
14		rembl 23308	. . . . . . . . 9
15	14	a1i 11	. . . . . . . 8 $/\$ $/\$
16		fvex 6201	. . . . . . . . . 10
17		c0ex 10034	. . . . . . . . . 10
18	16, 17	ifex 4156	. . . . . . . . 9
19	18	a1i 11	. . . . . . . 8 $/\$ $/\$ $/\$
20		eldifn 3733	. . . . . . . . . 10 $\$
21	20	adantl 482	. . . . . . . . 9 $/\$ $/\$ $/\$ $\$
22	21	iffalsed 4097	. . . . . . . 8 $/\$ $/\$ $/\$ $\$
23		iftrue 4092	. . . . . . . . . . . 12
24	23	mpteq2ia 4740	. . . . . . . . . . 11
25		resmpt 5449	. . . . . . . . . . . 12
26	12, 25	ax-mp 5	. . . . . . . . . . 11
27	24, 26	eqtr4i 2647	. . . . . . . . . 10
28		i1ff 23443	. . . . . . . . . . . . . . . . . 18
29	28	ffvelrnda 6359	. . . . . . . . . . . . . . . . 17 $/\$
30	29	recnd 10068	. . . . . . . . . . . . . . . 16 $/\$
31		ax-icn 9995	. . . . . . . . . . . . . . . . 17
32		i1ff 23443	. . . . . . . . . . . . . . . . . . 19
33	32	ffvelrnda 6359	. . . . . . . . . . . . . . . . . 18 $/\$
34	33	recnd 10068	. . . . . . . . . . . . . . . . 17 $/\$
35		mulcl 10020	. . . . . . . . . . . . . . . . 17 $/\$
36	31, 34, 35	sylancr 695	. . . . . . . . . . . . . . . 16 $/\$
37		addcl 10018	. . . . . . . . . . . . . . . 16 $/\$
38	30, 36, 37	syl2an 494	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
39	38	anandirs 874	. . . . . . . . . . . . . 14 $/\$ $/\$
40		reex 10027	. . . . . . . . . . . . . . . 16
41	40	a1i 11	. . . . . . . . . . . . . . 15 $/\$
42	29	adantlr 751	. . . . . . . . . . . . . . 15 $/\$ $/\$
43	36	adantll 750	. . . . . . . . . . . . . . 15 $/\$ $/\$
44	28	feqmptd 6249	. . . . . . . . . . . . . . . 16
45	44	adantr 481	. . . . . . . . . . . . . . 15 $/\$
46	40	a1i 11	. . . . . . . . . . . . . . . . 17
47	31	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
48		fconstmpt 5163	. . . . . . . . . . . . . . . . . 18
49	48	a1i 11	. . . . . . . . . . . . . . . . 17
50	32	feqmptd 6249	. . . . . . . . . . . . . . . . 17
51	46, 47, 33, 49, 50	offval2 6914	. . . . . . . . . . . . . . . 16
52	51	adantl 482	. . . . . . . . . . . . . . 15 $/\$
53	41, 42, 43, 45, 52	offval2 6914	. . . . . . . . . . . . . 14 $/\$
54		absf 14077	. . . . . . . . . . . . . . . 16
55	54	a1i 11	. . . . . . . . . . . . . . 15 $/\$
56	55	feqmptd 6249	. . . . . . . . . . . . . 14 $/\$
57		fveq2 6191	. . . . . . . . . . . . . 14
58	39, 53, 56, 57	fmptco 6396	. . . . . . . . . . . . 13 $/\$
59		ftc1anclem3 33487	. . . . . . . . . . . . 13 $/\$
60	58, 59	eqeltrrd 2702	. . . . . . . . . . . 12 $/\$
61		i1fmbf 23442	. . . . . . . . . . . 12 MblFn
62	60, 61	syl 17	. . . . . . . . . . 11 $/\$ MblFn
63		ioombl 23333	. . . . . . . . . . 11
64		mbfres 23411	. . . . . . . . . . 11 MblFn $/\$ MblFn
65	62, 63, 64	sylancl 694	. . . . . . . . . 10 $/\$ MblFn
66	27, 65	syl5eqel 2705	. . . . . . . . 9 $/\$ MblFn
67	66	adantl 482	. . . . . . . 8 $/\$ $/\$ MblFn
68	13, 15, 19, 22, 67	mbfss 23413	. . . . . . 7 $/\$ $/\$ MblFn
69	68	adantr 481	. . . . . 6 $/\$ $/\$ $/\$ $/\$ MblFn
70	39	abscld 14175	. . . . . . . . . 10 $/\$ $/\$
71	39	absge0d 14183	. . . . . . . . . 10 $/\$ $/\$
72		elrege0 12278	. . . . . . . . . 10 $/\$
73	70, 71, 72	sylanbrc 698	. . . . . . . . 9 $/\$ $/\$
74		0e0icopnf 12282	. . . . . . . . 9
75		ifcl 4130	. . . . . . . . 9 $/\$
76	73, 74, 75	sylancl 694	. . . . . . . 8 $/\$ $/\$
77		eqid 2622	. . . . . . . 8
78	76, 77	fmptd 6385	. . . . . . 7 $/\$
79	78	ad2antlr 763	. . . . . 6 $/\$ $/\$ $/\$ $/\$
80	70	rexrd 10089	. . . . . . . . . . 11 $/\$ $/\$
81		elxrge0 12281	. . . . . . . . . . 11 $/\$
82	80, 71, 81	sylanbrc 698	. . . . . . . . . 10 $/\$ $/\$
83		0e0iccpnf 12283	. . . . . . . . . 10
84		ifcl 4130	. . . . . . . . . 10 $/\$
85	82, 83, 84	sylancl 694	. . . . . . . . 9 $/\$ $/\$
86	85, 77	fmptd 6385	. . . . . . . 8 $/\$
87	86	ad2antlr 763	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
88		ifcl 4130	. . . . . . . . . . 11 $/\$
89	82, 83, 88	sylancl 694	. . . . . . . . . 10 $/\$ $/\$
90		eqid 2622	. . . . . . . . . 10
91	89, 90	fmptd 6385	. . . . . . . . 9 $/\$
92		ffn 6045	. . . . . . . . . . . . . . 15
93		frn 6053	. . . . . . . . . . . . . . . 16
94		ax-resscn 9993	. . . . . . . . . . . . . . . 16
95	93, 94	syl6ss 3615	. . . . . . . . . . . . . . 15
96		ffn 6045	. . . . . . . . . . . . . . . . 17
97	54, 96	ax-mp 5	. . . . . . . . . . . . . . . 16
98		fnco 5999	. . . . . . . . . . . . . . . 16 $/\$ $/\$
99	97, 98	mp3an1 1411	. . . . . . . . . . . . . . 15 $/\$
100	92, 95, 99	syl2anc 693	. . . . . . . . . . . . . 14
101	28, 100	syl 17	. . . . . . . . . . . . 13
102	101	adantr 481	. . . . . . . . . . . 12 $/\$
103		ffn 6045	. . . . . . . . . . . . . . 15
104		frn 6053	. . . . . . . . . . . . . . . 16
105	104, 94	syl6ss 3615	. . . . . . . . . . . . . . 15
106		fnco 5999	. . . . . . . . . . . . . . . 16 $/\$ $/\$
107	97, 106	mp3an1 1411	. . . . . . . . . . . . . . 15 $/\$
108	103, 105, 107	syl2anc 693	. . . . . . . . . . . . . 14
109	32, 108	syl 17	. . . . . . . . . . . . 13
110	109	adantl 482	. . . . . . . . . . . 12 $/\$
111		inidm 3822	. . . . . . . . . . . 12
112	28	adantr 481	. . . . . . . . . . . . 13 $/\$
113		fvco3 6275	. . . . . . . . . . . . 13 $/\$
114	112, 113	sylan 488	. . . . . . . . . . . 12 $/\$ $/\$
115	32	adantl 482	. . . . . . . . . . . . 13 $/\$
116		fvco3 6275	. . . . . . . . . . . . 13 $/\$
117	115, 116	sylan 488	. . . . . . . . . . . 12 $/\$ $/\$
118	102, 110, 41, 41, 111, 114, 117	offval 6904	. . . . . . . . . . 11 $/\$
119	30	addid1d 10236	. . . . . . . . . . . . . . . . 17 $/\$
120	119	mpteq2dva 4744	. . . . . . . . . . . . . . . 16
121	40	a1i 11	. . . . . . . . . . . . . . . . 17
122	17	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
123	31	a1i 11	. . . . . . . . . . . . . . . . . . 19 $/\$
124	48	a1i 11	. . . . . . . . . . . . . . . . . . 19
125		fconstmpt 5163	. . . . . . . . . . . . . . . . . . . 20
126	125	a1i 11	. . . . . . . . . . . . . . . . . . 19
127	121, 123, 122, 124, 126	offval2 6914	. . . . . . . . . . . . . . . . . 18
128		it0e0 11254	. . . . . . . . . . . . . . . . . . 19
129	128	mpteq2i 4741	. . . . . . . . . . . . . . . . . 18
130	127, 129	syl6eq 2672	. . . . . . . . . . . . . . . . 17
131	121, 29, 122, 44, 130	offval2 6914	. . . . . . . . . . . . . . . 16
132	120, 131, 44	3eqtr4d 2666	. . . . . . . . . . . . . . 15
133	132	coeq2d 5284	. . . . . . . . . . . . . 14
134		i1f0 23454	. . . . . . . . . . . . . . 15
135		ftc1anclem3 33487	. . . . . . . . . . . . . . 15 $/\$
136	134, 135	mpan2 707	. . . . . . . . . . . . . 14
137	133, 136	eqeltrrd 2702	. . . . . . . . . . . . 13
138	137	adantr 481	. . . . . . . . . . . 12 $/\$
139		coeq2 5280	. . . . . . . . . . . . . . 15
140	139	eleq1d 2686	. . . . . . . . . . . . . 14
141	140, 137	vtoclga 3272	. . . . . . . . . . . . 13
142	141	adantl 482	. . . . . . . . . . . 12 $/\$
143	138, 142	i1fadd 23462	. . . . . . . . . . 11 $/\$
144	118, 143	eqeltrrd 2702	. . . . . . . . . 10 $/\$
145	30	abscld 14175	. . . . . . . . . . . . . . . 16 $/\$
146	30	absge0d 14183	. . . . . . . . . . . . . . . 16 $/\$
147		elrege0 12278	. . . . . . . . . . . . . . . 16 $/\$
148	145, 146, 147	sylanbrc 698	. . . . . . . . . . . . . . 15 $/\$
149	34	abscld 14175	. . . . . . . . . . . . . . . 16 $/\$
150	34	absge0d 14183	. . . . . . . . . . . . . . . 16 $/\$
151		elrege0 12278	. . . . . . . . . . . . . . . 16 $/\$
152	149, 150, 151	sylanbrc 698	. . . . . . . . . . . . . . 15 $/\$
153		ge0addcl 12284	. . . . . . . . . . . . . . 15 $/\$
154	148, 152, 153	syl2an 494	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
155	154	anandirs 874	. . . . . . . . . . . . 13 $/\$ $/\$
156		eqid 2622	. . . . . . . . . . . . 13
157	155, 156	fmptd 6385	. . . . . . . . . . . 12 $/\$
158		0plef 23439	. . . . . . . . . . . 12 $/\$
159	157, 158	sylib 208	. . . . . . . . . . 11 $/\$ $/\$
160	159	simprd 479	. . . . . . . . . 10 $/\$
161		itg2itg1 23503	. . . . . . . . . . 11 $/\$
162		itg1cl 23452	. . . . . . . . . . . 12
163	162	adantr 481	. . . . . . . . . . 11 $/\$
164	161, 163	eqeltrd 2701	. . . . . . . . . 10 $/\$
165	144, 160, 164	syl2anc 693	. . . . . . . . 9 $/\$
166		icossicc 12260	. . . . . . . . . . 11
167		fss 6056	. . . . . . . . . . 11 $/\$
168	157, 166, 167	sylancl 694	. . . . . . . . . 10 $/\$
169		0re 10040	. . . . . . . . . . . . . 14
170		ifcl 4130	. . . . . . . . . . . . . 14 $/\$
171	70, 169, 170	sylancl 694	. . . . . . . . . . . . 13 $/\$ $/\$
172		readdcl 10019	. . . . . . . . . . . . . . 15 $/\$
173	145, 149, 172	syl2an 494	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
174	173	anandirs 874	. . . . . . . . . . . . 13 $/\$ $/\$
175	70	leidd 10594	. . . . . . . . . . . . . 14 $/\$ $/\$
176		breq1 4656	. . . . . . . . . . . . . . 15
177		breq1 4656	. . . . . . . . . . . . . . 15
178	176, 177	ifboth 4124	. . . . . . . . . . . . . 14 $/\$
179	175, 71, 178	syl2anc 693	. . . . . . . . . . . . 13 $/\$ $/\$
180		abstri 14070	. . . . . . . . . . . . . . . 16 $/\$
181	30, 36, 180	syl2an 494	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
182	181	anandirs 874	. . . . . . . . . . . . . 14 $/\$ $/\$
183		absmul 14034	. . . . . . . . . . . . . . . . . . 19 $/\$
184	31, 34, 183	sylancr 695	. . . . . . . . . . . . . . . . . 18 $/\$
185		absi 14026	. . . . . . . . . . . . . . . . . . 19
186	185	oveq1i 6660	. . . . . . . . . . . . . . . . . 18
187	184, 186	syl6eq 2672	. . . . . . . . . . . . . . . . 17 $/\$
188	149	recnd 10068	. . . . . . . . . . . . . . . . . 18 $/\$
189	188	mulid2d 10058	. . . . . . . . . . . . . . . . 17 $/\$
190	187, 189	eqtrd 2656	. . . . . . . . . . . . . . . 16 $/\$
191	190	adantll 750	. . . . . . . . . . . . . . 15 $/\$ $/\$
192	191	oveq2d 6666	. . . . . . . . . . . . . 14 $/\$ $/\$
193	182, 192	breqtrd 4679	. . . . . . . . . . . . 13 $/\$ $/\$
194	171, 70, 174, 179, 193	letrd 10194	. . . . . . . . . . . 12 $/\$ $/\$
195	194	ralrimiva 2966	. . . . . . . . . . 11 $/\$
196		eqidd 2623	. . . . . . . . . . . 12 $/\$
197		eqidd 2623	. . . . . . . . . . . 12 $/\$
198	41, 171, 174, 196, 197	ofrfval2 6915	. . . . . . . . . . 11 $/\$
199	195, 198	mpbird 247	. . . . . . . . . 10 $/\$
200		itg2le 23506	. . . . . . . . . 10 $/\$ $/\$
201	91, 168, 199, 200	syl3anc 1326	. . . . . . . . 9 $/\$
202		itg2lecl 23505	. . . . . . . . 9 $/\$ $/\$
203	91, 165, 201, 202	syl3anc 1326	. . . . . . . 8 $/\$
204	203	ad2antlr 763	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
205	91	ad2antlr 763	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
206		breq1 4656	. . . . . . . . . . 11
207		breq1 4656	. . . . . . . . . . 11
208		elioore 12205	. . . . . . . . . . . . . . 15
209	208, 175	sylan2 491	. . . . . . . . . . . . . 14 $/\$ $/\$
210	209	adantll 750	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
211	210	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
212	2	rexrd 10089	. . . . . . . . . . . . . . . . . 18
213	3	rexrd 10089	. . . . . . . . . . . . . . . . . 18
214	212, 213	jca 554	. . . . . . . . . . . . . . . . 17 $/\$
215		df-icc 12182	. . . . . . . . . . . . . . . . . . . . 21 $/\$
216	215	elixx3g 12188	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
217	216	simprbi 480	. . . . . . . . . . . . . . . . . . 19 $/\$
218	217	simpld 475	. . . . . . . . . . . . . . . . . 18
219	215	elixx3g 12188	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$ $/\$
220	219	simprbi 480	. . . . . . . . . . . . . . . . . . 19 $/\$
221	220	simprd 479	. . . . . . . . . . . . . . . . . 18
222	218, 221	anim12i 590	. . . . . . . . . . . . . . . . 17 $/\$ $/\$
223		ioossioo 12265	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
224	214, 222, 223	syl2an 494	. . . . . . . . . . . . . . . 16 $/\$ $/\$
225	5	adantr 481	. . . . . . . . . . . . . . . 16 $/\$ $/\$
226	224, 225	sstrd 3613	. . . . . . . . . . . . . . 15 $/\$ $/\$
227	226	sselda 3603	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
228		iftrue 4092	. . . . . . . . . . . . . 14
229	227, 228	syl 17	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
230	229	adantllr 755	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
231	211, 230	breqtrrd 4681	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
232		breq2 4657	. . . . . . . . . . . . 13
233		breq2 4657	. . . . . . . . . . . . 13
234	6	sselda 3603	. . . . . . . . . . . . . . 15 $/\$
235	234	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
236	71	adantll 750	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
237	235, 236	syldan 487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
238		0le0 11110	. . . . . . . . . . . . . 14
239	238	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
240	232, 233, 237, 239	ifbothda 4123	. . . . . . . . . . . 12 $/\$ $/\$
241	240	ad2antrr 762	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
242	206, 207, 231, 241	ifbothda 4123	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
243	242	ralrimivw 2967	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
244	40	a1i 11	. . . . . . . . . . 11
245	18	a1i 11	. . . . . . . . . . 11 $/\$
246	16, 17	ifex 4156	. . . . . . . . . . . 12
247	246	a1i 11	. . . . . . . . . . 11 $/\$
248		eqidd 2623	. . . . . . . . . . 11
249		eqidd 2623	. . . . . . . . . . 11
250	244, 245, 247, 248, 249	ofrfval2 6915	. . . . . . . . . 10
251	250	ad2antrr 762	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
252	243, 251	mpbird 247	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
253		itg2le 23506	. . . . . . . 8 $/\$ $/\$
254	87, 205, 252, 253	syl3anc 1326	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
255		itg2lecl 23505	. . . . . . 7 $/\$ $/\$
256	87, 204, 254, 255	syl3anc 1326	. . . . . 6 $/\$ $/\$ $/\$ $/\$
257	8	ffvelrnda 6359	. . . . . . . . . . . . . . 15 $/\$
258	257	adantlr 751	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
259	227, 258	syldan 487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
260	259	adantllr 755	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
261	208, 39	sylan2 491	. . . . . . . . . . . . . 14 $/\$ $/\$
262	261	adantll 750	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$
263	262	adantlr 751	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$ $/\$
264	260, 263	subcld 10392	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
265	264	abscld 14175	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
266	264	absge0d 14183	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
267		elrege0 12278	. . . . . . . . . 10 $/\$
268	265, 266, 267	sylanbrc 698	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
269	74	a1i 11	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
270	268, 269	ifclda 4120	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
271	270	adantr 481	. . . . . . 7 $/\$ $/\$ $/\$ $/\$ $/\$
272		eqid 2622	. . . . . . 7
273	271, 272	fmptd 6385	. . . . . 6 $/\$ $/\$ $/\$ $/\$
274	265	rexrd 10089	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
275		elxrge0 12281	. . . . . . . . . . 11 $/\$
276	274, 266, 275	sylanbrc 698	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
277	83	a1i 11	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
278	276, 277	ifclda 4120	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
279	278	adantr 481	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
280	279, 272	fmptd 6385	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
281		recncf 22705	. . . . . . . . . . . . 13
282		prid1g 4295	. . . . . . . . . . . . 13
283	281, 282	ax-mp 5	. . . . . . . . . . . 12
284		ftc1anclem2 33486	. . . . . . . . . . . 12 $/\$ $/\$
285	283, 284	mp3an3 1413	. . . . . . . . . . 11 $/\$
286	8, 7, 285	syl2anc 693	. . . . . . . . . 10
287		imcncf 22706	. . . . . . . . . . . . 13
288		prid2g 4296	. . . . . . . . . . . . 13
289	287, 288	ax-mp 5	. . . . . . . . . . . 12
290		ftc1anclem2 33486	. . . . . . . . . . . 12 $/\$ $/\$
291	289, 290	mp3an3 1413	. . . . . . . . . . 11 $/\$
292	8, 7, 291	syl2anc 693	. . . . . . . . . 10
293	286, 292	readdcld 10069	. . . . . . . . 9
294	293	ad2antrr 762	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
295	204, 294	readdcld 10069	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
296		ge0addcl 12284	. . . . . . . . . . . . 13 $/\$
297	296	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
298		ifcl 4130	. . . . . . . . . . . . . . 15 $/\$
299	73, 74, 298	sylancl 694	. . . . . . . . . . . . . 14 $/\$ $/\$
300	299, 90	fmptd 6385	. . . . . . . . . . . . 13 $/\$
301	300	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$
302	296	adantl 482	. . . . . . . . . . . . . 14 $/\$ $/\$
303	257	recld 13934	. . . . . . . . . . . . . . . . . . . 20 $/\$
304	303	recnd 10068	. . . . . . . . . . . . . . . . . . 19 $/\$
305	304	abscld 14175	. . . . . . . . . . . . . . . . . 18 $/\$
306	304	absge0d 14183	. . . . . . . . . . . . . . . . . 18 $/\$
307		elrege0 12278	. . . . . . . . . . . . . . . . . 18 $/\$
308	305, 306, 307	sylanbrc 698	. . . . . . . . . . . . . . . . 17 $/\$
309	74	a1i 11	. . . . . . . . . . . . . . . . 17 $/\$
310	308, 309	ifclda 4120	. . . . . . . . . . . . . . . 16
311	310	adantr 481	. . . . . . . . . . . . . . 15 $/\$
312		eqid 2622	. . . . . . . . . . . . . . 15
313	311, 312	fmptd 6385	. . . . . . . . . . . . . 14
314	257	imcld 13935	. . . . . . . . . . . . . . . . . . . 20 $/\$
315	314	recnd 10068	. . . . . . . . . . . . . . . . . . 19 $/\$
316	315	abscld 14175	. . . . . . . . . . . . . . . . . 18 $/\$
317	315	absge0d 14183	. . . . . . . . . . . . . . . . . 18 $/\$
318		elrege0 12278	. . . . . . . . . . . . . . . . . 18 $/\$
319	316, 317, 318	sylanbrc 698	. . . . . . . . . . . . . . . . 17 $/\$
320	319, 309	ifclda 4120	. . . . . . . . . . . . . . . 16
321	320	adantr 481	. . . . . . . . . . . . . . 15 $/\$
322		eqid 2622	. . . . . . . . . . . . . . 15
323	321, 322	fmptd 6385	. . . . . . . . . . . . . 14
324	302, 313, 323, 244, 244, 111	off 6912	. . . . . . . . . . . . 13
325	324	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$
326	40	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
327	297, 301, 325, 326, 326, 111	off 6912	. . . . . . . . . . 11 $/\$ $/\$
328		fss 6056	. . . . . . . . . . 11 $/\$
329	327, 166, 328	sylancl 694	. . . . . . . . . 10 $/\$ $/\$
330	329	adantr 481	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
331		0xr 10086	. . . . . . . . . . . . . 14
332	331	a1i 11	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
333	274, 332	ifclda 4120	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
334	257	adantlr 751	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
335	39	adantll 750	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
336	235, 335	syldan 487	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
337	334, 336	subcld 10392	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
338	337	abscld 14175	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
339	338	rexrd 10089	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
340	331	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$
341	339, 340	ifclda 4120	. . . . . . . . . . . . 13 $/\$ $/\$
342	341	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
343	336	abscld 14175	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
344		0red 10041	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
345	343, 344	ifclda 4120	. . . . . . . . . . . . . . 15 $/\$ $/\$
346		0red 10041	. . . . . . . . . . . . . . . . . 18 $/\$
347	305, 346	ifclda 4120	. . . . . . . . . . . . . . . . 17
348	316, 346	ifclda 4120	. . . . . . . . . . . . . . . . 17
349	347, 348	readdcld 10069	. . . . . . . . . . . . . . . 16
350	349	adantr 481	. . . . . . . . . . . . . . 15 $/\$ $/\$
351	345, 350	readdcld 10069	. . . . . . . . . . . . . 14 $/\$ $/\$
352	351	rexrd 10089	. . . . . . . . . . . . 13 $/\$ $/\$
353	352	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
354		breq1 4656	. . . . . . . . . . . . 13
355		breq1 4656	. . . . . . . . . . . . 13
356	227	adantllr 755	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
357	338	leidd 10594	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
358	357	adantlr 751	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
359		iftrue 4092	. . . . . . . . . . . . . . . 16
360	359	adantl 482	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$ $/\$ $/\$
361	358, 360	breqtrrd 4681	. . . . . . . . . . . . . 14 $/\$ $/\$ $/\$ $/\$ $/\$
362	356, 361	syldan 487	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
363		breq2 4657	. . . . . . . . . . . . . . 15
364		breq2 4657	. . . . . . . . . . . . . . 15
365	337	absge0d 14183	. . . . . . . . . . . . . . 15 $/\$ $/\$ $/\$
366	363, 364, 365, 239	ifbothda 4123	. . . . . . . . . . . . . 14 $/\$ $/\$
367	366	ad2antrr 762	. . . . . . . . . . . . 13 $/\$ $/\$ $/\$ $/\$ $/\$
368	354, 355, 362, 367	ifbothda 4123	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
369	257	negcld 10379	. . . . . . . . . . . . . . . . . . . . 21 $/\$
370	369	adantlr 751	. . . . . . . . . . . . . . . . . . . 20 $/\$ $/\$ $/\$
371	336, 370	addcld 10059	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
372	371	abscld 14175	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
373	369	abscld 14175	. . . . . . . . . . . . . . . . . . . 20 $/\$
374	373	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
375	343, 374	readdcld 10069	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
376	305, 316	readdcld 10069	. . . . . . . . . . . . . . . . . . . 20 $/\$
377	376	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
378	343, 377	readdcld 10069	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
379	336, 370	abstrid 14195	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
380		mulcl 10020	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
381	31, 315, 380	sylancr 695	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
382	304, 381	abstrid 14195	. . . . . . . . . . . . . . . . . . . . 21 $/\$
383	257	absnegd 14188	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
384	257	replimd 13937	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
385	384	fveq2d 6195	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
386	383, 385	eqtrd 2656	. . . . . . . . . . . . . . . . . . . . 21 $/\$
387		absmul 14034	. . . . . . . . . . . . . . . . . . . . . . . . 25 $/\$
388	31, 315, 387	sylancr 695	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
389	185	oveq1i 6660	. . . . . . . . . . . . . . . . . . . . . . . 24
390	388, 389	syl6eq 2672	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
391	316	recnd 10068	. . . . . . . . . . . . . . . . . . . . . . . 24 $/\$
392	391	mulid2d 10058	. . . . . . . . . . . . . . . . . . . . . . 23 $/\$
393	390, 392	eqtr2d 2657	. . . . . . . . . . . . . . . . . . . . . 22 $/\$
394	393	oveq2d 6666	. . . . . . . . . . . . . . . . . . . . 21 $/\$
395	382, 386, 394	3brtr4d 4685	. . . . . . . . . . . . . . . . . . . 20 $/\$
396	395	adantlr 751	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
397	374, 377, 343, 396	leadd2dd 10642	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
398	372, 375, 378, 379, 397	letrd 10194	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
399	334, 336	abssubd 14192	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
400	359	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
401	336, 334	negsubd 10398	. . . . . . . . . . . . . . . . . . 19 $/\$ $/\$ $/\$
402	401	fveq2d 6195	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$ $/\$
403	399, 400, 402	3eqtr4d 2666	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
404		iftrue 4092	. . . . . . . . . . . . . . . . . 18
405	404	adantl 482	. . . . . . . . . . . . . . . . 17 $/\$ $/\$ $/\$
406	398, 403, 405	3brtr4d 4685	. . . . . . . . . . . . . . . 16 $/\$ $/\$ $/\$
407	406	ex 450	. . . . . . . . . . . . . . 15 $/\$ $/\$
408	238	a1i 11	. . . . . . . . . . . . . . . 16
409		iffalse 4095	. . . . . . . . . . . . . . . 16
410		iffalse 4095	. . . . . . . . . . . . . . . 16
411	408, 409, 410	3brtr4d 4685	. . . . . . . . . . . . . . 15
412	407, 411	pm2.61d1 171	. . . . . . . . . . . . . 14 $/\$ $/\$
413		iftrue 4092	. . . . . . . . . . . . . . . . . 18
414		iftrue 4092	. . . . . . . . . . . . . . . . . 18
415	413, 414	oveq12d 6668	. . . . . . . . . . . . . . . . 17
416	228, 415	oveq12d 6668	. . . . . . . . . . . . . . . 16
417	416, 404	eqtr4d 2659	. . . . . . . . . . . . . . 15
418		00id 10211	. . . . . . . . . . . . . . . . . 18
419	418	oveq2i 6661	. . . . . . . . . . . . . . . . 17
420	419, 418	eqtri 2644	. . . . . . . . . . . . . . . 16
421		iffalse 4095	. . . . . . . . . . . . . . . . 17
422		iffalse 4095	. . . . . . . . . . . . . . . . . 18
423		iffalse 4095	. . . . . . . . . . . . . . . . . 18
424	422, 423	oveq12d 6668	. . . . . . . . . . . . . . . . 17
425	421, 424	oveq12d 6668	. . . . . . . . . . . . . . . 16
426	420, 425, 410	3eqtr4a 2682	. . . . . . . . . . . . . . 15
427	417, 426	pm2.61i 176	. . . . . . . . . . . . . 14
428	412, 427	syl6breqr 4695	. . . . . . . . . . . . 13 $/\$ $/\$
429	428	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $/\$
430	333, 342, 353, 368, 429	xrletrd 11993	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$
431	430	ralrimivw 2967	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
432		fvex 6201	. . . . . . . . . . . . . 14
433	432, 17	ifex 4156	. . . . . . . . . . . . 13
434	433	a1i 11	. . . . . . . . . . . 12 $/\$
435		ovexd 6680	. . . . . . . . . . . 12 $/\$
436		eqidd 2623	. . . . . . . . . . . 12
437		ovexd 6680	. . . . . . . . . . . . 13 $/\$
438	347	adantr 481	. . . . . . . . . . . . . 14 $/\$
439	348	adantr 481	. . . . . . . . . . . . . 14 $/\$
440		eqidd 2623	. . . . . . . . . . . . . 14
441		eqidd 2623	. . . . . . . . . . . . . 14
442	244, 438, 439, 440, 441	offval2 6914	. . . . . . . . . . . . 13
443	244, 247, 437, 249, 442	offval2 6914	. . . . . . . . . . . 12
444	244, 434, 435, 436, 443	ofrfval2 6915	. . . . . . . . . . 11
445	444	ad2antrr 762	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$
446	431, 445	mpbird 247	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$
447		itg2le 23506	. . . . . . . . 9 $/\$ $/\$
448	280, 330, 446, 447	syl3anc 1326	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
449	6	adantr 481	. . . . . . . . . . . 12 $/\$ $/\$
450	246	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$ $/\$
451		eldifn 3733	. . . . . . . . . . . . . 14 $\$
452	451	iffalsed 4097	. . . . . . . . . . . . 13 $\$
453	452	adantl 482	. . . . . . . . . . . 12 $/\$ $/\$ $/\$ $\$
454		ovexd 6680	. . . . . . . . . . . . . . . . . 18 $/\$ $/\$
455	41, 42, 454, 45, 52	offval2 6914	. . . . . . . . . . . . . . . . 17 $/\$
456	39, 455, 56, 57	fmptco 6396	. . . . . . . . . . . . . . . 16 $/\$
457	456	reseq1d 5395	. . . . . . . . . . . . . . 15 $/\$
458	6	resmptd 5452	. . . . . . . . . . . . . . 15
459	457, 458	sylan9eqr 2678	. . . . . . . . . . . . . 14 $/\$ $/\$
460	228	mpteq2ia 4740	. . . . . . . . . . . . . 14
461	459, 460	syl6eqr 2674	. . . . . . . . . . . . 13 $/\$ $/\$
462		i1fmbf 23442	. . . . . . . . . . . . . . 15 MblFn
463	59, 462	syl 17	. . . . . . . . . . . . . 14 $/\$ MblFn
464		fdm 6051	. . . . . . . . . . . . . . . 16
465	8, 464	syl 17	. . . . . . . . . . . . . . 15
466		iblmbf 23534	. . . . . . . . . . . . . . . 16 MblFn
467		mbfdm 23395	. . . . . . . . . . . . . . . 16 MblFn
468	7, 466, 467	3syl 18	. . . . . . . . . . . . . . 15
469	465, 468	eqeltrrd 2702	. . . . . . . . . . . . . 14
470		mbfres 23411	. . . . . . . . . . . . . 14 MblFn $/\$ MblFn
471	463, 469, 470	syl2anr 495	. . . . . . . . . . . . 13 $/\$ $/\$ MblFn
472	461, 471	eqeltrrd 2702	. . . . . . . . . . . 12 $/\$ $/\$ MblFn
473	449, 15, 450, 453, 472	mbfss 23413	. . . . . . . . . . 11 $/\$ $/\$ MblFn
474	203	adantl 482	. . . . . . . . . . 11 $/\$ $/\$
475		0cnd 10033	. . . . . . . . . . . . . . . . . 18 $/\$
476	304, 475	ifclda 4120	. . . . . . . . . . . . . . . . 17
477	476	adantr 481	. . . . . . . . . . . . . . . 16 $/\$
478		eqidd 2623	. . . . . . . . . . . . . . . 16
479	54	a1i 11	. . . . . . . . . . . . . . . . 17
480	479	feqmptd 6249	. . . . . . . . . . . . . . . 16
481		fveq2 6191	. . . . . . . . . . . . . . . . 17
482		fvif 6204	. . . . . . . . . . . . . . . . . 18
483		abs0 14025	. . . . . . . . . . . . . . . . . . 19
484		ifeq2 4091	. . . . . . . . . . . . . . . . . . 19
485	483, 484	ax-mp 5	. . . . . . . . . . . . . . . . . 18
486	482, 485	eqtri 2644	. . . . . . . . . . . . . . . . 17
487	481, 486	syl6eq 2672	. . . . . . . . . . . . . . . 16
488	477, 478, 480, 487	fmptco 6396	. . . . . . . . . . . . . . 15
489	303, 346	ifclda 4120	. . . . . . . . . . . . . . . . . 18
490	489	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
491		eqid 2622	. . . . . . . . . . . . . . . . 17
492	490, 491	fmptd 6385	. . . . . . . . . . . . . . . 16
493	14	a1i 11	. . . . . . . . . . . . . . . . 17
494	489	adantr 481	. . . . . . . . . . . . . . . . 17 $/\$
495	451	adantl 482	. . . . . . . . . . . . . . . . . 18 $/\$ $\$
496	495	iffalsed 4097	. . . . . . . . . . . . . . . . 17 $/\$ $\$
497		iftrue 4092	. . . . . . . . . . . . . . . . . . 19
498	497	mpteq2ia 4740	. . . . . . . . . . . . . . . . . 18
499	8	feqmptd 6249	. . . . . . . . . . . . . . . . . . . . 21
500	7, 466	syl 17	. . . . . . . . . . . . . . . . . . . . 21 MblFn
501	499, 500	eqeltrrd 2702	. . . . . . . . . . . . . . . . . . . 20 MblFn
502	257	ismbfcn2 23406	. . . . . . . . . . . . . . . . . . . 20 MblFn MblFn $/\$ MblFn
503	501, 502	mpbid 222	. . . . . . . . . . . . . . . . . . 19 MblFn $/\$ MblFn
504	503	simpld 475	. . . . . . . . . . . . . . . . . 18 MblFn
505	498, 504	syl5eqel 2705	. . . . . . . . . . . . . . . . 17 MblFn
506	6, 493, 494, 496, 505	mbfss 23413	. . . . . . . . . . . . . . . 16 MblFn
507		ftc1anclem1 33485	. . . . . . . . . . . . . . . 16 $/\$ MblFn MblFn
508	492, 506, 507	syl2anc 693	. . . . . . . . . . . . . . 15 MblFn
509	488, 508	eqeltrrd 2702	. . . . . . . . . . . . . 14 MblFn
510	509, 313, 286, 323, 292	itg2addnc 33464	. . . . . . . . . . . . 13
511	510, 293	eqeltrd 2701	. . . . . . . . . . . 12
512	511	adantr 481	. . . . . . . . . . 11 $/\$ $/\$
513	473, 301, 474, 325, 512	itg2addnc 33464	. . . . . . . . . 10 $/\$ $/\$
514	510	adantr 481	. . . . . . . . . . 11 $/\$ $/\$
515	514	oveq2d 6666	. . . . . . . . . 10 $/\$ $/\$
516	513, 515	eqtrd 2656	. . . . . . . . 9 $/\$ $/\$
517	516	adantr 481	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
518	448, 517	breqtrd 4679	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
519		itg2lecl 23505	. . . . . . 7 $/\$ $/\$
520	280, 295, 518, 519	syl3anc 1326	. . . . . 6 $/\$ $/\$ $/\$ $/\$
521	69, 79, 256, 273, 520	itg2addnc 33464	. . . . 5 $/\$ $/\$ $/\$ $/\$
522	244, 245, 434, 248, 436	offval2 6914	. . . . . . . . 9
523		eqeq2 2633	. . . . . . . . . . 11
524		eqeq2 2633	. . . . . . . . . . 11
525		iftrue 4092	. . . . . . . . . . . . 13
526	23, 525	oveq12d 6668	. . . . . . . . . . . 12
527	526	adantl 482	. . . . . . . . . . 11 $/\$
528		iffalse 4095	. . . . . . . . . . . . . 14
529		iffalse 4095	. . . . . . . . . . . . . 14
530	528, 529	oveq12d 6668	. . . . . . . . . . . . 13
531	530, 418	syl6eq 2672	. . . . . . . . . . . 12
532	531	adantl 482	. . . . . . . . . . 11 $/\$
533	523, 524, 527, 532	ifbothda 4123	. . . . . . . . . 10
534	533	mpteq2dv 4745	. . . . . . . . 9
535	522, 534	eqtrd 2656	. . . . . . . 8
536	535	ad2antrr 762	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
537		simplr 792	. . . . . . . . . . 11 $/\$ $/\$ $/\$ $/\$ $/\$
538	261	abscld 14175	. . . . . . . . . . . 12 $/\$ $/\$
539	538	recnd 10068	. . . . . . . . . . 11 $/\$ $/\$
540	537, 539	sylan 488	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
541	265	recnd 10068	. . . . . . . . . 10 $/\$ $/\$ $/\$ $/\$ $/\$
542	540, 541	addcomd 10238	. . . . . . . . 9 $/\$ $/\$ $/\$ $/\$ $/\$
543	542	ifeq1da 4116	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$
544	543	mpteq2dv 4745	. . . . . . 7 $/\$ $/\$ $/\$ $/\$
545	536, 544	eqtrd 2656	. . . . . 6 $/\$ $/\$ $/\$ $/\$
546	545	fveq2d 6195	. . . . 5 $/\$ $/\$ $/\$ $/\$
547	521, 546	eqtr3d 2658	. . . 4 $/\$ $/\$ $/\$ $/\$
548	10, 11, 547	syl2an 494	. . 3 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
549	548	adantr 481	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
550		rpcn 11841	. . . 4
551	550	2halvesd 11278	. . 3
552	551	ad3antlr 767	. 2 $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$ $/\$
553	9, 549, 552	3brtr3d 4684	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

cvv 3200 $\$ cdif 3571

cun 3572

wss 3574

cif 4086

csn 4177

cpr 4179 class class class wbr 4653

cmpt 4729

cxp 5112

cdm 5114

crn 5115

cres 5116

cima 5117

ccom 5118

wfn 5883

wf 5884

cfv 5888 (class class class)co 6650

cof 6895

cofr 6896

csup 8346

cc 9934

cr 9935

cc0 9936

c1 9937

ci 9938

caddc 9939

cmul 9941

cpnf 10071

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

ccncf 22679

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-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-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-rlim 14220 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-cncf 22681 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