Metamath Proof Explorer


Theorem iblabs

Description: The absolute value of an integrable function is integrable. (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses iblabs.1 ( ( 𝜑𝑥𝐴 ) → 𝐵𝑉 )
iblabs.2 ( 𝜑 → ( 𝑥𝐴𝐵 ) ∈ 𝐿1 )
Assertion iblabs ( 𝜑 → ( 𝑥𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )

Proof

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