Metamath Proof Explorer

Theorem iblconst

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

Ref Expression
Assertion iblconst 
|- ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( A X. { B } ) e. L^1 )

Proof

Step Hyp Ref Expression
1 fconstmpt 
 |-  ( A X. { B } ) = ( x e. A |-> B )
2 mbfconst 
 |-  ( ( A e. dom vol /\ B e. CC ) -> ( A X. { B } ) e. MblFn )
3 2 3adant2 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( A X. { B } ) e. MblFn )
4 1 3 eqeltrrid 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( x e. A |-> B ) e. MblFn )
5 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 )
6 5 mpteq2i 
 |-  ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) = ( x e. RR |-> if ( x e. A , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) )
7 6 fveq2i 
 |-  ( 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 , if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) , 0 ) ) )
8 simpl1 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> A e. dom vol )
9 simpl2 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> ( vol ` A ) e. RR )
10 simpl3 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> B e. CC )
11 ax-icn 
 |-  _i e. CC
12 ine0 
 |-  _i =/= 0
13 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
14 13 adantl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> k e. ZZ )
15 expclz 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) e. CC )
16 11 12 14 15 mp3an12i 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> ( _i ^ k ) e. CC )
17 expne0i 
 |-  ( ( _i e. CC /\ _i =/= 0 /\ k e. ZZ ) -> ( _i ^ k ) =/= 0 )
18 11 12 14 17 mp3an12i 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> ( _i ^ k ) =/= 0 )
19 10 16 18 divcld 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> ( B / ( _i ^ k ) ) e. CC )
20 19 recld 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> ( Re ` ( B / ( _i ^ k ) ) ) e. RR )
21 0re 
 |-  0 e. RR
22 ifcl 
 |-  ( ( ( Re ` ( B / ( _i ^ k ) ) ) e. RR /\ 0 e. RR ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. RR )
23 20 21 22 sylancl 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. RR )
24 max1 
 |-  ( ( 0 e. RR /\ ( Re ` ( B / ( _i ^ k ) ) ) e. RR ) -> 0 <_ if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) )
25 21 20 24 sylancr 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> 0 <_ if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) )
26 elrege0 
 |-  ( 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 ) ) )
27 23 25 26 sylanbrc 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,) +oo ) )
28 itg2const 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) e. ( 0 [,) +oo ) ) -> ( S.2 ` ( x e. RR |-> 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 ) x. ( vol ` A ) ) )
29 8 9 27 28 syl3anc 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> 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 ) x. ( vol ` A ) ) )
30 7 29 eqtrid 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) = ( if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) x. ( vol ` A ) ) )
31 23 9 remulcld 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ k e. ( 0 ... 3 ) ) -> ( if ( 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) x. ( vol ` A ) ) e. RR )
32 30 31 eqeltrd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ 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 )
33 32 ralrimiva 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> 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 )
34 eqidd 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( 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 ) ) )
35 eqidd 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) )
36 simpl3 
 |-  ( ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) /\ x e. A ) -> B e. CC )
37 34 35 36 isibl2 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( ( 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 ) ) )
38 4 33 37 mpbir2and 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( x e. A |-> B ) e. L^1 )
39 1 38 eqeltrid 
 |-  ( ( A e. dom vol /\ ( vol ` A ) e. RR /\ B e. CC ) -> ( A X. { B } ) e. L^1 )