Theorem climreclf

Description: The limit of a convergent real sequence is real. (Contributed by Glauco Siliprandi, 26-Jun-2021)

	Ref	Expression
Hypotheses	climreclf.k	|- F/ k ph
	climreclf.f	|- F/_ k F
	climreclf.z	|- Z = ( ZZ>= ` M )
	climreclf.m	|- ( ph -> M e. ZZ )
	climreclf.a	|- ( ph -> F ~~> A )
	climreclf.r	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
Assertion	climreclf	|- ( ph -> A e. RR )

Proof

Step	Hyp	Ref	Expression
1		climreclf.k	|- F/ k ph
2		climreclf.f	|- F/_ k F
3		climreclf.z	|- Z = ( ZZ>= ` M )
4		climreclf.m	|- ( ph -> M e. ZZ )
5		climreclf.a	|- ( ph -> F ~~> A )
6		climreclf.r	|- ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR )
7		nfv	|- F/ k j e. Z
8	1 7	nfan	|- F/ k ( ph /\ j e. Z )
9		nfcv	|- F/_ k j
10	2 9	nffv	|- F/_ k ( F ` j )
11		nfcv	|- F/_ k RR
12	10 11	nfel	|- F/ k ( F ` j ) e. RR
13	8 12	nfim	|- F/ k ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR )
14		eleq1w	|- ( k = j -> ( k e. Z <-> j e. Z ) )
15	14	anbi2d	|- ( k = j -> ( ( ph /\ k e. Z ) <-> ( ph /\ j e. Z ) ) )
16		fveq2	|- ( k = j -> ( F ` k ) = ( F ` j ) )
17	16	eleq1d	|- ( k = j -> ( ( F ` k ) e. RR <-> ( F ` j ) e. RR ) )
18	15 17	imbi12d	|- ( k = j -> ( ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR ) <-> ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR ) ) )
19	13 18 6	chvarfv	|- ( ( ph /\ j e. Z ) -> ( F ` j ) e. RR )
20	3 4 5 19	climrecl	|- ( ph -> A e. RR )