Metamath Proof Explorer

Theorem xlimpnfxnegmnf2

Description: A sequence converges to +oo if and only if its negation converges to -oo . (Contributed by Glauco Siliprandi, 23-Apr-2023)

Ref Expression
Hypotheses xlimpnfxnegmnf2.j 
|- F/_ j F
xlimpnfxnegmnf2.m 
|- ( ph -> M e. ZZ )
xlimpnfxnegmnf2.z 
|- Z = ( ZZ>= ` M )
xlimpnfxnegmnf2.f 
|- ( ph -> F : Z --> RR* )
Assertion xlimpnfxnegmnf2 
|- ( ph -> ( F ~~>* +oo <-> ( j e. Z |-> -e ( F ` j ) ) ~~>* -oo ) )

Proof

Step Hyp Ref Expression
1 xlimpnfxnegmnf2.j 
 |-  F/_ j F
2 xlimpnfxnegmnf2.m 
 |-  ( ph -> M e. ZZ )
3 xlimpnfxnegmnf2.z 
 |-  Z = ( ZZ>= ` M )
4 xlimpnfxnegmnf2.f 
 |-  ( ph -> F : Z --> RR* )
5 1 3 4 xlimpnfxnegmnf 
 |-  ( ph -> ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
6 1 2 3 4 xlimpnf 
 |-  ( ph -> ( F ~~>* +oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) ) )
7 nfmpt1 
 |-  F/_ j ( j e. Z |-> -e ( F ` j ) )
8 4 ffvelrnda 
 |-  ( ( ph /\ k e. Z ) -> ( F ` k ) e. RR* )
9 8 xnegcld 
 |-  ( ( ph /\ k e. Z ) -> -e ( F ` k ) e. RR* )
10 nfcv 
 |-  F/_ k -e ( F ` j )
11 nfcv 
 |-  F/_ j k
12 1 11 nffv 
 |-  F/_ j ( F ` k )
13 12 nfxneg 
 |-  F/_ j -e ( F ` k )
14 fveq2 
 |-  ( j = k -> ( F ` j ) = ( F ` k ) )
15 14 xnegeqd 
 |-  ( j = k -> -e ( F ` j ) = -e ( F ` k ) )
16 10 13 15 cbvmpt 
 |-  ( j e. Z |-> -e ( F ` j ) ) = ( k e. Z |-> -e ( F ` k ) )
17 9 16 fmptd 
 |-  ( ph -> ( j e. Z |-> -e ( F ` j ) ) : Z --> RR* )
18 7 2 3 17 xlimmnf 
 |-  ( ph -> ( ( j e. Z |-> -e ( F ` j ) ) ~~>* -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x ) )
19 3 uztrn2 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> j e. Z )
20 xnegex 
 |-  -e ( F ` j ) e. _V
21 fvmpt4 
 |-  ( ( j e. Z /\ -e ( F ` j ) e. _V ) -> ( ( j e. Z |-> -e ( F ` j ) ) ` j ) = -e ( F ` j ) )
22 20 21 mpan2 
 |-  ( j e. Z -> ( ( j e. Z |-> -e ( F ` j ) ) ` j ) = -e ( F ` j ) )
23 22 breq1d 
 |-  ( j e. Z -> ( ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> -e ( F ` j ) <_ x ) )
24 19 23 syl 
 |-  ( ( k e. Z /\ j e. ( ZZ>= ` k ) ) -> ( ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> -e ( F ` j ) <_ x ) )
25 24 ralbidva 
 |-  ( k e. Z -> ( A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
26 25 rexbiia 
 |-  ( E. k e. Z A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
27 26 ralbii 
 |-  ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) ( ( j e. Z |-> -e ( F ` j ) ) ` j ) <_ x <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
28 18 27 bitrdi 
 |-  ( ph -> ( ( j e. Z |-> -e ( F ` j ) ) ~~>* -oo <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
29 5 6 28 3bitr4d 
 |-  ( ph -> ( F ~~>* +oo <-> ( j e. Z |-> -e ( F ` j ) ) ~~>* -oo ) )