Theorem dfxlim2

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	dfxlim2.k	⊢ Ⅎ 𝑘 𝐹
	dfxlim2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
	dfxlim2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
	dfxlim2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
Assertion	dfxlim2	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) ) )

Proof

Step	Hyp	Ref	Expression
1		dfxlim2.k	⊢ Ⅎ 𝑘 𝐹
2		dfxlim2.m	⊢ ( 𝜑 → 𝑀 ∈ ℤ )
3		dfxlim2.z	⊢ 𝑍 = ( ℤ≥ ‘ 𝑀 )
4		dfxlim2.f	⊢ ( 𝜑 → 𝐹 : 𝑍 ⟶ ℝ* )
5	2 3 4	dfxlim2v	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) ) )
6		biid	⊢ ( 𝐹 ⇝ 𝐴 ↔ 𝐹 ⇝ 𝐴 )
7		breq2	⊢ ( 𝑦 = 𝑥 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
8	7	rexralbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
9		fveq2	⊢ ( 𝑖 = 𝑗 → ( ℤ≥ ‘ 𝑖 ) = ( ℤ≥ ‘ 𝑗 ) )
10	9	raleqdv	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ) )
11		nfcv	⊢ Ⅎ 𝑘 𝑙
12	1 11	nffv	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 )
13		nfcv	⊢ Ⅎ 𝑘 ≤
14		nfcv	⊢ Ⅎ 𝑘 𝑥
15	12 13 14	nfbr	⊢ Ⅎ 𝑘 ( 𝐹 ‘ 𝑙 ) ≤ 𝑥
16		nfv	⊢ Ⅎ 𝑙 ( 𝐹 ‘ 𝑘 ) ≤ 𝑥
17		fveq2	⊢ ( 𝑙 = 𝑘 → ( 𝐹 ‘ 𝑙 ) = ( 𝐹 ‘ 𝑘 ) )
18	17	breq1d	⊢ ( 𝑙 = 𝑘 → ( ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
19	15 16 18	cbvralw	⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
20	10 19	bitrdi	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
21	20	cbvrexvw	⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑥 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
22	8 21	bitrdi	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
23	22	cbvralvw	⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 )
24	23	anbi2i	⊢ ( ( 𝐴 = -∞ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ↔ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) )
25		breq1	⊢ ( 𝑦 = 𝑥 → ( 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
26	25	rexralbidv	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
27	9	raleqdv	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ) )
28	14 13 12	nfbr	⊢ Ⅎ 𝑘 𝑥 ≤ ( 𝐹 ‘ 𝑙 )
29		nfv	⊢ Ⅎ 𝑙 𝑥 ≤ ( 𝐹 ‘ 𝑘 )
30	17	breq2d	⊢ ( 𝑙 = 𝑘 → ( 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
31	28 29 30	cbvralw	⊢ ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
32	27 31	bitrdi	⊢ ( 𝑖 = 𝑗 → ( ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
33	32	cbvrexvw	⊢ ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑥 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
34	26 33	bitrdi	⊢ ( 𝑦 = 𝑥 → ( ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
35	34	cbvralvw	⊢ ( ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ↔ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) )
36	35	anbi2i	⊢ ( ( 𝐴 = +∞ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ↔ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) )
37	6 24 36	3orbi123i	⊢ ( ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) ( 𝐹 ‘ 𝑙 ) ≤ 𝑦 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑦 ∈ ℝ ∃ 𝑖 ∈ 𝑍 ∀ 𝑙 ∈ ( ℤ≥ ‘ 𝑖 ) 𝑦 ≤ ( 𝐹 ‘ 𝑙 ) ) ) ↔ ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) )
38	5 37	bitrdi	⊢ ( 𝜑 → ( 𝐹 ~~>* 𝐴 ↔ ( 𝐹 ⇝ 𝐴 ∨ ( 𝐴 = -∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) ( 𝐹 ‘ 𝑘 ) ≤ 𝑥 ) ∨ ( 𝐴 = +∞ ∧ ∀ 𝑥 ∈ ℝ ∃ 𝑗 ∈ 𝑍 ∀ 𝑘 ∈ ( ℤ≥ ‘ 𝑗 ) 𝑥 ≤ ( 𝐹 ‘ 𝑘 ) ) ) ) )