lmxrge0

Description: Express "sequence F converges to plus infinity" (i.e. diverges), for a sequence of nonnegative extended real numbers. (Contributed by Thierry Arnoux, 2-Aug-2017)

	Ref	Expression
Hypotheses	lmxrge0.j	$⊢ J = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
	lmxrge0.6	$⊢ φ \to F : ℕ ⟶ [0, +∞]$
	lmxrge0.7	$⊢ (φ \land k \in ℕ) \to F (k) = A$
Assertion	lmxrge0	$⊢ φ \to (F \underset{t}{⇝} (J) +∞ \leftrightarrow \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)$

Proof

Step	Hyp	Ref	Expression
1		lmxrge0.j	$⊢ J = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
2		lmxrge0.6	$⊢ φ \to F : ℕ ⟶ [0, +∞]$
3		lmxrge0.7	$⊢ (φ \land k \in ℕ) \to F (k) = A$
4		eqid	$⊢ ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞] = ℝ_{𝑠}^{} ↾_{𝑠} [0, +∞]$
5		xrstopn	$⊢ ordTop (\leq) = TopOpen (ℝ_{𝑠}^{*})$
6	4 5	resstopn	$⊢ ordTop (\leq) ↾_{𝑡} [0, +∞] = TopOpen (ℝ_{𝑠}^{*} ↾_{𝑠} [0, +∞])$
7	1 6	eqtr4i	$⊢ J = ordTop (\leq) ↾_{𝑡} [0, +∞]$
8		letopon	$⊢ ordTop (\leq) \in TopOn (ℝ^{*})$
9		iccssxr	$⊢ [0, +∞] \subseteq ℝ^{*}$
10		resttopon	$⊢ (ordTop (\leq) \in TopOn (ℝ^{}) \land [0, +∞] \subseteq ℝ^{}) \to ordTop (\leq) ↾_{𝑡} [0, +∞] \in TopOn ([0, +∞])$
11	8 9 10	mp2an	$⊢ ordTop (\leq) ↾_{𝑡} [0, +∞] \in TopOn ([0, +∞])$
12	7 11	eqeltri	$⊢ J \in TopOn ([0, +∞])$
13	12	a1i	$⊢ φ \to J \in TopOn ([0, +∞])$
14		nnuz	$⊢ ℕ = ℤ_{\geq 1}$
15		1zzd	$⊢ φ \to 1 \in ℤ$
16	13 14 15 2 3	lmbrf	$⊢ φ \to (F \underset{t}{⇝} (J) +∞ \leftrightarrow (+∞ \in [0, +∞] \land \forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)))$
17		0xr	$⊢ 0 \in ℝ^{*}$
18		pnfxr	$⊢ +∞ \in ℝ^{*}$
19		0lepnf	$⊢ 0 \leq +∞$
20		ubicc2	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land 0 \leq +∞) \to +∞ \in [0, +∞]$
21	17 18 19 20	mp3an	$⊢ +∞ \in [0, +∞]$
22	21	biantrur	$⊢ \forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a) \leftrightarrow (+∞ \in [0, +∞] \land \forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a))$
23	16 22	bitr4di	$⊢ φ \to (F \underset{t}{⇝} (J) +∞ \leftrightarrow \forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a))$
24		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
25	18	a1i	$⊢ x \in ℝ \to +∞ \in ℝ^{*}$
26		ltpnf	$⊢ x \in ℝ \to x < +∞$
27		ubioc1	$⊢ (x \in ℝ^{} \land +∞ \in ℝ^{} \land x < +∞) \to +∞ \in (x, +∞]$
28	24 25 26 27	syl3anc	$⊢ x \in ℝ \to +∞ \in (x, +∞]$
29		0ltpnf	$⊢ 0 < +∞$
30		ubioc1	$⊢ (0 \in ℝ^{} \land +∞ \in ℝ^{} \land 0 < +∞) \to +∞ \in (0, +∞]$
31	17 18 29 30	mp3an	$⊢ +∞ \in (0, +∞]$
32	28 31	jctir	$⊢ x \in ℝ \to (+∞ \in (x, +∞] \land +∞ \in (0, +∞])$
33		elin	$⊢ +∞ \in ((x, +∞] \cap (0, +∞]) \leftrightarrow (+∞ \in (x, +∞] \land +∞ \in (0, +∞])$
34	32 33	sylibr	$⊢ x \in ℝ \to +∞ \in ((x, +∞] \cap (0, +∞])$
35	34	ad2antlr	$⊢ ((φ \land x \in ℝ) \land \forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)) \to +∞ \in ((x, +∞] \cap (0, +∞])$
36		letop	$⊢ ordTop (\leq) \in Top$
37		ovex	$⊢ [0, +∞] \in V$
38		iocpnfordt	$⊢ (x, +∞] \in ordTop (\leq)$
39		iocpnfordt	$⊢ (0, +∞] \in ordTop (\leq)$
40		inopn	$⊢ (ordTop (\leq) \in Top \land (x, +∞] \in ordTop (\leq) \land (0, +∞] \in ordTop (\leq)) \to (x, +∞] \cap (0, +∞] \in ordTop (\leq)$
41	36 38 39 40	mp3an	$⊢ (x, +∞] \cap (0, +∞] \in ordTop (\leq)$
42		elrestr	$⊢ (ordTop (\leq) \in Top \land [0, +∞] \in V \land (x, +∞] \cap (0, +∞] \in ordTop (\leq)) \to ((x, +∞] \cap (0, +∞]) \cap [0, +∞] \in (ordTop (\leq) ↾_{𝑡} [0, +∞])$
43	36 37 41 42	mp3an	$⊢ ((x, +∞] \cap (0, +∞]) \cap [0, +∞] \in (ordTop (\leq) ↾_{𝑡} [0, +∞])$
44		inss2	$⊢ (x, +∞] \cap (0, +∞] \subseteq (0, +∞]$
45		iocssicc	$⊢ (0, +∞] \subseteq [0, +∞]$
46	44 45	sstri	$⊢ (x, +∞] \cap (0, +∞] \subseteq [0, +∞]$
47		sseqin2	$⊢ (x, +∞] \cap (0, +∞] \subseteq [0, +∞] \leftrightarrow [0, +∞] \cap ((x, +∞] \cap (0, +∞]) = (x, +∞] \cap (0, +∞]$
48	46 47	mpbi	$⊢ [0, +∞] \cap ((x, +∞] \cap (0, +∞]) = (x, +∞] \cap (0, +∞]$
49		incom	$⊢ [0, +∞] \cap ((x, +∞] \cap (0, +∞]) = ((x, +∞] \cap (0, +∞]) \cap [0, +∞]$
50	48 49	eqtr3i	$⊢ (x, +∞] \cap (0, +∞] = ((x, +∞] \cap (0, +∞]) \cap [0, +∞]$
51	43 50 7	3eltr4i	$⊢ (x, +∞] \cap (0, +∞] \in J$
52	51	a1i	$⊢ (φ \land x \in ℝ) \to (x, +∞] \cap (0, +∞] \in J$
53		eleq2	$⊢ a = (x, +∞] \cap (0, +∞] \to (+∞ \in a \leftrightarrow +∞ \in ((x, +∞] \cap (0, +∞]))$
54	53	adantl	$⊢ ((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \to (+∞ \in a \leftrightarrow +∞ \in ((x, +∞] \cap (0, +∞]))$
55	54	biimprd	$⊢ ((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \to (+∞ \in ((x, +∞] \cap (0, +∞]) \to +∞ \in a)$
56		simp-5r	$⊢ (((((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \land k \in ℤ_{\geq l}) \land A \in a) \to x \in ℝ$
57	56	rexrd	$⊢ (((((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \land k \in ℤ_{\geq l}) \land A \in a) \to x \in ℝ^{*}$
58		simpr	$⊢ (((((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \land k \in ℤ_{\geq l}) \land A \in a) \to A \in a$
59		simp-4r	$⊢ (((((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \land k \in ℤ_{\geq l}) \land A \in a) \to a = (x, +∞] \cap (0, +∞]$
60	58 59	eleqtrd	$⊢ (((((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \land k \in ℤ_{\geq l}) \land A \in a) \to A \in ((x, +∞] \cap (0, +∞])$
61		elin	$⊢ A \in ((x, +∞] \cap (0, +∞]) \leftrightarrow (A \in (x, +∞] \land A \in (0, +∞])$
62	61	simplbi	$⊢ A \in ((x, +∞] \cap (0, +∞]) \to A \in (x, +∞]$
63	60 62	syl	$⊢ (((((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \land k \in ℤ_{\geq l}) \land A \in a) \to A \in (x, +∞]$
64		elioc1	$⊢ (x \in ℝ^{} \land +∞ \in ℝ^{}) \to (A \in (x, +∞] \leftrightarrow (A \in ℝ^{*} \land x < A \land A \leq +∞))$
65	18 64	mpan2	$⊢ x \in ℝ^{} \to (A \in (x, +∞] \leftrightarrow (A \in ℝ^{} \land x < A \land A \leq +∞))$
66	65	biimpa	$⊢ (x \in ℝ^{} \land A \in (x, +∞]) \to (A \in ℝ^{} \land x < A \land A \leq +∞)$
67	66	simp2d	$⊢ (x \in ℝ^{*} \land A \in (x, +∞]) \to x < A$
68	57 63 67	syl2anc	$⊢ (((((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \land k \in ℤ_{\geq l}) \land A \in a) \to x < A$
69	68	ex	$⊢ ((((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to (A \in a \to x < A)$
70	69	ralimdva	$⊢ (((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \land l \in ℕ) \to (\forall k \in ℤ_{\geq l} A \in a \to \forall k \in ℤ_{\geq l} x < A)$
71	70	reximdva	$⊢ ((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \to (\exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} x < A)$
72		fveq2	$⊢ j = l \to ℤ_{\geq j} = ℤ_{\geq l}$
73	72	raleqdv	$⊢ j = l \to (\forall k \in ℤ_{\geq j} x < A \leftrightarrow \forall k \in ℤ_{\geq l} x < A)$
74	73	cbvrexvw	$⊢ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A \leftrightarrow \exists l \in ℕ \forall k \in ℤ_{\geq l} x < A$
75	71 74	syl6ibr	$⊢ ((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \to (\exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a \to \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)$
76	55 75	imim12d	$⊢ ((φ \land x \in ℝ) \land a = (x, +∞] \cap (0, +∞]) \to ((+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a) \to (+∞ \in ((x, +∞] \cap (0, +∞]) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A))$
77	52 76	rspcimdv	$⊢ (φ \land x \in ℝ) \to (\forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a) \to (+∞ \in ((x, +∞] \cap (0, +∞]) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A))$
78	77	imp	$⊢ ((φ \land x \in ℝ) \land \forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)) \to (+∞ \in ((x, +∞] \cap (0, +∞]) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)$
79	35 78	mpd	$⊢ ((φ \land x \in ℝ) \land \forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A$
80	79	ex	$⊢ (φ \land x \in ℝ) \to (\forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a) \to \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)$
81	80	ralrimdva	$⊢ φ \to (\forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a) \to \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)$
82		simplll	$⊢ (((φ \land a \in J) \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \land +∞ \in a) \to φ$
83		simpllr	$⊢ (((φ \land a \in J) \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \land +∞ \in a) \to a \in J$
84		simpr	$⊢ (((φ \land a \in J) \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \land +∞ \in a) \to +∞ \in a$
85	1	pnfneige0	$⊢ (a \in J \land +∞ \in a) \to \exists x \in ℝ (x, +∞] \subseteq a$
86	83 84 85	syl2anc	$⊢ (((φ \land a \in J) \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \land +∞ \in a) \to \exists x \in ℝ (x, +∞] \subseteq a$
87		simplr	$⊢ (((φ \land a \in J) \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \land +∞ \in a) \to \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A$
88		r19.29r	$⊢ (\exists x \in ℝ (x, +∞] \subseteq a \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \to \exists x \in ℝ ((x, +∞] \subseteq a \land \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)$
89		simp-4l	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to φ$
90		uznnssnn	$⊢ l \in ℕ \to ℤ_{\geq l} \subseteq ℕ$
91	90	ad2antlr	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to ℤ_{\geq l} \subseteq ℕ$
92		simpr	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to k \in ℤ_{\geq l}$
93	91 92	sseldd	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to k \in ℕ$
94	89 93	jca	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to (φ \land k \in ℕ)$
95		simp-4r	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to x \in ℝ$
96		simpllr	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to (x, +∞] \subseteq a$
97		simplr	$⊢ ((((φ \land k \in ℕ) \land x \in ℝ) \land (x, +∞] \subseteq a) \land x < A) \to (x, +∞] \subseteq a$
98		simplr	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x < A) \to x \in ℝ$
99	98	rexrd	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x < A) \to x \in ℝ^{*}$
100	2	ffvelcdmda	$⊢ (φ \land k \in ℕ) \to F (k) \in [0, +∞]$
101	3 100	eqeltrrd	$⊢ (φ \land k \in ℕ) \to A \in [0, +∞]$
102	9 101	sselid	$⊢ (φ \land k \in ℕ) \to A \in ℝ^{*}$
103	102	ad2antrr	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x < A) \to A \in ℝ^{*}$
104		simpr	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x < A) \to x < A$
105		pnfge	$⊢ A \in ℝ^{*} \to A \leq +∞$
106	103 105	syl	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x < A) \to A \leq +∞$
107	65	biimpar	$⊢ (x \in ℝ^{} \land (A \in ℝ^{} \land x < A \land A \leq +∞)) \to A \in (x, +∞]$
108	99 103 104 106 107	syl13anc	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land x < A) \to A \in (x, +∞]$
109	108	adantlr	$⊢ ((((φ \land k \in ℕ) \land x \in ℝ) \land (x, +∞] \subseteq a) \land x < A) \to A \in (x, +∞]$
110	97 109	sseldd	$⊢ ((((φ \land k \in ℕ) \land x \in ℝ) \land (x, +∞] \subseteq a) \land x < A) \to A \in a$
111	110	ex	$⊢ (((φ \land k \in ℕ) \land x \in ℝ) \land (x, +∞] \subseteq a) \to (x < A \to A \in a)$
112	94 95 96 111	syl21anc	$⊢ ((((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \land k \in ℤ_{\geq l}) \to (x < A \to A \in a)$
113	112	ralimdva	$⊢ (((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \land l \in ℕ) \to (\forall k \in ℤ_{\geq l} x < A \to \forall k \in ℤ_{\geq l} A \in a)$
114	113	reximdva	$⊢ ((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \to (\exists l \in ℕ \forall k \in ℤ_{\geq l} x < A \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)$
115	74 114	biimtrid	$⊢ ((φ \land x \in ℝ) \land (x, +∞] \subseteq a) \to (\exists j \in ℕ \forall k \in ℤ_{\geq j} x < A \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)$
116	115	expimpd	$⊢ (φ \land x \in ℝ) \to (((x, +∞] \subseteq a \land \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)$
117	116	rexlimdva	$⊢ φ \to (\exists x \in ℝ ((x, +∞] \subseteq a \land \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)$
118	88 117	syl5	$⊢ φ \to ((\exists x \in ℝ (x, +∞] \subseteq a \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a)$
119	118	imp	$⊢ (φ \land (\exists x \in ℝ (x, +∞] \subseteq a \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)) \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a$
120	82 86 87 119	syl12anc	$⊢ (((φ \land a \in J) \land \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A) \land +∞ \in a) \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a$
121	120	exp31	$⊢ (φ \land a \in J) \to (\forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A \to (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a))$
122	121	ralrimdva	$⊢ φ \to (\forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A \to \forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a))$
123	81 122	impbid	$⊢ φ \to (\forall a \in J (+∞ \in a \to \exists l \in ℕ \forall k \in ℤ_{\geq l} A \in a) \leftrightarrow \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)$
124	23 123	bitrd	$⊢ φ \to (F \underset{t}{⇝} (J) +∞ \leftrightarrow \forall x \in ℝ \exists j \in ℕ \forall k \in ℤ_{\geq j} x < A)$

Metamath Proof Explorer

Theorem lmxrge0

Proof