Metamath Proof Explorer

Theorem xlimpnf

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

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

Proof

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