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 28613

Description: Lemma for ftc1anc 28618. (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 5945	. . . . . . . . . 10 $/\$
2	1	recnd 9518	. . . . . . . . 9 $/\$
3		i1ff 21282	. . . . . . . . . . 11
4	3	ffvelrnda 5947	. . . . . . . . . 10 $/\$
5	4	recnd 9518	. . . . . . . . 9 $/\$
6		subcl 9715	. . . . . . . . 9 $/\$
7	2, 5, 6	syl2anr 478	. . . . . . . 8 $/\$ $/\$ $/\$
8	7	anandirs 827	. . . . . . 7 $/\$ $/\$
9	8	abscld 13035	. . . . . 6 $/\$ $/\$
10	9	rexrd 9539	. . . . 5 $/\$ $/\$
11	8	absge0d 13043	. . . . 5 $/\$ $/\$
12		elxrge0 11506	. . . . 5 $/\$
13	10, 11, 12	sylanbrc 664	. . . 4 $/\$ $/\$
14		eqid 2452	. . . 4
15	13, 14	fmptd 5971	. . 3 $/\$
16	15	3adant2 1007	. 2 $/\$ $/\$
17		reex 9479	. . . . . . 7
18	17	a1i 11	. . . . . 6 $/\$ $/\$
19		fvex 5804	. . . . . . 7
20	19	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
21		fvex 5804	. . . . . . 7
22	21	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
23		eqidd 2453	. . . . . 6 $/\$ $/\$
24		eqidd 2453	. . . . . 6 $/\$ $/\$
25	18, 20, 22, 23, 24	offval2 6441	. . . . 5 $/\$ $/\$
26	25	fveq2d 5798	. . . 4 $/\$ $/\$
27		id 22	. . . . . . . . . 10
28	27	feqmptd 5848	. . . . . . . . 9
29		absf 12938	. . . . . . . . . . 11
30	29	a1i 11	. . . . . . . . . 10
31	30	feqmptd 5848	. . . . . . . . 9
32		fveq2 5794	. . . . . . . . 9
33	2, 28, 31, 32	fmptco 5980	. . . . . . . 8
34	33	adantl 466	. . . . . . 7 $/\$
35		iblmbf 21373	. . . . . . . . 9 MblFn
36		ftc1anclem1 28610	. . . . . . . . 9 $/\$ MblFn MblFn
37	35, 36	sylan2 474	. . . . . . . 8 $/\$ MblFn
38	37	ancoms 453	. . . . . . 7 $/\$ MblFn
39	34, 38	eqeltrrd 2541	. . . . . 6 $/\$ MblFn
40	39	3adant1 1006	. . . . 5 $/\$ $/\$ MblFn
41	2	abscld 13035	. . . . . . . 8 $/\$
42	2	absge0d 13043	. . . . . . . 8 $/\$
43		elrege0 11504	. . . . . . . 8 $/\$
44	41, 42, 43	sylanbrc 664	. . . . . . 7 $/\$
45		eqid 2452	. . . . . . 7
46	44, 45	fmptd 5971	. . . . . 6
47	46	3ad2ant3 1011	. . . . 5 $/\$ $/\$
48		iftrue 3900	. . . . . . . . 9
49	48	mpteq2ia 4477	. . . . . . . 8
50	49	fveq2i 5797	. . . . . . 7
51	1	adantll 713	. . . . . . . . . 10 $/\$ $/\$
52		simpr 461	. . . . . . . . . . . 12 $/\$
53	52	feqmptd 5848	. . . . . . . . . . 11 $/\$
54		simpl 457	. . . . . . . . . . 11 $/\$
55	53, 54	eqeltrrd 2541	. . . . . . . . . 10 $/\$
56	51, 55, 39	iblabsnc 28599	. . . . . . . . 9 $/\$
57	41	adantll 713	. . . . . . . . . 10 $/\$ $/\$
58	42	adantll 713	. . . . . . . . . 10 $/\$ $/\$
59	57, 58	iblpos 21398	. . . . . . . . 9 $/\$ MblFn $/\$
60	56, 59	mpbid 210	. . . . . . . 8 $/\$ MblFn $/\$
61	60	simprd 463	. . . . . . 7 $/\$
62	50, 61	syl5eqelr 2545	. . . . . 6 $/\$
63	62	3adant1 1006	. . . . 5 $/\$ $/\$
64	5	abscld 13035	. . . . . . . 8 $/\$
65	5	absge0d 13043	. . . . . . . 8 $/\$
66		elrege0 11504	. . . . . . . 8 $/\$
67	64, 65, 66	sylanbrc 664	. . . . . . 7 $/\$
68		eqid 2452	. . . . . . 7
69	67, 68	fmptd 5971	. . . . . 6
70	69	3ad2ant1 1009	. . . . 5 $/\$ $/\$
71		iftrue 3900	. . . . . . . . 9
72	71	mpteq2ia 4477	. . . . . . . 8
73	72	fveq2i 5797	. . . . . . 7
74	3	feqmptd 5848	. . . . . . . . . . 11
75		i1fibl 21413	. . . . . . . . . . 11
76	74, 75	eqeltrrd 2541	. . . . . . . . . 10
77	29	a1i 11	. . . . . . . . . . . . 13
78	77	feqmptd 5848	. . . . . . . . . . . 12
79		fveq2 5794	. . . . . . . . . . . 12
80	5, 74, 78, 79	fmptco 5980	. . . . . . . . . . 11
81		i1fmbf 21281	. . . . . . . . . . . 12 MblFn
82		ftc1anclem1 28610	. . . . . . . . . . . 12 $/\$ MblFn MblFn
83	3, 81, 82	syl2anc 661	. . . . . . . . . . 11 MblFn
84	80, 83	eqeltrrd 2541	. . . . . . . . . 10 MblFn
85	4, 76, 84	iblabsnc 28599	. . . . . . . . 9
86	64, 65	iblpos 21398	. . . . . . . . 9 MblFn $/\$
87	85, 86	mpbid 210	. . . . . . . 8 MblFn $/\$
88	87	simprd 463	. . . . . . 7
89	73, 88	syl5eqelr 2545	. . . . . 6
90	89	3ad2ant1 1009	. . . . 5 $/\$ $/\$
91	40, 47, 63, 70, 90	itg2addnc 28589	. . . 4 $/\$ $/\$
92	26, 91	eqtr3d 2495	. . 3 $/\$ $/\$
93	63, 90	readdcld 9519	. . 3 $/\$ $/\$
94	92, 93	eqeltrd 2540	. 2 $/\$ $/\$
95		readdcl 9471	. . . . . . . . 9 $/\$
96	41, 64, 95	syl2anr 478	. . . . . . . 8 $/\$ $/\$ $/\$
97	96	anandirs 827	. . . . . . 7 $/\$ $/\$
98	97	rexrd 9539	. . . . . 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 10021	. . . . . 6 $/\$ $/\$
104		elxrge0 11506	. . . . . 6 $/\$
105	98, 103, 104	sylanbrc 664	. . . . 5 $/\$ $/\$
106		eqid 2452	. . . . 5
107	105, 106	fmptd 5971	. . . 4 $/\$
108	107	3adant2 1007	. . 3 $/\$ $/\$
109		abs2dif2 12934	. . . . . . . 8 $/\$
110	2, 5, 109	syl2anr 478	. . . . . . 7 $/\$ $/\$ $/\$
111	110	anandirs 827	. . . . . 6 $/\$ $/\$
112	111	ralrimiva 2827	. . . . 5 $/\$
113	17	a1i 11	. . . . . 6 $/\$
114		eqidd 2453	. . . . . 6 $/\$
115		eqidd 2453	. . . . . 6 $/\$
116	113, 9, 97, 114, 115	ofrfval2 6442	. . . . 5 $/\$
117	112, 116	mpbird 232	. . . 4 $/\$
118	117	3adant2 1007	. . 3 $/\$ $/\$
119		itg2le 21345	. . 3 $/\$ $/\$
120	16, 108, 118, 119	syl3anc 1219	. 2 $/\$ $/\$
121		itg2lecl 21344	. 2 $/\$ $/\$
122	16, 94, 120, 121	syl3anc 1219	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1370

wcel 1758

wral 2796

cvv 3072

cif 3894 class class class wbr 4395

cmpt 4453

cdm 4943

ccom 4947

wf 5517

cfv 5521 (class class class)co 6195

cof 6423

cofr 6424

cc 9386

cr 9387

cc0 9388

caddc 9391

cpnf 9521

cxr 9523

cle 9525

cmin 9701

cico 11408

cicc 11409

cabs 12836 MblFncmbf 21222

citg1 21223

citg2 21224

cibl 21225

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1592 ax-4 1603 ax-5 1671 ax-6 1710 ax-7 1730 ax-8 1760 ax-9 1762 ax-10 1777 ax-11 1782 ax-12 1794 ax-13 1954 ax-ext 2431 ax-rep 4506 ax-sep 4516 ax-nul 4524 ax-pow 4573 ax-pr 4634 ax-un 6477 ax-inf2 7953 ax-cnex 9444 ax-resscn 9445 ax-1cn 9446 ax-icn 9447 ax-addcl 9448 ax-addrcl 9449 ax-mulcl 9450 ax-mulrcl 9451 ax-mulcom 9452 ax-addass 9453 ax-mulass 9454 ax-distr 9455 ax-i2m1 9456 ax-1ne0 9457 ax-1rid 9458 ax-rnegex 9459 ax-rrecex 9460 ax-cnre 9461 ax-pre-lttri 9462 ax-pre-lttrn 9463 ax-pre-ltadd 9464 ax-pre-mulgt0 9465 ax-pre-sup 9466 ax-addf 9467

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 966 df-3an 967 df-tru 1373 df-fal 1376 df-ex 1588 df-nf 1591 df-sb 1703 df-eu 2265 df-mo 2266 df-clab 2438 df-cleq 2444 df-clel 2447 df-nfc 2602 df-ne 2647 df-nel 2648 df-ral 2801 df-rex 2802 df-reu 2803 df-rmo 2804 df-rab 2805 df-v 3074 df-sbc 3289 df-csb 3391 df-dif 3434 df-un 3436 df-in 3438 df-ss 3445 df-pss 3447 df-nul 3741 df-if 3895 df-pw 3965 df-sn 3981 df-pr 3983 df-tp 3985 df-op 3987 df-uni 4195 df-int 4232 df-iun 4276 df-disj 4366 df-br 4396 df-opab 4454 df-mpt 4455 df-tr 4489 df-eprel 4735 df-id 4739 df-po 4744 df-so 4745 df-fr 4782 df-se 4783 df-we 4784 df-ord 4825 df-on 4826 df-lim 4827 df-suc 4828 df-xp 4949 df-rel 4950 df-cnv 4951 df-co 4952 df-dm 4953 df-rn 4954 df-res 4955 df-ima 4956 df-iota 5484 df-fun 5523 df-fn 5524 df-f 5525 df-f1 5526 df-fo 5527 df-f1o 5528 df-fv 5529 df-isom 5530 df-riota 6156 df-ov 6198 df-oprab 6199 df-mpt2 6200 df-of 6425 df-ofr 6426 df-om 6582 df-1st 6682 df-2nd 6683 df-recs 6937 df-rdg 6971 df-1o 7025 df-2o 7026 df-oadd 7029 df-er 7206 df-map 7321 df-pm 7322 df-en 7416 df-dom 7417 df-sdom 7418 df-fin 7419 df-fi 7767 df-sup 7797 df-oi 7830 df-card 8215 df-cda 8443 df-pnf 9526 df-mnf 9527 df-xr 9528 df-ltxr 9529 df-le 9530 df-sub 9703 df-neg 9704 df-div 10100 df-nn 10429 df-2 10486 df-3 10487 df-n0 10686 df-z 10753 df-uz 10968 df-q 11060 df-rp 11098 df-xneg 11195 df-xadd 11196 df-xmul 11197 df-ioo 11410 df-ico 11412 df-icc 11413 df-fz 11550 df-fzo 11661 df-fl 11754 df-seq 11919 df-exp 11978 df-hash 12216 df-cj 12701 df-re 12702 df-im 12703 df-sqr 12837 df-abs 12838 df-clim 13079 df-sum 13277 df-rest 14475 df-topgen 14496 df-psmet 17929 df-xmet 17930 df-met 17931 df-bl 17932 df-mopn 17933 df-top 18630 df-bases 18632 df-topon 18633 df-cmp 19117 df-ovol 21075 df-vol 21076 df-mbf 21227 df-itg1 21228 df-itg2 21229 df-ibl 21230 df-0p 21276

This theorem is referenced by: ftc1anclem5 28614 ftc1anclem6 28615

W3C validator