Metamath Proof Explorer

Theorem iblabsnc

Description: Choice-free analogue of iblabs . As with ibladdnc , a measurability hypothesis is needed. (Contributed by Brendan Leahy, 7-Nov-2017)

Ref Expression
Hypotheses iblabsnc.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
iblabsnc.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
iblabsnc.m ${⊢}{\phi }\to \left({x}\in {A}⟼\left|{B}\right|\right)\in MblFn$
Assertion iblabsnc ${⊢}{\phi }\to \left({x}\in {A}⟼\left|{B}\right|\right)\in {𝐿}^{1}$

Proof

Step Hyp Ref Expression
1 iblabsnc.1 ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in {V}$
2 iblabsnc.2 ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}$
3 iblabsnc.m ${⊢}{\phi }\to \left({x}\in {A}⟼\left|{B}\right|\right)\in MblFn$
4 iblmbf ${⊢}\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}\to \left({x}\in {A}⟼{B}\right)\in MblFn$
5 2 4 syl ${⊢}{\phi }\to \left({x}\in {A}⟼{B}\right)\in MblFn$
6 5 1 mbfmptcl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}\in ℂ$
7 6 abscld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|{B}\right|\in ℝ$
8 7 rexrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|{B}\right|\in {ℝ}^{*}$
9 6 absge0d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le \left|{B}\right|$
10 elxrge0 ${⊢}\left|{B}\right|\in \left[0,\mathrm{+\infty }\right]↔\left(\left|{B}\right|\in {ℝ}^{*}\wedge 0\le \left|{B}\right|\right)$
11 8 9 10 sylanbrc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|{B}\right|\in \left[0,\mathrm{+\infty }\right]$
12 0e0iccpnf ${⊢}0\in \left[0,\mathrm{+\infty }\right]$
13 12 a1i ${⊢}\left({\phi }\wedge ¬{x}\in {A}\right)\to 0\in \left[0,\mathrm{+\infty }\right]$
14 11 13 ifclda ${⊢}{\phi }\to if\left({x}\in {A},\left|{B}\right|,0\right)\in \left[0,\mathrm{+\infty }\right]$
15 14 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to if\left({x}\in {A},\left|{B}\right|,0\right)\in \left[0,\mathrm{+\infty }\right]$
16 15 fmpttd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]$
17 reex ${⊢}ℝ\in \mathrm{V}$
18 17 a1i ${⊢}{\phi }\to ℝ\in \mathrm{V}$
19 6 recld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Re \left({B}\right)\in ℝ$
20 19 recnd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Re \left({B}\right)\in ℂ$
21 20 abscld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Re \left({B}\right)\right|\in ℝ$
22 20 absge0d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le \left|\Re \left({B}\right)\right|$
23 elrege0 ${⊢}\left|\Re \left({B}\right)\right|\in \left[0,\mathrm{+\infty }\right)↔\left(\left|\Re \left({B}\right)\right|\in ℝ\wedge 0\le \left|\Re \left({B}\right)\right|\right)$
24 21 22 23 sylanbrc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Re \left({B}\right)\right|\in \left[0,\mathrm{+\infty }\right)$
25 0e0icopnf ${⊢}0\in \left[0,\mathrm{+\infty }\right)$
26 25 a1i ${⊢}\left({\phi }\wedge ¬{x}\in {A}\right)\to 0\in \left[0,\mathrm{+\infty }\right)$
27 24 26 ifclda ${⊢}{\phi }\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\in \left[0,\mathrm{+\infty }\right)$
28 27 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\in \left[0,\mathrm{+\infty }\right)$
29 6 imcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Im \left({B}\right)\in ℝ$
30 29 recnd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \Im \left({B}\right)\in ℂ$
31 30 abscld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Im \left({B}\right)\right|\in ℝ$
32 30 absge0d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le \left|\Im \left({B}\right)\right|$
33 elrege0 ${⊢}\left|\Im \left({B}\right)\right|\in \left[0,\mathrm{+\infty }\right)↔\left(\left|\Im \left({B}\right)\right|\in ℝ\wedge 0\le \left|\Im \left({B}\right)\right|\right)$
34 31 32 33 sylanbrc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Im \left({B}\right)\right|\in \left[0,\mathrm{+\infty }\right)$
35 34 26 ifclda ${⊢}{\phi }\to if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\in \left[0,\mathrm{+\infty }\right)$
36 35 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\in \left[0,\mathrm{+\infty }\right)$
37 eqidd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)$
38 eqidd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)$
39 18 28 36 37 38 offval2 ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right){+}_{f}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)+if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)$
40 iftrue ${⊢}{x}\in {A}\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)=\left|\Re \left({B}\right)\right|$
41 iftrue ${⊢}{x}\in {A}\to if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)=\left|\Im \left({B}\right)\right|$
42 40 41 oveq12d ${⊢}{x}\in {A}\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)+if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)=\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|$
43 iftrue ${⊢}{x}\in {A}\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)=\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|$
44 42 43 eqtr4d ${⊢}{x}\in {A}\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)+if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)=if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)$
45 00id ${⊢}0+0=0$
46 iffalse ${⊢}¬{x}\in {A}\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)=0$
47 iffalse ${⊢}¬{x}\in {A}\to if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)=0$
48 46 47 oveq12d ${⊢}¬{x}\in {A}\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)+if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)=0+0$
49 iffalse ${⊢}¬{x}\in {A}\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)=0$
50 45 48 49 3eqtr4a ${⊢}¬{x}\in {A}\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)+if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)=if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)$
51 44 50 pm2.61i ${⊢}if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)+if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)=if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)$
52 51 mpteq2i ${⊢}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)+if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)$
53 39 52 eqtr2di ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right){+}_{f}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)$
54 53 fveq2d ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right){+}_{f}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)\right)$
55 eqid ${⊢}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)$
56 6 iblcn ${⊢}{\phi }\to \left(\left({x}\in {A}⟼{B}\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼\Re \left({B}\right)\right)\in {𝐿}^{1}\wedge \left({x}\in {A}⟼\Im \left({B}\right)\right)\in {𝐿}^{1}\right)\right)$
57 2 56 mpbid ${⊢}{\phi }\to \left(\left({x}\in {A}⟼\Re \left({B}\right)\right)\in {𝐿}^{1}\wedge \left({x}\in {A}⟼\Im \left({B}\right)\right)\in {𝐿}^{1}\right)$
58 57 simpld ${⊢}{\phi }\to \left({x}\in {A}⟼\Re \left({B}\right)\right)\in {𝐿}^{1}$
59 1 2 55 58 19 iblabsnclem ${⊢}{\phi }\to \left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)\right)\in ℝ\right)$
60 59 simpld ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)\in MblFn$
61 28 fmpttd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$
62 59 simprd ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)\right)\in ℝ$
63 36 fmpttd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right)$
64 eqid ${⊢}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)$
65 57 simprd ${⊢}{\phi }\to \left({x}\in {A}⟼\Im \left({B}\right)\right)\in {𝐿}^{1}$
66 1 2 64 65 29 iblabsnclem ${⊢}{\phi }\to \left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)\right)\in ℝ\right)$
67 66 simprd ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)\right)\in ℝ$
68 60 61 62 63 67 itg2addnc ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right){+}_{f}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)\right)+{\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)\right)$
69 54 68 eqtrd ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)\right)={\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)\right)+{\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)\right)$
70 62 67 readdcld ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|,0\right)\right)\right)+{\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Im \left({B}\right)\right|,0\right)\right)\right)\in ℝ$
71 69 70 eqeltrd ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)\right)\in ℝ$
72 21 31 readdcld ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|\in ℝ$
73 72 rexrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|\in {ℝ}^{*}$
74 21 31 22 32 addge0d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 0\le \left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|$
75 elxrge0 ${⊢}\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|\in \left[0,\mathrm{+\infty }\right]↔\left(\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|\in {ℝ}^{*}\wedge 0\le \left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|\right)$
76 73 74 75 sylanbrc ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|\in \left[0,\mathrm{+\infty }\right]$
77 76 13 ifclda ${⊢}{\phi }\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\in \left[0,\mathrm{+\infty }\right]$
78 77 adantr ${⊢}\left({\phi }\wedge {x}\in ℝ\right)\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\in \left[0,\mathrm{+\infty }\right]$
79 78 fmpttd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]$
80 ax-icn ${⊢}\mathrm{i}\in ℂ$
81 mulcl ${⊢}\left(\mathrm{i}\in ℂ\wedge \Im \left({B}\right)\in ℂ\right)\to \mathrm{i}\Im \left({B}\right)\in ℂ$
82 80 30 81 sylancr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \mathrm{i}\Im \left({B}\right)\in ℂ$
83 20 82 abstrid ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Re \left({B}\right)+\mathrm{i}\Im \left({B}\right)\right|\le \left|\Re \left({B}\right)\right|+\left|\mathrm{i}\Im \left({B}\right)\right|$
84 iftrue ${⊢}{x}\in {A}\to if\left({x}\in {A},\left|{B}\right|,0\right)=\left|{B}\right|$
85 84 adantl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left({x}\in {A},\left|{B}\right|,0\right)=\left|{B}\right|$
86 6 replimd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to {B}=\Re \left({B}\right)+\mathrm{i}\Im \left({B}\right)$
87 86 fveq2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|{B}\right|=\left|\Re \left({B}\right)+\mathrm{i}\Im \left({B}\right)\right|$
88 85 87 eqtrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left({x}\in {A},\left|{B}\right|,0\right)=\left|\Re \left({B}\right)+\mathrm{i}\Im \left({B}\right)\right|$
89 43 adantl ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)=\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|$
90 absmul ${⊢}\left(\mathrm{i}\in ℂ\wedge \Im \left({B}\right)\in ℂ\right)\to \left|\mathrm{i}\Im \left({B}\right)\right|=\left|\mathrm{i}\right|\left|\Im \left({B}\right)\right|$
91 80 30 90 sylancr ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\mathrm{i}\Im \left({B}\right)\right|=\left|\mathrm{i}\right|\left|\Im \left({B}\right)\right|$
92 absi ${⊢}\left|\mathrm{i}\right|=1$
93 92 oveq1i ${⊢}\left|\mathrm{i}\right|\left|\Im \left({B}\right)\right|=1\left|\Im \left({B}\right)\right|$
94 31 recnd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Im \left({B}\right)\right|\in ℂ$
95 94 mulid2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to 1\left|\Im \left({B}\right)\right|=\left|\Im \left({B}\right)\right|$
96 93 95 syl5eq ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\mathrm{i}\right|\left|\Im \left({B}\right)\right|=\left|\Im \left({B}\right)\right|$
97 91 96 eqtr2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Im \left({B}\right)\right|=\left|\mathrm{i}\Im \left({B}\right)\right|$
98 97 oveq2d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to \left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|=\left|\Re \left({B}\right)\right|+\left|\mathrm{i}\Im \left({B}\right)\right|$
99 89 98 eqtrd ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)=\left|\Re \left({B}\right)\right|+\left|\mathrm{i}\Im \left({B}\right)\right|$
100 83 88 99 3brtr4d ${⊢}\left({\phi }\wedge {x}\in {A}\right)\to if\left({x}\in {A},\left|{B}\right|,0\right)\le if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)$
101 100 ex ${⊢}{\phi }\to \left({x}\in {A}\to if\left({x}\in {A},\left|{B}\right|,0\right)\le if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)$
102 0le0 ${⊢}0\le 0$
103 102 a1i ${⊢}¬{x}\in {A}\to 0\le 0$
104 iffalse ${⊢}¬{x}\in {A}\to if\left({x}\in {A},\left|{B}\right|,0\right)=0$
105 103 104 49 3brtr4d ${⊢}¬{x}\in {A}\to if\left({x}\in {A},\left|{B}\right|,0\right)\le if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)$
106 101 105 pm2.61d1 ${⊢}{\phi }\to if\left({x}\in {A},\left|{B}\right|,0\right)\le if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)$
107 106 ralrimivw ${⊢}{\phi }\to \forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left({x}\in {A},\left|{B}\right|,0\right)\le if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)$
108 eqidd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right)$
109 eqidd ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)=\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)$
110 18 15 78 108 109 ofrfval2 ${⊢}{\phi }\to \left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right){\le }_{f}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)↔\forall {x}\in ℝ\phantom{\rule{.4em}{0ex}}if\left({x}\in {A},\left|{B}\right|,0\right)\le if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)$
111 107 110 mpbird ${⊢}{\phi }\to \left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right){\le }_{f}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)$
112 itg2le ${⊢}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge \left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge \left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right){\le }_{f}\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right)\right)\le {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)\right)$
113 16 79 111 112 syl3anc ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right)\right)\le {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)\right)$
114 itg2lecl ${⊢}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right):ℝ⟶\left[0,\mathrm{+\infty }\right]\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)\right)\in ℝ\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right)\right)\le {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|\Re \left({B}\right)\right|+\left|\Im \left({B}\right)\right|,0\right)\right)\right)\right)\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right)\right)\in ℝ$
115 16 71 113 114 syl3anc ${⊢}{\phi }\to {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right)\right)\in ℝ$
116 7 9 iblpos ${⊢}{\phi }\to \left(\left({x}\in {A}⟼\left|{B}\right|\right)\in {𝐿}^{1}↔\left(\left({x}\in {A}⟼\left|{B}\right|\right)\in MblFn\wedge {\int }^{2}\left(\left({x}\in ℝ⟼if\left({x}\in {A},\left|{B}\right|,0\right)\right)\right)\in ℝ\right)\right)$
117 3 115 116 mpbir2and ${⊢}{\phi }\to \left({x}\in {A}⟼\left|{B}\right|\right)\in {𝐿}^{1}$