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

Metamath Proof Explorer

Theorem iblss

Description: A subset of an integrable function is integrable. (Contributed by Mario Carneiro, 12-Aug-2014)

Ref Expression
Hypotheses iblss.1 
|- ( ph -> A C_ B )
iblss.2 
|- ( ph -> A e. dom vol )
iblss.3 
|- ( ( ph /\ x e. B ) -> C e. V )
iblss.4 
|- ( ph -> ( x e. B |-> C ) e. L^1 )
Assertion iblss 
|- ( ph -> ( x e. A |-> C ) e. L^1 )

Proof

Step Hyp Ref Expression
1 iblss.1 
 |-  ( ph -> A C_ B )
2 iblss.2 
 |-  ( ph -> A e. dom vol )
3 iblss.3 
 |-  ( ( ph /\ x e. B ) -> C e. V )
4 iblss.4 
 |-  ( ph -> ( x e. B |-> C ) e. L^1 )
5 1 resmptd 
 |-  ( ph -> ( ( x e. B |-> C ) |` A ) = ( x e. A |-> C ) )
6 iblmbf 
 |-  ( ( x e. B |-> C ) e. L^1 -> ( x e. B |-> C ) e. MblFn )
7 4 6 syl 
 |-  ( ph -> ( x e. B |-> C ) e. MblFn )
8 mbfres 
 |-  ( ( ( x e. B |-> C ) e. MblFn /\ A e. dom vol ) -> ( ( x e. B |-> C ) |` A ) e. MblFn )
9 7 2 8 syl2anc 
 |-  ( ph -> ( ( x e. B |-> C ) |` A ) e. MblFn )
10 5 9 eqeltrrd 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
11 ifan 
 |-  if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
12 1 sselda 
 |-  ( ( ph /\ x e. A ) -> x e. B )
13 12 ad4ant14 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. A ) -> x e. B )
14 7 3 mbfmptcl 
 |-  ( ( ph /\ x e. B ) -> C e. CC )
15 14 ad4ant14 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> C e. CC )
16 ax-icn 
 |-  _i e. CC
17 ine0 
 |-  _i =/= 0
18 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
19 18 ad3antlr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> k e. ZZ )
20 expclz 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) e. CC )
21 16 17 19 20 mp3an12i 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> ( _i ^ k ) e. CC )
22 expne0i 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) =/= 0 )
23 16 17 19 22 mp3an12i 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> ( _i ^ k ) =/= 0 )
24 15 21 23 divcld 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> ( C / ( _i ^ k ) ) e. CC )
25 24 recld 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) e. RR )
26 0re 
 |-  0 e. RR
27 ifcl 
 |-  ( ( ( Re ` ( C / ( _i ^ k ) ) ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR )
28 25 26 27 sylancl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR )
29 28 rexrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR* )
30 max1 
 |-  ( ( 0 e. RR /\ ( Re ` ( C / ( _i ^ k ) ) ) e. RR ) -> 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
31 26 25 30 sylancr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
32 elxrge0 
 |-  ( if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) <-> ( if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. RR* /\ 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
33 29 31 32 sylanbrc 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
34 13 33 syldan 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. A ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
35 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
36 35 a1i 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
37 34 36 ifclda 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) e. ( 0 [,] +oo ) )
38 11 37 eqeltrid 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
39 38 fmpttd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
40 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
41 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
42 40 41 4 3 iblitg 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
43 18 42 sylan2 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
44 ifan 
 |-  if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
45 35 a1i 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ -. x e. B ) -> 0 e. ( 0 [,] +oo ) )
46 33 45 ifclda 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) e. ( 0 [,] +oo ) )
47 44 46 eqeltrid 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
48 47 fmpttd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
49 28 leidd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
50 breq1 
 |-  ( if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) -> ( if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) <-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
51 breq1 
 |-  ( 0 = if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) -> ( 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) <-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
52 50 51 ifboth 
 |-  ( ( if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) /\ 0 <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
53 49 31 52 syl2anc 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
54 iftrue 
 |-  ( x e. B -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
55 54 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
56 53 55 breqtrrd 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ x e. B ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
57 0le0 
 |-  0 <_ 0
58 57 a1i 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ -. x e. B ) -> 0 <_ 0 )
59 13 stoic1a 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ -. x e. B ) -> -. x e. A )
60 59 iffalsed 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ -. x e. B ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
61 iffalse 
 |-  ( -. x e. B -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
62 61 adantl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ -. x e. B ) -> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
63 58 60 62 3brtr4d 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) /\ -. x e. B ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
64 56 63 pm2.61dan 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
65 64 11 44 3brtr4g 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) <_ if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
66 65 ralrimiva 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) <_ if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
67 reex 
 |-  RR e. _V
68 67 a1i 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> RR e. _V )
69 eqidd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
70 eqidd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
71 68 38 47 69 70 ofrfval2 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) <-> A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) <_ if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
72 66 71 mpbird 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
73 itg2le 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) oR <_ ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
74 39 48 72 73 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
75 itg2lecl 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
76 39 43 74 75 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
77 76 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
78 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
79 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
80 12 14 syldan 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
81 78 79 80 isibl2 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> C ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
82 10 77 81 mpbir2and 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )