This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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