Metamath Proof Explorer

Theorem iblsplit

Description: The union of two integrable functions is integrable. (Contributed by Glauco Siliprandi, 11-Dec-2019)

Ref Expression
Hypotheses iblsplit.1 
|- ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
iblsplit.2 
|- ( ph -> U = ( A u. B ) )
iblsplit.3 
|- ( ( ph /\ x e. U ) -> C e. CC )
iblsplit.4 
|- ( ph -> ( x e. A |-> C ) e. L^1 )
iblsplit.5 
|- ( ph -> ( x e. B |-> C ) e. L^1 )
Assertion iblsplit 
|- ( ph -> ( x e. U |-> C ) e. L^1 )

Proof

Step Hyp Ref Expression
1 iblsplit.1 
 |-  ( ph -> ( vol* ` ( A i^i B ) ) = 0 )
2 iblsplit.2 
 |-  ( ph -> U = ( A u. B ) )
3 iblsplit.3 
 |-  ( ( ph /\ x e. U ) -> C e. CC )
4 iblsplit.4 
 |-  ( ph -> ( x e. A |-> C ) e. L^1 )
5 iblsplit.5 
 |-  ( ph -> ( x e. B |-> C ) e. L^1 )
6 3 fmpttd 
 |-  ( ph -> ( x e. U |-> C ) : U --> CC )
7 ssun1 
 |-  A C_ ( A u. B )
8 7 2 sseqtrrid 
 |-  ( ph -> A C_ U )
9 8 resmptd 
 |-  ( ph -> ( ( x e. U |-> C ) |` A ) = ( x e. A |-> C ) )
10 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ y ) ) ) ) , ( Re ` ( C / ( _i ^ y ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ y ) ) ) ) , ( Re ` ( C / ( _i ^ y ) ) ) , 0 ) ) )
11 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C / ( _i ^ y ) ) ) = ( Re ` ( C / ( _i ^ y ) ) ) )
12 8 sseld 
 |-  ( ph -> ( x e. A -> x e. U ) )
13 12 imdistani 
 |-  ( ( ph /\ x e. A ) -> ( ph /\ x e. U ) )
14 13 3 syl 
 |-  ( ( ph /\ x e. A ) -> C e. CC )
15 10 11 14 isibl2 
 |-  ( ph -> ( ( x e. A |-> C ) e. L^1 <-> ( ( x e. A |-> C ) e. MblFn /\ A. y e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ y ) ) ) ) , ( Re ` ( C / ( _i ^ y ) ) ) , 0 ) ) ) e. RR ) ) )
16 4 15 mpbid 
 |-  ( ph -> ( ( x e. A |-> C ) e. MblFn /\ A. y e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ y ) ) ) ) , ( Re ` ( C / ( _i ^ y ) ) ) , 0 ) ) ) e. RR ) )
17 16 simpld 
 |-  ( ph -> ( x e. A |-> C ) e. MblFn )
18 9 17 eqeltrd 
 |-  ( ph -> ( ( x e. U |-> C ) |` A ) e. MblFn )
19 ssun2 
 |-  B C_ ( A u. B )
20 19 2 sseqtrrid 
 |-  ( ph -> B C_ U )
21 20 resmptd 
 |-  ( ph -> ( ( x e. U |-> C ) |` B ) = ( x e. B |-> C ) )
22 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ y ) ) ) ) , ( Re ` ( C / ( _i ^ y ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ y ) ) ) ) , ( Re ` ( C / ( _i ^ y ) ) ) , 0 ) ) )
23 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( Re ` ( C / ( _i ^ y ) ) ) = ( Re ` ( C / ( _i ^ y ) ) ) )
24 20 sseld 
 |-  ( ph -> ( x e. B -> x e. U ) )
25 24 imdistani 
 |-  ( ( ph /\ x e. B ) -> ( ph /\ x e. U ) )
26 25 3 syl 
 |-  ( ( ph /\ x e. B ) -> C e. CC )
27 22 23 26 isibl2 
 |-  ( ph -> ( ( x e. B |-> C ) e. L^1 <-> ( ( x e. B |-> C ) e. MblFn /\ A. y e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ y ) ) ) ) , ( Re ` ( C / ( _i ^ y ) ) ) , 0 ) ) ) e. RR ) ) )
28 5 27 mpbid 
 |-  ( ph -> ( ( x e. B |-> C ) e. MblFn /\ A. y e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ y ) ) ) ) , ( Re ` ( C / ( _i ^ y ) ) ) , 0 ) ) ) e. RR ) )
29 28 simpld 
 |-  ( ph -> ( x e. B |-> C ) e. MblFn )
30 21 29 eqeltrd 
 |-  ( ph -> ( ( x e. U |-> C ) |` B ) e. MblFn )
31 2 eqcomd 
 |-  ( ph -> ( A u. B ) = U )
32 6 18 30 31 mbfres2cn 
 |-  ( ph -> ( x e. U |-> C ) e. MblFn )
33 17 14 mbfdm2 
 |-  ( ph -> A e. dom vol )
34 33 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> A e. dom vol )
35 29 26 mbfdm2 
 |-  ( ph -> B e. dom vol )
36 35 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> B e. dom vol )
37 1 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( vol* ` ( A i^i B ) ) = 0 )
38 2 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> U = ( A u. B ) )
39 3 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> C e. CC )
40 ax-icn 
 |-  _i e. CC
41 40 a1i 
 |-  ( k e. ( 0 ... 3 ) -> _i e. CC )
42 elfznn0 
 |-  ( k e. ( 0 ... 3 ) -> k e. NN0 )
43 41 42 expcld 
 |-  ( k e. ( 0 ... 3 ) -> ( _i ^ k ) e. CC )
44 43 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( _i ^ k ) e. CC )
45 40 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> _i e. CC )
46 ine0 
 |-  _i =/= 0
47 46 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> _i =/= 0 )
48 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
49 48 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> k e. ZZ )
50 45 47 49 expne0d 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( _i ^ k ) =/= 0 )
51 39 44 50 divcld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( C / ( _i ^ k ) ) e. CC )
52 51 recld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( Re ` ( C / ( _i ^ k ) ) ) e. RR )
53 52 rexrd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> ( Re ` ( C / ( _i ^ k ) ) ) e. RR* )
54 53 adantr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) -> ( Re ` ( C / ( _i ^ k ) ) ) e. RR* )
55 simpr 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) -> 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) )
56 pnfge 
 |-  ( ( Re ` ( C / ( _i ^ k ) ) ) e. RR* -> ( Re ` ( C / ( _i ^ k ) ) ) <_ +oo )
57 54 56 syl 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) -> ( Re ` ( C / ( _i ^ k ) ) ) <_ +oo )
58 0xr 
 |-  0 e. RR*
59 pnfxr 
 |-  +oo e. RR*
60 elicc1 
 |-  ( ( 0 e. RR* /\ +oo e. RR* ) -> ( ( Re ` ( C / ( _i ^ k ) ) ) e. ( 0 [,] +oo ) <-> ( ( Re ` ( C / ( _i ^ k ) ) ) e. RR* /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) /\ ( Re ` ( C / ( _i ^ k ) ) ) <_ +oo ) ) )
61 58 59 60 mp2an 
 |-  ( ( Re ` ( C / ( _i ^ k ) ) ) e. ( 0 [,] +oo ) <-> ( ( Re ` ( C / ( _i ^ k ) ) ) e. RR* /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) /\ ( Re ` ( C / ( _i ^ k ) ) ) <_ +oo ) )
62 54 55 57 61 syl3anbrc 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) -> ( Re ` ( C / ( _i ^ k ) ) ) e. ( 0 [,] +oo ) )
63 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
64 63 a1i 
 |-  ( ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) /\ -. 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) -> 0 e. ( 0 [,] +oo ) )
65 62 64 ifclda 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. U ) -> if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
66 eqid 
 |-  ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) = ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
67 eqid 
 |-  ( x e. RR |-> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) = ( x e. RR |-> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
68 ifan 
 |-  if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) = if ( x e. U , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 )
69 68 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( x e. U , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) )
70 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 )
71 70 eqcomi 
 |-  if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 )
72 71 mpteq2i 
 |-  ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
73 72 a1i 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
74 73 fveq2d 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) )
75 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 ) ) )
76 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
77 75 76 14 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 ) ) )
78 4 77 mpbid 
 |-  ( ph -> ( ( 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 ) )
79 78 simprd 
 |-  ( 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 )
80 79 r19.21bi 
 |-  ( ( 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 )
81 74 80 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) ) e. RR )
82 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 )
83 82 eqcomi 
 |-  if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 )
84 83 mpteq2i 
 |-  ( x e. RR |-> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) = ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) )
85 84 fveq2i 
 |-  ( S.2 ` ( x e. RR |-> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) ) = ( S.2 ` ( x e. RR |-> if ( ( x e. B /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
86 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 ) ) )
87 eqidd 
 |-  ( ( ph /\ x e. B ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
88 86 87 26 isibl2 
 |-  ( ph -> ( ( x e. B |-> C ) e. L^1 <-> ( ( x e. B |-> C ) e. MblFn /\ A. 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 ) ) )
89 5 88 mpbid 
 |-  ( ph -> ( ( x e. B |-> C ) e. MblFn /\ A. 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 ) )
90 89 simprd 
 |-  ( ph -> A. 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 )
91 90 r19.21bi 
 |-  ( ( 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 )
92 85 91 eqeltrid 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) ) e. RR )
93 34 36 37 38 65 66 67 69 81 92 itg2split 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) = ( ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) ) ) )
94 81 92 readdcld 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( S.2 ` ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) ) + ( S.2 ` ( x e. RR |-> if ( x e. B , if ( 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) , 0 ) ) ) ) e. RR )
95 93 94 eqeltrd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
96 95 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
97 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) )
98 eqidd 
 |-  ( ( ph /\ x e. U ) -> ( Re ` ( C / ( _i ^ k ) ) ) = ( Re ` ( C / ( _i ^ k ) ) ) )
99 97 98 3 isibl2 
 |-  ( ph -> ( ( x e. U |-> C ) e. L^1 <-> ( ( x e. U |-> C ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. U /\ 0 <_ ( Re ` ( C / ( _i ^ k ) ) ) ) , ( Re ` ( C / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
100 32 96 99 mpbir2and 
 |-  ( ph -> ( x e. U |-> C ) e. L^1 )