Theorem climrecl

Description: The limit of a convergent real sequence is real. Corollary 12-2.5 of Gleason p. 172. (Contributed by NM, 10-Sep-2005) (Proof shortened by Mario Carneiro, 10-May-2016)

	Ref	Expression
Hypotheses	climshft2.1	|- Z = ( ZZ>= ` M )
	climshft2.2	|- ( ph -> M e. ZZ )
	climrecl.3	|- ( ph -> F ~~> A )
	climrecl.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
Assertion	climrecl	|- ( ph -> A e. RR )

Proof

Step	Hyp	Ref	Expression
1		climshft2.1	|- Z = ( ZZ>= ` M )
2		climshft2.2	|- ( ph -> M e. ZZ )
3		climrecl.3	|- ( ph -> F ~~> A )
4		climrecl.4	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
5	1	uzsup	|- ( M e. ZZ -> sup ( Z , RR* , < ) = +oo )
6	2 5	syl	|- ( ph -> sup ( Z , RR* , < ) = +oo )
7		climrel	|- Rel ~~>
8	7	brrelex1i	|- ( F ~~> A -> F e. _V )
9	3 8	syl	|- ( ph -> F e. _V )
10		eqid	|- ( k e. Z |-> ( F ` k ) ) = ( k e. Z |-> ( F ` k ) )
11	1 10	climmpt	|- ( ( M e. ZZ /\ F e. _V ) -> ( F ~~> A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
12	2 9 11	syl2anc	|- ( ph -> ( F ~~> A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
13	3 12	mpbid	|- ( ph -> ( k e. Z |-> ( F ` k ) ) ~~> A )
14	4	recnd	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. CC )
15	14	fmpttd	|- ( ph -> ( k e. Z |-> ( F ` k ) ) : Z --> CC )
16	1 2 15	rlimclim	|- ( ph -> ( ( k e. Z |-> ( F ` k ) ) ~~>r A <-> ( k e. Z |-> ( F ` k ) ) ~~> A ) )
17	13 16	mpbird	|- ( ph -> ( k e. Z |-> ( F ` k ) ) ~~>r A )
18	6 17 4	rlimrecl	|- ( ph -> A e. RR )