Step |
Hyp |
Ref |
Expression |
1 |
|
iprodefisum.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
iprodefisum.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
iprodefisum.3 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B ) |
4 |
|
iprodefisum.4 |
|- ( ( ph /\ k e. Z ) -> B e. CC ) |
5 |
|
iprodefisum.5 |
|- ( ph -> seq M ( + , F ) e. dom ~~> ) |
6 |
1 2 3 4 5
|
isumcl |
|- ( ph -> sum_ k e. Z B e. CC ) |
7 |
|
efne0 |
|- ( sum_ k e. Z B e. CC -> ( exp ` sum_ k e. Z B ) =/= 0 ) |
8 |
6 7
|
syl |
|- ( ph -> ( exp ` sum_ k e. Z B ) =/= 0 ) |
9 |
|
efcn |
|- exp e. ( CC -cn-> CC ) |
10 |
9
|
a1i |
|- ( ph -> exp e. ( CC -cn-> CC ) ) |
11 |
|
fveq2 |
|- ( j = k -> ( F ` j ) = ( F ` k ) ) |
12 |
|
eqid |
|- ( j e. Z |-> ( F ` j ) ) = ( j e. Z |-> ( F ` j ) ) |
13 |
|
fvex |
|- ( F ` k ) e. _V |
14 |
11 12 13
|
fvmpt |
|- ( k e. Z -> ( ( j e. Z |-> ( F ` j ) ) ` k ) = ( F ` k ) ) |
15 |
14
|
adantl |
|- ( ( ph /\ k e. Z ) -> ( ( j e. Z |-> ( F ` j ) ) ` k ) = ( F ` k ) ) |
16 |
3 4
|
eqeltrd |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
17 |
15 16
|
eqeltrd |
|- ( ( ph /\ k e. Z ) -> ( ( j e. Z |-> ( F ` j ) ) ` k ) e. CC ) |
18 |
1 2 17
|
serf |
|- ( ph -> seq M ( + , ( j e. Z |-> ( F ` j ) ) ) : Z --> CC ) |
19 |
1
|
eqcomi |
|- ( ZZ>= ` M ) = Z |
20 |
14 19
|
eleq2s |
|- ( k e. ( ZZ>= ` M ) -> ( ( j e. Z |-> ( F ` j ) ) ` k ) = ( F ` k ) ) |
21 |
20
|
adantl |
|- ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( ( j e. Z |-> ( F ` j ) ) ` k ) = ( F ` k ) ) |
22 |
2 21
|
seqfeq |
|- ( ph -> seq M ( + , ( j e. Z |-> ( F ` j ) ) ) = seq M ( + , F ) ) |
23 |
|
climdm |
|- ( seq M ( + , F ) e. dom ~~> <-> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) ) |
24 |
5 23
|
sylib |
|- ( ph -> seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) ) |
25 |
22 24
|
eqbrtrd |
|- ( ph -> seq M ( + , ( j e. Z |-> ( F ` j ) ) ) ~~> ( ~~> ` seq M ( + , F ) ) ) |
26 |
|
climcl |
|- ( seq M ( + , F ) ~~> ( ~~> ` seq M ( + , F ) ) -> ( ~~> ` seq M ( + , F ) ) e. CC ) |
27 |
24 26
|
syl |
|- ( ph -> ( ~~> ` seq M ( + , F ) ) e. CC ) |
28 |
1 2 10 18 25 27
|
climcncf |
|- ( ph -> ( exp o. seq M ( + , ( j e. Z |-> ( F ` j ) ) ) ) ~~> ( exp ` ( ~~> ` seq M ( + , F ) ) ) ) |
29 |
11
|
cbvmptv |
|- ( j e. Z |-> ( F ` j ) ) = ( k e. Z |-> ( F ` k ) ) |
30 |
16 29
|
fmptd |
|- ( ph -> ( j e. Z |-> ( F ` j ) ) : Z --> CC ) |
31 |
1 2 30
|
iprodefisumlem |
|- ( ph -> seq M ( x. , ( exp o. ( j e. Z |-> ( F ` j ) ) ) ) = ( exp o. seq M ( + , ( j e. Z |-> ( F ` j ) ) ) ) ) |
32 |
1 2 3 4
|
isum |
|- ( ph -> sum_ k e. Z B = ( ~~> ` seq M ( + , F ) ) ) |
33 |
32
|
fveq2d |
|- ( ph -> ( exp ` sum_ k e. Z B ) = ( exp ` ( ~~> ` seq M ( + , F ) ) ) ) |
34 |
28 31 33
|
3brtr4d |
|- ( ph -> seq M ( x. , ( exp o. ( j e. Z |-> ( F ` j ) ) ) ) ~~> ( exp ` sum_ k e. Z B ) ) |
35 |
|
fvco3 |
|- ( ( ( j e. Z |-> ( F ` j ) ) : Z --> CC /\ k e. Z ) -> ( ( exp o. ( j e. Z |-> ( F ` j ) ) ) ` k ) = ( exp ` ( ( j e. Z |-> ( F ` j ) ) ` k ) ) ) |
36 |
30 35
|
sylan |
|- ( ( ph /\ k e. Z ) -> ( ( exp o. ( j e. Z |-> ( F ` j ) ) ) ` k ) = ( exp ` ( ( j e. Z |-> ( F ` j ) ) ` k ) ) ) |
37 |
15
|
fveq2d |
|- ( ( ph /\ k e. Z ) -> ( exp ` ( ( j e. Z |-> ( F ` j ) ) ` k ) ) = ( exp ` ( F ` k ) ) ) |
38 |
3
|
fveq2d |
|- ( ( ph /\ k e. Z ) -> ( exp ` ( F ` k ) ) = ( exp ` B ) ) |
39 |
36 37 38
|
3eqtrd |
|- ( ( ph /\ k e. Z ) -> ( ( exp o. ( j e. Z |-> ( F ` j ) ) ) ` k ) = ( exp ` B ) ) |
40 |
|
efcl |
|- ( B e. CC -> ( exp ` B ) e. CC ) |
41 |
4 40
|
syl |
|- ( ( ph /\ k e. Z ) -> ( exp ` B ) e. CC ) |
42 |
1 2 8 34 39 41
|
iprodn0 |
|- ( ph -> prod_ k e. Z ( exp ` B ) = ( exp ` sum_ k e. Z B ) ) |