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

Metamath Proof Explorer

Theorem climrecl

Description: The limit of a convergent real sequence is real. Corollary 12-2.5 of Gleason p. 172. (Contributed by NM, 10-Sep-2005) (Proof shortened by Mario Carneiro, 10-May-2016)

Ref Expression
Hypotheses climshft2.1 ⊢ Z = ℤ ≥ M
climshft2.2 ⊢ φ → M ∈ ℤ
climrecl.3 ⊢ φ → F ⇝ A
climrecl.4 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
Assertion climrecl ⊢ φ → A ∈ ℝ

Proof

Step Hyp Ref Expression
1 climshft2.1 ⊢ Z = ℤ ≥ M
2 climshft2.2 ⊢ φ → M ∈ ℤ
3 climrecl.3 ⊢ φ → F ⇝ A
4 climrecl.4 ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℝ
5 1 uzsup ⊢ M ∈ ℤ → sup Z ℝ * < = +∞
6 2 5 syl ⊢ φ → sup Z ℝ * < = +∞
7 climrel ⊢ Rel ⁡ ⇝
8 7 brrelex1i ⊢ F ⇝ A → F ∈ V
9 3 8 syl ⊢ φ → F ∈ V
10 eqid ⊢ k ∈ Z ⟼ F ⁡ k = k ∈ Z ⟼ F ⁡ k
11 1 10 climmpt ⊢ M ∈ ℤ ∧ F ∈ V → F ⇝ A ↔ k ∈ Z ⟼ F ⁡ k ⇝ A
12 2 9 11 syl2anc ⊢ φ → F ⇝ A ↔ k ∈ Z ⟼ F ⁡ k ⇝ A
13 3 12 mpbid ⊢ φ → k ∈ Z ⟼ F ⁡ k ⇝ A
14 4 recnd ⊢ φ ∧ k ∈ Z → F ⁡ k ∈ ℂ
15 14 fmpttd ⊢ φ → k ∈ Z ⟼ F ⁡ k : Z ⟶ ℂ
16 1 2 15 rlimclim ⊢ φ → k ∈ Z ⟼ F ⁡ k ⇝ℝ A ↔ k ∈ Z ⟼ F ⁡ k ⇝ A
17 13 16 mpbird ⊢ φ → k ∈ Z ⟼ F ⁡ k ⇝ℝ A
18 6 17 4 rlimrecl ⊢ φ → A ∈ ℝ