limsupmnfuzlem

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupmnfuzlem.1	$⊢ φ \to M \in ℤ$
	limsupmnfuzlem.2	$⊢ Z = ℤ_{\geq M}$
	limsupmnfuzlem.3	$⊢ φ \to F : Z ⟶ ℝ^{*}$
Assertion	limsupmnfuzlem	$⊢ φ \to (lim sup (F) = −∞ \leftrightarrow \forall x \in ℝ \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x)$

Proof

Step	Hyp	Ref	Expression
1		limsupmnfuzlem.1	$⊢ φ \to M \in ℤ$
2		limsupmnfuzlem.2	$⊢ Z = ℤ_{\geq M}$
3		limsupmnfuzlem.3	$⊢ φ \to F : Z ⟶ ℝ^{*}$
4		nfcv	$⊢ \underline{Ⅎ} j F$
5		uzssre	$⊢ ℤ_{\geq M} \subseteq ℝ$
6	2 5	eqsstri	$⊢ Z \subseteq ℝ$
7	6	a1i	$⊢ φ \to Z \subseteq ℝ$
8	4 7 3	limsupmnf	$⊢ φ \to (lim sup (F) = −∞ \leftrightarrow \forall x \in ℝ \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x))$
9		breq1	$⊢ k = i \to (k \leq j \leftrightarrow i \leq j)$
10	9	imbi1d	$⊢ k = i \to ((k \leq j \to F (j) \leq x) \leftrightarrow (i \leq j \to F (j) \leq x))$
11	10	ralbidv	$⊢ k = i \to (\forall j \in Z (k \leq j \to F (j) \leq x) \leftrightarrow \forall j \in Z (i \leq j \to F (j) \leq x))$
12	11	cbvrexvw	$⊢ \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x) \leftrightarrow \exists i \in ℝ \forall j \in Z (i \leq j \to F (j) \leq x)$
13	12	biimpi	$⊢ \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x) \to \exists i \in ℝ \forall j \in Z (i \leq j \to F (j) \leq x)$
14		iftrue	$⊢ M \leq ⌈i⌉ \to if (M \leq ⌈i⌉, ⌈i⌉, M) = ⌈i⌉$
15	14	adantl	$⊢ ((φ \land i \in ℝ) \land M \leq ⌈i⌉) \to if (M \leq ⌈i⌉, ⌈i⌉, M) = ⌈i⌉$
16	1	ad2antrr	$⊢ ((φ \land i \in ℝ) \land M \leq ⌈i⌉) \to M \in ℤ$
17		ceilcl	$⊢ i \in ℝ \to ⌈i⌉ \in ℤ$
18	17	ad2antlr	$⊢ ((φ \land i \in ℝ) \land M \leq ⌈i⌉) \to ⌈i⌉ \in ℤ$
19		simpr	$⊢ ((φ \land i \in ℝ) \land M \leq ⌈i⌉) \to M \leq ⌈i⌉$
20	2 16 18 19	eluzd	$⊢ ((φ \land i \in ℝ) \land M \leq ⌈i⌉) \to ⌈i⌉ \in Z$
21	15 20	eqeltrd	$⊢ ((φ \land i \in ℝ) \land M \leq ⌈i⌉) \to if (M \leq ⌈i⌉, ⌈i⌉, M) \in Z$
22		iffalse	$⊢ \neg M \leq ⌈i⌉ \to if (M \leq ⌈i⌉, ⌈i⌉, M) = M$
23	22	adantl	$⊢ ((φ \land i \in ℝ) \land \neg M \leq ⌈i⌉) \to if (M \leq ⌈i⌉, ⌈i⌉, M) = M$
24	1 2	uzidd2	$⊢ φ \to M \in Z$
25	24	ad2antrr	$⊢ ((φ \land i \in ℝ) \land \neg M \leq ⌈i⌉) \to M \in Z$
26	23 25	eqeltrd	$⊢ ((φ \land i \in ℝ) \land \neg M \leq ⌈i⌉) \to if (M \leq ⌈i⌉, ⌈i⌉, M) \in Z$
27	21 26	pm2.61dan	$⊢ (φ \land i \in ℝ) \to if (M \leq ⌈i⌉, ⌈i⌉, M) \in Z$
28	27	3adant3	$⊢ (φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \to if (M \leq ⌈i⌉, ⌈i⌉, M) \in Z$
29		nfv	$⊢ Ⅎ j φ$
30		nfv	$⊢ Ⅎ j i \in ℝ$
31		nfra1	$⊢ Ⅎ j \forall j \in Z (i \leq j \to F (j) \leq x)$
32	29 30 31	nf3an	$⊢ Ⅎ j (φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x))$
33		simplr	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to i \in ℝ$
34	6 27	sseldi	$⊢ (φ \land i \in ℝ) \to if (M \leq ⌈i⌉, ⌈i⌉, M) \in ℝ$
35	34	adantr	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to if (M \leq ⌈i⌉, ⌈i⌉, M) \in ℝ$
36		eluzelre	$⊢ j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)} \to j \in ℝ$
37	36	adantl	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to j \in ℝ$
38		simpr	$⊢ (φ \land i \in ℝ) \to i \in ℝ$
39	17	zred	$⊢ i \in ℝ \to ⌈i⌉ \in ℝ$
40	39	adantl	$⊢ (φ \land i \in ℝ) \to ⌈i⌉ \in ℝ$
41		ceilge	$⊢ i \in ℝ \to i \leq ⌈i⌉$
42	41	adantl	$⊢ (φ \land i \in ℝ) \to i \leq ⌈i⌉$
43	6 24	sseldi	$⊢ φ \to M \in ℝ$
44	43	adantr	$⊢ (φ \land i \in ℝ) \to M \in ℝ$
45		max2	$⊢ (M \in ℝ \land ⌈i⌉ \in ℝ) \to ⌈i⌉ \leq if (M \leq ⌈i⌉, ⌈i⌉, M)$
46	44 40 45	syl2anc	$⊢ (φ \land i \in ℝ) \to ⌈i⌉ \leq if (M \leq ⌈i⌉, ⌈i⌉, M)$
47	38 40 34 42 46	letrd	$⊢ (φ \land i \in ℝ) \to i \leq if (M \leq ⌈i⌉, ⌈i⌉, M)$
48	47	adantr	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to i \leq if (M \leq ⌈i⌉, ⌈i⌉, M)$
49		eluzle	$⊢ j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)} \to if (M \leq ⌈i⌉, ⌈i⌉, M) \leq j$
50	49	adantl	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to if (M \leq ⌈i⌉, ⌈i⌉, M) \leq j$
51	33 35 37 48 50	letrd	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to i \leq j$
52	51	3adantl3	$⊢ ((φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to i \leq j$
53		simpl3	$⊢ ((φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to \forall j \in Z (i \leq j \to F (j) \leq x)$
54	1	ad2antrr	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to M \in ℤ$
55		eluzelz	$⊢ j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)} \to j \in ℤ$
56	55	adantl	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to j \in ℤ$
57	44	adantr	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to M \in ℝ$
58		max1	$⊢ (M \in ℝ \land ⌈i⌉ \in ℝ) \to M \leq if (M \leq ⌈i⌉, ⌈i⌉, M)$
59	43 39 58	syl2an	$⊢ (φ \land i \in ℝ) \to M \leq if (M \leq ⌈i⌉, ⌈i⌉, M)$
60	59	adantr	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to M \leq if (M \leq ⌈i⌉, ⌈i⌉, M)$
61	57 35 37 60 50	letrd	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to M \leq j$
62	2 54 56 61	eluzd	$⊢ ((φ \land i \in ℝ) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to j \in Z$
63	62	3adantl3	$⊢ ((φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to j \in Z$
64		rspa	$⊢ (\forall j \in Z (i \leq j \to F (j) \leq x) \land j \in Z) \to (i \leq j \to F (j) \leq x)$
65	53 63 64	syl2anc	$⊢ ((φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to (i \leq j \to F (j) \leq x)$
66	52 65	mpd	$⊢ ((φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \land j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}) \to F (j) \leq x$
67	66	ex	$⊢ (φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \to (j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)} \to F (j) \leq x)$
68	32 67	ralrimi	$⊢ (φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \to \forall j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)} F (j) \leq x$
69		fveq2	$⊢ k = if (M \leq ⌈i⌉, ⌈i⌉, M) \to ℤ_{\geq k} = ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)}$
70	69	raleqdv	$⊢ k = if (M \leq ⌈i⌉, ⌈i⌉, M) \to (\forall j \in ℤ_{\geq k} F (j) \leq x \leftrightarrow \forall j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)} F (j) \leq x)$
71	70	rspcev	$⊢ (if (M \leq ⌈i⌉, ⌈i⌉, M) \in Z \land \forall j \in ℤ_{\geq if (M \leq ⌈i⌉, ⌈i⌉, M)} F (j) \leq x) \to \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x$
72	28 68 71	syl2anc	$⊢ (φ \land i \in ℝ \land \forall j \in Z (i \leq j \to F (j) \leq x)) \to \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x$
73	72	3exp	$⊢ φ \to (i \in ℝ \to (\forall j \in Z (i \leq j \to F (j) \leq x) \to \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x))$
74	73	rexlimdv	$⊢ φ \to (\exists i \in ℝ \forall j \in Z (i \leq j \to F (j) \leq x) \to \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x)$
75	74	imp	$⊢ (φ \land \exists i \in ℝ \forall j \in Z (i \leq j \to F (j) \leq x)) \to \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x$
76	13 75	sylan2	$⊢ (φ \land \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x)) \to \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x$
77	76	ex	$⊢ φ \to (\exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x) \to \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x)$
78		rexss	$⊢ Z \subseteq ℝ \to (\exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x \leftrightarrow \exists k \in ℝ (k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x))$
79	6 78	ax-mp	$⊢ \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x \leftrightarrow \exists k \in ℝ (k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x)$
80	79	biimpi	$⊢ \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x \to \exists k \in ℝ (k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x)$
81		nfv	$⊢ Ⅎ j k \in Z$
82		nfra1	$⊢ Ⅎ j \forall j \in ℤ_{\geq k} F (j) \leq x$
83	81 82	nfan	$⊢ Ⅎ j (k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x)$
84		simp1r	$⊢ ((k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x) \land j \in Z \land k \leq j) \to \forall j \in ℤ_{\geq k} F (j) \leq x$
85		eqid	$⊢ ℤ_{\geq k} = ℤ_{\geq k}$
86	2	eluzelz2	$⊢ k \in Z \to k \in ℤ$
87	86	3ad2ant1	$⊢ (k \in Z \land j \in Z \land k \leq j) \to k \in ℤ$
88	2	eluzelz2	$⊢ j \in Z \to j \in ℤ$
89	88	3ad2ant2	$⊢ (k \in Z \land j \in Z \land k \leq j) \to j \in ℤ$
90		simp3	$⊢ (k \in Z \land j \in Z \land k \leq j) \to k \leq j$
91	85 87 89 90	eluzd	$⊢ (k \in Z \land j \in Z \land k \leq j) \to j \in ℤ_{\geq k}$
92	91	3adant1r	$⊢ ((k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x) \land j \in Z \land k \leq j) \to j \in ℤ_{\geq k}$
93		rspa	$⊢ (\forall j \in ℤ_{\geq k} F (j) \leq x \land j \in ℤ_{\geq k}) \to F (j) \leq x$
94	84 92 93	syl2anc	$⊢ ((k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x) \land j \in Z \land k \leq j) \to F (j) \leq x$
95	94	3exp	$⊢ (k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x) \to (j \in Z \to (k \leq j \to F (j) \leq x))$
96	83 95	ralrimi	$⊢ (k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x) \to \forall j \in Z (k \leq j \to F (j) \leq x)$
97	96	a1i	$⊢ φ \to ((k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x) \to \forall j \in Z (k \leq j \to F (j) \leq x))$
98	97	reximdv	$⊢ φ \to (\exists k \in ℝ (k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x) \to \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x))$
99	98	imp	$⊢ (φ \land \exists k \in ℝ (k \in Z \land \forall j \in ℤ_{\geq k} F (j) \leq x)) \to \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x)$
100	80 99	sylan2	$⊢ (φ \land \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x) \to \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x)$
101	100	ex	$⊢ φ \to (\exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x \to \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x))$
102	77 101	impbid	$⊢ φ \to (\exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x) \leftrightarrow \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x)$
103	102	ralbidv	$⊢ φ \to (\forall x \in ℝ \exists k \in ℝ \forall j \in Z (k \leq j \to F (j) \leq x) \leftrightarrow \forall x \in ℝ \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x)$
104	8 103	bitrd	$⊢ φ \to (lim sup (F) = −∞ \leftrightarrow \forall x \in ℝ \exists k \in Z \forall j \in ℤ_{\geq k} F (j) \leq x)$

Metamath Proof Explorer

Theorem limsupmnfuzlem

Proof