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

Metamath Proof Explorer

Theorem climreclmpt

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

Ref Expression
Hypotheses climreclmpt.k ⊢ Ⅎ k φ
climreclmpt.m ⊢ φ → M ∈ ℤ
climreclmpt.z ⊢ Z = ℤ ≥ M
climreclmpt.a ⊢ φ ∧ k ∈ Z → A ∈ ℝ
climreclmpt.b ⊢ φ → k ∈ Z ⟼ A ⇝ B
Assertion climreclmpt ⊢ φ → B ∈ ℝ

Proof

Step Hyp Ref Expression
1 climreclmpt.k ⊢ Ⅎ k φ
2 climreclmpt.m ⊢ φ → M ∈ ℤ
3 climreclmpt.z ⊢ Z = ℤ ≥ M
4 climreclmpt.a ⊢ φ ∧ k ∈ Z → A ∈ ℝ
5 climreclmpt.b ⊢ φ → k ∈ Z ⟼ A ⇝ B
6 nfmpt1 ⊢ Ⅎ _ k k ∈ Z ⟼ A
7 eqidd ⊢ φ → k ∈ Z ⟼ A = k ∈ Z ⟼ A
8 7 4 fvmpt2d ⊢ φ ∧ k ∈ Z → k ∈ Z ⟼ A ⁡ k = A
9 8 4 eqeltrd ⊢ φ ∧ k ∈ Z → k ∈ Z ⟼ A ⁡ k ∈ ℝ
10 1 6 3 2 5 9 climreclf ⊢ φ → B ∈ ℝ