limsupre

Description: If a sequence is bounded, then the limsup is real. (Contributed by Glauco Siliprandi, 11-Dec-2019) (Revised by AV, 13-Sep-2020)

	Ref	Expression
Hypotheses	limsupre.1	$⊢ φ \to B \subseteq ℝ$
	limsupre.2	$⊢ φ \to sup (B ℝ^{*} <) = +∞$
	limsupre.f	$⊢ φ \to F : B ⟶ ℝ$
	limsupre.bnd	$⊢ φ \to \exists b \in ℝ \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)$
Assertion	limsupre	$⊢ φ \to lim sup (F) \in ℝ$

Proof

Step	Hyp	Ref	Expression
1		limsupre.1	$⊢ φ \to B \subseteq ℝ$
2		limsupre.2	$⊢ φ \to sup (B ℝ^{*} <) = +∞$
3		limsupre.f	$⊢ φ \to F : B ⟶ ℝ$
4		limsupre.bnd	$⊢ φ \to \exists b \in ℝ \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)$
5		mnfxr	$⊢ −∞ \in ℝ^{*}$
6	5	a1i	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to −∞ \in ℝ^{*}$
7		renegcl	$⊢ b \in ℝ \to - b \in ℝ$
8	7	rexrd	$⊢ b \in ℝ \to - b \in ℝ^{*}$
9	8	ad2antlr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to - b \in ℝ^{*}$
10		reex	$⊢ ℝ \in V$
11	10	a1i	$⊢ φ \to ℝ \in V$
12	11 1	ssexd	$⊢ φ \to B \in V$
13		fex	$⊢ (F : B ⟶ ℝ \land B \in V) \to F \in V$
14	3 12 13	syl2anc	$⊢ φ \to F \in V$
15		limsupcl	$⊢ F \in V \to lim sup (F) \in ℝ^{*}$
16	14 15	syl	$⊢ φ \to lim sup (F) \in ℝ^{*}$
17	16	ad2antrr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to lim sup (F) \in ℝ^{*}$
18	7	mnfltd	$⊢ b \in ℝ \to −∞ < - b$
19	18	ad2antlr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to −∞ < - b$
20	1	ad2antrr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to B \subseteq ℝ$
21		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
22	21	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
23	3 22	fssd	$⊢ φ \to F : B ⟶ ℝ^{*}$
24	23	ad2antrr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to F : B ⟶ ℝ^{*}$
25	2	ad2antrr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to sup (B ℝ^{*} <) = +∞$
26		simpr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)$
27		nfv	$⊢ Ⅎ k (φ \land b \in ℝ)$
28		nfre1	$⊢ Ⅎ k \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)$
29	27 28	nfan	$⊢ Ⅎ k ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b))$
30		nfv	$⊢ Ⅎ j (φ \land b \in ℝ)$
31		nfv	$⊢ Ⅎ j k \in ℝ$
32		nfra1	$⊢ Ⅎ j \forall j \in B (k \leq j \to \|F (j)\| \leq b)$
33	30 31 32	nf3an	$⊢ Ⅎ j ((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b))$
34		simp13	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to \forall j \in B (k \leq j \to \|F (j)\| \leq b)$
35		simp2	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to j \in B$
36		simp3	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to k \leq j$
37		rspa	$⊢ (\forall j \in B (k \leq j \to \|F (j)\| \leq b) \land j \in B) \to (k \leq j \to \|F (j)\| \leq b)$
38	37	imp	$⊢ ((\forall j \in B (k \leq j \to \|F (j)\| \leq b) \land j \in B) \land k \leq j) \to \|F (j)\| \leq b$
39	34 35 36 38	syl21anc	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to \|F (j)\| \leq b$
40		simp11l	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to φ$
41	3	ffvelrnda	$⊢ (φ \land j \in B) \to F (j) \in ℝ$
42	40 35 41	syl2anc	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to F (j) \in ℝ$
43		simp11r	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to b \in ℝ$
44	42 43	absled	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to (\|F (j)\| \leq b \leftrightarrow (- b \leq F (j) \land F (j) \leq b))$
45	39 44	mpbid	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to (- b \leq F (j) \land F (j) \leq b)$
46	45	simpld	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to - b \leq F (j)$
47	46	3exp	$⊢ ((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to (j \in B \to (k \leq j \to - b \leq F (j)))$
48	33 47	ralrimi	$⊢ ((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to \forall j \in B (k \leq j \to - b \leq F (j))$
49	48	3exp	$⊢ (φ \land b \in ℝ) \to (k \in ℝ \to (\forall j \in B (k \leq j \to \|F (j)\| \leq b) \to \forall j \in B (k \leq j \to - b \leq F (j))))$
50	49	adantr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to (k \in ℝ \to (\forall j \in B (k \leq j \to \|F (j)\| \leq b) \to \forall j \in B (k \leq j \to - b \leq F (j))))$
51	29 50	reximdai	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to (\exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b) \to \exists k \in ℝ \forall j \in B (k \leq j \to - b \leq F (j)))$
52	26 51	mpd	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to \exists k \in ℝ \forall j \in B (k \leq j \to - b \leq F (j))$
53		breq2	$⊢ i = j \to (h \leq i \leftrightarrow h \leq j)$
54		fveq2	$⊢ i = j \to F (i) = F (j)$
55	54	breq2d	$⊢ i = j \to (- b \leq F (i) \leftrightarrow - b \leq F (j))$
56	53 55	imbi12d	$⊢ i = j \to ((h \leq i \to - b \leq F (i)) \leftrightarrow (h \leq j \to - b \leq F (j)))$
57	56	cbvralvw	$⊢ \forall i \in B (h \leq i \to - b \leq F (i)) \leftrightarrow \forall j \in B (h \leq j \to - b \leq F (j))$
58		breq1	$⊢ h = k \to (h \leq j \leftrightarrow k \leq j)$
59	58	imbi1d	$⊢ h = k \to ((h \leq j \to - b \leq F (j)) \leftrightarrow (k \leq j \to - b \leq F (j)))$
60	59	ralbidv	$⊢ h = k \to (\forall j \in B (h \leq j \to - b \leq F (j)) \leftrightarrow \forall j \in B (k \leq j \to - b \leq F (j)))$
61	57 60	syl5bb	$⊢ h = k \to (\forall i \in B (h \leq i \to - b \leq F (i)) \leftrightarrow \forall j \in B (k \leq j \to - b \leq F (j)))$
62	61	cbvrexvw	$⊢ \exists h \in ℝ \forall i \in B (h \leq i \to - b \leq F (i)) \leftrightarrow \exists k \in ℝ \forall j \in B (k \leq j \to - b \leq F (j))$
63	52 62	sylibr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to \exists h \in ℝ \forall i \in B (h \leq i \to - b \leq F (i))$
64	20 24 9 25 63	limsupbnd2	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to - b \leq lim sup (F)$
65	6 9 17 19 64	xrltletrd	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to −∞ < lim sup (F)$
66	65 4	r19.29a	$⊢ φ \to −∞ < lim sup (F)$
67		rexr	$⊢ b \in ℝ \to b \in ℝ^{*}$
68	67	ad2antlr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to b \in ℝ^{*}$
69		pnfxr	$⊢ +∞ \in ℝ^{*}$
70	69	a1i	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to +∞ \in ℝ^{*}$
71	45	simprd	$⊢ (((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \land j \in B \land k \leq j) \to F (j) \leq b$
72	71	3exp	$⊢ ((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to (j \in B \to (k \leq j \to F (j) \leq b))$
73	33 72	ralrimi	$⊢ ((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to \forall j \in B (k \leq j \to F (j) \leq b)$
74	73	3exp	$⊢ (φ \land b \in ℝ) \to (k \in ℝ \to (\forall j \in B (k \leq j \to \|F (j)\| \leq b) \to \forall j \in B (k \leq j \to F (j) \leq b)))$
75	74	adantr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to (k \in ℝ \to (\forall j \in B (k \leq j \to \|F (j)\| \leq b) \to \forall j \in B (k \leq j \to F (j) \leq b)))$
76	29 75	reximdai	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to (\exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b) \to \exists k \in ℝ \forall j \in B (k \leq j \to F (j) \leq b))$
77	26 76	mpd	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to \exists k \in ℝ \forall j \in B (k \leq j \to F (j) \leq b)$
78	54	breq1d	$⊢ i = j \to (F (i) \leq b \leftrightarrow F (j) \leq b)$
79	53 78	imbi12d	$⊢ i = j \to ((h \leq i \to F (i) \leq b) \leftrightarrow (h \leq j \to F (j) \leq b))$
80	79	cbvralvw	$⊢ \forall i \in B (h \leq i \to F (i) \leq b) \leftrightarrow \forall j \in B (h \leq j \to F (j) \leq b)$
81	58	imbi1d	$⊢ h = k \to ((h \leq j \to F (j) \leq b) \leftrightarrow (k \leq j \to F (j) \leq b))$
82	81	ralbidv	$⊢ h = k \to (\forall j \in B (h \leq j \to F (j) \leq b) \leftrightarrow \forall j \in B (k \leq j \to F (j) \leq b))$
83	80 82	syl5bb	$⊢ h = k \to (\forall i \in B (h \leq i \to F (i) \leq b) \leftrightarrow \forall j \in B (k \leq j \to F (j) \leq b))$
84	83	cbvrexvw	$⊢ \exists h \in ℝ \forall i \in B (h \leq i \to F (i) \leq b) \leftrightarrow \exists k \in ℝ \forall j \in B (k \leq j \to F (j) \leq b)$
85	77 84	sylibr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to \exists h \in ℝ \forall i \in B (h \leq i \to F (i) \leq b)$
86	20 24 68 85	limsupbnd1	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to lim sup (F) \leq b$
87		ltpnf	$⊢ b \in ℝ \to b < +∞$
88	87	ad2antlr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to b < +∞$
89	17 68 70 86 88	xrlelttrd	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to lim sup (F) < +∞$
90	89 4	r19.29a	$⊢ φ \to lim sup (F) < +∞$
91		xrrebnd	$⊢ lim sup (F) \in ℝ^{*} \to (lim sup (F) \in ℝ \leftrightarrow (−∞ < lim sup (F) \land lim sup (F) < +∞))$
92	16 91	syl	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (−∞ < lim sup (F) \land lim sup (F) < +∞))$
93	66 90 92	mpbir2and	$⊢ φ \to lim sup (F) \in ℝ$

Metamath Proof Explorer

Theorem limsupre

Proof