Metamath Proof Explorer

Theorem iprodclim3

Description: The sequence of partial finite product of a converging infinite product converge to the infinite product of the series. Note that j must not occur in A . (Contributed by Scott Fenton, 18-Dec-2017)

Ref Expression
Hypotheses iprodclim3.1 
|- Z = ( ZZ>= ` M )
iprodclim3.2 
|- ( ph -> M e. ZZ )
iprodclim3.3 
|- ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. Z |-> A ) ) ~~> y ) )
iprodclim3.4 
|- ( ph -> F e. dom ~~> )
iprodclim3.5 
|- ( ( ph /\ k e. Z ) -> A e. CC )
iprodclim3.6 
|- ( ( ph /\ j e. Z ) -> ( F ` j ) = prod_ k e. ( M ... j ) A )
Assertion iprodclim3 
|- ( ph -> F ~~> prod_ k e. Z A )

Proof

Step Hyp Ref Expression
1 iprodclim3.1 
 |-  Z = ( ZZ>= ` M )
2 iprodclim3.2 
 |-  ( ph -> M e. ZZ )
3 iprodclim3.3 
 |-  ( ph -> E. n e. Z E. y ( y =/= 0 /\ seq n ( x. , ( k e. Z |-> A ) ) ~~> y ) )
4 iprodclim3.4 
 |-  ( ph -> F e. dom ~~> )
5 iprodclim3.5 
 |-  ( ( ph /\ k e. Z ) -> A e. CC )
6 iprodclim3.6 
 |-  ( ( ph /\ j e. Z ) -> ( F ` j ) = prod_ k e. ( M ... j ) A )
7 climdm 
 |-  ( F e. dom ~~> <-> F ~~> ( ~~> ` F ) )
8 4 7 sylib 
 |-  ( ph -> F ~~> ( ~~> ` F ) )
9 prodfc 
 |-  prod_ m e. Z ( ( k e. Z |-> A ) ` m ) = prod_ k e. Z A
10 eqidd 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> A ) ` m ) = ( ( k e. Z |-> A ) ` m ) )
11 5 fmpttd 
 |-  ( ph -> ( k e. Z |-> A ) : Z --> CC )
12 11 ffvelrnda 
 |-  ( ( ph /\ m e. Z ) -> ( ( k e. Z |-> A ) ` m ) e. CC )
13 1 2 3 10 12 iprod 
 |-  ( ph -> prod_ m e. Z ( ( k e. Z |-> A ) ` m ) = ( ~~> ` seq M ( x. , ( k e. Z |-> A ) ) ) )
14 9 13 eqtr3id 
 |-  ( ph -> prod_ k e. Z A = ( ~~> ` seq M ( x. , ( k e. Z |-> A ) ) ) )
15 seqex 
 |-  seq M ( x. , ( k e. Z |-> A ) ) e. _V
16 15 a1i 
 |-  ( ph -> seq M ( x. , ( k e. Z |-> A ) ) e. _V )
17 fvres 
 |-  ( m e. ( M ... j ) -> ( ( ( k e. Z |-> A ) |` ( M ... j ) ) ` m ) = ( ( k e. Z |-> A ) ` m ) )
18 fzssuz 
 |-  ( M ... j ) C_ ( ZZ>= ` M )
19 18 1 sseqtrri 
 |-  ( M ... j ) C_ Z
20 resmpt 
 |-  ( ( M ... j ) C_ Z -> ( ( k e. Z |-> A ) |` ( M ... j ) ) = ( k e. ( M ... j ) |-> A ) )
21 19 20 ax-mp 
 |-  ( ( k e. Z |-> A ) |` ( M ... j ) ) = ( k e. ( M ... j ) |-> A )
22 21 fveq1i 
 |-  ( ( ( k e. Z |-> A ) |` ( M ... j ) ) ` m ) = ( ( k e. ( M ... j ) |-> A ) ` m )
23 17 22 eqtr3di 
 |-  ( m e. ( M ... j ) -> ( ( k e. Z |-> A ) ` m ) = ( ( k e. ( M ... j ) |-> A ) ` m ) )
24 23 prodeq2i 
 |-  prod_ m e. ( M ... j ) ( ( k e. Z |-> A ) ` m ) = prod_ m e. ( M ... j ) ( ( k e. ( M ... j ) |-> A ) ` m )
25 prodfc 
 |-  prod_ m e. ( M ... j ) ( ( k e. ( M ... j ) |-> A ) ` m ) = prod_ k e. ( M ... j ) A
26 24 25 eqtri 
 |-  prod_ m e. ( M ... j ) ( ( k e. Z |-> A ) ` m ) = prod_ k e. ( M ... j ) A
27 eqidd 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( M ... j ) ) -> ( ( k e. Z |-> A ) ` m ) = ( ( k e. Z |-> A ) ` m ) )
28 simpr 
 |-  ( ( ph /\ j e. Z ) -> j e. Z )
29 28 1 eleqtrdi 
 |-  ( ( ph /\ j e. Z ) -> j e. ( ZZ>= ` M ) )
30 elfzuz 
 |-  ( m e. ( M ... j ) -> m e. ( ZZ>= ` M ) )
31 30 1 eleqtrrdi 
 |-  ( m e. ( M ... j ) -> m e. Z )
32 31 12 sylan2 
 |-  ( ( ph /\ m e. ( M ... j ) ) -> ( ( k e. Z |-> A ) ` m ) e. CC )
33 32 adantlr 
 |-  ( ( ( ph /\ j e. Z ) /\ m e. ( M ... j ) ) -> ( ( k e. Z |-> A ) ` m ) e. CC )
34 27 29 33 fprodser 
 |-  ( ( ph /\ j e. Z ) -> prod_ m e. ( M ... j ) ( ( k e. Z |-> A ) ` m ) = ( seq M ( x. , ( k e. Z |-> A ) ) ` j ) )
35 26 34 eqtr3id 
 |-  ( ( ph /\ j e. Z ) -> prod_ k e. ( M ... j ) A = ( seq M ( x. , ( k e. Z |-> A ) ) ` j ) )
36 6 35 eqtr2d 
 |-  ( ( ph /\ j e. Z ) -> ( seq M ( x. , ( k e. Z |-> A ) ) ` j ) = ( F ` j ) )
37 1 16 4 2 36 climeq 
 |-  ( ph -> ( seq M ( x. , ( k e. Z |-> A ) ) ~~> x <-> F ~~> x ) )
38 37 iotabidv 
 |-  ( ph -> ( iota x seq M ( x. , ( k e. Z |-> A ) ) ~~> x ) = ( iota x F ~~> x ) )
39 df-fv 
 |-  ( ~~> ` seq M ( x. , ( k e. Z |-> A ) ) ) = ( iota x seq M ( x. , ( k e. Z |-> A ) ) ~~> x )
40 df-fv 
 |-  ( ~~> ` F ) = ( iota x F ~~> x )
41 38 39 40 3eqtr4g 
 |-  ( ph -> ( ~~> ` seq M ( x. , ( k e. Z |-> A ) ) ) = ( ~~> ` F ) )
42 14 41 eqtrd 
 |-  ( ph -> prod_ k e. Z A = ( ~~> ` F ) )
43 8 42 breqtrrd 
 |-  ( ph -> F ~~> prod_ k e. Z A )