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 31607

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	. . . . . 6 $/\$
2	1	ralrimiva 2881	. . . . 5
3		eqid 2467	. . . . . 6
4	3	fmpt 6053	. . . . 5
5	2, 4	sylib 196	. . . 4
6		ssun1 3672	. . . . . . . 8
7	6	a1i 11	. . . . . . 7
8		iblsplit.2	. . . . . . 7
9	7, 8	sseqtr4d 3546	. . . . . 6
10		resmpt 5329	. . . . . 6
11	9, 10	syl 16	. . . . 5
12		iblsplit.4	. . . . . . 7
13		eqidd 2468	. . . . . . . 8 $/\$ $/\$
14		eqidd 2468	. . . . . . . 8 $/\$
15	9	sseld 3508	. . . . . . . . . 10
16	15	imdistani 690	. . . . . . . . 9 $/\$ $/\$
17	16, 1	syl 16	. . . . . . . 8 $/\$
18	13, 14, 17	isibl2 22041	. . . . . . 7 MblFn $/\$ $/\$
19	12, 18	mpbid 210	. . . . . 6 MblFn $/\$ $/\$
20	19	simpld 459	. . . . 5 MblFn
21	11, 20	eqeltrd 2555	. . . 4 MblFn
22		ssun2 3673	. . . . . . . 8
23	22	a1i 11	. . . . . . 7
24	23, 8	sseqtr4d 3546	. . . . . 6
25		resmpt 5329	. . . . . 6
26	24, 25	syl 16	. . . . 5
27		iblsplit.5	. . . . . . 7
28		eqidd 2468	. . . . . . . 8 $/\$ $/\$
29		eqidd 2468	. . . . . . . 8 $/\$
30	24	sseld 3508	. . . . . . . . . 10
31	30	imdistani 690	. . . . . . . . 9 $/\$ $/\$
32	31, 1	syl 16	. . . . . . . 8 $/\$
33	28, 29, 32	isibl2 22041	. . . . . . 7 MblFn $/\$ $/\$
34	27, 33	mpbid 210	. . . . . 6 MblFn $/\$ $/\$
35	34	simpld 459	. . . . 5 MblFn
36	26, 35	eqeltrd 2555	. . . 4 MblFn
37	8	eqcomd 2475	. . . 4
38	5, 21, 36, 37	mbfres2cn 31599	. . 3 MblFn
39	20, 17	mbfdm2 21913	. . . . . . 7
40	39	adantr 465	. . . . . 6 $/\$
41	35, 32	mbfdm2 21913	. . . . . . 7
42	41	adantr 465	. . . . . 6 $/\$
43		iblsplit.1	. . . . . . 7
44	43	adantr 465	. . . . . 6 $/\$
45	8	adantr 465	. . . . . 6 $/\$
46	1	adantlr 714	. . . . . . . . . . . . 13 $/\$ $/\$
47		ax-icn 9563	. . . . . . . . . . . . . . . 16
48	47	a1i 11	. . . . . . . . . . . . . . 15
49		elfznn0 11782	. . . . . . . . . . . . . . 15
50	48, 49	expcld 12290	. . . . . . . . . . . . . 14
51	50	ad2antlr 726	. . . . . . . . . . . . 13 $/\$ $/\$
52	47	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
53		ine0 10004	. . . . . . . . . . . . . . 15
54	53	a1i 11	. . . . . . . . . . . . . 14 $/\$ $/\$
55	49	nn0zd 10976	. . . . . . . . . . . . . . 15
56	55	ad2antlr 726	. . . . . . . . . . . . . 14 $/\$ $/\$
57	52, 54, 56	expne0d 12296	. . . . . . . . . . . . 13 $/\$ $/\$
58	46, 51, 57	divcld 10332	. . . . . . . . . . . 12 $/\$ $/\$
59	58	recld 13007	. . . . . . . . . . 11 $/\$ $/\$
60	59	rexrd 9655	. . . . . . . . . 10 $/\$ $/\$
61	60	adantr 465	. . . . . . . . 9 $/\$ $/\$ $/\$
62		simpr 461	. . . . . . . . 9 $/\$ $/\$ $/\$
63		pnfge 11351	. . . . . . . . . 10
64	61, 63	syl 16	. . . . . . . . 9 $/\$ $/\$ $/\$
65	61, 62, 64	3jca 1176	. . . . . . . 8 $/\$ $/\$ $/\$ $/\$ $/\$
66		0xr 9652	. . . . . . . . . 10
67		pnfxr 11333	. . . . . . . . . 10
68	66, 67	pm3.2i 455	. . . . . . . . 9 $/\$
69		elicc1 11585	. . . . . . . . 9 $/\$ $/\$ $/\$
70	68, 69	ax-mp 5	. . . . . . . 8 $/\$ $/\$
71	65, 70	sylibr 212	. . . . . . 7 $/\$ $/\$ $/\$
72		0le0 10637	. . . . . . . . . 10
73		pnfge 11351	. . . . . . . . . . 11
74	66, 73	ax-mp 5	. . . . . . . . . 10
75	66, 72, 74	3pm3.2i 1174	. . . . . . . . 9 $/\$ $/\$
76		elicc1 11585	. . . . . . . . . 10 $/\$ $/\$ $/\$
77	68, 76	ax-mp 5	. . . . . . . . 9 $/\$ $/\$
78	75, 77	mpbir 209	. . . . . . . 8
79	78	a1i 11	. . . . . . 7 $/\$ $/\$ $/\$
80	71, 79	ifclda 3977	. . . . . 6 $/\$ $/\$
81		eqid 2467	. . . . . 6
82		eqid 2467	. . . . . 6
83		ifan 3991	. . . . . . 7 $/\$
84	83	mpteq2i 4536	. . . . . 6 $/\$
85		ifan 3991	. . . . . . . . . . 11 $/\$
86	85	eqcomi 2480	. . . . . . . . . 10 $/\$
87	86	mpteq2i 4536	. . . . . . . . 9 $/\$
88	87	a1i 11	. . . . . . . 8 $/\$ $/\$
89	88	fveq2d 5876	. . . . . . 7 $/\$ $/\$
90		eqidd 2468	. . . . . . . . . . . 12 $/\$ $/\$
91		eqidd 2468	. . . . . . . . . . . 12 $/\$
92	90, 91, 17	isibl2 22041	. . . . . . . . . . 11 MblFn $/\$ $/\$
93	12, 92	mpbid 210	. . . . . . . . . 10 MblFn $/\$ $/\$
94	93	simprd 463	. . . . . . . . 9 $/\$
95		rsp 2833	. . . . . . . . 9 $/\$ $/\$
96	94, 95	syl 16	. . . . . . . 8 $/\$
97	96	imp 429	. . . . . . 7 $/\$ $/\$
98	89, 97	eqeltrd 2555	. . . . . 6 $/\$
99		ifan 3991	. . . . . . . . . . 11 $/\$
100	99	eqcomi 2480	. . . . . . . . . 10 $/\$
101	100	mpteq2i 4536	. . . . . . . . 9 $/\$
102	101	fveq2i 5875	. . . . . . . 8 $/\$
103	102	a1i 11	. . . . . . 7 $/\$ $/\$
104		eqidd 2468	. . . . . . . . . . . 12 $/\$ $/\$
105		eqidd 2468	. . . . . . . . . . . 12 $/\$
106	104, 105, 32	isibl2 22041	. . . . . . . . . . 11 MblFn $/\$ $/\$
107	27, 106	mpbid 210	. . . . . . . . . 10 MblFn $/\$ $/\$
108	107	simprd 463	. . . . . . . . 9 $/\$
109		rsp 2833	. . . . . . . . 9 $/\$ $/\$
110	108, 109	syl 16	. . . . . . . 8 $/\$
111	110	imp 429	. . . . . . 7 $/\$ $/\$
112	103, 111	eqeltrd 2555	. . . . . 6 $/\$
113	40, 42, 44, 45, 80, 81, 82, 84, 98, 112	itg2split 22024	. . . . 5 $/\$ $/\$
114	98, 112	readdcld 9635	. . . . 5 $/\$
115	113, 114	eqeltrd 2555	. . . 4 $/\$ $/\$
116	115	ralrimiva 2881	. . 3 $/\$
117	38, 116	jca 532	. 2 MblFn $/\$ $/\$
118		eqidd 2468	. . 3 $/\$ $/\$
119		eqidd 2468	. . 3 $/\$
120	118, 119, 1	isibl2 22041	. 2 MblFn $/\$ $/\$
121	117, 120	mpbird 232	1

Colors of variables: wff setvar class

Syntax hints:

wn 3

wi 4

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

wceq 1379

wcel 1767

wne 2662

wral 2817

cun 3479

cin 3480

wss 3481

cif 3945 class class class wbr 4453

cmpt 4511

cdm 5005

cres 5007

wf 5590

cfv 5594 (class class class)co 6295

cc 9502

cr 9503

cc0 9504

ci 9506

caddc 9507

cpnf 9637

cxr 9639

cle 9641

cdiv 10218

c3 10598

cz 10876

cicc 11544

cfz 11684

cexp 12146

cre 12910

covol 21742

cvol 21743 MblFncmbf 21891

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

This theorem is referenced by: iblsplitf 31611 fourierdlem93 31823

W3C validator