This is an inofficial mirror of http://metamath.tirix.org for personal testing of a visualizer extension only.

Metamath Proof Explorer

Theorem limsupmnfuz

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 limsupmnfuz.1 
|- F/_ j F
limsupmnfuz.2 
|- ( ph -> M e. ZZ )
limsupmnfuz.3 
|- Z = ( ZZ>= ` M )
limsupmnfuz.4 
|- ( ph -> F : Z --> RR* )
Assertion limsupmnfuz 
|- ( 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 limsupmnfuz.1 
 |-  F/_ j F
2 limsupmnfuz.2 
 |-  ( ph -> M e. ZZ )
3 limsupmnfuz.3 
 |-  Z = ( ZZ>= ` M )
4 limsupmnfuz.4 
 |-  ( ph -> F : Z --> RR* )
5 2 3 4 limsupmnfuzlem 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y ) )
6 breq2 
 |-  ( y = x -> ( ( F ` l ) <_ y <-> ( F ` l ) <_ x ) )
7 6 ralbidv 
 |-  ( y = x -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x ) )
8 7 rexbidv 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x ) )
9 fveq2 
 |-  ( i = k -> ( ZZ>= ` i ) = ( ZZ>= ` k ) )
10 9 raleqdv 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x ) )
11 nfcv 
 |-  F/_ j l
12 1 11 nffv 
 |-  F/_ j ( F ` l )
13 nfcv 
 |-  F/_ j <_
14 nfcv 
 |-  F/_ j x
15 12 13 14 nfbr 
 |-  F/ j ( F ` l ) <_ x
16 nfv 
 |-  F/ l ( F ` j ) <_ x
17 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
18 17 breq1d 
 |-  ( l = j -> ( ( F ` l ) <_ x <-> ( F ` j ) <_ x ) )
19 15 16 18 cbvralw 
 |-  ( A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
20 19 a1i 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` k ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
21 10 20 bitrd 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
22 21 cbvrexvw 
 |-  ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
23 22 a1i 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
24 8 23 bitrd 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
25 24 cbvralvw 
 |-  ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x )
26 25 a1i 
 |-  ( ph -> ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )
27 5 26 bitrd 
 |-  ( ph -> ( ( limsup ` F ) = -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( F ` j ) <_ x ) )