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

Definition df-cnfld 16378
 Description: The field of complex numbers. Other number fields and rings can be constructed by applying the ↾s restriction operator, for instance ℂfld is the field of algebraic numbers. The contract of this set is defined entirely by cnfldex 16380, cnfldadd 16384, cnfldmul 16385, cnfldcj 16386, cnfldtset 16387, cnfldle 16388, cnfldds 16389, and cnfldbas 16383. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (New usage is discouraged.)
Assertion
Ref Expression
df-cnfld fld TopSet

Detailed syntax breakdown of Definition df-cnfld
StepHypRef Expression
1 ccnfld 16377 . 2 fld
2 cnx 13145 . . . . . . 7
3 cbs 13148 . . . . . . 7
42, 3cfv 5255 . . . . . 6
5 cc 8735 . . . . . 6
64, 5cop 3643 . . . . 5
7 cplusg 13208 . . . . . . 7
82, 7cfv 5255 . . . . . 6
9 caddc 8740 . . . . . 6
108, 9cop 3643 . . . . 5
11 cmulr 13209 . . . . . . 7
122, 11cfv 5255 . . . . . 6
13 cmul 8742 . . . . . 6
1412, 13cop 3643 . . . . 5
156, 10, 14ctp 3642 . . . 4
16 cstv 13210 . . . . . . 7
172, 16cfv 5255 . . . . . 6
18 ccj 11581 . . . . . 6
1917, 18cop 3643 . . . . 5
2019csn 3640 . . . 4
2115, 20cun 3150 . . 3
22 cts 13214 . . . . . 6 TopSet
232, 22cfv 5255 . . . . 5 TopSet
24 cabs 11719 . . . . . . 7
25 cmin 9037 . . . . . . 7
2624, 25ccom 4693 . . . . . 6
27 cmopn 16372 . . . . . 6
2826, 27cfv 5255 . . . . 5
2923, 28cop 3643 . . . 4 TopSet
30 cple 13215 . . . . . 6
312, 30cfv 5255 . . . . 5
32 cle 8868 . . . . 5
3331, 32cop 3643 . . . 4
34 cds 13217 . . . . . 6
352, 34cfv 5255 . . . . 5
3635, 26cop 3643 . . . 4
3729, 33, 36ctp 3642 . . 3 TopSet
3821, 37cun 3150 . 2 TopSet
391, 38wceq 1623 1 fld TopSet
 Colors of variables: wff set class This definition is referenced by:  cnfldstr  16379  cnfldbas  16383  cnfldadd  16384  cnfldmul  16385  cnfldcj  16386  cnfldtset  16387  cnfldle  16388  cnfldds  16389
 Copyright terms: Public domain W3C validator