Metamath Proof Explorer

Theorem sumrblem

Description: Lemma for sumrb . (Contributed by Mario Carneiro, 12-Aug-2013)

Ref Expression
Hypotheses summo.1 
|- F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
summo.2 
|- ( ( ph /\ k e. A ) -> B e. CC )
sumrb.3 
|- ( ph -> N e. ( ZZ>= ` M ) )
Assertion sumrblem 
|- ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( + , F ) |` ( ZZ>= ` N ) ) = seq N ( + , F ) )

Proof

Step Hyp Ref Expression
1 summo.1 
 |-  F = ( k e. ZZ |-> if ( k e. A , B , 0 ) )
2 summo.2 
 |-  ( ( ph /\ k e. A ) -> B e. CC )
3 sumrb.3 
 |-  ( ph -> N e. ( ZZ>= ` M ) )
4 addid2 
 |-  ( n e. CC -> ( 0 + n ) = n )
5 4 adantl 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. CC ) -> ( 0 + n ) = n )
6 0cnd 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> 0 e. CC )
7 3 adantr 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> N e. ( ZZ>= ` M ) )
8 iftrue 
 |-  ( k e. A -> if ( k e. A , B , 0 ) = B )
9 8 adantl 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) = B )
10 9 2 eqeltrd 
 |-  ( ( ph /\ k e. A ) -> if ( k e. A , B , 0 ) e. CC )
11 10 ex 
 |-  ( ph -> ( k e. A -> if ( k e. A , B , 0 ) e. CC ) )
12 iffalse 
 |-  ( -. k e. A -> if ( k e. A , B , 0 ) = 0 )
13 0cn 
 |-  0 e. CC
14 12 13 eqeltrdi 
 |-  ( -. k e. A -> if ( k e. A , B , 0 ) e. CC )
15 11 14 pm2.61d1 
 |-  ( ph -> if ( k e. A , B , 0 ) e. CC )
16 15 adantr 
 |-  ( ( ph /\ k e. ZZ ) -> if ( k e. A , B , 0 ) e. CC )
17 16 1 fmptd 
 |-  ( ph -> F : ZZ --> CC )
18 17 adantr 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> F : ZZ --> CC )
19 eluzelz 
 |-  ( N e. ( ZZ>= ` M ) -> N e. ZZ )
20 3 19 syl 
 |-  ( ph -> N e. ZZ )
21 20 adantr 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> N e. ZZ )
22 18 21 ffvelrnd 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( F ` N ) e. CC )
23 elfzelz 
 |-  ( n e. ( M ... ( N - 1 ) ) -> n e. ZZ )
24 23 adantl 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> n e. ZZ )
25 simplr 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> A C_ ( ZZ>= ` N ) )
26 20 zcnd 
 |-  ( ph -> N e. CC )
27 26 ad2antrr 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> N e. CC )
28 ax-1cn 
 |-  1 e. CC
29 npcan 
 |-  ( ( N e. CC /\ 1 e. CC ) -> ( ( N - 1 ) + 1 ) = N )
30 27 28 29 sylancl 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> ( ( N - 1 ) + 1 ) = N )
31 30 fveq2d 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> ( ZZ>= ` ( ( N - 1 ) + 1 ) ) = ( ZZ>= ` N ) )
32 25 31 sseqtrrd 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> A C_ ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
33 fznuz 
 |-  ( n e. ( M ... ( N - 1 ) ) -> -. n e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
34 33 adantl 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> -. n e. ( ZZ>= ` ( ( N - 1 ) + 1 ) ) )
35 32 34 ssneldd 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> -. n e. A )
36 24 35 eldifd 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> n e. ( ZZ \ A ) )
37 fveqeq2 
 |-  ( k = n -> ( ( F ` k ) = 0 <-> ( F ` n ) = 0 ) )
38 eldifi 
 |-  ( k e. ( ZZ \ A ) -> k e. ZZ )
39 eldifn 
 |-  ( k e. ( ZZ \ A ) -> -. k e. A )
40 39 12 syl 
 |-  ( k e. ( ZZ \ A ) -> if ( k e. A , B , 0 ) = 0 )
41 40 13 eqeltrdi 
 |-  ( k e. ( ZZ \ A ) -> if ( k e. A , B , 0 ) e. CC )
42 1 fvmpt2 
 |-  ( ( k e. ZZ /\ if ( k e. A , B , 0 ) e. CC ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
43 38 41 42 syl2anc 
 |-  ( k e. ( ZZ \ A ) -> ( F ` k ) = if ( k e. A , B , 0 ) )
44 43 40 eqtrd 
 |-  ( k e. ( ZZ \ A ) -> ( F ` k ) = 0 )
45 37 44 vtoclga 
 |-  ( n e. ( ZZ \ A ) -> ( F ` n ) = 0 )
46 36 45 syl 
 |-  ( ( ( ph /\ A C_ ( ZZ>= ` N ) ) /\ n e. ( M ... ( N - 1 ) ) ) -> ( F ` n ) = 0 )
47 5 6 7 22 46 seqid 
 |-  ( ( ph /\ A C_ ( ZZ>= ` N ) ) -> ( seq M ( + , F ) |` ( ZZ>= ` N ) ) = seq N ( + , F ) )