Theorem climreclf

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

	Ref	Expression
Hypotheses	climreclf.k	$$⊢Ⅎk\phi$$
	climreclf.f	$$⊢\underset{\_}{Ⅎ}kF$$
	climreclf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climreclf.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climreclf.a	$$⊢\phi \to F⇝A$$
	climreclf.r	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
Assertion	climreclf	$$⊢\phi \to A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		climreclf.k	$$⊢Ⅎk\phi$$
2		climreclf.f	$$⊢\underset{\_}{Ⅎ}kF$$
3		climreclf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		climreclf.m	$$⊢\phi \to M\in \mathbb{Z}$$
5		climreclf.a	$$⊢\phi \to F⇝A$$
6		climreclf.r	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
7		nfv	$$⊢Ⅎkj\in Z$$
8	1 7	nfan	$$⊢Ⅎk\left(\phi \wedge j\in Z\right)$$
9		nfcv	$$⊢\underset{\_}{Ⅎ}kj$$
10	2 9	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(j\right)$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}kℝ$$
12	10 11	nfel	$$⊢ℲkF\left(j\right)\in ℝ$$
13	8 12	nfim	$$⊢Ⅎk\left(\left(\phi \wedge j\in Z\right)\to F\left(j\right)\in ℝ\right)$$
14		eleq1w	$$⊢k=j\to \left(k\in Z\leftrightarrow j\in Z\right)$$
15	14	anbi2d	$$⊢k=j\to \left(\left(\phi \wedge k\in Z\right)\leftrightarrow \left(\phi \wedge j\in Z\right)\right)$$
16		fveq2	$$⊢k=j\to F\left(k\right)=F\left(j\right)$$
17	16	eleq1d	$$⊢k=j\to \left(F\left(k\right)\in ℝ\leftrightarrow F\left(j\right)\in ℝ\right)$$
18	15 17	imbi12d	$$⊢k=j\to \left(\left(\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ\right)\leftrightarrow \left(\left(\phi \wedge j\in Z\right)\to F\left(j\right)\in ℝ\right)\right)$$
19	13 18 6	chvarfv	$$⊢\left(\phi \wedge j\in Z\right)\to F\left(j\right)\in ℝ$$
20	3 4 5 19	climrecl	$$⊢\phi \to A\in ℝ$$