Theorem iblabsr

Description: A measurable function is integrable iff its absolute value is integrable. (See iblabs for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014)

	Ref	Expression
Hypotheses	iblabsr.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
	iblabsr.2	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
	iblabsr.3	$$⊢\phi \to \left(x\in A⟼\left|B\right|\right)\in {𝐿}^1$$
Assertion	iblabsr	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$

Proof

Step	Hyp	Ref	Expression
1		iblabsr.1	$$⊢\left(\phi \wedge x\in A\right)\to B\in V$$
2		iblabsr.2	$$⊢\phi \to \left(x\in A⟼B\right)\in MblFn$$
3		iblabsr.3	$$⊢\phi \to \left(x\in A⟼\left|B\right|\right)\in {𝐿}^1$$
4		ifan	$$⊢if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)$$
5	2 1	mbfmptcl	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
6	5	adantlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to B\in ℂ$$
7		ax-icn	$$⊢\mathrm{i}\in ℂ$$
8		ine0	$$⊢\mathrm{i}\ne 0$$
9		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
10	9	ad2antlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to k\in \mathbb{Z}$$
11		expclz	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\in ℂ$$
12	7 8 10 11	mp3an12i	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to {\mathrm{i}}^k\in ℂ$$
13		expne0i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\ne 0$$
14	7 8 10 13	mp3an12i	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to {\mathrm{i}}^k\ne 0$$
15	6 12 14	divcld	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \frac{B}{{\mathrm{i}}^k}\in ℂ$$
16	15	recld	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\in ℝ$$
17		0re	$$⊢0\in ℝ$$
18		ifcl	$$⊢\left(\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\in ℝ$$
19	16 17 18	sylancl	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\in ℝ$$
20	19	rexrd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\in {ℝ}^{*}$$
21		max1	$$⊢\left(0\in ℝ\wedge \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\in ℝ\right)\to 0\le if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)$$
22	17 16 21	sylancr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to 0\le if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)$$
23		elxrge0	$$⊢if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\in {ℝ}^{*}\wedge 0\le if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)$$
24	20 22 23	sylanbrc	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
25		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
26	25	a1i	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in A\right)\to 0\in \left[0,\mathrm{+\infty }\right]$$
27	24 26	ifclda	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
28	4 27	eqeltrid	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
29	28	adantr	$$⊢\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
30	29	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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]$$
31	5	abscld	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|\in ℝ$$
32	5	absge0d	$$⊢\left(\phi \wedge x\in A\right)\to 0\le \left|B\right|$$
33	31 32	iblpos	$$⊢\phi \to \left(\left(x\in A⟼\left|B\right|\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼\left|B\right|\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)\right)\in ℝ\right)\right)$$
34	3 33	mpbid	$$⊢\phi \to \left(\left(x\in A⟼\left|B\right|\right)\in MblFn\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)\right)\in ℝ\right)$$
35	34	simprd	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)\right)\in ℝ$$
36	35	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)\right)\in ℝ$$
37	31	rexrd	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|\in {ℝ}^{*}$$
38		elxrge0	$$⊢\left|B\right|\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(\left|B\right|\in {ℝ}^{*}\wedge 0\le \left|B\right|\right)$$
39	37 32 38	sylanbrc	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|\in \left[0,\mathrm{+\infty }\right]$$
40	25	a1i	$$⊢\left(\phi \wedge \neg x\in A\right)\to 0\in \left[0,\mathrm{+\infty }\right]$$
41	39 40	ifclda	$$⊢\phi \to if\left(x\in A,\left|B\right|,0\right)\in \left[0,\mathrm{+\infty }\right]$$
42	41	adantr	$$⊢\left(\phi \wedge x\in ℝ\right)\to if\left(x\in A,\left|B\right|,0\right)\in \left[0,\mathrm{+\infty }\right]$$
43	42	fmpttd	$$⊢\phi \to \left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]$$
44	43	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to \left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]$$
45	15	releabsd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\le \left|\frac{B}{{\mathrm{i}}^k}\right|$$
46	6 12 14	absdivd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \left|\frac{B}{{\mathrm{i}}^k}\right|=\frac{\left|B\right|}{\left|{\mathrm{i}}^k\right|}$$
47		elfznn0	$$⊢k\in \left(0\dots 3\right)\to k\in {\mathbb{N}}_0$$
48	47	ad2antlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to k\in {\mathbb{N}}_0$$
49		absexp	$$⊢\left(\mathrm{i}\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to \left|{\mathrm{i}}^k\right|={\left|\mathrm{i}\right|}^k$$
50	7 48 49	sylancr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \left|{\mathrm{i}}^k\right|={\left|\mathrm{i}\right|}^k$$
51		absi	$$⊢\left|\mathrm{i}\right|=1$$
52	51	oveq1i	$$⊢{\left|\mathrm{i}\right|}^k=1^k$$
53		1exp	$$⊢k\in \mathbb{Z}\to 1^k=1$$
54	10 53	syl	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to 1^k=1$$
55	52 54	syl5eq	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to {\left|\mathrm{i}\right|}^k=1$$
56	50 55	eqtrd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \left|{\mathrm{i}}^k\right|=1$$
57	56	oveq2d	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \frac{\left|B\right|}{\left|{\mathrm{i}}^k\right|}=\frac{\left|B\right|}{1}$$
58	31	recnd	$$⊢\left(\phi \wedge x\in A\right)\to \left|B\right|\in ℂ$$
59	58	adantlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \left|B\right|\in ℂ$$
60	59	div1d	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \frac{\left|B\right|}{1}=\left|B\right|$$
61	46 57 60	3eqtrd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \left|\frac{B}{{\mathrm{i}}^k}\right|=\left|B\right|$$
62	45 61	breqtrd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\le \left|B\right|$$
63	6	absge0d	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to 0\le \left|B\right|$$
64		breq1	$$⊢\Re \left(\frac{B}{{\mathrm{i}}^k}\right)=if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\to \left(\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\le \left|B\right|\leftrightarrow if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\le \left|B\right|\right)$$
65		breq1	$$⊢0=if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\to \left(0\le \left|B\right|\leftrightarrow if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\le \left|B\right|\right)$$
66	64 65	ifboth	$$⊢\left(\Re \left(\frac{B}{{\mathrm{i}}^k}\right)\le \left|B\right|\wedge 0\le \left|B\right|\right)\to if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\le \left|B\right|$$
67	62 63 66	syl2anc	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\le \left|B\right|$$
68		iftrue	$$⊢x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)$$
69	68	adantl	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)=if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)$$
70		iftrue	$$⊢x\in A\to if\left(x\in A,\left|B\right|,0\right)=\left|B\right|$$
71	70	adantl	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(x\in A,\left|B\right|,0\right)=\left|B\right|$$
72	67 69 71	3brtr4d	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)\le if\left(x\in A,\left|B\right|,0\right)$$
73	72	ex	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to \left(x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)\le if\left(x\in A,\left|B\right|,0\right)\right)$$
74		0le0	$$⊢0\le 0$$
75	74	a1i	$$⊢\neg x\in A\to 0\le 0$$
76		iffalse	$$⊢\neg x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)=0$$
77		iffalse	$$⊢\neg x\in A\to if\left(x\in A,\left|B\right|,0\right)=0$$
78	75 76 77	3brtr4d	$$⊢\neg x\in A\to if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)\le if\left(x\in A,\left|B\right|,0\right)$$
79	73 78	pm2.61d1	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(x\in A,if\left(0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right),0\right)\le if\left(x\in A,\left|B\right|,0\right)$$
80	4 79	eqbrtrid	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\le if\left(x\in A,\left|B\right|,0\right)$$
81	80	ralrimivw	$$⊢\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\le if\left(x\in A,\left|B\right|,0\right)$$
82		reex	$$⊢ℝ\in \mathrm{V}$$
83	82	a1i	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to ℝ\in \mathrm{V}$$
84	37	adantlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \left|B\right|\in {ℝ}^{*}$$
85	84 63 38	sylanbrc	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in A\right)\to \left|B\right|\in \left[0,\mathrm{+\infty }\right]$$
86	85 26	ifclda	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(x\in A,\left|B\right|,0\right)\in \left[0,\mathrm{+\infty }\right]$$
87	86	adantr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in ℝ\right)\to if\left(x\in A,\left|B\right|,0\right)\in \left[0,\mathrm{+\infty }\right]$$
88		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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)$$
89		eqidd	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to \left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)=\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)$$
90	83 29 87 88 89	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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right){\le }_f\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)\leftrightarrow \forall x\in ℝif\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\le if\left(x\in A,\left|B\right|,0\right)\right)$$
91	81 90	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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right){\le }_f\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)$$
92		itg2le	$$⊢\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge \left(x\in ℝ⟼if\left(x\in A,\left|B\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right){\le }_f\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)\right)\to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\le {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)\right)$$
93	30 44 91 92	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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\le {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,\left|B\right|,0\right)\right)\right)$$
94		itg2lecl	$$⊢\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,\left|B\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\le {\int }^2\left(\left(x\in ℝ⟼if\left(x\in A,\left|B\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
95	30 36 93 94	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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\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 A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ$$
97		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)$$
98		eqidd	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{B}{{\mathrm{i}}^k}\right)=\Re \left(\frac{B}{{\mathrm{i}}^k}\right)$$
99	97 98 1	isibl2	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼B\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{B}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{B}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)\right)$$
100	2 96 99	mpbir2and	$$⊢\phi \to \left(x\in A⟼B\right)\in {𝐿}^1$$