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 mullidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 · ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) = ( abs ‘ ( ℑ ‘ 𝐵 ) ) )
96 93 95 eqtrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( 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 )