Theorem itgsplit

Description: The S. integral splits under an almost disjoint union. (Contributed by Mario Carneiro, 11-Aug-2014)

	Ref	Expression
Hypotheses	itgsplit.i	$$⊢\phi \to {vol}^{*}\left(A\cap B\right)=0$$
	itgsplit.u	$$⊢\phi \to U=A\cup B$$
	itgsplit.c	$$⊢\left(\phi \wedge x\in U\right)\to C\in V$$
	itgsplit.a	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
	itgsplit.b	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$
Assertion	itgsplit	$$⊢\phi \to {\int }_{U}Cdx={\int }_{A}Cdx+{\int }_{B}Cdx$$

Proof

Step	Hyp	Ref	Expression
1		itgsplit.i	$$⊢\phi \to {vol}^{*}\left(A\cap B\right)=0$$
2		itgsplit.u	$$⊢\phi \to U=A\cup B$$
3		itgsplit.c	$$⊢\left(\phi \wedge x\in U\right)\to C\in V$$
4		itgsplit.a	$$⊢\phi \to \left(x\in A⟼C\right)\in {𝐿}^1$$
5		itgsplit.b	$$⊢\phi \to \left(x\in B⟼C\right)\in {𝐿}^1$$
6		iblmbf	$$⊢\left(x\in A⟼C\right)\in {𝐿}^1\to \left(x\in A⟼C\right)\in MblFn$$
7	4 6	syl	$$⊢\phi \to \left(x\in A⟼C\right)\in MblFn$$
8		ssun1	$$⊢A\subseteq A\cup B$$
9	8 2	sseqtrrid	$$⊢\phi \to A\subseteq U$$
10	9	sselda	$$⊢\left(\phi \wedge x\in A\right)\to x\in U$$
11	10 3	syldan	$$⊢\left(\phi \wedge x\in A\right)\to C\in V$$
12	7 11	mbfdm2	$$⊢\phi \to A\in \mathrm{dom}vol$$
13	12	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to A\in \mathrm{dom}vol$$
14		iblmbf	$$⊢\left(x\in B⟼C\right)\in {𝐿}^1\to \left(x\in B⟼C\right)\in MblFn$$
15	5 14	syl	$$⊢\phi \to \left(x\in B⟼C\right)\in MblFn$$
16		ssun2	$$⊢B\subseteq A\cup B$$
17	16 2	sseqtrrid	$$⊢\phi \to B\subseteq U$$
18	17	sselda	$$⊢\left(\phi \wedge x\in B\right)\to x\in U$$
19	18 3	syldan	$$⊢\left(\phi \wedge x\in B\right)\to C\in V$$
20	15 19	mbfdm2	$$⊢\phi \to B\in \mathrm{dom}vol$$
21	20	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to B\in \mathrm{dom}vol$$
22	1	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {vol}^{*}\left(A\cap B\right)=0$$
23	2	adantr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to U=A\cup B$$
24	2	eleq2d	$$⊢\phi \to \left(x\in U\leftrightarrow x\in \left(A\cup B\right)\right)$$
25		elun	$$⊢x\in \left(A\cup B\right)\leftrightarrow \left(x\in A\vee x\in B\right)$$
26	24 25	bitrdi	$$⊢\phi \to \left(x\in U\leftrightarrow \left(x\in A\vee x\in B\right)\right)$$
27	26	biimpa	$$⊢\left(\phi \wedge x\in U\right)\to \left(x\in A\vee x\in B\right)$$
28	7 11	mbfmptcl	$$⊢\left(\phi \wedge x\in A\right)\to C\in ℂ$$
29	15 19	mbfmptcl	$$⊢\left(\phi \wedge x\in B\right)\to C\in ℂ$$
30	28 29	jaodan	$$⊢\left(\phi \wedge \left(x\in A\vee x\in B\right)\right)\to C\in ℂ$$
31	27 30	syldan	$$⊢\left(\phi \wedge x\in U\right)\to C\in ℂ$$
32	31	adantlr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to C\in ℂ$$
33		ax-icn	$$⊢\mathrm{i}\in ℂ$$
34		elfznn0	$$⊢k\in \left(0\dots 3\right)\to k\in {\mathbb{N}}_0$$
35	34	adantl	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to k\in {\mathbb{N}}_0$$
36		expcl	$$⊢\left(\mathrm{i}\in ℂ\wedge k\in {\mathbb{N}}_0\right)\to {\mathrm{i}}^k\in ℂ$$
37	33 35 36	sylancr	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\mathrm{i}}^k\in ℂ$$
38	37	adantr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to {\mathrm{i}}^k\in ℂ$$
39		ine0	$$⊢\mathrm{i}\ne 0$$
40		elfzelz	$$⊢k\in \left(0\dots 3\right)\to k\in \mathbb{Z}$$
41	40	adantl	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to k\in \mathbb{Z}$$
42		expne0i	$$⊢\left(\mathrm{i}\in ℂ\wedge \mathrm{i}\ne 0\wedge k\in \mathbb{Z}\right)\to {\mathrm{i}}^k\ne 0$$
43	33 39 41 42	mp3an12i	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\mathrm{i}}^k\ne 0$$
44	43	adantr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\right)\to {\mathrm{i}}^k\ne 0$$
45	32 38 44	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 ℂ$$
46	45	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 ℝ$$
47		0re	$$⊢0\in ℝ$$
48		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 ℝ$$
49	46 47 48	sylancl	$$⊢\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 ℝ$$
50	49	rexrd	$$⊢\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 {ℝ}^{*}$$
51		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)$$
52	47 46 51	sylancr	$$⊢\left(\left(\phi \wedge k\in \left(0\dots 3\right)\right)\wedge x\in U\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)$$
53		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)$$
54	50 52 53	sylanbrc	$$⊢\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]$$
55		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)$$
56	55	mpteq2i	$$⊢\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(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)$$
57		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)$$
58	57	mpteq2i	$$⊢\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(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)$$
59		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)$$
60	59	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)$$
61		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)$$
62		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)$$
63	61 62 4 11	iblitg	$$⊢\left(\phi \wedge k\in \mathbb{Z}\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 ℝ$$
64	40 63	sylan2	$$⊢\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 ℝ$$
65		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)$$
66		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)$$
67	65 66 5 19	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 ℝ$$
68	40 67	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 ℝ$$
69	13 21 22 23 54 56 58 60 64 68	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(\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)+{\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)$$
70	69	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 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)={\mathrm{i}}^k\left({\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)+{\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)$$
71	63	recnd	$$⊢\left(\phi \wedge k\in \mathbb{Z}\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 ℂ$$
72	40 71	sylan2	$$⊢\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 ℂ$$
73	68	recnd	$$⊢\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 ℂ$$
74	37 72 73	adddid	$$⊢\left(\phi \wedge k\in \left(0\dots 3\right)\right)\to {\mathrm{i}}^k\left({\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)+{\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)={\mathrm{i}}^k{\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)+{\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)$$
75	70 74	eqtrd	$$⊢\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 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)={\mathrm{i}}^k{\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)+{\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)$$
76	75	sumeq2dv	$$⊢\phi \to \sum _{k=0}^3{\mathrm{i}}^k{\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)=\sum _{k=0}^3\left({\mathrm{i}}^k{\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)+{\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)\right)$$
77		fzfid	$$⊢\phi \to \left(0\dots 3\right)\in \mathrm{Fin}$$
78	37 72	mulcld	$$⊢\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 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 ℂ$$
79	37 73	mulcld	$$⊢\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)\in ℂ$$
80	77 78 79	fsumadd	$$⊢\phi \to \sum _{k=0}^3\left({\mathrm{i}}^k{\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)+{\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)\right)=\sum _{k=0}^3{\mathrm{i}}^k{\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)+\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)$$
81	76 80	eqtrd	$$⊢\phi \to \sum _{k=0}^3{\mathrm{i}}^k{\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)=\sum _{k=0}^3{\mathrm{i}}^k{\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)+\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)$$
82		eqid	$$⊢\Re \left(\frac{C}{{\mathrm{i}}^k}\right)=\Re \left(\frac{C}{{\mathrm{i}}^k}\right)$$
83	82	dfitg	$$⊢{\int }_{U}Cdx=\sum _{k=0}^3{\mathrm{i}}^k{\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)$$
84	82	dfitg	$$⊢{\int }_{A}Cdx=\sum _{k=0}^3{\mathrm{i}}^k{\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)$$
85	82	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)$$
86	84 85	oveq12i	$$⊢{\int }_{A}Cdx+{\int }_{B}Cdx=\sum _{k=0}^3{\mathrm{i}}^k{\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)+\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)$$
87	81 83 86	3eqtr4g	$$⊢\phi \to {\int }_{U}Cdx={\int }_{A}Cdx+{\int }_{B}Cdx$$