Metamath Proof Explorer

Theorem iblabsr

Description: A measurable function is integrable iff its absolute value is integrable. (See iblabs for the forward implication.) (Contributed by Mario Carneiro, 25-Aug-2014)

Ref Expression
Hypotheses iblabsr.1 
|- ( ( ph /\ x e. A ) -> B e. V )
iblabsr.2 
|- ( ph -> ( x e. A |-> B ) e. MblFn )
iblabsr.3 
|- ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )
Assertion iblabsr 
|- ( ph -> ( x e. A |-> B ) e. L^1 )

Proof

Step Hyp Ref Expression
1 iblabsr.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 iblabsr.2 
 |-  ( ph -> ( x e. A |-> B ) e. MblFn )
3 iblabsr.3 
 |-  ( ph -> ( x e. A |-> ( abs ` B ) ) e. L^1 )
4 ifan 
 |-  if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) = if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 )
5 2 1 mbfmptcl 
 |-  ( ( ph /\ x e. A ) -> B e. CC )
6 5 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> B e. CC )
7 ax-icn 
 |-  _i e. CC
8 ine0 
 |-  _i =/= 0
9 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
10 9 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> k e. ZZ )
11 expclz 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) e. CC )
12 7 8 10 11 mp3an12i 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( _i ^ k ) e. CC )
13 expne0i 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) =/= 0 )
14 7 8 10 13 mp3an12i 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( _i ^ k ) =/= 0 )
15 6 12 14 divcld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( B / ( _i ^ k ) ) e. CC )
16 15 recld 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) e. RR )
17 0re 
 |-  0 e. RR
18 ifcl 
 |-  ( ( ( Re ` ( B / ( _i ^ k ) ) ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. RR )
19 16 17 18 sylancl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. RR )
20 19 rexrd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. RR* )
21 max1 
 |-  ( ( 0 e. RR /\ ( Re ` ( B / ( _i ^ k ) ) ) e. RR ) -> 0 <_ if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) )
22 17 16 21 sylancr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> 0 <_ if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) )
23 elxrge0 
 |-  ( if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) <-> ( if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. RR* /\ 0 <_ if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) )
24 20 22 23 sylanbrc 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
25 0e0iccpnf 
 |-  0 e. ( 0 [,] +oo )
26 25 a1i 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
27 24 26 ifclda 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) e. ( 0 [,] +oo ) )
28 4 27 eqeltrid 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
29 28 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,] +oo ) )
30 29 fmpttd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
31 5 abscld 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR )
32 5 absge0d 
 |-  ( ( ph /\ x e. A ) -> 0 <_ ( abs ` B ) )
33 31 32 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 ) ) )
34 3 33 mpbid 
 |-  ( ph -> ( ( x e. A |-> ( abs ` B ) ) e. MblFn /\ ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) e. RR ) )
35 34 simprd 
 |-  ( ph -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) e. RR )
36 35 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) e. RR )
37 31 rexrd 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. RR* )
38 elxrge0 
 |-  ( ( abs ` B ) e. ( 0 [,] +oo ) <-> ( ( abs ` B ) e. RR* /\ 0 <_ ( abs ` B ) ) )
39 37 32 38 sylanbrc 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. ( 0 [,] +oo ) )
40 25 a1i 
 |-  ( ( ph /\ -. x e. A ) -> 0 e. ( 0 [,] +oo ) )
41 39 40 ifclda 
 |-  ( ph -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,] +oo ) )
42 41 adantr 
 |-  ( ( ph /\ x e. RR ) -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,] +oo ) )
43 42 fmpttd 
 |-  ( ph -> ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
44 43 adantr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) : RR --> ( 0 [,] +oo ) )
45 15 releabsd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) <_ ( abs ` ( B / ( _i ^ k ) ) ) )
46 6 12 14 absdivd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( abs ` ( B / ( _i ^ k ) ) ) = ( ( abs ` B ) / ( abs ` ( _i ^ k ) ) ) )
47 elfznn0 
 |-  ( k e. ( 0 ... 3 ) -> k e. NN0 )
48 47 ad2antlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> k e. NN0 )
49 absexp 
 |-  ( ( _i e. CC /\ k e. NN0 ) -> ( abs ` ( _i ^ k ) ) = ( ( abs ` _i ) ^ k ) )
50 7 48 49 sylancr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( abs ` ( _i ^ k ) ) = ( ( abs ` _i ) ^ k ) )
51 absi 
 |-  ( abs ` _i ) = 1
52 51 oveq1i 
 |-  ( ( abs ` _i ) ^ k ) = ( 1 ^ k )
53 1exp 
 |-  ( k e. ZZ -> ( 1 ^ k ) = 1 )
54 10 53 syl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( 1 ^ k ) = 1 )
55 52 54 syl5eq 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( ( abs ` _i ) ^ k ) = 1 )
56 50 55 eqtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( abs ` ( _i ^ k ) ) = 1 )
57 56 oveq2d 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( ( abs ` B ) / ( abs ` ( _i ^ k ) ) ) = ( ( abs ` B ) / 1 ) )
58 31 recnd 
 |-  ( ( ph /\ x e. A ) -> ( abs ` B ) e. CC )
59 58 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( abs ` B ) e. CC )
60 59 div1d 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( ( abs ` B ) / 1 ) = ( abs ` B ) )
61 46 57 60 3eqtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( abs ` ( B / ( _i ^ k ) ) ) = ( abs ` B ) )
62 45 61 breqtrd 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) <_ ( abs ` B ) )
63 6 absge0d 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> 0 <_ ( abs ` B ) )
64 breq1 
 |-  ( ( Re ` ( B / ( _i ^ k ) ) ) = if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) -> ( ( Re ` ( B / ( _i ^ k ) ) ) <_ ( abs ` B ) <-> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) <_ ( abs ` B ) ) )
65 breq1 
 |-  ( 0 = if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) -> ( 0 <_ ( abs ` B ) <-> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) <_ ( abs ` B ) ) )
66 64 65 ifboth 
 |-  ( ( ( Re ` ( B / ( _i ^ k ) ) ) <_ ( abs ` B ) /\ 0 <_ ( abs ` B ) ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) <_ ( abs ` B ) )
67 62 63 66 syl2anc 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) <_ ( abs ` B ) )
68 iftrue 
 |-  ( x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) )
69 68 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) = if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) )
70 iftrue 
 |-  ( x e. A -> if ( x e. A , ( abs ` B ) , 0 ) = ( abs ` B ) )
71 70 adantl 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( x e. A , ( abs ` B ) , 0 ) = ( abs ` B ) )
72 67 69 71 3brtr4d 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( x e. A , ( abs ` B ) , 0 ) )
73 72 ex 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( x e. A , ( abs ` B ) , 0 ) ) )
74 0le0 
 |-  0 <_ 0
75 74 a1i 
 |-  ( -. x e. A -> 0 <_ 0 )
76 iffalse 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) = 0 )
77 iffalse 
 |-  ( -. x e. A -> if ( x e. A , ( abs ` B ) , 0 ) = 0 )
78 75 76 77 3brtr4d 
 |-  ( -. x e. A -> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( x e. A , ( abs ` B ) , 0 ) )
79 73 78 pm2.61d1 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) <_ if ( x e. A , ( abs ` B ) , 0 ) )
80 4 79 eqbrtrid 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) <_ if ( x e. A , ( abs ` B ) , 0 ) )
81 80 ralrimivw 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) <_ if ( x e. A , ( abs ` B ) , 0 ) )
82 reex 
 |-  RR e. _V
83 82 a1i 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> RR e. _V )
84 37 adantlr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( abs ` B ) e. RR* )
85 84 63 38 sylanbrc 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. A ) -> ( abs ` B ) e. ( 0 [,] +oo ) )
86 85 26 ifclda 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,] +oo ) )
87 86 adantr 
 |-  ( ( ( ph /\ k e. ( 0 ... 3 ) ) /\ x e. RR ) -> if ( x e. A , ( abs ` B ) , 0 ) e. ( 0 [,] +oo ) )
88 eqidd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) )
89 eqidd 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) = ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) )
90 83 29 87 88 89 ofrfval2 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) <-> A. x e. RR if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) <_ if ( x e. A , ( abs ` B ) , 0 ) ) )
91 81 90 mpbird 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) )
92 itg2le 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) oR <_ ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) )
93 30 44 91 92 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) )
94 itg2lecl 
 |-  ( ( ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) : RR --> ( 0 [,] +oo ) /\ ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) e. RR /\ ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) <_ ( S.2 ` ( x e. RR |-> if ( x e. A , ( abs ` B ) , 0 ) ) ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
95 30 36 93 94 syl3anc 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
96 95 ralrimiva 
 |-  ( ph -> A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
97 eqidd 
 |-  ( ph -> ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) )
98 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) )
99 97 98 1 isibl2 
 |-  ( ph -> ( ( x e. A |-> B ) e. L^1 <-> ( ( x e. A |-> B ) e. MblFn /\ A. k e. ( 0 ... 3 ) ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR ) ) )
100 2 96 99 mpbir2and 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )