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 addid2
 |-  ( n e. CC -> ( 0 + n ) = n )
9 8 adantl
 |-  ( ( ( ph /\ N e. ( ZZ>= ` ( G ` 1 ) ) ) /\ n e. CC ) -> ( 0 + n ) = n )
10 addid1
 |-  ( 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 ffvelrn
 |-  ( ( 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 ) ) ) ) ) )