Metamath Proof Explorer

Theorem iblmulc2

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

Ref Expression
Hypotheses itgmulc2.1 
|- ( ph -> C e. CC )
itgmulc2.2 
|- ( ( ph /\ x e. A ) -> B e. V )
itgmulc2.3 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion iblmulc2 
|- ( ph -> ( x e. A |-> ( C x. B ) ) e. L^1 )

Proof

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