Theorem xlimpnfmpt

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	xlimpnfmpt.k	$$⊢Ⅎk\phi$$
	xlimpnfmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
	xlimpnfmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
	xlimpnfmpt.b	$$⊢\left(\phi \wedge k\in Z\right)\to B\in {ℝ}^{*}$$
	xlimpnfmpt.f	$$⊢F=\left(k\in Z⟼B\right)$$
Assertion	xlimpnfmpt	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{+\infty }\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le B\right)$$

Proof

Step	Hyp	Ref	Expression
1		xlimpnfmpt.k	$$⊢Ⅎk\phi$$
2		xlimpnfmpt.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		xlimpnfmpt.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		xlimpnfmpt.b	$$⊢\left(\phi \wedge k\in Z\right)\to B\in {ℝ}^{*}$$
5		xlimpnfmpt.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	xlimpnf	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{+\infty }\leftrightarrow \forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le F\left(k\right)\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	breq2d	$$⊢\left(\left(\phi \wedge i\in Z\right)\wedge k\in {\mathbb{Z}}_{\ge i}\right)\to \left(y\le F\left(k\right)\leftrightarrow y\le B\right)$$
19	11 18	ralbida	$$⊢\left(\phi \wedge i\in Z\right)\to \left(\forall k\in {\mathbb{Z}}_{\ge i}y\le F\left(k\right)\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge i}y\le B\right)$$
20	19	rexbidva	$$⊢\phi \to \left(\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le F\left(k\right)\leftrightarrow \exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le B\right)$$
21	20	ralbidv	$$⊢\phi \to \left(\forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le F\left(k\right)\leftrightarrow \forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le B\right)$$
22		breq1	$$⊢y=x\to \left(y\le B\leftrightarrow x\le B\right)$$
23	22	rexralbidv	$$⊢y=x\to \left(\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}x\le B\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}x\le B\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}x\le B\right)$$
26	25	cbvrexvw	$$⊢\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}x\le B\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le B$$
27	23 26	bitrdi	$$⊢y=x\to \left(\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le B\right)$$
28	27	cbvralvw	$$⊢\forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le B$$
29	28	a1i	$$⊢\phi \to \left(\forall y\in ℝ\exists i\in Z\forall k\in {\mathbb{Z}}_{\ge i}y\le B\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le B\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}x\le B\right)$$