:: Complex Numbers - Basic Theorems
:: by Library Committee
::
:: Received April 10, 2003
:: Copyright (c) 2003 Association of Mizar Users
theorem :: XCMPLX_1:1
theorem :: XCMPLX_1:2
theorem :: XCMPLX_1:3
theorem Th4: :: XCMPLX_1:4
theorem :: XCMPLX_1:5
theorem :: XCMPLX_1:6
theorem Th7: :: XCMPLX_1:7
theorem :: XCMPLX_1:8
theorem :: XCMPLX_1:9
theorem :: XCMPLX_1:10
theorem :: XCMPLX_1:11
theorem :: XCMPLX_1:12
theorem :: XCMPLX_1:13
theorem :: XCMPLX_1:14
theorem :: XCMPLX_1:15
theorem :: XCMPLX_1:16
theorem :: XCMPLX_1:17
theorem :: XCMPLX_1:18
theorem :: XCMPLX_1:19
theorem :: XCMPLX_1:20
theorem :: XCMPLX_1:21
theorem :: XCMPLX_1:22
theorem :: XCMPLX_1:23
theorem :: XCMPLX_1:24
Lm1:
for a, b being complex number holds (a " ) * (b " ) = (a * b) "
Lm2:
for a, b, c being complex number holds a / (b / c) = (a * c) / b
Lm3:
for b, a being complex number st b <> 0 holds
(a / b) * b = a
Lm4:
for a being complex number holds 1 / a = a "
Lm5:
for a being complex number st a <> 0 holds
a / a = 1
theorem :: XCMPLX_1:25
theorem :: XCMPLX_1:26
theorem :: XCMPLX_1:27
theorem :: XCMPLX_1:28
theorem :: XCMPLX_1:29
theorem :: XCMPLX_1:30
theorem :: XCMPLX_1:31
theorem :: XCMPLX_1:32
theorem :: XCMPLX_1:33
theorem :: XCMPLX_1:34
theorem :: XCMPLX_1:35
theorem :: XCMPLX_1:36
theorem :: XCMPLX_1:37
theorem :: XCMPLX_1:38
theorem :: XCMPLX_1:39
theorem :: XCMPLX_1:40
theorem :: XCMPLX_1:41
theorem :: XCMPLX_1:42
theorem :: XCMPLX_1:43
theorem :: XCMPLX_1:44
theorem :: XCMPLX_1:45
theorem :: XCMPLX_1:46
theorem :: XCMPLX_1:47
theorem :: XCMPLX_1:48
theorem Th49: :: XCMPLX_1:49
theorem :: XCMPLX_1:50
theorem :: XCMPLX_1:51
Lm7:
for a, b, c, d being complex number holds (a / b) * (c / d) = (a * c) / (b * d)
Lm8:
for a, b being complex number holds (a / b) " = b / a
Lm9:
for a, b, c being complex number holds a * (b / c) = (a * b) / c
theorem :: XCMPLX_1:52
theorem :: XCMPLX_1:53
Lm10:
for b, a being complex number st b <> 0 holds
a = (a * b) / b
theorem :: XCMPLX_1:54
Lm11:
for c, a, b being complex number st c <> 0 holds
a / b = (a * c) / (b * c)
theorem :: XCMPLX_1:55
theorem :: XCMPLX_1:56
Lm12:
for a, b being complex number holds (a * (b " )) " = (a " ) * b
theorem :: XCMPLX_1:57
theorem Th58: :: XCMPLX_1:58
Lm13:
for a, b being complex number st a " = b " holds
a = b
theorem Th59: :: XCMPLX_1:59
theorem :: XCMPLX_1:60
theorem :: XCMPLX_1:61
theorem :: XCMPLX_1:62
canceled;
theorem Th63: :: XCMPLX_1:63
theorem :: XCMPLX_1:64
theorem :: XCMPLX_1:65
theorem :: XCMPLX_1:66
theorem :: XCMPLX_1:67
theorem :: XCMPLX_1:68
theorem :: XCMPLX_1:69
theorem :: XCMPLX_1:70
theorem :: XCMPLX_1:71
theorem :: XCMPLX_1:72
theorem :: XCMPLX_1:73
theorem :: XCMPLX_1:74
theorem :: XCMPLX_1:75
theorem :: XCMPLX_1:76
theorem :: XCMPLX_1:77
theorem :: XCMPLX_1:78
Lm14:
for a, b, c, d being complex number holds (a / b) / (c / d) = (a * d) / (b * c)
theorem Th79: :: XCMPLX_1:79
theorem :: XCMPLX_1:80
theorem :: XCMPLX_1:81
theorem Th82: :: XCMPLX_1:82
theorem :: XCMPLX_1:83
Lm15:
for a, b being complex number holds a * (1 / b) = a / b
Lm16:
for c, a, b being complex number holds (1 / c) * (a / b) = a / (b * c)
theorem :: XCMPLX_1:84
theorem :: XCMPLX_1:85
theorem :: XCMPLX_1:86
theorem :: XCMPLX_1:87
theorem :: XCMPLX_1:88
theorem :: XCMPLX_1:89
theorem :: XCMPLX_1:90
theorem :: XCMPLX_1:91
theorem :: XCMPLX_1:92
theorem :: XCMPLX_1:93
theorem :: XCMPLX_1:94
theorem Th95: :: XCMPLX_1:95
theorem Th96: :: XCMPLX_1:96
theorem :: XCMPLX_1:97
theorem :: XCMPLX_1:98
theorem :: XCMPLX_1:99
theorem :: XCMPLX_1:100
Lm17:
for a being complex number holds 1 / (a " ) = a
theorem :: XCMPLX_1:101
theorem :: XCMPLX_1:102
theorem :: XCMPLX_1:103
theorem :: XCMPLX_1:104
theorem :: XCMPLX_1:105
theorem :: XCMPLX_1:106
theorem Th107: :: XCMPLX_1:107
theorem :: XCMPLX_1:108
theorem :: XCMPLX_1:109
theorem :: XCMPLX_1:110
theorem :: XCMPLX_1:111
theorem :: XCMPLX_1:112
theorem :: XCMPLX_1:113
theorem Th114: :: XCMPLX_1:114
theorem Th115: :: XCMPLX_1:115
theorem Th116: :: XCMPLX_1:116
theorem Th117: :: XCMPLX_1:117
theorem Th118: :: XCMPLX_1:118
theorem :: XCMPLX_1:119
theorem :: XCMPLX_1:120
Lm18:
for a, b being complex number holds - (a / b) = (- a) / b
theorem Th121: :: XCMPLX_1:121
theorem :: XCMPLX_1:122
theorem :: XCMPLX_1:123
theorem :: XCMPLX_1:124
theorem :: XCMPLX_1:125
theorem :: XCMPLX_1:126
theorem Th127: :: XCMPLX_1:127
theorem :: XCMPLX_1:128
theorem :: XCMPLX_1:129
theorem :: XCMPLX_1:130
theorem :: XCMPLX_1:131
theorem :: XCMPLX_1:132
theorem :: XCMPLX_1:133
theorem :: XCMPLX_1:134
theorem :: XCMPLX_1:135
theorem :: XCMPLX_1:136
theorem :: XCMPLX_1:137
theorem :: XCMPLX_1:138
theorem :: XCMPLX_1:139
theorem :: XCMPLX_1:140
theorem :: XCMPLX_1:141
theorem :: XCMPLX_1:142
theorem :: XCMPLX_1:143
theorem :: XCMPLX_1:144
theorem :: XCMPLX_1:145
theorem :: XCMPLX_1:146
theorem :: XCMPLX_1:147
theorem :: XCMPLX_1:148
theorem :: XCMPLX_1:149
theorem :: XCMPLX_1:150
theorem :: XCMPLX_1:151
theorem :: XCMPLX_1:152
theorem :: XCMPLX_1:153
theorem :: XCMPLX_1:154
theorem :: XCMPLX_1:155
theorem :: XCMPLX_1:156
theorem :: XCMPLX_1:157
theorem :: XCMPLX_1:158
theorem :: XCMPLX_1:159
theorem :: XCMPLX_1:160
theorem :: XCMPLX_1:161
theorem :: XCMPLX_1:162
theorem :: XCMPLX_1:163
theorem :: XCMPLX_1:164
theorem :: XCMPLX_1:165
theorem :: XCMPLX_1:166
theorem :: XCMPLX_1:167
theorem :: XCMPLX_1:168
theorem :: XCMPLX_1:169
theorem :: XCMPLX_1:170
theorem :: XCMPLX_1:171
theorem :: XCMPLX_1:172
theorem :: XCMPLX_1:173
theorem :: XCMPLX_1:174
theorem :: XCMPLX_1:175
theorem :: XCMPLX_1:176
theorem :: XCMPLX_1:177
theorem :: XCMPLX_1:178
theorem :: XCMPLX_1:179
theorem :: XCMPLX_1:180
theorem :: XCMPLX_1:181
theorem Th182: :: XCMPLX_1:182
theorem Th183: :: XCMPLX_1:183
theorem :: XCMPLX_1:184
theorem :: XCMPLX_1:185
theorem :: XCMPLX_1:186
theorem :: XCMPLX_1:187
theorem :: XCMPLX_1:188
theorem Th189: :: XCMPLX_1:189
theorem :: XCMPLX_1:190
theorem Th191: :: XCMPLX_1:191
theorem :: XCMPLX_1:192
theorem :: XCMPLX_1:193
theorem :: XCMPLX_1:194
theorem :: XCMPLX_1:195
theorem :: XCMPLX_1:196
theorem :: XCMPLX_1:197
theorem :: XCMPLX_1:198
theorem :: XCMPLX_1:199
Lm19:
for a being complex number st a <> 0 & a = a " & not a = 1 holds
a = - 1
theorem :: XCMPLX_1:200
theorem :: XCMPLX_1:201
theorem :: XCMPLX_1:202
theorem :: XCMPLX_1:203
theorem :: XCMPLX_1:204
theorem :: XCMPLX_1:205
theorem :: XCMPLX_1:206
theorem :: XCMPLX_1:207
theorem :: XCMPLX_1:208
theorem :: XCMPLX_1:209
theorem :: XCMPLX_1:210
theorem :: XCMPLX_1:211
theorem :: XCMPLX_1:212
canceled;
theorem Th213: :: XCMPLX_1:213
Lm20:
for a being complex number holds (- a) " = - (a " )
theorem :: XCMPLX_1:214
theorem :: XCMPLX_1:215
theorem :: XCMPLX_1:216
theorem :: XCMPLX_1:217
theorem :: XCMPLX_1:218
theorem :: XCMPLX_1:219
theorem :: XCMPLX_1:220
theorem :: XCMPLX_1:221
theorem :: XCMPLX_1:222
theorem :: XCMPLX_1:223
theorem :: XCMPLX_1:224
theorem :: XCMPLX_1:225
theorem :: XCMPLX_1:226
theorem :: XCMPLX_1:227
theorem :: XCMPLX_1:228
theorem :: XCMPLX_1:229
theorem :: XCMPLX_1:230
theorem :: XCMPLX_1:231
theorem :: XCMPLX_1:232
theorem :: XCMPLX_1:233
theorem :: XCMPLX_1:234
theorem :: XCMPLX_1:235
theorem :: XCMPLX_1:236
theorem :: XCMPLX_1:237