Theorem iblsplit

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

	Ref	Expression
Hypotheses	iblsplit.1	$$⊢\phi \to {vol}^{*}\left(A\cap B\right)=0$$
	iblsplit.2	$$⊢\phi \to U=A\cup B$$
	iblsplit.3	$$⊢\left(\phi \wedge x\in U\right)\to C\in ℂ$$
	iblsplit.4	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
	iblsplit.5	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$
Assertion	iblsplit	$$⊢\phi \to \left(x\in U⟼C\right)\in {𝐿}^1$$

Proof

Step	Hyp	Ref	Expression
1		iblsplit.1	$$⊢\phi \to {vol}^{*}\left(A\cap B\right)=0$$
2		iblsplit.2	$$⊢\phi \to U=A\cup B$$
3		iblsplit.3	$$⊢\left(\phi \wedge x\in U\right)\to C\in ℂ$$
4		iblsplit.4	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
5		iblsplit.5	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$
6	3	fmpttd	$$⊢\phi \to \left(x\in U⟼C\right):U⟶ℂ$$
7		ssun1	$$⊢A\subseteq A\cup B$$
8	7 2	sseqtrrid	$$⊢\phi \to A\subseteq U$$
9	8	resmptd	$$⊢\phi \to {\left(x\in U⟼C\right)\upharpoonright }_A=\left(x\in A⟼C\right)$$
10		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^y}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^y}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^y}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^y}\right),0\right)\right)$$
11		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{C}{{\mathrm{i}}^y}\right)=\Re \left(\frac{C}{{\mathrm{i}}^y}\right)$$
12	8	sseld	$$⊢\phi \to \left(x\in A\to x\in U\right)$$
13	12	imdistani	$$⊢\left(\phi \wedge x\in A\right)\to \left(\phi \wedge x\in U\right)$$
14	13 3	syl	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
15	10 11 14	isibl2	$$⊢\phi \to \left(\left(x\in A⟼C\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼C\right)\in MblFn\wedge \forall y\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^y}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^y}\right),0\right)\right)\right)\in ℝ\right)\right)$$
16	4 15	mpbid	$$⊢\phi \to \left(\left(x\in A⟼C\right)\in MblFn\wedge \forall y\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^y}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^y}\right),0\right)\right)\right)\in ℝ\right)$$
17	16	simpld	$$⊢\phi \to \left(x\in A⟼C\right)\in MblFn$$
18	9 17	eqeltrd	$$⊢\phi \to {\left(x\in U⟼C\right)\upharpoonright }_A\in MblFn$$
19		ssun2	$$⊢B\subseteq A\cup B$$
20	19 2	sseqtrrid	$$⊢\phi \to B\subseteq U$$
21	20	resmptd	$$⊢\phi \to {\left(x\in U⟼C\right)\upharpoonright }_B=\left(x\in B⟼C\right)$$
22		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^y}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^y}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^y}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^y}\right),0\right)\right)$$
23		eqidd	$$⊢\left(\phi \wedge x\in B\right)\to \Re \left(\frac{C}{{\mathrm{i}}^y}\right)=\Re \left(\frac{C}{{\mathrm{i}}^y}\right)$$
24	20	sseld	$$⊢\phi \to \left(x\in B\to x\in U\right)$$
25	24	imdistani	$$⊢\left(\phi \wedge x\in B\right)\to \left(\phi \wedge x\in U\right)$$
26	25 3	syl	$$⊢\left(\phi \wedge x\in B\right)\to C\in ℂ$$
27	22 23 26	isibl2	$$⊢\phi \to \left(\left(x\in B⟼C\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in B⟼C\right)\in MblFn\wedge \forall y\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^y}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^y}\right),0\right)\right)\right)\in ℝ\right)\right)$$
28	5 27	mpbid	$$⊢\phi \to \left(\left(x\in B⟼C\right)\in MblFn\wedge \forall y\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^y}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^y}\right),0\right)\right)\right)\in ℝ\right)$$
29	28	simpld	$$⊢\phi \to \left(x\in B⟼C\right)\in MblFn$$
30	21 29	eqeltrd	$$⊢\phi \to {\left(x\in U⟼C\right)\upharpoonright }_B\in MblFn$$
31	2	eqcomd	$$⊢\phi \to A\cup B=U$$
32	6 18 30 31	mbfres2cn	$$⊢\phi \to \left(x\in U⟼C\right)\in MblFn$$
33	17 14	mbfdm2	$$⊢\phi \to A\in \mathrm{dom}vol$$
34	33	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to A\in \mathrm{dom}vol$$
35	29 26	mbfdm2	$$⊢\phi \to B\in \mathrm{dom}vol$$
36	35	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to B\in \mathrm{dom}vol$$
37	1	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {vol}^{*}\left(A\cap B\right)=0$$
38	2	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to U=A\cup B$$
39	3	adantlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to C\in ℂ$$
40		ax-icn	$$⊢\mathrm{i}\in ℂ$$
41	40	a1i	$$⊢k\in \left(0\dots 3\right)\to \mathrm{i}\in ℂ$$
42		elfznn0	$$⊢k\in \left(0\dots 3\right)\to k\in {\mathbb{N}}_0$$
43	41 42	expcld	$$⊢k\in \left(0\dots 3\right)\to {\mathrm{i}}^k\in ℂ$$
44	43	ad2antlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to {\mathrm{i}}^k\in ℂ$$
45	40	a1i	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to \mathrm{i}\in ℂ$$
46		ine0	$$⊢\mathrm{i}\ne 0$$
47	46	a1i	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to \mathrm{i}\ne 0$$
48		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
49	48	ad2antlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to k\in \mathbb{Z}$$
50	45 47 49	expne0d	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to {\mathrm{i}}^k\ne 0$$
51	39 44 50	divcld	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to \frac{C}{{\mathrm{i}}^k}\in ℂ$$
52	51	recld	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in ℝ$$
53	52	rexrd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in {ℝ}^{*}$$
54	53	adantr	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in {ℝ}^{*}$$
55		simpr	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\to 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
56		pnfge	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in {ℝ}^{*}\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\le \mathrm{+\infty }$$
57	54 56	syl	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\le \mathrm{+\infty }$$
58		0xr	$$⊢0\in {ℝ}^{*}$$
59		pnfxr	$$⊢\mathrm{+\infty }\in {ℝ}^{*}$$
60		elicc1	$$⊢\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(\Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(\Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in {ℝ}^{*}\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\wedge \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\le \mathrm{+\infty }\right)\right)$$
61	58 59 60	mp2an	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(\Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in {ℝ}^{*}\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\wedge \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\le \mathrm{+\infty }\right)$$
62	54 55 57 61	syl3anbrc	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in \left[0,\mathrm{+\infty }\right]$$
63		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
64	63	a1i	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\wedge \neg 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right)\to 0\in \left[0,\mathrm{+\infty }\right]$$
65	62 64	ifclda	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
66		eqid	$$⊢\left(x\in ℝ⟼if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)$$
67		eqid	$$⊢\left(x\in ℝ⟼if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)=\left(x\in ℝ⟼if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)$$
68		ifan	$$⊢if\left(\left(x\in U\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in U,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
69	68	mpteq2i	$$⊢\left(x\in ℝ⟼if\left(\left(x\in U\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(x\in U,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)$$
70		ifan	$$⊢if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
71	70	eqcomi	$$⊢if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
72	71	mpteq2i	$$⊢\left(x\in ℝ⟼if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
73	72	a1i	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to \left(x\in ℝ⟼if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
74	73	fveq2d	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
75		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
76		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
77	75 76 14	isibl2	$$⊢\phi \to \left(\left(x\in A⟼C\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼C\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)\right)$$
78	4 77	mpbid	$$⊢\phi \to \left(\left(x\in A⟼C\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)$$
79	78	simprd	$$⊢\phi \to \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
80	79	r19.21bi	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
81	74 80	eqeltrd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)\right)\in ℝ$$
82		ifan	$$⊢if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)$$
83	82	eqcomi	$$⊢if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
84	83	mpteq2i	$$⊢\left(x\in ℝ⟼if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
85	84	fveq2i	$$⊢{\int }^2\left(\left(x\in ℝ⟼if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
86		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
87		eqidd	$$⊢\left(\phi \wedge x\in B\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
88	86 87 26	isibl2	$$⊢\phi \to \left(\left(x\in B⟼C\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in B⟼C\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)\right)$$
89	5 88	mpbid	$$⊢\phi \to \left(\left(x\in B⟼C\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)$$
90	89	simprd	$$⊢\phi \to \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
91	90	r19.21bi	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
92	85 91	eqeltrid	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)\right)\in ℝ$$
93	34 36 37 38 65 66 67 69 81 92	itg2split	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in U\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)\right)+{\int }^2\left(\left(x\in ℝ⟼if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)\right)$$
94	81 92	readdcld	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)\right)+{\int }^2\left(\left(x\in ℝ⟼if\left(x\in B,if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right),0\right)\right)\right)\in ℝ$$
95	93 94	eqeltrd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in U\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
96	95	ralrimiva	$$⊢\phi \to \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in U\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
97		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in U\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in U\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
98		eqidd	$$⊢\left(\phi \wedge x\in U\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
99	97 98 3	isibl2	$$⊢\phi \to \left(\left(x\in U⟼C\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in U⟼C\right)\in MblFn\wedge \forall k\in \left(0\dots 3\right){\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in U\wedge 0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)\right)$$
100	32 96 99	mpbir2and	$$⊢\phi \to \left(x\in U⟼C\right)\in {𝐿}^1$$