limsupgtlem

Description: For any positive real, the superior limit of F is larger than any of its values at large enough arguments, up to that positive real. (Contributed by Glauco Siliprandi, 2-Jan-2022)

	Ref	Expression
Hypotheses	limsupgtlem.m	$⊢ φ \to M \in ℤ$
	limsupgtlem.z	$⊢ Z = ℤ_{\geq M}$
	limsupgtlem.f	$⊢ φ \to F : Z ⟶ ℝ$
	limsupgtlem.r	$⊢ φ \to lim sup (F) \in ℝ$
	limsupgtlem.x	$⊢ φ \to X \in ℝ^{+}$
Assertion	limsupgtlem	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - X < lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		limsupgtlem.m	$⊢ φ \to M \in ℤ$
2		limsupgtlem.z	$⊢ Z = ℤ_{\geq M}$
3		limsupgtlem.f	$⊢ φ \to F : Z ⟶ ℝ$
4		limsupgtlem.r	$⊢ φ \to lim sup (F) \in ℝ$
5		limsupgtlem.x	$⊢ φ \to X \in ℝ^{+}$
6		nfv	$⊢ Ⅎ j φ$
7	1 2	uzn0d	$⊢ φ \to Z \neq \emptyset$
8		rnresss	$⊢ ran ({F ↾}_{ℤ_{\geq j}}) \subseteq ran F$
9	8	a1i	$⊢ φ \to ran ({F ↾}_{ℤ_{\geq j}}) \subseteq ran F$
10	3	frexr	$⊢ φ \to F : Z ⟶ ℝ^{*}$
11	10	frnd	$⊢ φ \to ran F \subseteq ℝ^{*}$
12	9 11	sstrd	$⊢ φ \to ran ({F ↾}_{ℤ_{\geq j}}) \subseteq ℝ^{*}$
13	12	supxrcld	$⊢ φ \to sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \in ℝ^{}$
14	13	adantr	$⊢ (φ \land j \in Z) \to sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \in ℝ^{}$
15		nfcv	$⊢ \underline{Ⅎ} k F$
16	15 1 2 3	limsupreuz	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (\exists x \in ℝ \forall j \in Z \exists k \in ℤ_{\geq j} x \leq F (k) \land \exists x \in ℝ \forall k \in Z F (k) \leq x))$
17	4 16	mpbid	$⊢ φ \to (\exists x \in ℝ \forall j \in Z \exists k \in ℤ_{\geq j} x \leq F (k) \land \exists x \in ℝ \forall k \in Z F (k) \leq x)$
18	17	simpld	$⊢ φ \to \exists x \in ℝ \forall j \in Z \exists k \in ℤ_{\geq j} x \leq F (k)$
19		rexr	$⊢ x \in ℝ \to x \in ℝ^{*}$
20	19	ad4antlr	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x \leq F (k)) \to x \in ℝ^{*}$
21	3	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F : Z ⟶ ℝ$
22	2	uztrn2	$⊢ (j \in Z \land k \in ℤ_{\geq j}) \to k \in Z$
23	22	adantll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in Z$
24	21 23	ffvelrnd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ$
25	24	rexrd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ^{*}$
26	25	3impa	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F (k) \in ℝ^{*}$
27	26	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x \leq F (k)) \to F (k) \in ℝ^{*}$
28	13	ad4antr	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x \leq F (k)) \to sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \in ℝ^{}$
29		simpr	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x \leq F (k)) \to x \leq F (k)$
30	12	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to ran ({F ↾}_{ℤ_{\geq j}}) \subseteq ℝ^{*}$
31		fvres	$⊢ k \in ℤ_{\geq j} \to ({F ↾}_{ℤ_{\geq j}}) (k) = F (k)$
32	31	eqcomd	$⊢ k \in ℤ_{\geq j} \to F (k) = ({F ↾}_{ℤ_{\geq j}}) (k)$
33	32	adantl	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) = ({F ↾}_{ℤ_{\geq j}}) (k)$
34	3	ffnd	$⊢ φ \to F Fn Z$
35	34	adantr	$⊢ (φ \land j \in Z) \to F Fn Z$
36	23	ssd	$⊢ (φ \land j \in Z) \to ℤ_{\geq j} \subseteq Z$
37		fnssres	$⊢ (F Fn Z \land ℤ_{\geq j} \subseteq Z) \to ({F ↾}_{ℤ_{\geq j}}) Fn ℤ_{\geq j}$
38	35 36 37	syl2anc	$⊢ (φ \land j \in Z) \to ({F ↾}_{ℤ_{\geq j}}) Fn ℤ_{\geq j}$
39	38	adantr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to ({F ↾}_{ℤ_{\geq j}}) Fn ℤ_{\geq j}$
40		simpr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to k \in ℤ_{\geq j}$
41	39 40	fnfvelrnd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to ({F ↾}_{ℤ_{\geq j}}) (k) \in ran ({F ↾}_{ℤ_{\geq j}})$
42	33 41	eqeltrd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \in ran ({F ↾}_{ℤ_{\geq j}})$
43		eqid	$⊢ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) = sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)$
44	30 42 43	supxrubd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to F (k) \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <)$
45	44	3impa	$⊢ (φ \land j \in Z \land k \in ℤ_{\geq j}) \to F (k) \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <)$
46	45	ad5ant134	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x \leq F (k)) \to F (k) \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <)$
47	20 27 28 29 46	xrletrd	$⊢ ((((φ \land x \in ℝ) \land j \in Z) \land k \in ℤ_{\geq j}) \land x \leq F (k)) \to x \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <)$
48	47	rexlimdva2	$⊢ ((φ \land x \in ℝ) \land j \in Z) \to (\exists k \in ℤ_{\geq j} x \leq F (k) \to x \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <))$
49	48	ralimdva	$⊢ (φ \land x \in ℝ) \to (\forall j \in Z \exists k \in ℤ_{\geq j} x \leq F (k) \to \forall j \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <))$
50	49	reximdva	$⊢ φ \to (\exists x \in ℝ \forall j \in Z \exists k \in ℤ_{\geq j} x \leq F (k) \to \exists x \in ℝ \forall j \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <))$
51	18 50	mpd	$⊢ φ \to \exists x \in ℝ \forall j \in Z x \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <)$
52	5	rphalfcld	$⊢ φ \to \frac{X}{2} \in ℝ^{+}$
53	6 7 14 51 52	infrpgernmpt	$⊢ φ \to \exists j \in Z sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{*} <) +_{𝑒} (\frac{X}{2})$
54		simp3	$⊢ (φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{} <) +_{𝑒} (\frac{X}{2})) \to sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{} <) +_{𝑒} (\frac{X}{2})$
55	1 2 10	limsupvaluz	$⊢ φ \to lim sup (F) = sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{} <)$
56	55	eqcomd	$⊢ φ \to sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{} <) = lim sup (F)$
57	56	oveq1d	$⊢ φ \to sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{} <) +_{𝑒} (\frac{X}{2}) = lim sup (F) +_{𝑒} (\frac{X}{2})$
58	57	3ad2ant1	$⊢ (φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{} <) +_{𝑒} (\frac{X}{2})) \to sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{*} <) +_{𝑒} (\frac{X}{2}) = lim sup (F) +_{𝑒} (\frac{X}{2})$
59	54 58	breqtrd	$⊢ (φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{} <) +_{𝑒} (\frac{X}{2})) \to sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})$
60	25	3adantl3	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to F (k) \in ℝ^{}$
61		simpl1	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to φ$
62	61 13	syl	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \in ℝ^{*}$
63	2	fvexi	$⊢ Z \in V$
64	63	a1i	$⊢ φ \to Z \in V$
65	3 64	fexd	$⊢ φ \to F \in V$
66	65	limsupcld	$⊢ φ \to lim sup (F) \in ℝ^{*}$
67	5	rpred	$⊢ φ \to X \in ℝ$
68	67	rehalfcld	$⊢ φ \to \frac{X}{2} \in ℝ$
69	68	rexrd	$⊢ φ \to \frac{X}{2} \in ℝ^{*}$
70	66 69	xaddcld	$⊢ φ \to lim sup (F) +_{𝑒} (\frac{X}{2}) \in ℝ^{*}$
71	61 70	syl	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to lim sup (F) +_{𝑒} (\frac{X}{2}) \in ℝ^{}$
72	44	3adantl3	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to F (k) \leq sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)$
73		simpl3	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})$
74	60 62 71 72 73	xrletrd	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to F (k) \leq lim sup (F) +_{𝑒} (\frac{X}{2})$
75	4 68	rexaddd	$⊢ φ \to lim sup (F) +_{𝑒} (\frac{X}{2}) = lim sup (F) + (\frac{X}{2})$
76	61 75	syl	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to lim sup (F) +_{𝑒} (\frac{X}{2}) = lim sup (F) + (\frac{X}{2})$
77	74 76	breqtrd	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to F (k) \leq lim sup (F) + (\frac{X}{2})$
78	68	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to \frac{X}{2} \in ℝ$
79	4	ad2antrr	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to lim sup (F) \in ℝ$
80	24 78 79	lesubaddd	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (F (k) - (\frac{X}{2}) \leq lim sup (F) \leftrightarrow F (k) \leq lim sup (F) + (\frac{X}{2}))$
81	80	3adantl3	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to (F (k) - (\frac{X}{2}) \leq lim sup (F) \leftrightarrow F (k) \leq lim sup (F) + (\frac{X}{2}))$
82	77 81	mpbird	$⊢ ((φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \land k \in ℤ_{\geq j}) \to F (k) - (\frac{X}{2}) \leq lim sup (F)$
83	82	ralrimiva	$⊢ (φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{*} <) \leq lim sup (F) +_{𝑒} (\frac{X}{2})) \to \forall k \in ℤ_{\geq j} F (k) - (\frac{X}{2}) \leq lim sup (F)$
84	59 83	syld3an3	$⊢ (φ \land j \in Z \land sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{*} <) +_{𝑒} (\frac{X}{2})) \to \forall k \in ℤ_{\geq j} F (k) - (\frac{X}{2}) \leq lim sup (F)$
85	84	3exp	$⊢ φ \to (j \in Z \to (sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{*} <) +_{𝑒} (\frac{X}{2}) \to \forall k \in ℤ_{\geq j} F (k) - (\frac{X}{2}) \leq lim sup (F)))$
86	6 85	reximdai	$⊢ φ \to (\exists j \in Z sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <) \leq sup (ran (j \in Z ⟼ sup (ran ({F ↾}_{ℤ_{\geq j}}) ℝ^{} <)) ℝ^{*} <) +_{𝑒} (\frac{X}{2}) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - (\frac{X}{2}) \leq lim sup (F))$
87	53 86	mpd	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - (\frac{X}{2}) \leq lim sup (F)$
88		simpll	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to φ$
89	3	ffvelrnda	$⊢ (φ \land k \in Z) \to F (k) \in ℝ$
90	67	adantr	$⊢ (φ \land k \in Z) \to X \in ℝ$
91	89 90	resubcld	$⊢ (φ \land k \in Z) \to F (k) - X \in ℝ$
92	91	adantr	$⊢ ((φ \land k \in Z) \land F (k) - (\frac{X}{2}) \leq lim sup (F)) \to F (k) - X \in ℝ$
93	68	adantr	$⊢ (φ \land k \in Z) \to \frac{X}{2} \in ℝ$
94	89 93	resubcld	$⊢ (φ \land k \in Z) \to F (k) - (\frac{X}{2}) \in ℝ$
95	94	adantr	$⊢ ((φ \land k \in Z) \land F (k) - (\frac{X}{2}) \leq lim sup (F)) \to F (k) - (\frac{X}{2}) \in ℝ$
96	4	ad2antrr	$⊢ ((φ \land k \in Z) \land F (k) - (\frac{X}{2}) \leq lim sup (F)) \to lim sup (F) \in ℝ$
97	5	rphalfltd	$⊢ φ \to \frac{X}{2} < X$
98	97	adantr	$⊢ (φ \land k \in Z) \to \frac{X}{2} < X$
99	93 90 89 98	ltsub2dd	$⊢ (φ \land k \in Z) \to F (k) - X < F (k) - (\frac{X}{2})$
100	99	adantr	$⊢ ((φ \land k \in Z) \land F (k) - (\frac{X}{2}) \leq lim sup (F)) \to F (k) - X < F (k) - (\frac{X}{2})$
101		simpr	$⊢ ((φ \land k \in Z) \land F (k) - (\frac{X}{2}) \leq lim sup (F)) \to F (k) - (\frac{X}{2}) \leq lim sup (F)$
102	92 95 96 100 101	ltletrd	$⊢ ((φ \land k \in Z) \land F (k) - (\frac{X}{2}) \leq lim sup (F)) \to F (k) - X < lim sup (F)$
103	102	ex	$⊢ (φ \land k \in Z) \to (F (k) - (\frac{X}{2}) \leq lim sup (F) \to F (k) - X < lim sup (F))$
104	88 23 103	syl2anc	$⊢ ((φ \land j \in Z) \land k \in ℤ_{\geq j}) \to (F (k) - (\frac{X}{2}) \leq lim sup (F) \to F (k) - X < lim sup (F))$
105	104	ralimdva	$⊢ (φ \land j \in Z) \to (\forall k \in ℤ_{\geq j} F (k) - (\frac{X}{2}) \leq lim sup (F) \to \forall k \in ℤ_{\geq j} F (k) - X < lim sup (F))$
106	105	reximdva	$⊢ φ \to (\exists j \in Z \forall k \in ℤ_{\geq j} F (k) - (\frac{X}{2}) \leq lim sup (F) \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - X < lim sup (F))$
107	87 106	mpd	$⊢ φ \to \exists j \in Z \forall k \in ℤ_{\geq j} F (k) - X < lim sup (F)$

Metamath Proof Explorer

Theorem limsupgtlem

Proof