# Metamath Proof Explorer

## Theorem iblcnlem

Description: Expand out the universal quantifier in isibl2 . (Contributed by Mario Carneiro, 6-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)$
itgcnlem.v ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
Assertion iblcnlem ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\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 itgcnlem.v ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
6 iblmbf ${⊢}\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}\to \left({x}\in {A}⟼{B}\right)\in MblFn$
7 6 a1i ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}\to \left({x}\in {A}⟼{B}\right)\in MblFn\right)$
8 simp1 ${⊢}\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)\to \left({x}\in {A}⟼{B}\right)\in MblFn$
9 8 a1i ${⊢}{\phi }\to \left(\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)\to \left({x}\in {A}⟼{B}\right)\in MblFn\right)$
10 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)$
11 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)$
12 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)$
13 eqid ${⊢}{\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)$
14 0cn ${⊢}0\in ℂ$
15 14 elimel ${⊢}if\left({B}\in ℂ,{B},0\right)\in ℂ$
16 15 a1i ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left({B}\in ℂ,{B},0\right)\in ℂ$
17 10 11 12 13 16 iblcnlem1 ${⊢}{\phi }\to \left(\left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)\in MblFn\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\right)\right)\right)$
18 17 adantr ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left(\left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)\in MblFn\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\right)\right)\right)$
19 eqid ${⊢}{A}={A}$
20 mbff ${⊢}\left({x}\in {A}⟼{B}\right)\in MblFn\to \left({x}\in {A}⟼{B}\right):\mathrm{dom}\left({x}\in {A}⟼{B}\right)⟶ℂ$
21 eqid ${⊢}\left({x}\in {A}⟼{B}\right)=\left({x}\in {A}⟼{B}\right)$
22 21 5 dmmptd ${⊢}{\phi }\to \mathrm{dom}\left({x}\in {A}⟼{B}\right)={A}$
23 22 feq2d ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right):\mathrm{dom}\left({x}\in {A}⟼{B}\right)⟶ℂ↔\left({x}\in {A}⟼{B}\right):{A}⟶ℂ\right)$
24 23 biimpa ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right):\mathrm{dom}\left({x}\in {A}⟼{B}\right)⟶ℂ\right)\to \left({x}\in {A}⟼{B}\right):{A}⟶ℂ$
25 20 24 sylan2 ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({x}\in {A}⟼{B}\right):{A}⟶ℂ$
26 21 fmpt ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ↔\left({x}\in {A}⟼{B}\right):{A}⟶ℂ$
27 25 26 sylibr ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ$
28 iftrue ${⊢}{B}\in ℂ\to if\left({B}\in ℂ,{B},0\right)={B}$
29 28 ralimi ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({B}\in ℂ,{B},0\right)={B}$
30 27 29 syl ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({B}\in ℂ,{B},0\right)={B}$
31 mpteq12 ${⊢}\left({A}={A}\wedge \forall {x}\in {A}\phantom{\rule{.4em}{0ex}}if\left({B}\in ℂ,{B},0\right)={B}\right)\to \left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)=\left({x}\in {A}⟼{B}\right)$
32 19 30 31 sylancr ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)=\left({x}\in {A}⟼{B}\right)$
33 32 eleq1d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left(\left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)\in {𝐿}^{1}↔\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}\right)$
34 32 eleq1d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left(\left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)\in MblFn↔\left({x}\in {A}⟼{B}\right)\in MblFn\right)$
35 eqid ${⊢}ℝ=ℝ$
36 28 imim2i ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to \left({x}\in {A}\to if\left({B}\in ℂ,{B},0\right)={B}\right)$
37 36 imp ${⊢}\left(\left({x}\in {A}\to {B}\in ℂ\right)\wedge {x}\in {A}\right)\to if\left({B}\in ℂ,{B},0\right)={B}$
38 37 fveq2d ${⊢}\left(\left({x}\in {A}\to {B}\in ℂ\right)\wedge {x}\in {A}\right)\to \Re \left(if\left({B}\in ℂ,{B},0\right)\right)=\Re \left({B}\right)$
39 38 ibllem ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)$
40 39 a1d ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to \left({x}\in ℝ\to if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)$
41 40 ralimi2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)$
42 27 41 syl ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)$
43 mpteq12 ${⊢}\left(ℝ=ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Re \left({B}\right)\right),\Re \left({B}\right),0\right)\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\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)$
44 35 42 43 sylancr ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\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)$
45 44 fveq2d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\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)$
46 45 1 eqtr4di ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={R}$
47 46 eleq1d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ↔{R}\in ℝ\right)$
48 38 negeqd ${⊢}\left(\left({x}\in {A}\to {B}\in ℂ\right)\wedge {x}\in {A}\right)\to -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)=-\Re \left({B}\right)$
49 48 ibllem ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)$
50 49 a1d ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to \left({x}\in ℝ\to if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)$
51 50 ralimi2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)$
52 27 51 syl ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)$
53 mpteq12 ${⊢}\left(ℝ=ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Re \left({B}\right)\right),-\Re \left({B}\right),0\right)\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\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)$
54 35 52 53 sylancr ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\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)$
55 54 fveq2d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\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)$
56 55 2 eqtr4di ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={S}$
57 56 eleq1d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ↔{S}\in ℝ\right)$
58 47 57 anbi12d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left(\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\right)↔\left({R}\in ℝ\wedge {S}\in ℝ\right)\right)$
59 37 fveq2d ${⊢}\left(\left({x}\in {A}\to {B}\in ℂ\right)\wedge {x}\in {A}\right)\to \Im \left(if\left({B}\in ℂ,{B},0\right)\right)=\Im \left({B}\right)$
60 59 ibllem ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)$
61 60 a1d ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to \left({x}\in ℝ\to if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)$
62 61 ralimi2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)$
63 27 62 syl ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)$
64 mpteq12 ${⊢}\left(ℝ=ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)$
65 35 63 64 sylancr ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left({B}\right)\right),\Im \left({B}\right),0\right)\right)$
66 65 fveq2d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={\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)$
67 66 3 eqtr4di ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={T}$
68 67 eleq1d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ↔{T}\in ℝ\right)$
69 59 negeqd ${⊢}\left(\left({x}\in {A}\to {B}\in ℂ\right)\wedge {x}\in {A}\right)\to -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)=-\Im \left({B}\right)$
70 69 ibllem ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)$
71 70 a1d ${⊢}\left({x}\in {A}\to {B}\in ℂ\right)\to \left({x}\in ℝ\to if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)$
72 71 ralimi2 ${⊢}\forall {x}\in {A}\phantom{\rule{.4em}{0ex}}{B}\in ℂ\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)$
73 27 72 syl ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)$
74 mpteq12 ${⊢}\left(ℝ=ℝ\wedge \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)=if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)$
75 35 73 74 sylancr ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)=\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left({B}\right)\right),-\Im \left({B}\right),0\right)\right)$
76 75 fveq2d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={\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)$
77 76 4 eqtr4di ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)={U}$
78 77 eleq1d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ↔{U}\in ℝ\right)$
79 68 78 anbi12d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left(\left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\right)↔\left({T}\in ℝ\wedge {U}\in ℝ\right)\right)$
80 34 58 79 3anbi123d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left(\left(\left({x}\in {A}⟼if\left({B}\in ℂ,{B},0\right)\right)\in MblFn\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Re \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Re \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\right)\wedge \left({\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le \Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left(\left({x}\in {A}\wedge 0\le -\Im \left(if\left({B}\in ℂ,{B},0\right)\right)\right),-\Im \left(if\left({B}\in ℂ,{B},0\right)\right),0\right)\right)\right)\in ℝ\right)\right)↔\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)$
81 18 33 80 3bitr3d ${⊢}\left({\phi }\wedge \left({x}\in {A}⟼{B}\right)\in MblFn\right)\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\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)$
82 81 ex ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in MblFn\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\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)\right)$
83 7 9 82 pm5.21ndd ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\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)$