Metamath Proof Explorer

Theorem iblmulc2nc

Description: Choice-free analogue of iblmulc2 . (Contributed by Brendan Leahy, 17-Nov-2017)

Ref Expression
Hypotheses itgmulc2nc.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
itgmulc2nc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
itgmulc2nc.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
itgmulc2nc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )
Assertion iblmulc2nc ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 )

Proof

Step Hyp Ref Expression
1 itgmulc2nc.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 itgmulc2nc.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 itgmulc2nc.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
4 itgmulc2nc.m ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )
5 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
6 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
7 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
8 3 7 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
9 8 2 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
10 6 9 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
11 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
12 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
13 12 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑘 ∈ ℤ )
14 ax-icn ⊢ i ∈ ℂ
15 ine0 ⊢ i ≠ 0
16 expclz ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ )
17 14 15 16 mp3an12 ⊢ ( 𝑘 ∈ ℤ → ( i ↑ 𝑘 ) ∈ ℂ )
18 13 17 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( i ↑ 𝑘 ) ∈ ℂ )
19 expne0i ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
20 14 15 19 mp3an12 ⊢ ( 𝑘 ∈ ℤ → ( i ↑ 𝑘 ) ≠ 0 )
21 13 20 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( i ↑ 𝑘 ) ≠ 0 )
22 11 18 21 divcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ∈ ℂ )
23 22 recld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ∈ ℝ )
24 0re ⊢ 0 ∈ ℝ
25 ifcl ⊢ ( ( ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
26 23 24 25 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
27 26 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* )
28 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
29 24 23 28 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
30 elxrge0 ⊢ ( if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) ↔ ( if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* ∧ 0 ≤ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
31 27 29 30 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
32 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
33 32 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
34 31 33 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
35 34 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
36 5 35 eqeltrid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
37 36 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
38 9 recld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℝ )
39 38 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ 𝐵 ) ∈ ℂ )
40 39 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ℜ ‘ 𝐵 ) ) ∈ ℝ )
41 9 imcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℝ )
42 41 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℑ ‘ 𝐵 ) ∈ ℂ )
43 42 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ℑ ‘ 𝐵 ) ) ∈ ℝ )
44 40 43 readdcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ∈ ℝ )
45 39 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( abs ‘ ( ℜ ‘ 𝐵 ) ) )
46 42 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( abs ‘ ( ℑ ‘ 𝐵 ) ) )
47 40 43 45 46 addge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) )
48 elrege0 ⊢ ( ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ∈ ℝ ∧ 0 ≤ ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
49 44 47 48 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ∈ ( 0 [,) +∞ ) )
50 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
51 50 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
52 49 51 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
53 52 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
54 53 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
55 reex ⊢ ℝ ∈ V
56 55 a1i ⊢ ( 𝜑 → ℝ ∈ V )
57 elrege0 ⊢ ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℜ ‘ 𝐵 ) ) ) )
58 40 45 57 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ℜ ‘ 𝐵 ) ) ∈ ( 0 [,) +∞ ) )
59 58 51 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
60 59 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
61 elrege0 ⊢ ( ( abs ‘ ( ℑ ‘ 𝐵 ) ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ ( ℑ ‘ 𝐵 ) ) ∈ ℝ ∧ 0 ≤ ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) )
62 43 46 61 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ℑ ‘ 𝐵 ) ) ∈ ( 0 [,) +∞ ) )
63 62 51 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
64 63 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ∈ ( 0 [,) +∞ ) )
65 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) )
66 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) )
67 56 60 64 65 66 offval2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) + if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) )
68 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) = ( abs ‘ ( ℜ ‘ 𝐵 ) ) )
69 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) = ( abs ‘ ( ℑ ‘ 𝐵 ) ) )
70 68 69 oveq12d ⊢ ( 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) + if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) = ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) )
71 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) = ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) )
72 70 71 eqtr4d ⊢ ( 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) + if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) )
73 00id ⊢ ( 0 + 0 ) = 0
74 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) = 0 )
75 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) = 0 )
76 74 75 oveq12d ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) + if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) = ( 0 + 0 ) )
77 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) = 0 )
78 73 76 77 3eqtr4a ⊢ ( ¬ 𝑥 ∈ 𝐴 → ( if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) + if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) )
79 72 78 pm2.61i ⊢ ( if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) + if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 )
80 79 mpteq2i ⊢ ( 𝑥 ∈ ℝ ↦ ( if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) + if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) )
81 67 80 eqtr2di ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) = ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) )
82 81 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) = ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ) )
83 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) )
84 9 iblcn ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) ) )
85 3 84 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 ∧ ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 ) )
86 85 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℜ ‘ 𝐵 ) ) ∈ 𝐿1 )
87 2 3 83 86 38 iblabsnclem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ) ∈ ℝ ) )
88 87 simpld ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ∈ MblFn )
89 60 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
90 87 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ) ∈ ℝ )
91 64 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
92 eqid ⊢ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) )
93 85 simprd ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( ℑ ‘ 𝐵 ) ) ∈ 𝐿1 )
94 2 3 92 93 41 iblabsnclem ⊢ ( 𝜑 → ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ∈ ℝ ) )
95 94 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ∈ ℝ )
96 88 89 90 91 95 itg2addnc ⊢ ( 𝜑 → ( ∫2 ‘ ( ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ∘f + ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ) )
97 82 96 eqtrd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) = ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ) )
98 90 95 readdcld ⊢ ( 𝜑 → ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ) ∈ ℝ )
99 97 98 eqeltrd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) ∈ ℝ )
100 1 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
101 1 absge0d ⊢ ( 𝜑 → 0 ≤ ( abs ‘ 𝐶 ) )
102 elrege0 ⊢ ( ( abs ‘ 𝐶 ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ 𝐶 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐶 ) ) )
103 100 101 102 sylanbrc ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ( 0 [,) +∞ ) )
104 54 99 103 itg2mulc ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { ( abs ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) ) = ( ( abs ‘ 𝐶 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) ) )
105 100 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( abs ‘ 𝐶 ) ∈ ℝ )
106 fconstmpt ⊢ ( ℝ × { ( abs ‘ 𝐶 ) } ) = ( 𝑥 ∈ ℝ ↦ ( abs ‘ 𝐶 ) )
107 106 a1i ⊢ ( 𝜑 → ( ℝ × { ( abs ‘ 𝐶 ) } ) = ( 𝑥 ∈ ℝ ↦ ( abs ‘ 𝐶 ) ) )
108 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) )
109 56 105 53 107 108 offval2 ⊢ ( 𝜑 → ( ( ℝ × { ( abs ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) )
110 71 oveq2d ⊢ ( 𝑥 ∈ 𝐴 → ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) = ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
111 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) = ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
112 110 111 eqtr4d ⊢ ( 𝑥 ∈ 𝐴 → ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
113 112 adantl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
114 100 recnd ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℂ )
115 114 mul01d ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) · 0 ) = 0 )
116 115 adantr ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · 0 ) = 0 )
117 77 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) = 0 )
118 117 oveq2d ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) = ( ( abs ‘ 𝐶 ) · 0 ) )
119 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) = 0 )
120 119 adantl ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) = 0 )
121 116 118 120 3eqtr4d ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
122 113 121 pm2.61dan ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
123 122 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) )
124 109 123 eqtrd ⊢ ( 𝜑 → ( ( ℝ × { ( abs ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) )
125 124 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { ( abs ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) )
126 97 oveq2d ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) , 0 ) ) ) ) = ( ( abs ‘ 𝐶 ) · ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ) ) )
127 104 125 126 3eqtr3d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) = ( ( abs ‘ 𝐶 ) · ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ) ) )
128 100 98 remulcld ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) · ( ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℜ ‘ 𝐵 ) ) , 0 ) ) ) + ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( ℑ ‘ 𝐵 ) ) , 0 ) ) ) ) ) ∈ ℝ )
129 127 128 eqeltrd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) ∈ ℝ )
130 129 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) ∈ ℝ )
131 100 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐶 ) ∈ ℝ )
132 131 44 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ∈ ℝ )
133 132 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ∈ ℝ* )
134 101 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( abs ‘ 𝐶 ) )
135 131 44 134 47 mulge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
136 elxrge0 ⊢ ( ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ∈ ℝ* ∧ 0 ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ) )
137 133 135 136 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ∈ ( 0 [,] +∞ ) )
138 32 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
139 137 138 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
140 139 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
141 140 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
142 9 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
143 131 142 remulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) ∈ ℝ )
144 143 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) ∈ ℝ )
145 132 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ∈ ℝ )
146 22 releabsd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) )
147 11 18 21 absdivd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / ( abs ‘ ( i ↑ 𝑘 ) ) ) )
148 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℕ0 )
149 absexp ⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = ( ( abs ‘ i ) ↑ 𝑘 ) )
150 14 148 149 sylancr ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = ( ( abs ‘ i ) ↑ 𝑘 ) )
151 absi ⊢ ( abs ‘ i ) = 1
152 151 oveq1i ⊢ ( ( abs ‘ i ) ↑ 𝑘 ) = ( 1 ↑ 𝑘 )
153 1exp ⊢ ( 𝑘 ∈ ℤ → ( 1 ↑ 𝑘 ) = 1 )
154 12 153 syl ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( 1 ↑ 𝑘 ) = 1 )
155 152 154 syl5eq ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( abs ‘ i ) ↑ 𝑘 ) = 1 )
156 150 155 eqtrd ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = 1 )
157 156 oveq2d ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / ( abs ‘ ( i ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / 1 ) )
158 157 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / ( abs ‘ ( i ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / 1 ) )
159 10 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℝ )
160 159 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℂ )
161 160 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℂ )
162 161 div1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / 1 ) = ( abs ‘ ( 𝐶 · 𝐵 ) ) )
163 147 158 162 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = ( abs ‘ ( 𝐶 · 𝐵 ) ) )
164 6 9 absmuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) = ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) )
165 164 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) = ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) )
166 163 165 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) )
167 146 166 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) )
168 mulcl ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐵 ) ∈ ℂ ) → ( i · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
169 14 42 168 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( i · ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
170 39 169 abstrid ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) ) ≤ ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
171 9 replimd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 = ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) )
172 171 fveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) = ( abs ‘ ( ( ℜ ‘ 𝐵 ) + ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
173 absmul ⊢ ( ( i ∈ ℂ ∧ ( ℑ ‘ 𝐵 ) ∈ ℂ ) → ( abs ‘ ( i · ( ℑ ‘ 𝐵 ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) )
174 14 42 173 sylancr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( i · ( ℑ ‘ 𝐵 ) ) ) = ( ( abs ‘ i ) · ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) )
175 151 oveq1i ⊢ ( ( abs ‘ i ) · ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) = ( 1 · ( abs ‘ ( ℑ ‘ 𝐵 ) ) )
176 174 175 eqtrdi ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( i · ( ℑ ‘ 𝐵 ) ) ) = ( 1 · ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) )
177 43 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ℑ ‘ 𝐵 ) ) ∈ ℂ )
178 177 mulid2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 1 · ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) = ( abs ‘ ( ℑ ‘ 𝐵 ) ) )
179 176 178 eqtr2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ℑ ‘ 𝐵 ) ) = ( abs ‘ ( i · ( ℑ ‘ 𝐵 ) ) ) )
180 179 oveq2d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) = ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( i · ( ℑ ‘ 𝐵 ) ) ) ) )
181 170 172 180 3brtr4d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ≤ ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) )
182 142 44 131 134 181 lemul2ad ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
183 182 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
184 23 144 145 167 183 letrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
185 135 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
186 breq1 ⊢ ( ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) → ( ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ↔ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ) )
187 breq1 ⊢ ( 0 = if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) → ( 0 ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ↔ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ) )
188 186 187 ifboth ⊢ ( ( ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ∧ 0 ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
189 184 185 188 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
190 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
191 190 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
192 111 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) = ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) )
193 189 191 192 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
194 193 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) )
195 0le0 ⊢ 0 ≤ 0
196 195 a1i ⊢ ( ¬ 𝑥 ∈ 𝐴 → 0 ≤ 0 )
197 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
198 196 197 119 3brtr4d ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
199 194 198 pm2.61d1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
200 5 199 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
201 200 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) )
202 55 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ℝ ∈ V )
203 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
204 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) )
205 202 36 140 203 204 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) )
206 201 205 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) )
207 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) )
208 37 141 206 207 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) )
209 itg2lecl ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( ( abs ‘ ( ℜ ‘ 𝐵 ) ) + ( abs ‘ ( ℑ ‘ 𝐵 ) ) ) ) , 0 ) ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
210 37 130 208 209 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
211 210 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
212 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
213 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) )
214 212 213 10 isibl2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
215 4 211 214 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 )