# 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 )`
` |-  ( ( ph /\ k e. ( ZZ>= ` M ) ) -> k e. ZZ )`
15 iftrue
` |-  ( k e. A -> if ( k e. A , B , 1 ) = B )`
` |-  ( ( ( ph /\ k e. ( ZZ>= ` M ) ) /\ k e. A ) -> if ( k e. A , B , 1 ) = B )`
` |-  ( ( ( 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 )`
` |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. CC ) -> ( m x. 1 ) = m )`
` |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> N e. ( ZZ>= ` M ) )`
32 simpr
` |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> n e. ( ZZ>= ` N ) )`
` |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> M e. ZZ )`
` |-  ( ( ( 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 )`
` |-  ( ( 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 )`
` |-  ( ( ( ph /\ n e. ( ZZ>= ` N ) ) /\ m e. ( ( N + 1 ) ... n ) ) -> ( F ` m ) = 1 )`
` |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) ` N ) = ( seq M ( x. , F ) ` n ) )`
` |-  ( ( ph /\ n e. ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) ` n ) = ( seq M ( x. , F ) ` N ) )`
` |-  ( ph -> seq M ( x. , F ) ~~> ( seq M ( x. , F ) ` N ) )`