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	34	elexd	$⊢ (φ \land n \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <) \in V$
39		eqid	$⊢ (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
40	1 2	uzn0d	$⊢ φ \to Z \neq \emptyset$
41	37 38 39 40	rnmptn0	$⊢ φ \to ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) \neq \emptyset$
42		nfcv	$⊢ \underline{Ⅎ} j F$
43	42 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))$
44	4 43	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)$
45	44	simpld	$⊢ φ \to \exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j)$
46		simp-4r	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ$
47	46	rexrd	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ^{*}$
48	5	3ad2ant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F : Z ⟶ ℝ^{*}$
49	2	uztrn2	$⊢ (i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
50	49	3adant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
51	48 50	ffvelrnd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ℝ^{*}$
52	51	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to F (j) \in ℝ^{*}$
53		rnresss	$⊢ ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
54	53	a1i	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
55	3	frnd	$⊢ φ \to ran F \subseteq ℝ$
56	55	adantr	$⊢ (φ \land i \in Z) \to ran F \subseteq ℝ$
57	54 56	sstrd	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ$
58		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
59	58	a1i	$⊢ (φ \land i \in Z) \to ℝ \subseteq ℝ^{*}$
60	57 59	sstrd	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
61	60	supxrcld	$⊢ (φ \land i \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \in ℝ^{}$
62	61	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 ℝ^{}$
63		simpr	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \leq F (j)$
64	60	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
65		fvres	$⊢ j \in ℤ_{\geq i} \to ({F ↾}_{ℤ_{\geq i}}) (j) = F (j)$
66	65	eqcomd	$⊢ j \in ℤ_{\geq i} \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
67	66	3ad2ant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
68	3	ffnd	$⊢ φ \to F Fn Z$
69	68	adantr	$⊢ (φ \land i \in Z) \to F Fn Z$
70		id	$⊢ i \in Z \to i \in Z$
71	2 70	uzssd2	$⊢ i \in Z \to ℤ_{\geq i} \subseteq Z$
72	71	adantl	$⊢ (φ \land i \in Z) \to ℤ_{\geq i} \subseteq Z$
73		fnssres	$⊢ (F Fn Z \land ℤ_{\geq i} \subseteq Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
74	69 72 73	syl2anc	$⊢ (φ \land i \in Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
75	74	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
76		simp3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in ℤ_{\geq i}$
77		fnfvelrn	$⊢ (({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i} \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
78	75 76 77	syl2anc	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
79	67 78	eqeltrd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
80		eqid	$⊢ sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
81	64 79 80	supxrubd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
82	81	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}}) ℝ^{*} <)$
83	47 52 62 63 82	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}}) ℝ^{*} <)$
84	83	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}}) ℝ^{*} <))$
85	84	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}}) ℝ^{*} <))$
86	85	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}}) ℝ^{*} <))$
87	45 86	mpd	$⊢ φ \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
88	87	idi	$⊢ φ \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
89		fveq2	$⊢ n = i \to ℤ_{\geq n} = ℤ_{\geq i}$
90	89	reseq2d	$⊢ n = i \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq i}}$
91	90	rneqd	$⊢ n = i \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq i}})$
92	91	supeq1d	$⊢ n = i \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
93		eqcom	$⊢ n = i \leftrightarrow i = n$
94	93	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}}) ℝ^{} <))$
95		eqcom	$⊢ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
96	95	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}}) ℝ^{} <))$
97	94 96	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}}) ℝ^{} <))$
98	92 97	mpbi	$⊢ i = n \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
99	98	breq2d	$⊢ i = n \to (x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
100	99	cbvralvw	$⊢ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow \forall n \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
101	100	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}}) ℝ^{} <)$
102	88 101	sylib	$⊢ φ \to \exists x \in ℝ \forall n \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)$
103	37 38	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	102 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 41 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