Definition df-clim 15242

Description: Define the limit relation for complex number sequences. See clim 15248 for its relational expression. (Contributed by NM, 28-Aug-2005.)

Assertion

Ref	Expression
df-clim	⊢ ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}

Distinct variable group:   𝑗,𝑘,𝑥,𝑦,𝑓

Detailed syntax breakdown of Definition df-clim

Step	Hyp	Ref	Expression
1		cli 15238	. 2 class ⇝
2		vy	. . . . . 6 setvar 𝑦
3	2	cv 1538	. . . . 5 class 𝑦
4		cc 10915	. . . . 5 class ℂ
5	3, 4	wcel 2104	. . . 4 wff 𝑦 ∈ ℂ
6		vk	. . . . . . . . . . 11 setvar 𝑘
7	6	cv 1538	. . . . . . . . . 10 class 𝑘
8		vf	. . . . . . . . . . 11 setvar 𝑓
9	8	cv 1538	. . . . . . . . . 10 class 𝑓
10	7, 9	cfv 6458	. . . . . . . . 9 class (𝑓‘𝑘)
11	10, 4	wcel 2104	. . . . . . . 8 wff (𝑓‘𝑘) ∈ ℂ
12		cmin 11251	. . . . . . . . . . 11 class −
13	10, 3, 12	co 7307	. . . . . . . . . 10 class ((𝑓‘𝑘) − 𝑦)
14		cabs 14990	. . . . . . . . . 10 class abs
15	13, 14	cfv 6458	. . . . . . . . 9 class (abs‘((𝑓‘𝑘) − 𝑦))
16		vx	. . . . . . . . . 10 setvar 𝑥
17	16	cv 1538	. . . . . . . . 9 class 𝑥
18		clt 11055	. . . . . . . . 9 class <
19	15, 17, 18	wbr 5081	. . . . . . . 8 wff (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥
20	11, 19	wa 397	. . . . . . 7 wff ((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥)
21		vj	. . . . . . . . 9 setvar 𝑗
22	21	cv 1538	. . . . . . . 8 class 𝑗
23		cuz 12628	. . . . . . . 8 class ℤ≥
24	22, 23	cfv 6458	. . . . . . 7 class (ℤ≥‘𝑗)
25	20, 6, 24	wral 3062	. . . . . 6 wff ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥)
26		cz 12365	. . . . . 6 class ℤ
27	25, 21, 26	wrex 3071	. . . . 5 wff ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥)
28		crp 12776	. . . . 5 class ℝ+
29	27, 16, 28	wral 3062	. . . 4 wff ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥)
30	5, 29	wa 397	. . 3 wff (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))
31	30, 8, 2	copab 5143	. 2 class {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}
32	1, 31	wceq 1539	1 wff ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+ ∃𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ≥‘𝑗)((𝑓‘𝑘) ∈ ℂ ∧ (abs‘((𝑓‘𝑘) − 𝑦)) < 𝑥))}

This definition is referenced by:  climrel  15246  clim  15248  climf  43212  climf2  43256