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 ) )