Theorem xlimmnfmpt

Description: A function converges to plus infinity if it eventually becomes (and stays) larger than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022)

	Ref	Expression
Hypotheses	xlimmnfmpt.k	$$⊢Ⅎk\phi$$
	xlimmnfmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	xlimmnfmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimmnfmpt.b	$$⊢\left(\phi \wedge k\in Z\right)\to B\in {ℝ}^{*}$$
	xlimmnfmpt.f	$$⊢F=\left(k\in Z⟼B\right)$$
Assertion	xlimmnfmpt	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}B\le x\right)$$

Proof

Step	Hyp	Ref	Expression
1		xlimmnfmpt.k	$$⊢Ⅎk\phi$$
2		xlimmnfmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		xlimmnfmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		xlimmnfmpt.b	$$⊢\left(\phi \wedge k\in Z\right)\to B\in {ℝ}^{*}$$
5		xlimmnfmpt.f	$$⊢F=\left(k\in Z⟼B\right)$$
6		nfmpt1	$$⊢\underset{\_}{Ⅎ}k\left(k\in Z⟼B\right)$$
7	5 6	nfcxfr	$$⊢\underset{\_}{Ⅎ}kF$$
8	1 4 5	fmptdf	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
9	7 2 3 8	xlimmnf	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{-\infty }\leftrightarrow \forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}F\left(k\right)\le y\right)$$
10		nfv	$$⊢Ⅎki\in Z$$
11	1 10	nfan	$$⊢Ⅎk\left(\phi \wedge i\in Z\right)$$
12	3	uztrn2	$$⊢\left(i\in Z\wedge k\in {\mathbb{Z}}_{\ge i}\right)\to k\in Z$$
13	12	adantll	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge i}\right)\to k\in Z$$
14		simpll	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge i}\right)\to \phi$$
15	14 13 4	syl2anc	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge i}\right)\to B\in {ℝ}^{*}$$
16	5	fvmpt2	$$⊢\left(k\in Z\wedge B\in {ℝ}^{*}\right)\to F\left(k\right)=B$$
17	13 15 16	syl2anc	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge i}\right)\to F\left(k\right)=B$$
18	17	breq1d	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge i}\right)\to \left(F\left(k\right)\le y\leftrightarrow B\le y\right)$$
19	11 18	ralbida	$$⊢\left(\phi \wedge i\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge i}F\left(k\right)\le y\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge i}B\le y\right)$$
20	19	rexbidva	$$⊢\phi \to \left(\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}F\left(k\right)\le y\leftrightarrow \exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}B\le y\right)$$
21	20	ralbidv	$$⊢\phi \to \left(\forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}F\left(k\right)\le y\leftrightarrow \forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}B\le y\right)$$
22		breq2	$$⊢y=x\to \left(B\le y\leftrightarrow B\le x\right)$$
23	22	rexralbidv	$$⊢y=x\to \left(\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}B\le y\leftrightarrow \exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}B\le x\right)$$
24		fveq2	$$⊢i=j\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge j}$$
25	24	raleqdv	$$⊢i=j\to \left(\forall k\in {\mathbb{Z}}_{\ge i}B\le x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}B\le x\right)$$
26	25	cbvrexvw	$$⊢\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}B\le x\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}B\le x$$
27	23 26	syl6bb	$$⊢y=x\to \left(\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}B\le y\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}B\le x\right)$$
28	27	cbvralvw	$$⊢\forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}B\le y\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}B\le x$$
29	28	a1i	$$⊢\phi \to \left(\forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}B\le y\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}B\le x\right)$$
30	9 21 29	3bitrd	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{-\infty }\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}B\le x\right)$$