Theorem climreclmpt

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

	Ref	Expression
Hypotheses	climreclmpt.k	⊢ Ⅎ 𝑘 𝜑
	climreclmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climreclmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climreclmpt.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
	climreclmpt.b	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ⇝ 𝐵 )
Assertion	climreclmpt	⊢ ( 𝜑 → 𝐵 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		climreclmpt.k	⊢ Ⅎ 𝑘 𝜑
2		climreclmpt.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		climreclmpt.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		climreclmpt.a	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → 𝐴 ∈ ℝ )
5		climreclmpt.b	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ⇝ 𝐵 )
6		nfmpt1	⊢ Ⅎ 𝑘 ( 𝑘 ∈ 𝑍 ↦ 𝐴 )
7		eqidd	⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) = ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) )
8	7 4	fvmpt2d	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) = 𝐴 )
9	8 4	eqeltrd	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( ( 𝑘 ∈ 𝑍 ↦ 𝐴 ) ‘ 𝑘 ) ∈ ℝ )
10	1 6 3 2 5 9	climreclf	⊢ ( 𝜑 → 𝐵 ∈ ℝ )