Theorem climreclf

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

	Ref	Expression
Hypotheses	climreclf.k	⊢ Ⅎ 𝑘 𝜑
	climreclf.f	⊢ Ⅎ 𝑘 𝐹
	climreclf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	climreclf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	climreclf.a	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
	climreclf.r	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
Assertion	climreclf	⊢ ( 𝜑 → 𝐴 ∈ ℝ )

Proof

Step	Hyp	Ref	Expression
1		climreclf.k	⊢ Ⅎ 𝑘 𝜑
2		climreclf.f	⊢ Ⅎ 𝑘 𝐹
3		climreclf.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		climreclf.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
5		climreclf.a	⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
6		climreclf.r	⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
7		nfv	⊢ Ⅎ 𝑘 𝑗 ∈ 𝑍
8	1 7	nfan	⊢ Ⅎ 𝑘 ( 𝜑 ∧ 𝑗 ∈ 𝑍 )
9		nfcv	⊢ Ⅎ 𝑘 𝑗
10	2 9	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 )
11		nfcv	⊢ Ⅎ 𝑘 ℝ
12	10 11	nfel	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑗 ) ∈ ℝ
13	8 12	nfim	⊢ Ⅎ 𝑘 ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
14		eleq1w	⊢ ( 𝑘 = 𝑗 → ( 𝑘 ∈ 𝑍 ↔ 𝑗 ∈ 𝑍 ) )
15	14	anbi2d	⊢ ( 𝑘 = 𝑗 → ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) ↔ ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) ) )
16		fveq2	⊢ ( 𝑘 = 𝑗 → ( 𝐹 ‘ 𝑘 ) = ( 𝐹 ‘ 𝑗 ) )
17	16	eleq1d	⊢ ( 𝑘 = 𝑗 → ( ( 𝐹 ‘ 𝑘 ) ∈ ℝ ↔ ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) )
18	15 17	imbi12d	⊢ ( 𝑘 = 𝑗 → ( ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ ) ↔ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ ) ) )
19	13 18 6	chvarfv	⊢ ( ( 𝜑 ∧ 𝑗 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑗 ) ∈ ℝ )
20	3 4 5 19	climrecl	⊢ ( 𝜑 → 𝐴 ∈ ℝ )