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 ) ) ) ) ) ) |