Metamath Proof Explorer

Theorem fprodcvg

Description: The sequence of partial products of a finite product converges to the whole product. (Contributed by Scott Fenton, 4-Dec-2017)

Ref Expression
Hypotheses prodmo.1 
|- F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
prodmo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
prodrb.3 
|- ( ph -> N e. ( ZZ>= ` M ) )
fprodcvg.4 
|- ( ph -> A C_ ( M ... N ) )
Assertion fprodcvg 
|- ( ph -> seq M ( x. , F ) ~~> ( seq M ( x. , F ) ` N ) )

Proof

Step Hyp Ref Expression
1 prodmo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 1 ) )
2 prodmo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 prodrb.3 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
4 fprodcvg.4 
 |-  ( ph -> A C_ ( M ... N ) )
5 eqid 
 |-  ( ZZ>= ` N ) = ( ZZ>= ` N )
6 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
7 3 6 syl 
 |-  ( ph -> N e. ZZ )
8 seqex 
 |-  seq M ( x. , F ) e. _V
9 8 a1i 
 |-  ( ph -> seq M ( x. , F ) e. _V )
10 eqid 
 |-  ( ZZ>= ` M ) = ( ZZ>= ` M )
11 eluzel2 
 |-  ( N e. ( ZZ>= ` M ) -> M e. ZZ )
12 3 11 syl 
 |-  ( ph -> M e. ZZ )
13 eluzelz 
 |-  ( k e. ( ZZ>= ` M ) -> k e. ZZ )
14 13 adantl 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> k e. ZZ )
15 iftrue 
 |-  ( k e. A -> if ( k e. A , B , 1 ) = B )
16 15 adantl 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ k e. A ) -> if ( k e. A , B , 1 ) = B )
17 2 adantlr 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ k e. A ) -> B e. CC )
18 16 17 eqeltrd 
 |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ k e. A ) -> if ( k e. A , B , 1 ) e. CC )
19 18 ex 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( k e. A -> if ( k e. A , B , 1 ) e. CC ) )
20 iffalse 
 |-  ( -. k e. A -> if ( k e. A , B , 1 ) = 1 )
21 ax-1cn 
 |-  1 e. CC
22 20 21 eqeltrdi 
 |-  ( -. k e. A -> if ( k e. A , B , 1 ) e. CC )
23 19 22 pm2.61d1 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> if ( k e. A , B , 1 ) e. CC )
24 1 fvmpt2 
 |-  ( ( k e. ZZ /\ if ( k e. A , B , 1 ) e. CC ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
25 14 23 24 syl2anc 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
26 25 23 eqeltrd 
 |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )
27 10 12 26 prodf 
 |-  ( ph -> seq M ( x. , F ) : ( ZZ>= ` M ) --> CC )
28 27 3 ffvelrnd 
 |-  ( ph -> ( seq M ( x. , F ) ` N ) e. CC )
29 mulid1 
 |-  ( m e. CC -> ( m x. 1 ) = m )
30 29 adantl 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. CC ) -> ( m x. 1 ) = m )
31 3 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> N e. ( ZZ>= ` M ) )
32 simpr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. ( ZZ>= ` N ) )
33 12 adantr 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> M e. ZZ )
34 26 adantlr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ k e. ( ZZ>= ` M ) ) -> ( F ` k ) e. CC )
35 10 33 34 prodf 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> seq M ( x. , F ) : ( ZZ>= ` M ) --> CC )
36 35 31 ffvelrnd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) ` N ) e. CC )
37 elfzuz 
 |-  ( m e. ( ( N + 1 ) ... n ) -> m e. ( ZZ>= ` ( N + 1 ) ) )
38 eluzelz 
 |-  ( m e. ( ZZ>= ` ( N + 1 ) ) -> m e. ZZ )
39 38 adantl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( N + 1 ) ) ) -> m e. ZZ )
40 4 sseld 
 |-  ( ph -> ( m e. A -> m e. ( M ... N ) ) )
41 fznuz 
 |-  ( m e. ( M ... N ) -> -. m e. ( ZZ>= ` ( N + 1 ) ) )
42 40 41 syl6 
 |-  ( ph -> ( m e. A -> -. m e. ( ZZ>= ` ( N + 1 ) ) ) )
43 42 con2d 
 |-  ( ph -> ( m e. ( ZZ>= ` ( N + 1 ) ) -> -. m e. A ) )
44 43 imp 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( N + 1 ) ) ) -> -. m e. A )
45 39 44 eldifd 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( N + 1 ) ) ) -> m e. ( ZZ \ A ) )
46 fveqeq2 
 |-  ( k = m -> ( ( F ` k ) = 1 <-> ( F ` m ) = 1 ) )
47 eldifi 
 |-  ( k e. ( ZZ \ A ) -> k e. ZZ )
48 eldifn 
 |-  ( k e. ( ZZ \ A ) -> -. k e. A )
49 48 20 syl 
 |-  ( k e. ( ZZ \ A ) -> if ( k e. A , B , 1 ) = 1 )
50 49 21 eqeltrdi 
 |-  ( k e. ( ZZ \ A ) -> if ( k e. A , B , 1 ) e. CC )
51 47 50 24 syl2anc 
 |-  ( k e. ( ZZ \ A ) -> ( F ` k ) = if ( k e. A , B , 1 ) )
52 51 49 eqtrd 
 |-  ( k e. ( ZZ \ A ) -> ( F ` k ) = 1 )
53 46 52 vtoclga 
 |-  ( m e. ( ZZ \ A ) -> ( F ` m ) = 1 )
54 45 53 syl 
 |-  ( ( ph /\ m e. ( ZZ>= ` ( N + 1 ) ) ) -> ( F ` m ) = 1 )
55 37 54 sylan2 
 |-  ( ( ph /\ m e. ( ( N + 1 ) ... n ) ) -> ( F ` m ) = 1 )
56 55 adantlr 
 |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( F ` m ) = 1 )
57 30 31 32 36 56 seqid2 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) ` N ) = ( seq M ( x. , F ) ` n ) )
58 57 eqcomd 
 |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) ` n ) = ( seq M ( x. , F ) ` N ) )
59 5 7 9 28 58 climconst 
 |-  ( ph -> seq M ( x. , F ) ~~> ( seq M ( x. , F ) ` N ) )