Metamath Proof Explorer


Theorem limsupvaluz2

Description: The superior limit, when the domain of a real-valued function is a set of upper integers, and the superior limit is real. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupvaluz2.m φ M
limsupvaluz2.z Z = M
limsupvaluz2.f φ F : Z
limsupvaluz2.r φ lim sup F
Assertion limsupvaluz2 φ lim sup F = sup ran k Z sup ran F k * < <

Proof

Step Hyp Ref Expression
1 limsupvaluz2.m φ M
2 limsupvaluz2.z Z = M
3 limsupvaluz2.f φ F : Z
4 limsupvaluz2.r φ lim sup F
5 3 frexr φ F : Z *
6 1 2 5 limsupvaluz φ lim sup F = sup ran n Z sup ran F n * < * <
7 3 adantr φ n Z F : Z
8 id n Z n Z
9 2 8 uzssd2 n Z n Z
10 9 adantl φ n Z n Z
11 7 10 feqresmpt φ n Z F n = m n F m
12 11 rneqd φ n Z ran F n = ran m n F m
13 12 supeq1d φ n Z sup ran F n * < = sup ran m n F m * <
14 nfcv _ m F
15 4 renepnfd φ lim sup F +∞
16 14 2 3 15 limsupubuz φ x m Z F m x
17 16 adantr φ n Z x m Z F m x
18 ssralv n Z m Z F m x m n F m x
19 9 18 syl n Z m Z F m x m n F m x
20 19 adantl φ n Z m Z F m x m n F m x
21 20 reximdv φ n Z x m Z F m x x m n F m x
22 17 21 mpd φ n Z x m n F m x
23 nfv m φ n Z
24 2 eluzelz2 n Z n
25 uzid n n n
26 ne0i n n n
27 24 25 26 3syl n Z n
28 27 adantl φ n Z n
29 7 adantr φ n Z m n F : Z
30 10 sselda φ n Z m n m Z
31 29 30 ffvelrnd φ n Z m n F m
32 23 28 31 supxrre3rnmpt φ n Z sup ran m n F m * < x m n F m x
33 22 32 mpbird φ n Z sup ran m n F m * <
34 13 33 eqeltrd φ n Z sup ran F n * <
35 34 fmpttd φ n Z sup ran F n * < : Z
36 35 frnd φ ran n Z sup ran F n * <
37 nfv n φ
38 34 elexd φ n Z sup ran F n * < V
39 eqid n Z sup ran F n * < = n Z sup ran F n * <
40 1 2 uzn0d φ Z
41 37 38 39 40 rnmptn0 φ ran n Z sup ran F n * <
42 nfcv _ j F
43 42 1 2 5 limsupre3uz φ lim sup F x i Z j i x F j x i Z j i F j x
44 4 43 mpbid φ x i Z j i x F j x i Z j i F j x
45 44 simpld φ x i Z j i x F j
46 simp-4r φ x i Z j i x F j x
47 46 rexrd φ x i Z j i x F j x *
48 5 3ad2ant1 φ i Z j i F : Z *
49 2 uztrn2 i Z j i j Z
50 49 3adant1 φ i Z j i j Z
51 48 50 ffvelrnd φ i Z j i F j *
52 51 ad5ant134 φ x i Z j i x F j F j *
53 rnresss ran F i ran F
54 53 a1i φ i Z ran F i ran F
55 3 frnd φ ran F
56 55 adantr φ i Z ran F
57 54 56 sstrd φ i Z ran F i
58 ressxr *
59 58 a1i φ i Z *
60 57 59 sstrd φ i Z ran F i *
61 60 supxrcld φ i Z sup ran F i * < *
62 61 ad5ant13 φ x i Z j i x F j sup ran F i * < *
63 simpr φ x i Z j i x F j x F j
64 60 3adant3 φ i Z j i ran F i *
65 fvres j i F i j = F j
66 65 eqcomd j i F j = F i j
67 66 3ad2ant3 φ i Z j i F j = F i j
68 3 ffnd φ F Fn Z
69 68 adantr φ i Z F Fn Z
70 id i Z i Z
71 2 70 uzssd2 i Z i Z
72 71 adantl φ i Z i Z
73 fnssres F Fn Z i Z F i Fn i
74 69 72 73 syl2anc φ i Z F i Fn i
75 74 3adant3 φ i Z j i F i Fn i
76 simp3 φ i Z j i j i
77 fnfvelrn F i Fn i j i F i j ran F i
78 75 76 77 syl2anc φ i Z j i F i j ran F i
79 67 78 eqeltrd φ i Z j i F j ran F i
80 eqid sup ran F i * < = sup ran F i * <
81 64 79 80 supxrubd φ i Z j i F j sup ran F i * <
82 81 ad5ant134 φ x i Z j i x F j F j sup ran F i * <
83 47 52 62 63 82 xrletrd φ x i Z j i x F j x sup ran F i * <
84 83 rexlimdva2 φ x i Z j i x F j x sup ran F i * <
85 84 ralimdva φ x i Z j i x F j i Z x sup ran F i * <
86 85 reximdva φ x i Z j i x F j x i Z x sup ran F i * <
87 45 86 mpd φ x i Z x sup ran F i * <
88 87 idi φ x i Z x sup ran F i * <
89 fveq2 n = i n = i
90 89 reseq2d n = i F n = F i
91 90 rneqd n = i ran F n = ran F i
92 91 supeq1d n = i sup ran F n * < = sup ran F i * <
93 eqcom n = i i = n
94 93 imbi1i n = i sup ran F n * < = sup ran F i * < i = n sup ran F n * < = sup ran F i * <
95 eqcom sup ran F n * < = sup ran F i * < sup ran F i * < = sup ran F n * <
96 95 imbi2i i = n sup ran F n * < = sup ran F i * < i = n sup ran F i * < = sup ran F n * <
97 94 96 bitri n = i sup ran F n * < = sup ran F i * < i = n sup ran F i * < = sup ran F n * <
98 92 97 mpbi i = n sup ran F i * < = sup ran F n * <
99 98 breq2d i = n x sup ran F i * < x sup ran F n * <
100 99 cbvralv i Z x sup ran F i * < n Z x sup ran F n * <
101 100 rexbii x i Z x sup ran F i * < x n Z x sup ran F n * <
102 88 101 sylib φ x n Z x sup ran F n * <
103 37 38 rnmptbd2 φ x n Z x sup ran F n * < x y ran n Z sup ran F n * < x y
104 102 103 mpbid φ x y ran n Z sup ran F n * < x y
105 infxrre ran n Z sup ran F n * < ran n Z sup ran F n * < x y ran n Z sup ran F n * < x y sup ran n Z sup ran F n * < * < = sup ran n Z sup ran F n * < <
106 36 41 104 105 syl3anc φ sup ran n Z sup ran F n * < * < = sup ran n Z sup ran F n * < <
107 fveq2 n = k n = k
108 107 reseq2d n = k F n = F k
109 108 rneqd n = k ran F n = ran F k
110 109 supeq1d n = k sup ran F n * < = sup ran F k * <
111 110 cbvmptv n Z sup ran F n * < = k Z sup ran F k * <
112 111 rneqi ran n Z sup ran F n * < = ran k Z sup ran F k * <
113 112 infeq1i sup ran n Z sup ran F n * < < = sup ran k Z sup ran F k * < <
114 113 a1i φ sup ran n Z sup ran F n * < < = sup ran k Z sup ran F k * < <
115 6 106 114 3eqtrd φ lim sup F = sup ran k Z sup ran F k * < <