Theorem itgeqa

Description: Approximate equality of integrals. If C ( x ) = D ( x ) for almost all x , then S. B C ( x )d x = S. B D ( x ) d x and one is integrable iff the other is. (Contributed by Mario Carneiro, 12-Aug-2014) (Revised by Mario Carneiro, 2-Sep-2014)

	Ref	Expression
Hypotheses	itgeqa.1	$$⊢\left(\phi \wedge x\in B\right)\to C\in ℂ$$
	itgeqa.2	$$⊢\left(\phi \wedge x\in B\right)\to D\in ℂ$$
	itgeqa.3	$$⊢\phi \to A\subseteq ℝ$$
	itgeqa.4	$$⊢\phi \to {vol}^{*}\left(A\right)=0$$
	itgeqa.5	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to C=D$$
Assertion	itgeqa	$$⊢\phi \to \left(\left(\left(x\in B⟼C\right)\in {𝐿}^1\leftrightarrow \left(x\in B⟼D\right)\in {𝐿}^1\right)\wedge {\int }_{B}Cdx={\int }_{B}Ddx\right)$$

Proof

Step	Hyp	Ref	Expression
1		itgeqa.1	$$⊢\left(\phi \wedge x\in B\right)\to C\in ℂ$$
2		itgeqa.2	$$⊢\left(\phi \wedge x\in B\right)\to D\in ℂ$$
3		itgeqa.3	$$⊢\phi \to A\subseteq ℝ$$
4		itgeqa.4	$$⊢\phi \to {vol}^{*}\left(A\right)=0$$
5		itgeqa.5	$$⊢\left(\phi \wedge x\in \left(B\setminus A\right)\right)\to C=D$$
6	3 4 5 1 2	mbfeqa	$$⊢\phi \to \left(\left(x\in B⟼C\right)\in MblFn\leftrightarrow \left(x\in B⟼D\right)\in MblFn\right)$$
7		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)$$
8	1	adantlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to C\in ℂ$$
9		ax-icn	$$⊢\mathrm{i}\in ℂ$$
10		ine0	$$⊢\mathrm{i}\ne 0$$
11		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
12	11	ad2antlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to k\in \mathbb{Z}$$
13		expclz	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\in ℂ$$
14	9 10 12 13	mp3an12i	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to {\mathrm{i}}^k\in ℂ$$
15		expne0i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\ne 0$$
16	9 10 12 15	mp3an12i	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to {\mathrm{i}}^k\ne 0$$
17	8 14 16	divcld	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to \frac{C}{{\mathrm{i}}^k}\in ℂ$$
18	17	recld	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in ℝ$$
19		0re	$$⊢0\in ℝ$$
20		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 ℝ$$
21	18 19 20	sylancl	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\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 ℝ$$
22	21	rexrd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\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 {ℝ}^{*}$$
23		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)$$
24	19 18 23	sylancr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\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)$$
25		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)$$
26	22 24 25	sylanbrc	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\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]$$
27		0e0iccpnf	$$⊢0\in \left[0,\mathrm{+\infty }\right]$$
28	27	a1i	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge \neg x\in B\right)\to 0\in \left[0,\mathrm{+\infty }\right]$$
29	26 28	ifclda	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\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]$$
30	7 29	eqeltrid	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\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]$$
31	30	adantr	$$⊢\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]$$
32	31	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]$$
33		ifan	$$⊢if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)=if\left(x\in B,if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right),0\right)$$
34	2	adantlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to D\in ℂ$$
35	34 14 16	divcld	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to \frac{D}{{\mathrm{i}}^k}\in ℂ$$
36	35	recld	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\in ℝ$$
37		ifcl	$$⊢\left(\Re \left(\frac{D}{{\mathrm{i}}^k}\right)\in ℝ\wedge 0\in ℝ\right)\to if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in ℝ$$
38	36 19 37	sylancl	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in ℝ$$
39	38	rexrd	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in {ℝ}^{*}$$
40		max1	$$⊢\left(0\in ℝ\wedge \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\in ℝ\right)\to 0\le if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)$$
41	19 36 40	sylancr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to 0\le if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)$$
42		elxrge0	$$⊢if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]\leftrightarrow \left(if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in {ℝ}^{*}\wedge 0\le if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)$$
43	39 41 42	sylanbrc	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in B\right)\to if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
44	43 28	ifclda	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(x\in B,if\left(0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
45	33 44	eqeltrid	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
46	45	adantr	$$⊢\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{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in \left[0,\mathrm{+\infty }\right]$$
47	46	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{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]$$
48	3	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to A\subseteq ℝ$$
49	4	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {vol}^{*}\left(A\right)=0$$
50		simpll	$$⊢\left(\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\wedge x\in B\right)\to \phi$$
51		simpr	$$⊢\left(\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\wedge x\in B\right)\to x\in B$$
52		eldifn	$$⊢x\in \left(ℝ\setminus A\right)\to \neg x\in A$$
53	52	ad2antlr	$$⊢\left(\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\wedge x\in B\right)\to \neg x\in A$$
54	51 53	eldifd	$$⊢\left(\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\wedge x\in B\right)\to x\in \left(B\setminus A\right)$$
55	50 54 5	syl2anc	$$⊢\left(\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\wedge x\in B\right)\to C=D$$
56	55	fvoveq1d	$$⊢\left(\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\wedge x\in B\right)\to \Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{D}{{\mathrm{i}}^k}\right)$$
57	56	ibllem	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\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)=if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)$$
58		eldifi	$$⊢x\in \left(ℝ\setminus A\right)\to x\in ℝ$$
59	58	adantl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to x\in ℝ$$
60		fvex	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)\in \mathrm{V}$$
61		c0ex	$$⊢0\in \mathrm{V}$$
62	60 61	ifex	$$⊢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 \mathrm{V}$$
63		eqid	$$⊢\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)$$
64	63	fvmpt2	$$⊢\left(x\in ℝ\wedge 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 \mathrm{V}\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\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)$$
65	59 62 64	sylancl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\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\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)$$
66		fvex	$$⊢\Re \left(\frac{D}{{\mathrm{i}}^k}\right)\in \mathrm{V}$$
67	66 61	ifex	$$⊢if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in \mathrm{V}$$
68		eqid	$$⊢\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)$$
69	68	fvmpt2	$$⊢\left(x\in ℝ\wedge if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\in \mathrm{V}\right)\to \left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(x\right)=if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)$$
70	59 67 69	sylancl	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\right)\right)\to \left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(x\right)=if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)$$
71	57 65 70	3eqtr4d	$$⊢\left(\phi \wedge x\in \left(ℝ\setminus A\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\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(x\right)$$
72	71	ralrimiva	$$⊢\phi \to \forall x\in \left(ℝ\setminus A\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)\left(x\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(x\right)$$
73		nfv	$$⊢Ⅎy\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\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(x\right)$$
74		nffvmpt1	$$⊢\underset{\_}{Ⅎ}x\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(y\right)$$
75		nffvmpt1	$$⊢\underset{\_}{Ⅎ}x\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(y\right)$$
76	74 75	nfeq	$$⊢Ⅎx\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(y\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(y\right)$$
77		fveq2	$$⊢x=y\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\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)\left(y\right)$$
78		fveq2	$$⊢x=y\to \left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(x\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(y\right)$$
79	77 78	eqeq12d	$$⊢x=y\to \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)\left(x\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(x\right)\leftrightarrow \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(y\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(y\right)\right)$$
80	73 76 79	cbvralw	$$⊢\forall x\in \left(ℝ\setminus A\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)\left(x\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(x\right)\leftrightarrow \forall y\in \left(ℝ\setminus A\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)\left(y\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(y\right)$$
81	72 80	sylib	$$⊢\phi \to \forall y\in \left(ℝ\setminus A\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)\left(y\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(y\right)$$
82	81	r19.21bi	$$⊢\left(\phi \wedge y\in \left(ℝ\setminus A\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(y\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(y\right)$$
83	82	adantlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge y\in \left(ℝ\setminus A\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(y\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\left(y\right)$$
84	32 47 48 49 83	itg2eqa	$$⊢\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)={\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
85	84	eleq1d	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to \left({\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 ℝ\leftrightarrow {\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)$$
86	85	ralbidva	$$⊢\phi \to \left(\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 ℝ\leftrightarrow \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{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)$$
87	6 86	anbi12d	$$⊢\phi \to \left(\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)\leftrightarrow \left(\left(x\in B⟼D\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{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)\right)$$
88		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)$$
89		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)$$
90	88 89 1	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)$$
91		eqidd	$$⊢\phi \to \left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)=\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)$$
92		eqidd	$$⊢\left(\phi \wedge x\in B\right)\to \Re \left(\frac{D}{{\mathrm{i}}^k}\right)=\Re \left(\frac{D}{{\mathrm{i}}^k}\right)$$
93	91 92 2	isibl2	$$⊢\phi \to \left(\left(x\in B⟼D\right)\in {𝐿}^1\leftrightarrow \left(\left(x\in B⟼D\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{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)\in ℝ\right)\right)$$
94	87 90 93	3bitr4d	$$⊢\phi \to \left(\left(x\in B⟼C\right)\in {𝐿}^1\leftrightarrow \left(x\in B⟼D\right)\in {𝐿}^1\right)$$
95	84	oveq2d	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\mathrm{i}}^k{\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)={\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
96	95	sumeq2dv	$$⊢\phi \to \sum _{k=0}^3{\mathrm{i}}^k{\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)=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
97		eqid	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
98	97	dfitg	$$⊢{\int }_{B}Cdx=\sum _{k=0}^3{\mathrm{i}}^k{\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)$$
99		eqid	$$⊢\Re \left(\frac{D}{{\mathrm{i}}^k}\right)=\Re \left(\frac{D}{{\mathrm{i}}^k}\right)$$
100	99	dfitg	$$⊢{\int }_{B}Ddx=\sum _{k=0}^3{\mathrm{i}}^k{\int }^2\left(\left(x\in ℝ⟼if\left(\left(x\in B\wedge 0\le \Re \left(\frac{D}{{\mathrm{i}}^k}\right)\right),\Re \left(\frac{D}{{\mathrm{i}}^k}\right),0\right)\right)\right)$$
101	96 98 100	3eqtr4g	$$⊢\phi \to {\int }_{B}Cdx={\int }_{B}Ddx$$
102	94 101	jca	$$⊢\phi \to \left(\left(\left(x\in B⟼C\right)\in {𝐿}^1\leftrightarrow \left(x\in B⟼D\right)\in {𝐿}^1\right)\wedge {\int }_{B}Cdx={\int }_{B}Ddx\right)$$