:: Complex Numbers - Basic Theorems
:: by Library Committee
::
:: Received April 10, 2003
:: Copyright (c) 2003-2021 Association of Mizar Users


:: '+' operation only
theorem :: XCMPLX_1:1
for a, b, c being Complex holds a + (b + c) = (a + b) + c ;

theorem :: XCMPLX_1:2
for a, b, c being Complex st a + c = b + c holds
a = b ;

theorem :: XCMPLX_1:3
for a, b being Complex st a = a + b holds
b = 0 ;

:: using operation '*'
theorem Th4: :: XCMPLX_1:4
for a, b, c being Complex holds a * (b * c) = (a * b) * c ;

theorem :: XCMPLX_1:5
for a, b, c being Complex st c <> 0 & a * c = b * c holds
a = b
proof end;

theorem :: XCMPLX_1:6
for a, b being Complex holds
( not a * b = 0 or a = 0 or b = 0 ) ;

theorem Th7: :: XCMPLX_1:7
for a, b being Complex st b <> 0 & a * b = b holds
a = 1
proof end;

:: operations '+' and '*' only
theorem :: XCMPLX_1:8
for a, b, c being Complex holds a * (b + c) = (a * b) + (a * c) ;

theorem :: XCMPLX_1:9
for a, b, c, d being Complex holds ((a + b) + c) * d = ((a * d) + (b * d)) + (c * d) ;

theorem :: XCMPLX_1:10
for a, b, c, d being Complex holds (a + b) * (c + d) = (((a * c) + (a * d)) + (b * c)) + (b * d) ;

theorem :: XCMPLX_1:11
for a being Complex holds 2 * a = a + a ;

theorem :: XCMPLX_1:12
for a being Complex holds 3 * a = (a + a) + a ;

theorem :: XCMPLX_1:13
for a being Complex holds 4 * a = ((a + a) + a) + a ;

:: using operation '-'
theorem :: XCMPLX_1:14
for a being Complex holds a - a = 0 ;

theorem :: XCMPLX_1:15
for a, b being Complex st a - b = 0 holds
a = b ;

theorem :: XCMPLX_1:16
for a, b being Complex st b - a = b holds
a = 0 ;

:: 2 times '-'
theorem :: XCMPLX_1:17
for a, b being Complex holds a = a - (b - b) ;

theorem :: XCMPLX_1:18
for a, b being Complex holds a - (a - b) = b ;

theorem :: XCMPLX_1:19
for a, b, c being Complex st a - c = b - c holds
a = b ;

theorem :: XCMPLX_1:20
for a, b, c being Complex st c - a = c - b holds
a = b ;

theorem :: XCMPLX_1:21
for a, b, c being Complex holds (a - b) - c = (a - c) - b ;

theorem :: XCMPLX_1:22
for a, b, c being Complex holds a - c = (a - b) - (c - b) ;

theorem :: XCMPLX_1:23
for a, b, c being Complex holds (c - a) - (c - b) = b - a ;

theorem :: XCMPLX_1:24
for a, b, c, d being Complex st a - b = c - d holds
a - c = b - d ;

Lm1: for a, b being Complex holds (a ") * (b ") = (a * b) "
proof end;

Lm2: for a, b, c being Complex holds a / (b / c) = (a * c) / b
proof end;

Lm3: for a, b being Complex st b <> 0 holds
(a / b) * b = a
proof end;

Lm4: for a being Complex holds 1 / a = a "
proof end;

Lm5: for a being Complex st a <> 0 holds
a / a = 1
proof end;

:: using operations '-' and '+'
theorem :: XCMPLX_1:25
for a, b being Complex holds a = a + (b - b) ;

theorem :: XCMPLX_1:26
for a, b being Complex holds a = (a + b) - b ;

theorem :: XCMPLX_1:27
for a, b being Complex holds a = (a - b) + b ;

theorem :: XCMPLX_1:28
for a, b, c being Complex holds a + c = (a + b) + (c - b) ;

:: 2 times '-'
theorem :: XCMPLX_1:29
for a, b, c being Complex holds (a + b) - c = (a - c) + b ;

theorem :: XCMPLX_1:30
for a, b, c being Complex holds (a - b) + c = (c - b) + a ;

theorem :: XCMPLX_1:31
for a, b, c being Complex holds a + c = (a + b) - (b - c) ;

theorem :: XCMPLX_1:32
for a, b, c being Complex holds a - c = (a + b) - (c + b) ;

theorem :: XCMPLX_1:33
for a, b, c, d being Complex st a + b = c + d holds
a - c = d - b ;

theorem :: XCMPLX_1:34
for a, b, c, d being Complex st a - c = d - b holds
a + b = c + d ;

theorem :: XCMPLX_1:35
for a, b, c, d being Complex st a + b = c - d holds
a + d = c - b ;

:: 3 times '-'
theorem :: XCMPLX_1:36
for a, b, c being Complex holds a - (b + c) = (a - b) - c ;

theorem :: XCMPLX_1:37
for a, b, c being Complex holds a - (b - c) = (a - b) + c ;

theorem :: XCMPLX_1:38
for a, b, c being Complex holds a - (b - c) = a + (c - b) ;

theorem :: XCMPLX_1:39
for a, b, c being Complex holds a - c = (a - b) + (b - c) ;

theorem :: XCMPLX_1:40
for a, b, c being Complex holds a * (b - c) = (a * b) - (a * c) ;

theorem :: XCMPLX_1:41
for a, b, c, d being Complex holds (a - b) * (c - d) = (b - a) * (d - c) ;

theorem :: XCMPLX_1:42
for a, b, c, d being Complex holds ((a - b) - c) * d = ((a * d) - (b * d)) - (c * d) ;

:: using operations '-' and '*', '+'
theorem :: XCMPLX_1:43
for a, b, c, d being Complex holds ((a + b) - c) * d = ((a * d) + (b * d)) - (c * d) ;

theorem :: XCMPLX_1:44
for a, b, c, d being Complex holds ((a - b) + c) * d = ((a * d) - (b * d)) + (c * d) ;

theorem :: XCMPLX_1:45
for a, b, c, d being Complex holds (a + b) * (c - d) = (((a * c) - (a * d)) + (b * c)) - (b * d) ;

theorem :: XCMPLX_1:46
for a, b, c, d being Complex holds (a - b) * (c + d) = (((a * c) + (a * d)) - (b * c)) - (b * d) ;

theorem :: XCMPLX_1:47
for a, b, d, e being Complex holds (a - b) * (e - d) = (((a * e) - (a * d)) - (b * e)) + (b * d) ;

:: using operation '/'
theorem :: XCMPLX_1:48
for a, b, c being Complex holds (a / b) / c = (a / c) / b
proof end;

:: 0
theorem Th49: :: XCMPLX_1:49
for a being Complex holds a / 0 = 0
proof end;

theorem :: XCMPLX_1:50
for a, b being Complex st a <> 0 & b <> 0 holds
a / b <> 0 ;

:: 2 times '/'
theorem :: XCMPLX_1:51
for a, b being Complex st b <> 0 holds
a = a / (b / b)
proof end;

Lm6: for a, b, c, d being Complex holds (a / b) * (c / d) = (a * c) / (b * d)
proof end;

Lm7: for a, b being Complex holds (a / b) " = b / a
proof end;

Lm8: for a, b, c being Complex holds a * (b / c) = (a * b) / c
proof end;

theorem :: XCMPLX_1:52
for a, b being Complex st a <> 0 holds
a / (a / b) = b
proof end;

theorem :: XCMPLX_1:53
for a, b, c being Complex st c <> 0 & a / c = b / c holds
a = b
proof end;

Lm9: for a, b being Complex st b <> 0 holds
a = (a * b) / b
proof end;

theorem :: XCMPLX_1:54
for a, b being Complex st a / b <> 0 holds
b = a / (a / b)
proof end;

Lm10: for a, b, c being Complex st c <> 0 holds
a / b = (a * c) / (b * c)
proof end;

theorem :: XCMPLX_1:55
for a, b, c being Complex st c <> 0 holds
a / b = (a / c) / (b / c)
proof end;

:: 1
theorem :: XCMPLX_1:56
for a being Complex holds 1 / (1 / a) = a
proof end;

Lm11: for a, b being Complex holds (a * (b ")) " = (a ") * b
proof end;

theorem :: XCMPLX_1:57
for a, b being Complex holds 1 / (a / b) = b / a
proof end;

theorem Th58: :: XCMPLX_1:58
for a, b being Complex st a / b = 1 holds
a = b
proof end;

Lm12: for a, b being Complex st a " = b " holds
a = b
proof end;

theorem Th59: :: XCMPLX_1:59
for a, b being Complex st 1 / a = 1 / b holds
a = b
proof end;

:: 0 and 1
theorem :: XCMPLX_1:60
for a being Complex st a <> 0 holds
a / a = 1 by Lm5;

theorem :: XCMPLX_1:61
for a, b being Complex st b <> 0 & b / a = b holds
a = 1
proof end;

:: using operations '/' and '+'
theorem Th62: :: XCMPLX_1:62
for a, b, c being Complex holds (a / c) + (b / c) = (a + b) / c
proof end;

theorem :: XCMPLX_1:63
for a, b, d, e being Complex holds ((a + b) + e) / d = ((a / d) + (b / d)) + (e / d)
proof end;

:: 2
theorem :: XCMPLX_1:64
for a being Complex holds (a + a) / 2 = a ;

theorem :: XCMPLX_1:65
for a being Complex holds (a / 2) + (a / 2) = a ;

theorem :: XCMPLX_1:66
for a, b being Complex st a = (a + b) / 2 holds
a = b ;

:: 3
theorem :: XCMPLX_1:67
for a being Complex holds ((a + a) + a) / 3 = a ;

theorem :: XCMPLX_1:68
for a being Complex holds ((a / 3) + (a / 3)) + (a / 3) = a ;

:: 4
theorem :: XCMPLX_1:69
for a being Complex holds (((a + a) + a) + a) / 4 = a ;

theorem :: XCMPLX_1:70
for a being Complex holds (((a / 4) + (a / 4)) + (a / 4)) + (a / 4) = a ;

theorem :: XCMPLX_1:71
for a being Complex holds (a / 4) + (a / 4) = a / 2 ;

theorem :: XCMPLX_1:72
for a being Complex holds (a + a) / 4 = a / 2 ;

:: using operations '/' and '*'
theorem :: XCMPLX_1:73
for a, b being Complex st a * b = 1 holds
a = 1 / b
proof end;

theorem :: XCMPLX_1:74
for a, b, c being Complex holds a * (b / c) = (a * b) / c by Lm8;

theorem :: XCMPLX_1:75
for a, b, e being Complex holds (a / b) * e = (e / b) * a
proof end;

:: 3 times '/'
theorem :: XCMPLX_1:76
for a, b, c, d being Complex holds (a / b) * (c / d) = (a * c) / (b * d) by Lm6;

theorem :: XCMPLX_1:77
for a, b, c being Complex holds a / (b / c) = (a * c) / b by Lm2;

Lm13: for a, b, c, d being Complex holds (a / b) / (c / d) = (a * d) / (b * c)
proof end;

theorem Th78: :: XCMPLX_1:78
for a, b, c being Complex holds a / (b * c) = (a / b) / c
proof end;

theorem :: XCMPLX_1:79
for a, b, c being Complex holds a / (b / c) = a * (c / b)
proof end;

theorem :: XCMPLX_1:80
for a, b, c being Complex holds a / (b / c) = (c / b) * a
proof end;

theorem Th81: :: XCMPLX_1:81
for a, b, e being Complex holds a / (b / e) = e * (a / b)
proof end;

theorem :: XCMPLX_1:82
for a, b, c being Complex holds a / (b / c) = (a / b) * c
proof end;

Lm14: for a, b being Complex holds a * (1 / b) = a / b
proof end;

Lm15: for a, b, c being Complex holds (1 / c) * (a / b) = a / (b * c)
proof end;

theorem :: XCMPLX_1:83
for a, b, c, d being Complex holds (a * b) / (c * d) = ((a / c) * b) / d
proof end;

:: 4 times '/'
theorem :: XCMPLX_1:84
for a, b, c, d being Complex holds (a / b) / (c / d) = (a * d) / (b * c) by Lm13;

theorem :: XCMPLX_1:85
for a, b, c, d being Complex holds (a / c) * (b / d) = (a / d) * (b / c)
proof end;

theorem :: XCMPLX_1:86
for a, b, c, d, e being Complex holds a / ((b * c) * (d / e)) = (e / c) * (a / (b * d))
proof end;

:: 0
theorem :: XCMPLX_1:87
for a, b being Complex st b <> 0 holds
(a / b) * b = a by Lm3;

theorem :: XCMPLX_1:88
for a, b being Complex st b <> 0 holds
a = a * (b / b)
proof end;

theorem :: XCMPLX_1:89
for a, b being Complex st b <> 0 holds
a = (a * b) / b by Lm9;

theorem :: XCMPLX_1:90
for a, b, c being Complex st b <> 0 holds
a * c = (a * b) * (c / b)
proof end;

:: 2 times '/'
theorem :: XCMPLX_1:91
for a, b, c being Complex st c <> 0 holds
a / b = (a * c) / (b * c) by Lm10;

theorem :: XCMPLX_1:92
for a, b, c being Complex st c <> 0 holds
a / b = (a / (b * c)) * c
proof end;

theorem :: XCMPLX_1:93
for a, b, c being Complex st b <> 0 holds
a * c = (a * b) / (b / c)
proof end;

theorem Th94: :: XCMPLX_1:94
for a, b, c, d being Complex st c <> 0 & d <> 0 & a * c = b * d holds
a / d = b / c
proof end;

theorem Th95: :: XCMPLX_1:95
for a, b, c, d being Complex st c <> 0 & d <> 0 & a / d = b / c holds
a * c = b * d
proof end;

theorem :: XCMPLX_1:96
for a, b, c, d being Complex st c <> 0 & d <> 0 & a * c = b / d holds
a * d = b / c
proof end;

:: 3 times '/'
theorem :: XCMPLX_1:97
for a, b, c being Complex st c <> 0 holds
a / b = c * ((a / c) / b)
proof end;

theorem :: XCMPLX_1:98
for a, b, c being Complex st c <> 0 holds
a / b = (a / c) * (c / b)
proof end;

:: 1
theorem :: XCMPLX_1:99
for a, b being Complex holds a * (1 / b) = a / b by Lm14;

Lm16: for a being Complex holds 1 / (a ") = a
proof end;

theorem :: XCMPLX_1:100
for a, b being Complex holds a / (1 / b) = a * b
proof end;

theorem :: XCMPLX_1:101
for a, b, c being Complex holds (a / b) * c = ((1 / b) * c) * a
proof end;

:: 3 times '/'
theorem :: XCMPLX_1:102
for a, b being Complex holds (1 / a) * (1 / b) = 1 / (a * b)
proof end;

theorem :: XCMPLX_1:103
for a, b, c being Complex holds (1 / c) * (a / b) = a / (b * c) by Lm15;

:: 4 times '/'
theorem :: XCMPLX_1:104
for a, b, c being Complex holds (a / b) / c = (1 / b) * (a / c)
proof end;

theorem :: XCMPLX_1:105
for a, b, c being Complex holds (a / b) / c = (1 / c) * (a / b)
proof end;

:: 1 and 0
theorem Th106: :: XCMPLX_1:106
for a being Complex st a <> 0 holds
a * (1 / a) = 1
proof end;

theorem :: XCMPLX_1:107
for a, b being Complex st b <> 0 holds
a = (a * b) * (1 / b)
proof end;

theorem :: XCMPLX_1:108
for a, b being Complex st b <> 0 holds
a = a * ((1 / b) * b)
proof end;

theorem :: XCMPLX_1:109
for a, b being Complex st b <> 0 holds
a = (a * (1 / b)) * b
proof end;

theorem :: XCMPLX_1:110
for a, b being Complex st b <> 0 holds
a = a / (b * (1 / b))
proof end;

theorem :: XCMPLX_1:111
for a, b being Complex st a <> 0 & b <> 0 holds
1 / (a * b) <> 0 ;

theorem :: XCMPLX_1:112
for a, b being Complex st a <> 0 & b <> 0 holds
(a / b) * (b / a) = 1
proof end;

:: using operations '*', '+' and '/'
theorem Th113: :: XCMPLX_1:113
for a, b, c being Complex st b <> 0 holds
(a / b) + c = (a + (b * c)) / b
proof end;

theorem Th114: :: XCMPLX_1:114
for a, b, c being Complex st c <> 0 holds
a + b = c * ((a / c) + (b / c))
proof end;

theorem Th115: :: XCMPLX_1:115
for a, b, c being Complex st c <> 0 holds
a + b = ((a * c) + (b * c)) / c
proof end;

theorem Th116: :: XCMPLX_1:116
for a, b, c, d being Complex st b <> 0 & d <> 0 holds
(a / b) + (c / d) = ((a * d) + (c * b)) / (b * d)
proof end;

theorem Th117: :: XCMPLX_1:117
for a, b being Complex st a <> 0 holds
a + b = a * (1 + (b / a))
proof end;

:: 2
theorem :: XCMPLX_1:118
for a, b being Complex holds (a / (2 * b)) + (a / (2 * b)) = a / b
proof end;

:: 3
theorem :: XCMPLX_1:119
for a, b being Complex holds ((a / (3 * b)) + (a / (3 * b))) + (a / (3 * b)) = a / b
proof end;

Lm17: for a, b being Complex holds - (a / b) = (- a) / b
proof end;

theorem Th120: :: XCMPLX_1:120
for a, b, c being Complex holds (a / c) - (b / c) = (a - b) / c
proof end;

theorem :: XCMPLX_1:121
for a being Complex holds a - (a / 2) = a / 2 ;

theorem :: XCMPLX_1:122
for a, b, c, d being Complex holds ((a - b) - c) / d = ((a / d) - (b / d)) - (c / d)
proof end;

theorem :: XCMPLX_1:123
for a, b, d, e being Complex st b <> 0 & d <> 0 & b <> d & a / b = e / d holds
a / b = (a - e) / (b - d)
proof end;

:: using operations '-', '/' and '+'
theorem :: XCMPLX_1:124
for a, b, d, e being Complex holds ((a + b) - e) / d = ((a / d) + (b / d)) - (e / d)
proof end;

theorem :: XCMPLX_1:125
for a, b, d, e being Complex holds ((a - b) + e) / d = ((a / d) - (b / d)) + (e / d)
proof end;

:: using operations '-', '/' and '*'
theorem Th126: :: XCMPLX_1:126
for a, b, e being Complex st b <> 0 holds
(a / b) - e = (a - (e * b)) / b
proof end;

theorem :: XCMPLX_1:127
for a, b, c being Complex st b <> 0 holds
c - (a / b) = ((c * b) - a) / b
proof end;

theorem :: XCMPLX_1:128
for a, b, c being Complex st c <> 0 holds
a - b = c * ((a / c) - (b / c))
proof end;

theorem :: XCMPLX_1:129
for a, b, c being Complex st c <> 0 holds
a - b = ((a * c) - (b * c)) / c
proof end;

theorem :: XCMPLX_1:130
for a, b, c, d being Complex st b <> 0 & d <> 0 holds
(a / b) - (c / d) = ((a * d) - (c * b)) / (b * d)
proof end;

theorem :: XCMPLX_1:131
for a, b being Complex st a <> 0 holds
a - b = a * (1 - (b / a))
proof end;

:: using operation '-', '/', '*' and '+'
theorem :: XCMPLX_1:132
for a, b, c being Complex st a <> 0 holds
c = (((a * c) + b) - b) / a by Lm9;

:: using unary operation '-'
theorem :: XCMPLX_1:133
for a, b being Complex st - a = - b holds
a = b ;

theorem :: XCMPLX_1:134
for a being Complex st - a = 0 holds
a = 0 ;

theorem :: XCMPLX_1:135
for a, b being Complex st a + (- b) = 0 holds
a = b ;

theorem :: XCMPLX_1:136
for a, b being Complex holds a = (a + b) + (- b) ;

theorem :: XCMPLX_1:137
for a, b being Complex holds a = a + (b + (- b)) ;

theorem :: XCMPLX_1:138
for a, b being Complex holds a = ((- b) + a) + b ;

theorem :: XCMPLX_1:139
for a, b being Complex holds - (a + b) = (- a) + (- b) ;

theorem :: XCMPLX_1:140
for a, b being Complex holds - ((- a) + b) = a + (- b) ;

theorem :: XCMPLX_1:141
for a, b being Complex holds a + b = - ((- a) + (- b)) ;

:: using unary and binary operation '-'
theorem :: XCMPLX_1:142
for a, b being Complex holds - (a - b) = b - a ;

theorem :: XCMPLX_1:143
for a, b being Complex holds (- a) - b = (- b) - a ;

theorem :: XCMPLX_1:144
for a, b being Complex holds a = (- b) - ((- a) - b) ;

:: binary '-' 4 times
theorem :: XCMPLX_1:145
for a, b, c being Complex holds ((- a) - b) - c = ((- a) - c) - b ;

theorem :: XCMPLX_1:146
for a, b, c being Complex holds ((- a) - b) - c = ((- b) - c) - a ;

theorem :: XCMPLX_1:147
for a, b, c being Complex holds ((- a) - b) - c = ((- c) - b) - a ;

theorem :: XCMPLX_1:148
for a, b, c being Complex holds (c - a) - (c - b) = - (a - b) ;

:: 0
theorem :: XCMPLX_1:149
for a being Complex holds 0 - a = - a ;

:: using unary and binary operations '-' and '+'
theorem :: XCMPLX_1:150
for a, b being Complex holds a + b = a - (- b) ;

theorem :: XCMPLX_1:151
for a, b being Complex holds a = a - (b + (- b)) ;

theorem :: XCMPLX_1:152
for a, b, c being Complex st a - c = b + (- c) holds
a = b ;

theorem :: XCMPLX_1:153
for a, b, c being Complex st c - a = c + (- b) holds
a = b ;

:: '+' 3 times
theorem :: XCMPLX_1:154
for a, b, c being Complex holds (a + b) - c = ((- c) + a) + b ;

theorem :: XCMPLX_1:155
for a, b, c being Complex holds (a - b) + c = ((- b) + c) + a ;

theorem :: XCMPLX_1:156
for a, b, c being Complex holds a - ((- b) - c) = (a + b) + c ;

:: binary '-' 3 times
theorem :: XCMPLX_1:157
for a, b, c being Complex holds (a - b) - c = ((- b) - c) + a ;

theorem :: XCMPLX_1:158
for a, b, c being Complex holds (a - b) - c = ((- c) + a) - b ;

theorem :: XCMPLX_1:159
for a, b, c being Complex holds (a - b) - c = ((- c) - b) + a ;

:: using unary and binary operations '-' and '+'
theorem :: XCMPLX_1:160
for a, b being Complex holds - (a + b) = (- b) - a ;

theorem :: XCMPLX_1:161
for a, b being Complex holds - (a - b) = (- a) + b ;

theorem :: XCMPLX_1:162
for a, b being Complex holds - ((- a) + b) = a - b ;

theorem :: XCMPLX_1:163
for a, b being Complex holds a + b = - ((- a) - b) ;

theorem :: XCMPLX_1:164
for a, b, c being Complex holds ((- a) + b) - c = ((- c) + b) - a ;

:: using unary and binary operations '-' and '+' (both '-' 2 times)
theorem :: XCMPLX_1:165
for a, b, c being Complex holds ((- a) + b) - c = ((- c) - a) + b ;

theorem :: XCMPLX_1:166
for a, b, c being Complex holds - ((a + b) + c) = ((- a) - b) - c ;

theorem :: XCMPLX_1:167
for a, b, c being Complex holds - ((a + b) - c) = ((- a) - b) + c ;

theorem :: XCMPLX_1:168
for a, b, c being Complex holds - ((a - b) + c) = ((- a) + b) - c ;

theorem :: XCMPLX_1:169
for a, b, c being Complex holds - ((a - b) - c) = ((- a) + b) + c ;

theorem :: XCMPLX_1:170
for a, b, c being Complex holds - (((- a) + b) + c) = (a - b) - c ;

theorem :: XCMPLX_1:171
for a, b, c being Complex holds - (((- a) + b) - c) = (a - b) + c ;

theorem :: XCMPLX_1:172
for a, b, c being Complex holds - (((- a) - b) + c) = (a + b) - c ;

theorem :: XCMPLX_1:173
for a, b, c being Complex holds - (((- a) - b) - c) = (a + b) + c ;

:: using unary operations '-' and '*'
theorem :: XCMPLX_1:174
for a, b being Complex holds (- a) * b = - (a * b) ;

theorem :: XCMPLX_1:175
for a, b being Complex holds (- a) * b = a * (- b) ;

theorem :: XCMPLX_1:176
for a, b being Complex holds (- a) * (- b) = a * b ;

theorem :: XCMPLX_1:177
for a, b being Complex holds - (a * (- b)) = a * b ;

theorem :: XCMPLX_1:178
for a, b being Complex holds - ((- a) * b) = a * b ;

theorem :: XCMPLX_1:179
for a being Complex holds (- 1) * a = - a ;

theorem :: XCMPLX_1:180
for a being Complex holds (- a) * (- 1) = a ;

theorem Th181: :: XCMPLX_1:181
for a, b being Complex st b <> 0 & a * b = - b holds
a = - 1
proof end;

:: Thx
theorem Th182: :: XCMPLX_1:182
for a being Complex holds
( not a * a = 1 or a = 1 or a = - 1 )
proof end;

theorem :: XCMPLX_1:183
for a being Complex holds (- a) + (2 * a) = a ;

theorem :: XCMPLX_1:184
for a, b, c being Complex holds (a - b) * c = (b - a) * (- c) ;

theorem :: XCMPLX_1:185
for a, b, c being Complex holds (a - b) * c = - ((b - a) * c) ;

theorem :: XCMPLX_1:186
for a being Complex holds a - (2 * a) = - a ;

:: using unary operations '-' and '/'
theorem :: XCMPLX_1:187
for a, b being Complex holds - (a / b) = (- a) / b by Lm17;

theorem Th188: :: XCMPLX_1:188
for a, b being Complex holds a / (- b) = - (a / b)
proof end;

theorem :: XCMPLX_1:189
for a, b being Complex holds - (a / (- b)) = a / b
proof end;

theorem Th190: :: XCMPLX_1:190
for a, b being Complex holds - ((- a) / b) = a / b
proof end;

theorem :: XCMPLX_1:191
for a, b being Complex holds (- a) / (- b) = a / b
proof end;

theorem :: XCMPLX_1:192
for a, b being Complex holds (- a) / b = a / (- b)
proof end;

theorem :: XCMPLX_1:193
for a being Complex holds - a = a / (- 1) ;

theorem :: XCMPLX_1:194
for a being Complex holds a = (- a) / (- 1) ;

theorem :: XCMPLX_1:195
for a, b being Complex st a / b = - 1 holds
( a = - b & b = - a )
proof end;

theorem :: XCMPLX_1:196
for a, b being Complex st b <> 0 & b / a = - b holds
a = - 1
proof end;

theorem :: XCMPLX_1:197
for a being Complex st a <> 0 holds
(- a) / a = - 1
proof end;

theorem :: XCMPLX_1:198
for a being Complex st a <> 0 holds
a / (- a) = - 1
proof end;

Lm18: for a being Complex st a <> 0 & a = a " & not a = 1 holds
a = - 1
proof end;

theorem :: XCMPLX_1:199
for a being Complex st a <> 0 & a = 1 / a & not a = 1 holds
a = - 1
proof end;

theorem :: XCMPLX_1:200
for a, b, d, e being Complex st b <> 0 & d <> 0 & b <> - d & a / b = e / d holds
a / b = (a + e) / (b + d)
proof end;

:: using operation '"'
theorem :: XCMPLX_1:201
for a, b being Complex st a " = b " holds
a = b by Lm12;

theorem :: XCMPLX_1:202
0 " = 0 ;

:: using '"' and '*'
theorem :: XCMPLX_1:203
for a, b being Complex st b <> 0 holds
a = (a * b) * (b ")
proof end;

theorem :: XCMPLX_1:204
for a, b being Complex holds (a ") * (b ") = (a * b) " by Lm1;

theorem :: XCMPLX_1:205
for a, b being Complex holds (a * (b ")) " = (a ") * b by Lm11;

theorem :: XCMPLX_1:206
for a, b being Complex holds ((a ") * (b ")) " = a * b
proof end;

theorem :: XCMPLX_1:207
for a, b being Complex st a <> 0 & b <> 0 holds
a * (b ") <> 0 ;

theorem :: XCMPLX_1:208
for a, b being Complex st a <> 0 & b <> 0 holds
(a ") * (b ") <> 0 ;

theorem :: XCMPLX_1:209
for a, b being Complex st a * (b ") = 1 holds
a = b
proof end;

theorem :: XCMPLX_1:210
for a, b being Complex st a * b = 1 holds
a = b "
proof end;

:: using '"', '*', and '+'
theorem Th211: :: XCMPLX_1:211
for a, b being Complex st a <> 0 & b <> 0 holds
(a ") + (b ") = (a + b) * ((a * b) ")
proof end;

Lm19: for a being Complex holds (- a) " = - (a ")
proof end;

:: using '"', '*', and '-'
theorem :: XCMPLX_1:212
for a, b being Complex st a <> 0 & b <> 0 holds
(a ") - (b ") = (b - a) * ((a * b) ")
proof end;

:: using '"' and '/'
theorem :: XCMPLX_1:213
for a, b being Complex holds (a / b) " = b / a by Lm7;

theorem :: XCMPLX_1:214
for a, b being Complex holds (a ") / (b ") = b / a
proof end;

theorem :: XCMPLX_1:215
for a being Complex holds 1 / a = a " by Lm4;

theorem :: XCMPLX_1:216
for a being Complex holds 1 / (a ") = a by Lm16;

theorem :: XCMPLX_1:217
for a being Complex holds (1 / a) " = a
proof end;

theorem :: XCMPLX_1:218
for a, b being Complex st 1 / a = b " holds
a = b
proof end;

:: using '"', '*', and '/'
theorem :: XCMPLX_1:219
for a, b being Complex holds a / (b ") = a * b
proof end;

theorem :: XCMPLX_1:220
for a, b, c being Complex holds (a ") * (c / b) = c / (a * b)
proof end;

theorem :: XCMPLX_1:221
for a, b being Complex holds (a ") / b = (a * b) "
proof end;

:: both unary operations
theorem :: XCMPLX_1:222
for a being Complex holds (- a) " = - (a ") by Lm19;

theorem :: XCMPLX_1:223
for a being Complex st a <> 0 & a = a " & not a = 1 holds
a = - 1 by Lm18;

:: from JORDAN4
theorem :: XCMPLX_1:224
for a, b, c being Complex holds ((a + b) + c) - b = a + c ;

theorem :: XCMPLX_1:225
for a, b, c being Complex holds ((a - b) + c) + b = a + c ;

theorem :: XCMPLX_1:226
for a, b, c being Complex holds ((a + b) - c) - b = a - c ;

theorem :: XCMPLX_1:227
for a, b, c being Complex holds ((a - b) - c) + b = a - c ;

theorem :: XCMPLX_1:228
for a, b being Complex holds (a - a) - b = - b ;

theorem :: XCMPLX_1:229
for a, b being Complex holds ((- a) + a) - b = - b ;

theorem :: XCMPLX_1:230
for a, b being Complex holds (a - b) - a = - b ;

theorem :: XCMPLX_1:231
for a, b being Complex holds ((- a) - b) + a = - b ;

:: from REAL_2, 2005.02.05, A.T.
theorem :: XCMPLX_1:232
for a, b being Complex st b <> 0 holds
ex e being Complex st a = b / e
proof end;

:: from IRRAT_1, 2005.02.05, A.T.
theorem :: XCMPLX_1:233
for a, b, c, d, e being Complex holds a / ((b * c) * (d / e)) = (e / c) * (a / (b * d))
proof end;

:: from BORSUK_6, 2005.02.05, A.T.
theorem :: XCMPLX_1:234
for a, b, c, d being Complex holds (((d - c) / b) * a) + c = ((1 - (a / b)) * c) + ((a / b) * d)
proof end;

:: Missing, 2005.07.04, A.T.
theorem :: XCMPLX_1:235
for a, b, c being Complex st a <> 0 holds
(a * b) + c = a * (b + (c / a))
proof end;