Metamath Proof Explorer

Theorem limsupmnfuzlem

Description: The superior limit of a function is -oo if and only if every real number is the upper bound of the restriction of the function to a set of upper integers. (Contributed by Glauco Siliprandi, 23-Oct-2021)

Ref Expression
Hypotheses limsupmnfuzlem.1 
|- ( ph -> M e. ZZ )
limsupmnfuzlem.2 
|- Z = ( ZZ>= ` M )
limsupmnfuzlem.3 
|- ( ph -> F : Z --> RR* )
Assertion limsupmnfuzlem 
|- ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )

Proof

Step Hyp Ref Expression
1 limsupmnfuzlem.1 
 |-  ( ph -> M e. ZZ )
2 limsupmnfuzlem.2 
 |-  Z = ( ZZ>= ` M )
3 limsupmnfuzlem.3 
 |-  ( ph -> F : Z --> RR* )
4 nfcv 
 |-  F/_ j F
5 uzssre 
 |-  ( ZZ>= ` M ) C_ RR
6 2 5 eqsstri 
 |-  Z C_ RR
7 6 a1i 
 |-  ( ph -> Z C_ RR )
8 4 7 3 limsupmnf 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) ) )
9 breq1 
 |-  ( k = i -> ( k <_ j <-> i <_ j ) )
10 9 imbi1d 
 |-  ( k = i -> ( ( k <_ j -> ( F ` j ) <_ x ) <-> ( i <_ j -> ( F ` j ) <_ x ) ) )
11 10 ralbidv 
 |-  ( k = i -> ( A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) <-> A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) )
12 11 cbvrexvw 
 |-  ( E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) <-> E. i e. RR A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) )
13 12 biimpi 
 |-  ( E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) -> E. i e. RR A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) )
14 iftrue 
 |-  ( M <_ ( |^ ` i ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) = ( |^ ` i ) )
15 14 adantl 
 |-  ( ( ( ph /\ i e. RR ) /\ M <_ ( |^ ` i ) ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) = ( |^ ` i ) )
16 1 ad2antrr 
 |-  ( ( ( ph /\ i e. RR ) /\ M <_ ( |^ ` i ) ) -> M e. ZZ )
17 ceilcl 
 |-  ( i e. RR -> ( |^ ` i ) e. ZZ )
18 17 ad2antlr 
 |-  ( ( ( ph /\ i e. RR ) /\ M <_ ( |^ ` i ) ) -> ( |^ ` i ) e. ZZ )
19 simpr 
 |-  ( ( ( ph /\ i e. RR ) /\ M <_ ( |^ ` i ) ) -> M <_ ( |^ ` i ) )
20 2 16 18 19 eluzd 
 |-  ( ( ( ph /\ i e. RR ) /\ M <_ ( |^ ` i ) ) -> ( |^ ` i ) e. Z )
21 15 20 eqeltrd 
 |-  ( ( ( ph /\ i e. RR ) /\ M <_ ( |^ ` i ) ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) e. Z )
22 iffalse 
 |-  ( -. M <_ ( |^ ` i ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) = M )
23 22 adantl 
 |-  ( ( ( ph /\ i e. RR ) /\ -. M <_ ( |^ ` i ) ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) = M )
24 1 2 uzidd2 
 |-  ( ph -> M e. Z )
25 24 ad2antrr 
 |-  ( ( ( ph /\ i e. RR ) /\ -. M <_ ( |^ ` i ) ) -> M e. Z )
26 23 25 eqeltrd 
 |-  ( ( ( ph /\ i e. RR ) /\ -. M <_ ( |^ ` i ) ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) e. Z )
27 21 26 pm2.61dan 
 |-  ( ( ph /\ i e. RR ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) e. Z )
28 27 3adant3 
 |-  ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) e. Z )
29 nfv 
 |-  F/ j ph
30 nfv 
 |-  F/ j i e. RR
31 nfra1 
 |-  F/ j A. j e. Z ( i <_ j -> ( F ` j ) <_ x )
32 29 30 31 nf3an 
 |-  F/ j ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) )
33 simplr 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> i e. RR )
34 6 27 sselid 
 |-  ( ( ph /\ i e. RR ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) e. RR )
35 34 adantr 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) e. RR )
36 eluzelre 
 |-  ( j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) -> j e. RR )
37 36 adantl 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> j e. RR )
38 simpr 
 |-  ( ( ph /\ i e. RR ) -> i e. RR )
39 17 zred 
 |-  ( i e. RR -> ( |^ ` i ) e. RR )
40 39 adantl 
 |-  ( ( ph /\ i e. RR ) -> ( |^ ` i ) e. RR )
41 ceilge 
 |-  ( i e. RR -> i <_ ( |^ ` i ) )
42 41 adantl 
 |-  ( ( ph /\ i e. RR ) -> i <_ ( |^ ` i ) )
43 6 24 sselid 
 |-  ( ph -> M e. RR )
44 43 adantr 
 |-  ( ( ph /\ i e. RR ) -> M e. RR )
45 max2 
 |-  ( ( M e. RR /\ ( |^ ` i ) e. RR ) -> ( |^ ` i ) <_ if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) )
46 44 40 45 syl2anc 
 |-  ( ( ph /\ i e. RR ) -> ( |^ ` i ) <_ if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) )
47 38 40 34 42 46 letrd 
 |-  ( ( ph /\ i e. RR ) -> i <_ if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) )
48 47 adantr 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> i <_ if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) )
49 eluzle 
 |-  ( j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) <_ j )
50 49 adantl 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) <_ j )
51 33 35 37 48 50 letrd 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> i <_ j )
52 51 3adantl3 
 |-  ( ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> i <_ j )
53 simpl3 
 |-  ( ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) )
54 1 ad2antrr 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> M e. ZZ )
55 eluzelz 
 |-  ( j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) -> j e. ZZ )
56 55 adantl 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> j e. ZZ )
57 44 adantr 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> M e. RR )
58 max1 
 |-  ( ( M e. RR /\ ( |^ ` i ) e. RR ) -> M <_ if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) )
59 43 39 58 syl2an 
 |-  ( ( ph /\ i e. RR ) -> M <_ if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) )
60 59 adantr 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> M <_ if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) )
61 57 35 37 60 50 letrd 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> M <_ j )
62 2 54 56 61 eluzd 
 |-  ( ( ( ph /\ i e. RR ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> j e. Z )
63 62 3adantl3 
 |-  ( ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> j e. Z )
64 rspa 
 |-  ( ( A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) /\ j e. Z ) -> ( i <_ j -> ( F ` j ) <_ x ) )
65 53 63 64 syl2anc 
 |-  ( ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> ( i <_ j -> ( F ` j ) <_ x ) )
66 52 65 mpd 
 |-  ( ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) /\ j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ) -> ( F ` j ) <_ x )
67 66 ex 
 |-  ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) -> ( j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) -> ( F ` j ) <_ x ) )
68 32 67 ralrimi 
 |-  ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) -> A. j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ( F ` j ) <_ x )
69 fveq2 
 |-  ( k = if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) -> ( ZZ>= ` k ) = ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) )
70 69 raleqdv 
 |-  ( k = if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) -> ( A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> A. j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ( F ` j ) <_ x ) )
71 70 rspcev 
 |-  ( ( if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) e. Z /\ A. j e. ( ZZ>= ` if ( M <_ ( |^ ` i ) , ( |^ ` i ) , M ) ) ( F ` j ) <_ x ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
72 28 68 71 syl2anc 
 |-  ( ( ph /\ i e. RR /\ A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
73 72 3exp 
 |-  ( ph -> ( i e. RR -> ( A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )
74 73 rexlimdv 
 |-  ( ph -> ( E. i e. RR A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
75 74 imp 
 |-  ( ( ph /\ E. i e. RR A. j e. Z ( i <_ j -> ( F ` j ) <_ x ) ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
76 13 75 sylan2 
 |-  ( ( ph /\ E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
77 76 ex 
 |-  ( ph -> ( E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) -> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
78 rexss 
 |-  ( Z C_ RR -> ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> E. k e. RR ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) )
79 6 78 ax-mp 
 |-  ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x <-> E. k e. RR ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
80 79 biimpi 
 |-  ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x -> E. k e. RR ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
81 nfv 
 |-  F/ j k e. Z
82 nfra1 
 |-  F/ j A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x
83 81 82 nfan 
 |-  F/ j ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
84 simp1r 
 |-  ( ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) /\ j e. Z /\ k <_ j ) -> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
85 eqid 
 |-  ( ZZ>= ` k ) = ( ZZ>= ` k )
86 2 eluzelz2 
 |-  ( k e. Z -> k e. ZZ )
87 86 3ad2ant1 
 |-  ( ( k e. Z /\ j e. Z /\ k <_ j ) -> k e. ZZ )
88 2 eluzelz2 
 |-  ( j e. Z -> j e. ZZ )
89 88 3ad2ant2 
 |-  ( ( k e. Z /\ j e. Z /\ k <_ j ) -> j e. ZZ )
90 simp3 
 |-  ( ( k e. Z /\ j e. Z /\ k <_ j ) -> k <_ j )
91 85 87 89 90 eluzd 
 |-  ( ( k e. Z /\ j e. Z /\ k <_ j ) -> j e. ( ZZ>= ` k ) )
92 91 3adant1r 
 |-  ( ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) /\ j e. Z /\ k <_ j ) -> j e. ( ZZ>= ` k ) )
93 rspa 
 |-  ( ( A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x /\ j e. ( ZZ>= ` k ) ) -> ( F ` j ) <_ x )
94 84 92 93 syl2anc 
 |-  ( ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) /\ j e. Z /\ k <_ j ) -> ( F ` j ) <_ x )
95 94 3exp 
 |-  ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> ( j e. Z -> ( k <_ j -> ( F ` j ) <_ x ) ) )
96 83 95 ralrimi 
 |-  ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) )
97 96 a1i 
 |-  ( ph -> ( ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) ) )
98 97 reximdv 
 |-  ( ph -> ( E. k e. RR ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) ) )
99 98 imp 
 |-  ( ( ph /\ E. k e. RR ( k e. Z /\ A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) ) -> E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) )
100 80 99 sylan2 
 |-  ( ( ph /\ E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) -> E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) )
101 100 ex 
 |-  ( ph -> ( E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x -> E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) ) )
102 77 101 impbid 
 |-  ( ph -> ( E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
103 102 ralbidv 
 |-  ( ph -> ( A. x e. RR E. k e. RR A. j e. Z ( k <_ j -> ( F ` j ) <_ x ) <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
104 8 103 bitrd 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )