Theorem xlimmnf

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

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

Proof

Step	Hyp	Ref	Expression
1		xlimmnf.k	$$⊢\underset{\_}{Ⅎ}kF$$
2		xlimmnf.m	$$⊢\phi \to M\in \mathbb{Z}$$
3		xlimmnf.z	$$⊢Z={\mathbb{Z}}_{\ge M}$$
4		xlimmnf.f	$$⊢\phi \to F:Z⟶{ℝ}^{*}$$
5	2 3 4	xlimmnfv	$$⊢\phi \to \left(F\underset{*}{⇝}\mathrm{-\infty }\leftrightarrow \forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\right)$$
6		breq2	$$⊢y=x\to \left(F\left(l\right)\le y\leftrightarrow F\left(l\right)\le x\right)$$
7	6	rexralbidv	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\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}F\left(l\right)\le x\leftrightarrow \forall l\in {\mathbb{Z}}_{\ge j}F\left(l\right)\le x\right)$$
10		nfcv	$$⊢\underset{\_}{Ⅎ}kl$$
11	1 10	nffv	$$⊢\underset{\_}{Ⅎ}kF\left(l\right)$$
12		nfcv	$$⊢\underset{\_}{Ⅎ}k\le$$
13		nfcv	$$⊢\underset{\_}{Ⅎ}kx$$
14	11 12 13	nfbr	$$⊢ℲkF\left(l\right)\le x$$
15		nfv	$$⊢ℲlF\left(k\right)\le x$$
16		fveq2	$$⊢l=k\to F\left(l\right)=F\left(k\right)$$
17	16	breq1d	$$⊢l=k\to \left(F\left(l\right)\le x\leftrightarrow F\left(k\right)\le x\right)$$
18	14 15 17	cbvralw	$$⊢\forall l\in {\mathbb{Z}}_{\ge j}F\left(l\right)\le x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x$$
19	9 18	bitrdi	$$⊢i=j\to \left(\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x\right)$$
20	19	cbvrexvw	$$⊢\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le x\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x$$
21	7 20	bitrdi	$$⊢y=x\to \left(\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x\right)$$
22	21	cbvralvw	$$⊢\forall y\in ℝ\exists i\in Z\forall l\in {\mathbb{Z}}_{\ge i}F\left(l\right)\le y\leftrightarrow \forall x\in ℝ\exists j\in Z\forall k\in {\mathbb{Z}}_{\ge j}F\left(k\right)\le x$$
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}F\left(k\right)\le x\right)$$