limsupbnd1

Description: If a sequence is eventually at most A , then the limsup is also at most A . (The converse is only true if the less or equal is replaced by strictly less than; consider the sequence 1 / n which is never less or equal to zero even though the limsup is.) (Contributed by Mario Carneiro, 7-Sep-2014) (Revised by AV, 12-Sep-2020)

	Ref	Expression
Hypotheses	limsupbnd.1	$⊢ φ \to B \subseteq ℝ$
	limsupbnd.2	$⊢ φ \to F : B ⟶ ℝ^{*}$
	limsupbnd.3	$⊢ φ \to A \in ℝ^{*}$
	limsupbnd1.4	$⊢ φ \to \exists k \in ℝ \forall j \in B (k \leq j \to F (j) \leq A)$
Assertion	limsupbnd1	$⊢ φ \to lim sup (F) \leq A$

Proof

Step	Hyp	Ref	Expression
1		limsupbnd.1	$⊢ φ \to B \subseteq ℝ$
2		limsupbnd.2	$⊢ φ \to F : B ⟶ ℝ^{*}$
3		limsupbnd.3	$⊢ φ \to A \in ℝ^{*}$
4		limsupbnd1.4	$⊢ φ \to \exists k \in ℝ \forall j \in B (k \leq j \to F (j) \leq A)$
5	1	adantr	$⊢ (φ \land k \in ℝ) \to B \subseteq ℝ$
6	2	adantr	$⊢ (φ \land k \in ℝ) \to F : B ⟶ ℝ^{*}$
7		simpr	$⊢ (φ \land k \in ℝ) \to k \in ℝ$
8	3	adantr	$⊢ (φ \land k \in ℝ) \to A \in ℝ^{*}$
9		eqid	$⊢ (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) = (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <))$
10	9	limsupgle	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land k \in ℝ \land A \in ℝ^{}) \to ((n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k) \leq A \leftrightarrow \forall j \in B (k \leq j \to F (j) \leq A))$
11	5 6 7 8 10	syl211anc	$⊢ (φ \land k \in ℝ) \to ((n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k) \leq A \leftrightarrow \forall j \in B (k \leq j \to F (j) \leq A))$
12		reex	$⊢ ℝ \in V$
13	12	ssex	$⊢ B \subseteq ℝ \to B \in V$
14	1 13	syl	$⊢ φ \to B \in V$
15		xrex	$⊢ ℝ^{*} \in V$
16	15	a1i	$⊢ φ \to ℝ^{*} \in V$
17		fex2	$⊢ (F : B ⟶ ℝ^{} \land B \in V \land ℝ^{} \in V) \to F \in V$
18	2 14 16 17	syl3anc	$⊢ φ \to F \in V$
19		limsupcl	$⊢ F \in V \to lim sup (F) \in ℝ^{*}$
20	18 19	syl	$⊢ φ \to lim sup (F) \in ℝ^{*}$
21	20	xrleidd	$⊢ φ \to lim sup (F) \leq lim sup (F)$
22	9	limsuple	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land lim sup (F) \in ℝ^{}) \to (lim sup (F) \leq lim sup (F) \leftrightarrow \forall k \in ℝ lim sup (F) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k))$
23	1 2 20 22	syl3anc	$⊢ φ \to (lim sup (F) \leq lim sup (F) \leftrightarrow \forall k \in ℝ lim sup (F) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k))$
24	21 23	mpbid	$⊢ φ \to \forall k \in ℝ lim sup (F) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k)$
25	24	r19.21bi	$⊢ (φ \land k \in ℝ) \to lim sup (F) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k)$
26	20	adantr	$⊢ (φ \land k \in ℝ) \to lim sup (F) \in ℝ^{*}$
27	9	limsupgf	$⊢ (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) : ℝ ⟶ ℝ^{*}$
28	27	a1i	$⊢ φ \to (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) : ℝ ⟶ ℝ^{*}$
29	28	ffvelrnda	$⊢ (φ \land k \in ℝ) \to (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k) \in ℝ^{*}$
30		xrletr	$⊢ (lim sup (F) \in ℝ^{} \land (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k) \in ℝ^{} \land A \in ℝ^{}) \to ((lim sup (F) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k) \land (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{*} <)) (k) \leq A) \to lim sup (F) \leq A)$
31	26 29 8 30	syl3anc	$⊢ (φ \land k \in ℝ) \to ((lim sup (F) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k) \land (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k) \leq A) \to lim sup (F) \leq A)$
32	25 31	mpand	$⊢ (φ \land k \in ℝ) \to ((n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (k) \leq A \to lim sup (F) \leq A)$
33	11 32	sylbird	$⊢ (φ \land k \in ℝ) \to (\forall j \in B (k \leq j \to F (j) \leq A) \to lim sup (F) \leq A)$
34	33	rexlimdva	$⊢ φ \to (\exists k \in ℝ \forall j \in B (k \leq j \to F (j) \leq A) \to lim sup (F) \leq A)$
35	4 34	mpd	$⊢ φ \to lim sup (F) \leq A$

Metamath Proof Explorer

Theorem limsupbnd1

Proof