xlimmnfv

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	xlimmnfv.m	$⊢ φ \to M \in ℤ$
	xlimmnfv.z	$⊢ Z = ℤ_{\geq M}$
	xlimmnfv.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
Assertion	xlimmnfv	$⊢ φ \to (F \underset{*}{⇝} −∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)$

Proof

Step	Hyp	Ref	Expression
1		xlimmnfv.m	$⊢ φ \to M \in ℤ$
2		xlimmnfv.z	$⊢ Z = ℤ_{\geq M}$
3		xlimmnfv.f	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4	1	ad2antrr	$⊢ ((φ \land F \underset{*}{⇝} −∞) \land x \in ℝ) \to M \in ℤ$
5	3	ad2antrr	$⊢ ((φ \land F \underset{}{⇝} −∞) \land x \in ℝ) \to F : Z ⟶ ℝ^{}$
6		simplr	$⊢ ((φ \land F \underset{}{⇝} −∞) \land x \in ℝ) \to F \underset{}{⇝} −∞$
7		simpr	$⊢ ((φ \land F \underset{*}{⇝} −∞) \land x \in ℝ) \to x \in ℝ$
8	4 2 5 6 7	xlimmnfvlem1	$⊢ ((φ \land F \underset{*}{⇝} −∞) \land x \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x$
9	8	ralrimiva	$⊢ (φ \land F \underset{*}{⇝} −∞) \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x$
10		nfv	$⊢ Ⅎ k φ$
11		nfcv	$⊢ \underline{Ⅎ} k ℝ$
12		nfcv	$⊢ \underline{Ⅎ} k Z$
13		nfra1	$⊢ Ⅎ k \forall k \in ℤ_{\geq j} F (k) \leq x$
14	12 13	nfrexw	$⊢ Ⅎ k \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x$
15	11 14	nfralw	$⊢ Ⅎ k \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x$
16	10 15	nfan	$⊢ Ⅎ k (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)$
17		nfv	$⊢ Ⅎ j φ$
18		nfcv	$⊢ \underline{Ⅎ} j ℝ$
19		nfre1	$⊢ Ⅎ j \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x$
20	18 19	nfralw	$⊢ Ⅎ j \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x$
21	17 20	nfan	$⊢ Ⅎ j (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)$
22	1	adantr	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \to M \in ℤ$
23	3	adantr	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \to F : Z ⟶ ℝ^{*}$
24		nfv	$⊢ Ⅎ j y \in ℝ$
25	21 24	nfan	$⊢ Ⅎ j ((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \land y \in ℝ)$
26	3	3ad2ant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F : Z ⟶ ℝ^{*}$
27	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
28	27	3adant1	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
29	26 28	ffvelcdmd	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F (k) \in ℝ^{*}$
30	29	ad5ant134	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) \leq y - 1) \to F (k) \in ℝ^{*}$
31		simp-4r	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) \leq y - 1) \to y \in ℝ$
32		peano2rem	$⊢ y \in ℝ \to y - 1 \in ℝ$
33	32	rexrd	$⊢ y \in ℝ \to y - 1 \in ℝ^{*}$
34	31 33	syl	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) \leq y - 1) \to y - 1 \in ℝ^{*}$
35		rexr	$⊢ y \in ℝ \to y \in ℝ^{*}$
36	35	ad4antlr	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) \leq y - 1) \to y \in ℝ^{*}$
37		simpr	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) \leq y - 1) \to F (k) \leq y - 1$
38	31	ltm1d	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) \leq y - 1) \to y - 1 < y$
39	30 34 36 37 38	xrlelttrd	$⊢ ((((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land F (k) \leq y - 1) \to F (k) < y$
40	39	ex	$⊢ (((φ \land y \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \to (F (k) \leq y - 1 \to F (k) < y)$
41	40	ralimdva	$⊢ ((φ \land y \in ℝ) \land j \in Z) \to (\forall k \in ℤ_{\geq j} F (k) \leq y - 1 \to \forall k \in ℤ_{\geq j} F (k) < y)$
42	41	imp	$⊢ (((φ \land y \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} F (k) \leq y - 1) \to \forall k \in ℤ_{\geq j} F (k) < y$
43	42	adantl3r	$⊢ ((((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \land y \in ℝ) \land j \in Z) \land \forall k \in ℤ_{\geq j} F (k) \leq y - 1) \to \forall k \in ℤ_{\geq j} F (k) < y$
44	43	3impa	$⊢ (((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \land y \in ℝ) \land j \in Z \land \forall k \in ℤ_{\geq j} F (k) \leq y - 1) \to \forall k \in ℤ_{\geq j} F (k) < y$
45	32	adantl	$⊢ (\forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x \land y \in ℝ) \to y - 1 \in ℝ$
46		simpl	$⊢ (\forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x \land y \in ℝ) \to \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x$
47		breq2	$⊢ x = y - 1 \to (F (k) \leq x \leftrightarrow F (k) \leq y - 1)$
48	47	ralbidv	$⊢ x = y - 1 \to (\forall k \in ℤ_{\geq j} F (k) \leq x \leftrightarrow \forall k \in ℤ_{\geq j} F (k) \leq y - 1)$
49	48	rexbidv	$⊢ x = y - 1 \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x \leftrightarrow \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq y - 1)$
50	49	rspcva	$⊢ (y - 1 \in ℝ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq y - 1$
51	45 46 50	syl2anc	$⊢ (\forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x \land y \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq y - 1$
52	51	adantll	$⊢ ((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \land y \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq y - 1$
53	25 44 52	reximdd	$⊢ ((φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \land y \in ℝ) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) < y$
54	53	ralrimiva	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \to \forall y \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) < y$
55	16 21 22 2 23 54	xlimmnfvlem2	$⊢ (φ \land \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x) \to F \underset{*}{⇝} −∞$
56	9 55	impbida	$⊢ φ \to (F \underset{*}{⇝} −∞ \leftrightarrow \forall x \in ℝ \exists j \in Z \forall k \in ℤ_{\geq j} F (k) \leq x)$

Metamath Proof Explorer

Theorem xlimmnfv

Proof