limsupvaluz2

Description: The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

	Ref	Expression
Hypotheses	limsupvaluz2.m	$⊢ φ \to M \in ℤ$
	limsupvaluz2.z	$⊢ Z = ℤ_{\geq M}$
	limsupvaluz2.f	$⊢ φ \to F : Z ⟶ ℝ$
	limsupvaluz2.r	$⊢ φ \to lim sup (F) \in ℝ$
Assertion	limsupvaluz2	$⊢ φ \to lim sup (F) = sup (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{*} <)) ℝ <)$

Proof

Step	Hyp	Ref	Expression
1		limsupvaluz2.m	$⊢ φ \to M \in ℤ$
2		limsupvaluz2.z	$⊢ Z = ℤ_{\geq M}$
3		limsupvaluz2.f	$⊢ φ \to F : Z ⟶ ℝ$
4		limsupvaluz2.r	$⊢ φ \to lim sup (F) \in ℝ$
5	3	frexr	$⊢ φ \to F : Z ⟶ ℝ^{*}$
6	1 2 5	limsupvaluz	$⊢ φ \to lim sup (F) = sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{} <)$
7	3	adantr	$⊢ (φ \land n \in Z) \to F : Z ⟶ ℝ$
8		id	$⊢ n \in Z \to n \in Z$
9	2 8	uzssd2	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
10	9	adantl	$⊢ (φ \land n \in Z) \to ℤ_{\geq n} \subseteq Z$
11	7 10	feqresmpt	$⊢ (φ \land n \in Z) \to {F ↾}_{ℤ_{\geq n}} = (m \in ℤ_{\geq n} ⟼ F (m))$
12	11	rneqd	$⊢ (φ \land n \in Z) \to ran ({F ↾}_{ℤ_{\geq n}}) = ran (m \in ℤ_{\geq n} ⟼ F (m))$
13	12	supeq1d	$⊢ (φ \land n \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m)) ℝ^{} <)$
14		nfcv	$⊢ \underline{Ⅎ} m F$
15	4	renepnfd	$⊢ φ \to lim sup (F) \neq +∞$
16	14 2 3 15	limsupubuz	$⊢ φ \to \exists x \in ℝ \forall m \in Z F (m) \leq x$
17	16	adantr	$⊢ (φ \land n \in Z) \to \exists x \in ℝ \forall m \in Z F (m) \leq x$
18		ssralv	$⊢ ℤ_{\geq n} \subseteq Z \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
19	9 18	syl	$⊢ n \in Z \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
20	19	adantl	$⊢ (φ \land n \in Z) \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
21	20	reximdv	$⊢ (φ \land n \in Z) \to (\exists x \in ℝ \forall m \in Z F (m) \leq x \to \exists x \in ℝ \forall m \in ℤ_{\geq n} F (m) \leq x)$
22	17 21	mpd	$⊢ (φ \land n \in Z) \to \exists x \in ℝ \forall m \in ℤ_{\geq n} F (m) \leq x$
23		nfv	$⊢ Ⅎ m (φ \land n \in Z)$
24	2	eluzelz2	$⊢ n \in Z \to n \in ℤ$
25		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
26		ne0i	$⊢ n \in ℤ_{\geq n} \to ℤ_{\geq n} \neq \emptyset$
27	24 25 26	3syl	$⊢ n \in Z \to ℤ_{\geq n} \neq \emptyset$
28	27	adantl	$⊢ (φ \land n \in Z) \to ℤ_{\geq n} \neq \emptyset$
29	7	adantr	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to F : Z ⟶ ℝ$
30	10	sselda	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
31	29 30	ffvelrnd	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to F (m) \in ℝ$
32	23 28 31	supxrre3rnmpt	$⊢ (φ \land n \in Z) \to (sup (ran (m \in ℤ_{\geq n} ⟼ F (m)) ℝ^{*} <) \in ℝ \leftrightarrow \exists x \in ℝ \forall m \in ℤ_{\geq n} F (m) \leq x)$
33	22 32	mpbird	$⊢ (φ \land n \in Z) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m)) ℝ^{*} <) \in ℝ$
34	13 33	eqeltrd	$⊢ (φ \land n \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <) \in ℝ$
35	34	fmpttd	$⊢ φ \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) : Z ⟶ ℝ$
36	35	frnd	$⊢ φ \to ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) \subseteq ℝ$
37		nfv	$⊢ Ⅎ n φ$
38		eqid	$⊢ (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
39	1 2	uzn0d	$⊢ φ \to Z \neq \emptyset$
40	37 34 38 39	rnmptn0	$⊢ φ \to ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) \neq \emptyset$
41		nfcv	$⊢ \underline{Ⅎ} j F$
42	41 1 2 5	limsupre3uz	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (\exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j) \land \exists x \in ℝ \exists i \in Z \forall j \in ℤ_{\geq i} F (j) \leq x))$
43	4 42	mpbid	$⊢ φ \to (\exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j) \land \exists x \in ℝ \exists i \in Z \forall j \in ℤ_{\geq i} F (j) \leq x)$
44	43	simpld	$⊢ φ \to \exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j)$
45		simp-4r	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ$
46	45	rexrd	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ^{*}$
47	5	3ad2ant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F : Z ⟶ ℝ^{*}$
48	2	uztrn2	$⊢ (i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
49	48	3adant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
50	47 49	ffvelrnd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ℝ^{*}$
51	50	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to F (j) \in ℝ^{*}$
52		rnresss	$⊢ ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
53	52	a1i	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
54	3	frnd	$⊢ φ \to ran F \subseteq ℝ$
55	54	adantr	$⊢ (φ \land i \in Z) \to ran F \subseteq ℝ$
56	53 55	sstrd	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ$
57		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
58	57	a1i	$⊢ (φ \land i \in Z) \to ℝ \subseteq ℝ^{*}$
59	56 58	sstrd	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
60	59	supxrcld	$⊢ (φ \land i \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \in ℝ^{}$
61	60	ad5ant13	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \in ℝ^{}$
62		simpr	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \leq F (j)$
63	59	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
64		fvres	$⊢ j \in ℤ_{\geq i} \to ({F ↾}_{ℤ_{\geq i}}) (j) = F (j)$
65	64	eqcomd	$⊢ j \in ℤ_{\geq i} \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
66	65	3ad2ant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
67	3	ffnd	$⊢ φ \to F Fn Z$
68	67	adantr	$⊢ (φ \land i \in Z) \to F Fn Z$
69		id	$⊢ i \in Z \to i \in Z$
70	2 69	uzssd2	$⊢ i \in Z \to ℤ_{\geq i} \subseteq Z$
71	70	adantl	$⊢ (φ \land i \in Z) \to ℤ_{\geq i} \subseteq Z$
72		fnssres	$⊢ (F Fn Z \land ℤ_{\geq i} \subseteq Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
73	68 71 72	syl2anc	$⊢ (φ \land i \in Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
74	73	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
75		simp3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in ℤ_{\geq i}$
76		fnfvelrn	$⊢ (({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i} \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
77	74 75 76	syl2anc	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
78	66 77	eqeltrd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
79		eqid	$⊢ sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
80	63 78 79	supxrubd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
81	80	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to F (j) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
82	46 51 61 62 81	xrletrd	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
83	82	rexlimdva2	$⊢ ((φ \land x \in ℝ) \land i \in Z) \to (\exists j \in ℤ_{\geq i} x \leq F (j) \to x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <))$
84	83	ralimdva	$⊢ (φ \land x \in ℝ) \to (\forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j) \to \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <))$
85	84	reximdva	$⊢ φ \to (\exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j) \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <))$
86	44 85	mpd	$⊢ φ \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
87	86	idi	$⊢ φ \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
88		fveq2	$⊢ n = i \to ℤ_{\geq n} = ℤ_{\geq i}$
89	88	reseq2d	$⊢ n = i \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq i}}$
90	89	rneqd	$⊢ n = i \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq i}})$
91	90	supeq1d	$⊢ n = i \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
92		eqcom	$⊢ n = i \leftrightarrow i = n$
93	92	imbi1i	$⊢ (n = i \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)) \leftrightarrow (i = n \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <))$
94		eqcom	$⊢ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
95	94	imbi2i	$⊢ (i = n \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)) \leftrightarrow (i = n \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
96	93 95	bitri	$⊢ (n = i \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)) \leftrightarrow (i = n \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
97	91 96	mpbi	$⊢ i = n \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
98	97	breq2d	$⊢ i = n \to (x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
99	98	cbvralvw	$⊢ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow \forall n \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
100	99	rexbii	$⊢ \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow \exists x \in ℝ \forall n \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
101	87 100	sylib	$⊢ φ \to \exists x \in ℝ \forall n \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)$
102	34	elexd	$⊢ (φ \land n \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <) \in V$
103	37 102	rnmptbd2	$⊢ φ \to (\exists x \in ℝ \forall n \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) \leftrightarrow \exists x \in ℝ \forall y \in ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) x \leq y)$
104	101 103	mpbid	$⊢ φ \to \exists x \in ℝ \forall y \in ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) x \leq y$
105		infxrre	$⊢ (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) \subseteq ℝ \land ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) \neq \emptyset \land \exists x \in ℝ \forall y \in ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) x \leq y) \to sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{} <) = sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <)$
106	36 40 104 105	syl3anc	$⊢ φ \to sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{} <) = sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) ℝ <)$
107		fveq2	$⊢ n = k \to ℤ_{\geq n} = ℤ_{\geq k}$
108	107	reseq2d	$⊢ n = k \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq k}}$
109	108	rneqd	$⊢ n = k \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq k}})$
110	109	supeq1d	$⊢ n = k \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)$
111	110	cbvmptv	$⊢ (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
112	111	rneqi	$⊢ ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
113	112	infeq1i	$⊢ sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <) = sup (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)) ℝ <)$
114	113	a1i	$⊢ φ \to sup (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <) = sup (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)) ℝ <)$
115	6 106 114	3eqtrd	$⊢ φ \to lim sup (F) = sup (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{*} <)) ℝ <)$

Metamath Proof Explorer

Theorem limsupvaluz2

Proof