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