Theorem iblcnlem1

Description: Lemma for iblcnlem . (Contributed by Mario Carneiro, 6-Aug-2014) (Revised by Mario Carneiro, 23-Aug-2014)

	Ref	Expression
Hypotheses	itgcnlem.r	$$⊢R={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(B\right)\right),\Re \left(B\right),0\right)\right)\right)$$
	itgcnlem.s	$$⊢S={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -\Re \left(B\right)\right),-\Re \left(B\right),0\right)\right)\right)$$
	itgcnlem.t	$$⊢T={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Im \left(B\right)\right),\Im \left(B\right),0\right)\right)\right)$$
	itgcnlem.u	$$⊢U={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -\Im \left(B\right)\right),-\Im \left(B\right),0\right)\right)\right)$$
	itgcnlem1.v	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
Assertion	iblcnlem1	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge \left(R\in ℝ\wedge S\in ℝ\right)\wedge \left(T\in ℝ\wedge U\in ℝ\right)\right)\right)$$

Proof

Step	Hyp	Ref	Expression
1		itgcnlem.r	$$⊢R={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(B\right)\right),\Re \left(B\right),0\right)\right)\right)$$
2		itgcnlem.s	$$⊢S={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -\Re \left(B\right)\right),-\Re \left(B\right),0\right)\right)\right)$$
3		itgcnlem.t	$$⊢T={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Im \left(B\right)\right),\Im \left(B\right),0\right)\right)\right)$$
4		itgcnlem.u	$$⊢U={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -\Im \left(B\right)\right),-\Im \left(B\right),0\right)\right)\right)$$
5		itgcnlem1.v	$$⊢\left(\phi \wedge x\in A\right)\to B\in ℂ$$
6		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)$$
7		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)$$
8	6 7 5	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)$$
9		c0ex	$$⊢0\in \mathrm{V}$$
10		1ex	$$⊢1\in \mathrm{V}$$
11		ax-icn	$$⊢\mathrm{i}\in ℂ$$
12		exp0	$$⊢\mathrm{i}\in ℂ\to {\mathrm{i}}^0=1$$
13	11 12	ax-mp	$$⊢{\mathrm{i}}^0=1$$
14	13	itgvallem	$$⊢k=0\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)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\right),0\right)\right)\right)$$
15	14	eleq1d	$$⊢k=0\to \left({\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 ℝ\leftrightarrow {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\right),0\right)\right)\right)\in ℝ\right)$$
16		exp1	$$⊢\mathrm{i}\in ℂ\to {\mathrm{i}}^1=\mathrm{i}$$
17	11 16	ax-mp	$$⊢{\mathrm{i}}^1=\mathrm{i}$$
18	17	itgvallem	$$⊢k=1\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)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{\mathrm{i}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)\right)\right)$$
19	18	eleq1d	$$⊢k=1\to \left({\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 ℝ\leftrightarrow {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{\mathrm{i}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)\right)\right)\in ℝ\right)$$
20	9 10 15 19	ralpr	$$⊢\forall k\in \left\{0,1\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 ℝ\leftrightarrow \left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\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}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)\right)\right)\in ℝ\right)$$
21	5	div1d	$$⊢\left(\phi \wedge x\in A\right)\to \frac{B}{1}=B$$
22	21	fveq2d	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{B}{1}\right)=\Re \left(B\right)$$
23	22	ibllem	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(B\right)\right),\Re \left(B\right),0\right)$$
24	23	mpteq2dv	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(B\right)\right),\Re \left(B\right),0\right)\right)$$
25	24	fveq2d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(B\right)\right),\Re \left(B\right),0\right)\right)\right)$$
26	25 1	eqtr4di	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\right),0\right)\right)\right)=R$$
27	26	eleq1d	$$⊢\phi \to \left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\right),0\right)\right)\right)\in ℝ\leftrightarrow R\in ℝ\right)$$
28		imval	$$⊢B\in ℂ\to \Im \left(B\right)=\Re \left(\frac{B}{\mathrm{i}}\right)$$
29	5 28	syl	$$⊢\left(\phi \wedge x\in A\right)\to \Im \left(B\right)=\Re \left(\frac{B}{\mathrm{i}}\right)$$
30	29	ibllem	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le \Im \left(B\right)\right),\Im \left(B\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{\mathrm{i}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)$$
31	30	mpteq2dv	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Im \left(B\right)\right),\Im \left(B\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{\mathrm{i}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)\right)$$
32	31	fveq2d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Im \left(B\right)\right),\Im \left(B\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{\mathrm{i}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)\right)\right)$$
33	3 32	syl5req	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{\mathrm{i}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)\right)\right)=T$$
34	33	eleq1d	$$⊢\phi \to \left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{\mathrm{i}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)\right)\right)\in ℝ\leftrightarrow T\in ℝ\right)$$
35	27 34	anbi12d	$$⊢\phi \to \left(\left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{1}\right)\right),\Re \left(\frac{B}{1}\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}}\right)\right),\Re \left(\frac{B}{\mathrm{i}}\right),0\right)\right)\right)\in ℝ\right)\leftrightarrow \left(R\in ℝ\wedge T\in ℝ\right)\right)$$
36	20 35	syl5bb	$$⊢\phi \to \left(\forall k\in \left\{0,1\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 ℝ\leftrightarrow \left(R\in ℝ\wedge T\in ℝ\right)\right)$$
37		2ex	$$⊢2\in \mathrm{V}$$
38		3ex	$$⊢3\in \mathrm{V}$$
39		i2	$$⊢{\mathrm{i}}^2=-1$$
40	39	itgvallem	$$⊢k=2\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)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\right),0\right)\right)\right)$$
41	40	eleq1d	$$⊢k=2\to \left({\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 ℝ\leftrightarrow {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\right),0\right)\right)\right)\in ℝ\right)$$
42		i3	$$⊢{\mathrm{i}}^3=-\mathrm{i}$$
43	42	itgvallem	$$⊢k=3\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)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-\mathrm{i}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)\right)\right)$$
44	43	eleq1d	$$⊢k=3\to \left({\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 ℝ\leftrightarrow {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-\mathrm{i}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)\right)\right)\in ℝ\right)$$
45	37 38 41 44	ralpr	$$⊢\forall k\in \left\{2,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 ℝ\leftrightarrow \left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\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}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)\right)\right)\in ℝ\right)$$
46	5	renegd	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(-B\right)=-\Re \left(B\right)$$
47		ax-1cn	$$⊢1\in ℂ$$
48	47	negnegi	$$⊢--1=1$$
49	48	oveq2i	$$⊢\frac{-B}{--1}=\frac{-B}{1}$$
50	5	negcld	$$⊢\left(\phi \wedge x\in A\right)\to -B\in ℂ$$
51	50	div1d	$$⊢\left(\phi \wedge x\in A\right)\to \frac{-B}{1}=-B$$
52	49 51	syl5eq	$$⊢\left(\phi \wedge x\in A\right)\to \frac{-B}{--1}=-B$$
53	47	negcli	$$⊢-1\in ℂ$$
54		neg1ne0	$$⊢-1\ne 0$$
55		div2neg	$$⊢\left(B\in ℂ\wedge -1\in ℂ\wedge -1\ne 0\right)\to \frac{-B}{--1}=\frac{B}{-1}$$
56	53 54 55	mp3an23	$$⊢B\in ℂ\to \frac{-B}{--1}=\frac{B}{-1}$$
57	5 56	syl	$$⊢\left(\phi \wedge x\in A\right)\to \frac{-B}{--1}=\frac{B}{-1}$$
58	52 57	eqtr3d	$$⊢\left(\phi \wedge x\in A\right)\to -B=\frac{B}{-1}$$
59	58	fveq2d	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(-B\right)=\Re \left(\frac{B}{-1}\right)$$
60	46 59	eqtr3d	$$⊢\left(\phi \wedge x\in A\right)\to -\Re \left(B\right)=\Re \left(\frac{B}{-1}\right)$$
61	60	ibllem	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le -\Re \left(B\right)\right),-\Re \left(B\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\right),0\right)$$
62	61	mpteq2dv	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -\Re \left(B\right)\right),-\Re \left(B\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\right),0\right)\right)$$
63	62	fveq2d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -\Re \left(B\right)\right),-\Re \left(B\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\right),0\right)\right)\right)$$
64	2 63	syl5req	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\right),0\right)\right)\right)=S$$
65	64	eleq1d	$$⊢\phi \to \left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\right),0\right)\right)\right)\in ℝ\leftrightarrow S\in ℝ\right)$$
66		imval	$$⊢-B\in ℂ\to \Im \left(-B\right)=\Re \left(\frac{-B}{\mathrm{i}}\right)$$
67	50 66	syl	$$⊢\left(\phi \wedge x\in A\right)\to \Im \left(-B\right)=\Re \left(\frac{-B}{\mathrm{i}}\right)$$
68	5	imnegd	$$⊢\left(\phi \wedge x\in A\right)\to \Im \left(-B\right)=-\Im \left(B\right)$$
69	11	negnegi	$$⊢-\left(-\mathrm{i}\right)=\mathrm{i}$$
70	69	eqcomi	$$⊢\mathrm{i}=-\left(-\mathrm{i}\right)$$
71	70	oveq2i	$$⊢\frac{-B}{\mathrm{i}}=\frac{-B}{-\left(-\mathrm{i}\right)}$$
72	11	negcli	$$⊢-\mathrm{i}\in ℂ$$
73		ine0	$$⊢\mathrm{i}\ne 0$$
74	11 73	negne0i	$$⊢-\mathrm{i}\ne 0$$
75		div2neg	$$⊢\left(B\in ℂ\wedge -\mathrm{i}\in ℂ\wedge -\mathrm{i}\ne 0\right)\to \frac{-B}{-\left(-\mathrm{i}\right)}=\frac{B}{-\mathrm{i}}$$
76	72 74 75	mp3an23	$$⊢B\in ℂ\to \frac{-B}{-\left(-\mathrm{i}\right)}=\frac{B}{-\mathrm{i}}$$
77	5 76	syl	$$⊢\left(\phi \wedge x\in A\right)\to \frac{-B}{-\left(-\mathrm{i}\right)}=\frac{B}{-\mathrm{i}}$$
78	71 77	syl5eq	$$⊢\left(\phi \wedge x\in A\right)\to \frac{-B}{\mathrm{i}}=\frac{B}{-\mathrm{i}}$$
79	78	fveq2d	$$⊢\left(\phi \wedge x\in A\right)\to \Re \left(\frac{-B}{\mathrm{i}}\right)=\Re \left(\frac{B}{-\mathrm{i}}\right)$$
80	67 68 79	3eqtr3d	$$⊢\left(\phi \wedge x\in A\right)\to -\Im \left(B\right)=\Re \left(\frac{B}{-\mathrm{i}}\right)$$
81	80	ibllem	$$⊢\phi \to if\left(\left(x\in A\wedge 0\le -\Im \left(B\right)\right),-\Im \left(B\right),0\right)=if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-\mathrm{i}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)$$
82	81	mpteq2dv	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -\Im \left(B\right)\right),-\Im \left(B\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-\mathrm{i}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)\right)$$
83	82	fveq2d	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le -\Im \left(B\right)\right),-\Im \left(B\right),0\right)\right)\right)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-\mathrm{i}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)\right)\right)$$
84	4 83	syl5req	$$⊢\phi \to {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-\mathrm{i}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)\right)\right)=U$$
85	84	eleq1d	$$⊢\phi \to \left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-\mathrm{i}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)\right)\right)\in ℝ\leftrightarrow U\in ℝ\right)$$
86	65 85	anbi12d	$$⊢\phi \to \left(\left({\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in A\wedge 0\le \Re \left(\frac{B}{-1}\right)\right),\Re \left(\frac{B}{-1}\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}}\right)\right),\Re \left(\frac{B}{-\mathrm{i}}\right),0\right)\right)\right)\in ℝ\right)\leftrightarrow \left(S\in ℝ\wedge U\in ℝ\right)\right)$$
87	45 86	syl5bb	$$⊢\phi \to \left(\forall k\in \left\{2,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 ℝ\leftrightarrow \left(S\in ℝ\wedge U\in ℝ\right)\right)$$
88	36 87	anbi12d	$$⊢\phi \to \left(\left(\forall k\in \left\{0,1\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 ℝ\wedge \forall k\in \left\{2,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)\leftrightarrow \left(\left(R\in ℝ\wedge T\in ℝ\right)\wedge \left(S\in ℝ\wedge U\in ℝ\right)\right)\right)$$
89		fz0to3un2pr	$$⊢\left(0\dots 3\right)=\left\{0,1\right\}\cup \left\{2,3\right\}$$
90	89	raleqi	$$⊢\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 ℝ\leftrightarrow \forall k\in \left(\left\{0,1\right\}\cup \left\{2,3\right\}\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 ℝ$$
91		ralunb	$$⊢\forall k\in \left(\left\{0,1\right\}\cup \left\{2,3\right\}\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 ℝ\leftrightarrow \left(\forall k\in \left\{0,1\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 ℝ\wedge \forall k\in \left\{2,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)$$
92	90 91	bitri	$$⊢\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 ℝ\leftrightarrow \left(\forall k\in \left\{0,1\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 ℝ\wedge \forall k\in \left\{2,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)$$
93		an4	$$⊢\left(\left(R\in ℝ\wedge S\in ℝ\right)\wedge \left(T\in ℝ\wedge U\in ℝ\right)\right)\leftrightarrow \left(\left(R\in ℝ\wedge T\in ℝ\right)\wedge \left(S\in ℝ\wedge U\in ℝ\right)\right)$$
94	88 92 93	3bitr4g	$$⊢\phi \to \left(\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 ℝ\leftrightarrow \left(\left(R\in ℝ\wedge S\in ℝ\right)\wedge \left(T\in ℝ\wedge U\in ℝ\right)\right)\right)$$
95	94	anbi2d	$$⊢\phi \to \left(\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)\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge \left(\left(R\in ℝ\wedge S\in ℝ\right)\wedge \left(T\in ℝ\wedge U\in ℝ\right)\right)\right)\right)$$
96		3anass	$$⊢\left(\left(x\in A⟼B\right)\in MblFn\wedge \left(R\in ℝ\wedge S\in ℝ\right)\wedge \left(T\in ℝ\wedge U\in ℝ\right)\right)\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge \left(\left(R\in ℝ\wedge S\in ℝ\right)\wedge \left(T\in ℝ\wedge U\in ℝ\right)\right)\right)$$
97	95 96	bitr4di	$$⊢\phi \to \left(\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)\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge \left(R\in ℝ\wedge S\in ℝ\right)\wedge \left(T\in ℝ\wedge U\in ℝ\right)\right)\right)$$
98	8 97	bitrd	$$⊢\phi \to \left(\left(x\in A⟼B\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in A⟼B\right)\in MblFn\wedge \left(R\in ℝ\wedge S\in ℝ\right)\wedge \left(T\in ℝ\wedge U\in ℝ\right)\right)\right)$$