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	3 12	fexd	$⊢ φ \to F \in V$
14		limsupcl	$⊢ F \in V \to lim sup (F) \in ℝ^{*}$
15	13 14	syl	$⊢ φ \to lim sup (F) \in ℝ^{*}$
16	15	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 ℝ^{*}$
17	7	mnfltd	$⊢ b \in ℝ \to −∞ < - b$
18	17	ad2antlr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to −∞ < - b$
19	1	ad2antrr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to B \subseteq ℝ$
20		ressxr	$⊢ ℝ \subseteq ℝ^{*}$
21	20	a1i	$⊢ φ \to ℝ \subseteq ℝ^{*}$
22	3 21	fssd	$⊢ φ \to F : B ⟶ ℝ^{*}$
23	22	ad2antrr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to F : B ⟶ ℝ^{*}$
24	2	ad2antrr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to sup (B ℝ^{*} <) = +∞$
25		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)$
26		nfv	$⊢ Ⅎ k (φ \land b \in ℝ)$
27		nfre1	$⊢ Ⅎ k \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)$
28	26 27	nfan	$⊢ Ⅎ k ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b))$
29		nfv	$⊢ Ⅎ j (φ \land b \in ℝ)$
30		nfv	$⊢ Ⅎ j k \in ℝ$
31		nfra1	$⊢ Ⅎ j \forall j \in B (k \leq j \to \|F (j)\| \leq b)$
32	29 30 31	nf3an	$⊢ Ⅎ j ((φ \land b \in ℝ) \land k \in ℝ \land \forall j \in B (k \leq j \to \|F (j)\| \leq b))$
33		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)$
34		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$
35		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$
36		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)$
37	36	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$
38	33 34 35 37	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$
39		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 φ$
40	3	ffvelrnda	$⊢ (φ \land j \in B) \to F (j) \in ℝ$
41	39 34 40	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 ℝ$
42		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 ℝ$
43	41 42	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))$
44	38 43	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)$
45	44	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)$
46	45	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)))$
47	32 46	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))$
48	47	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))))$
49	48	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))))$
50	28 49	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)))$
51	25 50	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))$
52		breq2	$⊢ i = j \to (h \leq i \leftrightarrow h \leq j)$
53		fveq2	$⊢ i = j \to F (i) = F (j)$
54	53	breq2d	$⊢ i = j \to (- b \leq F (i) \leftrightarrow - b \leq F (j))$
55	52 54	imbi12d	$⊢ i = j \to ((h \leq i \to - b \leq F (i)) \leftrightarrow (h \leq j \to - b \leq F (j)))$
56	55	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))$
57		breq1	$⊢ h = k \to (h \leq j \leftrightarrow k \leq j)$
58	57	imbi1d	$⊢ h = k \to ((h \leq j \to - b \leq F (j)) \leftrightarrow (k \leq j \to - b \leq F (j)))$
59	58	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)))$
60	56 59	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)))$
61	60	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))$
62	51 61	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))$
63	19 23 9 24 62	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)$
64	6 9 16 18 63	xrltletrd	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to −∞ < lim sup (F)$
65	64 4	r19.29a	$⊢ φ \to −∞ < lim sup (F)$
66		rexr	$⊢ b \in ℝ \to b \in ℝ^{*}$
67	66	ad2antlr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to b \in ℝ^{*}$
68		pnfxr	$⊢ +∞ \in ℝ^{*}$
69	68	a1i	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to +∞ \in ℝ^{*}$
70	44	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$
71	70	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))$
72	32 71	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)$
73	72	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)))$
74	73	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)))$
75	28 74	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))$
76	25 75	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)$
77	53	breq1d	$⊢ i = j \to (F (i) \leq b \leftrightarrow F (j) \leq b)$
78	52 77	imbi12d	$⊢ i = j \to ((h \leq i \to F (i) \leq b) \leftrightarrow (h \leq j \to F (j) \leq b))$
79	78	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)$
80	57	imbi1d	$⊢ h = k \to ((h \leq j \to F (j) \leq b) \leftrightarrow (k \leq j \to F (j) \leq b))$
81	80	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))$
82	79 81	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))$
83	82	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)$
84	76 83	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)$
85	19 23 67 84	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$
86		ltpnf	$⊢ b \in ℝ \to b < +∞$
87	86	ad2antlr	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to b < +∞$
88	16 67 69 85 87	xrlelttrd	$⊢ ((φ \land b \in ℝ) \land \exists k \in ℝ \forall j \in B (k \leq j \to \|F (j)\| \leq b)) \to lim sup (F) < +∞$
89	88 4	r19.29a	$⊢ φ \to lim sup (F) < +∞$
90		xrrebnd	$⊢ lim sup (F) \in ℝ^{*} \to (lim sup (F) \in ℝ \leftrightarrow (−∞ < lim sup (F) \land lim sup (F) < +∞))$
91	15 90	syl	$⊢ φ \to (lim sup (F) \in ℝ \leftrightarrow (−∞ < lim sup (F) \land lim sup (F) < +∞))$
92	65 89 91	mpbir2and	$⊢ φ \to lim sup (F) \in ℝ$

Metamath Proof Explorer

Theorem limsupre

Proof