:: The Field of Complex Numbers
:: by Anna Justyna Milewska
::
:: Received January 18, 2000
:: Copyright (c) 2000 Association of Mizar Users
theorem :: COMPLFLD:1
canceled;
theorem :: COMPLFLD:2
canceled;
:: deftheorem Def1 defines F_Complex COMPLFLD:def 1 :
Lm1:
1_ F_Complex = 1r
by Def1;
Lm2:
1. F_Complex = 1r
by Def1;
theorem :: COMPLFLD:3
theorem Th4: :: COMPLFLD:4
theorem Th5: :: COMPLFLD:5
theorem :: COMPLFLD:6
theorem Th7: :: COMPLFLD:7
theorem Th8: :: COMPLFLD:8
theorem Th9: :: COMPLFLD:9
theorem :: COMPLFLD:10
theorem :: COMPLFLD:11
theorem :: COMPLFLD:12
canceled;
theorem :: COMPLFLD:13
canceled;
theorem :: COMPLFLD:14
canceled;
theorem :: COMPLFLD:15
canceled;
theorem :: COMPLFLD:16
canceled;
theorem :: COMPLFLD:17
canceled;
theorem :: COMPLFLD:18
canceled;
theorem :: COMPLFLD:19
canceled;
theorem :: COMPLFLD:20
canceled;
theorem :: COMPLFLD:21
canceled;
theorem :: COMPLFLD:22
canceled;
theorem :: COMPLFLD:23
canceled;
theorem :: COMPLFLD:24
canceled;
theorem :: COMPLFLD:25
canceled;
theorem :: COMPLFLD:26
canceled;
theorem :: COMPLFLD:27
canceled;
theorem :: COMPLFLD:28
canceled;
theorem :: COMPLFLD:29
theorem :: COMPLFLD:30
canceled;
theorem :: COMPLFLD:31
canceled;
theorem :: COMPLFLD:32
canceled;
theorem :: COMPLFLD:33
canceled;
theorem :: COMPLFLD:34
canceled;
theorem :: COMPLFLD:35
theorem :: COMPLFLD:36
canceled;
theorem :: COMPLFLD:37
canceled;
theorem :: COMPLFLD:38
canceled;
theorem :: COMPLFLD:39
canceled;
theorem :: COMPLFLD:40
canceled;
theorem :: COMPLFLD:41
theorem :: COMPLFLD:42
theorem :: COMPLFLD:43
canceled;
theorem :: COMPLFLD:44
canceled;
theorem :: COMPLFLD:45
canceled;
theorem :: COMPLFLD:46
canceled;
theorem :: COMPLFLD:47
theorem :: COMPLFLD:48
theorem :: COMPLFLD:49
theorem :: COMPLFLD:50
theorem :: COMPLFLD:51
theorem :: COMPLFLD:52
canceled;
theorem :: COMPLFLD:53
theorem :: COMPLFLD:54
canceled;
theorem :: COMPLFLD:55
theorem :: COMPLFLD:56
theorem :: COMPLFLD:57
canceled;
theorem :: COMPLFLD:58
theorem :: COMPLFLD:59
theorem :: COMPLFLD:60
theorem :: COMPLFLD:61
theorem Th62: :: COMPLFLD:62
theorem :: COMPLFLD:63
theorem :: COMPLFLD:64
theorem :: COMPLFLD:65
theorem :: COMPLFLD:66
theorem :: COMPLFLD:67
theorem :: COMPLFLD:68
theorem :: COMPLFLD:69
theorem :: COMPLFLD:70
theorem :: COMPLFLD:71
theorem :: COMPLFLD:72
theorem :: COMPLFLD:73
theorem :: COMPLFLD:74
theorem :: COMPLFLD:75
theorem :: COMPLFLD:76
theorem :: COMPLFLD:77
theorem :: COMPLFLD:78
theorem :: COMPLFLD:79
theorem :: COMPLFLD:80
theorem :: COMPLFLD:81
theorem :: COMPLFLD:82
theorem :: COMPLFLD:83
theorem Th84: :: COMPLFLD:84
theorem :: COMPLFLD:85
theorem :: COMPLFLD:86
theorem :: COMPLFLD:87
theorem :: COMPLFLD:88
theorem :: COMPLFLD:89
theorem :: COMPLFLD:90
theorem :: COMPLFLD:91
theorem :: COMPLFLD:92
theorem :: COMPLFLD:93
theorem :: COMPLFLD:94
theorem :: COMPLFLD:95
canceled;
theorem :: COMPLFLD:96
theorem :: COMPLFLD:97
theorem :: COMPLFLD:98
theorem :: COMPLFLD:99
canceled;
theorem :: COMPLFLD:100
theorem :: COMPLFLD:101
theorem :: COMPLFLD:102
theorem :: COMPLFLD:103
theorem :: COMPLFLD:104
theorem :: COMPLFLD:105
theorem :: COMPLFLD:106
theorem :: COMPLFLD:107
theorem :: COMPLFLD:108
theorem :: COMPLFLD:109
theorem :: COMPLFLD:110
theorem :: COMPLFLD:111
theorem Th112: :: COMPLFLD:112
:: deftheorem Def2 defines CRoot COMPLFLD:def 2 :
theorem :: COMPLFLD:113
theorem :: COMPLFLD:114
theorem :: COMPLFLD:115