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 ⊢Ⅎ_jF
xlimpnfxnegmnf.2 ⊢Z=ℤ≥M
xlimpnfxnegmnf.3 ⊢φ→F:Z⟶ℝ*
Assertion xlimpnfxnegmnf ⊢φ→∀x∈ℝ∃k∈Z∀j∈ℤ≥kx≤F⁡j↔∀x∈ℝ∃k∈Z∀j∈ℤ≥k−F⁡j≤x

Proof

Step Hyp Ref Expression
1 xlimpnfxnegmnf.1 ⊢Ⅎ_jF
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∈ℤ≥kx≤F⁡j↔∃k∈Z∀j∈ℤ≥ky≤F⁡j
6 fveq2 ⊢k=i→ℤ≥k=ℤ≥i
7 6 raleqdv ⊢k=i→∀j∈ℤ≥ky≤F⁡j↔∀j∈ℤ≥iy≤F⁡j
8 nfv ⊢Ⅎly≤F⁡j
9 nfcv ⊢Ⅎ_jy
10 nfcv ⊢Ⅎ_j≤
11 nfcv ⊢Ⅎ_jl
12 1 11 nffv ⊢Ⅎ_jF⁡l
13 9 10 12 nfbr ⊢Ⅎjy≤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∈ℤ≥iy≤F⁡j↔∀l∈ℤ≥iy≤F⁡l
17 7 16 bitrdi ⊢k=i→∀j∈ℤ≥ky≤F⁡j↔∀l∈ℤ≥iy≤F⁡l
18 17 cbvrexvw ⊢∃k∈Z∀j∈ℤ≥ky≤F⁡j↔∃i∈Z∀l∈ℤ≥iy≤F⁡l
19 5 18 bitrdi ⊢x=y→∃k∈Z∀j∈ℤ≥kx≤F⁡j↔∃i∈Z∀l∈ℤ≥iy≤F⁡l
20 19 cbvralvw ⊢∀x∈ℝ∃k∈Z∀j∈ℤ≥kx≤F⁡j↔∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l
21 20 a1i ⊢φ→∀x∈ℝ∃k∈Z∀j∈ℤ≥kx≤F⁡j↔∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l
22 simpll ⊢φ∧∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l∧w∈ℝ→φ
23 simpr ⊢φ∧∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l∧w∈ℝ→w∈ℝ
24 xnegrecl ⊢w∈ℝ→−w∈ℝ
25 simpl ⊢∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l∧w∈ℝ→∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l
26 breq1 ⊢y=−w→y≤F⁡l↔−w≤F⁡l
27 26 rexralbidv ⊢y=−w→∃i∈Z∀l∈ℤ≥iy≤F⁡l↔∃i∈Z∀l∈ℤ≥i−w≤F⁡l
28 27 rspcva ⊢−w∈ℝ∧∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l→∃i∈Z∀l∈ℤ≥i−w≤F⁡l
29 24 25 28 syl2an2 ⊢∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l∧w∈ℝ→∃i∈Z∀l∈ℤ≥i−w≤F⁡l
30 29 adantll ⊢φ∧∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤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 ffvelcdmda ⊢φ∧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∈ℤ≥iy≤F⁡l∧w∈ℝ→∃i∈Z∀l∈ℤ≥i−F⁡l≤w
46 45 ralrimiva ⊢φ∧∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤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∈ℤ≥iy≤F⁡l
66 65 reximdva ⊢φ∧y∈ℝ→∃i∈Z∀l∈ℤ≥i−F⁡l≤−y→∃i∈Z∀l∈ℤ≥iy≤F⁡l
67 66 imp ⊢φ∧y∈ℝ∧∃i∈Z∀l∈ℤ≥i−F⁡l≤−y→∃i∈Z∀l∈ℤ≥iy≤F⁡l
68 47 48 55 67 syl21anc ⊢φ∧∀w∈ℝ∃i∈Z∀l∈ℤ≥i−F⁡l≤w∧y∈ℝ→∃i∈Z∀l∈ℤ≥iy≤F⁡l
69 68 ralrimiva ⊢φ∧∀w∈ℝ∃i∈Z∀l∈ℤ≥i−F⁡l≤w→∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤F⁡l
70 46 69 impbida ⊢φ→∀y∈ℝ∃i∈Z∀l∈ℤ≥iy≤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 ⊢Ⅎ_jx
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∈ℤ≥kx≤F⁡j↔∀x∈ℝ∃k∈Z∀j∈ℤ≥k−F⁡j≤x