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 )
5 4 adantl 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. CC ) -> ( 1 x. n ) = n )
6 1cnd 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> 1 e. CC )
7 3 adantr 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> N e. ( ZZ>= ` M ) )
8 iftrue 
 |-  ( k e. A -> if ( k e. A , B , 1 ) = B )
9 8 adantl 
 |-  ( ( ( ph /\ k e. ZZ ) /\ k e. A ) -> if ( k e. A , B , 1 ) = B )
10 2 adantlr 
 |-  ( ( ( 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 sselid 
 |-  ( ph -> N e. ZZ )
20 17 19 ffvelrnd 
 |-  ( ph -> ( F ` N ) e. CC )
21 20 adantr 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( F ` N ) e. CC )
22 elfzelz 
 |-  ( n e. ( M ... ( N - 1 ) ) -> n e. ZZ )
23 22 adantl 
 |-  ( ( ( 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 )
26 25 adantr 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> N e. CC )
27 26 adantr 
 |-  ( ( ( 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 ) ) )
33 32 adantl 
 |-  ( ( ( 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 ) )