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 28395

Description: Lemma for ftc1anc 28400. (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 5838	. . . . . . . . . 10 $/\$
2	1	recnd 9408	. . . . . . . . 9 $/\$
3		i1ff 21113	. . . . . . . . . . 11
4	3	ffvelrnda 5840	. . . . . . . . . 10 $/\$
5	4	recnd 9408	. . . . . . . . 9 $/\$
6		subcl 9605	. . . . . . . . 9 $/\$
7	2, 5, 6	syl2anr 475	. . . . . . . 8 $/\$ $/\$ $/\$
8	7	anandirs 822	. . . . . . 7 $/\$ $/\$
9	8	abscld 12918	. . . . . 6 $/\$ $/\$
10	9	rexrd 9429	. . . . 5 $/\$ $/\$
11	8	absge0d 12926	. . . . 5 $/\$ $/\$
12		elxrge0 11390	. . . . 5 $/\$
13	10, 11, 12	sylanbrc 659	. . . 4 $/\$ $/\$
14		eqid 2441	. . . 4
15	13, 14	fmptd 5864	. . 3 $/\$
16	15	3adant2 1002	. 2 $/\$ $/\$
17		reex 9369	. . . . . . 7
18	17	a1i 11	. . . . . 6 $/\$ $/\$
19		fvex 5698	. . . . . . 7
20	19	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
21		fvex 5698	. . . . . . 7
22	21	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
23		eqidd 2442	. . . . . 6 $/\$ $/\$
24		eqidd 2442	. . . . . 6 $/\$ $/\$
25	18, 20, 22, 23, 24	offval2 6335	. . . . 5 $/\$ $/\$
26	25	fveq2d 5692	. . . 4 $/\$ $/\$
27		id 22	. . . . . . . . . 10
28	27	feqmptd 5741	. . . . . . . . 9
29		absf 12821	. . . . . . . . . . 11
30	29	a1i 11	. . . . . . . . . 10
31	30	feqmptd 5741	. . . . . . . . 9
32		fveq2 5688	. . . . . . . . 9
33	2, 28, 31, 32	fmptco 5873	. . . . . . . 8
34	33	adantl 463	. . . . . . 7 $/\$
35		iblmbf 21204	. . . . . . . . 9 MblFn
36		ftc1anclem1 28392	. . . . . . . . 9 $/\$ MblFn MblFn
37	35, 36	sylan2 471	. . . . . . . 8 $/\$ MblFn
38	37	ancoms 450	. . . . . . 7 $/\$ MblFn
39	34, 38	eqeltrrd 2516	. . . . . 6 $/\$ MblFn
40	39	3adant1 1001	. . . . 5 $/\$ $/\$ MblFn
41	2	abscld 12918	. . . . . . . 8 $/\$
42	2	absge0d 12926	. . . . . . . 8 $/\$
43		elrege0 11388	. . . . . . . 8 $/\$
44	41, 42, 43	sylanbrc 659	. . . . . . 7 $/\$
45		eqid 2441	. . . . . . 7
46	44, 45	fmptd 5864	. . . . . 6
47	46	3ad2ant3 1006	. . . . 5 $/\$ $/\$
48		iftrue 3794	. . . . . . . . 9
49	48	mpteq2ia 4371	. . . . . . . 8
50	49	fveq2i 5691	. . . . . . 7
51	1	adantll 708	. . . . . . . . . 10 $/\$ $/\$
52		simpr 458	. . . . . . . . . . . 12 $/\$
53	52	feqmptd 5741	. . . . . . . . . . 11 $/\$
54		simpl 454	. . . . . . . . . . 11 $/\$
55	53, 54	eqeltrrd 2516	. . . . . . . . . 10 $/\$
56	51, 55, 39	iblabsnc 28381	. . . . . . . . 9 $/\$
57	41	adantll 708	. . . . . . . . . 10 $/\$ $/\$
58	42	adantll 708	. . . . . . . . . 10 $/\$ $/\$
59	57, 58	iblpos 21229	. . . . . . . . 9 $/\$ MblFn $/\$
60	56, 59	mpbid 210	. . . . . . . 8 $/\$ MblFn $/\$
61	60	simprd 460	. . . . . . 7 $/\$
62	50, 61	syl5eqelr 2526	. . . . . 6 $/\$
63	62	3adant1 1001	. . . . 5 $/\$ $/\$
64	5	abscld 12918	. . . . . . . 8 $/\$
65	5	absge0d 12926	. . . . . . . 8 $/\$
66		elrege0 11388	. . . . . . . 8 $/\$
67	64, 65, 66	sylanbrc 659	. . . . . . 7 $/\$
68		eqid 2441	. . . . . . 7
69	67, 68	fmptd 5864	. . . . . 6
70	69	3ad2ant1 1004	. . . . 5 $/\$ $/\$
71		iftrue 3794	. . . . . . . . 9
72	71	mpteq2ia 4371	. . . . . . . 8
73	72	fveq2i 5691	. . . . . . 7
74	3	feqmptd 5741	. . . . . . . . . . 11
75		i1fibl 21244	. . . . . . . . . . 11
76	74, 75	eqeltrrd 2516	. . . . . . . . . 10
77	29	a1i 11	. . . . . . . . . . . . 13
78	77	feqmptd 5741	. . . . . . . . . . . 12
79		fveq2 5688	. . . . . . . . . . . 12
80	5, 74, 78, 79	fmptco 5873	. . . . . . . . . . 11
81		i1fmbf 21112	. . . . . . . . . . . 12 MblFn
82		ftc1anclem1 28392	. . . . . . . . . . . 12 $/\$ MblFn MblFn
83	3, 81, 82	syl2anc 656	. . . . . . . . . . 11 MblFn
84	80, 83	eqeltrrd 2516	. . . . . . . . . 10 MblFn
85	4, 76, 84	iblabsnc 28381	. . . . . . . . 9
86	64, 65	iblpos 21229	. . . . . . . . 9 MblFn $/\$
87	85, 86	mpbid 210	. . . . . . . 8 MblFn $/\$
88	87	simprd 460	. . . . . . 7
89	73, 88	syl5eqelr 2526	. . . . . 6
90	89	3ad2ant1 1004	. . . . 5 $/\$ $/\$
91	40, 47, 63, 70, 90	itg2addnc 28371	. . . 4 $/\$ $/\$
92	26, 91	eqtr3d 2475	. . 3 $/\$ $/\$
93	63, 90	readdcld 9409	. . 3 $/\$ $/\$
94	92, 93	eqeltrd 2515	. 2 $/\$ $/\$
95		readdcl 9361	. . . . . . . . 9 $/\$
96	41, 64, 95	syl2anr 475	. . . . . . . 8 $/\$ $/\$ $/\$
97	96	anandirs 822	. . . . . . 7 $/\$ $/\$
98	97	rexrd 9429	. . . . . 6 $/\$ $/\$
99	41	adantll 708	. . . . . . 7 $/\$ $/\$
100	64	adantlr 709	. . . . . . 7 $/\$ $/\$
101	42	adantll 708	. . . . . . 7 $/\$ $/\$
102	65	adantlr 709	. . . . . . 7 $/\$ $/\$
103	99, 100, 101, 102	addge0d 9911	. . . . . 6 $/\$ $/\$
104		elxrge0 11390	. . . . . 6 $/\$
105	98, 103, 104	sylanbrc 659	. . . . 5 $/\$ $/\$
106		eqid 2441	. . . . 5
107	105, 106	fmptd 5864	. . . 4 $/\$
108	107	3adant2 1002	. . 3 $/\$ $/\$
109		abs2dif2 12817	. . . . . . . 8 $/\$
110	2, 5, 109	syl2anr 475	. . . . . . 7 $/\$ $/\$ $/\$
111	110	anandirs 822	. . . . . 6 $/\$ $/\$
112	111	ralrimiva 2797	. . . . 5 $/\$
113	17	a1i 11	. . . . . 6 $/\$
114		eqidd 2442	. . . . . 6 $/\$
115		eqidd 2442	. . . . . 6 $/\$
116	113, 9, 97, 114, 115	ofrfval2 6336	. . . . 5 $/\$
117	112, 116	mpbird 232	. . . 4 $/\$
118	117	3adant2 1002	. . 3 $/\$ $/\$
119		itg2le 21176	. . 3 $/\$ $/\$
120	16, 108, 118, 119	syl3anc 1213	. 2 $/\$ $/\$
121		itg2lecl 21175	. 2 $/\$ $/\$
122	16, 94, 120, 121	syl3anc 1213	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

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

wceq 1364

wcel 1761

wral 2713

cvv 2970

cif 3788 class class class wbr 4289

cmpt 4347

cdm 4836

ccom 4840

wf 5411

cfv 5415 (class class class)co 6090

cof 6317

cofr 6318

cc 9276

cr 9277

cc0 9278

caddc 9281

cpnf 9411

cxr 9413

cle 9415

cmin 9591

cico 11298

cicc 11299

cabs 12719 MblFncmbf 21053

citg1 21054

citg2 21055

cibl 21056

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1596 ax-4 1607 ax-5 1675 ax-6 1713 ax-7 1733 ax-8 1763 ax-9 1765 ax-10 1780 ax-11 1785 ax-12 1797 ax-13 1948 ax-ext 2422 ax-rep 4400 ax-sep 4410 ax-nul 4418 ax-pow 4467 ax-pr 4528 ax-un 6371 ax-inf2 7843 ax-cnex 9334 ax-resscn 9335 ax-1cn 9336 ax-icn 9337 ax-addcl 9338 ax-addrcl 9339 ax-mulcl 9340 ax-mulrcl 9341 ax-mulcom 9342 ax-addass 9343 ax-mulass 9344 ax-distr 9345 ax-i2m1 9346 ax-1ne0 9347 ax-1rid 9348 ax-rnegex 9349 ax-rrecex 9350 ax-cnre 9351 ax-pre-lttri 9352 ax-pre-lttrn 9353 ax-pre-ltadd 9354 ax-pre-mulgt0 9355 ax-pre-sup 9356 ax-addf 9357

This theorem depends on definitions: df-bi 185 df-or 370 df-an 371 df-3or 961 df-3an 962 df-tru 1367 df-fal 1370 df-ex 1592 df-nf 1595 df-sb 1706 df-eu 2261 df-mo 2262 df-clab 2428 df-cleq 2434 df-clel 2437 df-nfc 2566 df-ne 2606 df-nel 2607 df-ral 2718 df-rex 2719 df-reu 2720 df-rmo 2721 df-rab 2722 df-v 2972 df-sbc 3184 df-csb 3286 df-dif 3328 df-un 3330 df-in 3332 df-ss 3339 df-pss 3341 df-nul 3635 df-if 3789 df-pw 3859 df-sn 3875 df-pr 3877 df-tp 3879 df-op 3881 df-uni 4089 df-int 4126 df-iun 4170 df-disj 4260 df-br 4290 df-opab 4348 df-mpt 4349 df-tr 4383 df-eprel 4628 df-id 4632 df-po 4637 df-so 4638 df-fr 4675 df-se 4676 df-we 4677 df-ord 4718 df-on 4719 df-lim 4720 df-suc 4721 df-xp 4842 df-rel 4843 df-cnv 4844 df-co 4845 df-dm 4846 df-rn 4847 df-res 4848 df-ima 4849 df-iota 5378 df-fun 5417 df-fn 5418 df-f 5419 df-f1 5420 df-fo 5421 df-f1o 5422 df-fv 5423 df-isom 5424 df-riota 6049 df-ov 6093 df-oprab 6094 df-mpt2 6095 df-of 6319 df-ofr 6320 df-om 6476 df-1st 6576 df-2nd 6577 df-recs 6828 df-rdg 6862 df-1o 6916 df-2o 6917 df-oadd 6920 df-er 7097 df-map 7212 df-pm 7213 df-en 7307 df-dom 7308 df-sdom 7309 df-fin 7310 df-fi 7657 df-sup 7687 df-oi 7720 df-card 8105 df-cda 8333 df-pnf 9416 df-mnf 9417 df-xr 9418 df-ltxr 9419 df-le 9420 df-sub 9593 df-neg 9594 df-div 9990 df-nn 10319 df-2 10376 df-3 10377 df-n0 10576 df-z 10643 df-uz 10858 df-q 10950 df-rp 10988 df-xneg 11085 df-xadd 11086 df-xmul 11087 df-ioo 11300 df-ico 11302 df-icc 11303 df-fz 11434 df-fzo 11545 df-fl 11638 df-seq 11803 df-exp 11862 df-hash 12100 df-cj 12584 df-re 12585 df-im 12586 df-sqr 12720 df-abs 12721 df-clim 12962 df-sum 13160 df-rest 14357 df-topgen 14378 df-psmet 17768 df-xmet 17769 df-met 17770 df-bl 17771 df-mopn 17772 df-top 18462 df-bases 18464 df-topon 18465 df-cmp 18949 df-ovol 20907 df-vol 20908 df-mbf 21058 df-itg1 21059 df-itg2 21060 df-ibl 21061 df-0p 21107

This theorem is referenced by: ftc1anclem5 28396 ftc1anclem6 28397

W3C validator