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