Metamath Proof Explorer

Theorem xlimpnfxnegmnf

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 xlimpnfxnegmnf.1 
|- F/_ j F
xlimpnfxnegmnf.2 
|- Z = ( ZZ>= ` M )
xlimpnfxnegmnf.3 
|- ( ph -> F : Z --> RR* )
Assertion 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 ) )

Proof

Step Hyp Ref Expression
1 xlimpnfxnegmnf.1 
 |-  F/_ j F
2 xlimpnfxnegmnf.2 
 |-  Z = ( ZZ>= ` M )
3 xlimpnfxnegmnf.3 
 |-  ( ph -> F : Z --> RR* )
4 breq1 
 |-  ( x = y -> ( x <_ ( F ` j ) <-> y <_ ( F ` j ) ) )
5 4 rexralbidv 
 |-  ( x = y -> ( E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> E. k e. Z A. j e. ( ZZ>= ` k ) y <_ ( F ` j ) ) )
6 fveq2 
 |-  ( k = i -> ( ZZ>= ` k ) = ( ZZ>= ` i ) )
7 6 raleqdv 
 |-  ( k = i -> ( A. j e. ( ZZ>= ` k ) y <_ ( F ` j ) <-> A. j e. ( ZZ>= ` i ) y <_ ( F ` j ) ) )
8 nfv 
 |-  F/ l y <_ ( F ` j )
9 nfcv 
 |-  F/_ j y
10 nfcv 
 |-  F/_ j <_
11 nfcv 
 |-  F/_ j l
12 1 11 nffv 
 |-  F/_ j ( F ` l )
13 9 10 12 nfbr 
 |-  F/ j y <_ ( F ` l )
14 fveq2 
 |-  ( j = l -> ( F ` j ) = ( F ` l ) )
15 14 breq2d 
 |-  ( j = l -> ( y <_ ( F ` j ) <-> y <_ ( F ` l ) ) )
16 8 13 15 cbvralw 
 |-  ( A. j e. ( ZZ>= ` i ) y <_ ( F ` j ) <-> A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
17 7 16 bitrdi 
 |-  ( k = i -> ( A. j e. ( ZZ>= ` k ) y <_ ( F ` j ) <-> A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
18 17 cbvrexvw 
 |-  ( E. k e. Z A. j e. ( ZZ>= ` k ) y <_ ( F ` j ) <-> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
19 5 18 bitrdi 
 |-  ( x = y -> ( E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
20 19 cbvralvw 
 |-  ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
21 20 a1i 
 |-  ( ph -> ( A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) x <_ ( F ` j ) <-> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
22 simpll 
 |-  ( ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) /\ w e. RR ) -> ph )
23 simpr 
 |-  ( ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) /\ w e. RR ) -> w e. RR )
24 xnegrecl 
 |-  ( w e. RR -> -e w e. RR )
25 simpl 
 |-  ( ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ w e. RR ) -> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
26 breq1 
 |-  ( y = -e w -> ( y <_ ( F ` l ) <-> -e w <_ ( F ` l ) ) )
27 26 rexralbidv 
 |-  ( y = -e w -> ( E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) ) )
28 27 rspcva 
 |-  ( ( -e w e. RR /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) )
29 24 25 28 syl2an2 
 |-  ( ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) /\ w e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) )
30 29 adantll 
 |-  ( ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) /\ w e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) )
31 simpll 
 |-  ( ( ( ( ph /\ w e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> ( ph /\ w e. RR ) )
32 2 uztrn2 
 |-  ( ( i e. Z /\ l e. ( ZZ>= ` i ) ) -> l e. Z )
33 32 adantll 
 |-  ( ( ( ( ph /\ w e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> l e. Z )
34 rexr 
 |-  ( w e. RR -> w e. RR* )
35 34 ad2antlr 
 |-  ( ( ( ph /\ w e. RR ) /\ l e. Z ) -> w e. RR* )
36 3 ffvelrnda 
 |-  ( ( ph /\ l e. Z ) -> ( F ` l ) e. RR* )
37 36 adantlr 
 |-  ( ( ( ph /\ w e. RR ) /\ l e. Z ) -> ( F ` l ) e. RR* )
38 xlenegcon1 
 |-  ( ( w e. RR* /\ ( F ` l ) e. RR* ) -> ( -e w <_ ( F ` l ) <-> -e ( F ` l ) <_ w ) )
39 35 37 38 syl2anc 
 |-  ( ( ( ph /\ w e. RR ) /\ l e. Z ) -> ( -e w <_ ( F ` l ) <-> -e ( F ` l ) <_ w ) )
40 39 biimpd 
 |-  ( ( ( ph /\ w e. RR ) /\ l e. Z ) -> ( -e w <_ ( F ` l ) -> -e ( F ` l ) <_ w ) )
41 31 33 40 syl2anc 
 |-  ( ( ( ( ph /\ w e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> ( -e w <_ ( F ` l ) -> -e ( F ` l ) <_ w ) )
42 41 ralimdva 
 |-  ( ( ( ph /\ w e. RR ) /\ i e. Z ) -> ( A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) -> A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) )
43 42 reximdva 
 |-  ( ( ph /\ w e. RR ) -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) )
44 43 imp 
 |-  ( ( ( ph /\ w e. RR ) /\ E. i e. Z A. l e. ( ZZ>= ` i ) -e w <_ ( F ` l ) ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w )
45 22 23 30 44 syl21anc 
 |-  ( ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) /\ w e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w )
46 45 ralrimiva 
 |-  ( ( ph /\ A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) -> A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w )
47 simpll 
 |-  ( ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) /\ y e. RR ) -> ph )
48 simpr 
 |-  ( ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) /\ y e. RR ) -> y e. RR )
49 xnegrecl 
 |-  ( y e. RR -> -e y e. RR )
50 simpl 
 |-  ( ( A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w /\ y e. RR ) -> A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w )
51 breq2 
 |-  ( w = -e y -> ( -e ( F ` l ) <_ w <-> -e ( F ` l ) <_ -e y ) )
52 51 rexralbidv 
 |-  ( w = -e y -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y ) )
53 52 rspcva 
 |-  ( ( -e y e. RR /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y )
54 49 50 53 syl2an2 
 |-  ( ( A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w /\ y e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y )
55 54 adantll 
 |-  ( ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) /\ y e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y )
56 simpll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> ( ph /\ y e. RR ) )
57 32 adantll 
 |-  ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> l e. Z )
58 rexr 
 |-  ( y e. RR -> y e. RR* )
59 58 ad2antlr 
 |-  ( ( ( ph /\ y e. RR ) /\ l e. Z ) -> y e. RR* )
60 36 adantlr 
 |-  ( ( ( ph /\ y e. RR ) /\ l e. Z ) -> ( F ` l ) e. RR* )
61 xleneg 
 |-  ( ( y e. RR* /\ ( F ` l ) e. RR* ) -> ( y <_ ( F ` l ) <-> -e ( F ` l ) <_ -e y ) )
62 59 60 61 syl2anc 
 |-  ( ( ( ph /\ y e. RR ) /\ l e. Z ) -> ( y <_ ( F ` l ) <-> -e ( F ` l ) <_ -e y ) )
63 62 biimprd 
 |-  ( ( ( ph /\ y e. RR ) /\ l e. Z ) -> ( -e ( F ` l ) <_ -e y -> y <_ ( F ` l ) ) )
64 56 57 63 syl2anc 
 |-  ( ( ( ( ph /\ y e. RR ) /\ i e. Z ) /\ l e. ( ZZ>= ` i ) ) -> ( -e ( F ` l ) <_ -e y -> y <_ ( F ` l ) ) )
65 64 ralimdva 
 |-  ( ( ( ph /\ y e. RR ) /\ i e. Z ) -> ( A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y -> A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
66 65 reximdva 
 |-  ( ( ph /\ y e. RR ) -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y -> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) ) )
67 66 imp 
 |-  ( ( ( ph /\ y e. RR ) /\ E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ -e y ) -> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
68 47 48 55 67 syl21anc 
 |-  ( ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) /\ y e. RR ) -> E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
69 68 ralrimiva 
 |-  ( ( ph /\ A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) -> A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) )
70 46 69 impbida 
 |-  ( ph -> ( A. y e. RR E. i e. Z A. l e. ( ZZ>= ` i ) y <_ ( F ` l ) <-> A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w ) )
71 breq2 
 |-  ( w = x -> ( -e ( F ` l ) <_ w <-> -e ( F ` l ) <_ x ) )
72 71 rexralbidv 
 |-  ( w = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ x ) )
73 fveq2 
 |-  ( i = k -> ( ZZ>= ` i ) = ( ZZ>= ` k ) )
74 73 raleqdv 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ x <-> A. l e. ( ZZ>= ` k ) -e ( F ` l ) <_ x ) )
75 12 nfxneg 
 |-  F/_ j -e ( F ` l )
76 nfcv 
 |-  F/_ j x
77 75 10 76 nfbr 
 |-  F/ j -e ( F ` l ) <_ x
78 nfv 
 |-  F/ l -e ( F ` j ) <_ x
79 fveq2 
 |-  ( l = j -> ( F ` l ) = ( F ` j ) )
80 79 xnegeqd 
 |-  ( l = j -> -e ( F ` l ) = -e ( F ` j ) )
81 80 breq1d 
 |-  ( l = j -> ( -e ( F ` l ) <_ x <-> -e ( F ` j ) <_ x ) )
82 77 78 81 cbvralw 
 |-  ( A. l e. ( ZZ>= ` k ) -e ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
83 74 82 bitrdi 
 |-  ( i = k -> ( A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ x <-> A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
84 83 cbvrexvw 
 |-  ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ x <-> E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
85 72 84 bitrdi 
 |-  ( w = x -> ( E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
86 85 cbvralvw 
 |-  ( A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x )
87 86 a1i 
 |-  ( ph -> ( A. w e. RR E. i e. Z A. l e. ( ZZ>= ` i ) -e ( F ` l ) <_ w <-> A. x e. RR E. k e. Z A. j e. ( ZZ>= ` k ) -e ( F ` j ) <_ x ) )
88 21 70 87 3bitrd 
 |-  ( 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 ) )