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 ffvelrnda ( ( 𝜑𝑘𝑍 ) → ( 𝐹𝑘 ) ∈ ℝ* )
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 ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ( 𝑗𝑍 ↦ -𝑒 ( 𝐹𝑗 ) ) ~~>* -∞ ) )