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 _ j F
xlimpnfxnegmnf.2 Z = M
xlimpnfxnegmnf.3 φ F : Z *
Assertion xlimpnfxnegmnf φ x k Z j k x F j x k Z j k F j x

Proof

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