# Metamath Proof Explorer

## Theorem iblsplit

Description: The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iblsplit.1 ${⊢}{\phi }\to {vol}^{*}\left({A}\cap {B}\right)=0$
iblsplit.2 ${⊢}{\phi }\to {U}={A}\cup {B}$
iblsplit.3 ${⊢}\left({\phi }\wedge {x}\in {U}\right)\to {C}\in ℂ$
iblsplit.4 ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)\in {𝐿}^{1}$
iblsplit.5 ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)\in {𝐿}^{1}$
Assertion iblsplit ${⊢}{\phi }\to \left({x}\in {U}⟼{C}\right)\in {𝐿}^{1}$

### Proof

Step Hyp Ref Expression
1 iblsplit.1 ${⊢}{\phi }\to {vol}^{*}\left({A}\cap {B}\right)=0$
2 iblsplit.2 ${⊢}{\phi }\to {U}={A}\cup {B}$
3 iblsplit.3 ${⊢}\left({\phi }\wedge {x}\in {U}\right)\to {C}\in ℂ$
4 iblsplit.4 ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)\in {𝐿}^{1}$
5 iblsplit.5 ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)\in {𝐿}^{1}$
6 3 fmpttd ${⊢}{\phi }\to \left({x}\in {U}⟼{C}\right):{U}⟶ℂ$
7 ssun1 ${⊢}{A}\subseteq {A}\cup {B}$
8 7 2 sseqtrrid ${⊢}{\phi }\to {A}\subseteq {U}$
9 8 resmptd ${⊢}{\phi }\to {\left({x}\in {U}⟼{C}\right)↾}_{{A}}=\left({x}\in {A}⟼{C}\right)$
10 eqidd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right),0\right)\right)$
11 eqidd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)=\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)$
12 8 sseld ${⊢}{\phi }\to \left({x}\in {A}\to {x}\in {U}\right)$
13 12 imdistani ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left({\phi }\wedge {x}\in {U}\right)$
14 13 3 syl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {C}\in ℂ$
15 10 11 14 isibl2 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{C}\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼{C}\right)\in MblFn\wedge \forall {y}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right),0\right)\right)\right)\in ℝ\right)\right)$
16 4 15 mpbid ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{C}\right)\in MblFn\wedge \forall {y}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right),0\right)\right)\right)\in ℝ\right)$
17 16 simpld ${⊢}{\phi }\to \left({x}\in {A}⟼{C}\right)\in MblFn$
18 9 17 eqeltrd ${⊢}{\phi }\to {\left({x}\in {U}⟼{C}\right)↾}_{{A}}\in MblFn$
19 ssun2 ${⊢}{B}\subseteq {A}\cup {B}$
20 19 2 sseqtrrid ${⊢}{\phi }\to {B}\subseteq {U}$
21 20 resmptd ${⊢}{\phi }\to {\left({x}\in {U}⟼{C}\right)↾}_{{B}}=\left({x}\in {B}⟼{C}\right)$
22 eqidd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left(\left({x}\in {B}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {B}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right),0\right)\right)$
23 eqidd ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)=\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)$
24 20 sseld ${⊢}{\phi }\to \left({x}\in {B}\to {x}\in {U}\right)$
25 24 imdistani ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to \left({\phi }\wedge {x}\in {U}\right)$
26 25 3 syl ${⊢}\left({\phi }\wedge {x}\in {B}\right)\to {C}\in ℂ$
27 22 23 26 isibl2 ${⊢}{\phi }\to \left(\left({x}\in {B}⟼{C}\right)\in {𝐿}^{1}↔\left(\left({x}\in {B}⟼{C}\right)\in MblFn\wedge \forall {y}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {B}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right),0\right)\right)\right)\in ℝ\right)\right)$
28 5 27 mpbid ${⊢}{\phi }\to \left(\left({x}\in {B}⟼{C}\right)\in MblFn\wedge \forall {y}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {B}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right)\right),\Re \left(\frac{{C}}{{\mathrm{i}}^{{y}}}\right),0\right)\right)\right)\in ℝ\right)$
29 28 simpld ${⊢}{\phi }\to \left({x}\in {B}⟼{C}\right)\in MblFn$
30 21 29 eqeltrd ${⊢}{\phi }\to {\left({x}\in {U}⟼{C}\right)↾}_{{B}}\in MblFn$
31 2 eqcomd ${⊢}{\phi }\to {A}\cup {B}={U}$
32 6 18 30 31 mbfres2cn ${⊢}{\phi }\to \left({x}\in {U}⟼{C}\right)\in MblFn$
33 17 14 mbfdm2 ${⊢}{\phi }\to {A}\in \mathrm{dom}vol$
34 33 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to {A}\in \mathrm{dom}vol$
35 29 26 mbfdm2 ${⊢}{\phi }\to {B}\in \mathrm{dom}vol$
36 35 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to {B}\in \mathrm{dom}vol$
37 1 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to {vol}^{*}\left({A}\cap {B}\right)=0$
38 2 adantr ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to {U}={A}\cup {B}$
39 3 adantlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\to {C}\in ℂ$
40 ax-icn ${⊢}\mathrm{i}\in ℂ$
41 40 a1i ${⊢}{k}\in \left(0\dots 3\right)\to \mathrm{i}\in ℂ$
42 elfznn0 ${⊢}{k}\in \left(0\dots 3\right)\to {k}\in {ℕ}_{0}$
43 41 42 expcld ${⊢}{k}\in \left(0\dots 3\right)\to {\mathrm{i}}^{{k}}\in ℂ$
44 43 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\to {\mathrm{i}}^{{k}}\in ℂ$
45 40 a1i ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\to \mathrm{i}\in ℂ$
46 ine0 ${⊢}\mathrm{i}\ne 0$
47 46 a1i ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\to \mathrm{i}\ne 0$
48 elfzelz ${⊢}{k}\in \left(0\dots 3\right)\to {k}\in ℤ$
49 48 ad2antlr ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\to {k}\in ℤ$
50 45 47 49 expne0d ${⊢}\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\to {\mathrm{i}}^{{k}}\ne 0$
51 39 44 50 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 ℂ$
52 51 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 ℝ$
53 52 rexrd ${⊢}\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 {ℝ}^{*}$
54 53 adantr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)\to \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\in {ℝ}^{*}$
55 simpr ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)\to 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)$
56 pnfge ${⊢}\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\in {ℝ}^{*}\to \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\le \mathrm{+\infty }$
57 54 56 syl ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)\to \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\le \mathrm{+\infty }$
58 0xr ${⊢}0\in {ℝ}^{*}$
59 pnfxr ${⊢}\mathrm{+\infty }\in {ℝ}^{*}$
60 elicc1 ${⊢}\left(0\in {ℝ}^{*}\wedge \mathrm{+\infty }\in {ℝ}^{*}\right)\to \left(\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\in \left[0,\mathrm{+\infty }\right]↔\left(\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\in {ℝ}^{*}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\wedge \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\le \mathrm{+\infty }\right)\right)$
61 58 59 60 mp2an ${⊢}\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\in \left[0,\mathrm{+\infty }\right]↔\left(\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\in {ℝ}^{*}\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\wedge \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\le \mathrm{+\infty }\right)$
62 54 55 57 61 syl3anbrc ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\wedge 0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)\to \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\in \left[0,\mathrm{+\infty }\right]$
63 0e0iccpnf ${⊢}0\in \left[0,\mathrm{+\infty }\right]$
64 63 a1i ${⊢}\left(\left(\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\wedge {x}\in {U}\right)\wedge ¬0\le \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)\right)\to 0\in \left[0,\mathrm{+\infty }\right]$
65 62 64 ifclda ${⊢}\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]$
66 eqid ${⊢}\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)=\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)$
67 eqid ${⊢}\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)=\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)$
68 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)$
69 68 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)$
70 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)$
71 70 eqcomi ${⊢}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)=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)$
72 71 mpteq2i ${⊢}\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)=\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)$
73 72 a1i ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to \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)=\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)$
74 73 fveq2d ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to {\int }^{2}\left(\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)\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)$
75 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)$
76 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)$
77 75 76 14 isibl2 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{C}\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼{C}\right)\in MblFn\wedge \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\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)$
78 4 77 mpbid ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{C}\right)\in MblFn\wedge \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\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)$
79 78 simprd ${⊢}{\phi }\to \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\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 ℝ$
80 79 r19.21bi ${⊢}\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 ℝ$
81 74 80 eqeltrd ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to {\int }^{2}\left(\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)\right)\in ℝ$
82 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)$
83 82 eqcomi ${⊢}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(\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)$
84 83 mpteq2i ${⊢}\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)=\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)$
85 84 fveq2i ${⊢}{\int }^{2}\left(\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)\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)$
86 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)$
87 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)$
88 86 87 26 isibl2 ${⊢}{\phi }\to \left(\left({x}\in {B}⟼{C}\right)\in {𝐿}^{1}↔\left(\left({x}\in {B}⟼{C}\right)\in MblFn\wedge \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\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)$
89 5 88 mpbid ${⊢}{\phi }\to \left(\left({x}\in {B}⟼{C}\right)\in MblFn\wedge \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\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)$
90 89 simprd ${⊢}{\phi }\to \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\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 ℝ$
91 90 r19.21bi ${⊢}\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 ℝ$
92 85 91 eqeltrid ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to {\int }^{2}\left(\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)\right)\in ℝ$
93 34 36 37 38 65 66 67 69 81 92 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({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)\right)+{\int }^{2}\left(\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)\right)$
94 81 92 readdcld ${⊢}\left({\phi }\wedge {k}\in \left(0\dots 3\right)\right)\to {\int }^{2}\left(\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)\right)+{\int }^{2}\left(\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)\right)\in ℝ$
95 93 94 eqeltrd ${⊢}\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)\in ℝ$
96 95 ralrimiva ${⊢}{\phi }\to \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\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)\in ℝ$
97 eqidd ${⊢}{\phi }\to \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(\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)$
98 eqidd ${⊢}\left({\phi }\wedge {x}\in {U}\right)\to \Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)=\Re \left(\frac{{C}}{{\mathrm{i}}^{{k}}}\right)$
99 97 98 3 isibl2 ${⊢}{\phi }\to \left(\left({x}\in {U}⟼{C}\right)\in {𝐿}^{1}↔\left(\left({x}\in {U}⟼{C}\right)\in MblFn\wedge \forall {k}\in \left(0\dots 3\right)\phantom{\rule{.4em}{0ex}}{\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)\in ℝ\right)\right)$
100 32 96 99 mpbir2and ${⊢}{\phi }\to \left({x}\in {U}⟼{C}\right)\in {𝐿}^{1}$