Theorem iblss

Description: A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

	Ref	Expression
Hypotheses	iblss.1	$$⊢\phi \to A\subseteq B$$
	iblss.2	$$⊢\phi \to A\in \mathrm{dom}vol$$
	iblss.3	$$⊢\left(\phi \wedge x\in B\right)\to C\in V$$
	iblss.4	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$
Assertion	iblss	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$

Proof

Step	Hyp	Ref	Expression
1		iblss.1	$$⊢\phi \to A\subseteq B$$
2		iblss.2	$$⊢\phi \to A\in \mathrm{dom}vol$$
3		iblss.3	$$⊢\left(\phi \wedge x\in B\right)\to C\in V$$
4		iblss.4	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$
5	1	resmptd	$$⊢\phi \to {\left(x\in B⟼C\right)\upharpoonright }_A=\left(x\in A⟼C\right)$$
6		iblmbf	$$⊢\left(x\in B⟼C\right)\in {𝐿}^1\to \left(x\in B⟼C\right)\in MblFn$$
7	4 6	syl	$$⊢\phi \to \left(x\in B⟼C\right)\in MblFn$$
8		mbfres	$$⊢\left(\left(x\in B⟼C\right)\in MblFn\wedge A\in \mathrm{dom}vol\right)\to {\left(x\in B⟼C\right)\upharpoonright }_A\in MblFn$$
9	7 2 8	syl2anc	$$⊢\phi \to {\left(x\in B⟼C\right)\upharpoonright }_A\in MblFn$$
10	5 9	eqeltrrd	$$⊢\phi \to \left(x\in A⟼C\right)\in MblFn$$
11		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)$$
12	1	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in B$$
13	12	ad4ant14	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in A\right)\to x\in B$$
14	7 3	mbfmptcl	$$⊢\left(\phi \wedge x\in B\right)\to C\in ℂ$$
15	14	ad4ant14	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to C\in ℂ$$
16		ax-icn	$$⊢\mathrm{i}\in ℂ$$
17		ine0	$$⊢\mathrm{i}\ne 0$$
18		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
19	18	ad3antlr	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to k\in \mathbb{Z}$$
20		expclz	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\in ℂ$$
21	16 17 19 20	mp3an12i	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to {\mathrm{i}}^k\in ℂ$$
22		expne0i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\ne 0$$
23	16 17 19 22	mp3an12i	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to {\mathrm{i}}^k\ne 0$$
24	15 21 23	divcld	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to \frac{C}{{\mathrm{i}}^k}\in ℂ$$
25	24	recld	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in ℝ$$
26		0re	$$⊢0\in ℝ$$
27		ifcl	$$⊢\left(\Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in ℝ\wedge 0\in ℝ\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 ℝ$$
28	25 26 27	sylancl	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\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 ℝ$$
29	28	rexrd	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\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 {ℝ}^{*}$$
30		max1	$$⊢\left(0\in ℝ\wedge \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in ℝ\right)\to 0\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
31	26 25 30	sylancr	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to 0\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
32		elxrge0	$$⊢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]\leftrightarrow \left(if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\in {ℝ}^{*}\wedge 0\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
33	29 31 32	sylanbrc	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\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]$$
34	13 33	syldan	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in A\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]$$
35		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
36	35	a1i	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge \neg x\in A\right)\to 0\in \left[0,\mathrm{+\infty }\right]$$
37	34 36	ifclda	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\to 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)\in \left[0,\mathrm{+\infty }\right]$$
38	11 37	eqeltrid	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\to 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)\in \left[0,\mathrm{+\infty }\right]$$
39	38	fmpttd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\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[0,\mathrm{+\infty }\right]$$
40		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)$$
41		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)$$
42	40 41 4 3	iblitg	$$⊢\left(\phi \wedge k\in \mathbb{Z}\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 ℝ$$
43	18 42	sylan2	$$⊢\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 ℝ$$
44		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)$$
45	35	a1i	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge \neg x\in B\right)\to 0\in \left[0,\mathrm{+\infty }\right]$$
46	33 45	ifclda	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\to 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)\in \left[0,\mathrm{+\infty }\right]$$
47	44 46	eqeltrid	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\to 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)\in \left[0,\mathrm{+\infty }\right]$$
48	47	fmpttd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\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[0,\mathrm{+\infty }\right]$$
49	28	leidd	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
50		breq1	$$⊢if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\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)\to \left(if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\leftrightarrow 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)\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
51		breq1	$$⊢0=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)\to \left(0\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\leftrightarrow 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)\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)$$
52	50 51	ifboth	$$⊢\left(if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\wedge 0\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)\right)\to 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)\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
53	49 31 52	syl2anc	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to 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)\le if\left(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
54		iftrue	$$⊢x\in B\to 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(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
55	54	adantl	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to 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(0\le \Re \left(\frac{C}{{\mathrm{i}}^k}\right),\Re \left(\frac{C}{{\mathrm{i}}^k}\right),0\right)$$
56	53 55	breqtrrd	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge x\in B\right)\to 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)\le 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)$$
57		0le0	$$⊢0\le 0$$
58	57	a1i	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge \neg x\in B\right)\to 0\le 0$$
59	13	stoic1a	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge \neg x\in B\right)\to \neg x\in A$$
60	59	iffalsed	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge \neg x\in B\right)\to 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)=0$$
61		iffalse	$$⊢\neg x\in B\to 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)=0$$
62	61	adantl	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge \neg x\in B\right)\to 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)=0$$
63	58 60 62	3brtr4d	$$⊢\left(\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\wedge \neg x\in B\right)\to 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)\le 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)$$
64	56 63	pm2.61dan	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\to 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)\le 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)$$
65	64 11 44	3brtr4g	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\to 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)\le 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)$$
66	65	ralrimiva	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to \forall 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)\le 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)$$
67		reex	$$⊢ℝ\in \mathrm{V}$$
68	67	a1i	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to ℝ\in \mathrm{V}$$
69		eqidd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\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)$$
70		eqidd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\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)$$
71	68 38 47 69 70	ofrfval2	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to \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){\le }_f\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)\leftrightarrow \forall 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)\le 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)$$
72	66 71	mpbird	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\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){\le }_f\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)$$
73		itg2le	$$⊢\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):ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge \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[0,\mathrm{+\infty }\right]\wedge \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){\le }_f\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)\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)\le {\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)$$
74	39 48 72 73	syl3anc	$$⊢\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)\le {\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)$$
75		itg2lecl	$$⊢\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):ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {\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 ℝ\wedge {\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)\le {\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)\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 ℝ$$
76	39 43 74 75	syl3anc	$$⊢\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 ℝ$$
77	76	ralrimiva	$$⊢\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 ℝ$$
78		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)$$
79		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)$$
80	12 14	syldan	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
81	78 79 80	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)$$
82	10 77 81	mpbir2and	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$