Metamath Proof Explorer


Theorem 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 φ B
limsupre.2 φ sup B * < = +∞
limsupre.f φ F : B
limsupre.bnd φ b k j B k j F j b
Assertion limsupre φ lim sup F

Proof

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