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 = inf 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 = inf ran n Z sup ran F n * < * <
7 3 adantr φ n Z F : Z
8 2 uzssd3 n Z n Z
9 8 adantl φ n Z n Z
10 7 9 feqresmpt φ n Z F n = m n F m
11 10 rneqd φ n Z ran F n = ran m n F m
12 11 supeq1d φ n Z sup ran F n * < = sup ran m n F m * <
13 nfcv _ m F
14 4 renepnfd φ lim sup F +∞
15 13 2 3 14 limsupubuz φ x m Z F m x
16 15 adantr φ n Z x m Z F m x
17 ssralv n Z m Z F m x m n F m x
18 8 17 syl n Z m Z F m x m n F m x
19 18 adantl φ n Z m Z F m x m n F m x
20 19 reximdv φ n Z x m Z F m x x m n F m x
21 16 20 mpd φ n Z x m n F m x
22 nfv m φ n Z
23 2 eluzelz2 n Z n
24 uzid n n n
25 ne0i n n n
26 23 24 25 3syl n Z n
27 26 adantl φ n Z n
28 7 adantr φ n Z m n F : Z
29 9 sselda φ n Z m n m Z
30 28 29 ffvelcdmd φ n Z m n F m
31 22 27 30 supxrre3rnmpt φ n Z sup ran m n F m * < x m n F m x
32 21 31 mpbird φ n Z sup ran m n F m * <
33 12 32 eqeltrd φ n Z sup ran F n * <
34 33 fmpttd φ n Z sup ran F n * < : Z
35 34 frnd φ ran n Z sup ran F n * <
36 nfv n φ
37 eqid n Z sup ran F n * < = n Z sup ran F n * <
38 1 2 uzn0d φ Z
39 36 33 37 38 rnmptn0 φ ran n Z sup ran F n * <
40 nfcv _ j F
41 40 1 2 5 limsupre3uz φ lim sup F x i Z j i x F j x i Z j i F j x
42 4 41 mpbid φ x i Z j i x F j x i Z j i F j x
43 42 simpld φ x i Z j i x F j
44 simp-4r φ x i Z j i x F j x
45 44 rexrd φ x i Z j i x F j x *
46 5 3ad2ant1 φ i Z j i F : Z *
47 2 uztrn2 i Z j i j Z
48 47 3adant1 φ i Z j i j Z
49 46 48 ffvelcdmd φ i Z j i F j *
50 49 ad5ant134 φ x i Z j i x F j F j *
51 rnresss ran F i ran F
52 3 frnd φ ran F
53 52 adantr φ i Z ran F
54 51 53 sstrid φ i Z ran F i
55 54 ssrexr φ i Z ran F i *
56 55 supxrcld φ i Z sup ran F i * < *
57 56 ad5ant13 φ x i Z j i x F j sup ran F i * < *
58 simpr φ x i Z j i x F j x F j
59 55 3adant3 φ i Z j i ran F i *
60 fvres j i F i j = F j
61 60 eqcomd j i F j = F i j
62 61 3ad2ant3 φ i Z j i F j = F i j
63 3 ffnd φ F Fn Z
64 2 uzssd3 i Z i Z
65 fnssres F Fn Z i Z F i Fn i
66 63 64 65 syl2an φ i Z F i Fn i
67 fnfvelrn F i Fn i j i F i j ran F i
68 66 67 stoic3 φ i Z j i F i j ran F i
69 62 68 eqeltrd φ i Z j i F j ran F i
70 eqid sup ran F i * < = sup ran F i * <
71 59 69 70 supxrubd φ i Z j i F j sup ran F i * <
72 71 ad5ant134 φ x i Z j i x F j F j sup ran F i * <
73 45 50 57 58 72 xrletrd φ x i Z j i x F j x sup ran F i * <
74 73 rexlimdva2 φ x i Z j i x F j x sup ran F i * <
75 74 ralimdva φ x i Z j i x F j i Z x sup ran F i * <
76 75 reximdva φ x i Z j i x F j x i Z x sup ran F i * <
77 43 76 mpd φ x i Z x sup ran F i * <
78 fveq2 n = i n = i
79 78 reseq2d n = i F n = F i
80 79 rneqd n = i ran F n = ran F i
81 80 supeq1d n = i sup ran F n * < = sup ran F i * <
82 eqcom n = i i = n
83 eqcom sup ran F n * < = sup ran F i * < sup ran F i * < = sup ran F n * <
84 81 82 83 3imtr3i i = n sup ran F i * < = sup ran F n * <
85 84 breq2d i = n x sup ran F i * < x sup ran F n * <
86 85 cbvralvw i Z x sup ran F i * < n Z x sup ran F n * <
87 86 rexbii x i Z x sup ran F i * < x n Z x sup ran F n * <
88 77 87 sylib φ x n Z x sup ran F n * <
89 36 33 rnmptbd2 φ x n Z x sup ran F n * < x y ran n Z sup ran F n * < x y
90 88 89 mpbid φ x y ran n Z sup ran F n * < x y
91 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 inf ran n Z sup ran F n * < * < = inf ran n Z sup ran F n * < <
92 35 39 90 91 syl3anc φ inf ran n Z sup ran F n * < * < = inf ran n Z sup ran F n * < <
93 fveq2 n = k n = k
94 93 reseq2d n = k F n = F k
95 94 rneqd n = k ran F n = ran F k
96 95 supeq1d n = k sup ran F n * < = sup ran F k * <
97 96 cbvmptv n Z sup ran F n * < = k Z sup ran F k * <
98 97 rneqi ran n Z sup ran F n * < = ran k Z sup ran F k * <
99 98 infeq1i inf ran n Z sup ran F n * < < = inf ran k Z sup ran F k * < <
100 99 a1i φ inf ran n Z sup ran F n * < < = inf ran k Z sup ran F k * < <
101 6 92 100 3eqtrd φ lim sup F = inf ran k Z sup ran F k * < <