Theorem xlimpnf

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

Proof

Step	Hyp	Ref	Expression
1		xlimpnf.k	$$⊢\underset{\_}{Ⅎ}kF$$
2		xlimpnf.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		xlimpnf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		xlimpnf.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
5	2 3 4	xlimpnfv	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{+\infty }\leftrightarrow \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\right)$$
6		breq1	$$⊢y=x\to \left(y\le F\left(l\right)\leftrightarrow x\le F\left(l\right)\right)$$
7	6	rexralbidv	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\right)$$
8		fveq2	$$⊢i=j\to {\mathbb{Z}}_{\ge i}={\mathbb{Z}}_{\ge j}$$
9	8	raleqdv	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge j}x\le F\left(l\right)\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}kx$$
11		nfcv	$$⊢\underset{\_}{Ⅎ}k\le$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}kl$$
13	1 12	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(l\right)$$
14	10 11 13	nfbr	$$⊢Ⅎkx\le F\left(l\right)$$
15		nfv	$$⊢Ⅎlx\le F\left(k\right)$$
16		fveq2	$$⊢l=k\to F\left(l\right)=F\left(k\right)$$
17	16	breq2d	$$⊢l=k\to \left(x\le F\left(l\right)\leftrightarrow x\le F\left(k\right)\right)$$
18	14 15 17	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge j}x\le F\left(l\right)\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)$$
19	9 18	bitrdi	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)$$
20	19	cbvrexvw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}x\le F\left(l\right)\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)$$
21	7 20	bitrdi	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)$$
22	21	cbvralvw	$$⊢\forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}y\le F\left(l\right)\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)$$
23	5 22	bitrdi	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{+\infty }\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}x\le F\left(k\right)\right)$$