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