:: XCMPLX_1 semantic presentation

theorem Th1: :: XCMPLX_1:1

for b₁, b₂, b₃ being complex number holds b₁ + (b₂ + b₃) = (b₁ + b₂) + b₃ ;

theorem Th2: :: XCMPLX_1:2

for b₁, b₂, b₃ being complex number st b₁ + b₂ = b₃ + b₂ holds
b₁ = b₃ ;

theorem Th3: :: XCMPLX_1:3

for b₁, b₂ being complex number st b₁ = b₁ + b₂ holds
b₂ = 0 ;

theorem Th4: :: XCMPLX_1:4

for b₁, b₂, b₃ being complex number holds b₁ * (b₂ * b₃) = (b₁ * b₂) * b₃ ;

theorem Th5: :: XCMPLX_1:5

for b₁, b₂, b₃ being complex number st b₁ <> 0 & b₂ * b₁ = b₃ * b₁ holds
b₂ = b₃

proof end;

theorem Th6: :: XCMPLX_1:6

for b₁, b₂ being complex number holds
( not b₁ * b₂ = 0 or b₁ = 0 or b₂ = 0 )

proof end;

theorem Th7: :: XCMPLX_1:7

for b₁, b₂ being complex number st b₁ <> 0 & b₂ * b₁ = b₁ holds
b₂ = 1

proof end;

theorem Th8: :: XCMPLX_1:8

for b₁, b₂, b₃ being complex number holds b₁ * (b₂ + b₃) = (b₁ * b₂) + (b₁ * b₃) ;

theorem Th9: :: XCMPLX_1:9

for b₁, b₂, b₃, b₄ being complex number holds ((b₁ + b₂) + b₃) * b₄ = ((b₁ * b₄) + (b₂ * b₄)) + (b₃ * b₄) ;

theorem Th10: :: XCMPLX_1:10

for b₁, b₂, b₃, b₄ being complex number holds (b₁ + b₂) * (b₃ + b₄) = (((b₁ * b₃) + (b₁ * b₄)) + (b₂ * b₃)) + (b₂ * b₄) ;

theorem Th11: :: XCMPLX_1:11

for b₁ being complex number holds 2 * b₁ = b₁ + b₁ ;

theorem Th12: :: XCMPLX_1:12

for b₁ being complex number holds 3 * b₁ = (b₁ + b₁) + b₁ ;

theorem Th13: :: XCMPLX_1:13

for b₁ being complex number holds 4 * b₁ = ((b₁ + b₁) + b₁) + b₁ ;

theorem Th14: :: XCMPLX_1:14

for b₁ being complex number holds b₁ - b₁ = 0 ;

theorem Th15: :: XCMPLX_1:15

for b₁, b₂ being complex number st b₁ - b₂ = 0 holds
b₁ = b₂ ;

theorem Th16: :: XCMPLX_1:16

for b₁, b₂ being complex number st b₁ - b₂ = b₁ holds
b₂ = 0 ;

theorem Th17: :: XCMPLX_1:17

for b₁, b₂ being complex number holds b₁ = b₁ - (b₂ - b₂) ;

theorem Th18: :: XCMPLX_1:18

for b₁, b₂ being complex number holds b₁ - (b₁ - b₂) = b₂ ;

theorem Th19: :: XCMPLX_1:19

for b₁, b₂, b₃ being complex number st b₁ - b₂ = b₃ - b₂ holds
b₁ = b₃ ;

theorem Th20: :: XCMPLX_1:20

for b₁, b₂, b₃ being complex number st b₁ - b₂ = b₁ - b₃ holds
b₂ = b₃ ;

theorem Th21: :: XCMPLX_1:21

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) - b₃ = (b₁ - b₃) - b₂ ;

theorem Th22: :: XCMPLX_1:22

for b₁, b₂, b₃ being complex number holds b₁ - b₂ = (b₁ - b₃) - (b₂ - b₃) ;

theorem Th23: :: XCMPLX_1:23

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) - (b₁ - b₃) = b₃ - b₂ ;

theorem Th24: :: XCMPLX_1:24

for b₁, b₂, b₃, b₄ being complex number st b₁ - b₂ = b₃ - b₄ holds
b₁ - b₃ = b₂ - b₄ ;

Lemma4: for b₁, b₂ being complex number holds (b₁ " ) * (b₂ " ) = (b₁ * b₂) "

proof end;

Lemma5: for b₁, b₂, b₃ being complex number holds b₁ / (b₂ / b₃) = (b₁ * b₃) / b₂

proof end;

Lemma6: for b₁, b₂ being complex number st b₁ <> 0 holds
(b₂ / b₁) * b₁ = b₂

proof end;

Lemma7: for b₁ being complex number holds 1 / b₁ = b₁ "

proof end;

Lemma8: for b₁ being complex number st b₁ <> 0 holds
b₁ / b₁ = 1

proof end;

theorem Th25: :: XCMPLX_1:25

for b₁, b₂ being complex number holds b₁ = b₁ + (b₂ - b₂) ;

theorem Th26: :: XCMPLX_1:26

for b₁, b₂ being complex number holds b₁ = (b₁ + b₂) - b₂ ;

theorem Th27: :: XCMPLX_1:27

for b₁, b₂ being complex number holds b₁ = (b₁ - b₂) + b₂ ;

theorem Th28: :: XCMPLX_1:28

for b₁, b₂, b₃ being complex number holds b₁ + b₂ = (b₁ + b₃) + (b₂ - b₃) ;

theorem Th29: :: XCMPLX_1:29

for b₁, b₂, b₃ being complex number holds (b₁ + b₂) - b₃ = (b₁ - b₃) + b₂ ;

theorem Th30: :: XCMPLX_1:30

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) + b₃ = (b₃ - b₂) + b₁ ;

theorem Th31: :: XCMPLX_1:31

for b₁, b₂, b₃ being complex number holds b₁ + b₂ = (b₁ + b₃) - (b₃ - b₂) ;

theorem Th32: :: XCMPLX_1:32

for b₁, b₂, b₃ being complex number holds b₁ - b₂ = (b₁ + b₃) - (b₂ + b₃) ;

theorem Th33: :: XCMPLX_1:33

for b₁, b₂, b₃, b₄ being complex number st b₁ + b₂ = b₃ + b₄ holds
b₁ - b₃ = b₄ - b₂ ;

theorem Th34: :: XCMPLX_1:34

for b₁, b₂, b₃, b₄ being complex number st b₁ - b₂ = b₃ - b₄ holds
b₁ + b₄ = b₂ + b₃ ;

theorem Th35: :: XCMPLX_1:35

for b₁, b₂, b₃, b₄ being complex number st b₁ + b₂ = b₃ - b₄ holds
b₁ + b₄ = b₃ - b₂ ;

theorem Th36: :: XCMPLX_1:36

for b₁, b₂, b₃ being complex number holds b₁ - (b₂ + b₃) = (b₁ - b₂) - b₃ ;

theorem Th37: :: XCMPLX_1:37

for b₁, b₂, b₃ being complex number holds b₁ - (b₂ - b₃) = (b₁ - b₂) + b₃ ;

theorem Th38: :: XCMPLX_1:38

for b₁, b₂, b₃ being complex number holds b₁ - (b₂ - b₃) = b₁ + (b₃ - b₂) ;

theorem Th39: :: XCMPLX_1:39

for b₁, b₂, b₃ being complex number holds b₁ - b₂ = (b₁ - b₃) + (b₃ - b₂) ;

theorem Th40: :: XCMPLX_1:40

for b₁, b₂, b₃ being complex number holds b₁ * (b₂ - b₃) = (b₁ * b₂) - (b₁ * b₃) ;

theorem Th41: :: XCMPLX_1:41

for b₁, b₂, b₃, b₄ being complex number holds (b₁ - b₂) * (b₃ - b₄) = (b₂ - b₁) * (b₄ - b₃) ;

theorem Th42: :: XCMPLX_1:42

for b₁, b₂, b₃, b₄ being complex number holds ((b₁ - b₂) - b₃) * b₄ = ((b₁ * b₄) - (b₂ * b₄)) - (b₃ * b₄) ;

theorem Th43: :: XCMPLX_1:43

for b₁, b₂, b₃, b₄ being complex number holds ((b₁ + b₂) - b₃) * b₄ = ((b₁ * b₄) + (b₂ * b₄)) - (b₃ * b₄) ;

theorem Th44: :: XCMPLX_1:44

for b₁, b₂, b₃, b₄ being complex number holds ((b₁ - b₂) + b₃) * b₄ = ((b₁ * b₄) - (b₂ * b₄)) + (b₃ * b₄) ;

theorem Th45: :: XCMPLX_1:45

for b₁, b₂, b₃, b₄ being complex number holds (b₁ + b₂) * (b₃ - b₄) = (((b₁ * b₃) - (b₁ * b₄)) + (b₂ * b₃)) - (b₂ * b₄) ;

theorem Th46: :: XCMPLX_1:46

for b₁, b₂, b₃, b₄ being complex number holds (b₁ - b₂) * (b₃ + b₄) = (((b₁ * b₃) + (b₁ * b₄)) - (b₂ * b₃)) - (b₂ * b₄) ;

theorem Th47: :: XCMPLX_1:47

for b₁, b₂, b₃, b₄ being complex number holds (b₁ - b₂) * (b₃ - b₄) = (((b₁ * b₃) - (b₁ * b₄)) - (b₂ * b₃)) + (b₂ * b₄) ;

theorem Th48: :: XCMPLX_1:48

for b₁, b₂, b₃ being complex number holds (b₁ / b₂) / b₃ = (b₁ / b₃) / b₂

proof end;

theorem Th49: :: XCMPLX_1:49

for b₁ being complex number holds b₁ / 0 = 0

proof end;

Lemma10: 0 " = 0
;

theorem Th50: :: XCMPLX_1:50

for b₁, b₂ being complex number st b₁ <> 0 & b₂ <> 0 holds
b₁ / b₂ <> 0

proof end;

theorem Th51: :: XCMPLX_1:51

for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = b₂ / (b₁ / b₁)

proof end;

Lemma12: for b₁, b₂, b₃, b₄ being complex number holds (b₁ / b₂) * (b₃ / b₄) = (b₁ * b₃) / (b₂ * b₄)

proof end;

Lemma13: for b₁, b₂ being complex number holds (b₁ / b₂) " = b₂ / b₁

proof end;

Lemma14: for b₁, b₂, b₃ being complex number holds b₁ * (b₂ / b₃) = (b₁ * b₂) / b₃

proof end;

theorem Th52: :: XCMPLX_1:52

for b₁, b₂ being complex number st b₁ <> 0 holds
b₁ / (b₁ / b₂) = b₂

proof end;

theorem Th53: :: XCMPLX_1:53

for b₁, b₂, b₃ being complex number st b₁ <> 0 & b₂ / b₁ = b₃ / b₁ holds
b₂ = b₃

proof end;

Lemma15: for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = (b₂ * b₁) / b₁

proof end;

theorem Th54: :: XCMPLX_1:54

for b₁, b₂ being complex number st b₁ / b₂ <> 0 holds
b₂ = b₁ / (b₁ / b₂)

proof end;

Lemma16: for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ / b₃ = (b₂ * b₁) / (b₃ * b₁)

proof end;

theorem Th55: :: XCMPLX_1:55

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ / b₃ = (b₂ / b₁) / (b₃ / b₁)

proof end;

theorem Th56: :: XCMPLX_1:56

for b₁ being complex number holds 1 / (1 / b₁) = b₁

proof end;

Lemma17: for b₁, b₂ being complex number holds (b₁ * (b₂ " )) " = (b₁ " ) * b₂

proof end;

theorem Th57: :: XCMPLX_1:57

for b₁, b₂ being complex number holds 1 / (b₁ / b₂) = b₂ / b₁

proof end;

theorem Th58: :: XCMPLX_1:58

for b₁, b₂ being complex number st b₁ / b₂ = 1 holds
b₁ = b₂

proof end;

Lemma19: for b₁, b₂ being complex number st b₁ " = b₂ " holds
b₁ = b₂

proof end;

theorem Th59: :: XCMPLX_1:59

for b₁, b₂ being complex number st 1 / b₁ = 1 / b₂ holds
b₁ = b₂

proof end;

theorem Th60: :: XCMPLX_1:60

for b₁ being complex number st b₁ <> 0 holds
b₁ / b₁ = 1 by Lemma8;

theorem Th61: :: XCMPLX_1:61

for b₁, b₂ being complex number st b₁ <> 0 & b₁ / b₂ = b₁ holds
b₂ = 1

proof end;

theorem Th62: :: XCMPLX_1:62

for b₁ being complex number holds b₁ / 0 = 0

proof end;

theorem Th63: :: XCMPLX_1:63

for b₁, b₂, b₃ being complex number holds (b₁ / b₂) + (b₃ / b₂) = (b₁ + b₃) / b₂

proof end;

theorem Th64: :: XCMPLX_1:64

for b₁, b₂, b₃, b₄ being complex number holds ((b₁ + b₂) + b₃) / b₄ = ((b₁ / b₄) + (b₂ / b₄)) + (b₃ / b₄)

proof end;

theorem Th65: :: XCMPLX_1:65

for b₁ being complex number holds (b₁ + b₁) / 2 = b₁ ;

theorem Th66: :: XCMPLX_1:66

for b₁ being complex number holds (b₁ / 2) + (b₁ / 2) = b₁ ;

theorem Th67: :: XCMPLX_1:67

for b₁, b₂ being complex number st b₁ = (b₁ + b₂) / 2 holds
b₁ = b₂ ;

theorem Th68: :: XCMPLX_1:68

for b₁ being complex number holds ((b₁ + b₁) + b₁) / 3 = b₁ ;

theorem Th69: :: XCMPLX_1:69

for b₁ being complex number holds ((b₁ / 3) + (b₁ / 3)) + (b₁ / 3) = b₁ ;

theorem Th70: :: XCMPLX_1:70

for b₁ being complex number holds (((b₁ + b₁) + b₁) + b₁) / 4 = b₁ ;

theorem Th71: :: XCMPLX_1:71

for b₁ being complex number holds (((b₁ / 4) + (b₁ / 4)) + (b₁ / 4)) + (b₁ / 4) = b₁ ;

theorem Th72: :: XCMPLX_1:72

for b₁ being complex number holds (b₁ / 4) + (b₁ / 4) = b₁ / 2 ;

theorem Th73: :: XCMPLX_1:73

for b₁ being complex number holds (b₁ + b₁) / 4 = b₁ / 2 ;

theorem Th74: :: XCMPLX_1:74

for b₁, b₂ being complex number st b₁ * b₂ = 1 holds
b₁ = 1 / b₂

proof end;

theorem Th75: :: XCMPLX_1:75

for b₁, b₂, b₃ being complex number holds b₁ * (b₂ / b₃) = (b₁ * b₂) / b₃ by Lemma14;

theorem Th76: :: XCMPLX_1:76

for b₁, b₂, b₃ being complex number holds (b₁ / b₂) * b₃ = (b₃ / b₂) * b₁

proof end;

theorem Th77: :: XCMPLX_1:77

for b₁, b₂, b₃, b₄ being complex number holds (b₁ / b₂) * (b₃ / b₄) = (b₁ * b₃) / (b₂ * b₄) by Lemma12;

theorem Th78: :: XCMPLX_1:78

for b₁, b₂, b₃ being complex number holds b₁ / (b₂ / b₃) = (b₁ * b₃) / b₂ by Lemma5;

Lemma22: for b₁, b₂, b₃, b₄ being complex number holds (b₁ / b₂) / (b₃ / b₄) = (b₁ * b₄) / (b₂ * b₃)

proof end;

theorem Th79: :: XCMPLX_1:79

for b₁, b₂, b₃ being complex number holds b₁ / (b₂ * b₃) = (b₁ / b₂) / b₃

proof end;

theorem Th80: :: XCMPLX_1:80

for b₁, b₂, b₃ being complex number holds b₁ / (b₂ / b₃) = b₁ * (b₃ / b₂)

proof end;

theorem Th81: :: XCMPLX_1:81

for b₁, b₂, b₃ being complex number holds b₁ / (b₂ / b₃) = (b₃ / b₂) * b₁

proof end;

theorem Th82: :: XCMPLX_1:82

for b₁, b₂, b₃ being complex number holds b₁ / (b₂ / b₃) = b₃ * (b₁ / b₂)

proof end;

theorem Th83: :: XCMPLX_1:83

for b₁, b₂, b₃ being complex number holds b₁ / (b₂ / b₃) = (b₁ / b₂) * b₃

proof end;

Lemma25: for b₁, b₂ being complex number holds b₁ * (1 / b₂) = b₁ / b₂

proof end;

Lemma26: for b₁, b₂, b₃ being complex number holds (1 / b₁) * (b₂ / b₃) = b₂ / (b₃ * b₁)

proof end;

theorem Th84: :: XCMPLX_1:84

for b₁, b₂, b₃, b₄ being complex number holds (b₁ * b₂) / (b₃ * b₄) = ((b₁ / b₃) * b₂) / b₄

proof end;

theorem Th85: :: XCMPLX_1:85

for b₁, b₂, b₃, b₄ being complex number holds (b₁ / b₂) / (b₃ / b₄) = (b₁ * b₄) / (b₂ * b₃) by Lemma22;

theorem Th86: :: XCMPLX_1:86

for b₁, b₂, b₃, b₄ being complex number holds (b₁ / b₂) * (b₃ / b₄) = (b₁ / b₄) * (b₃ / b₂)

proof end;

theorem Th87: :: XCMPLX_1:87

for b₁, b₂, b₃, b₄, b₅ being complex number holds b₁ / ((b₂ * b₃) * (b₄ / b₅)) = (b₅ / b₃) * (b₁ / (b₂ * b₄))

proof end;

theorem Th88: :: XCMPLX_1:88

for b₁, b₂ being complex number st b₁ <> 0 holds
(b₂ / b₁) * b₁ = b₂ by Lemma6;

theorem Th89: :: XCMPLX_1:89

for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = b₂ * (b₁ / b₁)

proof end;

theorem Th90: :: XCMPLX_1:90

for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = (b₂ * b₁) / b₁ by Lemma15;

theorem Th91: :: XCMPLX_1:91

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ * b₃ = (b₂ * b₁) * (b₃ / b₁)

proof end;

theorem Th92: :: XCMPLX_1:92

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ / b₃ = (b₂ * b₁) / (b₃ * b₁) by Lemma16;

theorem Th93: :: XCMPLX_1:93

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ / b₃ = (b₂ / (b₃ * b₁)) * b₁

proof end;

theorem Th94: :: XCMPLX_1:94

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ * b₃ = (b₂ * b₁) / (b₁ / b₃)

proof end;

theorem Th95: :: XCMPLX_1:95

for b₁, b₂, b₃, b₄ being complex number st b₁ <> 0 & b₂ <> 0 & b₃ * b₁ = b₄ * b₂ holds
b₃ / b₂ = b₄ / b₁

proof end;

theorem Th96: :: XCMPLX_1:96

for b₁, b₂, b₃, b₄ being complex number st b₁ <> 0 & b₂ <> 0 & b₃ / b₂ = b₄ / b₁ holds
b₃ * b₁ = b₄ * b₂

proof end;

theorem Th97: :: XCMPLX_1:97

for b₁, b₂, b₃, b₄ being complex number st b₁ <> 0 & b₂ <> 0 & b₃ * b₁ = b₄ / b₂ holds
b₃ * b₂ = b₄ / b₁

proof end;

theorem Th98: :: XCMPLX_1:98

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ / b₃ = b₁ * ((b₂ / b₁) / b₃)

proof end;

theorem Th99: :: XCMPLX_1:99

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ / b₃ = (b₂ / b₁) * (b₁ / b₃)

proof end;

theorem Th100: :: XCMPLX_1:100

for b₁, b₂ being complex number holds b₁ * (1 / b₂) = b₁ / b₂ by Lemma25;

Lemma30: for b₁ being complex number holds 1 / (b₁ " ) = b₁

proof end;

theorem Th101: :: XCMPLX_1:101

for b₁, b₂ being complex number holds b₁ / (1 / b₂) = b₁ * b₂

proof end;

theorem Th102: :: XCMPLX_1:102

for b₁, b₂, b₃ being complex number holds (b₁ / b₂) * b₃ = ((1 / b₂) * b₃) * b₁

proof end;

theorem Th103: :: XCMPLX_1:103

for b₁, b₂ being complex number holds (1 / b₁) * (1 / b₂) = 1 / (b₁ * b₂)

proof end;

theorem Th104: :: XCMPLX_1:104

for b₁, b₂, b₃ being complex number holds (1 / b₁) * (b₂ / b₃) = b₂ / (b₃ * b₁) by Lemma26;

theorem Th105: :: XCMPLX_1:105

for b₁, b₂, b₃ being complex number holds (b₁ / b₂) / b₃ = (1 / b₂) * (b₁ / b₃)

proof end;

theorem Th106: :: XCMPLX_1:106

for b₁, b₂, b₃ being complex number holds (b₁ / b₂) / b₃ = (1 / b₃) * (b₁ / b₂)

proof end;

theorem Th107: :: XCMPLX_1:107

for b₁ being complex number st b₁ <> 0 holds
b₁ * (1 / b₁) = 1

proof end;

theorem Th108: :: XCMPLX_1:108

for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = (b₂ * b₁) * (1 / b₁)

proof end;

theorem Th109: :: XCMPLX_1:109

for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = b₂ * ((1 / b₁) * b₁)

proof end;

theorem Th110: :: XCMPLX_1:110

for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = (b₂ * (1 / b₁)) * b₁

proof end;

theorem Th111: :: XCMPLX_1:111

for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = b₂ / (b₁ * (1 / b₁))

proof end;

theorem Th112: :: XCMPLX_1:112

for b₁, b₂ being complex number st b₁ <> 0 & b₂ <> 0 holds
1 / (b₁ * b₂) <> 0

proof end;

theorem Th113: :: XCMPLX_1:113

for b₁, b₂ being complex number st b₁ <> 0 & b₂ <> 0 holds
(b₁ / b₂) * (b₂ / b₁) = 1

proof end;

theorem Th114: :: XCMPLX_1:114

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
(b₂ / b₁) + b₃ = (b₂ + (b₁ * b₃)) / b₁

proof end;

theorem Th115: :: XCMPLX_1:115

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ + b₃ = b₁ * ((b₂ / b₁) + (b₃ / b₁))

proof end;

theorem Th116: :: XCMPLX_1:116

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ + b₃ = ((b₂ * b₁) + (b₃ * b₁)) / b₁

proof end;

theorem Th117: :: XCMPLX_1:117

for b₁, b₂, b₃, b₄ being complex number st b₁ <> 0 & b₂ <> 0 holds
(b₃ / b₁) + (b₄ / b₂) = ((b₃ * b₂) + (b₄ * b₁)) / (b₁ * b₂)

proof end;

theorem Th118: :: XCMPLX_1:118

for b₁, b₂ being complex number st b₁ <> 0 holds
b₁ + b₂ = b₁ * (1 + (b₂ / b₁))

proof end;

theorem Th119: :: XCMPLX_1:119

for b₁, b₂ being complex number holds (b₁ / (2 * b₂)) + (b₁ / (2 * b₂)) = b₁ / b₂

proof end;

theorem Th120: :: XCMPLX_1:120

for b₁, b₂ being complex number holds ((b₁ / (3 * b₂)) + (b₁ / (3 * b₂))) + (b₁ / (3 * b₂)) = b₁ / b₂

proof end;

Lemma37: for b₁, b₂ being complex number holds - (b₁ / b₂) = (- b₁) / b₂

proof end;

theorem Th121: :: XCMPLX_1:121

for b₁, b₂, b₃ being complex number holds (b₁ / b₂) - (b₃ / b₂) = (b₁ - b₃) / b₂

proof end;

theorem Th122: :: XCMPLX_1:122

for b₁ being complex number holds b₁ - (b₁ / 2) = b₁ / 2 ;

theorem Th123: :: XCMPLX_1:123

for b₁, b₂, b₃, b₄ being complex number holds ((b₁ - b₂) - b₃) / b₄ = ((b₁ / b₄) - (b₂ / b₄)) - (b₃ / b₄)

proof end;

theorem Th124: :: XCMPLX_1:124

for b₁, b₂, b₃, b₄ being complex number st b₁ <> 0 & b₂ <> 0 & b₁ <> b₂ & b₃ / b₁ = b₄ / b₂ holds
b₃ / b₁ = (b₃ - b₄) / (b₁ - b₂)

proof end;

theorem Th125: :: XCMPLX_1:125

for b₁, b₂, b₃, b₄ being complex number holds ((b₁ + b₂) - b₃) / b₄ = ((b₁ / b₄) + (b₂ / b₄)) - (b₃ / b₄)

proof end;

theorem Th126: :: XCMPLX_1:126

for b₁, b₂, b₃, b₄ being complex number holds ((b₁ - b₂) + b₃) / b₄ = ((b₁ / b₄) - (b₂ / b₄)) + (b₃ / b₄)

proof end;

theorem Th127: :: XCMPLX_1:127

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
(b₂ / b₁) - b₃ = (b₂ - (b₃ * b₁)) / b₁

proof end;

theorem Th128: :: XCMPLX_1:128

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ - (b₃ / b₁) = ((b₂ * b₁) - b₃) / b₁

proof end;

theorem Th129: :: XCMPLX_1:129

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ - b₃ = b₁ * ((b₂ / b₁) - (b₃ / b₁))

proof end;

theorem Th130: :: XCMPLX_1:130

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ - b₃ = ((b₂ * b₁) - (b₃ * b₁)) / b₁

proof end;

theorem Th131: :: XCMPLX_1:131

for b₁, b₂, b₃, b₄ being complex number st b₁ <> 0 & b₂ <> 0 holds
(b₃ / b₁) - (b₄ / b₂) = ((b₃ * b₂) - (b₄ * b₁)) / (b₁ * b₂)

proof end;

theorem Th132: :: XCMPLX_1:132

for b₁, b₂ being complex number st b₁ <> 0 holds
b₁ - b₂ = b₁ * (1 - (b₂ / b₁))

proof end;

theorem Th133: :: XCMPLX_1:133

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
b₂ = (((b₁ * b₂) + b₃) - b₃) / b₁ by Lemma15;

theorem Th134: :: XCMPLX_1:134

for b₁, b₂ being complex number st - b₁ = - b₂ holds
b₁ = b₂ ;

theorem Th135: :: XCMPLX_1:135

for b₁ being complex number st - b₁ = 0 holds
b₁ = 0 ;

theorem Th136: :: XCMPLX_1:136

for b₁, b₂ being complex number st b₁ + (- b₂) = 0 holds
b₁ = b₂ ;

theorem Th137: :: XCMPLX_1:137

for b₁, b₂ being complex number holds b₁ = (b₁ + b₂) + (- b₂) ;

theorem Th138: :: XCMPLX_1:138

for b₁, b₂ being complex number holds b₁ = b₁ + (b₂ + (- b₂)) ;

theorem Th139: :: XCMPLX_1:139

for b₁, b₂ being complex number holds b₁ = ((- b₂) + b₁) + b₂ ;

theorem Th140: :: XCMPLX_1:140

for b₁, b₂ being complex number holds - (b₁ + b₂) = (- b₁) + (- b₂) ;

theorem Th141: :: XCMPLX_1:141

for b₁, b₂ being complex number holds - ((- b₁) + b₂) = b₁ + (- b₂) ;

theorem Th142: :: XCMPLX_1:142

for b₁, b₂ being complex number holds b₁ + b₂ = - ((- b₁) + (- b₂)) ;

theorem Th143: :: XCMPLX_1:143

for b₁, b₂ being complex number holds - (b₁ - b₂) = b₂ - b₁ ;

theorem Th144: :: XCMPLX_1:144

for b₁, b₂ being complex number holds (- b₁) - b₂ = (- b₂) - b₁ ;

theorem Th145: :: XCMPLX_1:145

for b₁, b₂ being complex number holds b₁ = (- b₂) - ((- b₁) - b₂) ;

theorem Th146: :: XCMPLX_1:146

for b₁, b₂, b₃ being complex number holds ((- b₁) - b₂) - b₃ = ((- b₁) - b₃) - b₂ ;

theorem Th147: :: XCMPLX_1:147

for b₁, b₂, b₃ being complex number holds ((- b₁) - b₂) - b₃ = ((- b₂) - b₃) - b₁ ;

theorem Th148: :: XCMPLX_1:148

for b₁, b₂, b₃ being complex number holds ((- b₁) - b₂) - b₃ = ((- b₃) - b₂) - b₁ ;

theorem Th149: :: XCMPLX_1:149

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) - (b₁ - b₃) = - (b₂ - b₃) ;

theorem Th150: :: XCMPLX_1:150

for b₁ being complex number holds 0 - b₁ = - b₁ ;

theorem Th151: :: XCMPLX_1:151

for b₁, b₂ being complex number holds b₁ + b₂ = b₁ - (- b₂) ;

theorem Th152: :: XCMPLX_1:152

for b₁, b₂ being complex number holds b₁ = b₁ - (b₂ + (- b₂)) ;

theorem Th153: :: XCMPLX_1:153

for b₁, b₂, b₃ being complex number st b₁ - b₂ = b₃ + (- b₂) holds
b₁ = b₃ ;

theorem Th154: :: XCMPLX_1:154

for b₁, b₂, b₃ being complex number st b₁ - b₂ = b₁ + (- b₃) holds
b₂ = b₃ ;

theorem Th155: :: XCMPLX_1:155

for b₁, b₂, b₃ being complex number holds (b₁ + b₂) - b₃ = ((- b₃) + b₁) + b₂ ;

theorem Th156: :: XCMPLX_1:156

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) + b₃ = ((- b₂) + b₃) + b₁ ;

theorem Th157: :: XCMPLX_1:157

for b₁, b₂, b₃ being complex number holds b₁ - ((- b₂) - b₃) = (b₁ + b₂) + b₃ ;

theorem Th158: :: XCMPLX_1:158

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) - b₃ = ((- b₂) - b₃) + b₁ ;

theorem Th159: :: XCMPLX_1:159

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) - b₃ = ((- b₃) + b₁) - b₂ ;

theorem Th160: :: XCMPLX_1:160

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) - b₃ = ((- b₃) - b₂) + b₁ ;

theorem Th161: :: XCMPLX_1:161

for b₁, b₂ being complex number holds - (b₁ + b₂) = (- b₂) - b₁ ;

theorem Th162: :: XCMPLX_1:162

for b₁, b₂ being complex number holds - (b₁ - b₂) = (- b₁) + b₂ ;

theorem Th163: :: XCMPLX_1:163

for b₁, b₂ being complex number holds - ((- b₁) + b₂) = b₁ - b₂ ;

theorem Th164: :: XCMPLX_1:164

for b₁, b₂ being complex number holds b₁ + b₂ = - ((- b₁) - b₂) ;

theorem Th165: :: XCMPLX_1:165

for b₁, b₂, b₃ being complex number holds ((- b₁) + b₂) - b₃ = ((- b₃) + b₂) - b₁ ;

theorem Th166: :: XCMPLX_1:166

for b₁, b₂, b₃ being complex number holds ((- b₁) + b₂) - b₃ = ((- b₃) - b₁) + b₂ ;

theorem Th167: :: XCMPLX_1:167

for b₁, b₂, b₃ being complex number holds - ((b₁ + b₂) + b₃) = ((- b₁) - b₂) - b₃ ;

theorem Th168: :: XCMPLX_1:168

for b₁, b₂, b₃ being complex number holds - ((b₁ + b₂) - b₃) = ((- b₁) - b₂) + b₃ ;

theorem Th169: :: XCMPLX_1:169

for b₁, b₂, b₃ being complex number holds - ((b₁ - b₂) + b₃) = ((- b₁) + b₂) - b₃ ;

theorem Th170: :: XCMPLX_1:170

for b₁, b₂, b₃ being complex number holds - ((b₁ - b₂) - b₃) = ((- b₁) + b₂) + b₃ ;

theorem Th171: :: XCMPLX_1:171

for b₁, b₂, b₃ being complex number holds - (((- b₁) + b₂) + b₃) = (b₁ - b₂) - b₃ ;

theorem Th172: :: XCMPLX_1:172

for b₁, b₂, b₃ being complex number holds - (((- b₁) + b₂) - b₃) = (b₁ - b₂) + b₃ ;

theorem Th173: :: XCMPLX_1:173

for b₁, b₂, b₃ being complex number holds - (((- b₁) - b₂) + b₃) = (b₁ + b₂) - b₃ ;

theorem Th174: :: XCMPLX_1:174

for b₁, b₂, b₃ being complex number holds - (((- b₁) - b₂) - b₃) = (b₁ + b₂) + b₃ ;

theorem Th175: :: XCMPLX_1:175

for b₁, b₂ being complex number holds (- b₁) * b₂ = - (b₁ * b₂) ;

theorem Th176: :: XCMPLX_1:176

for b₁, b₂ being complex number holds (- b₁) * b₂ = b₁ * (- b₂) ;

theorem Th177: :: XCMPLX_1:177

for b₁, b₂ being complex number holds (- b₁) * (- b₂) = b₁ * b₂ ;

theorem Th178: :: XCMPLX_1:178

for b₁, b₂ being complex number holds - (b₁ * (- b₂)) = b₁ * b₂ ;

theorem Th179: :: XCMPLX_1:179

for b₁, b₂ being complex number holds - ((- b₁) * b₂) = b₁ * b₂ ;

theorem Th180: :: XCMPLX_1:180

for b₁ being complex number holds (- 1) * b₁ = - b₁ ;

theorem Th181: :: XCMPLX_1:181

for b₁ being complex number holds (- b₁) * (- 1) = b₁ ;

theorem Th182: :: XCMPLX_1:182

for b₁, b₂ being complex number st b₁ <> 0 & b₂ * b₁ = - b₁ holds
b₂ = - 1

proof end;

theorem Th183: :: XCMPLX_1:183

for b₁ being complex number holds
( not b₁ * b₁ = 1 or b₁ = 1 or b₁ = - 1 )

proof end;

theorem Th184: :: XCMPLX_1:184

for b₁ being complex number holds (- b₁) + (2 * b₁) = b₁ ;

theorem Th185: :: XCMPLX_1:185

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) * b₃ = (b₂ - b₁) * (- b₃) ;

theorem Th186: :: XCMPLX_1:186

for b₁, b₂, b₃ being complex number holds (b₁ - b₂) * b₃ = - ((b₂ - b₁) * b₃) ;

theorem Th187: :: XCMPLX_1:187

for b₁ being complex number holds b₁ - (2 * b₁) = - b₁ ;

theorem Th188: :: XCMPLX_1:188

for b₁, b₂ being complex number holds - (b₁ / b₂) = (- b₁) / b₂ by Lemma37;

theorem Th189: :: XCMPLX_1:189

for b₁, b₂ being complex number holds b₁ / (- b₂) = - (b₁ / b₂)

proof end;

theorem Th190: :: XCMPLX_1:190

for b₁, b₂ being complex number holds - (b₁ / (- b₂)) = b₁ / b₂

proof end;

theorem Th191: :: XCMPLX_1:191

for b₁, b₂ being complex number holds - ((- b₁) / b₂) = b₁ / b₂

proof end;

theorem Th192: :: XCMPLX_1:192

for b₁, b₂ being complex number holds (- b₁) / (- b₂) = b₁ / b₂

proof end;

theorem Th193: :: XCMPLX_1:193

for b₁, b₂ being complex number holds (- b₁) / b₂ = b₁ / (- b₂)

proof end;

theorem Th194: :: XCMPLX_1:194

for b₁ being complex number holds - b₁ = b₁ / (- 1)

proof end;

theorem Th195: :: XCMPLX_1:195

for b₁ being complex number holds b₁ = (- b₁) / (- 1)

proof end;

theorem Th196: :: XCMPLX_1:196

for b₁, b₂ being complex number st b₁ / b₂ = - 1 holds
( b₁ = - b₂ & b₂ = - b₁ )

proof end;

theorem Th197: :: XCMPLX_1:197

for b₁, b₂ being complex number st b₁ <> 0 & b₁ / b₂ = - b₁ holds
b₂ = - 1

proof end;

theorem Th198: :: XCMPLX_1:198

for b₁ being complex number st b₁ <> 0 holds
(- b₁) / b₁ = - 1

proof end;

theorem Th199: :: XCMPLX_1:199

for b₁ being complex number st b₁ <> 0 holds
b₁ / (- b₁) = - 1

proof end;

Lemma44: for b₁ being complex number st b₁ <> 0 & b₁ = b₁ " & not b₁ = 1 holds
b₁ = - 1

proof end;

theorem Th200: :: XCMPLX_1:200

for b₁ being complex number st b₁ <> 0 & b₁ = 1 / b₁ & not b₁ = 1 holds
b₁ = - 1

proof end;

theorem Th201: :: XCMPLX_1:201

for b₁, b₂, b₃, b₄ being complex number st b₁ <> 0 & b₂ <> 0 & b₁ <> - b₂ & b₃ / b₁ = b₄ / b₂ holds
b₃ / b₁ = (b₃ + b₄) / (b₁ + b₂)

proof end;

theorem Th202: :: XCMPLX_1:202

for b₁, b₂ being complex number st b₁ " = b₂ " holds
b₁ = b₂ by Lemma19;

theorem Th203: :: XCMPLX_1:203

0 " = 0 ;

theorem Th204: :: XCMPLX_1:204

for b₁, b₂ being complex number st b₁ <> 0 holds
b₂ = (b₂ * b₁) * (b₁ " )

proof end;

theorem Th205: :: XCMPLX_1:205

for b₁, b₂ being complex number holds (b₁ " ) * (b₂ " ) = (b₁ * b₂) " by Lemma4;

theorem Th206: :: XCMPLX_1:206

for b₁, b₂ being complex number holds (b₁ * (b₂ " )) " = (b₁ " ) * b₂ by Lemma17;

theorem Th207: :: XCMPLX_1:207

for b₁, b₂ being complex number holds ((b₁ " ) * (b₂ " )) " = b₁ * b₂

proof end;

theorem Th208: :: XCMPLX_1:208

for b₁, b₂ being complex number st b₁ <> 0 & b₂ <> 0 holds
b₁ * (b₂ " ) <> 0

proof end;

theorem Th209: :: XCMPLX_1:209

for b₁, b₂ being complex number st b₁ <> 0 & b₂ <> 0 holds
(b₁ " ) * (b₂ " ) <> 0

proof end;

theorem Th210: :: XCMPLX_1:210

for b₁, b₂ being complex number st b₁ * (b₂ " ) = 1 holds
b₁ = b₂

proof end;

theorem Th211: :: XCMPLX_1:211

for b₁, b₂ being complex number st b₁ * b₂ = 1 holds
b₁ = b₂ "

proof end;

theorem Th212: :: XCMPLX_1:212

canceled;

theorem Th213: :: XCMPLX_1:213

for b₁, b₂ being complex number st b₁ <> 0 & b₂ <> 0 holds
(b₁ " ) + (b₂ " ) = (b₁ + b₂) * ((b₁ * b₂) " )

proof end;

Lemma47: for b₁ being complex number holds (- b₁) " = - (b₁ " )

proof end;

theorem Th214: :: XCMPLX_1:214

for b₁, b₂ being complex number st b₁ <> 0 & b₂ <> 0 holds
(b₁ " ) - (b₂ " ) = (b₂ - b₁) * ((b₁ * b₂) " )

proof end;

theorem Th215: :: XCMPLX_1:215

for b₁, b₂ being complex number holds (b₁ / b₂) " = b₂ / b₁ by Lemma13;

theorem Th216: :: XCMPLX_1:216

for b₁, b₂ being complex number holds (b₁ " ) / (b₂ " ) = b₂ / b₁

proof end;

theorem Th217: :: XCMPLX_1:217

for b₁ being complex number holds 1 / b₁ = b₁ " by Lemma7;

theorem Th218: :: XCMPLX_1:218

for b₁ being complex number holds 1 / (b₁ " ) = b₁ by Lemma30;

theorem Th219: :: XCMPLX_1:219

for b₁ being complex number holds (1 / b₁) " = b₁

proof end;

theorem Th220: :: XCMPLX_1:220

for b₁, b₂ being complex number st 1 / b₁ = b₂ " holds
b₁ = b₂

proof end;

theorem Th221: :: XCMPLX_1:221

for b₁, b₂ being complex number holds b₁ / (b₂ " ) = b₁ * b₂

proof end;

theorem Th222: :: XCMPLX_1:222

for b₁, b₂, b₃ being complex number holds (b₁ " ) * (b₂ / b₃) = b₂ / (b₁ * b₃)

proof end;

theorem Th223: :: XCMPLX_1:223

for b₁, b₂ being complex number holds (b₁ " ) / b₂ = (b₁ * b₂) "

proof end;

theorem Th224: :: XCMPLX_1:224

for b₁ being complex number holds (- b₁) " = - (b₁ " ) by Lemma47;

theorem Th225: :: XCMPLX_1:225

for b₁ being complex number st b₁ <> 0 & b₁ = b₁ " & not b₁ = 1 holds
b₁ = - 1 by Lemma44;

theorem Th226: :: XCMPLX_1:226

for b₁, b₂, b₃ being complex number holds ((b₁ + b₂) + b₃) - b₂ = b₁ + b₃ ;

theorem Th227: :: XCMPLX_1:227

for b₁, b₂, b₃ being complex number holds ((b₁ - b₂) + b₃) + b₂ = b₁ + b₃ ;

theorem Th228: :: XCMPLX_1:228

for b₁, b₂, b₃ being complex number holds ((b₁ + b₂) - b₃) - b₂ = b₁ - b₃ ;

theorem Th229: :: XCMPLX_1:229

for b₁, b₂, b₃ being complex number holds ((b₁ - b₂) - b₃) + b₂ = b₁ - b₃ ;

theorem Th230: :: XCMPLX_1:230

for b₁, b₂ being complex number holds (b₁ - b₁) - b₂ = - b₂ ;

theorem Th231: :: XCMPLX_1:231

for b₁, b₂ being complex number holds ((- b₁) + b₁) - b₂ = - b₂ ;

theorem Th232: :: XCMPLX_1:232

for b₁, b₂ being complex number holds (b₁ - b₂) - b₁ = - b₂ ;

theorem Th233: :: XCMPLX_1:233

for b₁, b₂ being complex number holds ((- b₁) - b₂) + b₁ = - b₂ ;

theorem Th234: :: XCMPLX_1:234

for b₁, b₂ being complex number st b₂ <> 0 holds
ex b₃ being complex number st b₁ = b₂ / b₃

proof end;

theorem Th235: :: XCMPLX_1:235

for b₁, b₂, b₃, b₄, b₅ being complex number holds b₁ / ((b₂ * b₃) * (b₄ / b₅)) = (b₅ / b₃) * (b₁ / (b₂ * b₄))

proof end;

theorem Th236: :: XCMPLX_1:236

for b₁, b₂, b₃, b₄ being complex number holds (((b₁ - b₂) / b₃) * b₄) + b₂ = ((1 - (b₄ / b₃)) * b₂) + ((b₄ / b₃) * b₁)

proof end;

theorem Th237: :: XCMPLX_1:237

for b₁, b₂, b₃ being complex number st b₁ <> 0 holds
(b₁ * b₂) + b₃ = b₁ * (b₂ + (b₃ / b₁))

proof end;