COMPLEX1

:: The Complex Numbers
::  by Czes{\l}aw Byli\'nski
::
:: Received March 1, 1990
:: Copyright (c) 1990-2026 Association of Mizar Users
::           (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.

environ

 vocabularies NUMBERS, SUBSET_1, XREAL_0, SQUARE_1, ARYTM_3, CARD_1, XXREAL_0,
      XCMPLX_0, FUNCT_1, FUNCT_2, XBOOLE_0, RELAT_1, REAL_1, FUNCOP_1, ARYTM_0,
      ARYTM_1, COMPLEX1, ORDINAL1;
 notations TARSKI, SUBSET_1, ORDINAL1, ARYTM_0, NUMBERS, XCMPLX_0, XREAL_0,
      REAL_1, SQUARE_1, RELAT_1, FUNCT_1, FUNCT_2, FUNCT_4, XXREAL_0;
 constructors FUNCT_4, ARYTM_0, REAL_1, SQUARE_1, MEMBERED, RELSET_1, XXREAL_0;
 registrations XBOOLE_0, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
      SQUARE_1, ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, ARITHM;
 equalities SQUARE_1;
 theorems SQUARE_1, XREAL_0, FUNCT_2, XBOOLE_0, TARSKI, NUMBERS, FUNCT_4,
      XCMPLX_0, XCMPLX_1, ARYTM_0, XREAL_1, XXREAL_0, CARD_1;

begin

reserve a,b,c,d for Real;

:: Auxiliary theorems

theorem Th1:
  a^2 + b^2 = 0 implies a = 0
proof
  0 <= a^2 & 0 <= b^2 by XREAL_1:63;
  hence thesis;
end;

Lm1: 0 <= a^2 + b^2
proof
  0<=a^2 & 0<=b^2 by XREAL_1:63;
  hence thesis;
end;

:: Complex Numbers

definition
  let z be Complex;
  func Re z -> number means
  :Def1:
  it = z if z is real
  otherwise ex f being Function of 2,REAL st z = f & it = f.0;
  existence
  proof
    thus z is real implies ex IT being set st IT = z
    proof
      assume z is real; then
      z in REAL by XREAL_0:def 1;
      hence thesis;
    end;
A1: z in COMPLEX by XCMPLX_0:def 2;
    assume not z is real; then
    not z in REAL; 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, f;
    thus thesis;
  end;
  uniqueness;
  consistency;
  func Im z -> number means
  :Def2:
  it = 0 if z is real otherwise ex f being Function of
  2,REAL st z = f & it = f.1;
  existence
  proof
    thus z is real implies ex IT being set st IT = 0;
A2: z in COMPLEX by XCMPLX_0:def 2;
    assume not z is real; then
    not z in REAL; 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, f;
    thus thesis;
  end;
  uniqueness;
  consistency;
end;

registration
  let z be Complex;
  cluster Re z -> real;
  coherence
  proof
    per cases;
    suppose
      z is real;
      hence thesis by Def1;
    end;
    suppose
      not 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 thesis by A1;
    end;
  end;
  cluster Im z -> real;
  coherence
  proof
    per cases;
    suppose
      z is real;
      hence thesis by Def2;
    end;
    suppose
      not 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 thesis by A2;
    end;
  end;
end;

definition
  let z be Complex;
  redefine func Re z -> Element of REAL;  :: redefines Re (COMPLEX1, definition)
  coherence by XREAL_0:def 1;
  redefine func Im z -> Element of REAL;  :: redefines Im (COMPLEX1, definition)
  coherence by XREAL_0:def 1;
end;

registration
  let r be Real;
  cluster Im r -> zero;
  coherence by Def2;
end;

theorem Th2:
  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;
  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,b;
  dom f = {0,1} by CARD_1:50,FUNCT_2:def 1;
  hence thesis by FUNCT_4:66;
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;
  reconsider a9 =a, b9 = b as Element of REAL;
  thus Re [*a,b*] = a
  proof
    per cases;
    suppose
      b = 0;
      then [*a,b*] = a by ARYTM_0:def 5;
      hence thesis by Def1;
    end;
    suppose
      b <> 0; 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;
A2:   not [*a,b*] in REAL & f.0 = a by A1,ARYTM_0:8,FUNCT_4:63; then
      not [*a,b*] is real by XREAL_0:def 1;
      hence thesis by Def1,A2;
    end;
  end;
  per cases;
  suppose
A2: b = 0;
    then [*a,b*] = a by ARYTM_0:def 5;
    hence thesis by A2;
  end;
  suppose
    b <> 0;
    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;
A4: not [*a,b*] in REAL & f.1 = b by A3,ARYTM_0:8,FUNCT_4:63; then
    not [*a,b*] is real by XREAL_0:def 1;
    hence thesis by Def2,A4;
  end;
end;

reserve z,z1,z2 for Complex;

Lm3: [*Re z, Im z*] = z
proof
A1: z in COMPLEX by XCMPLX_0:def 2;
  per cases;
  suppose
A2: z is real;
    then Im z = 0;
    hence [*Re z, Im z*] = Re z by ARYTM_0:def 5
      .= z by A2,Def1;
  end;
  suppose
A3: not z is real; then
a3: not z in REAL;
A4: ex f being Function of 2,REAL st z = f & Im z = f.1 by Def2,A3;
    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 thesis by A5,A7,A6,ARYTM_0:def 5;
  end;
end;

theorem Th3:
  Re z1 = Re z2 & Im z1 = Im z2 implies z1 = z2
proof
  assume Re z1 = Re z2 & Im z1 = Im z2;
  hence z1 = [*Re z2,Im z2*] by Lm3
    .= z2 by Lm3;
end;

definition
  let z1,z2 be Complex;
  redefine pred z1 = z2 means  :: redefines = (HIDDEN, definition)
  Re z1 = Re z2 & Im z1 = Im z2;
  compatibility by Th3;
end;

notation
  synonym 0c for 0;
end;

definition
  redefine func 0c -> Element of COMPLEX;  :: redefines 0c (COMPLEX1, synonym) → 0 (ORDINAL1, definition)
  correctness by XCMPLX_0:def 2;
end;

definition
  func 1r -> Element of COMPLEX equals
  1;
  correctness by XCMPLX_0:def 2;
  redefine func <i> -> Element of COMPLEX;  :: redefines <i> (XCMPLX_0, definition)
  coherence by XCMPLX_0:def 2;
end;

theorem Th4:
  Re 0 = 0 & Im 0 = 0
proof
  reconsider zz=0 as Element of REAL by XREAL_0:def 1;
  0 = [*zz,zz*] by ARYTM_0:def 5;
  hence thesis by Lm2;
end;

theorem Th5:
  z = 0 iff (Re z)^2 + (Im z)^2 = 0
by Th4,Th1;

theorem Th6:
  Re(1r) = 1 & Im(1r) = 0
proof
  reconsider zz=0,j=1 as Element of REAL by XREAL_0:def 1;
  1r = [*j,zz*] by ARYTM_0:def 5;
  hence thesis by Lm2;
end;


theorem Th7:
  Re(<i>) = 0 & Im(<i>) = 1
proof
  reconsider zz=0,j=1 as Element of REAL by XREAL_0:def 1;
  <i> = [*zz,j*] by ARYTM_0:def 5,XCMPLX_0:def 1;
  hence thesis by Lm2;
end;

Lm7: for x being Real, x1,x2 being Element of REAL st x = [*x1,x2*]
holds x2 = 0 & x = x1
proof
  let x be Real, x1,x2 being Element of REAL;
  assume
A1: x = [*x1,x2*];
A2: x in REAL by XREAL_0:def 1;
  hereby
    assume x2 <> 0;
    then x = (0,1) --> (x1,x2) by A1,ARYTM_0:def 5;
    hence contradiction by A2,ARYTM_0:8;
  end;
  hence thesis by A1,ARYTM_0:def 5;
end;

Lm8: for x9,y9 being Element of REAL, x,y being Real st x9 = x & y9 = y
holds +(x9,y9) = x + y
proof
  let x9,y9 be Element of REAL, x,y be Real such that
A1: x9 = x & y9 = 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 thesis by A1,A3,A4,ARYTM_0:def 5;
end;

Lm9: for x being Element of REAL holds opp x = -x
proof
  let x be Element of REAL;
  +(x,opp x) = 0 by ARYTM_0:def 3;
  then x + opp x = 0 by Lm8;
  hence thesis;
end;

Lm10: for x9,y9 being Element of REAL, x,y being Real st x9 = x & y9 =
y holds *(x9,y9) = x * y
proof
  let x9,y9 be Element of REAL, x,y be Real such that
A1: x9 = x & y9 = 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,12
    .= +(*(x1,y1),opp*(x2,y2)) by ARYTM_0:15
    .= x * y by A4,A7,ARYTM_0:def 5;
end;

Lm11: for x,y,z being Complex st z = x + y holds Re z = Re x + Re y
proof
  let x,y,z be Complex such that
A1: z = 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;
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;
end;

Lm12: for x,y,z being Complex st z = x+y holds Im z = Im x + Im y
proof
  let x,y,z be Complex such that
A1: z = 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;
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;
end;

Lm13: for x,y,z being Complex st z = x * y holds Re z = Re x * Re y -
Im x * Im y
proof
  let x,y,z be Complex such that
A1: z = 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),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;
end;

Lm14: for x,y,z being Complex st z = x*y holds Im z = Re x * Im y + Im
x * Re y
proof
  let x,y,z be Complex such that
A1: z = 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),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;
end;

Lm15: z1+z2 = [* Re z1 + Re z2, Im z1 + Im z2 *]
proof
  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 z = Im z1 + Im z2 by Lm2
    .= Im z9 by Lm12;
  Re z = Re z1 + Re z2 by Lm2
    .= Re z9 by Lm11;
  hence thesis by A1;
end;

Lm16: z1 * z2 = [* Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im
z1 *]
proof
  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 z = Re z1 * Im z2 + Re z2 * Im z1 by Lm2
    .= Im z9 by Lm14;
  Re z = Re z1 * Re z2 - Im z1 * Im z2 by Lm2
    .= Re z9 by Lm13;
  hence thesis by A1;
end;

Lm17: Re(z1 * z2) = Re z1 * Re z2 - Im
z1 * Im z2 & Im(z1 * z2) = Re z1 * Im z2 + Re z2 * Im z1
proof
  z1 * z2 = [*Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im z1
  *] by Lm16;
  hence thesis by Lm2;
end;

Lm18: Re(z1 + z2) = Re z1 + Re z2 & Im(z1 + z2) = Im z1 + Im z2
proof
  (z1 + z2) = [* Re z1 + Re z2, Im z1 + Im z2 *] by Lm15;
  hence thesis by Lm2;
end;

Lm19: for x being Element of REAL holds Re (x*<i>) = 0
proof
  let x be Element of REAL;
  thus Re (x*<i>) = Re x * Re (<i>) - Im x * Im (<i>) by Lm17
    .= Re x * 0 - 0 * Im (<i>) by Th7
    .= 0;
end;

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

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

definition
::$CD
end;

theorem Th8:
  Re(z1 + z2) = Re z1 + Re z2 & Im(z1 + z2) = Im z1 + Im z2
proof
  (z1 + z2) = [* Re z1 + Re z2, Im z1 + Im z2 *] by Lm15;
  hence thesis by Lm2;
end;

definition
::$CD
end;

theorem Th9:
  Re(z1 * z2) = Re z1 * Re z2 - Im z1 * Im z2 &
  Im(z1 * z2) = Re z1 * Im z2 + Re z2 * Im z1
proof
  z1 * z2 = [*Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im z1
  *] by Lm16;
  hence thesis by Lm2;
end;

theorem
  Re (a*<i>) = 0
proof
  thus Re (a*<i>) = Re a * Re (<i>) - Im a * Im (<i>) by Th9
  .= Re a * 0 - 0 * Im (<i>) by Th7
  .= 0;
end;

theorem
  Im (a*<i>) = a
proof
  thus Im (a*<i>) = Re a * Im (<i>) + Im a * Re (<i>) by Th9
  .= a by Def1,Th7;
end;

theorem Th12:
  Re(a+b*<i>) = a & Im(a+b*<i>) = b
proof
  reconsider a,b as Element of REAL by XREAL_0:def 1;
  (a+b*<i>) = [*a,b*] by Lm21;
  hence thesis by Lm2;
end;

theorem Th13:
  Re z+(Im z)*<i> = z
proof
  [*Re z, Im z*] = z by Lm3;
  hence thesis by Lm21;
end;

theorem Th14:
  Im z1 = 0 & Im z2 = 0 implies Re(z1*z2) = Re z1 * Re z2 & Im(z1*z2) = 0
proof
  assume that
A1: Im z1 = 0 and
A2: Im z2 = 0;
  thus Re(z1*z2) = Re z1 * Re z2 - Im z1 * Im z2 by Th9
    .= Re z1 * Re z2 by A1;
  thus Im(z1*z2) = Re z1 * Im z2 + Re z2 * Im z1 by Th9
    .= 0 by A1,A2;
end;

theorem Th15:
  Re z1 = 0 & Re z2 = 0 implies Re(z1*z2) = - Im z1 * Im z2 & Im(z1*z2) = 0
proof
  assume that
A1: Re z1 = 0 and
A2: Re z2 = 0;
  thus Re(z1*z2) = Re z1 * Re z2 - Im z1 * Im z2 by Th9
    .= - Im z1 * Im z2 by A1;
  thus Im(z1*z2) = Re z1 * Im z2 + Re z2 * Im z1 by Th9
    .= 0 by A1,A2;
end;

theorem
  Re(z*z) = (Re z)^2 - (Im z)^2 & Im(z*z) = 2*(Re z *Im z)
proof
  thus Re(z*z) = (Re z)^2 - (Im z)^2 by Th9;
  thus Im(z*z) = Re z *Im z + Re z *Im z by Th9
    .= 2*(Re z *Im z);
end;

definition
::$CD
end;

Lm22: for z being Complex holds -z = -Re z+(-Im z)*<i>
proof let z be Complex;
    reconsider zz=0 as Element of REAL by XREAL_0:def 1;
    set z9 = [* -Re z, -Im z *];
    z9 + z = [* Re z9 + Re z, Im z9 + Im z *] by Lm15
      .= [* -Re z + Re z, Im z9 + Im z *] by Lm2
      .= [* zz, -Im z + Im z *] by Lm2
      .= 0 by ARYTM_0:def 5;
 hence thesis by Lm21;
end;

theorem Th17:
  Re(-z) = -(Re z) & Im(-z) = -(Im z)
proof
  -z = -Re z+(-Im z)*<i> by Lm22;
  hence thesis by Th12;
end;

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

definition
::$CD
end;

Lm23: for z1,z2 being Complex holds
   z1 - z2 =  Re z1 - Re z2 + (Im z1 - Im z2)*<i>
proof let z1,z2 be Complex;
A1: z1 = Re z1 + (Im z1)*<i> by Th13;
    z1 - z2 = z1 + -z2 .= z1 + (-Re z2+(-Im z2)*<i>) by Lm22
      .= Re z1 - Re z2 + (Im z1 - Im z2)*<i> by A1;
 hence thesis;
end;

theorem Th19:
  Re(z1 - z2) = Re z1 - Re z2 & Im(z1 - z2) = Im z1 - Im z2
proof
    thus Re(z1 - z2) = Re(Re z1 - Re z2 + (Im z1 - Im z2)*<i>) by Lm23
    .= Re z1 - Re z2 by Th12;
  thus Im(z1 - z2) = Im(Re z1 - Re z2 + (Im z1 - Im z2)*<i>) by Lm23
    .= Im z1 - Im z2 by Th12;
end;

definition
::$CD
end;

Lm24: for z being Complex
  holds z"  = Re z / ((Re z)^2+(Im z)^2)+((- Im z) / ((Re z)^2+(Im z)^2))*<i>
proof let z be Complex;
    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;
    per cases;
    suppose
      z = 0;
      hence thesis by Th4;
    end;
    suppose
A1:   z <> 0;
      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 thesis by A1,XCMPLX_0:def 7;
    end;
end;

theorem Th20:
  Re(z") = Re z / ((Re z)^2+(Im z)^2) &
  Im(z") = (- Im z) / ((Re z)^2+(Im z)^2)
proof
  z" = Re z / ((Re z)^2+(Im z)^2)+((- Im z) / ((Re z)^2+(Im z)^2))*<i>
  by Lm24;
  hence thesis by Th12;
end;

theorem
  <i>" = -<i>;

theorem Th22:
  Re z <> 0 & Im z = 0 implies Re(z") = (Re z)" & Im(z") = 0
proof
  assume that
A1: Re z <> 0 and
A2: 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;
  Im(z") = (- Im z) / ((Re z)^2+(Im z)^2) by Th20;
  hence thesis by A2;
end;

theorem Th23:
  Re z = 0 & Im z <> 0 implies Re(z") = 0 & Im(z") = -(Im z)"
proof
  assume that
A1: Re z = 0 and
A2: Im z <> 0;
  Re(z") = Re z / ((Re z)^2+(Im z)^2) by Th20;
  hence Re(z") = 0 by A1;
  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;
end;

definition
::$CD
end;

Lm25: for z1,z2 being Complex
  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>
proof let z1,z2 be Complex;
    reconsider z1,z2 as Element of COMPLEX by XCMPLX_0:def 2;
    reconsider k = (Re z2)^2 + (Im z2)^2 as Element of REAL by XREAL_0:def 1;
    reconsider r = Re z2/k, i = (-Im z2)/k as Element of REAL;
A1: Re[*r,i*] = Re(Re z2/k+(-Im z2)/k*<i>) by Lm21
      .= Re z2/k by Th12;
A2: Im[*r,i*] = Im(Re z2/k+(-Im z2)/k*<i>) by Lm21
      .= (-Im z2)/k by Th12;
    reconsider r1 = (Re z1)/1 * (Re z2/k) - Im z1 * ((-Im z2)/k),
        i1 =Re z1 * ((-Im z2)/k) + (Re z2/k) * Im z1
      as Element of REAL by XREAL_0:def 1;
    z1 / z2 = z1 * z2" by XCMPLX_0:def 9
      .= z1*(r+i*<i>) by Lm24
      .= z1*[*r,i*] by Lm21
      .= [* r1, i1 *] by A1,A2,Lm16
      .= (Re z1)/1 * (Re z2/k) - Im z1 * ((-Im z2)/k)+ (Re z1 * ((-Im z2)/k)
    + (Re z2/k) * Im z1)*<i> by Lm21
      .= Re z1 * Re z2/(1*k) - (Im z1)/1 * ((-Im z2)/k)+ (Re z1 * ((-Im z2)/
    k) + (Re z2/k) * Im z1)*<i> by XCMPLX_1:76
      .= Re z1 * Re z2/k - Im z1 * (-Im z2)/(1*k)+ ((Re z1)/1 * ((-Im z2)/k)
    + (Re z2/k) * Im z1)*<i> by XCMPLX_1:76
      .= Re z1 * Re z2/k - Im z1 * (-Im z2)/k+ (Re z1 * (-Im z2)/(1*k) + (Re
    z2/k) * ((Im z1)/1))*<i> by XCMPLX_1:76
      .= Re z1 * Re z2/k - Im z1 * (-Im z2)/k+ (Re z1 * (-Im z2)/k + Im z1 *
    Re z2/(1*k))*<i> by XCMPLX_1:76
      .= (Re z1 * Re z2 - Im z1 * (-Im z2))/k+ (Re z1 * (-Im z2)/k + Im z1 *
    Re z2/(1*k))*<i> by XCMPLX_1:120
      .= (Re z1 * Re z2 + Im z1 * Im z2)/k+ ((-Re z1 * Im z2 + Im z1 * Re z2
    )/k)*<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 thesis;
end;

theorem
  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
  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 Lm25
    .= (Re z1 * Re z2 + Im z1 * Im z2) / ((Re z2)^2 + (Im z2)^2) by Th12;
  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 Lm25
    .= (Re z2 * Im z1 - Re z1 * Im z2) / ((Re z2)^2 + (Im z2)^2) by Th12;
end;

theorem
  Im z1 = 0 & Im z2 = 0 & Re z2 <> 0 implies Re(z1/z2) = (Re z1)/(Re z2)
  & Im(z1/z2) = 0
proof
  assume that
A1: Im z1 = 0 and
A2: Im z2 = 0 & Re 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;
  thus thesis by A1,A3,Th14;
end;

theorem
  Re z1 = 0 & Re z2 = 0 & Im z2 <> 0 implies Re(z1/z2) = (Im z1)/(Im z2)
  & Im(z1/z2) = 0
proof
  assume that
A1: Re z1 = 0 and
A2: Re z2 = 0 & Im 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;
  thus thesis by A1,A3,Th15;
end;

definition
  let z be Complex;
  func z*' -> Complex equals
  Re z-(Im z)*<i>;
  correctness;
  involutiveness
  proof
    let z,z9 be Complex;
    assume z = Re z9-(Im z9)*<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>;
  end;
end;

theorem Th27:
  Re (z*') = Re z & Im (z*') = -Im z
proof
  z*' = Re z+(-Im z)*<i>;
  hence thesis by Th12;
end;

theorem
  0*' = 0 by Th4;

theorem
  z*' = 0 implies z = 0
proof
  assume z*' = 0;
  then 0 = Re z+(-Im z)*<i>;
  hence Re z = Re 0 & Im z = Im 0 by Th12;
end;

theorem
  1r*' = 1r by Th6;

theorem
  <i>*' = -<i> by Th7;

theorem Th32:
  (z1 + z2)*' = z1*' + z2*'
proof
  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;
  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;
end;

theorem Th33:
  (-z)*' = -(z*')
proof
  thus Re ((-z)*') = Re -z by Th27
    .= - Re z by Th17
    .= - Re (z*') by Th27
    .= Re -(z*') by Th17;
  thus Im ((-z)*') = -Im -z by Th27
    .= - -Im z by Th17
    .= - Im (z*') by Th27
    .= Im -(z*') by Th17;
end;

theorem
  (z1 - z2)*' = z1*' - z2*'
proof
  thus (z1 - z2)*' = (z1 + -z2)*' .= z1*' + (-z2)*' by Th32
    .= z1*' + -(z2*') by Th33
    .= z1*' - z2*';
end;

theorem Th35:
  (z1*z2)*' = z1*'*z2*'
proof
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;
  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;
end;

theorem Th36:
  z"*' = z*'"
proof
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*')) / ((Re (z*'))^2+(Im (z*'))^2) by A1
    .= Re(z*'") by Th20;

  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;
end;

theorem
  (z1/z2)*' = (z1*')/(z2*')
proof
  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;
end;

theorem Th38:
  Im z = 0 implies z*' = z
by Th27;

registration
  let r be Real;
  reduce r*' to r;
  reducibility by Th38;
end;

theorem
  Re z = 0 implies z*' = -z
proof
  assume
A1: Re z = 0;
  hence z*' = -0+(-Im z)*<i> .= -z by A1,Lm22;
end;

theorem
  Re(z*z*') = (Re z)^2 + (Im z)^2 & Im(z*z*') = 0
proof
  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;
  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;
end;

theorem
  Re(z + z*') = 2*Re z & Im(z + z*') = 0
proof
  thus Re(z + z*') = Re z + Re (z*') by Th8
    .= Re z + Re z by Th27
    .= 2*Re z;
  thus Im(z + (z*')) = Im z + Im (z*') by Th8
    .= Im z + -Im z by Th27
    .= 0;
end;

theorem
  Re(z - z*') = 0 & Im(z - z*') = 2*Im z
proof
  thus Re(z - z*') = Re z - Re (z*') by Th19
    .= Re z - Re z by Th27
    .= 0;
  thus Im(z - z*') = Im z - Im (z*') by Th19
    .= Im z - -Im z by Th27
    .= 2*Im z;
end;

definition
  let z be Complex;
  func |.z.| -> Real equals
  sqrt ((Re z)^2 + (Im z)^2);
  coherence;
  projectivity
  proof
    let r be Real;
     reconsider rr = r as Element of REAL by XREAL_0:def 1;
    let z be Complex;
    assume
A1: r = sqrt ((Re z)^2 + (Im z)^2);
    (Re z)^2 >= 0 & (Im z)^2 >= 0 by XREAL_1:63;
    then r >= 0 by A1,SQUARE_1:def 2;
    then
A2: Re rr >= 0 by Def1;
    thus r = Re rr by Def1
      .= sqrt ((Re r)^2 + (Im r)^2) by A2,SQUARE_1:22;
  end;
end;

theorem Th43:
  a >= 0 implies |.a.| = a
proof
  assume a >= 0;
  then Re a >= 0 by Def1;
  hence |.a.| = Re a by SQUARE_1:22
  .= a by Def1;
end;

registration let z be zero Complex;
  cluster |.z.| -> zero;
  coherence by Th4;
end;

theorem
  |.0.| = 0;

registration
  let z be non zero Complex;
  cluster |.z.| -> non zero;
  coherence
  proof
    assume |.z.| is zero;
    then (Re z)^2 + (Im z)^2 = 0 by Lm1,SQUARE_1:24;
    hence thesis by Th5;
  end;
end;

theorem
  |.z.| = 0 implies z = 0;

registration
  let z;
  cluster |.z.| -> non negative;
  coherence
  proof
    0 <= (Re z)^2 + (Im z)^2 by Lm1;
    hence thesis by SQUARE_1:def 2;
  end;
end;

theorem
  0 <= |.z.|;

theorem
  z <> 0 iff 0 < |.z.|;

theorem Th48:
  |.1r.| = 1 by Th6;

theorem
  |.<i>.| = 1 by Th7;

Lm26: |.-z.| = |.z.|
proof
  thus |.-z.| = sqrt ((-Re z)^2 + (Im -z)^2) by Th17
    .= sqrt ((-Re z)^2 + (-Im z)^2) by Th17
    .= |.z.|;
end;

Lm27: a <= 0 implies |.a.| = -a
proof
  assume a <= 0;
  then |.-a.| = -a by Th43;
  hence thesis by Lm26;
end;

Lm28: sqrt a^2 = |.a.|
proof
  per cases;
  suppose
A1: 0 <= a;
    then sqrt a^2 = a by SQUARE_1:22;
    hence thesis by A1,Th43;
  end;
  suppose
A2: not 0 <= a;
    then |.a.| = -a by Lm27;
    hence thesis by A2,SQUARE_1:23;
  end;
end;

theorem
  Im z = 0 implies |.z.| = |.Re z.| by Lm28;

theorem
  Re z = 0 implies |.z.| = |.Im z.| by Lm28;

theorem
  |.-z.| = |.z.| by Lm26;

theorem Th53:
  |.z*'.| = |.z.|
proof
  thus |.z*'.| = sqrt ((Re z)^2 + (Im (z*'))^2) by Th27
    .= sqrt ((Re z)^2 + (-Im z)^2) by Th27
    .= |.z.|;
end;

Lm29: -|.a.| <= a & a <= |.a.|
proof
  a < 0 implies -|.a.| <= a & a <= |.a.|
  proof
    assume a < 0;
    then |.a.| = -a by Lm27;
    hence thesis;
  end;
  hence thesis by Th43;
end;

theorem
  Re z <= |.z.|
proof
  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 Lm28;
  Re z <= |.Re z.| by Lm29;
  hence thesis by A2,XXREAL_0:2;
end;

theorem
  Im z <= |.z.|
proof
  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 Lm28;
  Im z <= |.Im z.| by Lm29;
  hence thesis by A2,XXREAL_0:2;
end;

::$L https://en.wikipedia.org/wiki/Triangle_inequality The Triangle Inequality
theorem Th56:
  |.z1 + z2.| <= |.z1.| + |.z2.|
proof
  set r1 = Re z1, r2 = Re z2, i1 = Im z1, i2 = Im z2;
A1: (Im(z1 + z2))^2 = (i1 + i2)^2 by Th8
    .= i1^2 + 2*i1*i2 + i2^2;
A2: 0 <= r1^2+i1^2 by Lm1;
  (r1^2+i1^2)*(r2^2+i2^2)-(r1*r2+i1*i2)^2 = (r1*i2-i1*r2)^2;
  then 0 <= (r1^2+i1^2)*(r2^2+i2^2)-(r1*r2+i1*i2)^2 by XREAL_1:63;
  then
A3: (r1*r2+i1*i2)^2+0 <= (r1^2+i1^2)*(r2^2+i2^2) by XREAL_1:19;
  r1*r2+i1*i2 <= |.r1*r2+i1*i2.| by Lm29;
  then
A4: r1*r2+i1*i2 <= sqrt (r1*r2+i1*i2)^2 by Lm28;
A5: 0 <= r2^2+i2^2 by Lm1;
  then
A6: (sqrt (r2^2+i2^2))^2 = r2^2+i2^2 by SQUARE_1:def 2;
  0<=(r1*r2+i1*i2)^2 by XREAL_1:63;
  then sqrt (r1*r2+i1*i2)^2 <= sqrt ((r1^2+i1^2)*(r2^2+i2^2)) by A3,SQUARE_1:26
;
  then sqrt (r1*r2+i1*i2)^2 <= sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2) by A2,A5,
SQUARE_1:29;
  then
A7: r1*r2 + i1*i2 <= sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2) by A4,XXREAL_0:2;
  (2*r1*r2 + 2*i1*i2) = 2*(r1*r2 + i1*i2);
  then (2*r1*r2 + 2*i1*i2) <= 2*(sqrt (r1^2+i1^2)*sqrt (r2^2+i2^2)) by A7,
XREAL_1:64;
  then
A8: (r1^2 + i1^2)+(2*r1*r2+2*i1*i2) <= (r1^2+i1^2)+2*sqrt (r1^2+i1^2)*sqrt
  (r2^2+i2^2) by XREAL_1:7;
  (Re(z1 + z2))^2 = (r1+ r2)^2 by Th8
    .= r1^2 + 2*r1*r2 + r2^2;
  then
  (Re(z1+z2))^2+(Im(z1+z2))^2 = r1^2 + i1^2 + (2*r1*r2 + 2*i1*i2) + (r2^2
  + i2^2) by A1;
  then
A9: (Re(z1+z2))^2+(Im(z1+z2))^2 <= (r1^2+i1^2)+2*sqrt (r1^2+i1^2)*sqrt (r2
  ^2+i2^2)+(r2^2+i2^2) by A8,XREAL_1:7;
A10: 0 <= (Re(z1 + z2))^2 + (Im(z1 + z2))^2 by Lm1;
  (sqrt (r1^2+i1^2))^2 = r1^2+i1^2 by A2,SQUARE_1:def 2;
  then sqrt ((Re(z1 + z2))^2 + (Im(z1 + z2))^2) <= sqrt ((sqrt (r1^2+i1^2) +
  sqrt (r2^2+i2^2))^2) by A6,A9,A10,SQUARE_1:26;
  hence thesis by SQUARE_1:22;
end;

theorem Th57:
  |.z1 - z2.| <= |.z1.| + |.z2.|
proof
  |.z1 - z2.| = |.z1 + - z2.|;
  then |.z1 - z2.| <= |.z1.| + |.-z2.| by Th56;
  hence thesis by Lm26;
end;

theorem
  |.z1.| - |.z2.| <= |.z1 + z2.|
proof
  z1 = z1 + z2 - z2;
  then |.z1.| <= |.z1 + z2.| + |.z2.| by Th57;
  hence thesis by XREAL_1:20;
end;

theorem Th59:
  |.z1.| - |.z2.| <= |.z1 - z2.|
proof
  z1 = z1 - z2 + z2;
  then |.z1.| <= |.z1 - z2.| + |.z2.| by Th56;
  hence thesis by XREAL_1:20;
end;

theorem Th60:
  |.z1 - z2.| = |.z2 - z1.|
proof
  thus |.z1 - z2.| = |.-(z2 - z1).| .= |.z2 - z1.| by Lm26;
end;

theorem Th61:
  |.z1 - z2.| = 0 iff z1 = z2
proof
  thus |.z1 - z2.| = 0 implies z1 = z2
  proof
    assume |.z1 - z2.| = 0;
    then z1 - z2 = 0;
    hence thesis;
  end;
  thus thesis;
end;

theorem
  z1 <> z2 iff 0 < |.z1 - z2.|
proof
  thus z1 <> z2 implies 0 < |.z1 - z2.|
  proof
    assume z1 <> z2;
    then |.z1 - z2.| <> 0 by Th61;
    hence thesis;
  end;
  thus thesis;
end;

theorem
  |.z1 - z2.| <= |.z1 - z.| + |.z - z2.|
proof
  |.z1 - z2.| = |.(z1 - z) + (z - z2).|;
  hence thesis by Th56;
end;

Lm30: -b <= a & a <= b iff |.a.| <= b
proof
A1: |.a.| <= b implies -b <= a & a <= b
  proof
    assume
A2: |.a.| <= b;
 a < -0 implies -b <= a & a <= b
    proof
      assume
A3:   a < -0;
      then -a <= b by A2,Lm27;
      then -b <= -(-a) by XREAL_1:24;
      hence thesis by A3;
    end;
    hence thesis by A2,Th43;
  end;
  -b <= a & a <= b implies |.a.| <= b
  proof
    assume that
A4: -b <= a and
A5: a <= b;
    -a <= -(-b) by A4,XREAL_1:24;
    then a < 0 implies |.a.| <= b by Lm27;
    hence thesis by A5,Th43;
  end;
  hence thesis by A1;
end;

theorem
  |.|.z1.| - |.z2.|.| <= |.z1 - z2.|
proof
  |.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 thesis by A1,Lm30;
end;

theorem Th65:
  |.z1*z2.| = |.z1.|*|.z2.|
proof
  set r1 = Re z1, r2 = Re z2, i1 = Im z1, i2 = Im z2;
A1: 0<=r1^2 + i1^2 & 0<=r2^2 + i2^2 by Lm1;
A2: (Im(z1*z2))^2 = (r1*i2 + r2*i1)^2 by Th9
    .= 2*(r1*r2)*(i1*i2) + ((r1*i2)^2 + (r2*i1)^2);
  (Re(z1*z2))^2 = (r1*r2 - i1*i2)^2 by Th9
    .= (r1*r2)^2 + (i1*i2)^2 + - 2*(r1*r2)*(i1*i2);
  then (Re(z1*z2))^2+(Im(z1*z2))^2 = (r1^2 + i1^2)*(r2^2 + i2^2) by A2;
  hence thesis by A1,SQUARE_1:29;
end;

theorem Th66:
  |.z".| = |.z.|"
proof
  per cases;
  suppose
A1: z <> 0;
    set r2i2 = (Re z)^2+(Im z)^2;
A2: r2i2 <> 0 by A1,Th5;
A3: 0 <= r2i2 by Lm1;
    thus |.z".| = sqrt ((Re z / r2i2)^2 + (Im(z"))^2) by Th20
      .= sqrt ((Re z / r2i2)^2 + ((-Im z) / r2i2)^2) by Th20
      .= sqrt ((Re z)^2 / r2i2^2 + ((-Im z) / r2i2)^2) by XCMPLX_1:76
      .= sqrt ((Re z)^2 / r2i2^2 + (-Im z)^2 / r2i2^2) by XCMPLX_1:76
      .= sqrt ((1*r2i2) / (r2i2*r2i2)) by XCMPLX_1:62
      .= sqrt (1 / r2i2) by A2,XCMPLX_1:91
      .= 1 / |.z.| by A3,SQUARE_1:18,30
      .= |.z.|" by XCMPLX_1:215;
  end;
  suppose
A4: z = 0;
    hence |.z".| = 0" .= |.z.|" by A4;
  end;
end;

theorem Th67:
  |.z1.| / |.z2.| = |.z1/z2.|
proof
  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;
end;

theorem
  |.z*z.| = (Re z)^2 + (Im z)^2
proof
  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 thesis by Lm1,SQUARE_1:22;
end;

theorem
  |.z*z.| = |.z*z*'.|
proof
  thus |.z*z.| = |.z.|*|.z.| by Th65
    .= |.z.|*|.z*'.| by Th53
    .= |.z*z*'.| by Th65;
end;

:: Originally from SQUARE_1

theorem
  a <= 0 implies |.a.| = -a by Lm27;

theorem Th71:
  |.a.| = a or |.a.| = -a
proof
  a >= 0 or a < 0;
  hence thesis by Lm27,Th43;
end;

theorem :: SQUARE_1'91
  sqrt a^2 = |.a.| by Lm28;

theorem :: SQUARE_1'34
  min(a,b) = (a + b - |.a - b.|) / 2
proof
  per cases;
  suppose
A1: a <= b;
    |.a - b.| = |.-(b - a).| .= |.b - a.| by Lm26
      .= b - a by A1,Th43,XREAL_1:48;
    hence thesis by A1,XXREAL_0:def 9;
  end;
  suppose
A2: b <= a;
    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;
  end;
end;

theorem :: SQUARE_1'45
  max(a,b) = (a + b + |.a - b.|) / 2
proof
  per cases;
  suppose
A1: b <= a;
    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;
  end;
  suppose
A2: a <= b;
    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 Lm26;
  end;
end;

theorem Th75: :: SQUARE_1'62
  |.a.|^2 = a^2
proof
  |.a.| = a or |.a.| = -a by Th71;
  hence thesis;
end;

theorem
  -|.a.| <= a & a <= |.a.| by Lm29;

theorem
  a+b*<i> = c+d*<i> implies a = c & b = d
proof
  assume
A1: a+b*<i> = c+d*<i>;
  then a-c+(b-d)*<i> = 0;
  then a-c = 0 by Th4,Th12;
  hence thesis by A1;
end;

:: from JGRAPH_1, 29.12.2006, AK

theorem
  sqrt(a^2+b^2) <= |.a.|+|.b.|
proof
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;
  (|.a.|+|.b.|)^2=(|.a.|)^2+2*(|.a.|)*(|.b.|)+(|.b.|)^2 & |.a.|^2=a^2
           by Th75;
  then
  (|.a.|+|.b.|)^2 - (sqrt(a^2+b^2))^2= a^2+2*(|.a.|)*(|.b.|)+b
  ^2-(a^2+b^2) by A2,Th75
    .=2*(|.a.|)*(|.b.|);
  then (|.a.|+|.b.|)^2>= (sqrt(a^2+b^2))^2 by XREAL_1:49;
  then sqrt((|.a.|+|.b.|)^2)>=sqrt((sqrt(a^2+b^2))^2) by A1,SQUARE_1:26;
  hence thesis by A2,SQUARE_1:22;
end;

theorem
  |.a.| <= sqrt(a^2+b^2)
proof
  a^2>=0 & a^2+0<= a^2+b^2 by XREAL_1:6,63;
  then sqrt(a^2)<= sqrt(a^2+b^2) by SQUARE_1:26;
  hence thesis by Lm28;
end;

theorem
|. 1/z1 .| = 1 / |.z1.| by Th48,Th67;

theorem
 for z1,z2 being Complex
  holds z1 + z2 =  Re z1 + Re z2 + (Im z1 + Im z2)*<i>
proof let z1,z2 be Complex;
    z1 + z2 = [* Re z1 + Re z2, Im z1 + Im z2 *] by Lm15;
 hence thesis by Lm21;
end;

theorem
 for z1,z2 being Complex holds
  z1 * z2 = Re z1 * Re z2 - Im z1 * Im z2+(Re z1 * Im z2 + Re z2 * Im z1)*<i>
proof let z1,z2 be Complex;
  z1 * z2 = [* Re z1 * Re z2 - Im z1 * Im z2, Re z1 * Im z2 + Re z2 * Im
    z1 *] by Lm16;
 hence thesis by Lm21;
end;

theorem
 for z being Complex holds -z = -Re z+(-Im z)*<i> by Lm22;

theorem
 for z1,z2 being Complex holds
   z1 - z2 =  Re z1 - Re z2 + (Im z1 - Im z2)*<i> by Lm23;

theorem
 for z being Complex
  holds z"  = Re z / ((Re z)^2+(Im z)^2)+((- Im z) / ((Re z)^2+(Im z)^2))*<i>
    by Lm24;

theorem
 for z1,z2 being Complex
  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> by Lm25;