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 ⊢ Ⅎ 𝑗 𝐹
xlimpnfxnegmnf.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
xlimpnfxnegmnf.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion xlimpnfxnegmnf ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )

Proof

Step Hyp Ref Expression
1 xlimpnfxnegmnf.1 ⊢ Ⅎ 𝑗 𝐹
2 xlimpnfxnegmnf.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 xlimpnfxnegmnf.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 breq1 ⊢ ( 𝑥 = 𝑦 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
5 4 rexralbidv ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
6 fveq2 ⊢ ( 𝑘 = 𝑖 → ( ℤ≥ ‘ 𝑘 ) = ( ℤ≥ ‘ 𝑖 ) )
7 6 raleqdv ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ) )
8 nfv ⊢ Ⅎ 𝑙 𝑦 ≤ ( 𝐹 ‘ 𝑗 )
9 nfcv ⊢ Ⅎ 𝑗 𝑦
10 nfcv ⊢ Ⅎ 𝑗 ≤
11 nfcv ⊢ Ⅎ 𝑗 𝑙
12 1 11 nffv ⊢ Ⅎ 𝑗 ( 𝐹 ‘ 𝑙 )
13 9 10 12 nfbr ⊢ Ⅎ 𝑗 𝑦 ≤ ( 𝐹 ‘ 𝑙 )
14 fveq2 ⊢ ( 𝑗 = 𝑙 → ( 𝐹 ‘ 𝑗 ) = ( 𝐹 ‘ 𝑙 ) )
15 14 breq2d ⊢ ( 𝑗 = 𝑙 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ↔ 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
16 8 13 15 cbvralw ⊢ ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) )
17 7 16 bitrdi ⊢ ( 𝑘 = 𝑖 → ( ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
18 17 cbvrexvw ⊢ ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑦 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) )
19 5 18 bitrdi ⊢ ( 𝑥 = 𝑦 → ( ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
20 19 cbvralvw ⊢ ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) )
21 20 a1i ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
22 simpll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ∧ 𝑤 ∈ ℝ ) → 𝜑 )
23 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ∧ 𝑤 ∈ ℝ ) → 𝑤 ∈ ℝ )
24 xnegrecl ⊢ ( 𝑤 ∈ ℝ → -𝑒 𝑤 ∈ ℝ )
25 simpl ⊢ ( ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ 𝑤 ∈ ℝ ) → ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) )
26 breq1 ⊢ ( 𝑦 = -𝑒 𝑤 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) ) )
27 26 rexralbidv ⊢ ( 𝑦 = -𝑒 𝑤 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) ) )
28 27 rspcva ⊢ ( ( -𝑒 𝑤 ∈ ℝ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) )
29 24 25 28 syl2an2 ⊢ ( ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) )
30 29 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) )
31 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝜑 ∧ 𝑤 ∈ ℝ ) )
32 2 uztrn2 ⊢ ( ( 𝑖 ∈ 𝑍 ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑙 ∈ 𝑍 )
33 32 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑙 ∈ 𝑍 )
34 rexr ⊢ ( 𝑤 ∈ ℝ → 𝑤 ∈ ℝ* )
35 34 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ 𝑍 ) → 𝑤 ∈ ℝ* )
36 3 ffvelcdmda ⊢ ( ( 𝜑 ∧ 𝑙 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑙 ) ∈ ℝ* )
37 36 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑙 ) ∈ ℝ* )
38 xlenegcon1 ⊢ ( ( 𝑤 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑙 ) ∈ ℝ* ) → ( -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) ↔ -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) )
39 35 37 38 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ 𝑍 ) → ( -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) ↔ -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) )
40 39 biimpd ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑙 ∈ 𝑍 ) → ( -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) → -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) )
41 31 33 40 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) → -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) )
42 41 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) → ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) )
43 42 reximdva ⊢ ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) )
44 43 imp ⊢ ( ( ( 𝜑 ∧ 𝑤 ∈ ℝ ) ∧ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 𝑤 ≤ ( 𝐹 ‘ 𝑙 ) ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 )
45 22 23 30 44 syl21anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ∧ 𝑤 ∈ ℝ ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 )
46 45 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) → ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 )
47 simpll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) ∧ 𝑦 ∈ ℝ ) → 𝜑 )
48 simpr ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) ∧ 𝑦 ∈ ℝ ) → 𝑦 ∈ ℝ )
49 xnegrecl ⊢ ( 𝑦 ∈ ℝ → -𝑒 𝑦 ∈ ℝ )
50 simpl ⊢ ( ( ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ∧ 𝑦 ∈ ℝ ) → ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 )
51 breq2 ⊢ ( 𝑤 = -𝑒 𝑦 → ( -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ↔ -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 ) )
52 51 rexralbidv ⊢ ( 𝑤 = -𝑒 𝑦 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 ) )
53 52 rspcva ⊢ ( ( -𝑒 𝑦 ∈ ℝ ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 )
54 49 50 53 syl2an2 ⊢ ( ( ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ∧ 𝑦 ∈ ℝ ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 )
55 54 adantll ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 )
56 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( 𝜑 ∧ 𝑦 ∈ ℝ ) )
57 32 adantll ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → 𝑙 ∈ 𝑍 )
58 rexr ⊢ ( 𝑦 ∈ ℝ → 𝑦 ∈ ℝ* )
59 58 ad2antlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ 𝑍 ) → 𝑦 ∈ ℝ* )
60 36 adantlr ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ 𝑍 ) → ( 𝐹 ‘ 𝑙 ) ∈ ℝ* )
61 xleneg ⊢ ( ( 𝑦 ∈ ℝ* ∧ ( 𝐹 ‘ 𝑙 ) ∈ ℝ* ) → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 ) )
62 59 60 61 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ 𝑍 ) → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 ) )
63 62 biimprd ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑙 ∈ 𝑍 ) → ( -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 → 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
64 56 57 63 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) ∧ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ) → ( -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 → 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
65 64 ralimdva ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ 𝑖 ∈ 𝑍 ) → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 → ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
66 65 reximdva ⊢ ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) )
67 66 imp ⊢ ( ( ( 𝜑 ∧ 𝑦 ∈ ℝ ) ∧ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ -𝑒 𝑦 ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) )
68 47 48 55 67 syl21anc ⊢ ( ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) ∧ 𝑦 ∈ ℝ ) → ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) )
69 68 ralrimiva ⊢ ( ( 𝜑 ∧ ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) → ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) )
70 46 69 impbida ⊢ ( 𝜑 → ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ) )
71 breq2 ⊢ ( 𝑤 = 𝑥 → ( -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ↔ -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
72 71 rexralbidv ⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
73 fveq2 ⊢ ( 𝑖 = 𝑘 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑘 ) )
74 73 raleqdv ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
75 12 nfxneg ⊢ Ⅎ 𝑗 -𝑒 ( 𝐹 ‘ 𝑙 )
76 nfcv ⊢ Ⅎ 𝑗 𝑥
77 75 10 76 nfbr ⊢ Ⅎ 𝑗 -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
78 nfv ⊢ Ⅎ 𝑙 -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥
79 fveq2 ⊢ ( 𝑙 = 𝑗 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑗 ) )
80 79 xnegeqd ⊢ ( 𝑙 = 𝑗 → -𝑒 ( 𝐹 ‘ 𝑙 ) = -𝑒 ( 𝐹 ‘ 𝑗 ) )
81 80 breq1d ⊢ ( 𝑙 = 𝑗 → ( -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
82 77 78 81 cbvralw ⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
83 74 82 bitrdi ⊢ ( 𝑖 = 𝑘 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
84 83 cbvrexvw ⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
85 72 84 bitrdi ⊢ ( 𝑤 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ↔ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
86 85 cbvralvw ⊢ ( ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 )
87 86 a1i ⊢ ( 𝜑 → ( ∀ 𝑤 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) -𝑒 ( 𝐹 ‘ 𝑙 ) ≤ 𝑤 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )
88 21 70 87 3bitrd ⊢ ( 𝜑 → ( ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) 𝑥 ≤ ( 𝐹 ‘ 𝑗 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑘 ∈ 𝑍 ∀ 𝑗 ∈ ( ℤ≥ ‘ 𝑘 ) -𝑒 ( 𝐹 ‘ 𝑗 ) ≤ 𝑥 ) )