ftc1anclem4 - Mathbox for Brendan Leahy

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

Theorem ftc1anclem4 30298

Description: Lemma for ftc1anc 30303. (Contributed by Brendan Leahy, 17-Jun-2018.)

**Assertion**
Ref	Expression
ftc1anclem4	$/\$ $/\$

Distinct variable groups:

Proof of Theorem ftc1anclem4 Dummy variable

is distinct from all other variables.

Step	Hyp	Ref	Expression
1		ffvelrn 6030	. . . . . . . . . 10 $/\$
2	1	recnd 9639	. . . . . . . . 9 $/\$
3		i1ff 22209	. . . . . . . . . . 11
4	3	ffvelrnda 6032	. . . . . . . . . 10 $/\$
5	4	recnd 9639	. . . . . . . . 9 $/\$
6		subcl 9838	. . . . . . . . 9 $/\$
7	2, 5, 6	syl2anr 478	. . . . . . . 8 $/\$ $/\$ $/\$
8	7	anandirs 831	. . . . . . 7 $/\$ $/\$
9	8	abscld 13279	. . . . . 6 $/\$ $/\$
10	9	rexrd 9660	. . . . 5 $/\$ $/\$
11	8	absge0d 13287	. . . . 5 $/\$ $/\$
12		elxrge0 11654	. . . . 5 $/\$
13	10, 11, 12	sylanbrc 664	. . . 4 $/\$ $/\$
14		eqid 2457	. . . 4
15	13, 14	fmptd 6056	. . 3 $/\$
16	15	3adant2 1015	. 2 $/\$ $/\$
17		reex 9600	. . . . . . 7
18	17	a1i 11	. . . . . 6 $/\$ $/\$
19		fvex 5882	. . . . . . 7
20	19	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
21		fvex 5882	. . . . . . 7
22	21	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
23		eqidd 2458	. . . . . 6 $/\$ $/\$
24		eqidd 2458	. . . . . 6 $/\$ $/\$
25	18, 20, 22, 23, 24	offval2 6555	. . . . 5 $/\$ $/\$
26	25	fveq2d 5876	. . . 4 $/\$ $/\$
27		id 22	. . . . . . . . . 10
28	27	feqmptd 5926	. . . . . . . . 9
29		absf 13182	. . . . . . . . . . 11
30	29	a1i 11	. . . . . . . . . 10
31	30	feqmptd 5926	. . . . . . . . 9
32		fveq2 5872	. . . . . . . . 9
33	2, 28, 31, 32	fmptco 6065	. . . . . . . 8
34	33	adantl 466	. . . . . . 7 $/\$
35		iblmbf 22300	. . . . . . . . 9 MblFn
36		ftc1anclem1 30295	. . . . . . . . 9 $/\$ MblFn MblFn
37	35, 36	sylan2 474	. . . . . . . 8 $/\$ MblFn
38	37	ancoms 453	. . . . . . 7 $/\$ MblFn
39	34, 38	eqeltrrd 2546	. . . . . 6 $/\$ MblFn
40	39	3adant1 1014	. . . . 5 $/\$ $/\$ MblFn
41	2	abscld 13279	. . . . . . . 8 $/\$
42	2	absge0d 13287	. . . . . . . 8 $/\$
43		elrege0 11652	. . . . . . . 8 $/\$
44	41, 42, 43	sylanbrc 664	. . . . . . 7 $/\$
45		eqid 2457	. . . . . . 7
46	44, 45	fmptd 6056	. . . . . 6
47	46	3ad2ant3 1019	. . . . 5 $/\$ $/\$
48		iftrue 3950	. . . . . . . . 9
49	48	mpteq2ia 4539	. . . . . . . 8
50	49	fveq2i 5875	. . . . . . 7
51	1	adantll 713	. . . . . . . . . 10 $/\$ $/\$
52		simpr 461	. . . . . . . . . . . 12 $/\$
53	52	feqmptd 5926	. . . . . . . . . . 11 $/\$
54		simpl 457	. . . . . . . . . . 11 $/\$
55	53, 54	eqeltrrd 2546	. . . . . . . . . 10 $/\$
56	51, 55, 39	iblabsnc 30284	. . . . . . . . 9 $/\$
57	41	adantll 713	. . . . . . . . . 10 $/\$ $/\$
58	42	adantll 713	. . . . . . . . . 10 $/\$ $/\$
59	57, 58	iblpos 22325	. . . . . . . . 9 $/\$ MblFn $/\$
60	56, 59	mpbid 210	. . . . . . . 8 $/\$ MblFn $/\$
61	60	simprd 463	. . . . . . 7 $/\$
62	50, 61	syl5eqelr 2550	. . . . . 6 $/\$
63	62	3adant1 1014	. . . . 5 $/\$ $/\$
64	5	abscld 13279	. . . . . . . 8 $/\$
65	5	absge0d 13287	. . . . . . . 8 $/\$
66		elrege0 11652	. . . . . . . 8 $/\$
67	64, 65, 66	sylanbrc 664	. . . . . . 7 $/\$
68		eqid 2457	. . . . . . 7
69	67, 68	fmptd 6056	. . . . . 6
70	69	3ad2ant1 1017	. . . . 5 $/\$ $/\$
71		iftrue 3950	. . . . . . . . 9
72	71	mpteq2ia 4539	. . . . . . . 8
73	72	fveq2i 5875	. . . . . . 7
74	3	feqmptd 5926	. . . . . . . . . . 11
75		i1fibl 22340	. . . . . . . . . . 11
76	74, 75	eqeltrrd 2546	. . . . . . . . . 10
77	29	a1i 11	. . . . . . . . . . . . 13
78	77	feqmptd 5926	. . . . . . . . . . . 12
79		fveq2 5872	. . . . . . . . . . . 12
80	5, 74, 78, 79	fmptco 6065	. . . . . . . . . . 11
81		i1fmbf 22208	. . . . . . . . . . . 12 MblFn
82		ftc1anclem1 30295	. . . . . . . . . . . 12 $/\$ MblFn MblFn
83	3, 81, 82	syl2anc 661	. . . . . . . . . . 11 MblFn
84	80, 83	eqeltrrd 2546	. . . . . . . . . 10 MblFn
85	4, 76, 84	iblabsnc 30284	. . . . . . . . 9
86	64, 65	iblpos 22325	. . . . . . . . 9 MblFn $/\$
87	85, 86	mpbid 210	. . . . . . . 8 MblFn $/\$
88	87	simprd 463	. . . . . . 7
89	73, 88	syl5eqelr 2550	. . . . . 6
90	89	3ad2ant1 1017	. . . . 5 $/\$ $/\$
91	40, 47, 63, 70, 90	itg2addnc 30274	. . . 4 $/\$ $/\$
92	26, 91	eqtr3d 2500	. . 3 $/\$ $/\$
93	63, 90	readdcld 9640	. . 3 $/\$ $/\$
94	92, 93	eqeltrd 2545	. 2 $/\$ $/\$
95		readdcl 9592	. . . . . . . . 9 $/\$
96	41, 64, 95	syl2anr 478	. . . . . . . 8 $/\$ $/\$ $/\$
97	96	anandirs 831	. . . . . . 7 $/\$ $/\$
98	97	rexrd 9660	. . . . . 6 $/\$ $/\$
99	41	adantll 713	. . . . . . 7 $/\$ $/\$
100	64	adantlr 714	. . . . . . 7 $/\$ $/\$
101	42	adantll 713	. . . . . . 7 $/\$ $/\$
102	65	adantlr 714	. . . . . . 7 $/\$ $/\$
103	99, 100, 101, 102	addge0d 10149	. . . . . 6 $/\$ $/\$
104		elxrge0 11654	. . . . . 6 $/\$
105	98, 103, 104	sylanbrc 664	. . . . 5 $/\$ $/\$
106		eqid 2457	. . . . 5
107	105, 106	fmptd 6056	. . . 4 $/\$
108	107	3adant2 1015	. . 3 $/\$ $/\$
109		abs2dif2 13178	. . . . . . . 8 $/\$
110	2, 5, 109	syl2anr 478	. . . . . . 7 $/\$ $/\$ $/\$
111	110	anandirs 831	. . . . . 6 $/\$ $/\$
112	111	ralrimiva 2871	. . . . 5 $/\$
113	17	a1i 11	. . . . . 6 $/\$
114		eqidd 2458	. . . . . 6 $/\$
115		eqidd 2458	. . . . . 6 $/\$
116	113, 9, 97, 114, 115	ofrfval2 6556	. . . . 5 $/\$
117	112, 116	mpbird 232	. . . 4 $/\$
118	117	3adant2 1015	. . 3 $/\$ $/\$
119		itg2le 22272	. . 3 $/\$ $/\$
120	16, 108, 118, 119	syl3anc 1228	. 2 $/\$ $/\$
121		itg2lecl 22271	. 2 $/\$ $/\$
122	16, 94, 120, 121	syl3anc 1228	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wcel 1819

wral 2807

cvv 3109

cif 3944 class class class wbr 4456

cmpt 4515

cdm 5008

ccom 5012

wf 5590

cfv 5594 (class class class)co 6296

cof 6537

cofr 6538

cc 9507

cr 9508

cc0 9509

caddc 9512

cpnf 9642

cxr 9644

cle 9646

cmin 9824

cico 11556

cicc 11557

cabs 13079 MblFncmbf 22149

citg1 22150

citg2 22151

cibl 22152

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1619 ax-4 1632 ax-5 1705 ax-6 1748 ax-7 1791 ax-8 1821 ax-9 1823 ax-10 1838 ax-11 1843 ax-12 1855 ax-13 2000 ax-ext 2435 ax-rep 4568 ax-sep 4578 ax-nul 4586 ax-pow 4634 ax-pr 4695 ax-un 6591 ax-inf2 8075 ax-cnex 9565 ax-resscn 9566 ax-1cn 9567 ax-icn 9568 ax-addcl 9569 ax-addrcl 9570 ax-mulcl 9571 ax-mulrcl 9572 ax-mulcom 9573 ax-addass 9574 ax-mulass 9575 ax-distr 9576 ax-i2m1 9577 ax-1ne0 9578 ax-1rid 9579 ax-rnegex 9580 ax-rrecex 9581 ax-cnre 9582 ax-pre-lttri 9583 ax-pre-lttrn 9584 ax-pre-ltadd 9585 ax-pre-mulgt0 9586 ax-pre-sup 9587 ax-addf 9588

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1398 df-fal 1401 df-ex 1614 df-nf 1618 df-sb 1741 df-eu 2287 df-mo 2288 df-clab 2443 df-cleq 2449 df-clel 2452 df-nfc 2607 df-ne 2654 df-nel 2655 df-ral 2812 df-rex 2813 df-reu 2814 df-rmo 2815 df-rab 2816 df-v 3111 df-sbc 3328 df-csb 3431 df-dif 3474 df-un 3476 df-in 3478 df-ss 3485 df-pss 3487 df-nul 3794 df-if 3945 df-pw 4017 df-sn 4033 df-pr 4035 df-tp 4037 df-op 4039 df-uni 4252 df-int 4289 df-iun 4334 df-disj 4428 df-br 4457 df-opab 4516 df-mpt 4517 df-tr 4551 df-eprel 4800 df-id 4804 df-po 4809 df-so 4810 df-fr 4847 df-se 4848 df-we 4849 df-ord 4890 df-on 4891 df-lim 4892 df-suc 4893 df-xp 5014 df-rel 5015 df-cnv 5016 df-co 5017 df-dm 5018 df-rn 5019 df-res 5020 df-ima 5021 df-iota 5557 df-fun 5596 df-fn 5597 df-f 5598 df-f1 5599 df-fo 5600 df-f1o 5601 df-fv 5602 df-isom 5603 df-riota 6258 df-ov 6299 df-oprab 6300 df-mpt2 6301 df-of 6539 df-ofr 6540 df-om 6700 df-1st 6799 df-2nd 6800 df-recs 7060 df-rdg 7094 df-1o 7148 df-2o 7149 df-oadd 7152 df-er 7329 df-map 7440 df-pm 7441 df-en 7536 df-dom 7537 df-sdom 7538 df-fin 7539 df-fi 7889 df-sup 7919 df-oi 7953 df-card 8337 df-cda 8565 df-pnf 9647 df-mnf 9648 df-xr 9649 df-ltxr 9650 df-le 9651 df-sub 9826 df-neg 9827 df-div 10228 df-nn 10557 df-2 10615 df-3 10616 df-n0 10817 df-z 10886 df-uz 11107 df-q 11208 df-rp 11246 df-xneg 11343 df-xadd 11344 df-xmul 11345 df-ioo 11558 df-ico 11560 df-icc 11561 df-fz 11698 df-fzo 11822 df-fl 11932 df-seq 12111 df-exp 12170 df-hash 12409 df-cj 12944 df-re 12945 df-im 12946 df-sqrt 13080 df-abs 13081 df-clim 13323 df-sum 13521 df-rest 14840 df-topgen 14861 df-psmet 18538 df-xmet 18539 df-met 18540 df-bl 18541 df-mopn 18542 df-top 19526 df-bases 19528 df-topon 19529 df-cmp 20014 df-ovol 22002 df-vol 22003 df-mbf 22154 df-itg1 22155 df-itg2 22156 df-ibl 22157 df-0p 22203

This theorem is referenced by: ftc1anclem5 30299 ftc1anclem6 30300

W3C validator