Metamath Proof Explorer

Theorem xlimmnfv

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