MPE Home Metamath Proof Explorer < Previous   Next >
Nearby theorems
Mirrors  >  Home  >  MPE Home  >  Th. List  >  df-clim Structured version   Visualization version   GIF version

Definition df-clim 14009
Description: Define the limit relation for complex number sequences. See clim 14015 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
StepHypRef Expression
1 cli 14005 . 2 class
2 vy . . . . . 6 setvar 𝑦
32cv 1473 . . . . 5 class 𝑦
4 cc 9786 . . . . 5 class
53, 4wcel 1975 . . . 4 wff 𝑦 ∈ ℂ
6 vk . . . . . . . . . . 11 setvar 𝑘
76cv 1473 . . . . . . . . . 10 class 𝑘
8 vf . . . . . . . . . . 11 setvar 𝑓
98cv 1473 . . . . . . . . . 10 class 𝑓
107, 9cfv 5786 . . . . . . . . 9 class (𝑓𝑘)
1110, 4wcel 1975 . . . . . . . 8 wff (𝑓𝑘) ∈ ℂ
12 cmin 10113 . . . . . . . . . . 11 class
1310, 3, 12co 6523 . . . . . . . . . 10 class ((𝑓𝑘) − 𝑦)
14 cabs 13764 . . . . . . . . . 10 class abs
1513, 14cfv 5786 . . . . . . . . 9 class (abs‘((𝑓𝑘) − 𝑦))
16 vx . . . . . . . . . 10 setvar 𝑥
1716cv 1473 . . . . . . . . 9 class 𝑥
18 clt 9926 . . . . . . . . 9 class <
1915, 17, 18wbr 4573 . . . . . . . 8 wff (abs‘((𝑓𝑘) − 𝑦)) < 𝑥
2011, 19wa 382 . . . . . . 7 wff ((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥)
21 vj . . . . . . . . 9 setvar 𝑗
2221cv 1473 . . . . . . . 8 class 𝑗
23 cuz 11515 . . . . . . . 8 class
2422, 23cfv 5786 . . . . . . 7 class (ℤ𝑗)
2520, 6, 24wral 2891 . . . . . 6 wff 𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥)
26 cz 11206 . . . . . 6 class
2725, 21, 26wrex 2892 . . . . 5 wff 𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥)
28 crp 11660 . . . . 5 class +
2927, 16, 28wral 2891 . . . 4 wff 𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥)
305, 29wa 382 . . 3 wff (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))
3130, 8, 2copab 4632 . 2 class {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
321, 31wceq 1474 1 wff ⇝ = {⟨𝑓, 𝑦⟩ ∣ (𝑦 ∈ ℂ ∧ ∀𝑥 ∈ ℝ+𝑗 ∈ ℤ ∀𝑘 ∈ (ℤ𝑗)((𝑓𝑘) ∈ ℂ ∧ (abs‘((𝑓𝑘) − 𝑦)) < 𝑥))}
Colors of variables: wff setvar class
This definition is referenced by:  climrel  14013  clim  14015  climf  38489  climf2  38533
  Copyright terms: Public domain W3C validator