iblsplit - Mathbox for Glauco Siliprandi

	Mathbox for Glauco Siliprandi	< Previous Next > Nearby theorems
Mirrors > Home > MPE Home > Th. List > Mathboxes > iblsplit		Structured version Unicode version

Theorem iblsplit 31947

Description: The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019.)

**Hypotheses**
Ref	Expression
iblsplit.1
iblsplit.2
iblsplit.3	$/\$
iblsplit.4
iblsplit.5

**Assertion**
Ref	Expression
iblsplit

Distinct variable groups:

Allowed substitution hint:

(

)

Proof of Theorem iblsplit Dummy variables

are mutually distinct and distinct from all other variables.

Step	Hyp	Ref	Expression
1		iblsplit.3	. . . 4 $/\$
2		eqid 2457	. . . 4
3	1, 2	fmptd 6056	. . 3
4		ssun1 3663	. . . . . 6
5		iblsplit.2	. . . . . 6
6	4, 5	syl5sseqr 3548	. . . . 5
7	6	resmptd 5335	. . . 4
8		iblsplit.4	. . . . . 6
9		eqidd 2458	. . . . . . 7 $/\$ $/\$
10		eqidd 2458	. . . . . . 7 $/\$
11	6	sseld 3498	. . . . . . . . 9
12	11	imdistani 690	. . . . . . . 8 $/\$ $/\$
13	12, 1	syl 16	. . . . . . 7 $/\$
14	9, 10, 13	isibl2 22299	. . . . . 6 MblFn $/\$ $/\$
15	8, 14	mpbid 210	. . . . 5 MblFn $/\$ $/\$
16	15	simpld 459	. . . 4 MblFn
17	7, 16	eqeltrd 2545	. . 3 MblFn
18		ssun2 3664	. . . . . 6
19	18, 5	syl5sseqr 3548	. . . . 5
20	19	resmptd 5335	. . . 4
21		iblsplit.5	. . . . . 6
22		eqidd 2458	. . . . . . 7 $/\$ $/\$
23		eqidd 2458	. . . . . . 7 $/\$
24	19	sseld 3498	. . . . . . . . 9
25	24	imdistani 690	. . . . . . . 8 $/\$ $/\$
26	25, 1	syl 16	. . . . . . 7 $/\$
27	22, 23, 26	isibl2 22299	. . . . . 6 MblFn $/\$ $/\$
28	21, 27	mpbid 210	. . . . 5 MblFn $/\$ $/\$
29	28	simpld 459	. . . 4 MblFn
30	20, 29	eqeltrd 2545	. . 3 MblFn
31	5	eqcomd 2465	. . 3
32	3, 17, 30, 31	mbfres2cn 31939	. 2 MblFn
33	16, 13	mbfdm2 22171	. . . . . 6
34	33	adantr 465	. . . . 5 $/\$
35	29, 26	mbfdm2 22171	. . . . . 6
36	35	adantr 465	. . . . 5 $/\$
37		iblsplit.1	. . . . . 6
38	37	adantr 465	. . . . 5 $/\$
39	5	adantr 465	. . . . 5 $/\$
40	1	adantlr 714	. . . . . . . . . . 11 $/\$ $/\$
41		ax-icn 9568	. . . . . . . . . . . . . 14
42	41	a1i 11	. . . . . . . . . . . . 13
43		elfznn0 11797	. . . . . . . . . . . . 13
44	42, 43	expcld 12313	. . . . . . . . . . . 12
45	44	ad2antlr 726	. . . . . . . . . . 11 $/\$ $/\$
46	41	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
47		ine0 10013	. . . . . . . . . . . . 13
48	47	a1i 11	. . . . . . . . . . . 12 $/\$ $/\$
49		elfzelz 11713	. . . . . . . . . . . . 13
50	49	ad2antlr 726	. . . . . . . . . . . 12 $/\$ $/\$
51	46, 48, 50	expne0d 12319	. . . . . . . . . . 11 $/\$ $/\$
52	40, 45, 51	divcld 10341	. . . . . . . . . 10 $/\$ $/\$
53	52	recld 13039	. . . . . . . . 9 $/\$ $/\$
54	53	rexrd 9660	. . . . . . . 8 $/\$ $/\$
55	54	adantr 465	. . . . . . 7 $/\$ $/\$ $/\$
56		simpr 461	. . . . . . 7 $/\$ $/\$ $/\$
57		pnfge 11364	. . . . . . . 8
58	55, 57	syl 16	. . . . . . 7 $/\$ $/\$ $/\$
59		0xr 9657	. . . . . . . 8
60		pnfxr 11346	. . . . . . . 8
61		elicc1 11598	. . . . . . . 8 $/\$ $/\$ $/\$
62	59, 60, 61	mp2an 672	. . . . . . 7 $/\$ $/\$
63	55, 56, 58, 62	syl3anbrc 1180	. . . . . 6 $/\$ $/\$ $/\$
64		0e0iccpnf 11656	. . . . . . 7
65	64	a1i 11	. . . . . 6 $/\$ $/\$ $/\$
66	63, 65	ifclda 3976	. . . . 5 $/\$ $/\$
67		eqid 2457	. . . . 5
68		eqid 2457	. . . . 5
69		ifan 3990	. . . . . 6 $/\$
70	69	mpteq2i 4540	. . . . 5 $/\$
71		ifan 3990	. . . . . . . . . 10 $/\$
72	71	eqcomi 2470	. . . . . . . . 9 $/\$
73	72	mpteq2i 4540	. . . . . . . 8 $/\$
74	73	a1i 11	. . . . . . 7 $/\$ $/\$
75	74	fveq2d 5876	. . . . . 6 $/\$ $/\$
76		eqidd 2458	. . . . . . . . . 10 $/\$ $/\$
77		eqidd 2458	. . . . . . . . . 10 $/\$
78	76, 77, 13	isibl2 22299	. . . . . . . . 9 MblFn $/\$ $/\$
79	8, 78	mpbid 210	. . . . . . . 8 MblFn $/\$ $/\$
80	79	simprd 463	. . . . . . 7 $/\$
81	80	r19.21bi 2826	. . . . . 6 $/\$ $/\$
82	75, 81	eqeltrd 2545	. . . . 5 $/\$
83		ifan 3990	. . . . . . . . 9 $/\$
84	83	eqcomi 2470	. . . . . . . 8 $/\$
85	84	mpteq2i 4540	. . . . . . 7 $/\$
86	85	fveq2i 5875	. . . . . 6 $/\$
87		eqidd 2458	. . . . . . . . . 10 $/\$ $/\$
88		eqidd 2458	. . . . . . . . . 10 $/\$
89	87, 88, 26	isibl2 22299	. . . . . . . . 9 MblFn $/\$ $/\$
90	21, 89	mpbid 210	. . . . . . . 8 MblFn $/\$ $/\$
91	90	simprd 463	. . . . . . 7 $/\$
92	91	r19.21bi 2826	. . . . . 6 $/\$ $/\$
93	86, 92	syl5eqel 2549	. . . . 5 $/\$
94	34, 36, 38, 39, 66, 67, 68, 70, 82, 93	itg2split 22282	. . . 4 $/\$ $/\$
95	82, 93	readdcld 9640	. . . 4 $/\$
96	94, 95	eqeltrd 2545	. . 3 $/\$ $/\$
97	96	ralrimiva 2871	. 2 $/\$
98		eqidd 2458	. . 3 $/\$ $/\$
99		eqidd 2458	. . 3 $/\$
100	98, 99, 1	isibl2 22299	. 2 MblFn $/\$ $/\$
101	32, 97, 100	mpbir2and 922	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

wb 184 $/\$ wa 369 $/\$ w3a 973

wceq 1395

wcel 1819

wne 2652

wral 2807

cun 3469

cin 3470

cif 3944 class class class wbr 4456

cmpt 4515

cdm 5008

cres 5010

cfv 5594 (class class class)co 6296

cc 9507

cr 9508

cc0 9509

ci 9511

caddc 9512

cpnf 9642

cxr 9644

cle 9646

cdiv 10227

c3 10607

cz 10885

cicc 11557

cfz 11697

cexp 12169

cre 12942

covol 22000

cvol 22001 MblFncmbf 22149

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

This theorem is referenced by: iblsplitf 31951

W3C validator