Metamath Proof Explorer


Theorem climmpt2

Description: Relate an integer limit on a not-quite-function to a real limit. (Contributed by Mario Carneiro, 17-Sep-2014)

Ref Expression
Hypotheses climmpt2.1
|- Z = ( ZZ>= ` M )
climmpt2.2
|- ( ph -> M e. ZZ )
climmpt2.3
|- ( ph -> F e. V )
climmpt2.5
|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
Assertion climmpt2
|- ( ph -> ( F ~~> A <-> ( n e. Z |-> ( F ` n ) ) ~~>r A ) )

Proof

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