Metamath Proof Explorer

Theorem xlimpnfv

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 xlimpnfv.m 
|- ( ph -> M e. ZZ )
xlimpnfv.z 
|- Z = ( ZZ>= ` M )
xlimpnfv.f 
|- ( ph -> F : Z --> RR* )
Assertion xlimpnfv 
|- ( 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 xlimpnfv.m 
 |-  ( ph -> M e. ZZ )
2 xlimpnfv.z 
 |-  Z = ( ZZ>= ` M )
3 xlimpnfv.f 
 |-  ( ph -> F : Z --> RR* )
4 1 ad2antrr 
 |-  ( ( ( ph /\ F ~~>* +oo ) /\ x e. RR ) -> M e. ZZ )
5 3 ad2antrr 
 |-  ( ( ( ph /\ F ~~>* +oo ) /\ x e. RR ) -> F : Z --> RR* )
6 simplr 
 |-  ( ( ( ph /\ F ~~>* +oo ) /\ x e. RR ) -> F ~~>* +oo )
7 simpr 
 |-  ( ( ( ph /\ F ~~>* +oo ) /\ x e. RR ) -> x e. RR )
8 4 2 5 6 7 xlimpnfvlem1 
 |-  ( ( ( ph /\ F ~~>* +oo ) /\ x e. RR ) -> E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
9 8 ralrimiva 
 |-  ( ( ph /\ F ~~>* +oo ) -> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
10 nfv 
 |-  F/ k ph
11 nfcv 
 |-  F/_ k RR
12 nfcv 
 |-  F/_ k Z
13 nfra1 
 |-  F/ k A. k e. ( ZZ>= ` j ) x <_ ( F ` k )
14 12 13 nfrex 
 |-  F/ k E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k )
15 11 14 nfralw 
 |-  F/ k A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k )
16 10 15 nfan 
 |-  F/ k ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
17 nfv 
 |-  F/ j ph
18 nfcv 
 |-  F/_ j RR
19 nfre1 
 |-  F/ j E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k )
20 18 19 nfralw 
 |-  F/ j A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k )
21 17 20 nfan 
 |-  F/ j ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
22 1 adantr 
 |-  ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) -> M e. ZZ )
23 3 adantr 
 |-  ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) -> F : Z --> RR* )
24 nfv 
 |-  F/ j y e. RR
25 21 24 nfan 
 |-  F/ j ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) /\ y e. RR )
26 simp-4r 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( y + 1 ) <_ ( F ` k ) ) -> y e. RR )
27 rexr 
 |-  ( y e. RR -> y e. RR* )
28 26 27 syl 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( y + 1 ) <_ ( F ` k ) ) -> y e. RR* )
29 peano2re 
 |-  ( y e. RR -> ( y + 1 ) e. RR )
30 29 rexrd 
 |-  ( y e. RR -> ( y + 1 ) e. RR* )
31 26 30 syl 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( y + 1 ) <_ ( F ` k ) ) -> ( y + 1 ) e. RR* )
32 3 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> F : Z --> RR* )
33 2 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
34 33 3adant1 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
35 32 34 ffvelrnd 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> ( F ` k ) e. RR* )
36 35 ad5ant134 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( y + 1 ) <_ ( F ` k ) ) -> ( F ` k ) e. RR* )
37 26 ltp1d 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( y + 1 ) <_ ( F ` k ) ) -> y < ( y + 1 ) )
38 simpr 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( y + 1 ) <_ ( F ` k ) ) -> ( y + 1 ) <_ ( F ` k ) )
39 28 31 36 37 38 xrltletrd 
 |-  ( ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( y + 1 ) <_ ( F ` k ) ) -> y < ( F ` k ) )
40 39 ex 
 |-  ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( y + 1 ) <_ ( F ` k ) -> y < ( F ` k ) ) )
41 40 ralimdva 
 |-  ( ( ( ph /\ y e. RR ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) -> A. k e. ( ZZ>= ` j ) y < ( F ` k ) ) )
42 41 imp 
 |-  ( ( ( ( ph /\ y e. RR ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) ) -> A. k e. ( ZZ>= ` j ) y < ( F ` k ) )
43 42 adantl3r 
 |-  ( ( ( ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) /\ y e. RR ) /\ j e. Z ) /\ A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) ) -> A. k e. ( ZZ>= ` j ) y < ( F ` k ) )
44 43 3impa 
 |-  ( ( ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) /\ y e. RR ) /\ j e. Z /\ A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) ) -> A. k e. ( ZZ>= ` j ) y < ( F ` k ) )
45 29 adantl 
 |-  ( ( A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) /\ y e. RR ) -> ( y + 1 ) e. RR )
46 simpl 
 |-  ( ( A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) /\ y e. RR ) -> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) )
47 breq1 
 |-  ( x = ( y + 1 ) -> ( x <_ ( F ` k ) <-> ( y + 1 ) <_ ( F ` k ) ) )
48 47 ralbidv 
 |-  ( x = ( y + 1 ) -> ( A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) <-> A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) ) )
49 48 rexbidv 
 |-  ( x = ( y + 1 ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) <-> E. j e. Z A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) ) )
50 49 rspcva 
 |-  ( ( ( y + 1 ) e. RR /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) )
51 45 46 50 syl2anc 
 |-  ( ( A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) /\ y e. RR ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) )
52 51 adantll 
 |-  ( ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) /\ y e. RR ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( y + 1 ) <_ ( F ` k ) )
53 25 44 52 reximdd 
 |-  ( ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) /\ y e. RR ) -> E. j e. Z A. k e. ( ZZ>= ` j ) y < ( F ` k ) )
54 53 ralrimiva 
 |-  ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) -> A. y e. RR E. j e. Z A. k e. ( ZZ>= ` j ) y < ( F ` k ) )
55 16 21 22 2 23 54 xlimpnfvlem2 
 |-  ( ( ph /\ A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) -> F ~~>* +oo )
56 9 55 impbida 
 |-  ( ph -> ( F ~~>* +oo <-> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) x <_ ( F ` k ) ) )