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 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
iblabsnc.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )
iblabsnc.m ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn )
Assertion iblabsnc ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )

Proof

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