Metamath Proof Explorer

Theorem iprodefisum

Description: Applying the exponential function to an infinite sum yields an infinite product. (Contributed by Scott Fenton, 11-Feb-2018)

Ref Expression
Hypotheses iprodefisum.1 
|- Z = ( ZZ>= ` M )
iprodefisum.2 
|- ( ph -> M e. ZZ )
iprodefisum.3 
|- ( ( ph /\ k e. Z ) -> ( F ` k ) = B )
iprodefisum.4 
|- ( ( ph /\ k e. Z ) -> B e. CC )
iprodefisum.5 
|- ( ph -> seq M ( + , F ) e. dom ~~> )
Assertion iprodefisum 
|- ( ph -> prod_ k e. Z ( exp ` B ) = ( exp ` sum_ k e. Z B ) )

Proof

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