Theorem climreclmpt

Description: The limit of B convergent real sequence is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	climreclmpt.k	$$⊢Ⅎk\phi$$
	climreclmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	climreclmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	climreclmpt.a	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
	climreclmpt.b	$$⊢\phi \to \left(k\in Z⟼A\right)⇝B$$
Assertion	climreclmpt	$$⊢\phi \to B\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		climreclmpt.k	$$⊢Ⅎk\phi$$
2		climreclmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		climreclmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		climreclmpt.a	$$⊢\left(\phi \wedge k\in Z\right)\to A\in ℝ$$
5		climreclmpt.b	$$⊢\phi \to \left(k\in Z⟼A\right)⇝B$$
6		nfmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in Z⟼A\right)$$
7		eqidd	$$⊢\phi \to \left(k\in Z⟼A\right)=\left(k\in Z⟼A\right)$$
8	7 4	fvmpt2d	$$⊢\left(\phi \wedge k\in Z\right)\to \left(k\in Z⟼A\right)\left(k\right)=A$$
9	8 4	eqeltrd	$$⊢\left(\phi \wedge k\in Z\right)\to \left(k\in Z⟼A\right)\left(k\right)\in ℝ$$
10	1 6 3 2 5 9	climreclf	$$⊢\phi \to B\in ℝ$$