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 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
climshft2.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
climrecl.3 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
climrecl.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
Assertion climrecl ( 𝜑 → 𝐴 ∈ ℝ )

Proof

Step Hyp Ref Expression
1 climshft2.1 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
2 climshft2.2 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 climrecl.3 ⊢ ( 𝜑 → 𝐹 ⇝ 𝐴 )
4 climrecl.4 ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ )
5 1 uzsup ⊢ ( 𝑀 ∈ ℤ → sup ( 𝑍 , ℝ* , < ) = +∞ )
6 2 5 syl ⊢ ( 𝜑 → sup ( 𝑍 , ℝ* , < ) = +∞ )
7 climrel ⊢ Rel ⇝
8 7 brrelex1i ⊢ ( 𝐹 ⇝ 𝐴 → 𝐹 ∈ V )
9 3 8 syl ⊢ ( 𝜑 → 𝐹 ∈ V )
10 eqid ⊢ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) = ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) )
11 1 10 climmpt ⊢ ( ( 𝑀 ∈ ℤ ∧ 𝐹 ∈ V ) → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ 𝐴 ) )
12 2 9 11 syl2anc ⊢ ( 𝜑 → ( 𝐹 ⇝ 𝐴 ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ 𝐴 ) )
13 3 12 mpbid ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ 𝐴 )
14 4 recnd ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℂ )
15 14 fmpttd ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) : 𝑍 ⟶ ℂ )
16 1 2 15 rlimclim ⊢ ( 𝜑 → ( ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝𝑟 𝐴 ↔ ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝ 𝐴 ) )
17 13 16 mpbird ⊢ ( 𝜑 → ( 𝑘 ∈ 𝑍 ↦ ( 𝐹 ‘ 𝑘 ) ) ⇝𝑟 𝐴 )
18 6 17 4 rlimrecl ⊢ ( 𝜑 → 𝐴 ∈ ℝ )