:: COMPLEX1 semantic presentation

begin


theorem Th1: :: COMPLEX1:1
for a, b being real number st (a ^2) + (b ^2) = 0 holds
a = 0
proof
let a, b be real number ; ::_thesis: ( (a ^2) + (b ^2) = 0 implies a = 0 )
 ( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63;
hence  ( (a ^2) + (b ^2) = 0 implies a = 0 ) ; ::_thesis: verum
end;

Lm1:  for a, b being real number holds 0 <= (a ^2) + (b ^2)
proof
let a, b be real number ; ::_thesis: 0 <= (a ^2) + (b ^2)
 ( 0 <= a ^2 & 0 <= b ^2 ) by XREAL_1:63;
hence  0 <= (a ^2) + (b ^2) ; ::_thesis: verum
end;

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 & it = f . 0 );
existence
 ( ( z in REAL implies ex b1 being set st b1 = z ) & ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st
( z = f & b1 = f . 0 ) ) )
proof
thus  ( z in REAL implies ex IT being set st IT = z ) ; ::_thesis: ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st
( z = f & b1 = f . 0 ) )
A1: z in COMPLEX by XCMPLX_0:def_2;
assume  not z in REAL ; ::_thesis: ex b1 being set ex f being Function of 2,REAL st
( z = f & b1 = f . 0 )
then  z in (Funcs (2,REAL)) \  {  x where x is Element of Funcs (2,REAL) : x . 1 = 0  }  by A1, CARD_1:50, NUMBERS:def_2, XBOOLE_0:def_3;
then reconsider f = z as Function of 2,REAL by FUNCT_2:66;
take  f . 0 ; ::_thesis: ex f being Function of 2,REAL st
( z = f & f . 0 = f . 0 )
take  f ; ::_thesis: ( z = f & f . 0 = f . 0 )
thus  ( z = f & f . 0 = f . 0 ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set holds
( ( z in REAL & b1 = z & b2 = z implies b1 = b2 ) & ( not z in REAL & ex f being Function of 2,REAL st
( z = f & b1 = f . 0 ) & ex f being Function of 2,REAL st
( z = f & 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 & it = f . 1 );
existence
 ( ( z in REAL implies ex b1 being set st b1 = 0 ) & ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st
( z = f & b1 = f . 1 ) ) )
proof
thus  ( z in REAL implies ex IT being set st IT = 0 ) ; ::_thesis: ( not z in REAL implies ex b1 being set ex f being Function of 2,REAL st
( z = f & b1 = f . 1 ) )
A2: z in COMPLEX by XCMPLX_0:def_2;
assume  not z in REAL ; ::_thesis: ex b1 being set ex f being Function of 2,REAL st
( z = f & b1 = f . 1 )
then  z in (Funcs (2,REAL)) \  {  x where x is Element of Funcs (2,REAL) : x . 1 = 0  }  by A2, CARD_1:50, NUMBERS:def_2, XBOOLE_0:def_3;
then reconsider f = z as Function of 2,REAL by FUNCT_2:66;
take  f . 1 ; ::_thesis: ex f being Function of 2,REAL st
( z = f & f . 1 = f . 1 )
take  f ; ::_thesis: ( z = f & f . 1 = f . 1 )
thus  ( z = f & f . 1 = f . 1 ) ; ::_thesis: verum
end;
uniqueness
 for b1, b2 being set holds
( ( z in REAL & b1 = 0 & b2 = 0 implies b1 = b2 ) & ( not z in REAL & ex f being Function of 2,REAL st
( z = f & b1 = f . 1 ) & ex f being Function of 2,REAL st
( z = f & 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 ) ) & ( not z in REAL implies ( b2 = Re z iff ex f being Function of 2,REAL st
( z = f & 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 ) ) & ( not z in REAL implies ( b2 = Im z iff ex f being Function of 2,REAL st
( z = f & b2 = f . 1 ) ) ) );

registration
let z be complex number ;
cluster Re z ->  real ;
coherence
 Re z is real
proof
percases ( z in REAL or not z in REAL ) ;
suppose z in REAL ; ::_thesis: Re z is real
hence  Re z is real by Def1; ::_thesis: verum
end;
suppose not z in REAL ; ::_thesis: Re z is real
then consider f being Function of 2,REAL such that
 z = f and
A1: Re z = f . 0 by Def1;
 0 in 2 by CARD_1:50, TARSKI:def_2;
then  f . 0 in REAL by FUNCT_2:5;
hence  Re z is real by A1; ::_thesis: verum
end;
end;
end;
cluster Im z ->  real ;
coherence
 Im z is real
proof
percases ( z in REAL or not z in REAL ) ;
suppose z in REAL ; ::_thesis: Im z is real
hence  Im z is real by Def2; ::_thesis: verum
end;
suppose not z in REAL ; ::_thesis: Im z is real
then consider f being Function of 2,REAL such that
 z = f and
A2: Im z = f . 1 by Def2;
 1 in 2 by CARD_1:50, TARSKI:def_2;
then  f . 1 in REAL by FUNCT_2:5;
hence  Im z is real by A2; ::_thesis: verum
end;
end;
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 Th2: :: COMPLEX1:2
for f being Function of 2,REAL ex a, b being Element of REAL st f = (0,1) --> (a,b)
proof
let f be Function of 2,REAL; ::_thesis: ex a, b being Element of REAL st f = (0,1) --> (a,b)
 ( 0 in 2 & 1 in 2 ) by CARD_1:50, TARSKI:def_2;
then reconsider a = f . 0, b = f . 1 as Element of REAL by FUNCT_2:5;
take  a ; ::_thesis: ex b being Element of REAL st f = (0,1) --> (a,b)
take  b ; ::_thesis: f = (0,1) --> (a,b)
 dom f = {0,1} by CARD_1:50, FUNCT_2:def_1;
hence  f = (0,1) --> (a,b) by FUNCT_4:66; ::_thesis: verum
end;

Lm2:  for a, b being Element of REAL holds
( Re [*a,b*] = a & Im [*a,b*] = b )
proof
let a, b be Element of REAL ; ::_thesis: ( Re [*a,b*] = a & Im [*a,b*] = b )
reconsider a9 = a, b9 = b as Element of REAL ;
thus  Re [*a,b*] = a ::_thesis: Im [*a,b*] = b
proof
percases ( b = 0 or b <> 0 ) ;
suppose b = 0 ; ::_thesis: Re [*a,b*] = a
then  [*a,b*] = a by ARYTM_0:def_5;
hence  Re [*a,b*] = a by Def1; ::_thesis: verum
end;
suppose b <> 0 ; ::_thesis: Re [*a,b*] = a
then A1: [*a,b*] = (0,1) --> (a9,b9) by ARYTM_0:def_5;
then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:50;
 ( not [*a,b*] in REAL & f . 0 = a ) by A1, ARYTM_0:8, FUNCT_4:63;
hence  Re [*a,b*] = a by Def1; ::_thesis: verum
end;
end;
end;
percases ( b = 0 or b <> 0 ) ;
supposeA2: b = 0 ; ::_thesis: Im [*a,b*] = b
then  [*a,b*] = a by ARYTM_0:def_5;
hence  Im [*a,b*] = b by A2, Def2; ::_thesis: verum
end;
suppose b <> 0 ; ::_thesis: Im [*a,b*] = b
then A3: [*a,b*] = (0,1) --> (a9,b9) by ARYTM_0:def_5;
then reconsider f = [*a,b*] as Function of 2,REAL by CARD_1:50;
 ( not [*a,b*] in REAL & f . 1 = b ) by A3, ARYTM_0:8, FUNCT_4:63;
hence  Im [*a,b*] = b by Def2; ::_thesis: verum
end;
end;
end;

   Lm3:  for z being complex number holds [*(Re z),(Im z)*] = z
proof
let z be complex number ; ::_thesis: [*(Re z),(Im z)*] = z
A1: z in COMPLEX by XCMPLX_0:def_2;
percases ( z in REAL or not z in REAL ) ;
supposeA2: z in REAL ; ::_thesis: [*(Re z),(Im z)*] = z
then  Im z = 0 by Def2;
hence [*(Re z),(Im z)*] = Re z by ARYTM_0:def_5
.= z by A2, Def1 ;
::_thesis: verum
end;
supposeA3: not z in REAL ; ::_thesis: [*(Re z),(Im z)*] = z
then A4: ex f being Function of 2,REAL st
( z = f & Im z = f . 1 ) by Def2;
then consider a, b being Element of REAL  such that
A5: z = (0,1) --> (a,b) by Th2;
reconsider f = z as Element of Funcs (2,REAL) by A5, CARD_1:50, FUNCT_2:8;
 z in (Funcs (2,REAL)) \  {  x where x is Element of Funcs (2,REAL) : x . 1 = 0  }  by A1, A3, CARD_1:50, NUMBERS:def_2, XBOOLE_0:def_3;
then  not z in  {  x where x is Element of Funcs (2,REAL) : x . 1 = 0  }  by XBOOLE_0:def_5;
then  f . 1 <> 0 ;
then A6: b <> 0 by A5, FUNCT_4:63;
 ex f being Function of 2,REAL st
( z = f & Re z = f . 0 ) by A3, Def1;
then A7: Re z = a by A5, FUNCT_4:63;
 Im z = b by A4, A5, FUNCT_4:63;
hence  [*(Re z),(Im z)*] = z by A5, A7, A6, ARYTM_0:def_5; ::_thesis: verum
end;
end;
end;

theorem Th3: :: COMPLEX1:3
for z1, z2 being complex number st Re z1 = Re z2 & Im z1 = Im z2 holds
z1 = z2
proof
let z1, z2 be complex number ; ::_thesis: ( Re z1 = Re z2 & Im z1 = Im z2 implies z1 = z2 )
assume  ( Re z1 = Re z2 & Im z1 = Im z2 ) ; ::_thesis: z1 = z2
hence z1 = [*(Re z2),(Im z2)*] by Lm3
.= z2 by Lm3 ;
::_thesis: verum
end;

definition
let z1, z2 be complex number ;
redefine pred z1 = z2 means :: COMPLEX1:def 3
( Re z1 = Re z2 & Im z1 = Im z2 );
compatibility
 ( z1 = z2 iff ( Re z1 = Re z2 & 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 & 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 & 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 )
proof
let z be complex number ; ::_thesis: ( z = 0 iff ((Re z) ^2) + ((Im z) ^2) = 0 )
set r = Re z;
set i = Im z;
thus  ( z = 0 implies ((Re z) ^2) + ((Im z) ^2) = 0 ) by Th4; ::_thesis: ( ((Re z) ^2) + ((Im z) ^2) = 0 implies z = 0 )
assume  0 = ((Re z) ^2) + ((Im z) ^2) ; ::_thesis: z = 0
then  ( Re z = 0 & Im z = 0 ) by Th1;
hence  z = 0 by Th3, Th4; ::_thesis: verum
end;

theorem Th6: :: COMPLEX1:6
( Re 1r = 1 & 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 & 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
let x be real number ; ::_thesis: for x1, x2 being Element of REAL st x = [*x1,x2*] holds
( x2 = 0 & x = x1 )
let x1, x2 be Element of REAL ; ::_thesis: ( x = [*x1,x2*] implies ( x2 = 0 & x = x1 ) )
assume A1: x = [*x1,x2*] ; ::_thesis: ( x2 = 0 & x = x1 )
A2: x in REAL by XREAL_0:def_1;
hereby  ::_thesis: x = x1
assume  x2 <> 0 ; ::_thesis: contradiction
then  x = (0,1) --> (x1,x2) by A1, ARYTM_0:def_5;
hence  contradiction by A2, ARYTM_0:8; ::_thesis: verum
end;
hence  x = x1 by A1, ARYTM_0:def_5; ::_thesis: verum
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
let x9, y9 be Element of REAL ; ::_thesis: for x, y being real number st x9 = x & y9 = y holds
+ (x9,y9) = x + y
let x, y be real number ; ::_thesis: ( x9 = x & y9 = y implies + (x9,y9) = x + y )
assume A1: ( x9 = x & y9 = y ) ; ::_thesis: + (x9,y9) = x + y
consider x1, x2, y1, y2 being Element of REAL  such that
A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and
A3: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4;
 ( x2 = 0 & y2 = 0 ) by A2, Lm7;
then A4: + (x2,y2) = 0 by ARYTM_0:11;
 ( x = x1 & y = y1 ) by A2, Lm7;
hence  + (x9,y9) = x + y by A1, A3, A4, ARYTM_0:def_5; ::_thesis: verum
end;

Lm9:  for x being Element of REAL holds opp x = - x
proof
let x be Element of REAL ; ::_thesis: opp x = - x
 + (x,(opp x)) = 0 by ARYTM_0:def_3;
then  x + (opp x) = 0 by Lm8;
hence  opp x = - x ; ::_thesis: verum
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
let x9, y9 be Element of REAL ; ::_thesis: for x, y being real number st x9 = x & y9 = y holds
* (x9,y9) = x * y
let x, y be real number ; ::_thesis: ( x9 = x & y9 = y implies * (x9,y9) = x * y )
assume A1: ( x9 = x & y9 = y ) ; ::_thesis: * (x9,y9) = x * y
consider x1, x2, y1, y2 being Element of REAL  such that
A2: x = [*x1,x2*] and
A3: y = [*y1,y2*] and
A4: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5;
 x2 = 0 by A2, Lm7;
then A5: * (x2,y1) = 0 by ARYTM_0:12;
A6: y2 = 0 by A3, Lm7;
then  * (x1,y2) = 0 by ARYTM_0:12;
then A7: + ((* (x1,y2)),(* (x2,y1))) = 0 by A5, ARYTM_0:11;
 ( x = x1 & y = y1 ) by A2, A3, Lm7;
hence  * (x9,y9) = + ((* (x1,y1)),(* ((opp x2),y2))) by A1, A6, ARYTM_0:11, ARYTM_0:12
.= + ((* (x1,y1)),(opp (* (x2,y2)))) by ARYTM_0:15
.= x * y by A4, A7, ARYTM_0:def_5 ;
::_thesis: verum
end;

Lm11:  for x, y, z being complex number st z = x + y holds
Re z = (Re x) + (Re y)
proof
let x, y, z be complex number ; ::_thesis: ( z = x + y implies Re z = (Re x) + (Re y) )
assume A1: z = x + y ; ::_thesis: Re z = (Re x) + (Re y)
consider x1, x2, y1, y2 being Element of REAL  such that
A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and
A3: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4;
A4: ( Re x = x1 & Re y = y1 ) by A2, Lm2;
thus  Re z = + (x1,y1) by A1, A3, Lm2
.= (Re x) + (Re y) by A4, Lm8 ; ::_thesis: verum
end;

Lm12:  for x, y, z being complex number st z = x + y holds
Im z = (Im x) + (Im y)
proof
let x, y, z be complex number ; ::_thesis: ( z = x + y implies Im z = (Im x) + (Im y) )
assume A1: z = x + y ; ::_thesis: Im z = (Im x) + (Im y)
consider x1, x2, y1, y2 being Element of REAL  such that
A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and
A3: x + y = [*(+ (x1,y1)),(+ (x2,y2))*] by XCMPLX_0:def_4;
A4: ( Im x = x2 & Im y = y2 ) by A2, Lm2;
thus  Im z = + (x2,y2) by A1, A3, Lm2
.= (Im x) + (Im y) by A4, Lm8 ; ::_thesis: verum
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
let x, y, z be complex number ; ::_thesis: ( z = x * y implies Re z = ((Re x) * (Re y)) - ((Im x) * (Im y)) )
assume A1: z = x * y ; ::_thesis: Re z = ((Re x) * (Re y)) - ((Im x) * (Im y))
consider x1, x2, y1, y2 being Element of REAL  such that
A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and
A3: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5;
A4: ( Re x = x1 & Re y = y1 ) by A2, Lm2;
A5: ( Im x = x2 & Im y = y2 ) by A2, Lm2;
thus  Re z = + ((* (x1,y1)),(opp (* (x2,y2)))) by A1, A3, Lm2
.= (* (x1,y1)) + (opp (* (x2,y2))) by Lm8
.= (x1 * y1) + (opp (* (x2,y2))) by Lm10
.= (x1 * y1) + (- (* (x2,y2))) by Lm9
.= (x1 * y1) - (* (x2,y2))
.= ((Re x) * (Re y)) - ((Im x) * (Im y)) by A4, A5, Lm10 ; ::_thesis: verum
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
let x, y, z be complex number ; ::_thesis: ( z = x * y implies Im z = ((Re x) * (Im y)) + ((Im x) * (Re y)) )
assume A1: z = x * y ; ::_thesis: Im z = ((Re x) * (Im y)) + ((Im x) * (Re y))
consider x1, x2, y1, y2 being Element of REAL  such that
A2: ( x = [*x1,x2*] & y = [*y1,y2*] ) and
A3: x * y = [*(+ ((* (x1,y1)),(opp (* (x2,y2))))),(+ ((* (x1,y2)),(* (x2,y1))))*] by XCMPLX_0:def_5;
A4: ( Im x = x2 & Im y = y2 ) by A2, Lm2;
A5: ( Re x = x1 & Re y = y1 ) by A2, Lm2;
thus  Im z = + ((* (x1,y2)),(* (x2,y1))) by A1, A3, Lm2
.= (* (x1,y2)) + (* (x2,y1)) by Lm8
.= (x1 * y2) + (* (x2,y1)) by Lm10
.= ((Re x) * (Im y)) + ((Im x) * (Re y)) by A4, A5, Lm10 ; ::_thesis: verum
end;

Lm15:  for z1, z2 being complex number holds z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*]
proof
let z1, z2 be complex number ; ::_thesis: z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*]
set z = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*];
reconsider z9 = z1 + z2 as Element of COMPLEX by XCMPLX_0:def_2;
A1: Im [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] = (Im z1) + (Im z2) by Lm2
.= Im z9 by Lm12 ;
Re [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] = (Re z1) + (Re z2) by Lm2
.= Re z9 by Lm11 ;
hence  z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by A1, Th3; ::_thesis: verum
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
let z1, z2 be complex number ; ::_thesis: z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*]
set z = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*];
reconsider z9 = z1 * z2 as Element of COMPLEX by XCMPLX_0:def_2;
A1: Im [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) by Lm2
.= Im z9 by Lm14 ;
Re [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) by Lm2
.= Re z9 by Lm13 ;
hence  z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by A1, Th3; ::_thesis: verum
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
let z1, z2 be complex number ; ::_thesis: ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )
 z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by Lm16;
hence  ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) by Lm2; ::_thesis: verum
end;

Lm18:  for z1, z2 being complex number holds
( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )
proof
let z1, z2 be complex number ; ::_thesis: ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )
 z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15;
hence  ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) by Lm2; ::_thesis: verum
end;

Lm19:  for x being Real holds Re (x * <i>) = 0
proof
let x be Real; ::_thesis: Re (x * <i>) = 0
thus  Re (x * <i>) = ((Re x) * (Re <i>)) - ((Im x) * (Im <i>)) by Lm17
.= ((Re x) * 0) - (0 * (Im <i>)) by Def2, Th7
.= 0 ; ::_thesis: verum
end;

Lm20:  for x being Real holds Im (x * <i>) = x
proof
let x be Real; ::_thesis: Im (x * <i>) = x
thus  Im (x * <i>) = ((Re x) * (Im <i>)) + ((Im x) * (Re <i>)) by Lm17
.= x by Def1, Th7 ; ::_thesis: verum
end;

Lm21:  for x, y being Real holds [*x,y*] = x + (y * <i>)
proof
let x, y be Real; ::_thesis: [*x,y*] = x + (y * <i>)
A1: Im (x + (y * <i>)) = (Im x) + (Im (y * <i>)) by Lm18
.= 0 + (Im (y * <i>)) by Def2
.= y by Lm20 ;
Re (x + (y * <i>)) = (Re x) + (Re (y * <i>)) by Lm18
.= (Re x) + 0 by Lm19
.= x by Def1 ;
hence  [*x,y*] = x + (y * <i>) by A1, Lm3; ::_thesis: verum
end;

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>) )
proof
 z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15;
hence  for b1 being Element of COMPLEX holds
( b1 = z1 + z2 iff b1 = ((Re z1) + (Re z2)) + (((Im z1) + (Im z2)) * <i>) ) by Lm21; ::_thesis: verum
end;
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) & Im (z1 + z2) = (Im z1) + (Im z2) )
proof
let z1, z2 be complex number ; ::_thesis: ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) )
 z1 + z2 = [*((Re z1) + (Re z2)),((Im z1) + (Im z2))*] by Lm15;
hence  ( Re (z1 + z2) = (Re z1) + (Re z2) & Im (z1 + z2) = (Im z1) + (Im z2) ) by Lm2; ::_thesis: verum
end;

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>) )
proof
 z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by Lm16;
hence  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>) ) by Lm21; ::_thesis: verum
end;
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)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )
proof
let z1, z2 be complex number ; ::_thesis: ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) )
 z1 * z2 = [*(((Re z1) * (Re z2)) - ((Im z1) * (Im z2))),(((Re z1) * (Im z2)) + ((Re z2) * (Im z1)))*] by Lm16;
hence  ( Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) & Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) ) by Lm2; ::_thesis: verum
end;

theorem :: COMPLEX1:10
for a being real number holds Re (a * <i>) = 0
proof
let a be real number ; ::_thesis: Re (a * <i>) = 0
A1: a in REAL by XREAL_0:def_1;
thus  Re (a * <i>) = ((Re a) * (Re <i>)) - ((Im a) * (Im <i>)) by Th9
.= ((Re a) * 0) - (0 * (Im <i>)) by Def2, Th7, A1
.= 0 ; ::_thesis: verum
end;

theorem :: COMPLEX1:11
for a being real number holds Im (a * <i>) = a
proof
let a be real number ; ::_thesis: Im (a * <i>) = a
A1: a in REAL by XREAL_0:def_1;
thus  Im (a * <i>) = ((Re a) * (Im <i>)) + ((Im a) * (Re <i>)) by Th9
.= a by Def1, Th7, A1 ; ::_thesis: verum
end;

theorem Th12: :: COMPLEX1:12
for a, b being real number holds
( Re (a + (b * <i>)) = a & Im (a + (b * <i>)) = b )
proof
let a, b be real number ; ::_thesis: ( Re (a + (b * <i>)) = a & Im (a + (b * <i>)) = b )
reconsider a = a, b = b as Real by XREAL_0:def_1;
 a + (b * <i>) = [*a,b*] by Lm21;
hence  ( Re (a + (b * <i>)) = a & Im (a + (b * <i>)) = b ) by Lm2; ::_thesis: verum
end;

theorem Th13: :: COMPLEX1:13
for z being complex number holds (Re z) + ((Im z) * <i>) = z
proof
let z be complex number ; ::_thesis: (Re z) + ((Im z) * <i>) = z
 [*(Re z),(Im z)*] = z by Lm3;
hence  (Re z) + ((Im z) * <i>) = z by Lm21; ::_thesis: verum
end;

theorem Th14: :: COMPLEX1:14
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
let z1, z2 be complex number ; ::_thesis: ( Im z1 = 0 & Im z2 = 0 implies ( Re (z1 * z2) = (Re z1) * (Re z2) & Im (z1 * z2) = 0 ) )
assume that
A1: Im z1 = 0 and
A2: Im z2 = 0 ; ::_thesis: ( Re (z1 * z2) = (Re z1) * (Re z2) & Im (z1 * z2) = 0 )
thus  Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) by Th9
.= (Re z1) * (Re z2) by A1 ; ::_thesis: Im (z1 * z2) = 0
thus  Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) by Th9
.= 0 by A1, A2 ; ::_thesis: verum
end;

theorem Th15: :: COMPLEX1:15
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
let z1, z2 be complex number ; ::_thesis: ( Re z1 = 0 & Re z2 = 0 implies ( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 ) )
assume that
A1: Re z1 = 0 and
A2: Re z2 = 0 ; ::_thesis: ( Re (z1 * z2) = - ((Im z1) * (Im z2)) & Im (z1 * z2) = 0 )
thus  Re (z1 * z2) = ((Re z1) * (Re z2)) - ((Im z1) * (Im z2)) by Th9
.= - ((Im z1) * (Im z2)) by A1 ; ::_thesis: Im (z1 * z2) = 0
thus  Im (z1 * z2) = ((Re z1) * (Im z2)) + ((Re z2) * (Im z1)) by Th9
.= 0 by A1, A2 ; ::_thesis: verum
end;

theorem :: COMPLEX1:16
for z being complex number holds
( Re (z * z) = ((Re z) ^2) - ((Im z) ^2) & Im (z * z) = 2 * ((Re z) * (Im z)) )
proof
let z be complex number ; ::_thesis: ( Re (z * z) = ((Re z) ^2) - ((Im z) ^2) & Im (z * z) = 2 * ((Re z) * (Im z)) )
thus  Re (z * z) = ((Re z) ^2) - ((Im z) ^2) by Th9; ::_thesis: Im (z * z) = 2 * ((Re z) * (Im z))
thus  Im (z * z) = ((Re z) * (Im z)) + ((Re z) * (Im z)) by Th9
.= 2 * ((Re z) * (Im z)) ; ::_thesis: verum
end;

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>) )
proof
set z9 = [*(- (Re z)),(- (Im z))*];
[*(- (Re z)),(- (Im z))*] + z = [*((Re [*(- (Re z)),(- (Im z))*]) + (Re z)),((Im [*(- (Re z)),(- (Im z))*]) + (Im z))*] by Lm15
.= [*((- (Re z)) + (Re z)),((Im [*(- (Re z)),(- (Im z))*]) + (Im z))*] by Lm2
.= [*0,((- (Im z)) + (Im z))*] by Lm2
.= 0 by ARYTM_0:def_5 ;
hence  for b1 being Element of COMPLEX holds
( b1 = - z iff b1 = (- (Re z)) + ((- (Im z)) * <i>) ) by Lm21; ::_thesis: verum
end;
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) & Im (- z) = - (Im z) )
proof
let z be complex number ; ::_thesis: ( Re (- z) = - (Re z) & Im (- z) = - (Im z) )
 z in COMPLEX by XCMPLX_0:def_2;
then  - z = (- (Re z)) + ((- (Im z)) * <i>) by Def7;
hence  ( Re (- z) = - (Re z) & Im (- z) = - (Im z) ) by Th12; ::_thesis: verum
end;

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>) )
proof
A1: z1 = (Re z1) + ((Im z1) * <i>) by Th13;
z1 - z2 = z1 + (- z2)
.= z1 + ((- (Re z2)) + ((- (Im z2)) * <i>)) by Def7
.= ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) by A1 ;
hence  for b1 being Element of COMPLEX holds
( b1 = z1 - z2 iff b1 = ((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>) ) ; ::_thesis: verum
end;
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) & Im (z1 - z2) = (Im z1) - (Im z2) )
proof
let z1, z2 be complex number ; ::_thesis: ( Re (z1 - z2) = (Re z1) - (Re z2) & Im (z1 - z2) = (Im z1) - (Im z2) )
A1: ( z1 in COMPLEX & z2 in COMPLEX ) by XCMPLX_0:def_2;
hence  Re (z1 - z2) = Re (((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>)) by Def8
.= (Re z1) - (Re z2) by Th12 ;
::_thesis: Im (z1 - z2) = (Im z1) - (Im z2)
thus  Im (z1 - z2) = Im (((Re z1) - (Re z2)) + (((Im z1) - (Im z2)) * <i>)) by A1, Def8
.= (Im z1) - (Im z2) by Th12 ; ::_thesis: verum
end;

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>) )
proof
reconsider z9 = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) as Element of COMPLEX by XCMPLX_0:def_2;
percases ( z = 0 or z <> 0 ) ;
suppose z = 0 ; ::_thesis: 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>) )
hence  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>) ) by Th4; ::_thesis: verum
end;
supposeA1: z <> 0 ; ::_thesis: 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>) )
then A2: ((Re z) ^2) + ((Im z) ^2) <> 0 by Th5;
A3: Im z9 = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th12;
then A4: ((Re z) * (Im z9)) + ((Re z9) * (Im z)) = (((Re z) / 1) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) + (((Re z) / (((Re z) ^2) + ((Im z) ^2))) * (Im z)) by Th12
.= (((Re z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) + ((((Re z) / (((Re z) ^2) + ((Im z) ^2))) * (Im z)) / 1) by XCMPLX_1:76
.= (((Re z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) + ((((Im z) / 1) * (Re z)) / (((Re z) ^2) + ((Im z) ^2))) by XCMPLX_1:76
.= ((- ((Re z) * (Im z))) + ((Re z) * (Im z))) / (((Re z) ^2) + ((Im z) ^2)) by XCMPLX_1:62
.= 0 ;
A5: ((Re z) * (Re z9)) - ((Im z) * (Im z9)) = (((Re z) / 1) * ((Re z) / (((Re z) ^2) + ((Im z) ^2)))) - ((Im z) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) by A3, Th12
.= (((Re z) * (Re z)) / (1 * (((Re z) ^2) + ((Im z) ^2)))) - (((Im z) / 1) * ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:76
.= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - (((Im z) * (- (Im z))) / (1 * (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:76
.= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - ((- ((Im z) ^2)) / (1 * (((Re z) ^2) + ((Im z) ^2))))
.= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) - (- (((Im z) ^2) / (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:187
.= (((Re z) ^2) / (((Re z) ^2) + ((Im z) ^2))) + (((Im z) ^2) / (1 * (((Re z) ^2) + ((Im z) ^2))))
.= (((Re z) ^2) + ((Im z) ^2)) / (((Re z) ^2) + ((Im z) ^2)) by XCMPLX_1:62
.= 1 by A2, XCMPLX_1:60 ;
z * z9 = [*(((Re z) * (Re z9)) - ((Im z) * (Im z9))),(((Re z) * (Im z9)) + ((Re z9) * (Im z)))*] by Lm16
.= 1 by A5, A4, ARYTM_0:def_5 ;
hence  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>) ) by A1, XCMPLX_0:def_7; ::_thesis: verum
end;
end;
end;
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)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) )
proof
let z be complex number ; ::_thesis: ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) )
 z in COMPLEX by XCMPLX_0:def_2;
then  z " = ((Re z) / (((Re z) ^2) + ((Im z) ^2))) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) * <i>) by Def9;
hence  ( Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) & Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) ) by Th12; ::_thesis: verum
end;

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

theorem Th22: :: COMPLEX1:22
for z being complex number st Re z <> 0 & Im z = 0 holds
( Re (z ") = (Re z) " & Im (z ") = 0 )
proof
let z be complex number ; ::_thesis: ( Re z <> 0 & Im z = 0 implies ( Re (z ") = (Re z) " & Im (z ") = 0 ) )
assume that
A1: Re z <> 0 and
A2: Im z = 0 ; ::_thesis: ( Re (z ") = (Re z) " & Im (z ") = 0 )
 Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20;
hence  Re (z ") = (1 * (Re z)) / ((Re z) * (Re z)) by A2
.= 1 / (Re z) by A1, XCMPLX_1:91
.= (Re z) " by XCMPLX_1:215 ;
::_thesis: Im (z ") = 0
 Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th20;
hence  Im (z ") = 0 by A2; ::_thesis: verum
end;

theorem Th23: :: COMPLEX1:23
for z being complex number st Re z = 0 & Im z <> 0 holds
( Re (z ") = 0 & Im (z ") = - ((Im z) ") )
proof
let z be complex number ; ::_thesis: ( Re z = 0 & Im z <> 0 implies ( Re (z ") = 0 & Im (z ") = - ((Im z) ") ) )
assume that
A1: Re z = 0 and
A2: Im z <> 0 ; ::_thesis: ( Re (z ") = 0 & Im (z ") = - ((Im z) ") )
 Re (z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20;
hence  Re (z ") = 0 by A1; ::_thesis: Im (z ") = - ((Im z) ")
 Im (z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2)) by Th20;
hence  Im (z ") = - ((1 * (Im z)) / ((Im z) * (Im z))) by A1, XCMPLX_1:187
.= - (1 / (Im z)) by A2, XCMPLX_1:91
.= - ((Im z) ") by XCMPLX_1:215 ;
::_thesis: verum
end;

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>) )
proof
reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def_2;
set k = ((Re z2) ^2) + ((Im z2) ^2);
A1: Re [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] = Re (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) + (((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>)) by Lm21
.= (Re z2) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ;
A2: Im [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] = Im (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) + (((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>)) by Lm21
.= (- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ;
z1 / z2 = z1 * (z2 ") by XCMPLX_0:def_9
.= z1 * [*((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))),((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))*] by Lm21
.= [*((((Re z1) / 1) * ((Re z2) / (((Re z2) ^2) + ((Im z2) ^2)))) - ((Im z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))),(((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1)))*] by A1, A2, Lm16
.= ((((Re z1) / 1) * ((Re z2) / (((Re z2) ^2) + ((Im z2) ^2)))) - ((Im z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))) + ((((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * <i>) by Lm21
.= ((((Re z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2)))) - (((Im z1) / 1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2))))) + ((((Re z1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * <i>) by XCMPLX_1:76
.= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) + (((((Re z1) / 1) * ((- (Im z2)) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * (Im z1))) * <i>) by XCMPLX_1:76
.= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((((Re z1) * (- (Im z2))) / (1 * (((Re z2) ^2) + ((Im z2) ^2)))) + (((Re z2) / (((Re z2) ^2) + ((Im z2) ^2))) * ((Im z1) / 1))) * <i>) by XCMPLX_1:76
.= ((((Re z1) * (Re z2)) / (((Re z2) ^2) + ((Im z2) ^2))) - (((Im z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)))) + (((((Re z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((Im z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) * <i>) by XCMPLX_1:76
.= ((((Re z1) * (Re z2)) - ((Im z1) * (- (Im z2)))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((((Re z1) * (- (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + (((Im z1) * (Re z2)) / (1 * (((Re z2) ^2) + ((Im z2) ^2))))) * <i>) by XCMPLX_1:120
.= ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))) + ((((- ((Re z1) * (Im z2))) + ((Im z1) * (Re z2))) / (((Re z2) ^2) + ((Im z2) ^2))) * <i>) by XCMPLX_1:62
.= ((((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>) ;
hence  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>) ) ; ::_thesis: verum
end;
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)) & Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) )
proof
let z1, z2 be complex number ; ::_thesis: ( 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)) )
thus  Re (z1 / z2) = Re (((((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>)) by Def10
.= (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ; ::_thesis: Im (z1 / z2) = (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2))
thus  Im (z1 / z2) = Im (((((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>)) by Def10
.= (((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2) + ((Im z2) ^2)) by Th12 ; ::_thesis: verum
end;

theorem :: COMPLEX1:25
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
let z1, z2 be complex number ; ::_thesis: ( Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 implies ( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 ) )
assume that
A1: Im z1 = 0 and
A2: ( Im z2 = 0 & Re z2 <> 0 ) ; ::_thesis: ( Re (z1 / z2) = (Re z1) / (Re z2) & Im (z1 / z2) = 0 )
A3: ( z1 / z2 = z1 * (z2 ") & Im (z2 ") = 0 ) by A2, Th22, XCMPLX_0:def_9;
hence  Re (z1 / z2) = (Re z1) * (Re (z2 ")) by A1, Th14
.= (Re z1) * ((Re z2) ") by A2, Th22
.= (Re z1) / (Re z2) by XCMPLX_0:def_9 ;
::_thesis: Im (z1 / z2) = 0
thus  Im (z1 / z2) = 0 by A1, A3, Th14; ::_thesis: verum
end;

theorem :: COMPLEX1:26
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
let z1, z2 be complex number ; ::_thesis: ( Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 implies ( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 ) )
assume that
A1: Re z1 = 0 and
A2: ( Re z2 = 0 & Im z2 <> 0 ) ; ::_thesis: ( Re (z1 / z2) = (Im z1) / (Im z2) & Im (z1 / z2) = 0 )
A3: ( z1 / z2 = z1 * (z2 ") & Re (z2 ") = 0 ) by A2, Th23, XCMPLX_0:def_9;
hence  Re (z1 / z2) = - ((Im z1) * (Im (z2 "))) by A1, Th15
.= - ((Im z1) * (- ((Im z2) "))) by A2, Th23
.= - (- ((Im z1) * ((Im z2) ")))
.= (Im z1) / (Im z2) by XCMPLX_0:def_9 ;
::_thesis: Im (z1 / z2) = 0
thus  Im (z1 / z2) = 0 by A1, A3, Th15; ::_thesis: verum
end;

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>)
proof
let z, z9 be complex number ; ::_thesis: ( z = (Re z9) - ((Im z9) * <i>) implies z9 = (Re z) - ((Im z) * <i>) )
assume  z = (Re z9) - ((Im z9) * <i>) ; ::_thesis: z9 = (Re z) - ((Im z) * <i>)
then  z = (Re z9) + ((- (Im z9)) * <i>) ;
then  ( Re z = Re z9 & - (Im z) = - (- (Im z9)) ) by Th12;
hence z9 = (Re z) + ((- (Im z)) * <i>) by Th13
.= (Re z) - ((Im z) * <i>) ;
::_thesis: verum
end;
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 & Im (z *') = - (Im z) )
proof
let z be complex number ; ::_thesis: ( Re (z *') = Re z & Im (z *') = - (Im z) )
 z *' = (Re z) + ((- (Im z)) * <i>) ;
hence  ( Re (z *') = Re z & Im (z *') = - (Im z) ) by Th12; ::_thesis: verum
end;

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

theorem :: COMPLEX1:29
for z being complex number st z *' = 0 holds
z = 0
proof
let z be complex number ; ::_thesis: ( z *' = 0 implies z = 0 )
assume  z *' = 0 ; ::_thesis: z = 0
then  0 = (Re z) + ((- (Im z)) * <i>) ;
hence  ( Re z = Re 0 & Im z = Im 0 ) by Th4, Th12; :: according to COMPLEX1:def_3 ::_thesis: verum
end;

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 *')
proof
let z1, z2 be complex number ; ::_thesis: (z1 + z2) *' = (z1 *') + (z2 *')
thus  Re ((z1 + z2) *') = Re (z1 + z2) by Th27
.= (Re z1) + (Re z2) by Th8
.= (Re (z1 *')) + (Re z2) by Th27
.= (Re (z1 *')) + (Re (z2 *')) by Th27
.= Re ((z1 *') + (z2 *')) by Th8 ; :: according to COMPLEX1:def_3 ::_thesis: Im ((z1 + z2) *') = Im ((z1 *') + (z2 *'))
thus  Im ((z1 + z2) *') = - (Im (z1 + z2)) by Th27
.= - ((Im z1) + (- (- (Im z2)))) by Th8
.= (- (Im z1)) + (- (Im z2))
.= (Im (z1 *')) + (- (Im z2)) by Th27
.= (Im (z1 *')) + (Im (z2 *')) by Th27
.= Im ((z1 *') + (z2 *')) by Th8 ; ::_thesis: verum
end;

theorem Th33: :: COMPLEX1:33
for z being complex number holds (- z) *' = - (z *')
proof
let z be complex number ; ::_thesis: (- z) *' = - (z *')
thus  Re ((- z) *') = Re (- z) by Th27
.= - (Re z) by Th17
.= - (Re (z *')) by Th27
.= Re (- (z *')) by Th17 ; :: according to COMPLEX1:def_3 ::_thesis: Im ((- z) *') = Im (- (z *'))
thus  Im ((- z) *') = - (Im (- z)) by Th27
.= - (- (Im z)) by Th17
.= - (Im (z *')) by Th27
.= Im (- (z *')) by Th17 ; ::_thesis: verum
end;

theorem :: COMPLEX1:34
for z1, z2 being complex number holds (z1 - z2) *' = (z1 *') - (z2 *')
proof
let z1, z2 be complex number ; ::_thesis: (z1 - z2) *' = (z1 *') - (z2 *')
thus (z1 - z2) *' = (z1 + (- z2)) *'
.= (z1 *') + ((- z2) *') by Th32
.= (z1 *') + (- (z2 *')) by Th33
.= (z1 *') - (z2 *') ; ::_thesis: verum
end;

theorem Th35: :: COMPLEX1:35
for z1, z2 being complex number holds (z1 * z2) *' = (z1 *') * (z2 *')
proof
let z1, z2 be complex number ; ::_thesis: (z1 * z2) *' = (z1 *') * (z2 *')
A1: ( Re (z1 *') = Re z1 & Re (z2 *') = Re z2 ) by Th27;
A2: ( Im (z1 *') = - (Im z1) & Im (z2 *') = - (Im z2) ) by Th27;
thus  Re ((z1 * z2) *') = Re (z1 * z2) by Th27
.= ((Re (z1 *')) * (Re (z2 *'))) - ((- (Im (z1 *'))) * (- (Im (z2 *')))) by A1, A2, Th9
.= ((Re (z1 *')) * (Re (z2 *'))) - (- (- ((Im (z1 *')) * (Im (z2 *')))))
.= Re ((z1 *') * (z2 *')) by Th9 ; :: according to COMPLEX1:def_3 ::_thesis: Im ((z1 * z2) *') = Im ((z1 *') * (z2 *'))
thus  Im ((z1 * z2) *') = - (Im (z1 * z2)) by Th27
.= - (((Re (z1 *')) * (- (Im (z2 *')))) + ((Re (z2 *')) * (- (Im (z1 *'))))) by A1, A2, Th9
.= ((Re (z2 *')) * (Im (z1 *'))) + (- (- ((Re (z1 *')) * (Im (z2 *')))))
.= Im ((z1 *') * (z2 *')) by Th9 ; ::_thesis: verum
end;

theorem Th36: :: COMPLEX1:36
for z being complex number holds (z ") *' = (z *') "
proof
let z be complex number ; ::_thesis: (z ") *' = (z *') "
A1: ( Re z = Re (z *') & - (Im z) = Im (z *') ) by Th27;
thus  Re ((z ") *') = Re (z ") by Th27
.= (Re z) / (((Re z) ^2) + ((Im z) ^2)) by Th20
.= Re ((z *') ") by A1, Th20 ; :: according to COMPLEX1:def_3 ::_thesis: Im ((z ") *') = Im ((z *') ")
thus  Im ((z ") *') = - (Im (z ")) by Th27
.= - ((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) by Th20
.= (- (Im (z *'))) / (((Re (z *')) ^2) + ((Im (z *')) ^2)) by A1, XCMPLX_1:187
.= Im ((z *') ") by Th20 ; ::_thesis: verum
end;

theorem :: COMPLEX1:37
for z1, z2 being complex number holds (z1 / z2) *' = (z1 *') / (z2 *')
proof
let z1, z2 be complex number ; ::_thesis: (z1 / z2) *' = (z1 *') / (z2 *')
thus (z1 / z2) *' = (z1 * (z2 ")) *' by XCMPLX_0:def_9
.= (z1 *') * ((z2 ") *') by Th35
.= (z1 *') * ((z2 *') ") by Th36
.= (z1 *') / (z2 *') by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: COMPLEX1:38
for z being complex number st Im z = 0 holds
z *' = z
proof
let z be complex number ; ::_thesis: ( Im z = 0 implies z *' = z )
 ( Re (z *') = Re z & Im (z *') = - (Im z) ) by Th27;
hence  ( Im z = 0 implies z *' = z ) by Th3; ::_thesis: verum
end;

theorem :: COMPLEX1:39
for z being complex number st Re z = 0 holds
z *' = - z
proof
let z be complex number ; ::_thesis: ( Re z = 0 implies z *' = - z )
A1: z in COMPLEX by XCMPLX_0:def_2;
assume A2: Re z = 0 ; ::_thesis: z *' = - z
hence z *' = (- 0) + ((- (Im z)) * <i>)
.= - z by A1, A2, Def7 ;
::_thesis: verum
end;

theorem :: COMPLEX1:40
for z being complex number holds
( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 )
proof
let z be complex number ; ::_thesis: ( Re (z * (z *')) = ((Re z) ^2) + ((Im z) ^2) & Im (z * (z *')) = 0 )
thus  Re (z * (z *')) = ((Re z) * (Re (z *'))) - ((Im z) * (Im (z *'))) by Th9
.= ((Re z) * (Re z)) - ((Im z) * (Im (z *'))) by Th27
.= ((Re z) * (Re z)) - ((Im z) * (- (Im z))) by Th27
.= ((Re z) ^2) + ((Im z) ^2) ; ::_thesis: Im (z * (z *')) = 0
thus  Im (z * (z *')) = ((Re z) * (Im (z *'))) + ((Re (z *')) * (Im z)) by Th9
.= ((Re z) * (- (Im z))) + ((Re (z *')) * (Im z)) by Th27
.= (- ((Re z) * (Im z))) + ((Re z) * (Im z)) by Th27
.= 0 ; ::_thesis: verum
end;

theorem :: COMPLEX1:41
for z being complex number holds
( Re (z + (z *')) = 2 * (Re z) & Im (z + (z *')) = 0 )
proof
let z be complex number ; ::_thesis: ( Re (z + (z *')) = 2 * (Re z) & Im (z + (z *')) = 0 )
thus  Re (z + (z *')) = (Re z) + (Re (z *')) by Th8
.= (Re z) + (Re z) by Th27
.= 2 * (Re z) ; ::_thesis: Im (z + (z *')) = 0
thus  Im (z + (z *')) = (Im z) + (Im (z *')) by Th8
.= (Im z) + (- (Im z)) by Th27
.= 0 ; ::_thesis: verum
end;

theorem :: COMPLEX1:42
for z being complex number holds
( Re (z - (z *')) = 0 & Im (z - (z *')) = 2 * (Im z) )
proof
let z be complex number ; ::_thesis: ( Re (z - (z *')) = 0 & Im (z - (z *')) = 2 * (Im z) )
thus  Re (z - (z *')) = (Re z) - (Re (z *')) by Th19
.= (Re z) - (Re z) by Th27
.= 0 ; ::_thesis: Im (z - (z *')) = 2 * (Im z)
thus  Im (z - (z *')) = (Im z) - (Im (z *')) by Th19
.= (Im z) - (- (Im z)) by Th27
.= 2 * (Im z) ; ::_thesis: verum
end;

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))
proof
let r be real number ; ::_thesis: for b1 being complex number st r = sqrt (((Re b1) ^2) + ((Im b1) ^2)) holds
r = sqrt (((Re r) ^2) + ((Im r) ^2))
let z be complex number ; ::_thesis: ( r = sqrt (((Re z) ^2) + ((Im z) ^2)) implies r = sqrt (((Re r) ^2) + ((Im r) ^2)) )
assume A1: r = sqrt (((Re z) ^2) + ((Im z) ^2)) ; ::_thesis: r = sqrt (((Re r) ^2) + ((Im r) ^2))
then A2: Im r = 0 by Def2;
 ( (Re z) ^2 >= 0 & (Im z) ^2 >= 0 ) by XREAL_1:63;
then  r >= 0 by A1, SQUARE_1:def_2;
then A3: Re r >= 0 by A1, Def1;
thus r = Re r by A1, Def1
.= sqrt (((Re r) ^2) + ((Im r) ^2)) by A3, A2, SQUARE_1:22 ; ::_thesis: verum
end;
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
proof
let a be real number ; ::_thesis: ( a >= 0 implies |.a.| = a )
A1: a in REAL by XREAL_0:def_1;
then A2: Im a = 0 by Def2;
assume  a >= 0 ; ::_thesis: |.a.| = a
then  Re a >= 0 by A1, Def1;
hence |.a.| = Re a by A2, SQUARE_1:22
.= a by A1, Def1 ;
::_thesis: verum
end;

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
proof
assume  |.z.| is zero ; ::_thesis: contradiction
then  ((Re z) ^2) + ((Im z) ^2) = 0 by Lm1, SQUARE_1:24;
hence  contradiction by Th5; ::_thesis: verum
end;
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
proof
 0 <= ((Re z) ^2) + ((Im z) ^2) by Lm1;
hence  not |.z.| is negative by SQUARE_1:def_2; ::_thesis: verum
end;
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.|
proof
let z be complex number ; ::_thesis: |.(- z).| = |.z.|
thus |.(- z).| = sqrt (((- (Re z)) ^2) + ((Im (- z)) ^2)) by Th17
.= sqrt (((- (Re z)) ^2) + ((- (Im z)) ^2)) by Th17
.= |.z.| ; ::_thesis: verum
end;

Lm23:  for a being real number st a <= 0 holds
|.a.| = - a
proof
let a be real number ; ::_thesis: ( a <= 0 implies |.a.| = - a )
assume  a <= 0 ; ::_thesis: |.a.| = - a
then  |.(- a).| = - a by Th43;
hence  |.a.| = - a by Lm22; ::_thesis: verum
end;

Lm24:  for a being real number holds sqrt (a ^2) = |.a.|
proof
let a be real number ; ::_thesis: sqrt (a ^2) = |.a.|
percases ( 0 <= a or not 0 <= a ) ;
supposeA1: 0 <= a ; ::_thesis: sqrt (a ^2) = |.a.|
then  sqrt (a ^2) = a by SQUARE_1:22;
hence  sqrt (a ^2) = |.a.| by A1, Th43; ::_thesis: verum
end;
supposeA2: not 0 <= a ; ::_thesis: sqrt (a ^2) = |.a.|
then  |.a.| = - a by Lm23;
hence  sqrt (a ^2) = |.a.| by A2, SQUARE_1:23; ::_thesis: verum
end;
end;
end;

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.|
proof
let z be complex number ; ::_thesis: |.(z *').| = |.z.|
thus |.(z *').| = sqrt (((Re z) ^2) + ((Im (z *')) ^2)) by Th27
.= sqrt (((Re z) ^2) + ((- (Im z)) ^2)) by Th27
.= |.z.| ; ::_thesis: verum
end;

Lm25:  for a being real number holds
( - |.a.| <= a & a <= |.a.| )
proof
let a be real number ; ::_thesis: ( - |.a.| <= a & a <= |.a.| )
 ( a < 0 implies ( - |.a.| <= a & a <= |.a.| ) )
proof
assume  a < 0 ; ::_thesis: ( - |.a.| <= a & a <= |.a.| )
then  |.a.| = - a by Lm23;
hence  ( - |.a.| <= a & a <= |.a.| ) ; ::_thesis: verum
end;
hence  ( - |.a.| <= a & a <= |.a.| ) by Th43; ::_thesis: verum
end;

theorem :: COMPLEX1:54
for z being complex number holds Re z <= |.z.|
proof
let z be complex number ; ::_thesis: Re z <= |.z.|
 0 <= (Im z) ^2 by XREAL_1:63;
then A1: ((Re z) ^2) + 0 <= ((Re z) ^2) + ((Im z) ^2) by XREAL_1:7;
 0 <= (Re z) ^2 by XREAL_1:63;
then  sqrt ((Re z) ^2) <= |.z.| by A1, SQUARE_1:26;
then A2: |.(Re z).| <= |.z.| by Lm24;
 Re z <= |.(Re z).| by Lm25;
hence  Re z <= |.z.| by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem :: COMPLEX1:55
for z being complex number holds Im z <= |.z.|
proof
let z be complex number ; ::_thesis: Im z <= |.z.|
 0 <= (Re z) ^2 by XREAL_1:63;
then A1: ((Im z) ^2) + 0 <= ((Re z) ^2) + ((Im z) ^2) by XREAL_1:7;
 0 <= (Im z) ^2 by XREAL_1:63;
then  sqrt ((Im z) ^2) <= |.z.| by A1, SQUARE_1:26;
then A2: |.(Im z).| <= |.z.| by Lm24;
 Im z <= |.(Im z).| by Lm25;
hence  Im z <= |.z.| by A2, XXREAL_0:2; ::_thesis: verum
end;

theorem Th56: :: COMPLEX1:56
for z1, z2 being complex number holds |.(z1 + z2).| <= |.z1.| + |.z2.|
proof
let z1, z2 be complex number ; ::_thesis: |.(z1 + z2).| <= |.z1.| + |.z2.|
set r1 = Re z1;
set r2 = Re z2;
set i1 = Im z1;
set i2 = Im z2;
A1: (Im (z1 + z2)) ^2 = ((Im z1) + (Im z2)) ^2 by Th8
.= (((Im z1) ^2) + ((2 * (Im z1)) * (Im z2))) + ((Im z2) ^2) ;
A2: 0 <= ((Re z1) ^2) + ((Im z1) ^2) by Lm1;
 ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) - ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) = (((Re z1) * (Im z2)) - ((Im z1) * (Re z2))) ^2 ;
then  0 <= ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) - ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) by XREAL_1:63;
then A3: ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) + 0 <= (((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2)) by XREAL_1:19;
 ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= |.(((Re z1) * (Re z2)) + ((Im z1) * (Im z2))).| by Lm25;
then A4: ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) by Lm24;
A5: 0 <= ((Re z2) ^2) + ((Im z2) ^2) by Lm1;
then A6: (sqrt (((Re z2) ^2) + ((Im z2) ^2))) ^2 = ((Re z2) ^2) + ((Im z2) ^2) by SQUARE_1:def_2;
 0 <= (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2 by XREAL_1:63;
then  sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) <= sqrt ((((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2))) by A3, SQUARE_1:26;
then  sqrt ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ^2) <= (sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2))) by A2, A5, SQUARE_1:29;
then A7: ((Re z1) * (Re z2)) + ((Im z1) * (Im z2)) <= (sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2))) by A4, XXREAL_0:2;
 ((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)) = 2 * (((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) ;
then  ((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)) <= 2 * ((sqrt (((Re z1) ^2) + ((Im z1) ^2))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2)))) by A7, XREAL_1:64;
then A8: (((Re z1) ^2) + ((Im z1) ^2)) + (((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2))) <= (((Re z1) ^2) + ((Im z1) ^2)) + ((2 * (sqrt (((Re z1) ^2) + ((Im z1) ^2)))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2)))) by XREAL_1:7;
(Re (z1 + z2)) ^2 = ((Re z1) + (Re z2)) ^2 by Th8
.= (((Re z1) ^2) + ((2 * (Re z1)) * (Re z2))) + ((Re z2) ^2) ;
then  ((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2) = ((((Re z1) ^2) + ((Im z1) ^2)) + (((2 * (Re z1)) * (Re z2)) + ((2 * (Im z1)) * (Im z2)))) + (((Re z2) ^2) + ((Im z2) ^2)) by A1;
then A9: ((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2) <= ((((Re z1) ^2) + ((Im z1) ^2)) + ((2 * (sqrt (((Re z1) ^2) + ((Im z1) ^2)))) * (sqrt (((Re z2) ^2) + ((Im z2) ^2))))) + (((Re z2) ^2) + ((Im z2) ^2)) by A8, XREAL_1:7;
A10: 0 <= ((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2) by Lm1;
 (sqrt (((Re z1) ^2) + ((Im z1) ^2))) ^2 = ((Re z1) ^2) + ((Im z1) ^2) by A2, SQUARE_1:def_2;
then  sqrt (((Re (z1 + z2)) ^2) + ((Im (z1 + z2)) ^2)) <= sqrt (((sqrt (((Re z1) ^2) + ((Im z1) ^2))) + (sqrt (((Re z2) ^2) + ((Im z2) ^2)))) ^2) by A6, A9, A10, SQUARE_1:26;
hence  |.(z1 + z2).| <= |.z1.| + |.z2.| by SQUARE_1:22; ::_thesis: verum
end;

theorem Th57: :: COMPLEX1:57
for z1, z2 being complex number holds |.(z1 - z2).| <= |.z1.| + |.z2.|
proof
let z1, z2 be complex number ; ::_thesis: |.(z1 - z2).| <= |.z1.| + |.z2.|
 |.(z1 - z2).| = |.(z1 + (- z2)).| ;
then  |.(z1 - z2).| <= |.z1.| + |.(- z2).| by Th56;
hence  |.(z1 - z2).| <= |.z1.| + |.z2.| by Lm22; ::_thesis: verum
end;

theorem :: COMPLEX1:58
for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 + z2).|
proof
let z1, z2 be complex number ; ::_thesis: |.z1.| - |.z2.| <= |.(z1 + z2).|
 z1 = (z1 + z2) - z2 ;
then  |.z1.| <= |.(z1 + z2).| + |.z2.| by Th57;
hence  |.z1.| - |.z2.| <= |.(z1 + z2).| by XREAL_1:20; ::_thesis: verum
end;

theorem Th59: :: COMPLEX1:59
for z1, z2 being complex number holds |.z1.| - |.z2.| <= |.(z1 - z2).|
proof
let z1, z2 be complex number ; ::_thesis: |.z1.| - |.z2.| <= |.(z1 - z2).|
 z1 = (z1 - z2) + z2 ;
then  |.z1.| <= |.(z1 - z2).| + |.z2.| by Th56;
hence  |.z1.| - |.z2.| <= |.(z1 - z2).| by XREAL_1:20; ::_thesis: verum
end;

theorem Th60: :: COMPLEX1:60
for z1, z2 being complex number holds |.(z1 - z2).| = |.(z2 - z1).|
proof
let z1, z2 be complex number ; ::_thesis: |.(z1 - z2).| = |.(z2 - z1).|
thus |.(z1 - z2).| = |.(- (z2 - z1)).|
.= |.(z2 - z1).| by Lm22 ; ::_thesis: verum
end;

theorem Th61: :: COMPLEX1:61
for z1, z2 being complex number holds
( |.(z1 - z2).| = 0 iff z1 = z2 )
proof
let z1, z2 be complex number ; ::_thesis: ( |.(z1 - z2).| = 0 iff z1 = z2 )
thus  ( |.(z1 - z2).| = 0 implies z1 = z2 ) ::_thesis: ( z1 = z2 implies |.(z1 - z2).| = 0 )
proof
assume  |.(z1 - z2).| = 0 ; ::_thesis: z1 = z2
then  z1 - z2 = 0 ;
hence  z1 = z2 ; ::_thesis: verum
end;
thus  ( z1 = z2 implies |.(z1 - z2).| = 0 ) ; ::_thesis: verum
end;

theorem :: COMPLEX1:62
for z1, z2 being complex number holds
( z1 <> z2 iff 0 < |.(z1 - z2).| )
proof
let z1, z2 be complex number ; ::_thesis: ( z1 <> z2 iff 0 < |.(z1 - z2).| )
thus  ( z1 <> z2 implies 0 < |.(z1 - z2).| ) ::_thesis: ( 0 < |.(z1 - z2).| implies z1 <> z2 )
proof
assume  z1 <> z2 ; ::_thesis: 0 < |.(z1 - z2).|
then  |.(z1 - z2).| <> 0 by Th61;
hence  0 < |.(z1 - z2).| ; ::_thesis: verum
end;
thus  ( 0 < |.(z1 - z2).| implies z1 <> z2 ) ; ::_thesis: verum
end;

theorem :: COMPLEX1:63
for z1, z2, z being complex number holds |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
proof
let z1, z2, z be complex number ; ::_thesis: |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).|
 |.(z1 - z2).| = |.((z1 - z) + (z - z2)).| ;
hence  |.(z1 - z2).| <= |.(z1 - z).| + |.(z - z2).| by Th56; ::_thesis: verum
end;

Lm26:  for b, a being real number holds
( ( - b <= a & a <= b ) iff |.a.| <= b )
proof
let b, a be real number ; ::_thesis: ( ( - b <= a & a <= b ) iff |.a.| <= b )
A1: ( |.a.| <= b implies ( - b <= a & a <= b ) )
proof
assume A2: |.a.| <= b ; ::_thesis: ( - b <= a & a <= b )
 ( a < - 0 implies ( - b <= a & a <= b ) )
proof
assume A3: a < - 0 ; ::_thesis: ( - b <= a & a <= b )
then  - a <= b by A2, Lm23;
then  - b <= - (- a) by XREAL_1:24;
hence  ( - b <= a & a <= b ) by A3; ::_thesis: verum
end;
hence  ( - b <= a & a <= b ) by A2, Th43; ::_thesis: verum
end;
 ( - b <= a & a <= b implies |.a.| <= b )
proof
assume that
A4: - b <= a and
A5: a <= b ; ::_thesis: |.a.| <= b
 - a <= - (- b) by A4, XREAL_1:24;
then  ( a < 0 implies |.a.| <= b ) by Lm23;
hence  |.a.| <= b by A5, Th43; ::_thesis: verum
end;
hence  ( ( - b <= a & a <= b ) iff |.a.| <= b ) by A1; ::_thesis: verum
end;

theorem :: COMPLEX1:64
for z1, z2 being complex number holds |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
proof
let z1, z2 be complex number ; ::_thesis: |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).|
 |.z2.| - |.z1.| <= |.(z2 - z1).| by Th59;
then  - (|.z1.| - |.z2.|) <= |.(z1 - z2).| by Th60;
then A1: - |.(z1 - z2).| <= - (- (|.z1.| - |.z2.|)) by XREAL_1:24;
 |.z1.| - |.z2.| <= |.(z1 - z2).| by Th59;
hence  |.(|.z1.| - |.z2.|).| <= |.(z1 - z2).| by A1, Lm26; ::_thesis: verum
end;

theorem Th65: :: COMPLEX1:65
for z1, z2 being complex number holds |.(z1 * z2).| = |.z1.| * |.z2.|
proof
let z1, z2 be complex number ; ::_thesis: |.(z1 * z2).| = |.z1.| * |.z2.|
set r1 = Re z1;
set r2 = Re z2;
set i1 = Im z1;
set i2 = Im z2;
A1: ( 0 <= ((Re z1) ^2) + ((Im z1) ^2) & 0 <= ((Re z2) ^2) + ((Im z2) ^2) ) by Lm1;
A2: (Im (z1 * z2)) ^2 = (((Re z1) * (Im z2)) + ((Re z2) * (Im z1))) ^2 by Th9
.= ((2 * ((Re z1) * (Re z2))) * ((Im z1) * (Im z2))) + ((((Re z1) * (Im z2)) ^2) + (((Re z2) * (Im z1)) ^2)) ;
(Re (z1 * z2)) ^2 = (((Re z1) * (Re z2)) - ((Im z1) * (Im z2))) ^2 by Th9
.= ((((Re z1) * (Re z2)) ^2) + (((Im z1) * (Im z2)) ^2)) + (- ((2 * ((Re z1) * (Re z2))) * ((Im z1) * (Im z2)))) ;
then  ((Re (z1 * z2)) ^2) + ((Im (z1 * z2)) ^2) = (((Re z1) ^2) + ((Im z1) ^2)) * (((Re z2) ^2) + ((Im z2) ^2)) by A2;
hence  |.(z1 * z2).| = |.z1.| * |.z2.| by A1, SQUARE_1:29; ::_thesis: verum
end;

theorem Th66: :: COMPLEX1:66
for z being complex number holds |.(z ").| = |.z.| "
proof
let z be complex number ; ::_thesis: |.(z ").| = |.z.| "
percases ( z <> 0 or z = 0 ) ;
supposeA1: z <> 0 ; ::_thesis: |.(z ").| = |.z.| "
set r2i2 = ((Re z) ^2) + ((Im z) ^2);
A2: ((Re z) ^2) + ((Im z) ^2) <> 0 by A1, Th5;
A3: 0 <= ((Re z) ^2) + ((Im z) ^2) by Lm1;
thus |.(z ").| = sqrt ((((Re z) / (((Re z) ^2) + ((Im z) ^2))) ^2) + ((Im (z ")) ^2)) by Th20
.= sqrt ((((Re z) / (((Re z) ^2) + ((Im z) ^2))) ^2) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) ^2)) by Th20
.= sqrt ((((Re z) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2)) + (((- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) ^2)) by XCMPLX_1:76
.= sqrt ((((Re z) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2)) + (((- (Im z)) ^2) / ((((Re z) ^2) + ((Im z) ^2)) ^2))) by XCMPLX_1:76
.= sqrt ((1 * (((Re z) ^2) + ((Im z) ^2))) / ((((Re z) ^2) + ((Im z) ^2)) * (((Re z) ^2) + ((Im z) ^2)))) by XCMPLX_1:62
.= sqrt (1 / (((Re z) ^2) + ((Im z) ^2))) by A2, XCMPLX_1:91
.= 1 / |.z.| by A3, SQUARE_1:18, SQUARE_1:30
.= |.z.| " by XCMPLX_1:215 ; ::_thesis: verum
end;
supposeA4: z = 0 ; ::_thesis: |.(z ").| = |.z.| "
hence |.(z ").| = 0 "
.= |.z.| " by A4 ;
::_thesis: verum
end;
end;
end;

theorem Th67: :: COMPLEX1:67
for z1, z2 being complex number holds |.z1.| / |.z2.| = |.(z1 / z2).|
proof
let z1, z2 be complex number ; ::_thesis: |.z1.| / |.z2.| = |.(z1 / z2).|
thus |.z1.| / |.z2.| = |.z1.| * (|.z2.| ") by XCMPLX_0:def_9
.= |.z1.| * |.(z2 ").| by Th66
.= |.(z1 * (z2 ")).| by Th65
.= |.(z1 / z2).| by XCMPLX_0:def_9 ; ::_thesis: verum
end;

theorem :: COMPLEX1:68
for z being complex number holds |.(z * z).| = ((Re z) ^2) + ((Im z) ^2)
proof
let z be complex number ; ::_thesis: |.(z * z).| = ((Re z) ^2) + ((Im z) ^2)
 ( 0 <= ((Re z) ^2) + ((Im z) ^2) & |.(z * z).| = |.z.| * |.z.| ) by Lm1, Th65;
then  |.(z * z).| = sqrt ((((Re z) ^2) + ((Im z) ^2)) ^2) by SQUARE_1:29;
hence  |.(z * z).| = ((Re z) ^2) + ((Im z) ^2) by Lm1, SQUARE_1:22; ::_thesis: verum
end;

theorem :: COMPLEX1:69
for z being complex number holds |.(z * z).| = |.(z * (z *')).|
proof
let z be complex number ; ::_thesis: |.(z * z).| = |.(z * (z *')).|
thus |.(z * z).| = |.z.| * |.z.| by Th65
.= |.z.| * |.(z *').| by Th53
.= |.(z * (z *')).| by Th65 ; ::_thesis: verum
end;

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 )
proof
let a be real number ; ::_thesis: ( |.a.| = a or |.a.| = - a )
 ( a >= 0 or a < 0 ) ;
hence  ( |.a.| = a or |.a.| = - a ) by Lm23, Th43; ::_thesis: verum
end;

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
proof
let a, b be real number ; ::_thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2
percases ( a <= b or b <= a ) ;
supposeA1: a <= b ; ::_thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2
|.(a - b).| = |.(- (b - a)).|
.= |.(b - a).| by Lm22
.= b - a by A1, Th43, XREAL_1:48 ;
hence  min (a,b) = ((a + b) - |.(a - b).|) / 2 by A1, XXREAL_0:def_9; ::_thesis: verum
end;
supposeA2: b <= a ; ::_thesis: min (a,b) = ((a + b) - |.(a - b).|) / 2
hence  min (a,b) = ((a + b) - (a - b)) / 2 by XXREAL_0:def_9
.= ((a + b) - |.(a - b).|) / 2 by A2, Th43, XREAL_1:48 ;
::_thesis: verum
end;
end;
end;

theorem :: COMPLEX1:74
for a, b being real number holds max (a,b) = ((a + b) + |.(a - b).|) / 2
proof
let a, b be real number ; ::_thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2
percases ( b <= a or a <= b ) ;
supposeA1: b <= a ; ::_thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2
hence  max (a,b) = ((a + b) + (a - b)) / 2 by XXREAL_0:def_10
.= ((a + b) + |.(a - b).|) / 2 by A1, Th43, XREAL_1:48 ;
::_thesis: verum
end;
supposeA2: a <= b ; ::_thesis: max (a,b) = ((a + b) + |.(a - b).|) / 2
then A3: 0 <= b - a by XREAL_1:48;
thus  max (a,b) = ((a + b) + (- (a - b))) / 2 by A2, XXREAL_0:def_10
.= ((a + b) + |.(- (a - b)).|) / 2 by A3, Th43
.= ((a + b) + |.(a - b).|) / 2 by Lm22 ; ::_thesis: verum
end;
end;
end;

theorem Th75: :: COMPLEX1:75
for a being real number holds |.a.| ^2 = a ^2
proof
let a be real number ; ::_thesis: |.a.| ^2 = a ^2
 ( |.a.| = a or |.a.| = - a ) by Th71;
hence  |.a.| ^2 = a ^2 ; ::_thesis: verum
end;

theorem :: COMPLEX1:76
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:77
for a, b, c, d being real number st a + (b * <i>) = c + (d * <i>) holds
( a = c & b = d )
proof
let a, b, c, d be real number ; ::_thesis: ( a + (b * <i>) = c + (d * <i>) implies ( a = c & b = d ) )
assume A1: a + (b * <i>) = c + (d * <i>) ; ::_thesis: ( a = c & b = d )
then  (a - c) + ((b - d) * <i>) = 0 ;
then  a - c = 0 by Th4, Th12;
hence  ( a = c & b = d ) by A1; ::_thesis: verum
end;

theorem :: COMPLEX1:78
for a, b being real number holds sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b)
proof
let a, b be real number ; ::_thesis: sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b)
A1: (sqrt ((a ^2) + (b ^2))) ^2 >= 0 by XREAL_1:63;
 ( a ^2 >= 0 & b ^2 >= 0 ) by XREAL_1:63;
then A2: (sqrt ((a ^2) + (b ^2))) ^2 = (a ^2) + (b ^2) by SQUARE_1:def_2;
 ( ((abs a) + (abs b)) ^2 = (((abs a) ^2) + ((2 * (abs a)) * (abs b))) + ((abs b) ^2) & (abs a) ^2 = a ^2 ) by Th75;
then (((abs a) + (abs b)) ^2) - ((sqrt ((a ^2) + (b ^2))) ^2) = (((a ^2) + ((2 * (abs a)) * (abs b))) + (b ^2)) - ((a ^2) + (b ^2)) by A2, Th75
.= (2 * (abs a)) * (abs b) ;
then  ((abs a) + (abs b)) ^2 >= (sqrt ((a ^2) + (b ^2))) ^2 by XREAL_1:49;
then  sqrt (((abs a) + (abs b)) ^2) >= sqrt ((sqrt ((a ^2) + (b ^2))) ^2) by A1, SQUARE_1:26;
hence  sqrt ((a ^2) + (b ^2)) <= (abs a) + (abs b) by A2, SQUARE_1:22; ::_thesis: verum
end;

theorem :: COMPLEX1:79
for a, b being real number holds abs a <= sqrt ((a ^2) + (b ^2))
proof
let a, b be real number ; ::_thesis: abs a <= sqrt ((a ^2) + (b ^2))
 ( a ^2 >= 0 & (a ^2) + 0 <= (a ^2) + (b ^2) ) by XREAL_1:6, XREAL_1:63;
then  sqrt (a ^2) <= sqrt ((a ^2) + (b ^2)) by SQUARE_1:26;
hence  abs a <= sqrt ((a ^2) + (b ^2)) by Lm24; ::_thesis: verum
end;

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