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


begin

:: Auxiliary theorems
theorem Th1: :: COMPLEX1:1
for a, b being real number st (a ^2) + (b ^2) = 0 holds
a = 0
proofend;

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

:: Complex Numbers
definition
let z be complex number ;
func Re z ->  set  means :Def1: :: COMPLEX1:def 1
it = z if z in REAL
otherwise  ex f being Function of 2,REAL st
( z = f &amp; it = f . 0 );
existence
 ( ( z in REAL implies ex b1 being set st b1 = z ) &amp; ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st
( z = f &amp; b1 = f . 0 ) ) )
proofend;
uniqueness
 for b1, b2 being set holds
( ( z in REAL &amp; b1 = z &amp; b2 = z implies b1 = b2 ) &amp; ( not z in REAL &amp; ex f being Function of 2,REAL st
( z = f &amp; b1 = f . 0 ) &amp; ex f being Function of 2,REAL st
( z = f &amp; b2 = f . 0 ) implies b1 = b2 ) ) ;
consistency
 for b1 being set holds verum ;
func Im z ->  set  means :Def2: :: COMPLEX1:def 2
it = 0  if z in REAL
otherwise  ex f being Function of 2,REAL st
( z = f &amp; it = f . 1 );
existence
 ( ( z in REAL implies ex b1 being set st b1 = 0 ) &amp; ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st
( z = f &amp; b1 = f . 1 ) ) )
proofend;
uniqueness
 for b1, b2 being set holds
( ( z in REAL &amp; b1 = 0 &amp; b2 = 0 implies b1 = b2 ) &amp; ( not z in REAL &amp; ex f being Function of 2,REAL st
( z = f &amp; b1 = f . 1 ) &amp; ex f being Function of 2,REAL st
( z = f &amp; b2 = f . 1 ) implies b1 = b2 ) ) ;
consistency
 for b1 being set holds verum ;
end;

:: deftheorem Def1 defines Re COMPLEX1:def_1_:_
 for z being complex number
for b2 being set holds
( ( z in REAL implies ( b2 = Re z iff b2 = z ) ) &amp; ( not z in REAL implies ( b2 = Re z iff ex f being Function of 2,REAL st
( z = f &amp; b2 = f . 0 ) ) ) );

:: deftheorem Def2 defines Im COMPLEX1:def_2_:_
 for z being complex number
for b2 being set holds
( ( z in REAL implies ( b2 = Im z iff b2 = 0 ) ) &amp; ( not z in REAL implies ( b2 = Im z iff ex f being Function of 2,REAL st
( z = f &amp; b2 = f . 1 ) ) ) );

registration
let z be complex number ;
cluster Re z ->  real ;
coherence
 Re z is real
proofend;
cluster Im z ->  real ;
coherence
 Im z is real
proofend;
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 Th2: :: COMPLEX1:2
for f being Function of 2,REAL ex a, b being Element of REAL st f = (0,1) --> (a,b)
proofend;

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

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

theorem Th3: :: COMPLEX1:3
for z1, z2 being complex number st Re z1 = Re z2 &amp; Im z1 = Im z2 holds
z1 = z2
proofend;

definition
let z1, z2 be complex number ;
redefine pred z1 = z2 means :: COMPLEX1:def 3
( Re z1 = Re z2 &amp; Im z1 = Im z2 );
compatibility
 ( z1 = z2 iff ( Re z1 = Re z2 &amp; Im z1 = Im z2 ) ) by Th3;
end;

:: deftheorem  defines = COMPLEX1:def_3_:_
 for z1, z2 being complex number holds
( z1 = z2 iff ( Re z1 = Re z2 &amp; 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
func 1r  ->  Element of COMPLEX  equals :: COMPLEX1:def 4
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  defines 1r COMPLEX1:def_4_:_
 1r = 1;

Lm4:  0 = [*0,0*]
by ARYTM_0:def_5;

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

theorem Th4: :: COMPLEX1:4
( Re 0 = 0 &amp; Im 0 = 0 ) by Lm2, Lm4;

theorem Th5: :: COMPLEX1:5
for z being complex number holds
( z = 0 iff ((Re z) ^2) + ((Im z) ^2) = 0 )
proofend;

theorem Th6: :: COMPLEX1:6
( Re 1r = 1 &amp; Im 1r = 0 ) by Lm2, Lm5;

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

theorem Th7: :: COMPLEX1:7
( Re <i> = 0 &amp; 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 &amp; x = x1 )
proofend;

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

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

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

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

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

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

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

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

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)))*]
proofend;

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

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

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

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

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

definition
let z1, z2 be Element of COMPLEX ;
:: original:+
redefine funcz1 + z2 ->  Element of COMPLEX  equals :: COMPLEX1:def 5
((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>);
coherence
 z1 + z2 is Element of COMPLEX by XCMPLX_0:def_2;
compatibility
 for b1 being Element of COMPLEX holds
( b1 = z1 + z2 iff b1 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>) )
proofend;
end;

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

theorem Th8: :: COMPLEX1:8
for z1, z2 being complex number holds
( Re (z1 + z2) = (Re z1) + (Re z2) &amp; Im (z1 + z2) = (Im z1) + (Im z2) )
proofend;

definition
let z1, z2 be Element of COMPLEX ;
:: original:*
redefine funcz1 * z2 ->  Element of COMPLEX  equals :: COMPLEX1:def 6
(((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 b1 being Element of COMPLEX holds
( b1 = z1 * z2 iff b1 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) * <i>) )
proofend;
end;

:: deftheorem  defines * COMPLEX1:def_6_:_
 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 Th9: :: COMPLEX1:9
for z1, z2 being complex number holds
( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) &amp; Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )
proofend;

theorem :: COMPLEX1:10
for a being real number holds Re (a * <i>) = 0
proofend;

theorem :: COMPLEX1:11
for a being real number holds Im (a * <i>) = a
proofend;

theorem Th12: :: COMPLEX1:12
for a, b being real number holds
( Re (a + (b * <i>)) = a &amp; Im (a + (b * <i>)) = b )
proofend;

theorem Th13: :: COMPLEX1:13
for z being complex number holds (Re z) + ((Im z) * <i>) = z
proofend;

theorem Th14: :: COMPLEX1:14
for z1, z2 being complex number st Im z1 = 0 &amp; Im z2 = 0 holds
( Re (z1 * z2) = (Re z1) * (Re z2) &amp; Im (z1 * z2) = 0 )
proofend;

theorem Th15: :: COMPLEX1:15
for z1, z2 being complex number st Re z1 = 0 &amp; Re z2 = 0 holds
( Re (z1 * z2) = - ((Im z1) * (Im z2)) &amp; Im (z1 * z2) = 0 )
proofend;

theorem :: COMPLEX1:16
for z being complex number holds
( Re (z * z) = ((Re z) ^2) - ((Im z) ^2) &amp; Im (z * z) = 2 * ((Re z) * (Im z)) )
proofend;

definition
let z be Element of COMPLEX ;
:: original:-
redefine func - z ->  Element of COMPLEX  equals :Def7: :: COMPLEX1:def 7
(- (Re z)) + ((- (Im z)) * <i>);
coherence
 - z is Element of COMPLEX by XCMPLX_0:def_2;
compatibility
 for b1 being Element of COMPLEX holds
( b1 = - z iff b1 = (- (Re z)) + ((- (Im z)) * <i>) )
proofend;
end;

:: deftheorem Def7 defines - COMPLEX1:def_7_:_
 for z being Element of COMPLEX holds - z = (- (Re z)) + ((- (Im z)) * <i>);

theorem Th17: :: COMPLEX1:17
for z being complex number holds
( Re (- z) = - (Re z) &amp; Im (- z) = - (Im z) )
proofend;

theorem :: COMPLEX1:18
<i> * <i> = - 1r ;

definition
let z1, z2 be Element of COMPLEX ;
:: original:-
redefine funcz1 - z2 ->  Element of COMPLEX  equals :Def8: :: COMPLEX1:def 8
((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>);
coherence
 z1 - z2 is Element of COMPLEX by XCMPLX_0:def_2;
compatibility
 for b1 being Element of COMPLEX holds
( b1 = z1 - z2 iff b1 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) )
proofend;
end;

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

theorem Th19: :: COMPLEX1:19
for z1, z2 being complex number holds
( Re (z1 - z2) = (Re z1) - (Re z2) &amp; Im (z1 - z2) = (Im z1) - (Im z2) )
proofend;

definition
let z be Element of COMPLEX ;
:: original:"
redefine funcz "  ->  Element of COMPLEX  equals :Def9: :: COMPLEX1:def 9
((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 b1 being Element of COMPLEX holds
( b1 = z " iff b1 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) )
proofend;
end;

:: deftheorem Def9 defines " COMPLEX1:def_9_:_
 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 Th20: :: COMPLEX1:20
for z being complex number holds
( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) &amp; Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) )
proofend;

theorem :: COMPLEX1:21
<i> " = - <i> ;

theorem Th22: :: COMPLEX1:22
for z being complex number st Re z <> 0 &amp; Im z = 0 holds
( Re (z ") = (Re z) " &amp; Im (z ") = 0 )
proofend;

theorem Th23: :: COMPLEX1:23
for z being complex number st Re z = 0 &amp; Im z <> 0 holds
( Re (z ") = 0 &amp; Im (z ") = - ((Im z) ") )
proofend;

definition
let z1, z2 be complex number ;
:: original:/
redefine funcz1 / z2 ->  Element of COMPLEX  equals :Def10: :: COMPLEX1:def 10
((((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 b1 being Element of COMPLEX holds
( b1 = z1 / z2 iff b1 = ((((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>) )
proofend;
end;

:: deftheorem Def10 defines / COMPLEX1:def_10_:_
 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:24
for z1, z2 being complex number holds
( Re (z1 / z2) = (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) &amp; Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) )
proofend;

theorem :: COMPLEX1:25
for z1, z2 being complex number st Im z1 = 0 &amp; Im z2 = 0 &amp; Re z2 <> 0 holds
( Re (z1 / z2) = (Re z1) / (Re z2) &amp; Im (z1 / z2) = 0 )
proofend;

theorem :: COMPLEX1:26
for z1, z2 being complex number st Re z1 = 0 &amp; Re z2 = 0 &amp; Im z2 <> 0 holds
( Re (z1 / z2) = (Im z1) / (Im z2) &amp; Im (z1 / z2) = 0 )
proofend;

definition
let z be complex number ;
funcz *'  ->  complex number  equals :: COMPLEX1:def 11
(Re z) - ((Im z) * <i>);
correctness
coherence
(Re z) - ((Im z) * <i>) is complex number ;
;
involutiveness
 for b1, b2 being complex number st b1 = (Re b2) - ((Im b2) * <i>) holds
b2 = (Re b1) - ((Im b1) * <i>)
proofend;
end;

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

definition
let z be complex number ;
:: original:*'
redefine funcz *'  ->  Element of COMPLEX ;
coherence
 z *' is Element of COMPLEX by XCMPLX_0:def_2;
end;

theorem Th27: :: COMPLEX1:27
for z being complex number holds
( Re (z *') = Re z &amp; Im (z *') = - (Im z) )
proofend;

theorem :: COMPLEX1:28
0 *' = 0 by Th4;

theorem :: COMPLEX1:29
for z being complex number st z *' = 0 holds
z = 0
proofend;

theorem :: COMPLEX1:30
1r *' = 1r by Th6;

theorem :: COMPLEX1:31
<i> *' = - <i> by Th7;

theorem Th32: :: COMPLEX1:32
for z1, z2 being complex number holds (z1 + z2) *' = (z1 *') + (z2 *')
proofend;

theorem Th33: :: COMPLEX1:33
for z being complex number holds (- z) *' = - (z *')
proofend;

theorem :: COMPLEX1:34
for z1, z2 being complex number holds (z1 - z2) *' = (z1 *') - (z2 *')
proofend;

theorem Th35: :: COMPLEX1:35
for z1, z2 being complex number holds (z1 * z2) *' = (z1 *') * (z2 *')
proofend;

theorem Th36: :: COMPLEX1:36
for z being complex number holds (z ") *' = (z *') "
proofend;

theorem :: COMPLEX1:37
for z1, z2 being complex number holds (z1 / z2) *' = (z1 *') / (z2 *')
proofend;

theorem :: COMPLEX1:38
for z being complex number st Im z = 0 holds
z *' = z
proofend;

theorem :: COMPLEX1:39
for z being complex number st Re z = 0 holds
z *' = - z
proofend;

theorem :: COMPLEX1:40
for z being complex number holds
( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) &amp; Im (z * (z *')) = 0 )
proofend;

theorem :: COMPLEX1:41
for z being complex number holds
( Re (z + (z *')) = 2 * (Re z) &amp; Im (z + (z *')) = 0 )
proofend;

theorem :: COMPLEX1:42
for z being complex number holds
( Re (z - (z *')) = 0 &amp; Im (z - (z *')) = 2 * (Im z) )
proofend;

definition
let z be complex number ;
func|.z.| ->  real number  equals :: COMPLEX1:def 12
 sqrt (((Re z) ^2) + ((Im z) ^2));
coherence
 sqrt (((Re z) ^2) + ((Im z) ^2)) is real number ;
projectivity
 for b1 being real number
for b2 being complex number st b1 = sqrt (((Re b2) ^2) + ((Im b2) ^2)) holds
b1 = sqrt (((Re b1) ^2) + ((Im b1) ^2))
proofend;
end;

:: deftheorem  defines |. COMPLEX1:def_12_:_
 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 Th43: :: COMPLEX1:43
for a being real number st a >= 0 holds
|.a.| = a
proofend;

registration
cluster|.0.| ->  zero real ;
coherence
 |.0.| is zero by Th4, SQUARE_1:17;
end;

theorem :: COMPLEX1:44
|.0.| = 0 ;

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

theorem :: COMPLEX1:45
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
proofend;
end;

theorem :: COMPLEX1:46
for z being complex number holds 0 <= |.z.| ;

theorem :: COMPLEX1:47
for z being complex number holds
( z <> 0 iff 0 < |.z.| ) ;

theorem Th48: :: COMPLEX1:48
|.1r.| = 1 by Th6, SQUARE_1:18;

theorem :: COMPLEX1:49
|.<i>.| = 1 by Th7, SQUARE_1:18;

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

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

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

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

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

theorem :: COMPLEX1:52
for z being complex number holds |.(- z).| = |.z.| by Lm22;

theorem Th53: :: COMPLEX1:53
for z being complex number holds |.(z *').| = |.z.|
proofend;

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

theorem :: COMPLEX1:54
for z being complex number holds Re z <= |.z.|
proofend;

theorem :: COMPLEX1:55
for z being complex number holds Im z <= |.z.|
proofend;

theorem Th56: :: COMPLEX1:56
for z1, z2 being complex number holds |.(z1 + z2).| <= |.z1.| + |.z2.|
proofend;

theorem Th57: :: COMPLEX1:57
for z1, z2 being complex number holds |.(z1 - z2).| <= |.z1.| + |.z2.|
proofend;

theorem :: COMPLEX1:58
for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 + z2).|
proofend;

theorem Th59: :: COMPLEX1:59
for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 - z2).|
proofend;

theorem Th60: :: COMPLEX1:60
for z1, z2 being complex number holds |.(z1 - z2).| = |.(z2 - z1).|
proofend;

theorem Th61: :: COMPLEX1:61
for z1, z2 being complex number holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
proofend;

theorem :: COMPLEX1:62
for z1, z2 being complex number holds
( z1 <> z2 iff 0 < |.(z1 - z2).| )
proofend;

theorem :: COMPLEX1:63
for z1, z2, z being complex number holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
proofend;

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

theorem :: COMPLEX1:64
for z1, z2 being complex number holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
proofend;

theorem Th65: :: COMPLEX1:65
for z1, z2 being complex number holds |.(z1 * z2).| = |.z1.| * |.z2.|
proofend;

theorem Th66: :: COMPLEX1:66
for z being complex number holds |.(z ").| = |.z.| "
proofend;

theorem Th67: :: COMPLEX1:67
for z1, z2 being complex number holds |.z1.| / |.z2.| = |.(z1 / z2).|
proofend;

theorem :: COMPLEX1:68
for z being complex number holds |.(z * z).| = ((Re z) ^2) + ((Im z) ^2)
proofend;

theorem :: COMPLEX1:69
for z being complex number holds |.(z * z).| = |.(z * (z *')).|
proofend;

:: Originally from SQUARE_1
theorem :: COMPLEX1:70
for a being real number st a <= 0 holds
|.a.| = - a by Lm23;

theorem Th71: :: COMPLEX1:71
for a being real number holds
( |.a.| = a or |.a.| = - a )
proofend;

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

theorem :: COMPLEX1:73
for a, b being real number holds min (a,b) = ((a + b) - |.(a - b).|) / 2
proofend;

theorem :: COMPLEX1:74
for a, b being real number holds max (a,b) = ((a + b) + |.(a - b).|) / 2
proofend;

theorem Th75: :: COMPLEX1:75
for a being real number holds |.a.| ^2 = a ^2
proofend;

theorem :: COMPLEX1:76
for a being real number holds
( - |.a.| <= a &amp; 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:77
for a, b, c, d being real number st a + (b * <i>) = c + (d * <i>) holds
( a = c &amp; b = d )
proofend;

:: from JGRAPH_1, 29.12.2006, AK
theorem :: COMPLEX1:78
for a, b being real number holds sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b)
proofend;

theorem :: COMPLEX1:79
for a, b being real number holds abs a <= sqrt ((a ^2) + (b ^2))
proofend;

theorem :: COMPLEX1:80
for z1 being complex number holds |.(1 / z1).| = 1 / |.z1.| by Th48, Th67;