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

Definition df-clim 13311
Description: Define the limit relation for complex number sequences. See clim 13317 for its relational expression. (Contributed by NM, 28-Aug-2005.)
Assertion
Ref Expression
df-clim
Distinct variable group:   , , , ,

Detailed syntax breakdown of Definition df-clim
StepHypRef Expression
1 cli 13307 . 2
2 vy . . . . . 6
32cv 1394 . . . . 5
4 cc 9511 . . . . 5
53, 4wcel 1818 . . . 4
6 vk . . . . . . . . . . 11
76cv 1394 . . . . . . . . . 10
8 vf . . . . . . . . . . 11
98cv 1394 . . . . . . . . . 10
107, 9cfv 5593 . . . . . . . . 9
1110, 4wcel 1818 . . . . . . . 8
12 cmin 9828 . . . . . . . . . . 11
1310, 3, 12co 6296 . . . . . . . . . 10
14 cabs 13067 . . . . . . . . . 10
1513, 14cfv 5593 . . . . . . . . 9
16 vx . . . . . . . . . 10
1716cv 1394 . . . . . . . . 9
18 clt 9649 . . . . . . . . 9
1915, 17, 18wbr 4452 . . . . . . . 8
2011, 19wa 369 . . . . . . 7
21 vj . . . . . . . . 9
2221cv 1394 . . . . . . . 8
23 cuz 11110 . . . . . . . 8
2422, 23cfv 5593 . . . . . . 7
2520, 6, 24wral 2807 . . . . . 6
26 cz 10889 . . . . . 6
2725, 21, 26wrex 2808 . . . . 5
28 crp 11249 . . . . 5
2927, 16, 28wral 2807 . . . 4
305, 29wa 369 . . 3
3130, 8, 2copab 4509 . 2
321, 31wceq 1395 1
Colors of variables: wff setvar class
This definition is referenced by:  climrel  13315  clim  13317  climf  31628
  Copyright terms: Public domain W3C validator