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 ) |