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={\mathbb{Z}}_{\ge M}$$
	climshft2.2	$$⊢\phi \to M\in \mathbb{Z}$$
	climrecl.3	$$⊢\phi \to F⇝A$$
	climrecl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
Assertion	climrecl	$$⊢\phi \to A\in ℝ$$

Proof

Step	Hyp	Ref	Expression
1		climshft2.1	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		climshft2.2	$$⊢\phi \to M\in \mathbb{Z}$$
3		climrecl.3	$$⊢\phi \to F⇝A$$
4		climrecl.4	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℝ$$
5	1	uzsup	$$⊢M\in \mathbb{Z}\to sup\left(Z,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
6	2 5	syl	$$⊢\phi \to sup\left(Z,{ℝ}^{*},<\right)=\mathrm{+\infty }$$
7		climrel	$$⊢\mathrm{Rel}⇝$$
8	7	brrelex1i	$$⊢F⇝A\to F\in \mathrm{V}$$
9	3 8	syl	$$⊢\phi \to F\in \mathrm{V}$$
10		eqid	$$⊢\left(k\in Z⟼F\left(k\right)\right)=\left(k\in Z⟼F\left(k\right)\right)$$
11	1 10	climmpt	$$⊢\left(M\in \mathbb{Z}\wedge F\in \mathrm{V}\right)\to \left(F⇝A\leftrightarrow \left(k\in Z⟼F\left(k\right)\right)⇝A\right)$$
12	2 9 11	syl2anc	$$⊢\phi \to \left(F⇝A\leftrightarrow \left(k\in Z⟼F\left(k\right)\right)⇝A\right)$$
13	3 12	mpbid	$$⊢\phi \to \left(k\in Z⟼F\left(k\right)\right)⇝A$$
14	4	recnd	$$⊢\left(\phi \wedge k\in Z\right)\to F\left(k\right)\in ℂ$$
15	14	fmpttd	$$⊢\phi \to \left(k\in Z⟼F\left(k\right)\right):Z⟶ℂ$$
16	1 2 15	rlimclim	$$⊢\phi \to \left(\left(k\in Z⟼F\left(k\right)\right)\underset{ℝ}{⇝}A\leftrightarrow \left(k\in Z⟼F\left(k\right)\right)⇝A\right)$$
17	13 16	mpbird	$$⊢\phi \to \left(k\in Z⟼F\left(k\right)\right)\underset{ℝ}{⇝}A$$
18	6 17 4	rlimrecl	$$⊢\phi \to A\in ℝ$$