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

Definition df-cnfld 16659
 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 16661, cnfldadd 16663, cnfldmul 16664, cnfldcj 16665, cnfldtset 16666, cnfldle 16667, cnfldds 16668, and cnfldbas 16662. We may add additional members to this in the future. (Contributed by Stefan O'Rear, 27-Nov-2014.) (Revised by Thierry Arnoux, 15-Dec-2017.) (New usage is discouraged.)
Assertion
Ref Expression
df-cnfld fld TopSet metUnif

Detailed syntax breakdown of Definition df-cnfld
StepHypRef Expression
1 ccnfld 16658 . 2 fld
2 cnx 13421 . . . . . . 7
3 cbs 13424 . . . . . . 7
42, 3cfv 5413 . . . . . 6
5 cc 8944 . . . . . 6
64, 5cop 3777 . . . . 5
7 cplusg 13484 . . . . . . 7
82, 7cfv 5413 . . . . . 6
9 caddc 8949 . . . . . 6
108, 9cop 3777 . . . . 5
11 cmulr 13485 . . . . . . 7
122, 11cfv 5413 . . . . . 6
13 cmul 8951 . . . . . 6
1412, 13cop 3777 . . . . 5
156, 10, 14ctp 3776 . . . 4
16 cstv 13486 . . . . . . 7
172, 16cfv 5413 . . . . . 6
18 ccj 11856 . . . . . 6
1917, 18cop 3777 . . . . 5
2019csn 3774 . . . 4
2115, 20cun 3278 . . 3
22 cts 13490 . . . . . . 7 TopSet
232, 22cfv 5413 . . . . . 6 TopSet
24 cabs 11994 . . . . . . . 8
25 cmin 9247 . . . . . . . 8
2624, 25ccom 4841 . . . . . . 7
27 cmopn 16646 . . . . . . 7
2826, 27cfv 5413 . . . . . 6
2923, 28cop 3777 . . . . 5 TopSet
30 cple 13491 . . . . . . 7
312, 30cfv 5413 . . . . . 6
32 cle 9077 . . . . . 6
3331, 32cop 3777 . . . . 5
34 cds 13493 . . . . . . 7
352, 34cfv 5413 . . . . . 6
3635, 26cop 3777 . . . . 5
3729, 33, 36ctp 3776 . . . 4 TopSet
38 cunif 13494 . . . . . . 7
392, 38cfv 5413 . . . . . 6
40 cmetu 16648 . . . . . . 7 metUnif
4126, 40cfv 5413 . . . . . 6 metUnif
4239, 41cop 3777 . . . . 5 metUnif
4342csn 3774 . . . 4 metUnif
4437, 43cun 3278 . . 3 TopSet metUnif
4521, 44cun 3278 . 2 TopSet metUnif
461, 45wceq 1649 1 fld TopSet metUnif
 Colors of variables: wff set class This definition is referenced by:  cnfldstr  16660  cnfldbas  16662  cnfldadd  16663  cnfldmul  16664  cnfldcj  16665  cnfldtset  16666  cnfldle  16667  cnfldds  16668  cnfldunif  16669
 Copyright terms: Public domain W3C validator