:: COMPLEX1 semantic presentation

E1: one = succ 0 by ORDINAL2:def 4
.= 1 ;

E2: 2 = succ 1
.= (succ 0) \/ {1} by ORDINAL1:def 1
.= ({} \/ {0}) \/ {1} by ORDINAL1:def 1
.= {0,one } by Lemma1, ENUMSET1:41 ;

theorem Th1: :: COMPLEX1:1

canceled;

theorem Th2: :: COMPLEX1:2

for b₁, b₂ being real number holds
( (b₁ ^2 ) + (b₂ ^2 ) = 0 iff ( b₁ = 0 & b₂ = 0 ) )

proof end;

Lemma4: for b₁, b₂ being Element of REAL holds 0 <= (b₁ ^2 ) + (b₂ ^2 )

proof end;

registration

cluster -> complex Element of COMPLEX ;
coherence ;

end;

definition

let c₁ be complex number ;
canceled;
func Re c₁ -> set means :Def2: :: COMPLEX1:def 2
a₂ = a₁ if a₁ in REAL
otherwise ex b₁ being Function of 2, REAL st
( a₁ = b₁ & a₂ = b₁ . 0 );
existence

proof end;

uniqueness ;
consistency ;
func Im c₁ -> set means :Def3: :: COMPLEX1:def 3
a₂ = 0 if a₁ in REAL
otherwise ex b₁ being Function of 2, REAL st
( a₁ = b₁ & a₂ = b₁ . 1 );
existence

proof end;

uniqueness ;
consistency ;

end;

:: deftheorem Def1 COMPLEX1:def 1 :

:: deftheorem Def2 defines Re COMPLEX1:def 2 :

:: deftheorem Def3 defines Im COMPLEX1:def 3 :

registration

let c₁ be complex number ;
cluster Re a₁ -> real ;
coherence

proof end;

cluster Im a₁ -> real ;
coherence

proof end;

end;

definition

let c₁ be complex number ;
redefine func Re as Re c₁ -> Real;
coherence by XREAL_0:def 1;
redefine func Im as Im c₁ -> Real;
coherence by XREAL_0:def 1;

end;

theorem Th3: :: COMPLEX1:3

canceled;

theorem Th4: :: COMPLEX1:4

canceled;

theorem Th5: :: COMPLEX1:5

for b₁ being Function of 2, REAL ex b₂, b₃ being Element of REAL st b₁ = 0,1 --> b₂,b₃

proof end;

Lemma8: for b₁, b₂ being Element of REAL holds
( Re [*b₁,b₂*] = b₁ & Im [*b₁,b₂*] = b₂ )

proof end;

Lemma9: for b₁ being complex number holds [*(Re b₁),(Im b₁)*] = b₁

proof end;

theorem Th6: :: COMPLEX1:6

canceled;

theorem Th7: :: COMPLEX1:7

canceled;

theorem Th8: :: COMPLEX1:8

canceled;

theorem Th9: :: COMPLEX1:9

for b₁, b₂ being complex number st Re b₁ = Re b₂ & Im b₁ = Im b₂ holds
b₁ = b₂

proof end;

definition

let c₁, c₂ be complex number ;
canceled;
redefine pred c₁ = c₂ means :: COMPLEX1:def 5
( Re a₁ = Re a₂ & Im a₁ = Im a₂ );
compatibility by Th9;

end;

:: deftheorem Def4 COMPLEX1:def 4 :

:: deftheorem Def5 defines = COMPLEX1:def 5 :

definition

func 0c -> Element of COMPLEX equals :: COMPLEX1:def 6
0;
correctness by XCMPLX_0:def 2;
func 1r -> Element of COMPLEX equals :: COMPLEX1:def 7
1;
correctness by XCMPLX_0:def 2;
redefine func as -> Element of COMPLEX equals :: COMPLEX1:def 8
[*0,1*];
coherence by XCMPLX_0:def 2;
compatibility by Lemma1, ARYTM_0:def 7, XCMPLX_0:def 1;

end;

:: deftheorem Def6 defines 0c COMPLEX1:def 6 :

:: deftheorem Def7 defines 1r COMPLEX1:def 7 :

:: deftheorem Def8 defines COMPLEX1:def 8 :

Lemma11: 0 = [*0,0*]
by ARYTM_0:def 7;

Lemma12: 1r = [*1,0*]
by ARYTM_0:def 7;

registration

cluster 0c -> zero complex ;
coherence ;

end;

theorem Th10: :: COMPLEX1:10

canceled;

theorem Th11: :: COMPLEX1:11

canceled;

theorem Th12: :: COMPLEX1:12

( Re 0 = 0 & Im 0 = 0 ) by Lemma11, Lemma8;

theorem Th13: :: COMPLEX1:13

for b₁ being complex number holds
( b₁ = 0 iff ((Re b₁) ^2 ) + ((Im b₁) ^2 ) = 0 )

proof end;

theorem Th14: :: COMPLEX1:14

canceled;

theorem Th15: :: COMPLEX1:15

( Re 1r = 1 & Im 1r = 0 ) by Lemma12, Lemma8;

theorem Th16: :: COMPLEX1:16

canceled;

theorem Th17: :: COMPLEX1:17

( Re = 0 & Im = 1 ) by Lemma8;

Lemma17: for b₁ being real number
for b₂, b₃ being Element of REAL st b₁ = [*b₂,b₃*] holds
( b₃ = 0 & b₁ = b₂ )

proof end;

Lemma18: for b₁, b₂ being Element of REAL
for b₃, b₄ being real number st b₁ = b₃ & b₂ = b₄ holds
+ b₁,b₂ = b₃ + b₄

proof end;

Lemma19: for b₁ being Element of REAL holds opp b₁ = - b₁

proof end;

Lemma20: for b₁, b₂ being Element of REAL
for b₃, b₄ being real number st b₁ = b₃ & b₂ = b₄ holds
* b₁,b₂ = b₃ * b₄

proof end;

Lemma21: for b₁, b₂, b₃ being Element of COMPLEX st b₃ = b₁ + b₂ holds
Re b₃ = (Re b₁) + (Re b₂)

proof end;

Lemma22: for b₁, b₂, b₃ being Element of COMPLEX st b₃ = b₁ + b₂ holds
Im b₃ = (Im b₁) + (Im b₂)

proof end;

Lemma23: for b₁, b₂, b₃ being Element of COMPLEX st b₃ = b₁ * b₂ holds
Re b₃ = ((Re b₁) * (Re b₂)) - ((Im b₁) * (Im b₂))

proof end;

Lemma24: for b₁, b₂, b₃ being Element of COMPLEX st b₃ = b₁ * b₂ holds
Im b₃ = ((Re b₁) * (Im b₂)) + ((Im b₁) * (Re b₂))

proof end;

Lemma25: for b₁, b₂ being Element of COMPLEX holds b₁ + b₂ = [*((Re b₁) + (Re b₂)),((Im b₁) + (Im b₂))*]

proof end;

Lemma26: for b₁, b₂ being Element of COMPLEX holds b₁ * b₂ = [*(((Re b₁) * (Re b₂)) - ((Im b₁) * (Im b₂))),(((Re b₁) * (Im b₂)) + ((Re b₂) * (Im b₁)))*]

proof end;

Lemma27: for b₁, b₂ being complex number holds
( Re (b₁ * b₂) = ((Re b₁) * (Re b₂)) - ((Im b₁) * (Im b₂)) & Im (b₁ * b₂) = ((Re b₁) * (Im b₂)) + ((Re b₂) * (Im b₁)) )

proof end;

Lemma28: for b₁, b₂ being complex number holds
( Re (b₁ + b₂) = (Re b₁) + (Re b₂) & Im (b₁ + b₂) = (Im b₁) + (Im b₂) )

proof end;

Lemma29: for b₁ being Real holds Re (b₁ * ) = 0

proof end;

Lemma30: for b₁ being Real holds Im (b₁ * ) = b₁

proof end;

Lemma31: for b₁, b₂ being Real holds [*b₁,b₂*] = b₁ + (b₂ * )

proof end;

definition

let c₁, c₂ be Element of COMPLEX ;
redefine func + as c₁ + c₂ -> Element of COMPLEX equals :: COMPLEX1:def 9
((Re a₁) + (Re a₂)) + (((Im a₁) + (Im a₂)) * );
coherence by XCMPLX_0:def 2;
compatibility

proof end;

end;

:: deftheorem Def9 defines + COMPLEX1:def 9 :

theorem Th18: :: COMPLEX1:18

canceled;

theorem Th19: :: COMPLEX1:19

for b₁, b₂ being complex number holds
( Re (b₁ + b₂) = (Re b₁) + (Re b₂) & Im (b₁ + b₂) = (Im b₁) + (Im b₂) )

proof end;

definition

let c₁, c₂ be Element of COMPLEX ;
redefine func * as c₁ * c₂ -> Element of COMPLEX equals :: COMPLEX1:def 10
(((Re a₁) * (Re a₂)) - ((Im a₁) * (Im a₂))) + ((((Re a₁) * (Im a₂)) + ((Re a₂) * (Im a₁))) * );
coherence by XCMPLX_0:def 2;
compatibility

proof end;

end;

:: deftheorem Def10 defines * COMPLEX1:def 10 :

theorem Th20: :: COMPLEX1:20

canceled;

theorem Th21: :: COMPLEX1:21

canceled;

theorem Th22: :: COMPLEX1:22

canceled;

theorem Th23: :: COMPLEX1:23

canceled;

theorem Th24: :: COMPLEX1:24

for b₁, b₂ being complex number holds
( Re (b₁ * b₂) = ((Re b₁) * (Re b₂)) - ((Im b₁) * (Im b₂)) & Im (b₁ * b₂) = ((Re b₁) * (Im b₂)) + ((Re b₂) * (Im b₁)) )

proof end;

theorem Th25: :: COMPLEX1:25

for b₁ being Real holds Re (b₁ * ) = 0

proof end;

theorem Th26: :: COMPLEX1:26

for b₁ being Real holds Im (b₁ * ) = b₁

proof end;

theorem Th27: :: COMPLEX1:27

for b₁, b₂ being Real holds [*b₁,b₂*] = b₁ + (b₂ * )

proof end;

theorem Th28: :: COMPLEX1:28

for b₁, b₂ being Element of REAL holds
( Re (b₁ + (b₂ * )) = b₁ & Im (b₁ + (b₂ * )) = b₂ )

proof end;

theorem Th29: :: COMPLEX1:29

for b₁ being complex number holds (Re b₁) + ((Im b₁) * ) = b₁

proof end;

theorem Th30: :: COMPLEX1:30

for b₁, b₂ being complex number st Im b₁ = 0 & Im b₂ = 0 holds
( Re (b₁ * b₂) = (Re b₁) * (Re b₂) & Im (b₁ * b₂) = 0 )

proof end;

theorem Th31: :: COMPLEX1:31

for b₁, b₂ being complex number st Re b₁ = 0 & Re b₂ = 0 holds
( Re (b₁ * b₂) = - ((Im b₁) * (Im b₂)) & Im (b₁ * b₂) = 0 )

proof end;

theorem Th32: :: COMPLEX1:32

for b₁ being Element of COMPLEX holds
( Re (b₁ * b₁) = ((Re b₁) ^2 ) - ((Im b₁) ^2 ) & Im (b₁ * b₁) = 2 * ((Re b₁) * (Im b₁)) ) by Th24;

definition

let c₁ be Element of COMPLEX ;
redefine func - as - c₁ -> Element of COMPLEX equals :Def11: :: COMPLEX1:def 11
(- (Re a₁)) + ((- (Im a₁)) * );
coherence by XCMPLX_0:def 2;
compatibility

proof end;

end;

:: deftheorem Def11 defines - COMPLEX1:def 11 :

theorem Th33: :: COMPLEX1:33

canceled;

theorem Th34: :: COMPLEX1:34

for b₁ being complex number holds
( Re (- b₁) = - (Re b₁) & Im (- b₁) = - (Im b₁) )

proof end;

- = 0 + ((- 1) * )
;

then Lemma42: ( Re (- ) = 0 & Im (- ) = - 1 )
by Th28;

theorem Th35: :: COMPLEX1:35

canceled;

theorem Th36: :: COMPLEX1:36

canceled;

theorem Th37: :: COMPLEX1:37

* = - 1r ;

definition

let c₁, c₂ be Element of COMPLEX ;
redefine func - as c₁ - c₂ -> Element of COMPLEX equals :: COMPLEX1:def 12
((Re a₁) - (Re a₂)) + (((Im a₁) - (Im a₂)) * );
coherence by XCMPLX_0:def 2;
compatibility

proof end;

end;

:: deftheorem Def12 defines - COMPLEX1:def 12 :

theorem Th38: :: COMPLEX1:38

canceled;

theorem Th39: :: COMPLEX1:39

canceled;

theorem Th40: :: COMPLEX1:40

canceled;

theorem Th41: :: COMPLEX1:41

canceled;

theorem Th42: :: COMPLEX1:42

canceled;

theorem Th43: :: COMPLEX1:43

canceled;

theorem Th44: :: COMPLEX1:44

canceled;

theorem Th45: :: COMPLEX1:45

canceled;

theorem Th46: :: COMPLEX1:46

canceled;

theorem Th47: :: COMPLEX1:47

canceled;

theorem Th48: :: COMPLEX1:48

for b₁, b₂ being Element of COMPLEX holds
( Re (b₁ - b₂) = (Re b₁) - (Re b₂) & Im (b₁ - b₂) = (Im b₁) - (Im b₂) ) by Th28;

definition

let c₁ be Element of COMPLEX ;
redefine func " as c₁ " -> Element of COMPLEX equals :Def13: :: COMPLEX1:def 13
((Re a₁) / (((Re a₁) ^2 ) + ((Im a₁) ^2 ))) + (((- (Im a₁)) / (((Re a₁) ^2 ) + ((Im a₁) ^2 ))) * );
coherence by XCMPLX_0:def 2;
compatibility

proof end;

end;

:: deftheorem Def13 defines " COMPLEX1:def 13 :

theorem Th49: :: COMPLEX1:49

canceled;

theorem Th50: :: COMPLEX1:50

canceled;

theorem Th51: :: COMPLEX1:51

canceled;

theorem Th52: :: COMPLEX1:52

canceled;

theorem Th53: :: COMPLEX1:53

canceled;

theorem Th54: :: COMPLEX1:54

canceled;

theorem Th55: :: COMPLEX1:55

canceled;

theorem Th56: :: COMPLEX1:56

canceled;

theorem Th57: :: COMPLEX1:57

canceled;

theorem Th58: :: COMPLEX1:58

canceled;

theorem Th59: :: COMPLEX1:59

canceled;

theorem Th60: :: COMPLEX1:60

canceled;

theorem Th61: :: COMPLEX1:61

canceled;

theorem Th62: :: COMPLEX1:62

canceled;

theorem Th63: :: COMPLEX1:63

canceled;

theorem Th64: :: COMPLEX1:64

for b₁ being complex number holds
( Re (b₁ " ) = (Re b₁) / (((Re b₁) ^2 ) + ((Im b₁) ^2 )) & Im (b₁ " ) = (- (Im b₁)) / (((Re b₁) ^2 ) + ((Im b₁) ^2 )) )

proof end;

theorem Th65: :: COMPLEX1:65

canceled;

theorem Th66: :: COMPLEX1:66

canceled;

theorem Th67: :: COMPLEX1:67

canceled;

theorem Th68: :: COMPLEX1:68

canceled;

theorem Th69: :: COMPLEX1:69

canceled;

theorem Th70: :: COMPLEX1:70

canceled;

theorem Th71: :: COMPLEX1:71

canceled;

theorem Th72: :: COMPLEX1:72

" = - ;

theorem Th73: :: COMPLEX1:73

canceled;

theorem Th74: :: COMPLEX1:74

canceled;

theorem Th75: :: COMPLEX1:75

canceled;

theorem Th76: :: COMPLEX1:76

canceled;

theorem Th77: :: COMPLEX1:77

canceled;

theorem Th78: :: COMPLEX1:78

canceled;

theorem Th79: :: COMPLEX1:79

for b₁ being Element of COMPLEX st Re b₁ <> 0 & Im b₁ = 0 holds
( Re (b₁ " ) = (Re b₁) " & Im (b₁ " ) = 0 )

proof end;

theorem Th80: :: COMPLEX1:80

for b₁ being Element of COMPLEX st Re b₁ = 0 & Im b₁ <> 0 holds
( Re (b₁ " ) = 0 & Im (b₁ " ) = - ((Im b₁) " ) )

proof end;

definition

let c₁, c₂ be Element of COMPLEX ;
redefine func / as c₁ / c₂ -> Element of COMPLEX equals :: COMPLEX1:def 14
((((Re a₁) * (Re a₂)) + ((Im a₁) * (Im a₂))) / (((Re a₂) ^2 ) + ((Im a₂) ^2 ))) + (((((Re a₂) * (Im a₁)) - ((Re a₁) * (Im a₂))) / (((Re a₂) ^2 ) + ((Im a₂) ^2 ))) * );
coherence by XCMPLX_0:def 2;
compatibility

proof end;

end;

:: deftheorem Def14 defines / COMPLEX1:def 14 :

theorem Th81: :: COMPLEX1:81

canceled;

theorem Th82: :: COMPLEX1:82

for b₁, b₂ being Element of COMPLEX holds
( Re (b₁ / b₂) = (((Re b₁) * (Re b₂)) + ((Im b₁) * (Im b₂))) / (((Re b₂) ^2 ) + ((Im b₂) ^2 )) & Im (b₁ / b₂) = (((Re b₂) * (Im b₁)) - ((Re b₁) * (Im b₂))) / (((Re b₂) ^2 ) + ((Im b₂) ^2 )) ) by Th28;

theorem Th83: :: COMPLEX1:83

canceled;

theorem Th84: :: COMPLEX1:84

canceled;

theorem Th85: :: COMPLEX1:85

canceled;

theorem Th86: :: COMPLEX1:86

canceled;

theorem Th87: :: COMPLEX1:87

canceled;

theorem Th88: :: COMPLEX1:88

canceled;

theorem Th89: :: COMPLEX1:89

canceled;

theorem Th90: :: COMPLEX1:90

canceled;

theorem Th91: :: COMPLEX1:91

canceled;

theorem Th92: :: COMPLEX1:92

canceled;

theorem Th93: :: COMPLEX1:93

canceled;

theorem Th94: :: COMPLEX1:94

canceled;

theorem Th95: :: COMPLEX1:95

canceled;

theorem Th96: :: COMPLEX1:96

canceled;

theorem Th97: :: COMPLEX1:97

canceled;

theorem Th98: :: COMPLEX1:98

canceled;

theorem Th99: :: COMPLEX1:99

canceled;

theorem Th100: :: COMPLEX1:100

canceled;

theorem Th101: :: COMPLEX1:101

canceled;

theorem Th102: :: COMPLEX1:102

canceled;

theorem Th103: :: COMPLEX1:103

canceled;

theorem Th104: :: COMPLEX1:104

canceled;

theorem Th105: :: COMPLEX1:105

canceled;

theorem Th106: :: COMPLEX1:106

canceled;

theorem Th107: :: COMPLEX1:107

canceled;

theorem Th108: :: COMPLEX1:108

canceled;

theorem Th109: :: COMPLEX1:109

for b₁, b₂ being Element of COMPLEX st Im b₁ = 0 & Im b₂ = 0 & Re b₂ <> 0 holds
( Re (b₁ / b₂) = (Re b₁) / (Re b₂) & Im (b₁ / b₂) = 0 )

proof end;

theorem Th110: :: COMPLEX1:110

for b₁, b₂ being Element of COMPLEX st Re b₁ = 0 & Re b₂ = 0 & Im b₂ <> 0 holds
( Re (b₁ / b₂) = (Im b₁) / (Im b₂) & Im (b₁ / b₂) = 0 )

proof end;

definition

let c₁ be complex number ;
func c₁ *' -> complex number equals :: COMPLEX1:def 15
(Re a₁) - ((Im a₁) * );
correctness ;
involutiveness

proof end;

end;

:: deftheorem Def15 defines *' COMPLEX1:def 15 :

definition

let c₁ be complex number ;
redefine func *' as c₁ *' -> Element of COMPLEX ;
coherence by XCMPLX_0:def 2;

end;

theorem Th111: :: COMPLEX1:111

canceled;

theorem Th112: :: COMPLEX1:112

for b₁ being complex number holds
( Re (b₁ *' ) = Re b₁ & Im (b₁ *' ) = - (Im b₁) )

proof end;

theorem Th113: :: COMPLEX1:113

0 *' = 0 by Th12;

theorem Th114: :: COMPLEX1:114

for b₁ being complex number st b₁ *' = 0 holds
b₁ = 0

proof end;

theorem Th115: :: COMPLEX1:115

1r *' = 1r by Th15;

Lemma49: ( Re ( *' ) = 0 & Im ( *' ) = - 1 )
by Th17, Th112;

theorem Th116: :: COMPLEX1:116

*' = - by Lemma42, Lemma49, Th9;

theorem Th117: :: COMPLEX1:117

canceled;

theorem Th118: :: COMPLEX1:118

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

proof end;

theorem Th119: :: COMPLEX1:119

for b₁ being Element of COMPLEX holds (- b₁) *' = - (b₁ *' )

proof end;

theorem Th120: :: COMPLEX1:120

for b₁, b₂ being Element of COMPLEX holds (b₁ - b₂) *' = (b₁ *' ) - (b₂ *' )

proof end;

theorem Th121: :: COMPLEX1:121

for b₁, b₂ being Element of COMPLEX holds (b₁ * b₂) *' = (b₁ *' ) * (b₂ *' )

proof end;

theorem Th122: :: COMPLEX1:122

for b₁ being Element of COMPLEX holds (b₁ " ) *' = (b₁ *' ) "

proof end;

theorem Th123: :: COMPLEX1:123

for b₁, b₂ being Element of COMPLEX holds (b₁ / b₂) *' = (b₁ *' ) / (b₂ *' )

proof end;

theorem Th124: :: COMPLEX1:124

for b₁ being Element of COMPLEX st Im b₁ = 0 holds
b₁ *' = b₁

proof end;

theorem Th125: :: COMPLEX1:125

for b₁ being Element of COMPLEX st Re b₁ = 0 holds
b₁ *' = - b₁ ;

theorem Th126: :: COMPLEX1:126

for b₁ being Element of COMPLEX holds
( Re (b₁ * (b₁ *' )) = ((Re b₁) ^2 ) + ((Im b₁) ^2 ) & Im (b₁ * (b₁ *' )) = 0 )

proof end;

theorem Th127: :: COMPLEX1:127

for b₁ being Element of COMPLEX holds
( Re (b₁ + (b₁ *' )) = 2 * (Re b₁) & Im (b₁ + (b₁ *' )) = 0 )

proof end;

theorem Th128: :: COMPLEX1:128

for b₁ being Element of COMPLEX holds
( Re (b₁ - (b₁ *' )) = 0 & Im (b₁ - (b₁ *' )) = 2 * (Im b₁) )

proof end;

definition

let c₁ be complex number ;
func |.c₁.| -> complex number equals :: COMPLEX1:def 16
sqrt (((Re a₁) ^2 ) + ((Im a₁) ^2 ));
coherence ;
projectivity

proof end;

end;

:: deftheorem Def16 defines |. COMPLEX1:def 16 :

registration

let c₁ be complex number ;
cluster |.a₁.| -> complex real ;
coherence ;

end;

definition

let c₁ be complex number ;
redefine func |. as |.c₁.| -> Real;
coherence ;

end;

Lemma54: sqrt ((0 ^2 ) + (0 ^2 )) = 0
by SQUARE_1:82;

theorem Th129: :: COMPLEX1:129

for b₁ being real number st b₁ >= 0 holds
|.b₁.| = b₁

proof end;

theorem Th130: :: COMPLEX1:130

|.0.| = 0 by Lemma54, Th12;

theorem Th131: :: COMPLEX1:131

for b₁ being complex number st |.b₁.| = 0 holds
b₁ = 0

proof end;

theorem Th132: :: COMPLEX1:132

for b₁ being complex number holds 0 <= |.b₁.|

proof end;

theorem Th133: :: COMPLEX1:133

for b₁ being complex number holds
( b₁ <> 0 iff 0 < |.b₁.| )

proof end;

Lemma59: sqrt ((1 ^2 ) + (0 ^2 )) = 1
by SQUARE_1:83;

theorem Th134: :: COMPLEX1:134

|.1r .| = 1 by Lemma59, Th15;

Lemma60: sqrt ((0 ^2 ) + (1 ^2 )) = 1
by SQUARE_1:83;

theorem Th135: :: COMPLEX1:135

|. .| = 1 by Lemma60, Th17;

Lemma61: for b₁ being complex number holds |.(- b₁).| = |.b₁.|

proof end;

Lemma62: for b₁ being real number st b₁ <= 0 holds
|.b₁.| = - b₁

proof end;

Lemma63: for b₁ being real number holds sqrt (b₁ ^2 ) = |.b₁.|

proof end;

theorem Th136: :: COMPLEX1:136

for b₁ being complex number st Im b₁ = 0 holds
|.b₁.| = |.(Re b₁).| by Lemma63;

theorem Th137: :: COMPLEX1:137

for b₁ being complex number st Re b₁ = 0 holds
|.b₁.| = |.(Im b₁).| by Lemma63;

theorem Th138: :: COMPLEX1:138

for b₁ being complex number holds |.(- b₁).| = |.b₁.| by Lemma61;

theorem Th139: :: COMPLEX1:139

for b₁ being complex number holds |.(b₁ *' ).| = |.b₁.|

proof end;

Lemma65: for b₁ being real number holds
( - |.b₁.| <= b₁ & b₁ <= |.b₁.| )

proof end;

theorem Th140: :: COMPLEX1:140

for b₁ being complex number holds Re b₁ <= |.b₁.|

proof end;

theorem Th141: :: COMPLEX1:141

for b₁ being complex number holds Im b₁ <= |.b₁.|

proof end;

theorem Th142: :: COMPLEX1:142

for b₁, b₂ being complex number holds |.(b₁ + b₂).| <= |.b₁.| + |.b₂.|

proof end;

theorem Th143: :: COMPLEX1:143

for b₁, b₂ being complex number holds |.(b₁ - b₂).| <= |.b₁.| + |.b₂.|

proof end;

theorem Th144: :: COMPLEX1:144

for b₁, b₂ being complex number holds |.b₁.| - |.b₂.| <= |.(b₁ + b₂).|

proof end;

theorem Th145: :: COMPLEX1:145

for b₁, b₂ being complex number holds |.b₁.| - |.b₂.| <= |.(b₁ - b₂).|

proof end;

theorem Th146: :: COMPLEX1:146

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

proof end;

theorem Th147: :: COMPLEX1:147

for b₁, b₂ being complex number holds
( |.(b₁ - b₂).| = 0 iff b₁ = b₂ )

proof end;

theorem Th148: :: COMPLEX1:148

for b₁, b₂ being complex number holds
( b₁ <> b₂ iff 0 < |.(b₁ - b₂).| )

proof end;

theorem Th149: :: COMPLEX1:149

for b₁, b₂, b₃ being complex number holds |.(b₂ - b₃).| <= |.(b₂ - b₁).| + |.(b₁ - b₃).|

proof end;

Lemma71: for b₁, b₂ being real number holds
( ( - b₂ <= b₁ & b₁ <= b₂ ) iff |.b₁.| <= b₂ )

proof end;

theorem Th150: :: COMPLEX1:150

for b₁, b₂ being complex number holds |.(|.b₁.| - |.b₂.|).| <= |.(b₁ - b₂).|

proof end;

theorem Th151: :: COMPLEX1:151

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

proof end;

theorem Th152: :: COMPLEX1:152

for b₁ being complex number holds |.(b₁ " ).| = |.b₁.| "

proof end;

theorem Th153: :: COMPLEX1:153

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

proof end;

theorem Th154: :: COMPLEX1:154

for b₁ being complex number holds |.(b₁ * b₁).| = ((Re b₁) ^2 ) + ((Im b₁) ^2 )

proof end;

theorem Th155: :: COMPLEX1:155

for b₁ being complex number holds |.(b₁ * b₁).| = |.(b₁ * (b₁ *' )).|

proof end;

theorem Th156: :: COMPLEX1:156

for b₁ being real number st b₁ <= 0 holds
|.b₁.| = - b₁ by Lemma62;

theorem Th157: :: COMPLEX1:157

for b₁ being real number holds
( |.b₁.| = b₁ or |.b₁.| = - b₁ )

proof end;

theorem Th158: :: COMPLEX1:158

for b₁ being real number holds sqrt (b₁ ^2 ) = |.b₁.| by Lemma63;

theorem Th159: :: COMPLEX1:159

for b₁, b₂ being real number holds min b₁,b₂ = ((b₁ + b₂) - |.(b₁ - b₂).|) / 2

proof end;

theorem Th160: :: COMPLEX1:160

for b₁, b₂ being real number holds max b₁,b₂ = ((b₁ + b₂) + |.(b₁ - b₂).|) / 2

proof end;

theorem Th161: :: COMPLEX1:161

for b₁ being real number holds |.b₁.| ^2 = b₁ ^2

proof end;

theorem Th162: :: COMPLEX1:162

for b₁ being real number holds
( - |.b₁.| <= b₁ & b₁ <= |.b₁.| ) by Lemma65;

notation

let c₁ be complex number ;
synonym absc₁.| for |.c₁.|;

end;

definition

let c₁ be complex number ;
redefine func |. as abs c₁ -> Real;
coherence ;

end;

theorem Th163: :: COMPLEX1:163

for b₁, b₂, b₃, b₄ being Element of REAL st b₁ + (b₂ * ) = b₃ + (b₄ * ) holds
( b₁ = b₃ & b₂ = b₄ )

proof end;