COMPLFLD

:: The Field of Complex Numbers
::  by Anna Justyna Milewska
::
:: Received January 18, 2000
:: Copyright (c) 2000-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 STRUCT_0, ALGSTR_0, NUMBERS, BINOP_2, MESFUNC1, COMPLEX1,
      SUPINF_2, XBOOLE_0, XCMPLX_0, SUBSET_1, ORDINAL1, ARYTM_3, FUNCT_1,
      RELAT_1, VECTSP_1, GROUP_1, RLVECT_1, BINOP_1, LATTICES, ARYTM_1, CARD_1,
      XXREAL_0, NAT_1, NEWTON, COMPTRIG, COMPLFLD, MEMBERED;
 notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1,
      REAL_1, NAT_1, MEMBERED, FUNCT_1, XXREAL_0, COMPTRIG, BINOP_1, BINOP_2,
      STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, NEWTON, VECTSP_1;
 constructors BINOP_1, XXREAL_0, REAL_1, NAT_1, BINOP_2, NEWTON, COMPTRIG,
      VECTSP_1, RLVECT_1, GROUP_1, MEMBERED;
 registrations ORDINAL1, RELSET_1, NUMBERS, XCMPLX_0, NAT_1, COMPLEX1,
      STRUCT_0, VECTSP_1, XREAL_0, MEMBERED;
 requirements NUMERALS, SUBSET, ARITHM;
 definitions RLVECT_1, VECTSP_1, COMPTRIG, ALGSTR_0;
 equalities STRUCT_0, COMPLEX1, ALGSTR_0;
 expansions RLVECT_1, GROUP_1, VECTSP_1, STRUCT_0;
 theorems COMPLEX1, RLVECT_1, VECTSP_1, XCMPLX_0, XCMPLX_1, BINOP_2, GROUP_1,
      COMPTRIG, NEWTON, ORDINAL1, NAT_1, XREAL_1;
 schemes NAT_1;

begin

definition
  func F_Complex -> strict doubleLoopStr means  :Def1:
  the carrier of it = COMPLEX & the addF of it = addcomplex &
  the multF of it = multcomplex & 1.it = 1r & 0.it = 0c;
  existence
  proof
    take doubleLoopStr (# COMPLEX,addcomplex,multcomplex,1r,0c #);
    thus thesis;
  end;
  uniqueness;
end;

registration
  cluster F_Complex -> non empty;
  coherence by Def1;
end;

registration
  cluster the carrier of F_Complex -> complex-membered;
  coherence by Def1;
end;

registration
  let a,b be Complex;
  let x,y be Element of F_Complex;
  identify x+y with a+b when x=a, y=b;
  compatibility
  proof
    reconsider a9=a, b9=b as Element of COMPLEX by XCMPLX_0:def 2;
    assume x=a & y=b;
    hence x+y = addcomplex.(a9,b9) by Def1
      .= a+b by BINOP_2:def 3;
  end;
  identify x*y with a*b when x=a, y=b;
  compatibility
  proof
    reconsider a9=a, b9=b as Element of COMPLEX by XCMPLX_0:def 2;
    assume x=a & y=b;
    hence x*y = multcomplex.(a9,b9) by Def1
      .= a*b by BINOP_2:def 5;
  end;
end;

registration
  cluster F_Complex -> well-unital;
  coherence
  proof
    let x be Element of F_Complex;
    1.F_Complex = 1r by Def1;
    hence thesis;
  end;
end;

Lm1: 1_F_Complex = 1r by Def1;

Lm2: 1.F_Complex = 1r by Def1;

registration
  cluster F_Complex -> add-associative right_zeroed right_complementable
    Abelian commutative associative left_unital right_unital distributive
    almost_left_invertible non degenerated;
  coherence
  proof
    thus F_Complex is add-associative;
    thus F_Complex is right_zeroed
    proof
      let x be Element of F_Complex;
      reconsider x1=x as Element of COMPLEX by Def1;
      thus x + 0.F_Complex = (the addF of F_Complex).(x1,0c) by Def1
        .= addcomplex.(x1,0c) by Def1
        .= x1 + 0c by BINOP_2:def 3
        .= x;
    end;
    thus F_Complex is right_complementable
    proof
      let x be Element of F_Complex;
      reconsider x1=x as Element of COMPLEX by Def1;
      -x1 in COMPLEX by XCMPLX_0:def 2;
      then reconsider y=-x1 as Element of F_Complex by Def1;
      take y;
      thus thesis by Def1;
    end;
    thus F_Complex is Abelian;
    thus F_Complex is commutative;
    thus F_Complex is associative;
    thus F_Complex is left_unital;
    thus F_Complex is right_unital;
    thus F_Complex is distributive;
    thus F_Complex is almost_left_invertible
    proof
      let x be Element of F_Complex;
      reconsider x1=x as Element of COMPLEX by Def1;
      assume
A1:   x <> 0.F_Complex;
      x1" in COMPLEX by XCMPLX_0:def 2;
      then reconsider y=x1" as Element of F_Complex by Def1;
      take y;
      x1<>0c by A1,Def1;
      hence thesis by Lm2,XCMPLX_0:def 7;
    end;
    thus F_Complex is non degenerated by Def1,Lm1;
  end;
end;

theorem
  for x1,y1 be Element of F_Complex for x2,y2 be Complex st
  x1 = x2 & y1 = y2 holds x1 + y1 = x2 + y2;

theorem Th2:
  for x1 be Element of F_Complex for x2 be Complex st
  x1 = x2 holds - x1 = - x2
proof
  let x1 be Element of F_Complex;
  let x2 be Complex;
  assume
A1: x1 = x2;
  reconsider x2 as Element of COMPLEX by XCMPLX_0:def 2;
  -x2 in COMPLEX by XCMPLX_0:def 2;
  then reconsider x9=-x2 as Element of F_Complex by Def1;
  x1 + x9 = 0.F_Complex by A1,Def1;
  hence thesis by RLVECT_1:def 10;
end;

registration
  let a be Complex;
  let x be Element of F_Complex;
  identify -x with -a when x=a;
  compatibility by Th2;
end;

registration
  let a,b be Complex;
  let x,y be Element of F_Complex;
  identify x-y with a-b when x=a, y=b;
  compatibility;
end;

theorem
  for x1,y1 be Element of F_Complex for x2,y2 be Complex st
  x1 = x2 & y1 = y2 holds x1 - y1 = x2 - y2;

theorem
  for x1,y1 be Element of F_Complex for x2,y2 be Complex st
  x1 = x2 & y1 = y2 holds x1 * y1 = x2 * y2;

theorem Th5:
  for x1 be Element of F_Complex for x2 be Complex st
  x1 = x2 & x1 <> 0.F_Complex holds x1" = x2"
proof
  let x1 be Element of F_Complex;
  let x2 be Complex;
  reconsider x4 = x2 as Element of COMPLEX by XCMPLX_0:def 2;
  x4" in COMPLEX by XCMPLX_0:def 2;
  then reconsider x9= x4" as Element of F_Complex by Def1;
  assume that
A1: x1 = x2 and
A2: x1 <> 0.F_Complex;
  0c = 0.F_Complex by Def1;
  then x1 * x9 = 1.F_Complex by A1,A2,Lm2,XCMPLX_0:def 7;
  hence thesis by A2,VECTSP_1:def 10;
end;

registration
  let a be Complex;
  let x be non zero Element of F_Complex;
  identify x" with a" when x=a;
  compatibility by Th5;
end;

theorem Th6:
  for x1,y1 be Element of F_Complex for x2,y2 be Complex st
  x1 = x2 & y1 = y2 & y1 <> 0.F_Complex holds x1/y1 = x2/y2
proof
  let x1,y1 be Element of F_Complex;
  let x2,y2 be Complex;
  assume that
A1: x1 = x2 and
A2: y1 = y2;
  assume y1 <> 0.F_Complex;
  then y1" = y2" by A2,Th5;
  hence thesis by A1,XCMPLX_0:def 9;
end;

registration
  let a,b be Complex;
  let x,y be non zero Element of F_Complex;
  identify x/y with a/b when x=a, y=b;
  compatibility by Th6;
end;

theorem Th7:
  0.F_Complex = 0c by Def1;

theorem
  1_F_Complex = 1r by Def1;

theorem
  1_F_Complex + 1_F_Complex <> 0.F_Complex by Def1,Lm1;

definition
  let z be Element of F_Complex;
  redefine func z *' -> Element of F_Complex;  :: redefines *' (COMPLEX1, definition)
  coherence
  proof
    z *' in COMPLEX by XCMPLX_0:def 2;
    hence thesis by Def1;
  end;
end;

reserve z,z1,z2,z3,z4 for Element of F_Complex;

theorem
  -z = (-1_F_Complex) * z by Lm1;

theorem
  z1 - -z2 = z1 + z2;

theorem
  z1 = z1 + z - z;

theorem
  z1 = z1 - z + z;

theorem
  z1 <> 0.F_Complex & z2 <> 0.F_Complex & z1" = z2" implies z1 = z2
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z1 <> 0.F_Complex;
  assume
A2: z2 <> 0.F_Complex;
  assume z1" = z2";
  then z19" = z2" by A1,Th5
    .= z29" by A2,Th5;
  hence thesis by XCMPLX_1:201;
end;

theorem
  z2 <> 0.F_Complex & (z1 * z2 = 1.F_Complex or z2 * z1 = 1.F_Complex)
  implies z1 = z2"
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  assume
A2: z1 * z2 = 1.F_Complex or z2 * z1 = 1.F_Complex;
  per cases by A2;
  suppose
A3: z1 * z2 = 1.F_Complex;
A4: z2" = z29" by A1,Th5;
    z19 * z29 = 1r by A3,Def1;
    hence thesis by A1,A4,Th7,XCMPLX_0:def 7;
  end;
  suppose
A5: z2 * z1 = 1.F_Complex;
A6: z2" = z29" by A1,Th5;
    z29 * z19 = 1r by A5,Def1;
    hence thesis by A1,A6,Th7,XCMPLX_0:def 7;
  end;
end;

theorem
  z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies
  z1 = z3 * z2" & z1 = z2" * z3
proof
  reconsider z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  then
A2: z2" = z29" by Th5;
  assume
A3: z1 * z2 = z3 or z2 * z1 = z3;
  per cases by A3;
  suppose
    z1 * z2 = z3;
    hence thesis by A1,A2,Th7,XCMPLX_1:203;
  end;
  suppose
    z2 * z1 = z3;
    hence thesis by A1,A2,Th7,XCMPLX_1:203;
  end;
end;

theorem
  (1.F_Complex)" = 1.F_Complex
proof
  1.F_Complex = 1r" by Def1;
  hence thesis;
end;

theorem
  z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1 * z2)" = z1" * z2"
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z1 <> 0.F_Complex;
  then
A2: z1" = z19" by Th5;
  assume
A3: z2 <> 0.F_Complex;
  then
A4: z2" = z29" by Th5;
  z1 * z2 <> 0.F_Complex by A1,A3,VECTSP_1:12;
  hence (z1 * z2)" = (z19 * z29)" by Th5
    .= z1" * z2" by A2,A4,XCMPLX_1:204;
end;

theorem
  z <> 0.F_Complex implies (-z)" = -(z")
proof
  reconsider z1=z as Element of COMPLEX by Def1;
  assume
A2: z <> 0.F_Complex;
  -z <> 0.F_Complex by A2,VECTSP_1:28;
  hence (-z)" = (-z1)" by Th5
    .= -(z1") by XCMPLX_1:222
    .= -(z") by A2,Th5;
end;

theorem
  z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
  z1" + z2" = (z1 + z2) * (z1 * z2)"
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z1 <> 0.F_Complex;
  then
A2: z1" = z19" by Th5;
  assume
A3: z2 <> 0.F_Complex;
  then z1 * z2 <> 0.F_Complex by A1,VECTSP_1:12;
  then
A4: (z1 * z2)" = (z19 * z29)" by Th5;
  z2" = z29" by A3,Th5;
  hence thesis by A1,A2,A3,A4,Th7,XCMPLX_1:211;
end;

theorem
  z1 <> 0.F_Complex & z2 <> 0.F_Complex implies
  z1" - z2" = (z2 - z1) * (z1 * z2)"
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A2: z1 <> 0.F_Complex;
  then
A3: z1" = z19" by Th5;
  assume
A4: z2 <> 0.F_Complex;
  then z1 * z2 <> 0.F_Complex by A2,VECTSP_1:12;
  then
A5: (z1 * z2)" = (z19 * z29)" by Th5;
  thus z1" - z2" = z19" - z29" by A3,A4,Th5
    .= (z2 - z1) * (z1 * z2)" by A2,A4,A5,Th7,XCMPLX_1:212;
end;

theorem
  z <> 0.F_Complex implies z" = (1.F_Complex) / z;

theorem
  z / (1.F_Complex) = z
proof
  1.F_Complex = 1r by Def1;
  hence thesis;
end;

theorem
  z <> 0.F_Complex implies z / z = 1.F_Complex
proof
  reconsider z1=z as Element of COMPLEX by Def1;
  assume
A1: z <> 0.F_Complex;
  hence z / z = z1 / z1 by Th6
    .= 1r by A1,Th7,XCMPLX_1:60
    .= 1.F_Complex by Def1;
end;

theorem
  z <> 0.F_Complex implies (0.F_Complex) / z = 0.F_Complex;

theorem Th26:
  z2 <> 0.F_Complex & z1 / z2 = 0.F_Complex implies z1 = 0. F_Complex
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  assume z1 / z2 = 0.F_Complex;
  then z19 / z29 = 0.F_Complex by A1,Th6;
  hence thesis by A1,Th7;
end;

theorem
  z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
  (z1 / z2) * (z3 / z4) = (z1 * z3) / (z2 * z4)
proof
  reconsider z19=z1,z29=z2,z39=z3,z49=z4 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  assume
A2: z4 <> 0.F_Complex;
  then
A3: z2 * z4 <> 0.F_Complex by A1,VECTSP_1:12;
A4: z39 / z49 = z3 / z4 by A2,Th6;
  z19 / z29 = z1 / z2 by A1,Th6;
  hence (z1 / z2) * (z3 / z4) = (z19 * z39) / (z29 * z49) by A4,XCMPLX_1:76
    .= (z1 * z3) / (z2 * z4) by A3,Th6;
end;

theorem
  z2 <> 0.F_Complex implies z * (z1 / z2) = (z * z1) / z2;

theorem
  z2 <> 0.F_Complex & z1 / z2 = 1.F_Complex implies z1 = z2
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  assume z1 / z2 = 1.F_Complex;
  then z19 / z29 = 1.F_Complex by A1,Th6;
  then z19 / z29 = 1 by Def1;
  hence thesis by XCMPLX_1:58;
end;

theorem
  z <> 0.F_Complex implies z1 = (z1 * z) / z
proof
  reconsider z19=z1,z9=z as Element of COMPLEX by Def1;
  assume
A1: z <> 0.F_Complex;
  hence z1 = (z19 * z9) / z9 by Th7,XCMPLX_1:89
    .= (z1 * z) / z by A1,Th6;
end;

theorem
  z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1 / z2)" = z2 / z1
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z1 <> 0.F_Complex;
  assume
A2: z2 <> 0.F_Complex;
  then
A3: z19 / z29 = z1 / z2 by Th6;
  z1 / z2 <> 0.F_Complex by A1,A2,Th26;
  hence (z1 / z2)" = (z19 / z29)" by A3,Th5
    .= z29 / z19 by XCMPLX_1:213
    .= z2 / z1 by A1,Th6;
end;

theorem
  z1 <> 0.F_Complex & z2 <> 0.F_Complex implies (z1" / z2") = z2 / z1
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z1 <> 0.F_Complex;
  assume z2 <> 0.F_Complex;
  then
A2: z2" = z29" & z2" <> 0.F_Complex by Th5,VECTSP_1:25;
  z1" = z19" by A1,Th5;
  hence (z1" / z2") = (z19" / z29") by A2,Th6
    .= z29 / z19 by XCMPLX_1:214
    .= z2 / z1 by A1,Th6;
end;

theorem
  z2 <> 0.F_Complex implies z1 / z2" = z1 * z2
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume z2 <> 0.F_Complex;
  then z2" <> 0.F_Complex & z2" = z29" by Th5,VECTSP_1:25;
  hence z1 / z2" = z19 / z29" by Th6
    .= z1 * z2 by XCMPLX_1:219;
end;

theorem
  z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1" / z2 = (z1 * z2)"
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z1 <> 0.F_Complex;
  assume
A2: z2 <> 0.F_Complex;
  then
A3: z1 * z2 <> 0.F_Complex by A1,VECTSP_1:12;
  z1" = z19" by A1,Th5;
  hence z1" / z2 = z19" / z29 by A2,Th6
    .= (z19 * z29)" by XCMPLX_1:221
    .= (z1 * z2)" by A3,Th5;
end;

theorem
  z1 <> 0.F_Complex & z2 <> 0.F_Complex implies z1"* (z / z2) = z / (z1 * z2)
proof
  reconsider z19=z1,z29=z2,z9=z as Element of COMPLEX by Def1;
  assume
A1: z1 <> 0.F_Complex;
  assume
A2: z2 <> 0.F_Complex;
  then
A3: z1 * z2 <> 0.F_Complex by A1,VECTSP_1:12;
A4: z9 / z29 = z / z2 by A2,Th6;
  z1" = z19" by A1,Th5;
  hence z1"* (z / z2) = z9 / (z19 * z29) by A4,XCMPLX_1:220
    .= z / (z1 * z2) by A3,Th6;
end;

theorem
  z <> 0.F_Complex & z2 <> 0.F_Complex implies
  (z1 / z2) = (z1 * z) / (z2 * z) & (z1 / z2) = (z * z1) / (z * z2)
proof
  reconsider z19=z1,z29=z2,z9=z as Element of COMPLEX by Def1;
  assume
A1: z <> 0.F_Complex;
  assume
A2: z2 <> 0.F_Complex;
  then
A3: z2 * z <> 0.F_Complex by A1,VECTSP_1:12;
  thus (z1 / z2) = (z19 / z29) by A2,Th6
    .= (z19 * z9) / (z29 * z9) by A1,Th7,XCMPLX_1:91
    .= (z1 * z) / (z2 * z) by A3,Th6;
  hence thesis;
end;

theorem
  z2 <> 0.F_Complex & z3 <> 0.F_Complex implies z1 / (z2 * z3) = z1 / z2 / z3
proof
  reconsider z19=z1,z29=z2,z39=z3 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  then
A2: z1 / z2 = z19 / z29 by Th6;
  assume
A3: z3 <> 0.F_Complex;
  then z2 * z3 <> 0.F_Complex by A1,VECTSP_1:12;
  hence z1 / (z2 * z3) = z19 / (z29 * z39) by Th6
    .= z19 / z29 / z39 by XCMPLX_1:78
    .= z1 / z2 / z3 by A3,A2,Th6;
end;

theorem
  z2 <> 0.F_Complex & z3 <> 0.F_Complex implies
  (z1 * z3) / z2 = z1 / (z2 / z3)
proof
  reconsider z19=z1,z29=z2,z39=z3 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  assume
A2: z3 <> 0.F_Complex;
  then
A3: z2 / z3 <> 0.F_Complex by A1,Th26;
A4: z2 / z3 = z29 / z39 by A2,Th6;
  thus (z1 * z3) / z2 = (z19 * z39) / z29 by A1,Th6
    .= z19 / (z29 / z39) by XCMPLX_1:77
    .= z1 / (z2 / z3) by A4,A3,Th6;
end;

theorem
  z2 <> 0.F_Complex & z3 <> 0.F_Complex & z4 <> 0.F_Complex implies
  (z1 / z2) / (z3 / z4) = (z1 * z4) / (z2 * z3)
proof
  reconsider z19=z1,z29=z2,z39=z3,z49=z4 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  then
A2: z1 / z2 = z19 / z29 by Th6;
  assume
A3: z3 <> 0.F_Complex;
  then
A4: z2 * z3 <> 0.F_Complex by A1,VECTSP_1:12;
  assume
A5: z4 <> 0.F_Complex;
  then
A6: z3 / z4 = z39 / z49 by Th6;
  z3 / z4 <> 0.F_Complex by A3,A5,Th26;
  hence (z1 / z2) / (z3 / z4) = (z19 / z29) / (z39 / z49) by A2,A6,Th6
    .= (z19 * z49) / (z29 * z39) by XCMPLX_1:84
    .= (z1 * z4) / (z2 * z3) by A4,Th6;
end;

theorem
  z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
  z1 / z2 + z3 / z4 = (z1 * z4 + z3 * z2) / (z2 * z4)
proof
  reconsider z19=z1,z29=z2,z39=z3,z49=z4 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  then
A2: z1 / z2 = z19 / z29 by Th6;
  assume
A3: z4 <> 0.F_Complex;
  then
A4: z2 * z4 <> 0.F_Complex by A1,VECTSP_1:12;
  z3 / z4 = z39 / z49 by A3,Th6;
  hence
  z1 / z2 + z3 / z4 = (z19 * z49 + z39 * z29) / (z29 * z49) by A1,A3,A2,Th7,
XCMPLX_1:116
    .= (z1 * z4 + z3 * z2) / (z2 * z4) by A4,Th6;
end;

theorem
  z <> 0.F_Complex implies z1 / z + z2 / z = (z1 + z2) / z;

theorem
  z2 <> 0.F_Complex implies -(z1 / z2) = (-z1) / z2 & -(z1 / z2) = z1 / (-z2)
proof
  assume
A1: z2 <> 0.F_Complex;
  then
A2: -z2 <> 0.F_Complex by VECTSP_1:28;
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  thus -(z1 / z2) = -(z19 / z29) by A1,Th6
    .= (-z19) / z29 by XCMPLX_1:187
    .= (-z1) / z2 by A1,Th6;
  thus -(z1 / z2) = -(z19 / z29) by A1,Th6
    .= z19 / -(z29) by XCMPLX_1:188
    .= z1 / -z2 by A2,Th6;
end;

theorem
  z2 <> 0.F_Complex implies z1 / z2 = (-z1) / (-z2)
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  then
A2: -z2 <> 0.F_Complex by VECTSP_1:28;
  thus z1 / z2 = z19 / z29 by A1,Th6
    .= (-z19) / (-z29) by XCMPLX_1:191
    .= (-z1) / (-z2) by A2,Th6;
end;

theorem
  z2 <> 0.F_Complex & z4 <> 0.F_Complex implies
  z1 / z2 - z3 / z4 = (z1 * z4 - z3 * z2) / (z2 * z4)
proof
  reconsider z19=z1,z29=z2,z39=z3,z49=z4 as Element of COMPLEX by Def1;
  assume
A2: z2 <> 0.F_Complex;
  then
A3: z19 / z29 = z1 / z2 by Th6;
  assume
A4: z4 <> 0.F_Complex;
  then
A5: z2 * z4 <> 0.F_Complex by A2,VECTSP_1:12;
 thus z1 / z2 - z3 / z4 = z19 / z29 - z39 / z49 by A3,A4,Th6
    .= (z19 * z49 - z39 * z29) / (z29 * z49) by A2,A4,Th7,XCMPLX_1:130
    .= (z1 * z4 - z3 * z2) / (z2 * z4) by A5,Th6;
end;

theorem
  z <> 0.F_Complex implies z1 / z - z2 / z = (z1 - z2) / z;

theorem
  z2 <> 0.F_Complex & (z1 * z2 = z3 or z2 * z1 = z3) implies z1 = z3 / z2
proof
  reconsider z39=z3,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  assume
A2: z1 * z2 = z3 or z2 * z1 = z3;
  per cases by A2;
  suppose
    z1 * z2 = z3;
    hence z1 = z39 / z29 by A1,Th7,XCMPLX_1:89
      .= z3 / z2 by A1,Th6;
  end;
  suppose
    z2 * z1 = z3;
    hence z1 = z39 / z29 by A1,Th7,XCMPLX_1:89
      .= z3 / z2 by A1,Th6;
  end;
end;

theorem
  (0.F_Complex)*' = 0.F_Complex
proof
  0.F_Complex = 0c by Def1;
  hence thesis;
end;

theorem Th48:
  z*' = 0.F_Complex implies z = 0.F_Complex
proof
  assume z*' = 0.F_Complex;
  then z*' = 0c by Def1;
  then z = 0c by COMPLEX1:29;
  hence thesis by Def1;
end;

theorem
  (1.F_Complex)*' = 1.F_Complex
proof
  1.F_Complex = 1r by Def1;
  hence thesis;
end;

theorem
  z*'*' = z;

theorem
  (z1 + z2)*' = z1*' + z2*' by COMPLEX1:32;

theorem
  (-z)*' = -(z*') by COMPLEX1:33;

theorem
  (z1 - z2)*' = z1*' - z2*' by COMPLEX1:34;

theorem
  (z1 * z2)*' = z1*' * z2*' by COMPLEX1:35;

theorem
  z <> 0.F_Complex implies z"*' = z*'"
proof
  reconsider z1=z as Element of COMPLEX by Def1;
  assume
A1: z <> 0.F_Complex;
  then
A2: z*' <> 0.F_Complex by Th48;
  z" = z1" by A1,Th5;
  hence z"*' = z1*'" by COMPLEX1:36
    .= z*'" by A2,Th5;
end;

theorem
  z2 <> 0.F_Complex implies (z1 / z2)*' = (z1*') / (z2*')
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume
A1: z2 <> 0.F_Complex;
  then
A2: z2*' <> 0.F_Complex by Th48;
  z19 / z29 = z1 / z2 by A1,Th6;
  hence (z1 / z2)*' = (z19*') / (z29*') by COMPLEX1:37
    .= (z1*') / (z2*') by A2,Th6;
end;

theorem
  |.0.F_Complex.| = 0 by Def1,COMPLEX1:44;

theorem
  |.z.| = 0 implies z = 0.F_Complex by Th7;

theorem
  z <> 0.F_Complex iff 0 < |.z.| by Th7,COMPLEX1:47;

theorem
  |.1.F_Complex.| = 1 by Def1,COMPLEX1:48;

theorem
  |.-z.| = |.z.| by COMPLEX1:52;

theorem
  |.z1 + z2.| <= |.z1.| + |.z2.| by COMPLEX1:56;

theorem
  |.z1 - z2.| <= |.z1.| + |.z2.| by COMPLEX1:57;

theorem
  |.z1.| - |.z2.| <= |.z1 + z2.| by COMPLEX1:58;

theorem
  |.z1.| - |.z2.| <= |.z1 - z2.| by COMPLEX1:59;

theorem
  |.z1 - z2.| = |.z2 - z1.| by COMPLEX1:60;

theorem
  |.z1 - z2.| = 0 iff z1 = z2 by COMPLEX1:61;

theorem
  z1 <> z2 iff 0 < |.z1 - z2.| by COMPLEX1:62;

theorem
  |.z1 - z2.| <= |.z1 - z.| + |.z - z2.| by COMPLEX1:63;

theorem
  |.|.z1.| - |.z2.|.| <= |.z1 - z2.| by COMPLEX1:64;

theorem
  |.z1*z2.| = |.z1.|*|.z2.| by COMPLEX1:65;

theorem
  z <> 0.F_Complex implies |.z".| = |.z.|"
proof
  reconsider z1=z as Element of COMPLEX by Def1;
  assume z <> 0.F_Complex;
  then z" = z1" by Th5;
  hence thesis by COMPLEX1:66;
end;

theorem
  z2 <> 0.F_Complex implies |.z1.| / |.z2.| = |.z1 / z2.|
proof
  reconsider z19=z1,z29=z2 as Element of COMPLEX by Def1;
  assume z2 <> 0.F_Complex;
  then z19 / z29 = z1 / z2 by Th6;
  hence thesis by COMPLEX1:67;
end;

begin :: Addenda
:: from COMPTRIG, 2006.08.12, A.T.

scheme
  Regrwithout0 { P[Nat] } : P[1]
provided
A1: ex k be non zero Element of NAT st P[k] and
A2: for k be non zero Element of NAT st k <> 1 & P[k]
   ex n be non zero Element of NAT st n < k & P[n]
proof
  consider t be non zero Element of NAT such that
A3: P[t] by A1;
  defpred R[Nat] means P[$1+1];
A4: now
    let k be Nat;
    assume that
A5: k <> 0 and
A6: R[k];
    reconsider k1=k+1 as non zero Element of NAT;
    k+1 > 0+1 by A5,NAT_1:3,XREAL_1:6;
    then consider n be non zero Element of NAT such that
A7: n < k1 and
A8: P[n] by A2,A6;
    consider l be Nat such that
A9: n = l+1 by NAT_1:6;
    take l;
    thus l < k by A7,A9,XREAL_1:6;
    thus R[l] by A8,A9;
  end;
  ex s be Nat st t = s+1 by NAT_1:6;
  then
A10: ex k be Nat st R[k] by A3;
  R[0] from NAT_1:sch 7(A10,A4);
  hence thesis;
end;

theorem Th74:
  for e being Element of F_Complex, n be Nat holds
  (power F_Complex).(e,n) = e|^n
proof
  let e be Element of F_Complex;
  defpred P[Nat] means (power F_Complex).(e,$1) = e|^$1;
A1: now
    let n be Nat;
    reconsider n9 = n as Element of NAT by ORDINAL1:def 12;
    reconsider p = (power F_Complex).(e,n9) as Element of F_Complex;
    assume
A2: P[n];
    (power F_Complex).(e,n+1) = p*e by GROUP_1:def 7
      .= e|^(n+1) by A2,NEWTON:6;
    hence P[n+1];
  end;
  (power F_Complex).(e,0) = 1_F_Complex by GROUP_1:def 7
  .= 1 by Def1;
  then
A3: P[0] by NEWTON:4;
  thus for n being Nat holds P[n] from NAT_1:sch 2(A3,A1);
end;

definition
  let x be Element of F_Complex;
  let n be non zero Element of NAT;
  redefine mode CRoot of n,x -> Element of F_Complex means  :: redefines CRoot (COMPTRIG, definition)
    :Def2: (power F_Complex).(it,n) = x;
  coherence
  proof
    let e be CRoot of n,x;
    e is Element of COMPLEX by XCMPLX_0:def 2;
    hence thesis by Def1;
  end;
  compatibility
  proof
    let e be Element of F_Complex;
    thus e is CRoot of n,x implies (power F_Complex).(e,n) = x
    proof
      assume e is CRoot of n,x;
      then e|^n = x by COMPTRIG:def 2;
      hence thesis by Th74;
    end;
    assume (power F_Complex).(e,n) = x;
    hence e|^n = x by Th74;
  end;
end;

theorem
  for x be Element of F_Complex for v be CRoot of 1,x holds v = x
proof
  let x be Element of F_Complex;
  let v be CRoot of 1,x;
  (power F_Complex).(v,1) = x by Def2;
  hence thesis by GROUP_1:50;
end;

theorem
  for n be non zero Element of NAT for v be CRoot of n,0.F_Complex
  holds v = 0.F_Complex
proof
  let n be non zero Element of NAT;
  let v be CRoot of n,0.F_Complex;
  defpred P[Element of omega] means (power F_Complex).(v,$1) = 0.F_Complex;
A1: now
    let k be non zero Element of NAT;
    assume that
A2: k <> 1 and
A3: P[k];
    consider t be Nat such that
A4: k = t+1 by NAT_1:6;
    reconsider t as Element of NAT by ORDINAL1:def 12;
    reconsider t as non zero Element of NAT by A2,A4;
    take t;
    thus t < k by A4,NAT_1:13;
    (power F_Complex).(v,k) = (power F_Complex).(v,t)*v by A4,GROUP_1:def 7;
    then (power F_Complex).(v,t) = 0.F_Complex or v = 0.F_Complex by A3,
VECTSP_1:12;
    hence P[t] by NAT_1:3,VECTSP_1:36;
  end;
A5: ex n be non zero Element of NAT st P[n]
  proof
    take n;
    thus thesis by Def2;
  end;
  P[1] from Regrwithout0(A5,A1);
  hence thesis by GROUP_1:50;
end;

theorem
  for n be non zero Element of NAT for x be Element of F_Complex
  for v be CRoot of n,x st v = 0.F_Complex holds x = 0.F_Complex
proof
  let n be non zero Element of NAT;
  let x be Element of F_Complex;
  let v be CRoot of n,x;
  assume v = 0.F_Complex;
  then (power F_Complex).(0.F_Complex,n) = x by Def2;
  hence thesis by NAT_1:3,VECTSP_1:36;
end;