This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem iblmulc2

Description: Multiply an integral by a constant. (Contributed by Mario Carneiro, 25-Aug-2014)

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

Proof

Step Hyp Ref Expression
1 itgmulc2.1 ⊢ ( 𝜑 → 𝐶 ∈ ℂ )
2 itgmulc2.2 ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ 𝑉 )
3 itgmulc2.3 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 )
4 iblmbf ⊢ ( ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ 𝐿1 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
5 3 4 syl ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ 𝐵 ) ∈ MblFn )
6 1 2 5 mbfmulc2 ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn )
7 ifan ⊢ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) = if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 )
8 1 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐶 ∈ ℂ )
9 5 2 mbfmptcl ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 𝐵 ∈ ℂ )
10 8 9 mulcld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
11 10 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 𝐶 · 𝐵 ) ∈ ℂ )
12 ax-icn ⊢ i ∈ ℂ
13 ine0 ⊢ i ≠ 0
14 elfzelz ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℤ )
15 14 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑘 ∈ ℤ )
16 expclz ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ∈ ℂ )
17 12 13 15 16 mp3an12i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( i ↑ 𝑘 ) ∈ ℂ )
18 expne0i ⊢ ( ( i ∈ ℂ ∧ i ≠ 0 ∧ 𝑘 ∈ ℤ ) → ( i ↑ 𝑘 ) ≠ 0 )
19 12 13 15 18 mp3an12i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( i ↑ 𝑘 ) ≠ 0 )
20 11 17 19 divcld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ∈ ℂ )
21 20 recld ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ∈ ℝ )
22 0re ⊢ 0 ∈ ℝ
23 ifcl ⊢ ( ( ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ∈ ℝ ∧ 0 ∈ ℝ ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
24 21 22 23 sylancl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ )
25 24 rexrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* )
26 max1 ⊢ ( ( 0 ∈ ℝ ∧ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ∈ ℝ ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
27 22 21 26 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
28 elxrge0 ⊢ ( if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) ↔ ( if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ℝ* ∧ 0 ≤ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
29 25 27 28 sylanbrc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
30 0e0iccpnf ⊢ 0 ∈ ( 0 [,] +∞ )
31 30 a1i ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
32 29 31 ifclda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
33 32 adantr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ∈ ( 0 [,] +∞ ) )
34 7 33 eqeltrid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
35 34 fmpttd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
36 reex ⊢ ℝ ∈ V
37 36 a1i ⊢ ( 𝜑 → ℝ ∈ V )
38 1 abscld ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℝ )
39 38 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → ( abs ‘ 𝐶 ) ∈ ℝ )
40 9 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ℝ )
41 9 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( abs ‘ 𝐵 ) )
42 elrege0 ⊢ ( ( abs ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ 𝐵 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐵 ) ) )
43 40 41 42 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ 𝐵 ) ∈ ( 0 [,) +∞ ) )
44 0e0icopnf ⊢ 0 ∈ ( 0 [,) +∞ )
45 44 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,) +∞ ) )
46 43 45 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
47 46 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ∈ ( 0 [,) +∞ ) )
48 fconstmpt ⊢ ( ℝ × { ( abs ‘ 𝐶 ) } ) = ( 𝑥 ∈ ℝ ↦ ( abs ‘ 𝐶 ) )
49 48 a1i ⊢ ( 𝜑 → ( ℝ × { ( abs ‘ 𝐶 ) } ) = ( 𝑥 ∈ ℝ ↦ ( abs ‘ 𝐶 ) ) )
50 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) )
51 37 39 47 49 50 offval2 ⊢ ( 𝜑 → ( ( ℝ × { ( abs ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) )
52 ovif2 ⊢ ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) , ( ( abs ‘ 𝐶 ) · 0 ) )
53 8 9 absmuld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) = ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) )
54 53 ifeq1da ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , ( ( abs ‘ 𝐶 ) · 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) , ( ( abs ‘ 𝐶 ) · 0 ) ) )
55 38 recnd ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ℂ )
56 55 mul01d ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) · 0 ) = 0 )
57 56 ifeq2d ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , ( ( abs ‘ 𝐶 ) · 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) )
58 54 57 eqtr3d ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( ( abs ‘ 𝐶 ) · ( abs ‘ 𝐵 ) ) , ( ( abs ‘ 𝐶 ) · 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) )
59 52 58 eqtrid ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) = if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) )
60 59 mpteq2dv ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ ( ( abs ‘ 𝐶 ) · if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) )
61 51 60 eqtrd ⊢ ( 𝜑 → ( ( ℝ × { ( abs ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) )
62 61 fveq2d ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { ( abs ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ) = ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) )
63 47 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) : ℝ ⟶ ( 0 [,) +∞ ) )
64 2 3 iblabs ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 )
65 40 41 iblpos ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) ) )
66 64 65 mpbid ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( abs ‘ 𝐵 ) ) ∈ MblFn ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ ) )
67 66 simprd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ∈ ℝ )
68 abscl ⊢ ( 𝐶 ∈ ℂ → ( abs ‘ 𝐶 ) ∈ ℝ )
69 absge0 ⊢ ( 𝐶 ∈ ℂ → 0 ≤ ( abs ‘ 𝐶 ) )
70 elrege0 ⊢ ( ( abs ‘ 𝐶 ) ∈ ( 0 [,) +∞ ) ↔ ( ( abs ‘ 𝐶 ) ∈ ℝ ∧ 0 ≤ ( abs ‘ 𝐶 ) ) )
71 68 69 70 sylanbrc ⊢ ( 𝐶 ∈ ℂ → ( abs ‘ 𝐶 ) ∈ ( 0 [,) +∞ ) )
72 1 71 syl ⊢ ( 𝜑 → ( abs ‘ 𝐶 ) ∈ ( 0 [,) +∞ ) )
73 63 67 72 itg2mulc ⊢ ( 𝜑 → ( ∫2 ‘ ( ( ℝ × { ( abs ‘ 𝐶 ) } ) ∘f · ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ) = ( ( abs ‘ 𝐶 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ) )
74 62 73 eqtr3d ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) = ( ( abs ‘ 𝐶 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ) )
75 38 67 remulcld ⊢ ( 𝜑 → ( ( abs ‘ 𝐶 ) · ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ 𝐵 ) , 0 ) ) ) ) ∈ ℝ )
76 74 75 eqeltrd ⊢ ( 𝜑 → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) ∈ ℝ )
77 76 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) ∈ ℝ )
78 10 abscld ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℝ )
79 78 rexrd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℝ* )
80 10 absge0d ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) )
81 elxrge0 ⊢ ( ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ( 0 [,] +∞ ) ↔ ( ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℝ* ∧ 0 ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) ) )
82 79 80 81 sylanbrc ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ( 0 [,] +∞ ) )
83 30 a1i ⊢ ( ( 𝜑 ∧ ¬ 𝑥 ∈ 𝐴 ) → 0 ∈ ( 0 [,] +∞ ) )
84 82 83 ifclda ⊢ ( 𝜑 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
85 84 adantr ⊢ ( ( 𝜑 ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
86 85 fmpttd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
87 86 adantr ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) )
88 20 releabsd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) )
89 11 17 19 absdivd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / ( abs ‘ ( i ↑ 𝑘 ) ) ) )
90 elfznn0 ⊢ ( 𝑘 ∈ ( 0 ... 3 ) → 𝑘 ∈ ℕ0 )
91 90 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 𝑘 ∈ ℕ0 )
92 absexp ⊢ ( ( i ∈ ℂ ∧ 𝑘 ∈ ℕ0 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = ( ( abs ‘ i ) ↑ 𝑘 ) )
93 12 91 92 sylancr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = ( ( abs ‘ i ) ↑ 𝑘 ) )
94 absi ⊢ ( abs ‘ i ) = 1
95 94 oveq1i ⊢ ( ( abs ‘ i ) ↑ 𝑘 ) = ( 1 ↑ 𝑘 )
96 1exp ⊢ ( 𝑘 ∈ ℤ → ( 1 ↑ 𝑘 ) = 1 )
97 15 96 syl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( 1 ↑ 𝑘 ) = 1 )
98 95 97 eqtrid ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ i ) ↑ 𝑘 ) = 1 )
99 93 98 eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( i ↑ 𝑘 ) ) = 1 )
100 99 oveq2d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / ( abs ‘ ( i ↑ 𝑘 ) ) ) = ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / 1 ) )
101 78 recnd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℂ )
102 101 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( 𝐶 · 𝐵 ) ) ∈ ℂ )
103 102 div1d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ( abs ‘ ( 𝐶 · 𝐵 ) ) / 1 ) = ( abs ‘ ( 𝐶 · 𝐵 ) ) )
104 89 100 103 3eqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( abs ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = ( abs ‘ ( 𝐶 · 𝐵 ) ) )
105 88 104 breqtrd ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) )
106 80 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → 0 ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) )
107 breq1 ⊢ ( ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) → ( ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) ↔ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) ) )
108 breq1 ⊢ ( 0 = if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) → ( 0 ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) ↔ if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) ) )
109 107 108 ifboth ⊢ ( ( ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) ∧ 0 ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) )
110 105 106 109 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ ( abs ‘ ( 𝐶 · 𝐵 ) ) )
111 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
112 111 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) )
113 iftrue ⊢ ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) = ( abs ‘ ( 𝐶 · 𝐵 ) ) )
114 113 adantl ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) = ( abs ‘ ( 𝐶 · 𝐵 ) ) )
115 110 112 114 3brtr4d ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ 𝐴 ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) )
116 115 ex ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) )
117 0le0 ⊢ 0 ≤ 0
118 117 a1i ⊢ ( ¬ 𝑥 ∈ 𝐴 → 0 ≤ 0 )
119 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) = 0 )
120 iffalse ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) = 0 )
121 118 119 120 3brtr4d ⊢ ( ¬ 𝑥 ∈ 𝐴 → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) )
122 116 121 pm2.61d1 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( 𝑥 ∈ 𝐴 , if ( 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) )
123 7 122 eqbrtrid ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) )
124 123 ralrimivw ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) )
125 36 a1i ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ℝ ∈ V )
126 85 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) ∧ 𝑥 ∈ ℝ ) → if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ∈ ( 0 [,] +∞ ) )
127 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
128 eqidd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) )
129 125 34 126 127 128 ofrfval2 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ↔ ∀ 𝑥 ∈ ℝ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ≤ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) )
130 124 129 mpbird ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) )
131 itg2le ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ∘r ≤ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) )
132 35 87 130 131 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) )
133 itg2lecl ⊢ ( ( ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) : ℝ ⟶ ( 0 [,] +∞ ) ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) ∈ ℝ ∧ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ≤ ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( 𝑥 ∈ 𝐴 , ( abs ‘ ( 𝐶 · 𝐵 ) ) , 0 ) ) ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
134 35 77 132 133 syl3anc ⊢ ( ( 𝜑 ∧ 𝑘 ∈ ( 0 ... 3 ) ) → ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
135 134 ralrimiva ⊢ ( 𝜑 → ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ )
136 eqidd ⊢ ( 𝜑 → ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) = ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) )
137 eqidd ⊢ ( ( 𝜑 ∧ 𝑥 ∈ 𝐴 ) → ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) = ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) )
138 136 137 10 isibl2 ⊢ ( 𝜑 → ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 ↔ ( ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ MblFn ∧ ∀ 𝑘 ∈ ( 0 ... 3 ) ( ∫2 ‘ ( 𝑥 ∈ ℝ ↦ if ( ( 𝑥 ∈ 𝐴 ∧ 0 ≤ ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) ) , ( ℜ ‘ ( ( 𝐶 · 𝐵 ) / ( i ↑ 𝑘 ) ) ) , 0 ) ) ) ∈ ℝ ) ) )
139 6 135 138 mpbir2and ⊢ ( 𝜑 → ( 𝑥 ∈ 𝐴 ↦ ( 𝐶 · 𝐵 ) ) ∈ 𝐿1 )