Metamath Proof Explorer

Theorem isercolllem3

Description: Lemma for isercoll . (Contributed by Mario Carneiro, 6-Apr-2015)

Ref Expression
Hypotheses isercoll.z 
|- Z = ( ZZ>= ` M )
isercoll.m 
|- ( ph -> M e. ZZ )
isercoll.g 
|- ( ph -> G : NN --> Z )
isercoll.i 
|- ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
isercoll.0 
|- ( ( ph /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )
isercoll.f 
|- ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC )
isercoll.h 
|- ( ( ph /\ k e. NN ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
Assertion isercolllem3 
|- ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( seq M ( + , F ) ` N ) = ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) )

Proof

Step Hyp Ref Expression
1 isercoll.z 
 |-  Z = ( ZZ>= ` M )
2 isercoll.m 
 |-  ( ph -> M e. ZZ )
3 isercoll.g 
 |-  ( ph -> G : NN --> Z )
4 isercoll.i 
 |-  ( ( ph /\ k e. NN ) -> ( G ` k ) < ( G ` ( k + 1 ) ) )
5 isercoll.0 
 |-  ( ( ph /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )
6 isercoll.f 
 |-  ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC )
7 isercoll.h 
 |-  ( ( ph /\ k e. NN ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
8 addlid 
 |-  ( n e. CC -> ( 0 + n ) = n )
9 8 adantl 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ n e. CC ) -> ( 0 + n ) = n )
10 addrid 
 |-  ( n e. CC -> ( n + 0 ) = n )
11 10 adantl 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ n e. CC ) -> ( n + 0 ) = n )
12 addcl 
 |-  ( ( n e. CC /\ k e. CC ) -> ( n + k ) e. CC )
13 12 adantl 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ ( n e. CC /\ k e. CC ) ) -> ( n + k ) e. CC )
14 0cnd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> 0 e. CC )
15 cnvimass 
 |-  ( `' G " ( M ... N ) ) C_ dom G
16 3 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> G : NN --> Z )
17 15 16 fssdm 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) C_ NN )
18 1 2 3 4 isercolllem1 
 |-  ( ( ph /\ ( `' G " ( M ... N ) ) C_ NN ) -> ( G |` ( `' G " ( M ... N ) ) ) Isom < , < ( ( `' G " ( M ... N ) ) , ( G " ( `' G " ( M ... N ) ) ) ) )
19 17 18 syldan 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G |` ( `' G " ( M ... N ) ) ) Isom < , < ( ( `' G " ( M ... N ) ) , ( G " ( `' G " ( M ... N ) ) ) ) )
20 1 2 3 4 isercolllem2 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) = ( `' G " ( M ... N ) ) )
21 isoeq4 
 |-  ( ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) = ( `' G " ( M ... N ) ) -> ( ( G |` ( `' G " ( M ... N ) ) ) Isom < , < ( ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) , ( G " ( `' G " ( M ... N ) ) ) ) <-> ( G |` ( `' G " ( M ... N ) ) ) Isom < , < ( ( `' G " ( M ... N ) ) , ( G " ( `' G " ( M ... N ) ) ) ) ) )
22 20 21 syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( ( G |` ( `' G " ( M ... N ) ) ) Isom < , < ( ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) , ( G " ( `' G " ( M ... N ) ) ) ) <-> ( G |` ( `' G " ( M ... N ) ) ) Isom < , < ( ( `' G " ( M ... N ) ) , ( G " ( `' G " ( M ... N ) ) ) ) ) )
23 19 22 mpbird 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G |` ( `' G " ( M ... N ) ) ) Isom < , < ( ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) , ( G " ( `' G " ( M ... N ) ) ) ) )
24 15 a1i 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) C_ dom G )
25 sseqin2 
 |-  ( ( `' G " ( M ... N ) ) C_ dom G <-> ( dom G i^i ( `' G " ( M ... N ) ) ) = ( `' G " ( M ... N ) ) )
26 24 25 sylib 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( dom G i^i ( `' G " ( M ... N ) ) ) = ( `' G " ( M ... N ) ) )
27 1nn 
 |-  1 e. NN
28 27 a1i 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> 1 e. NN )
29 ffvelcdm 
 |-  ( ( G : NN --> Z /\ 1 e. NN ) -> ( G ` 1 ) e. Z )
30 3 27 29 sylancl 
 |-  ( ph -> ( G ` 1 ) e. Z )
31 30 1 eleqtrdi 
 |-  ( ph -> ( G ` 1 ) e. ( ZZ>= ` M ) )
32 31 adantr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` 1 ) e. ( ZZ>= ` M ) )
33 simpr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> N e. ( ZZ>= ` ( G ` 1 ) ) )
34 elfzuzb 
 |-  ( ( G ` 1 ) e. ( M ... N ) <-> ( ( G ` 1 ) e. ( ZZ>= ` M ) /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) )
35 32 33 34 sylanbrc 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G ` 1 ) e. ( M ... N ) )
36 ffn 
 |-  ( G : NN --> Z -> G Fn NN )
37 elpreima 
 |-  ( G Fn NN -> ( 1 e. ( `' G " ( M ... N ) ) <-> ( 1 e. NN /\ ( G ` 1 ) e. ( M ... N ) ) ) )
38 16 36 37 3syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( 1 e. ( `' G " ( M ... N ) ) <-> ( 1 e. NN /\ ( G ` 1 ) e. ( M ... N ) ) ) )
39 28 35 38 mpbir2and 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> 1 e. ( `' G " ( M ... N ) ) )
40 39 ne0d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( `' G " ( M ... N ) ) =/= (/) )
41 26 40 eqnetrd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( dom G i^i ( `' G " ( M ... N ) ) ) =/= (/) )
42 imadisj 
 |-  ( ( G " ( `' G " ( M ... N ) ) ) = (/) <-> ( dom G i^i ( `' G " ( M ... N ) ) ) = (/) )
43 42 necon3bii 
 |-  ( ( G " ( `' G " ( M ... N ) ) ) =/= (/) <-> ( dom G i^i ( `' G " ( M ... N ) ) ) =/= (/) )
44 41 43 sylibr 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... N ) ) ) =/= (/) )
45 ffun 
 |-  ( G : NN --> Z -> Fun G )
46 funimacnv 
 |-  ( Fun G -> ( G " ( `' G " ( M ... N ) ) ) = ( ( M ... N ) i^i ran G ) )
47 16 45 46 3syl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... N ) ) ) = ( ( M ... N ) i^i ran G ) )
48 inss1 
 |-  ( ( M ... N ) i^i ran G ) C_ ( M ... N )
49 47 48 eqsstrdi 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( G " ( `' G " ( M ... N ) ) ) C_ ( M ... N ) )
50 simpl 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ph )
51 elfzuz 
 |-  ( n e. ( M ... N ) -> n e. ( ZZ>= ` M ) )
52 51 1 eleqtrrdi 
 |-  ( n e. ( M ... N ) -> n e. Z )
53 50 52 6 syl2an 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ n e. ( M ... N ) ) -> ( F ` n ) e. CC )
54 47 difeq2d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( ( M ... N ) \ ( G " ( `' G " ( M ... N ) ) ) ) = ( ( M ... N ) \ ( ( M ... N ) i^i ran G ) ) )
55 difin 
 |-  ( ( M ... N ) \ ( ( M ... N ) i^i ran G ) ) = ( ( M ... N ) \ ran G )
56 54 55 eqtrdi 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( ( M ... N ) \ ( G " ( `' G " ( M ... N ) ) ) ) = ( ( M ... N ) \ ran G ) )
57 52 ssriv 
 |-  ( M ... N ) C_ Z
58 ssdif 
 |-  ( ( M ... N ) C_ Z -> ( ( M ... N ) \ ran G ) C_ ( Z \ ran G ) )
59 57 58 mp1i 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( ( M ... N ) \ ran G ) C_ ( Z \ ran G ) )
60 56 59 eqsstrd 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( ( M ... N ) \ ( G " ( `' G " ( M ... N ) ) ) ) C_ ( Z \ ran G ) )
61 60 sselda 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ n e. ( ( M ... N ) \ ( G " ( `' G " ( M ... N ) ) ) ) ) -> n e. ( Z \ ran G ) )
62 5 adantlr 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ n e. ( Z \ ran G ) ) -> ( F ` n ) = 0 )
63 61 62 syldan 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ n e. ( ( M ... N ) \ ( G " ( `' G " ( M ... N ) ) ) ) ) -> ( F ` n ) = 0 )
64 elfznn 
 |-  ( k e. ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) -> k e. NN )
65 50 64 7 syl2an 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) ) -> ( H ` k ) = ( F ` ( G ` k ) ) )
66 20 eleq2d 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( k e. ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) <-> k e. ( `' G " ( M ... N ) ) ) )
67 66 biimpa 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) ) -> k e. ( `' G " ( M ... N ) ) )
68 67 fvresd 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) ) -> ( ( G |` ( `' G " ( M ... N ) ) ) ` k ) = ( G ` k ) )
69 68 fveq2d 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) ) -> ( F ` ( ( G |` ( `' G " ( M ... N ) ) ) ` k ) ) = ( F ` ( G ` k ) ) )
70 65 69 eqtr4d 
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ k e. ( 1 ... ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) ) -> ( H ` k ) = ( F ` ( ( G |` ( `' G " ( M ... N ) ) ) ` k ) ) )
71 9 11 13 14 23 44 49 53 63 70 seqcoll2 
 |-  ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) -> ( seq M ( + , F ) ` N ) = ( seq 1 ( + , H ) ` ( # ` ( G " ( `' G " ( M ... N ) ) ) ) ) )