Metamath Proof Explorer

Theorem xlimmnfmpt

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 xlimmnfmpt.k 
|- F/ k ph
xlimmnfmpt.m 
|- ( ph -> M e. ZZ )
xlimmnfmpt.z 
|- Z = ( ZZ>= ` M )
xlimmnfmpt.b 
|- ( ( ph /\ k e. Z ) -> B e. RR* )
xlimmnfmpt.f 
|- F = ( k e. Z |-> B )
Assertion xlimmnfmpt 
|- ( ph -> ( F ~~>* -oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) )

Proof

Step Hyp Ref Expression
1 xlimmnfmpt.k 
 |-  F/ k ph
2 xlimmnfmpt.m 
 |-  ( ph -> M e. ZZ )
3 xlimmnfmpt.z 
 |-  Z = ( ZZ>= ` M )
4 xlimmnfmpt.b 
 |-  ( ( ph /\ k e. Z ) -> B e. RR* )
5 xlimmnfmpt.f 
 |-  F = ( k e. Z |-> B )
6 nfmpt1 
 |-  F/_ k ( k e. Z |-> B )
7 5 6 nfcxfr 
 |-  F/_ k F
8 1 4 5 fmptdf 
 |-  ( ph -> F : Z --> RR* )
9 7 2 3 8 xlimmnf 
 |-  ( ph -> ( F ~~>* -oo <-> A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) ( F ` k ) <_ y ) )
10 nfv 
 |-  F/ k i e. Z
11 1 10 nfan 
 |-  F/ k ( ph /\ i e. Z )
12 3 uztrn2 
 |-  ( ( i e. Z /\ k e. ( ZZ>= ` i ) ) -> k e. Z )
13 12 adantll 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> k e. Z )
14 simpll 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ph )
15 14 13 4 syl2anc 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> B e. RR* )
16 5 fvmpt2 
 |-  ( ( k e. Z /\ B e. RR* ) -> ( F ` k ) = B )
17 13 15 16 syl2anc 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( F ` k ) = B )
18 17 breq1d 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( ( F ` k ) <_ y <-> B <_ y ) )
19 11 18 ralbida 
 |-  ( ( ph /\ i e. Z ) -> ( A. k e. ( ZZ>= ` i ) ( F ` k ) <_ y <-> A. k e. ( ZZ>= ` i ) B <_ y ) )
20 19 rexbidva 
 |-  ( ph -> ( E. i e. Z A. k e. ( ZZ>= ` i ) ( F ` k ) <_ y <-> E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y ) )
21 20 ralbidv 
 |-  ( ph -> ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) ( F ` k ) <_ y <-> A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y ) )
22 breq2 
 |-  ( y = x -> ( B <_ y <-> B <_ x ) )
23 22 rexralbidv 
 |-  ( y = x -> ( E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y <-> E. i e. Z A. k e. ( ZZ>= ` i ) B <_ x ) )
24 fveq2 
 |-  ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) )
25 24 raleqdv 
 |-  ( i = j -> ( A. k e. ( ZZ>= ` i ) B <_ x <-> A. k e. ( ZZ>= ` j ) B <_ x ) )
26 25 cbvrexvw 
 |-  ( E. i e. Z A. k e. ( ZZ>= ` i ) B <_ x <-> E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x )
27 23 26 bitrdi 
 |-  ( y = x -> ( E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y <-> E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) )
28 27 cbvralvw 
 |-  ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x )
29 28 a1i 
 |-  ( ph -> ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) B <_ y <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) )
30 9 21 29 3bitrd 
 |-  ( ph -> ( F ~~>* -oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) B <_ x ) )