Theorem xlimclim2

Description: Given a sequence of extended reals, it converges to a real number A w.r.t. the standard topology on the reals (see climreeq ), if and only if it converges to A w.r.t. to the standard topology on the extended reals. In order for the first part of the statement to even make sense, the sequence will of course eventually become (and stay) real: showing this, is the key step of the proof. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimclim2.m	$$⊢\phi \to M\in \mathbb{Z}$$
	xlimclim2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimclim2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
	xlimclim2.a	$$⊢\phi \to A\in ℝ$$
Assertion	xlimclim2	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$

Proof

Step	Hyp	Ref	Expression
1		xlimclim2.m	$$⊢\phi \to M\in \mathbb{Z}$$
2		xlimclim2.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
3		xlimclim2.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
4		xlimclim2.a	$$⊢\phi \to A\in ℝ$$
5		simpr	$$⊢\left(\phi \wedge F\underset{*}{⇝}A\right)\to F\underset{*}{⇝}A$$
6	3	adantr	$$⊢\left(\phi \wedge F\underset{*}{⇝}A\right)\to F:Z⟶{ℝ}^{*}$$
7	4	adantr	$$⊢\left(\phi \wedge F\underset{*}{⇝}A\right)\to A\in ℝ$$
8	1	adantr	$$⊢\left(\phi \wedge F\underset{*}{⇝}A\right)\to M\in \mathbb{Z}$$
9	8 2 6 7 5	xlimxrre	$$⊢\left(\phi \wedge F\underset{*}{⇝}A\right)\to \exists j\in Z\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ$$
10	2 6 7 9	xlimclim2lem	$$⊢\left(\phi \wedge F\underset{*}{⇝}A\right)\to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$
11	5 10	mpbid	$$⊢\left(\phi \wedge F\underset{*}{⇝}A\right)\to F⇝A$$
12		simpr	$$⊢\left(\phi \wedge F⇝A\right)\to F⇝A$$
13	3	adantr	$$⊢\left(\phi \wedge F⇝A\right)\to F:Z⟶{ℝ}^{*}$$
14	4	adantr	$$⊢\left(\phi \wedge F⇝A\right)\to A\in ℝ$$
15	1	adantr	$$⊢\left(\phi \wedge F⇝A\right)\to M\in \mathbb{Z}$$
16	15 2 13 14 12	climxrre	$$⊢\left(\phi \wedge F⇝A\right)\to \exists j\in Z\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ$$
17	2 13 14 16	xlimclim2lem	$$⊢\left(\phi \wedge F⇝A\right)\to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$
18	12 17	mpbird	$$⊢\left(\phi \wedge F⇝A\right)\to F\underset{*}{⇝}A$$
19	11 18	impbida	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$