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 )