This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

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