ftc1anclem4 - Mathbox for Brendan Leahy

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

Theorem ftc1anclem4 32013

Description: Lemma for ftc1anc 32018. (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 6018	. . . . . . . . . 10 $/\$
2	1	recnd 9666	. . . . . . . . 9 $/\$
3		i1ff 22627	. . . . . . . . . . 11
4	3	ffvelrnda 6020	. . . . . . . . . 10 $/\$
5	4	recnd 9666	. . . . . . . . 9 $/\$
6		subcl 9871	. . . . . . . . 9 $/\$
7	2, 5, 6	syl2anr 481	. . . . . . . 8 $/\$ $/\$ $/\$
8	7	anandirs 839	. . . . . . 7 $/\$ $/\$
9	8	abscld 13491	. . . . . 6 $/\$ $/\$
10	9	rexrd 9687	. . . . 5 $/\$ $/\$
11	8	absge0d 13499	. . . . 5 $/\$ $/\$
12		elxrge0 11738	. . . . 5 $/\$
13	10, 11, 12	sylanbrc 669	. . . 4 $/\$ $/\$
14		eqid 2450	. . . 4
15	13, 14	fmptd 6044	. . 3 $/\$
16	15	3adant2 1026	. 2 $/\$ $/\$
17		reex 9627	. . . . . . 7
18	17	a1i 11	. . . . . 6 $/\$ $/\$
19		fvex 5873	. . . . . . 7
20	19	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
21		fvex 5873	. . . . . . 7
22	21	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
23		eqidd 2451	. . . . . 6 $/\$ $/\$
24		eqidd 2451	. . . . . 6 $/\$ $/\$
25	18, 20, 22, 23, 24	offval2 6545	. . . . 5 $/\$ $/\$
26	25	fveq2d 5867	. . . 4 $/\$ $/\$
27		id 22	. . . . . . . . . 10
28	27	feqmptd 5916	. . . . . . . . 9
29		absf 13393	. . . . . . . . . . 11
30	29	a1i 11	. . . . . . . . . 10
31	30	feqmptd 5916	. . . . . . . . 9
32		fveq2 5863	. . . . . . . . 9
33	2, 28, 31, 32	fmptco 6054	. . . . . . . 8
34	33	adantl 468	. . . . . . 7 $/\$
35		iblmbf 22718	. . . . . . . . 9 MblFn
36		ftc1anclem1 32010	. . . . . . . . 9 $/\$ MblFn MblFn
37	35, 36	sylan2 477	. . . . . . . 8 $/\$ MblFn
38	37	ancoms 455	. . . . . . 7 $/\$ MblFn
39	34, 38	eqeltrrd 2529	. . . . . 6 $/\$ MblFn
40	39	3adant1 1025	. . . . 5 $/\$ $/\$ MblFn
41	2	abscld 13491	. . . . . . . 8 $/\$
42	2	absge0d 13499	. . . . . . . 8 $/\$
43		elrege0 11735	. . . . . . . 8 $/\$
44	41, 42, 43	sylanbrc 669	. . . . . . 7 $/\$
45		eqid 2450	. . . . . . 7
46	44, 45	fmptd 6044	. . . . . 6
47	46	3ad2ant3 1030	. . . . 5 $/\$ $/\$
48		iftrue 3886	. . . . . . . . 9
49	48	mpteq2ia 4484	. . . . . . . 8
50	49	fveq2i 5866	. . . . . . 7
51	1	adantll 719	. . . . . . . . . 10 $/\$ $/\$
52		simpr 463	. . . . . . . . . . . 12 $/\$
53	52	feqmptd 5916	. . . . . . . . . . 11 $/\$
54		simpl 459	. . . . . . . . . . 11 $/\$
55	53, 54	eqeltrrd 2529	. . . . . . . . . 10 $/\$
56	51, 55, 39	iblabsnc 31999	. . . . . . . . 9 $/\$
57	41	adantll 719	. . . . . . . . . 10 $/\$ $/\$
58	42	adantll 719	. . . . . . . . . 10 $/\$ $/\$
59	57, 58	iblpos 22743	. . . . . . . . 9 $/\$ MblFn $/\$
60	56, 59	mpbid 214	. . . . . . . 8 $/\$ MblFn $/\$
61	60	simprd 465	. . . . . . 7 $/\$
62	50, 61	syl5eqelr 2533	. . . . . 6 $/\$
63	62	3adant1 1025	. . . . 5 $/\$ $/\$
64	5	abscld 13491	. . . . . . . 8 $/\$
65	5	absge0d 13499	. . . . . . . 8 $/\$
66		elrege0 11735	. . . . . . . 8 $/\$
67	64, 65, 66	sylanbrc 669	. . . . . . 7 $/\$
68		eqid 2450	. . . . . . 7
69	67, 68	fmptd 6044	. . . . . 6
70	69	3ad2ant1 1028	. . . . 5 $/\$ $/\$
71		iftrue 3886	. . . . . . . . 9
72	71	mpteq2ia 4484	. . . . . . . 8
73	72	fveq2i 5866	. . . . . . 7
74	3	feqmptd 5916	. . . . . . . . . . 11
75		i1fibl 22758	. . . . . . . . . . 11
76	74, 75	eqeltrrd 2529	. . . . . . . . . 10
77	29	a1i 11	. . . . . . . . . . . . 13
78	77	feqmptd 5916	. . . . . . . . . . . 12
79		fveq2 5863	. . . . . . . . . . . 12
80	5, 74, 78, 79	fmptco 6054	. . . . . . . . . . 11
81		i1fmbf 22626	. . . . . . . . . . . 12 MblFn
82		ftc1anclem1 32010	. . . . . . . . . . . 12 $/\$ MblFn MblFn
83	3, 81, 82	syl2anc 666	. . . . . . . . . . 11 MblFn
84	80, 83	eqeltrrd 2529	. . . . . . . . . 10 MblFn
85	4, 76, 84	iblabsnc 31999	. . . . . . . . 9
86	64, 65	iblpos 22743	. . . . . . . . 9 MblFn $/\$
87	85, 86	mpbid 214	. . . . . . . 8 MblFn $/\$
88	87	simprd 465	. . . . . . 7
89	73, 88	syl5eqelr 2533	. . . . . 6
90	89	3ad2ant1 1028	. . . . 5 $/\$ $/\$
91	40, 47, 63, 70, 90	itg2addnc 31989	. . . 4 $/\$ $/\$
92	26, 91	eqtr3d 2486	. . 3 $/\$ $/\$
93	63, 90	readdcld 9667	. . 3 $/\$ $/\$
94	92, 93	eqeltrd 2528	. 2 $/\$ $/\$
95		readdcl 9619	. . . . . . . . 9 $/\$
96	41, 64, 95	syl2anr 481	. . . . . . . 8 $/\$ $/\$ $/\$
97	96	anandirs 839	. . . . . . 7 $/\$ $/\$
98	97	rexrd 9687	. . . . . 6 $/\$ $/\$
99	41	adantll 719	. . . . . . 7 $/\$ $/\$
100	64	adantlr 720	. . . . . . 7 $/\$ $/\$
101	42	adantll 719	. . . . . . 7 $/\$ $/\$
102	65	adantlr 720	. . . . . . 7 $/\$ $/\$
103	99, 100, 101, 102	addge0d 10186	. . . . . 6 $/\$ $/\$
104		elxrge0 11738	. . . . . 6 $/\$
105	98, 103, 104	sylanbrc 669	. . . . 5 $/\$ $/\$
106		eqid 2450	. . . . 5
107	105, 106	fmptd 6044	. . . 4 $/\$
108	107	3adant2 1026	. . 3 $/\$ $/\$
109		abs2dif2 13389	. . . . . . . 8 $/\$
110	2, 5, 109	syl2anr 481	. . . . . . 7 $/\$ $/\$ $/\$
111	110	anandirs 839	. . . . . 6 $/\$ $/\$
112	111	ralrimiva 2801	. . . . 5 $/\$
113	17	a1i 11	. . . . . 6 $/\$
114		eqidd 2451	. . . . . 6 $/\$
115		eqidd 2451	. . . . . 6 $/\$
116	113, 9, 97, 114, 115	ofrfval2 6546	. . . . 5 $/\$
117	112, 116	mpbird 236	. . . 4 $/\$
118	117	3adant2 1026	. . 3 $/\$ $/\$
119		itg2le 22690	. . 3 $/\$ $/\$
120	16, 108, 118, 119	syl3anc 1267	. 2 $/\$ $/\$
121		itg2lecl 22689	. 2 $/\$ $/\$
122	16, 94, 120, 121	syl3anc 1267	1 $/\$ $/\$

Colors of variables: wff setvar class

Syntax hints:

wi 4 $/\$ wa 371 $/\$ w3a 984

wceq 1443

wcel 1886

wral 2736

cvv 3044

cif 3880 class class class wbr 4401

cmpt 4460

cdm 4833

ccom 4837

wf 5577

cfv 5581 (class class class)co 6288

cof 6526

cofr 6527

cc 9534

cr 9535

cc0 9536

caddc 9539

cpnf 9669

cxr 9671

cle 9673

cmin 9857

cico 11634

cicc 11635

cabs 13290 MblFncmbf 22565

citg1 22566

citg2 22567

cibl 22568

This theorem was proved from axioms: ax-mp 5 ax-1 6 ax-2 7 ax-3 8 ax-gen 1668 ax-4 1681 ax-5 1757 ax-6 1804 ax-7 1850 ax-8 1888 ax-9 1895 ax-10 1914 ax-11 1919 ax-12 1932 ax-13 2090 ax-ext 2430 ax-rep 4514 ax-sep 4524 ax-nul 4533 ax-pow 4580 ax-pr 4638 ax-un 6580 ax-inf2 8143 ax-cnex 9592 ax-resscn 9593 ax-1cn 9594 ax-icn 9595 ax-addcl 9596 ax-addrcl 9597 ax-mulcl 9598 ax-mulrcl 9599 ax-mulcom 9600 ax-addass 9601 ax-mulass 9602 ax-distr 9603 ax-i2m1 9604 ax-1ne0 9605 ax-1rid 9606 ax-rnegex 9607 ax-rrecex 9608 ax-cnre 9609 ax-pre-lttri 9610 ax-pre-lttrn 9611 ax-pre-ltadd 9612 ax-pre-mulgt0 9613 ax-pre-sup 9614 ax-addf 9615

This theorem depends on definitions: df-bi 189 df-or 372 df-an 373 df-3or 985 df-3an 986 df-tru 1446 df-fal 1449 df-ex 1663 df-nf 1667 df-sb 1797 df-eu 2302 df-mo 2303 df-clab 2437 df-cleq 2443 df-clel 2446 df-nfc 2580 df-ne 2623 df-nel 2624 df-ral 2741 df-rex 2742 df-reu 2743 df-rmo 2744 df-rab 2745 df-v 3046 df-sbc 3267 df-csb 3363 df-dif 3406 df-un 3408 df-in 3410 df-ss 3417 df-pss 3419 df-nul 3731 df-if 3881 df-pw 3952 df-sn 3968 df-pr 3970 df-tp 3972 df-op 3974 df-uni 4198 df-int 4234 df-iun 4279 df-disj 4373 df-br 4402 df-opab 4461 df-mpt 4462 df-tr 4497 df-eprel 4744 df-id 4748 df-po 4754 df-so 4755 df-fr 4792 df-se 4793 df-we 4794 df-xp 4839 df-rel 4840 df-cnv 4841 df-co 4842 df-dm 4843 df-rn 4844 df-res 4845 df-ima 4846 df-pred 5379 df-ord 5425 df-on 5426 df-lim 5427 df-suc 5428 df-iota 5545 df-fun 5583 df-fn 5584 df-f 5585 df-f1 5586 df-fo 5587 df-f1o 5588 df-fv 5589 df-isom 5590 df-riota 6250 df-ov 6291 df-oprab 6292 df-mpt2 6293 df-of 6528 df-ofr 6529 df-om 6690 df-1st 6790 df-2nd 6791 df-wrecs 7025 df-recs 7087 df-rdg 7125 df-1o 7179 df-2o 7180 df-oadd 7183 df-er 7360 df-map 7471 df-pm 7472 df-en 7567 df-dom 7568 df-sdom 7569 df-fin 7570 df-fi 7922 df-sup 7953 df-inf 7954 df-oi 8022 df-card 8370 df-cda 8595 df-pnf 9674 df-mnf 9675 df-xr 9676 df-ltxr 9677 df-le 9678 df-sub 9859 df-neg 9860 df-div 10267 df-nn 10607 df-2 10665 df-3 10666 df-n0 10867 df-z 10935 df-uz 11157 df-q 11262 df-rp 11300 df-xneg 11406 df-xadd 11407 df-xmul 11408 df-ioo 11636 df-ico 11638 df-icc 11639 df-fz 11782 df-fzo 11913 df-fl 12025 df-seq 12211 df-exp 12270 df-hash 12513 df-cj 13155 df-re 13156 df-im 13157 df-sqrt 13291 df-abs 13292 df-clim 13545 df-sum 13746 df-rest 15314 df-topgen 15335 df-psmet 18955 df-xmet 18956 df-met 18957 df-bl 18958 df-mopn 18959 df-top 19914 df-bases 19915 df-topon 19916 df-cmp 20395 df-ovol 22409 df-vol 22411 df-mbf 22570 df-itg1 22571 df-itg2 22572 df-ibl 22573 df-0p 22621

This theorem is referenced by: ftc1anclem5 32014 ftc1anclem6 32015

W3C validator