limsupbnd2

Description: If a sequence is eventually greater than A , then the limsup is also greater than A . (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 ℝ^{*}$
	limsupbnd2.4	$⊢ φ \to sup (B ℝ^{*} <) = +∞$
	limsupbnd2.5	$⊢ φ \to \exists k \in ℝ \forall j \in B (k \leq j \to A \leq F (j))$
Assertion	limsupbnd2	$⊢ φ \to A \leq lim sup (F)$

Proof

Step	Hyp	Ref	Expression
1		limsupbnd.1	$⊢ φ \to B \subseteq ℝ$
2		limsupbnd.2	$⊢ φ \to F : B ⟶ ℝ^{*}$
3		limsupbnd.3	$⊢ φ \to A \in ℝ^{*}$
4		limsupbnd2.4	$⊢ φ \to sup (B ℝ^{*} <) = +∞$
5		limsupbnd2.5	$⊢ φ \to \exists k \in ℝ \forall j \in B (k \leq j \to A \leq F (j))$
6		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
7	1 6	sstrdi	$⊢ φ \to B \subseteq ℝ^{*}$
8		supxrunb1	$⊢ B \subseteq ℝ^{} \to (\forall n \in ℝ \exists j \in B n \leq j \leftrightarrow sup (B ℝ^{} <) = +∞)$
9	7 8	syl	$⊢ φ \to (\forall n \in ℝ \exists j \in B n \leq j \leftrightarrow sup (B ℝ^{*} <) = +∞)$
10	4 9	mpbird	$⊢ φ \to \forall n \in ℝ \exists j \in B n \leq j$
11		ifcl	$⊢ (m \in ℝ \land k \in ℝ) \to if (k \leq m, m, k) \in ℝ$
12		breq1	$⊢ n = if (k \leq m, m, k) \to (n \leq j \leftrightarrow if (k \leq m, m, k) \leq j)$
13	12	rexbidv	$⊢ n = if (k \leq m, m, k) \to (\exists j \in B n \leq j \leftrightarrow \exists j \in B if (k \leq m, m, k) \leq j)$
14	13	rspccva	$⊢ (\forall n \in ℝ \exists j \in B n \leq j \land if (k \leq m, m, k) \in ℝ) \to \exists j \in B if (k \leq m, m, k) \leq j$
15	10 11 14	syl2an	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to \exists j \in B if (k \leq m, m, k) \leq j$
16		r19.29	$⊢ (\forall j \in B (k \leq j \to A \leq F (j)) \land \exists j \in B if (k \leq m, m, k) \leq j) \to \exists j \in B ((k \leq j \to A \leq F (j)) \land if (k \leq m, m, k) \leq j)$
17		simplrr	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to k \in ℝ$
18		simprl	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to m \in ℝ$
19	18	adantr	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to m \in ℝ$
20		max1	$⊢ (k \in ℝ \land m \in ℝ) \to k \leq if (k \leq m, m, k)$
21	17 19 20	syl2anc	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to k \leq if (k \leq m, m, k)$
22	19 17 11	syl2anc	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to if (k \leq m, m, k) \in ℝ$
23	1	adantr	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to B \subseteq ℝ$
24	23	sselda	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to j \in ℝ$
25		letr	$⊢ (k \in ℝ \land if (k \leq m, m, k) \in ℝ \land j \in ℝ) \to ((k \leq if (k \leq m, m, k) \land if (k \leq m, m, k) \leq j) \to k \leq j)$
26	17 22 24 25	syl3anc	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to ((k \leq if (k \leq m, m, k) \land if (k \leq m, m, k) \leq j) \to k \leq j)$
27	21 26	mpand	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (if (k \leq m, m, k) \leq j \to k \leq j)$
28	27	imim1d	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to ((k \leq j \to A \leq F (j)) \to (if (k \leq m, m, k) \leq j \to A \leq F (j)))$
29	28	impd	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (((k \leq j \to A \leq F (j)) \land if (k \leq m, m, k) \leq j) \to A \leq F (j))$
30		max2	$⊢ (k \in ℝ \land m \in ℝ) \to m \leq if (k \leq m, m, k)$
31	17 19 30	syl2anc	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to m \leq if (k \leq m, m, k)$
32		letr	$⊢ (m \in ℝ \land if (k \leq m, m, k) \in ℝ \land j \in ℝ) \to ((m \leq if (k \leq m, m, k) \land if (k \leq m, m, k) \leq j) \to m \leq j)$
33	19 22 24 32	syl3anc	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to ((m \leq if (k \leq m, m, k) \land if (k \leq m, m, k) \leq j) \to m \leq j)$
34	31 33	mpand	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (if (k \leq m, m, k) \leq j \to m \leq j)$
35	34	adantld	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (((k \leq j \to A \leq F (j)) \land if (k \leq m, m, k) \leq j) \to m \leq j)$
36		eqid	$⊢ (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) = (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <))$
37	36	limsupgf	$⊢ (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) : ℝ ⟶ ℝ^{*}$
38	37	ffvelrni	$⊢ m \in ℝ \to (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \in ℝ^{*}$
39	38	adantl	$⊢ (φ \land m \in ℝ) \to (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \in ℝ^{*}$
40	39	xrleidd	$⊢ (φ \land m \in ℝ) \to (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m)$
41	40	adantrr	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m)$
42	2	adantr	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to F : B ⟶ ℝ^{*}$
43	18 38	syl	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \in ℝ^{*}$
44	36	limsupgle	$⊢ ((B \subseteq ℝ \land F : B ⟶ ℝ^{}) \land m \in ℝ \land (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \in ℝ^{}) \to ((n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \leftrightarrow \forall j \in B (m \leq j \to F (j) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m)))$
45	23 42 18 43 44	syl211anc	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to ((n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \leftrightarrow \forall j \in B (m \leq j \to F (j) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m)))$
46	41 45	mpbid	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to \forall j \in B (m \leq j \to F (j) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
47	46	r19.21bi	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (m \leq j \to F (j) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
48	35 47	syld	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (((k \leq j \to A \leq F (j)) \land if (k \leq m, m, k) \leq j) \to F (j) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
49	29 48	jcad	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (((k \leq j \to A \leq F (j)) \land if (k \leq m, m, k) \leq j) \to (A \leq F (j) \land F (j) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m)))$
50	3	ad2antrr	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to A \in ℝ^{*}$
51	42	ffvelrnda	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to F (j) \in ℝ^{*}$
52	43	adantr	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \in ℝ^{*}$
53		xrletr	$⊢ (A \in ℝ^{} \land F (j) \in ℝ^{} \land (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m) \in ℝ^{}) \to ((A \leq F (j) \land F (j) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m)) \to A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{*} <)) (m))$
54	50 51 52 53	syl3anc	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to ((A \leq F (j) \land F (j) \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m)) \to A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
55	49 54	syld	$⊢ ((φ \land (m \in ℝ \land k \in ℝ)) \land j \in B) \to (((k \leq j \to A \leq F (j)) \land if (k \leq m, m, k) \leq j) \to A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
56	55	rexlimdva	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to (\exists j \in B ((k \leq j \to A \leq F (j)) \land if (k \leq m, m, k) \leq j) \to A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
57	16 56	syl5	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to ((\forall j \in B (k \leq j \to A \leq F (j)) \land \exists j \in B if (k \leq m, m, k) \leq j) \to A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
58	15 57	mpan2d	$⊢ (φ \land (m \in ℝ \land k \in ℝ)) \to (\forall j \in B (k \leq j \to A \leq F (j)) \to A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
59	58	anassrs	$⊢ ((φ \land m \in ℝ) \land k \in ℝ) \to (\forall j \in B (k \leq j \to A \leq F (j)) \to A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
60	59	rexlimdva	$⊢ (φ \land m \in ℝ) \to (\exists k \in ℝ \forall j \in B (k \leq j \to A \leq F (j)) \to A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
61	60	ralrimdva	$⊢ φ \to (\exists k \in ℝ \forall j \in B (k \leq j \to A \leq F (j)) \to \forall m \in ℝ A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
62	5 61	mpd	$⊢ φ \to \forall m \in ℝ A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m)$
63	36	limsuple	$⊢ (B \subseteq ℝ \land F : B ⟶ ℝ^{} \land A \in ℝ^{}) \to (A \leq lim sup (F) \leftrightarrow \forall m \in ℝ A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
64	1 2 3 63	syl3anc	$⊢ φ \to (A \leq lim sup (F) \leftrightarrow \forall m \in ℝ A \leq (n \in ℝ ⟼ sup (F [[n, +∞)] \cap ℝ^{} ℝ^{} <)) (m))$
65	62 64	mpbird	$⊢ φ \to A \leq lim sup (F)$

Metamath Proof Explorer

Theorem limsupbnd2

Proof