Step |
Hyp |
Ref |
Expression |
1 |
|
climmpt2.1 |
|- Z = ( ZZ>= ` M ) |
2 |
|
climmpt2.2 |
|- ( ph -> M e. ZZ ) |
3 |
|
climmpt2.3 |
|- ( ph -> F e. V ) |
4 |
|
climmpt2.5 |
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC ) |
5 |
|
eqid |
|- ( n e. Z |-> ( F ` n ) ) = ( n e. Z |-> ( F ` n ) ) |
6 |
1 5
|
climmpt |
|- ( ( M e. ZZ /\ F e. V ) -> ( F ~~> A <-> ( n e. Z |-> ( F ` n ) ) ~~> A ) ) |
7 |
2 3 6
|
syl2anc |
|- ( ph -> ( F ~~> A <-> ( n e. Z |-> ( F ` n ) ) ~~> A ) ) |
8 |
4
|
ralrimiva |
|- ( ph -> A. k e. Z ( F ` k ) e. CC ) |
9 |
|
fveq2 |
|- ( k = m -> ( F ` k ) = ( F ` m ) ) |
10 |
9
|
eleq1d |
|- ( k = m -> ( ( F ` k ) e. CC <-> ( F ` m ) e. CC ) ) |
11 |
10
|
cbvralvw |
|- ( A. k e. Z ( F ` k ) e. CC <-> A. m e. Z ( F ` m ) e. CC ) |
12 |
|
fveq2 |
|- ( m = n -> ( F ` m ) = ( F ` n ) ) |
13 |
12
|
eleq1d |
|- ( m = n -> ( ( F ` m ) e. CC <-> ( F ` n ) e. CC ) ) |
14 |
13
|
cbvralvw |
|- ( A. m e. Z ( F ` m ) e. CC <-> A. n e. Z ( F ` n ) e. CC ) |
15 |
11 14
|
bitri |
|- ( A. k e. Z ( F ` k ) e. CC <-> A. n e. Z ( F ` n ) e. CC ) |
16 |
8 15
|
sylib |
|- ( ph -> A. n e. Z ( F ` n ) e. CC ) |
17 |
16
|
r19.21bi |
|- ( ( ph /\ n e. Z ) -> ( F ` n ) e. CC ) |
18 |
17
|
fmpttd |
|- ( ph -> ( n e. Z |-> ( F ` n ) ) : Z --> CC ) |
19 |
1 2 18
|
rlimclim |
|- ( ph -> ( ( n e. Z |-> ( F ` n ) ) ~~>r A <-> ( n e. Z |-> ( F ` n ) ) ~~> A ) ) |
20 |
7 19
|
bitr4d |
|- ( ph -> ( F ~~> A <-> ( n e. Z |-> ( F ` n ) ) ~~>r A ) ) |