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 ⊢ Ⅎ k φ
climreclf.f ⊢ Ⅎ _ k F
climreclf.z ⊢ Z = ℤ ≥ M
climreclf.m ⊢ φ → M ∈ ℤ
climreclf.a ⊢ φ → F ⇝ A
climreclf.r ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
Assertion climreclf ⊢ φ → A ∈ ℝ

Proof

Step Hyp Ref Expression
1 climreclf.k ⊢ Ⅎ k φ
2 climreclf.f ⊢ Ⅎ _ k F
3 climreclf.z ⊢ Z = ℤ ≥ M
4 climreclf.m ⊢ φ → M ∈ ℤ
5 climreclf.a ⊢ φ → F ⇝ A
6 climreclf.r ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
7 nfv ⊢ Ⅎ k j ∈ Z
8 1 7 nfan ⊢ Ⅎ k φ ∧ j ∈ Z
9 nfcv ⊢ Ⅎ _ k j
10 2 9 nffv ⊢ Ⅎ _ k F ⁡ j
11 nfcv ⊢ Ⅎ _ k ℝ
12 10 11 nfel ⊢ Ⅎ k F ⁡ j ∈ ℝ
13 8 12 nfim ⊢ Ⅎ k φ ∧ j ∈ Z → F ⁡ j ∈ ℝ
14 eleq1w ⊢ k = j → k ∈ Z ↔ j ∈ Z
15 14 anbi2d ⊢ k = j → φ ∧ k ∈ Z ↔ φ ∧ j ∈ Z
16 fveq2 ⊢ k = j → F ⁡ k = F ⁡ j
17 16 eleq1d ⊢ k = j → F ⁡ k ∈ ℝ ↔ F ⁡ j ∈ ℝ
18 15 17 imbi12d ⊢ k = j → φ ∧ k ∈ Z → F ⁡ k ∈ ℝ ↔ φ ∧ j ∈ Z → F ⁡ j ∈ ℝ
19 13 18 6 chvarfv ⊢ φ ∧ j ∈ Z → F ⁡ j ∈ ℝ
20 3 4 5 19 climrecl ⊢ φ → A ∈ ℝ