Metamath Proof Explorer

Theorem xlimpnfxnegmnf2

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 xlimpnfxnegmnf2.j ⊢ Ⅎ 𝑗 𝐹
xlimpnfxnegmnf2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
xlimpnfxnegmnf2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimpnfxnegmnf2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion xlimpnfxnegmnf2 ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ~~>* -∞ ) )

Proof

Step Hyp Ref Expression
1 xlimpnfxnegmnf2.j ⊢ Ⅎ 𝑗 𝐹
2 xlimpnfxnegmnf2.m ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3 xlimpnfxnegmnf2.z ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4 xlimpnfxnegmnf2.f ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
5 1 3 4 xlimpnfxnegmnf ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
6 1 2 3 4 xlimpnf ⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ) )
7 nfmpt1 ⊢ Ⅎ 𝑗 ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) )
8 4 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
9 8 xnegcld ⊢ ( ( 𝜑 ∧ 𝑘 ∈ 𝑍 ) → -𝑒 ( 𝐹 ‘ 𝑘 ) ∈ ℝ* )
10 nfcv ⊢ Ⅎ 𝑘 -𝑒 ( 𝐹 ‘ 𝑗 )
11 nfcv ⊢ Ⅎ 𝑗 𝑘
12 1 11 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑘 )
13 12 nfxneg ⊢ Ⅎ 𝑗 -𝑒 ( 𝐹 ‘ 𝑘 )
14 fveq2 ⊢ ( 𝑗 = 𝑘 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑘 ) )
15 14 xnegeqd ⊢ ( 𝑗 = 𝑘 → -𝑒 ( 𝐹 ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑘 ) )
16 10 13 15 cbvmpt ⊢ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) = ( 𝑘 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑘 ) )
17 9 16 fmptd ⊢ ( 𝜑 → ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) : 𝑍 ⟶ ℝ* )
18 7 2 3 17 xlimmnf ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ~~>* -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ) )
19 3 uztrn2 ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → 𝑗 ∈ 𝑍 )
20 xnegex ⊢ -𝑒 ( 𝐹 ‘ 𝑗 ) ∈ V
21 fvmpt4 ⊢ ( ( 𝑗 ∈ 𝑍 ∧ -𝑒 ( 𝐹 ‘ 𝑗 ) ∈ V ) → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
22 20 21 mpan2 ⊢ ( 𝑗 ∈ 𝑍 → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
23 22 breq1d ⊢ ( 𝑗 ∈ 𝑍 → ( ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
24 19 23 syl ⊢ ( ( 𝑘 ∈ 𝑍 ∧ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ) → ( ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
25 24 ralbidva ⊢ ( 𝑘 ∈ 𝑍 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
26 25 rexbiia ⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
27 26 ralbii ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ‘ 𝑗 ) ≤ 𝑥 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
28 18 27 bitrdi ⊢ ( 𝜑 → ( ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ~~>* -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
29 5 6 28 3bitr4d ⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ( 𝑗 ∈ 𝑍 ↦ -𝑒 ( 𝐹 ‘ 𝑗 ) ) ~~>* -∞ ) )