Metamath Proof Explorer

Theorem xlimmnfvlem2

Description: Lemma for xlimmnf : the "if" part of the biconditional. (Contributed by Glauco Siliprandi, 5-Feb-2022)

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

Proof

Step Hyp Ref Expression
1 xlimmnfvlem2.k 
 |-  F/ k ph
2 xlimmnfvlem2.j 
 |-  F/ j ph
3 xlimmnfvlem2.m 
 |-  ( ph -> M e. ZZ )
4 xlimmnfvlem2.z 
 |-  Z = ( ZZ>= ` M )
5 xlimmnfvlem2.f 
 |-  ( ph -> F : Z --> RR* )
6 xlimmnfvlem2.g 
 |-  ( ph -> A. x e. RR E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) < x )
7 letopon 
 |-  ( ordTop ` <_ ) e. ( TopOn ` RR* )
8 7 a1i 
 |-  ( ph -> ( ordTop ` <_ ) e. ( TopOn ` RR* ) )
9 8 elfvexd 
 |-  ( ph -> RR* e. _V )
10 cnex 
 |-  CC e. _V
11 10 a1i 
 |-  ( ph -> CC e. _V )
12 4 uzsscn2 
 |-  Z C_ CC
13 12 a1i 
 |-  ( ph -> Z C_ CC )
14 elpm2r 
 |-  ( ( ( RR* e. _V /\ CC e. _V ) /\ ( F : Z --> RR* /\ Z C_ CC ) ) -> F e. ( RR* ^pm CC ) )
15 9 11 5 13 14 syl22anc 
 |-  ( ph -> F e. ( RR* ^pm CC ) )
16 mnfxr 
 |-  -oo e. RR*
17 16 a1i 
 |-  ( ph -> -oo e. RR* )
18 mnfnei 
 |-  ( ( u e. ( ordTop ` <_ ) /\ -oo e. u ) -> E. x e. RR ( -oo [,) x ) C_ u )
19 18 adantll 
 |-  ( ( ( ph /\ u e. ( ordTop ` <_ ) ) /\ -oo e. u ) -> E. x e. RR ( -oo [,) x ) C_ u )
20 nfv 
 |-  F/ j x e. RR
21 2 20 nfan 
 |-  F/ j ( ph /\ x e. RR )
22 nfv 
 |-  F/ j ( -oo [,) x ) C_ u
23 21 22 nfan 
 |-  F/ j ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u )
24 simprr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) < x ) ) -> A. k e. ( ZZ>= ` j ) ( F ` k ) < x )
25 nfv 
 |-  F/ k x e. RR
26 1 25 nfan 
 |-  F/ k ( ph /\ x e. RR )
27 nfv 
 |-  F/ k ( -oo [,) x ) C_ u
28 26 27 nfan 
 |-  F/ k ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u )
29 nfv 
 |-  F/ k j e. Z
30 28 29 nfan 
 |-  F/ k ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z )
31 4 uztrn2 
 |-  ( ( j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
32 31 3adant1 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. Z )
33 5 fdmd 
 |-  ( ph -> dom F = Z )
34 33 3ad2ant1 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> dom F = Z )
35 32 34 eleqtrrd 
 |-  ( ( ph /\ j e. Z /\ k e. ( ZZ>= ` j ) ) -> k e. dom F )
36 35 ad5ant134 
 |-  ( ( ( ( ( ph /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> k e. dom F )
37 36 adantl4r 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> k e. dom F )
38 simp-4r 
 |-  ( ( ( ( ( ph /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ( -oo [,) x ) C_ u )
39 38 adantl4r 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ( -oo [,) x ) C_ u )
40 16 a1i 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> -oo e. RR* )
41 simp-4r 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> x e. RR )
42 rexr 
 |-  ( x e. RR -> x e. RR* )
43 41 42 syl 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> x e. RR* )
44 simp-4l 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ph )
45 31 ad4ant23 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> k e. Z )
46 5 ffvelcdmda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR* )
47 44 45 46 syl2anc 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ( F ` k ) e. RR* )
48 47 mnfled 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> -oo <_ ( F ` k ) )
49 simpr 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ( F ` k ) < x )
50 40 43 47 48 49 elicod 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ( F ` k ) e. ( -oo [,) x ) )
51 50 adantl3r 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ( F ` k ) e. ( -oo [,) x ) )
52 39 51 sseldd 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ( F ` k ) e. u )
53 37 52 jca 
 |-  ( ( ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) /\ ( F ` k ) < x ) -> ( k e. dom F /\ ( F ` k ) e. u ) )
54 53 ex 
 |-  ( ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) /\ k e. ( ZZ>= ` j ) ) -> ( ( F ` k ) < x -> ( k e. dom F /\ ( F ` k ) e. u ) ) )
55 30 54 ralimdaa 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z ) -> ( A. k e. ( ZZ>= ` j ) ( F ` k ) < x -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
56 55 adantrr 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) < x ) ) -> ( A. k e. ( ZZ>= ` j ) ( F ` k ) < x -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
57 24 56 mpd 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ ( j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) < x ) ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
58 57 3impb 
 |-  ( ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) /\ j e. Z /\ A. k e. ( ZZ>= ` j ) ( F ` k ) < x ) -> A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
59 6 r19.21bi 
 |-  ( ( ph /\ x e. RR ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) < x )
60 59 adantr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( F ` k ) < x )
61 23 58 60 reximdd 
 |-  ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) -> E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
62 4 rexuz3 
 |-  ( M e. ZZ -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
63 3 62 syl 
 |-  ( ph -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
64 63 ad2antrr 
 |-  ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) -> ( E. j e. Z A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) <-> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
65 61 64 mpbid 
 |-  ( ( ( ph /\ x e. RR ) /\ ( -oo [,) x ) C_ u ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
66 65 rexlimdva2 
 |-  ( ph -> ( E. x e. RR ( -oo [,) x ) C_ u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
67 66 ad2antrr 
 |-  ( ( ( ph /\ u e. ( ordTop ` <_ ) ) /\ -oo e. u ) -> ( E. x e. RR ( -oo [,) x ) C_ u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
68 19 67 mpd 
 |-  ( ( ( ph /\ u e. ( ordTop ` <_ ) ) /\ -oo e. u ) -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) )
69 68 ex 
 |-  ( ( ph /\ u e. ( ordTop ` <_ ) ) -> ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
70 69 ralrimiva 
 |-  ( ph -> A. u e. ( ordTop ` <_ ) ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) )
71 15 17 70 3jca 
 |-  ( ph -> ( F e. ( RR* ^pm CC ) /\ -oo e. RR* /\ A. u e. ( ordTop ` <_ ) ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) )
72 nfcv 
 |-  F/_ k F
73 72 8 lmbr3 
 |-  ( ph -> ( F ( ~~>t ` ( ordTop ` <_ ) ) -oo <-> ( F e. ( RR* ^pm CC ) /\ -oo e. RR* /\ A. u e. ( ordTop ` <_ ) ( -oo e. u -> E. j e. ZZ A. k e. ( ZZ>= ` j ) ( k e. dom F /\ ( F ` k ) e. u ) ) ) ) )
74 71 73 mpbird 
 |-  ( ph -> F ( ~~>t ` ( ordTop ` <_ ) ) -oo )
75 df-xlim 
 |-  ~~>* = ( ~~>t ` ( ordTop ` <_ ) )
76 75 breqi 
 |-  ( F ~~>* -oo <-> F ( ~~>t ` ( ordTop ` <_ ) ) -oo )
77 76 a1i 
 |-  ( ph -> ( F ~~>* -oo <-> F ( ~~>t ` ( ordTop ` <_ ) ) -oo ) )
78 74 77 mpbird 
 |-  ( ph -> F ~~>* -oo )