Metamath Proof Explorer

Theorem iblmulc2nc

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

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

Proof

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