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 30011

Description: Lemma for ftc1anc 30016. (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 9634	. . . . . . . . 9 $/\$
3		i1ff 21951	. . . . . . . . . . 11
4	3	ffvelrnda 6032	. . . . . . . . . 10 $/\$
5	4	recnd 9634	. . . . . . . . 9 $/\$
6		subcl 9831	. . . . . . . . 9 $/\$
7	2, 5, 6	syl2anr 478	. . . . . . . 8 $/\$ $/\$ $/\$
8	7	anandirs 829	. . . . . . 7 $/\$ $/\$
9	8	abscld 13247	. . . . . 6 $/\$ $/\$
10	9	rexrd 9655	. . . . 5 $/\$ $/\$
11	8	absge0d 13255	. . . . 5 $/\$ $/\$
12		elxrge0 11641	. . . . 5 $/\$
13	10, 11, 12	sylanbrc 664	. . . 4 $/\$ $/\$
14		eqid 2467	. . . 4
15	13, 14	fmptd 6056	. . 3 $/\$
16	15	3adant2 1015	. 2 $/\$ $/\$
17		reex 9595	. . . . . . 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 2468	. . . . . 6 $/\$ $/\$
24		eqidd 2468	. . . . . 6 $/\$ $/\$
25	18, 20, 22, 23, 24	offval2 6551	. . . . 5 $/\$ $/\$
26	25	fveq2d 5876	. . . 4 $/\$ $/\$
27		id 22	. . . . . . . . . 10
28	27	feqmptd 5927	. . . . . . . . 9
29		absf 13150	. . . . . . . . . . 11
30	29	a1i 11	. . . . . . . . . 10
31	30	feqmptd 5927	. . . . . . . . 9
32		fveq2 5872	. . . . . . . . 9
33	2, 28, 31, 32	fmptco 6065	. . . . . . . 8
34	33	adantl 466	. . . . . . 7 $/\$
35		iblmbf 22042	. . . . . . . . 9 MblFn
36		ftc1anclem1 30008	. . . . . . . . 9 $/\$ MblFn MblFn
37	35, 36	sylan2 474	. . . . . . . 8 $/\$ MblFn
38	37	ancoms 453	. . . . . . 7 $/\$ MblFn
39	34, 38	eqeltrrd 2556	. . . . . 6 $/\$ MblFn
40	39	3adant1 1014	. . . . 5 $/\$ $/\$ MblFn
41	2	abscld 13247	. . . . . . . 8 $/\$
42	2	absge0d 13255	. . . . . . . 8 $/\$
43		elrege0 11639	. . . . . . . 8 $/\$
44	41, 42, 43	sylanbrc 664	. . . . . . 7 $/\$
45		eqid 2467	. . . . . . 7
46	44, 45	fmptd 6056	. . . . . 6
47	46	3ad2ant3 1019	. . . . 5 $/\$ $/\$
48		iftrue 3951	. . . . . . . . 9
49	48	mpteq2ia 4535	. . . . . . . 8
50	49	fveq2i 5875	. . . . . . 7
51	1	adantll 713	. . . . . . . . . 10 $/\$ $/\$
52		simpr 461	. . . . . . . . . . . 12 $/\$
53	52	feqmptd 5927	. . . . . . . . . . 11 $/\$
54		simpl 457	. . . . . . . . . . 11 $/\$
55	53, 54	eqeltrrd 2556	. . . . . . . . . 10 $/\$
56	51, 55, 39	iblabsnc 29997	. . . . . . . . 9 $/\$
57	41	adantll 713	. . . . . . . . . 10 $/\$ $/\$
58	42	adantll 713	. . . . . . . . . 10 $/\$ $/\$
59	57, 58	iblpos 22067	. . . . . . . . 9 $/\$ MblFn $/\$
60	56, 59	mpbid 210	. . . . . . . 8 $/\$ MblFn $/\$
61	60	simprd 463	. . . . . . 7 $/\$
62	50, 61	syl5eqelr 2560	. . . . . 6 $/\$
63	62	3adant1 1014	. . . . 5 $/\$ $/\$
64	5	abscld 13247	. . . . . . . 8 $/\$
65	5	absge0d 13255	. . . . . . . 8 $/\$
66		elrege0 11639	. . . . . . . 8 $/\$
67	64, 65, 66	sylanbrc 664	. . . . . . 7 $/\$
68		eqid 2467	. . . . . . 7
69	67, 68	fmptd 6056	. . . . . 6
70	69	3ad2ant1 1017	. . . . 5 $/\$ $/\$
71		iftrue 3951	. . . . . . . . 9
72	71	mpteq2ia 4535	. . . . . . . 8
73	72	fveq2i 5875	. . . . . . 7
74	3	feqmptd 5927	. . . . . . . . . . 11
75		i1fibl 22082	. . . . . . . . . . 11
76	74, 75	eqeltrrd 2556	. . . . . . . . . 10
77	29	a1i 11	. . . . . . . . . . . . 13
78	77	feqmptd 5927	. . . . . . . . . . . 12
79		fveq2 5872	. . . . . . . . . . . 12
80	5, 74, 78, 79	fmptco 6065	. . . . . . . . . . 11
81		i1fmbf 21950	. . . . . . . . . . . 12 MblFn
82		ftc1anclem1 30008	. . . . . . . . . . . 12 $/\$ MblFn MblFn
83	3, 81, 82	syl2anc 661	. . . . . . . . . . 11 MblFn
84	80, 83	eqeltrrd 2556	. . . . . . . . . 10 MblFn
85	4, 76, 84	iblabsnc 29997	. . . . . . . . 9
86	64, 65	iblpos 22067	. . . . . . . . 9 MblFn $/\$
87	85, 86	mpbid 210	. . . . . . . 8 MblFn $/\$
88	87	simprd 463	. . . . . . 7
89	73, 88	syl5eqelr 2560	. . . . . 6
90	89	3ad2ant1 1017	. . . . 5 $/\$ $/\$
91	40, 47, 63, 70, 90	itg2addnc 29987	. . . 4 $/\$ $/\$
92	26, 91	eqtr3d 2510	. . 3 $/\$ $/\$
93	63, 90	readdcld 9635	. . 3 $/\$ $/\$
94	92, 93	eqeltrd 2555	. 2 $/\$ $/\$
95		readdcl 9587	. . . . . . . . 9 $/\$
96	41, 64, 95	syl2anr 478	. . . . . . . 8 $/\$ $/\$ $/\$
97	96	anandirs 829	. . . . . . 7 $/\$ $/\$
98	97	rexrd 9655	. . . . . 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 10140	. . . . . 6 $/\$ $/\$
104		elxrge0 11641	. . . . . 6 $/\$
105	98, 103, 104	sylanbrc 664	. . . . 5 $/\$ $/\$
106		eqid 2467	. . . . 5
107	105, 106	fmptd 6056	. . . 4 $/\$
108	107	3adant2 1015	. . 3 $/\$ $/\$
109		abs2dif2 13146	. . . . . . . 8 $/\$
110	2, 5, 109	syl2anr 478	. . . . . . 7 $/\$ $/\$ $/\$
111	110	anandirs 829	. . . . . 6 $/\$ $/\$
112	111	ralrimiva 2881	. . . . 5 $/\$
113	17	a1i 11	. . . . . 6 $/\$
114		eqidd 2468	. . . . . 6 $/\$
115		eqidd 2468	. . . . . 6 $/\$
116	113, 9, 97, 114, 115	ofrfval2 6552	. . . . 5 $/\$
117	112, 116	mpbird 232	. . . 4 $/\$
118	117	3adant2 1015	. . 3 $/\$ $/\$
119		itg2le 22014	. . 3 $/\$ $/\$
120	16, 108, 118, 119	syl3anc 1228	. 2 $/\$ $/\$
121		itg2lecl 22013	. 2 $/\$ $/\$
122	16, 94, 120, 121	syl3anc 1228	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1379

wcel 1767

wral 2817

cvv 3118

cif 3945 class class class wbr 4453

cmpt 4511

cdm 5005

ccom 5009

wf 5590

cfv 5594 (class class class)co 6295

cof 6533

cofr 6534

cc 9502

cr 9503

cc0 9504

caddc 9507

cpnf 9637

cxr 9639

cle 9641

cmin 9817

cico 11543

cicc 11544

cabs 13047 MblFncmbf 21891

citg1 21892

citg2 21893

cibl 21894

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1601 ax-4 1612 ax-5 1680 ax-6 1719 ax-7 1739 ax-8 1769 ax-9 1771 ax-10 1786 ax-11 1791 ax-12 1803 ax-13 1968 ax-ext 2445 ax-rep 4564 ax-sep 4574 ax-nul 4582 ax-pow 4631 ax-pr 4692 ax-un 6587 ax-inf2 8070 ax-cnex 9560 ax-resscn 9561 ax-1cn 9562 ax-icn 9563 ax-addcl 9564 ax-addrcl 9565 ax-mulcl 9566 ax-mulrcl 9567 ax-mulcom 9568 ax-addass 9569 ax-mulass 9570 ax-distr 9571 ax-i2m1 9572 ax-1ne0 9573 ax-1rid 9574 ax-rnegex 9575 ax-rrecex 9576 ax-cnre 9577 ax-pre-lttri 9578 ax-pre-lttrn 9579 ax-pre-ltadd 9580 ax-pre-mulgt0 9581 ax-pre-sup 9582 ax-addf 9583

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 974 df-3an 975 df-tru 1382 df-fal 1385 df-ex 1597 df-nf 1600 df-sb 1712 df-eu 2279 df-mo 2280 df-clab 2453 df-cleq 2459 df-clel 2462 df-nfc 2617 df-ne 2664 df-nel 2665 df-ral 2822 df-rex 2823 df-reu 2824 df-rmo 2825 df-rab 2826 df-v 3120 df-sbc 3337 df-csb 3441 df-dif 3484 df-un 3486 df-in 3488 df-ss 3495 df-pss 3497 df-nul 3791 df-if 3946 df-pw 4018 df-sn 4034 df-pr 4036 df-tp 4038 df-op 4040 df-uni 4252 df-int 4289 df-iun 4333 df-disj 4424 df-br 4454 df-opab 4512 df-mpt 4513 df-tr 4547 df-eprel 4797 df-id 4801 df-po 4806 df-so 4807 df-fr 4844 df-se 4845 df-we 4846 df-ord 4887 df-on 4888 df-lim 4889 df-suc 4890 df-xp 5011 df-rel 5012 df-cnv 5013 df-co 5014 df-dm 5015 df-rn 5016 df-res 5017 df-ima 5018 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 6256 df-ov 6298 df-oprab 6299 df-mpt2 6300 df-of 6535 df-ofr 6536 df-om 6696 df-1st 6795 df-2nd 6796 df-recs 7054 df-rdg 7088 df-1o 7142 df-2o 7143 df-oadd 7146 df-er 7323 df-map 7434 df-pm 7435 df-en 7529 df-dom 7530 df-sdom 7531 df-fin 7532 df-fi 7883 df-sup 7913 df-oi 7947 df-card 8332 df-cda 8560 df-pnf 9642 df-mnf 9643 df-xr 9644 df-ltxr 9645 df-le 9646 df-sub 9819 df-neg 9820 df-div 10219 df-nn 10549 df-2 10606 df-3 10607 df-n0 10808 df-z 10877 df-uz 11095 df-q 11195 df-rp 11233 df-xneg 11330 df-xadd 11331 df-xmul 11332 df-ioo 11545 df-ico 11547 df-icc 11548 df-fz 11685 df-fzo 11805 df-fl 11909 df-seq 12088 df-exp 12147 df-hash 12386 df-cj 12912 df-re 12913 df-im 12914 df-sqrt 13048 df-abs 13049 df-clim 13291 df-sum 13489 df-rest 14695 df-topgen 14716 df-psmet 18281 df-xmet 18282 df-met 18283 df-bl 18284 df-mopn 18285 df-top 19268 df-bases 19270 df-topon 19271 df-cmp 19755 df-ovol 21744 df-vol 21745 df-mbf 21896 df-itg1 21897 df-itg2 21898 df-ibl 21899 df-0p 21945

This theorem is referenced by: ftc1anclem5 30012 ftc1anclem6 30013

W3C validator