:: The Complex Numbers
:: by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990-2011 Association of Mizar Users

begin

theorem :: COMPLEX1:1

canceled;

theorem Th2: :: COMPLEX1:2

for a, b being real number st (a ^2) + (b ^2) = 0 holds
a = 0

proof end;

Lm1: for a, b being real number holds 0 <= (a ^2) + (b ^2)

proof end;

definition

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

proof end;

uniqueness
for b₁, b₂ being set holds
( ( z in REAL & b₁ = z & b₂ = z implies b₁ = b₂ ) & ( not z in REAL & ex f being Function of 2,REAL st
( z = f & b₁ = f . 0 ) & ex f being Function of 2,REAL st
( z = f & b₂ = f . 0 ) implies b₁ = b₂ ) ) ;
consistency
for b₁ being set holds verum ;
func Im z -> set means :Def3: :: COMPLEX1:def 3
it = 0 if z in REAL
otherwise ex f being Function of 2,REAL st
( z = f & it = f . 1 );
existence
( ( z in REAL implies ex b₁ being set st b₁ = 0 ) & ( not z in REAL implies ex b₁ being set ex f being Function of 2,REAL st
( z = f & b₁ = f . 1 ) ) )

proof end;

uniqueness
for b₁, b₂ being set holds
( ( z in REAL & b₁ = 0 & b₂ = 0 implies b₁ = b₂ ) & ( not z in REAL & ex f being Function of 2,REAL st
( z = f & b₁ = f . 1 ) & ex f being Function of 2,REAL st
( z = f & b₂ = f . 1 ) implies b₁ = b₂ ) ) ;
consistency
for b₁ being set holds verum ;

end;

:: deftheorem COMPLEX1:def 1 :
canceled;

:: deftheorem Def2 defines Re COMPLEX1:def 2 :
for z being complex number
for b₂ being set holds
( ( z in REAL implies ( b₂ = Re z iff b₂ = z ) ) & ( not z in REAL implies ( b₂ = Re z iff ex f being Function of 2,REAL st
( z = f & b₂ = f . 0 ) ) ) );

:: deftheorem Def3 defines Im COMPLEX1:def 3 :
for z being complex number
for b₂ being set holds
( ( z in REAL implies ( b₂ = Im z iff b₂ = 0 ) ) & ( not z in REAL implies ( b₂ = Im z iff ex f being Function of 2,REAL st
( z = f & b₂ = f . 1 ) ) ) );

registration

let z be complex number ;
cluster Re z -> real ;
coherence
Re z is real

proof end;

cluster Im z -> real ;
coherence
Im z is real

proof end;

end;

definition

let z be complex number ;
:: original: Re
redefine func Re z -> Real;
coherence
Re z is Real by XREAL_0:def 1;
:: original: Im
redefine func Im z -> Real;
coherence
Im z is Real by XREAL_0:def 1;

end;

theorem :: COMPLEX1:3

canceled;

theorem :: COMPLEX1:4

canceled;

theorem Th5: :: COMPLEX1:5

for f being Function of 2,REAL ex a, b being Element of REAL st f = (0,1) --> (a,b)

proof end;

Lm2: for a, b being Element of REAL holds
( Re [*a,b*] = a & Im [*a,b*] = b )

proof end;

Lm3: for z being complex number holds [*(Re z),(Im z)*] = z

proof end;

theorem :: COMPLEX1:6

canceled;

theorem :: COMPLEX1:7

canceled;

theorem :: COMPLEX1:8

canceled;

theorem Th9: :: COMPLEX1:9

for z1, z2 being complex number st Re z1 = Re z2 & Im z1 = Im z2 holds
z1 = z2

proof end;

definition

let z1, z2 be complex number ;
canceled;
redefine pred z1 = z2 means :: COMPLEX1:def 5
( Re z1 = Re z2 & Im z1 = Im z2 );
compatibility
( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) ) by Th9;

end;

:: deftheorem COMPLEX1:def 4 :
canceled;

:: deftheorem defines = COMPLEX1:def 5 :
for z1, z2 being complex number holds
( z1 = z2 iff ( Re z1 = Re z2 & Im z1 = Im z2 ) );

notation

synonym 0c for 0 ;

end;

definition

:: original: 0c
redefine func 0c -> Element of COMPLEX ;
correctness
coherence
0c is Element of COMPLEX ;
by XCMPLX_0:def 2;

end;

definition

canceled;
func 1r -> Element of COMPLEX equals :: COMPLEX1:def 7
1;
correctness
coherence
1 is Element of COMPLEX ;
by XCMPLX_0:def 2;
:: original: <i>
redefine func <i> -> Element of COMPLEX ;
coherence
<i> is Element of COMPLEX by XCMPLX_0:def 2;

end;

:: deftheorem COMPLEX1:def 6 :
canceled;

:: deftheorem defines 1r COMPLEX1:def 7 :
1r = 1;

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

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

theorem :: COMPLEX1:10

canceled;

theorem :: COMPLEX1:11

canceled;

theorem Th12: :: COMPLEX1:12

( Re 0 = 0 & Im 0 = 0 ) by Lm2, Lm4;

theorem Th13: :: COMPLEX1:13

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

proof end;

theorem :: COMPLEX1:14

canceled;

theorem Th15: :: COMPLEX1:15

( Re 1r = 1 & Im 1r = 0 ) by Lm2, Lm5;

theorem :: COMPLEX1:16

canceled;

Lm6: <i> = [*0,1*]
by ARYTM_0:def 7, XCMPLX_0:def 1;

theorem Th17: :: COMPLEX1:17

( Re <i> = 0 & Im <i> = 1 ) by Lm2, Lm6;

Lm7: for x being real number
for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )

proof end;

Lm8: for x9, y9 being Element of REAL
for x, y being real number st x9 = x & y9 = y holds
+ (x9,y9) = x + y

proof end;

Lm9: for x being Element of REAL holds opp x = - x

proof end;

Lm10: for x9, y9 being Element of REAL
for x, y being real number st x9 = x & y9 = y holds
* (x9,y9) = x * y

proof end;

Lm11: for x, y, z being complex number st z = x + y holds
Re z = (Re x) + (Re y)

proof end;

Lm12: for x, y, z being complex number st z = x + y holds
Im z = (Im x) + (Im y)

proof end;

Lm13: for x, y, z being complex number st z = x * y holds
Re z = ((Re x) * (Re y)) - ((Im x) * (Im y))

proof end;

Lm14: for x, y, z being complex number st z = x * y holds
Im z = ((Re x) * (Im y)) + ((Im x) * (Re y))

proof end;

Lm15: for z1, z2 being complex number holds z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*]

proof end;

Lm16: for z1, z2 being complex number holds z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*]

proof end;

Lm17: for z1, z2 being complex number holds
( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )

proof end;

Lm18: for z1, z2 being complex number holds
( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )

proof end;

Lm19: for x being Real holds Re (x * <i>) = 0

proof end;

Lm20: for x being Real holds Im (x * <i>) = x

proof end;

Lm21: for x, y being Real holds [*x,y*] = x + (y * <i>)

proof end;

definition

canceled;
let z1, z2 be Element of COMPLEX ;
:: original: +
redefine func z1 + z2 -> Element of COMPLEX equals :: COMPLEX1:def 9
((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>);
coherence
z1 + z2 is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b₁ being Element of COMPLEX holds
( b₁ = z1 + z2 iff b₁ = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>) )

proof end;

end;

:: deftheorem COMPLEX1:def 8 :
canceled;

:: deftheorem defines + COMPLEX1:def 9 :
for z1, z2 being Element of COMPLEX holds z1 + z2 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>);

theorem :: COMPLEX1:18

canceled;

theorem Th19: :: COMPLEX1:19

for z1, z2 being complex number holds
( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )

proof end;

definition

let z1, z2 be Element of COMPLEX ;
:: original: *
redefine func z1 * z2 -> Element of COMPLEX equals :: COMPLEX1:def 10
(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>);
coherence
z1 * z2 is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b₁ being Element of COMPLEX holds
( b₁ = z1 * z2 iff b₁ = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>) )

proof end;

end;

:: deftheorem defines * COMPLEX1:def 10 :
for z1, z2 being Element of COMPLEX holds z1 * z2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>);

theorem :: COMPLEX1:20

canceled;

theorem :: COMPLEX1:21

canceled;

theorem :: COMPLEX1:22

canceled;

theorem :: COMPLEX1:23

canceled;

theorem Th24: :: COMPLEX1:24

for z1, z2 being complex number holds
( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )

proof end;

theorem :: COMPLEX1:25

for a being real number holds Re (a * <i>) = 0

proof end;

theorem :: COMPLEX1:26

for a being real number holds Im (a * <i>) = a

proof end;

theorem :: COMPLEX1:27

canceled;

theorem Th28: :: COMPLEX1:28

for a, b being real number holds
( Re (a + (b * <i>)) = a & Im (a + (b * <i>)) = b )

proof end;

theorem Th29: :: COMPLEX1:29

for z being complex number holds (Re z) + ((Im z) * <i>) = z

proof end;

theorem Th30: :: COMPLEX1:30

for z1, z2 being complex number st Im z1 = 0 & Im z2 = 0 holds
( Re (z1 * z2) = (Re z1) * (Re z2) & Im (z1 * z2) = 0 )

proof end;

theorem Th31: :: COMPLEX1:31

for z1, z2 being complex number st Re z1 = 0 & Re z2 = 0 holds
( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 )

proof end;

theorem :: COMPLEX1:32

for z being complex number holds
( Re (z * z) = ((Re z) ^2) - ((Im z) ^2) & Im (z * z) = 2 * ((Re z) * (Im z)) )

proof end;

definition

let z be Element of COMPLEX ;
:: original: -
redefine func - z -> Element of COMPLEX equals :Def11: :: COMPLEX1:def 11
(- (Re z)) + ((- (Im z)) * <i>);
coherence
- z is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b₁ being Element of COMPLEX holds
( b₁ = - z iff b₁ = (- (Re z)) + ((- (Im z)) * <i>) )

proof end;

end;

:: deftheorem Def11 defines - COMPLEX1:def 11 :
for z being Element of COMPLEX holds - z = (- (Re z)) + ((- (Im z)) * <i>);

theorem :: COMPLEX1:33

canceled;

theorem Th34: :: COMPLEX1:34

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

proof end;

theorem :: COMPLEX1:35

canceled;

theorem :: COMPLEX1:36

canceled;

theorem :: COMPLEX1:37

<i> * <i> = - 1r ;

definition

let z1, z2 be Element of COMPLEX ;
:: original: -
redefine func z1 - z2 -> Element of COMPLEX equals :Def12: :: COMPLEX1:def 12
((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>);
coherence
z1 - z2 is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b₁ being Element of COMPLEX holds
( b₁ = z1 - z2 iff b₁ = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) )

proof end;

end;

:: deftheorem Def12 defines - COMPLEX1:def 12 :
for z1, z2 being Element of COMPLEX holds z1 - z2 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>);

theorem :: COMPLEX1:38

canceled;

theorem :: COMPLEX1:39

canceled;

theorem :: COMPLEX1:40

canceled;

theorem :: COMPLEX1:41

canceled;

theorem :: COMPLEX1:42

canceled;

theorem :: COMPLEX1:43

canceled;

theorem :: COMPLEX1:44

canceled;

theorem :: COMPLEX1:45

canceled;

theorem :: COMPLEX1:46

canceled;

theorem :: COMPLEX1:47

canceled;

theorem Th48: :: COMPLEX1:48

for z1, z2 being complex number holds
( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) )

proof end;

definition

let z be Element of COMPLEX ;
:: original: "
redefine func z " -> Element of COMPLEX equals :Def13: :: COMPLEX1:def 13
((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>);
coherence
z " is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b₁ being Element of COMPLEX holds
( b₁ = z " iff b₁ = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) )

proof end;

end;

:: deftheorem Def13 defines " COMPLEX1:def 13 :
for z being Element of COMPLEX holds z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>);

theorem :: COMPLEX1:49

canceled;

theorem :: COMPLEX1:50

canceled;

theorem :: COMPLEX1:51

canceled;

theorem :: COMPLEX1:52

canceled;

theorem :: COMPLEX1:53

canceled;

theorem :: COMPLEX1:54

canceled;

theorem :: COMPLEX1:55

canceled;

theorem :: COMPLEX1:56

canceled;

theorem :: COMPLEX1:57

canceled;

theorem :: COMPLEX1:58

canceled;

theorem :: COMPLEX1:59

canceled;

theorem :: COMPLEX1:60

canceled;

theorem :: COMPLEX1:61

canceled;

theorem :: COMPLEX1:62

canceled;

theorem :: COMPLEX1:63

canceled;

theorem Th64: :: COMPLEX1:64

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

proof end;

theorem :: COMPLEX1:65

canceled;

theorem :: COMPLEX1:66

canceled;

theorem :: COMPLEX1:67

canceled;

theorem :: COMPLEX1:68

canceled;

theorem :: COMPLEX1:69

canceled;

theorem :: COMPLEX1:70

canceled;

theorem :: COMPLEX1:71

canceled;

theorem :: COMPLEX1:72

<i> " = - <i> ;

theorem :: COMPLEX1:73

canceled;

theorem :: COMPLEX1:74

canceled;

theorem :: COMPLEX1:75

canceled;

theorem :: COMPLEX1:76

canceled;

theorem :: COMPLEX1:77

canceled;

theorem :: COMPLEX1:78

canceled;

theorem Th79: :: COMPLEX1:79

for z being complex number st Re z <> 0 & Im z = 0 holds
( Re (z ") = (Re z) " & Im (z ") = 0 )

proof end;

theorem Th80: :: COMPLEX1:80

for z being complex number st Re z = 0 & Im z <> 0 holds
( Re (z ") = 0 & Im (z ") = - ((Im z) ") )

proof end;

definition

let z1, z2 be complex number ;
:: original: /
redefine func z1 / z2 -> Element of COMPLEX equals :Def14: :: COMPLEX1:def 14
((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>);
coherence
z1 / z2 is Element of COMPLEX by XCMPLX_0:def 2;
compatibility
for b₁ being Element of COMPLEX holds
( b₁ = z1 / z2 iff b₁ = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>) )

proof end;

end;

:: deftheorem Def14 defines / COMPLEX1:def 14 :
for z1, z2 being complex number holds z1 / z2 = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>);

theorem :: COMPLEX1:81

canceled;

theorem :: COMPLEX1:82

for z1, z2 being complex number holds
( Re (z1 / z2) = (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) & Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) )

proof end;

theorem :: COMPLEX1:83

canceled;

theorem :: COMPLEX1:84

canceled;

theorem :: COMPLEX1:85

canceled;

theorem :: COMPLEX1:86

canceled;

theorem :: COMPLEX1:87

canceled;

theorem :: COMPLEX1:88

canceled;

theorem :: COMPLEX1:89

canceled;

theorem :: COMPLEX1:90

canceled;

theorem :: COMPLEX1:91

canceled;

theorem :: COMPLEX1:92

canceled;

theorem :: COMPLEX1:93

canceled;

theorem :: COMPLEX1:94

canceled;

theorem :: COMPLEX1:95

canceled;

theorem :: COMPLEX1:96

canceled;

theorem :: COMPLEX1:97

canceled;

theorem :: COMPLEX1:98

canceled;

theorem :: COMPLEX1:99

canceled;

theorem :: COMPLEX1:100

canceled;

theorem :: COMPLEX1:101

canceled;

theorem :: COMPLEX1:102

canceled;

theorem :: COMPLEX1:103

canceled;

theorem :: COMPLEX1:104

canceled;

theorem :: COMPLEX1:105

canceled;

theorem :: COMPLEX1:106

canceled;

theorem :: COMPLEX1:107

canceled;

theorem :: COMPLEX1:108

canceled;

theorem :: COMPLEX1:109

for z1, z2 being complex number st Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 holds
( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 )

proof end;

theorem :: COMPLEX1:110

for z1, z2 being complex number st Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 holds
( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 )

proof end;

definition

let z be complex number ;
func z *' -> complex number equals :: COMPLEX1:def 15
(Re z) - ((Im z) * <i>);
correctness
coherence
(Re z) - ((Im z) * <i>) is complex number ;
;
involutiveness
for b₁, b₂ being complex number st b₁ = (Re b₂) - ((Im b₂) * <i>) holds
b₂ = (Re b₁) - ((Im b₁) * <i>)

proof end;

end;

:: deftheorem defines *' COMPLEX1:def 15 :
for z being complex number holds z *' = (Re z) - ((Im z) * <i>);

definition

let z be complex number ;
:: original: *'
redefine func z *' -> Element of COMPLEX ;
coherence
z *' is Element of COMPLEX by XCMPLX_0:def 2;

end;

theorem :: COMPLEX1:111

canceled;

theorem Th112: :: COMPLEX1:112

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

proof end;

theorem :: COMPLEX1:113

0 *' = 0 by Th12;

theorem :: COMPLEX1:114

for z being complex number st z *' = 0 holds
z = 0

proof end;

theorem :: COMPLEX1:115

1r *' = 1r by Th15;

theorem :: COMPLEX1:116

<i> *' = - <i> by Th17;

theorem :: COMPLEX1:117

canceled;

theorem Th118: :: COMPLEX1:118

for z1, z2 being complex number holds (z1 + z2) *' = (z1 *') + (z2 *')

proof end;

theorem Th119: :: COMPLEX1:119

for z being complex number holds (- z) *' = - (z *')

proof end;

theorem :: COMPLEX1:120

for z1, z2 being complex number holds (z1 - z2) *' = (z1 *') - (z2 *')

proof end;

theorem Th121: :: COMPLEX1:121

for z1, z2 being complex number holds (z1 * z2) *' = (z1 *') * (z2 *')

proof end;

theorem Th122: :: COMPLEX1:122

for z being complex number holds (z ") *' = (z *') "

proof end;

theorem :: COMPLEX1:123

for z1, z2 being complex number holds (z1 / z2) *' = (z1 *') / (z2 *')

proof end;

theorem :: COMPLEX1:124

for z being complex number st Im z = 0 holds
z *' = z

proof end;

theorem :: COMPLEX1:125

for z being complex number st Re z = 0 holds
z *' = - z

proof end;

theorem :: COMPLEX1:126

for z being complex number holds
( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 )

proof end;

theorem :: COMPLEX1:127

for z being complex number holds
( Re (z + (z *')) = 2 * (Re z) & Im (z + (z *')) = 0 )

proof end;

theorem :: COMPLEX1:128

for z being complex number holds
( Re (z - (z *')) = 0 & Im (z - (z *')) = 2 * (Im z) )

proof end;

definition

let z be complex number ;
func |.z.| -> real number equals :: COMPLEX1:def 16
sqrt (((Re z) ^2) + ((Im z) ^2));
coherence
sqrt (((Re z) ^2) + ((Im z) ^2)) is real number ;
projectivity
for b₁, b₂ being real number st b₁ = sqrt (((Re b₂) ^2) + ((Im b₂) ^2)) holds
b₁ = sqrt (((Re b₁) ^2) + ((Im b₁) ^2))

proof end;

end;

:: deftheorem defines |. COMPLEX1:def 16 :
for z being complex number holds |.z.| = sqrt (((Re z) ^2) + ((Im z) ^2));

definition

let z be complex number ;
:: original: |.
redefine func |.z.| -> Real;
coherence
|.z.| is Real ;

end;

theorem Th129: :: COMPLEX1:129

for a being real number st a >= 0 holds
|.a.| = a

proof end;

registration

cluster |.0.| -> zero real ;
coherence
|.0.| is zero by Th12, SQUARE_1:82;

end;

theorem :: COMPLEX1:130

|.0.| = 0 ;

registration

let z be non zero complex number ;
cluster |.z.| -> non zero real ;
coherence
not |.z.| is zero

proof end;

end;

theorem :: COMPLEX1:131

for z being complex number st |.z.| = 0 holds
z = 0 ;

registration

let z be complex number ;
cluster |.z.| -> real non negative ;
coherence
not |.z.| is negative

proof end;

end;

theorem :: COMPLEX1:132

for z being complex number holds 0 <= |.z.| ;

theorem :: COMPLEX1:133

for z being complex number holds
( z <> 0 iff 0 < |.z.| ) ;

theorem Th134: :: COMPLEX1:134

|.1r.| = 1 by Th15, SQUARE_1:83;

theorem :: COMPLEX1:135

|.<i>.| = 1 by Th17, SQUARE_1:83;

Lm22: for z being complex number holds |.(- z).| = |.z.|

proof end;

Lm23: for a being real number st a <= 0 holds
|.a.| = - a

proof end;

Lm24: for a being real number holds sqrt (a ^2) = |.a.|

proof end;

theorem :: COMPLEX1:136

for z being complex number st Im z = 0 holds
|.z.| = |.(Re z).| by Lm24;

theorem :: COMPLEX1:137

for z being complex number st Re z = 0 holds
|.z.| = |.(Im z).| by Lm24;

theorem :: COMPLEX1:138

for z being complex number holds |.(- z).| = |.z.| by Lm22;

theorem Th139: :: COMPLEX1:139

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

proof end;

Lm25: for a being real number holds
( - |.a.| <= a & a <= |.a.| )

proof end;

theorem :: COMPLEX1:140

for z being complex number holds Re z <= |.z.|

proof end;

theorem :: COMPLEX1:141

for z being complex number holds Im z <= |.z.|

proof end;

theorem Th142: :: COMPLEX1:142

for z1, z2 being complex number holds |.(z1 + z2).| <= |.z1.| + |.z2.|

proof end;

theorem Th143: :: COMPLEX1:143

for z1, z2 being complex number holds |.(z1 - z2).| <= |.z1.| + |.z2.|

proof end;

theorem :: COMPLEX1:144

for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 + z2).|

proof end;

theorem Th145: :: COMPLEX1:145

for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 - z2).|

proof end;

theorem Th146: :: COMPLEX1:146

for z1, z2 being complex number holds |.(z1 - z2).| = |.(z2 - z1).|

proof end;

theorem Th147: :: COMPLEX1:147

for z1, z2 being complex number holds
( |.(z1 - z2).| = 0 iff z1 = z2 )

proof end;

theorem :: COMPLEX1:148

for z1, z2 being complex number holds
( z1 <> z2 iff 0 < |.(z1 - z2).| )

proof end;

theorem :: COMPLEX1:149

for z1, z2, z being complex number holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|

proof end;

Lm26: for b, a being real number holds
( ( - b <= a & a <= b ) iff |.a.| <= b )

proof end;

theorem :: COMPLEX1:150

for z1, z2 being complex number holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|

proof end;

theorem Th151: :: COMPLEX1:151

for z1, z2 being complex number holds |.(z1 * z2).| = |.z1.| * |.z2.|

proof end;

theorem Th152: :: COMPLEX1:152

for z being complex number holds |.(z ").| = |.z.| "

proof end;

theorem Th153: :: COMPLEX1:153

for z1, z2 being complex number holds |.z1.| / |.z2.| = |.(z1 / z2).|

proof end;

theorem :: COMPLEX1:154

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

proof end;

theorem :: COMPLEX1:155

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

proof end;

theorem :: COMPLEX1:156

for a being real number st a <= 0 holds
|.a.| = - a by Lm23;

theorem Th157: :: COMPLEX1:157

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

proof end;

theorem :: COMPLEX1:158

for a being real number holds sqrt (a ^2) = |.a.| by Lm24;

theorem :: COMPLEX1:159

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

proof end;

theorem :: COMPLEX1:160

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

proof end;

theorem Th161: :: COMPLEX1:161

for a being real number holds |.a.| ^2 = a ^2

proof end;

theorem :: COMPLEX1:162

for a being real number holds
( - |.a.| <= a & a <= |.a.| ) by Lm25;

notation

let z be complex number ;
synonym abs z for |.z.|;

end;

definition

let z be complex number ;
:: original: |.
redefine func abs z -> Real;
coherence
|.z.| is Real ;

end;

theorem :: COMPLEX1:163

for a, b, c, d being real number st a + (b * <i>) = c + (d * <i>) holds
( a = c & b = d )

proof end;

theorem :: COMPLEX1:164

for a, b being real number holds sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b)

proof end;

theorem :: COMPLEX1:165

for a, b being real number holds abs a <= sqrt ((a ^2) + (b ^2))

proof end;

theorem :: COMPLEX1:166

for z1 being complex number holds |.(1 / z1).| = 1 / |.z1.| by Th134, Th153;