Metamath Proof Explorer

Theorem xlimpnfmpt

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

Proof

Step Hyp Ref Expression
1 xlimpnfmpt.k 
 |-  F/ k ph
2 xlimpnfmpt.m 
 |-  ( ph -> M e. ZZ )
3 xlimpnfmpt.z 
 |-  Z = ( ZZ>= ` M )
4 xlimpnfmpt.b 
 |-  ( ( ph /\ k e. Z ) -> B e. RR* )
5 xlimpnfmpt.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 xlimpnf 
 |-  ( ph -> ( F ~~>* +oo <-> A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) y <_ ( F ` k ) ) )
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 breq2d 
 |-  ( ( ( ph /\ i e. Z ) /\ k e. ( ZZ>= ` i ) ) -> ( y <_ ( F ` k ) <-> y <_ B ) )
19 11 18 ralbida 
 |-  ( ( ph /\ i e. Z ) -> ( A. k e. ( ZZ>= ` i ) y <_ ( F ` k ) <-> A. k e. ( ZZ>= ` i ) y <_ B ) )
20 19 rexbidva 
 |-  ( ph -> ( E. i e. Z A. k e. ( ZZ>= ` i ) y <_ ( F ` k ) <-> E. i e. Z A. k e. ( ZZ>= ` i ) y <_ B ) )
21 20 ralbidv 
 |-  ( ph -> ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) y <_ ( F ` k ) <-> A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) y <_ B ) )
22 breq1 
 |-  ( y = x -> ( y <_ B <-> x <_ B ) )
23 22 rexralbidv 
 |-  ( y = x -> ( E. i e. Z A. k e. ( ZZ>= ` i ) y <_ B <-> E. i e. Z A. k e. ( ZZ>= ` i ) x <_ B ) )
24 fveq2 
 |-  ( i = j -> ( ZZ>= ` i ) = ( ZZ>= ` j ) )
25 24 raleqdv 
 |-  ( i = j -> ( A. k e. ( ZZ>= ` i ) x <_ B <-> A. k e. ( ZZ>= ` j ) x <_ B ) )
26 25 cbvrexvw 
 |-  ( E. i e. Z A. k e. ( ZZ>= ` i ) x <_ B <-> E. j e. Z A. k e. ( ZZ>= ` j ) x <_ B )
27 23 26 bitrdi 
 |-  ( y = x -> ( E. i e. Z A. k e. ( ZZ>= ` i ) y <_ B <-> E. j e. Z A. k e. ( ZZ>= ` j ) x <_ B ) )
28 27 cbvralvw 
 |-  ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) y <_ B <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ B )
29 28 a1i 
 |-  ( ph -> ( A. y e. RR E. i e. Z A. k e. ( ZZ>= ` i ) y <_ B <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ B ) )
30 9 21 29 3bitrd 
 |-  ( ph -> ( F ~~>* +oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ B ) )