Metamath Proof Explorer

Theorem xlimmnf

Description: A function converges to minus infinity if it eventually becomes (and stays) smaller than any given real number. (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses xlimmnf.k 
|- F/_ k F
xlimmnf.m 
|- ( ph -> M e. ZZ )
xlimmnf.z 
|- Z = ( ZZ>= ` M )
xlimmnf.f 
|- ( ph -> F : Z --> RR* )
Assertion xlimmnf 
|- ( ph -> ( F ~~>* -oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )

Proof

Step Hyp Ref Expression
1 xlimmnf.k 
 |-  F/_ k F
2 xlimmnf.m 
 |-  ( ph -> M e. ZZ )
3 xlimmnf.z 
 |-  Z = ( ZZ>= ` M )
4 xlimmnf.f 
 |-  ( ph -> F : Z --> RR* )
5 2 3 4 xlimmnfv 
 |-  ( ph -> ( 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 rexralbidv 
 |-  ( 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 ) )
8 fveq2 
 |-  ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) )
9 8 raleqdv 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` j ) ( F ` l ) <_ x ) )
10 nfcv 
 |-  F/_ k l
11 1 10 nffv 
 |-  F/_ k ( F ` l )
12 nfcv 
 |-  F/_ k <_
13 nfcv 
 |-  F/_ k x
14 11 12 13 nfbr 
 |-  F/ k ( F ` l ) <_ x
15 nfv 
 |-  F/ l ( F ` k ) <_ x
16 fveq2 
 |-  ( l = k -> ( F ` l ) = ( F ` k ) )
17 16 breq1d 
 |-  ( l = k -> ( ( F ` l ) <_ x <-> ( F ` k ) <_ x ) )
18 14 15 17 cbvralw 
 |-  ( A. l e. ( ZZ>= ` j ) ( F ` l ) <_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x )
19 9 18 bitrdi 
 |-  ( i = j -> ( A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )
20 19 cbvrexvw 
 |-  ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ x <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x )
21 7 20 bitrdi 
 |-  ( y = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )
22 21 cbvralvw 
 |-  ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) ( F ` l ) <_ y <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x )
23 5 22 bitrdi 
 |-  ( ph -> ( F ~~>* -oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) <_ x ) )