Metamath Proof Explorer

Theorem itgcl

Description: The integral of an integrable function is a complex number. This is Metamath 100 proof #86. (Contributed by Mario Carneiro, 29-Jun-2014)

Ref Expression
Hypotheses itgmpt.1 
|- ( ( ph /\ x e. A ) -> B e. V )
itgcl.2 
|- ( ph -> ( x e. A |-> B ) e. L^1 )
Assertion itgcl 
|- ( ph -> S. A B _d x e. CC )

Proof

Step Hyp Ref Expression
1 itgmpt.1 
 |-  ( ( ph /\ x e. A ) -> B e. V )
2 itgcl.2 
 |-  ( ph -> ( x e. A |-> B ) e. L^1 )
3 eqid 
 |-  ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) )
4 3 dfitg 
 |-  S. A B _d x = sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) )
5 fzfid 
 |-  ( ph -> ( 0 ... 3 ) e. Fin )
6 ax-icn 
 |-  _i e. CC
7 elfznn0 
 |-  ( k e. ( 0 ... 3 ) -> k e. NN0 )
8 7 adantl 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> k e. NN0 )
9 expcl 
 |-  ( ( _i e. CC /\ k e. NN0 ) -> ( _i ^ k ) e. CC )
10 6 8 9 sylancr 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( _i ^ k ) e. CC )
11 elfzelz 
 |-  ( k e. ( 0 ... 3 ) -> k e. ZZ )
12 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 ) ) )
13 eqidd 
 |-  ( ( ph /\ x e. A ) -> ( Re ` ( B / ( _i ^ k ) ) ) = ( Re ` ( B / ( _i ^ k ) ) ) )
14 12 13 2 1 iblitg 
 |-  ( ( ph /\ k e. ZZ ) -> ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) e. RR )
15 11 14 sylan2 
 |-  ( ( 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 )
16 15 recnd 
 |-  ( ( 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. CC )
17 10 16 mulcld 
 |-  ( ( ph /\ k e. ( 0 ... 3 ) ) -> ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) e. CC )
18 5 17 fsumcl 
 |-  ( ph -> sum_ k e. ( 0 ... 3 ) ( ( _i ^ k ) x. ( S.2 ` ( x e. RR |-> if ( ( x e. A /\ 0 <_ ( Re ` ( B / ( _i ^ k ) ) ) ) , ( Re ` ( B / ( _i ^ k ) ) ) , 0 ) ) ) ) e. CC )
19 4 18 eqeltrid 
 |-  ( ph -> S. A B _d x e. CC )