Theorem xlimclim2lem

Description: Lemma for xlimclim2 . Here it is additionally assumed that the sequence will eventually become (and stay) real. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step	Hyp	Ref	Expression
1		xlimclim2lem.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
2		xlimclim2lem.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
3		xlimclim2lem.a	$$⊢\phi \to A\in ℝ$$
4		xlimclim2lem.r	$$⊢\phi \to \exists j\in Z\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ$$
5	1 2	fuzxrpmcn	$$⊢\phi \to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
6	5	ad2antrr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ\right)\to F\in \left({ℝ}^{*}{\uparrow }_{𝑝𝑚}ℂ\right)$$
7	1	eluzelz2	$$⊢j\in Z\to j\in \mathbb{Z}$$
8	7	ad2antlr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ\right)\to j\in \mathbb{Z}$$
9	6 8	xlimres	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ\right)\to \left(F\underset{*}{⇝}A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)\underset{*}{⇝}A\right)$$
10		eqid	$$⊢{\mathbb{Z}}_{\ge j}={\mathbb{Z}}_{\ge j}$$
11		simpr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ\right)\to \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ$$
12	3	ad2antrr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ\right)\to A\in ℝ$$
13	8 10 11 12	xlimclim	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)\underset{*}{⇝}A\leftrightarrow \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)⇝A\right)$$
14	1	fvexi	$$⊢Z\in \mathrm{V}$$
15	14	a1i	$$⊢\phi \to Z\in \mathrm{V}$$
16	2 15	fexd	$$⊢\phi \to F\in \mathrm{V}$$
17		climres	$$⊢\left(j\in \mathbb{Z}\wedge F\in \mathrm{V}\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)⇝A\leftrightarrow F⇝A\right)$$
18	7 16 17	syl2anr	$$⊢\left(\phi \wedge j\in Z\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)⇝A\leftrightarrow F⇝A\right)$$
19	18	adantr	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ\right)\to \left(\left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right)⇝A\leftrightarrow F⇝A\right)$$
20	9 13 19	3bitrd	$$⊢\left(\left(\phi \wedge j\in Z\right)\wedge \left({F\upharpoonright }_{{\mathbb{Z}}_{\ge j}}\right):{\mathbb{Z}}_{\ge j}⟶ℝ\right)\to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$
21	20 4	r19.29a	$$⊢\phi \to \left(F\underset{*}{⇝}A\leftrightarrow F⇝A\right)$$