Metamath Proof Explorer


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 ( 𝜑𝐴 ∈ ℝ )