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