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 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 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 )