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) = inf (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) = inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{} <)$
7	3	adantr	$⊢ (φ \land n \in Z) \to F : Z ⟶ ℝ$
8	2	uzssd3	$⊢ n \in Z \to ℤ_{\geq n} \subseteq Z$
9	8	adantl	$⊢ (φ \land n \in Z) \to ℤ_{\geq n} \subseteq Z$
10	7 9	feqresmpt	$⊢ (φ \land n \in Z) \to {F ↾}_{ℤ_{\geq n}} = (m \in ℤ_{\geq n} ⟼ F (m))$
11	10	rneqd	$⊢ (φ \land n \in Z) \to ran ({F ↾}_{ℤ_{\geq n}}) = ran (m \in ℤ_{\geq n} ⟼ F (m))$
12	11	supeq1d	$⊢ (φ \land n \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran (m \in ℤ_{\geq n} ⟼ F (m)) ℝ^{} <)$
13		nfcv	$⊢ \underline{Ⅎ} m F$
14	4	renepnfd	$⊢ φ \to lim sup (F) \neq +∞$
15	13 2 3 14	limsupubuz	$⊢ φ \to \exists x \in ℝ \forall m \in Z F (m) \leq x$
16	15	adantr	$⊢ (φ \land n \in Z) \to \exists x \in ℝ \forall m \in Z F (m) \leq x$
17		ssralv	$⊢ ℤ_{\geq n} \subseteq Z \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
18	8 17	syl	$⊢ n \in Z \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
19	18	adantl	$⊢ (φ \land n \in Z) \to (\forall m \in Z F (m) \leq x \to \forall m \in ℤ_{\geq n} F (m) \leq x)$
20	19	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)$
21	16 20	mpd	$⊢ (φ \land n \in Z) \to \exists x \in ℝ \forall m \in ℤ_{\geq n} F (m) \leq x$
22		nfv	$⊢ Ⅎ m (φ \land n \in Z)$
23	2	eluzelz2	$⊢ n \in Z \to n \in ℤ$
24		uzid	$⊢ n \in ℤ \to n \in ℤ_{\geq n}$
25		ne0i	$⊢ n \in ℤ_{\geq n} \to ℤ_{\geq n} \neq \emptyset$
26	23 24 25	3syl	$⊢ n \in Z \to ℤ_{\geq n} \neq \emptyset$
27	26	adantl	$⊢ (φ \land n \in Z) \to ℤ_{\geq n} \neq \emptyset$
28	7	adantr	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to F : Z ⟶ ℝ$
29	9	sselda	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to m \in Z$
30	28 29	ffvelcdmd	$⊢ ((φ \land n \in Z) \land m \in ℤ_{\geq n}) \to F (m) \in ℝ$
31	22 27 30	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)$
32	21 31	mpbird	$⊢ (φ \land n \in Z) \to sup (ran (m \in ℤ_{\geq n} ⟼ F (m)) ℝ^{*} <) \in ℝ$
33	12 32	eqeltrd	$⊢ (φ \land n \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <) \in ℝ$
34	33	fmpttd	$⊢ φ \to (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) : Z ⟶ ℝ$
35	34	frnd	$⊢ φ \to ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) \subseteq ℝ$
36		nfv	$⊢ Ⅎ n φ$
37		eqid	$⊢ (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
38	1 2	uzn0d	$⊢ φ \to Z \neq \emptyset$
39	36 33 37 38	rnmptn0	$⊢ φ \to ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) \neq \emptyset$
40		nfcv	$⊢ \underline{Ⅎ} j F$
41	40 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))$
42	4 41	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)$
43	42	simpld	$⊢ φ \to \exists x \in ℝ \forall i \in Z \exists j \in ℤ_{\geq i} x \leq F (j)$
44		simp-4r	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ$
45	44	rexrd	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \in ℝ^{*}$
46	5	3ad2ant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F : Z ⟶ ℝ^{*}$
47	2	uztrn2	$⊢ (i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
48	47	3adant1	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to j \in Z$
49	46 48	ffvelcdmd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ℝ^{*}$
50	49	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to F (j) \in ℝ^{*}$
51		rnresss	$⊢ ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ran F$
52	3	frnd	$⊢ φ \to ran F \subseteq ℝ$
53	52	adantr	$⊢ (φ \land i \in Z) \to ran F \subseteq ℝ$
54	51 53	sstrid	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ$
55	54	ssrexr	$⊢ (φ \land i \in Z) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
56	55	supxrcld	$⊢ (φ \land i \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \in ℝ^{}$
57	56	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 ℝ^{}$
58		simpr	$⊢ ((((φ \land x \in ℝ) \land i \in Z) \land j \in ℤ_{\geq i}) \land x \leq F (j)) \to x \leq F (j)$
59	55	3adant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ran ({F ↾}_{ℤ_{\geq i}}) \subseteq ℝ^{*}$
60		fvres	$⊢ j \in ℤ_{\geq i} \to ({F ↾}_{ℤ_{\geq i}}) (j) = F (j)$
61	60	eqcomd	$⊢ j \in ℤ_{\geq i} \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
62	61	3ad2ant3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) = ({F ↾}_{ℤ_{\geq i}}) (j)$
63	3	ffnd	$⊢ φ \to F Fn Z$
64	2	uzssd3	$⊢ i \in Z \to ℤ_{\geq i} \subseteq Z$
65		fnssres	$⊢ (F Fn Z \land ℤ_{\geq i} \subseteq Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
66	63 64 65	syl2an	$⊢ (φ \land i \in Z) \to ({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i}$
67		fnfvelrn	$⊢ (({F ↾}_{ℤ_{\geq i}}) Fn ℤ_{\geq i} \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
68	66 67	stoic3	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to ({F ↾}_{ℤ_{\geq i}}) (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
69	62 68	eqeltrd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \in ran ({F ↾}_{ℤ_{\geq i}})$
70		eqid	$⊢ sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
71	59 69 70	supxrubd	$⊢ (φ \land i \in Z \land j \in ℤ_{\geq i}) \to F (j) \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
72	71	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}}) ℝ^{*} <)$
73	45 50 57 58 72	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}}) ℝ^{*} <)$
74	73	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}}) ℝ^{*} <))$
75	74	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}}) ℝ^{*} <))$
76	75	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}}) ℝ^{*} <))$
77	43 76	mpd	$⊢ φ \to \exists x \in ℝ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{*} <)$
78		fveq2	$⊢ n = i \to ℤ_{\geq n} = ℤ_{\geq i}$
79	78	reseq2d	$⊢ n = i \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq i}}$
80	79	rneqd	$⊢ n = i \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq i}})$
81	80	supeq1d	$⊢ n = i \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <)$
82		eqcom	$⊢ n = i \leftrightarrow i = n$
83		eqcom	$⊢ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
84	81 82 83	3imtr3i	$⊢ i = n \to sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
85	84	breq2d	$⊢ i = n \to (x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <))$
86	85	cbvralvw	$⊢ \forall i \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq i}}) ℝ^{} <) \leftrightarrow \forall n \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)$
87	86	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}}) ℝ^{} <)$
88	77 87	sylib	$⊢ φ \to \exists x \in ℝ \forall n \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)$
89	36 33	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)$
90	88 89	mpbid	$⊢ φ \to \exists x \in ℝ \forall y \in ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) x \leq y$
91		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 inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{} <) = inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <)$
92	35 39 90 91	syl3anc	$⊢ φ \to inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ^{} <) = inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{*} <)) ℝ <)$
93		fveq2	$⊢ n = k \to ℤ_{\geq n} = ℤ_{\geq k}$
94	93	reseq2d	$⊢ n = k \to {F ↾}_{ℤ_{\geq n}} = {F ↾}_{ℤ_{\geq k}}$
95	94	rneqd	$⊢ n = k \to ran ({F ↾}_{ℤ_{\geq n}}) = ran ({F ↾}_{ℤ_{\geq k}})$
96	95	supeq1d	$⊢ n = k \to sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)$
97	96	cbvmptv	$⊢ (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
98	97	rneqi	$⊢ ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) = ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <))$
99	98	infeq1i	$⊢ inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <) = inf (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)) ℝ <)$
100	99	a1i	$⊢ φ \to inf (ran (n \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq n}}) ℝ^{} <)) ℝ <) = inf (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{} <)) ℝ <)$
101	6 92 100	3eqtrd	$⊢ φ \to lim sup (F) = inf (ran (k \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq k}}) ℝ^{*} <)) ℝ <)$

Metamath Proof Explorer

Theorem limsupvaluz2

Proof