Metamath Proof Explorer

Theorem dfxlim2v

Description: An alternative definition for the convergence relation in the extended real numbers. This resembles what's found in most textbooks: three distinct definitions for the same symbol (limit of a sequence). (Contributed by Glauco Siliprandi, 5-Feb-2022)

Ref Expression
Hypotheses dfxlim2v.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
dfxlim2v.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
dfxlim2v.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion dfxlim2v ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) ) )

Proof

Step Hyp Ref Expression
1 dfxlim2v.1 ⊢ ( 𝜑 → 𝑀 ∈ ℤ )
2 dfxlim2v.2 ⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
3 dfxlim2v.3 ⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
4 simplr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 ∈ ℝ ) → 𝐹 ~~>* 𝐴 )
5 1 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝑀 ∈ ℤ )
6 3 adantr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐹 : 𝑍 ⟶ ℝ* )
7 simpr ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → 𝐴 ∈ ℝ )
8 5 2 6 7 xlimclim2 ⊢ ( ( 𝜑 ∧ 𝐴 ∈ ℝ ) → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
9 8 adantlr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐹 ~~>* 𝐴 ↔ 𝐹 ⇝ 𝐴 ) )
10 4 9 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 ∈ ℝ ) → 𝐹 ⇝ 𝐴 )
11 10 3mix1d ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 ∈ ℝ ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
12 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = -∞ ) → 𝐴 = -∞ )
13 simpl ⊢ ( ( 𝐹 ~~>* 𝐴 ∧ 𝐴 = -∞ ) → 𝐹 ~~>* 𝐴 )
14 simpr ⊢ ( ( 𝐹 ~~>* 𝐴 ∧ 𝐴 = -∞ ) → 𝐴 = -∞ )
15 13 14 breqtrd ⊢ ( ( 𝐹 ~~>* 𝐴 ∧ 𝐴 = -∞ ) → 𝐹 ~~>* -∞ )
16 15 adantll ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = -∞ ) → 𝐹 ~~>* -∞ )
17 nfcv ⊢ Ⅎ 𝑘 𝐹
18 17 1 2 3 xlimmnf ⊢ ( 𝜑 → ( 𝐹 ~~>* -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
19 18 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = -∞ ) → ( 𝐹 ~~>* -∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
20 16 19 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = -∞ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
21 3mix2 ⊢ ( ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
22 12 20 21 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = -∞ ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
23 22 adantlr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ ¬ 𝐴 ∈ ℝ ) ∧ 𝐴 = -∞ ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
24 simpll ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ ¬ 𝐴 ∈ ℝ ) ∧ ¬ 𝐴 = -∞ ) → ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) )
25 xlimcl ⊢ ( 𝐹 ~~>* 𝐴 → 𝐴 ∈ ℝ* )
26 25 ad3antlr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ ¬ 𝐴 ∈ ℝ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ∈ ℝ* )
27 simplr ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ ¬ 𝐴 ∈ ℝ ) ∧ ¬ 𝐴 = -∞ ) → ¬ 𝐴 ∈ ℝ )
28 neqne ⊢ ( ¬ 𝐴 = -∞ → 𝐴 ≠ -∞ )
29 28 adantl ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ ¬ 𝐴 ∈ ℝ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 ≠ -∞ )
30 26 27 29 xrnmnfpnf ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ ¬ 𝐴 ∈ ℝ ) ∧ ¬ 𝐴 = -∞ ) → 𝐴 = +∞ )
31 simpr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = +∞ ) → 𝐴 = +∞ )
32 simpl ⊢ ( ( 𝐹 ~~>* 𝐴 ∧ 𝐴 = +∞ ) → 𝐹 ~~>* 𝐴 )
33 simpr ⊢ ( ( 𝐹 ~~>* 𝐴 ∧ 𝐴 = +∞ ) → 𝐴 = +∞ )
34 32 33 breqtrd ⊢ ( ( 𝐹 ~~>* 𝐴 ∧ 𝐴 = +∞ ) → 𝐹 ~~>* +∞ )
35 34 adantll ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = +∞ ) → 𝐹 ~~>* +∞ )
36 17 1 2 3 xlimpnf ⊢ ( 𝜑 → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
37 36 ad2antrr ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = +∞ ) → ( 𝐹 ~~>* +∞ ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
38 35 37 mpbid ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = +∞ ) → ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
39 3mix3 ⊢ ( ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
40 31 38 39 syl2anc ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ 𝐴 = +∞ ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
41 24 30 40 syl2anc ⊢ ( ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ ¬ 𝐴 ∈ ℝ ) ∧ ¬ 𝐴 = -∞ ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
42 23 41 pm2.61dan ⊢ ( ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) ∧ ¬ 𝐴 ∈ ℝ ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
43 11 42 pm2.61dan ⊢ ( ( 𝜑 ∧ 𝐹 ~~>* 𝐴 ) → ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
44 1 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝑀 ∈ ℤ )
45 3 adantr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 : 𝑍 ⟶ ℝ* )
46 simpr ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ⇝ 𝐴 )
47 44 2 45 46 climxlim2 ⊢ ( ( 𝜑 ∧ 𝐹 ⇝ 𝐴 ) → 𝐹 ~~>* 𝐴 )
48 18 biimpar ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) → 𝐹 ~~>* -∞ )
49 48 adantrl ⊢ ( ( 𝜑 ∧ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ) → 𝐹 ~~>* -∞ )
50 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ) → 𝐴 = -∞ )
51 49 50 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ) → 𝐹 ~~>* 𝐴 )
52 36 biimpar ⊢ ( ( 𝜑 ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) → 𝐹 ~~>* +∞ )
53 52 adantrl ⊢ ( ( 𝜑 ∧ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) → 𝐹 ~~>* +∞ )
54 simprl ⊢ ( ( 𝜑 ∧ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) → 𝐴 = +∞ )
55 53 54 breqtrrd ⊢ ( ( 𝜑 ∧ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) → 𝐹 ~~>* 𝐴 )
56 47 51 55 3jaodan ⊢ ( ( 𝜑 ∧ ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) ) → 𝐹 ~~>* 𝐴 )
57 43 56 impbida ⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) ) )