:: 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;