# Metamath Proof Explorer

## Theorem prodrblem

Description: Lemma for prodrb . (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 ) )`
Assertion prodrblem
`|- ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) = seq N ( x. , F ) )`

### 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 mulid2
` |-  ( n e. CC -> ( 1 x. n ) = n )`
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. CC ) -> ( 1 x. n ) = n )`
6 1cnd
` |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> 1 e. CC )`
` |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> N e. ( ZZ>= ` M ) )`
8 iftrue
` |-  ( k e. A -> if ( k e. A , B , 1 ) = B )`
` |-  ( ( ( ph /\ k e. ZZ ) /\ k e. A ) -> if ( k e. A , B , 1 ) = B )`
` |-  ( ( ( ph /\ k e. ZZ ) /\ k e. A ) -> B e. CC )`
11 9 10 eqeltrd
` |-  ( ( ( ph /\ k e. ZZ ) /\ k e. A ) -> if ( k e. A , B , 1 ) e. CC )`
12 11 ex
` |-  ( ( ph /\ k e. ZZ ) -> ( k e. A -> if ( k e. A , B , 1 ) e. CC ) )`
13 iffalse
` |-  ( -. k e. A -> if ( k e. A , B , 1 ) = 1 )`
14 ax-1cn
` |-  1 e. CC`
15 13 14 eqeltrdi
` |-  ( -. k e. A -> if ( k e. A , B , 1 ) e. CC )`
16 12 15 pm2.61d1
` |-  ( ( ph /\ k e. ZZ ) -> if ( k e. A , B , 1 ) e. CC )`
17 16 1 fmptd
` |-  ( ph -> F : ZZ --> CC )`
18 uzssz
` |-  ( ZZ>= ` M ) C_ ZZ`
19 18 3 sseldi
` |-  ( ph -> N e. ZZ )`
20 17 19 ffvelrnd
` |-  ( ph -> ( F ` N ) e. CC )`
` |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( F ` N ) e. CC )`
22 elfzelz
` |-  ( n e. ( M ... ( N - 1 ) ) -> n e. ZZ )`
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> n e. ZZ )`
24 simplr
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> A C_ ( ZZ>= ` N ) )`
25 19 zcnd
` |-  ( ph -> N e. CC )`
` |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> N e. CC )`
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> N e. CC )`
28 1cnd
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> 1 e. CC )`
29 27 28 npcand
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )`
30 29 fveq2d
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) = ( ZZ>= ` N ) )`
31 24 30 sseqtrrd
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> A C_ ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )`
32 fznuz
` |-  ( n e. ( M ... ( N - 1 ) ) -> -. n e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )`
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> -. n e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )`
34 31 33 ssneldd
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> -. n e. A )`
35 23 34 eldifd
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> n e. ( ZZ \ A ) )`
36 fveqeq2
` |-  ( k = n -> ( ( F ` k ) = 1 <-> ( F ` n ) = 1 ) )`
37 eldifi
` |-  ( k e. ( ZZ \ A ) -> k e. ZZ )`
38 eldifn
` |-  ( k e. ( ZZ \ A ) -> -. k e. A )`
39 38 13 syl
` |-  ( k e. ( ZZ \ A ) -> if ( k e. A , B , 1 ) = 1 )`
40 39 14 eqeltrdi
` |-  ( k e. ( ZZ \ A ) -> if ( k e. A , B , 1 ) e. CC )`
41 1 fvmpt2
` |-  ( ( k e. ZZ /\ if ( k e. A , B , 1 ) e. CC ) -> ( F ` k ) = if ( k e. A , B , 1 ) )`
42 37 40 41 syl2anc
` |-  ( k e. ( ZZ \ A ) -> ( F ` k ) = if ( k e. A , B , 1 ) )`
43 42 39 eqtrd
` |-  ( k e. ( ZZ \ A ) -> ( F ` k ) = 1 )`
44 36 43 vtoclga
` |-  ( n e. ( ZZ \ A ) -> ( F ` n ) = 1 )`
45 35 44 syl
` |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> ( F ` n ) = 1 )`
46 5 6 7 21 45 seqid
` |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( x. , F ) |` ( ZZ>= ` N ) ) = seq N ( x. , F ) )`