:: Gaussian Integers
::  by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013-2016 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, NEWTON, ORDINAL1, SQUARE_1, ARYTM_3, CARD_1,
      XXREAL_0, XCMPLX_0, FUNCT_1, FUNCT_2, XBOOLE_0, RELAT_1, REAL_1, INT_1,
      ARYTM_1, COMPLEX1, GAUSSINT, ZFMISC_1, BINOP_1, BINOP_2, TARSKI,
      ZMODUL01, STRUCT_0, ALGSTR_0, RLVECT_1, GCD_1, VECTMETR, INT_2, NAT_1,
      SUPINF_2, MESFUNC1, FINSET_1, CARD_3, FUNCSDOM, VECTSP_1, VECTSP_2,
      RAT_1, EC_PF_1, LATTICES, GROUP_1, QUOFIELD, REALSET1, MCART_1, FUNCT_7,
      INT_3, POLYALG1;
 notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
      PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, REALSET1, FINSET_1, CARD_1, CARD_3,
      NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, INT_1, RAT_1, COMPLEX1,
      INT_2, INT_3, BINOP_2, NEWTON, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1,
      VECTSP_1, FUNCSDOM, VECTSP_2, GCD_1, QUOFIELD, EC_PF_1, ZMODUL01,
      POLYALG1;
 constructors REAL_1, SQUARE_1, MEMBERED, RELSET_1, NAT_1, BINOP_2, ZMODUL01,
      FUNCSDOM, WELLORD2, CARD_3, QUOFIELD, REALSET1, EC_PF_1, GCD_1, RAT_1,
      POLYALG1;
 registrations XBOOLE_0, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
      VECTSP_1, CARD_1, CARD_3, MEMBERED, SUBSET_1, INT_1, STRUCT_0, ALGSTR_0,
      REALSET1, EC_PF_1, ZMODUL01, XTUPLE_0, QUOFIELD, SQUARE_1, RAT_1, NAT_1,
      INT_3, ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
 definitions TARSKI, XBOOLE_0, STRUCT_0, ALGSTR_0, VECTSP_1, GROUP_1,
      POLYALG1;
 equalities SQUARE_1, XCMPLX_0, COMPLEX1, BINOP_1, STRUCT_0, ALGSTR_0,
      VECTSP_1, ZMODUL01, QUOFIELD, REALSET1;
 expansions TARSKI, STRUCT_0, ALGSTR_0, VECTSP_1, ZMODUL01, POLYALG1;
 theorems FUNCT_2, XBOOLE_0, TARSKI, NUMBERS, INT_1, XCMPLX_0, XCMPLX_1,
      XREAL_1, STRUCT_0, ALGSTR_0, XXREAL_0, COMPLEX1, ORDINAL1, RLVECT_1,
      NAT_1, BINOP_1, BINOP_2, RELAT_1, ZFMISC_1, FUNCT_1, SQUARE_1, ABSVALUE,
      VECTSP_1, GROUP_1, CARD_1, CARD_2, CARD_3, CARD_4, VECTSP_2, RAT_1,
      EC_PF_1, QUOFIELD, WELLORD2, INT_2, INT_3, GCD_1, XREAL_0, SUBSET_1;
 schemes NAT_1, BINOP_1, FUNCT_2;

begin :: 1. Gaussian integer ring

theorem Th1:
  for x,y be Nat st x+y = 1 holds (x = 1 & y = 0) or (x = 0 & y = 1)
  proof
    let x, y be Nat;
    assume A1: x+y = 1;
    x <= 1
    proof
      assume not x <= 1; then
      1 + 0 < x + y by XREAL_1:8;
      hence contradiction by A1;
    end;
    then x=0 or x = 1 by NAT_1:25;
    hence (x = 1 & y = 0) or (x = 0 & y = 1) by A1;
  end;

definition
  let z be Complex;
  attr z is g_integer means :Def1:
  Re z in INT & Im z in INT;
end;

Lm1: for z being Complex st Re z is integer & Im z is integer
  holds z is g_integer by INT_1:def 2;

registration
  cluster -> g_integer for Integer;
  coherence
  proof
    let c be Integer;
    Re c = c & Im c = 0 by COMPLEX1:def 1,def 2;
    hence Re c in INT & Im c in INT by INT_1:def 2;
  end;
end;

definition
  mode G_INTEG is g_integer Complex;
end;

registration
  let z be G_INTEG;
  cluster Re z -> integer;
  coherence
  proof
    Re z in INT by Def1;
    hence thesis;
  end;
  cluster Im z -> integer;
  coherence
  proof
    Im z in INT by Def1;
    hence thesis;
  end;
end;

registration
  let z1, z2 be G_INTEG;
  cluster z1+z2 -> g_integer;
  coherence
  proof
    Re(z1 + z2) = Re z1 + Re z2 & Im(z1 + z2) = Im z1 + Im z2 by COMPLEX1:8;
    hence thesis by INT_1:def 2;
  end;
  cluster z1-z2 -> g_integer;
  coherence
  proof
    Re(z1 - z2) = Re z1 - Re z2 & Im(z1 - z2) = Im z1 - Im z2 by COMPLEX1:19;
    hence thesis by INT_1:def 2;
  end;
  cluster z1*z2 -> g_integer;
  coherence
  proof
    Re(z1 * z2) = Re z1 * Re z2 - Im z1 * Im z2
    & Im(z1 * z2) = Re z1 * Im z2 + Re z2 * Im z1 by COMPLEX1:9;
    hence thesis by INT_1:def 2;
  end;
end;

registration
  cluster <i> -> g_integer;
  coherence by COMPLEX1:7,INT_1:def 2;
end;

registration
  let z be G_INTEG;
  cluster -z -> g_integer;
  coherence
  proof
    (Re(-z) = -(Re z)) & (Im(-z) = -(Im z)) by COMPLEX1:17;
    hence thesis by INT_1:def 2;
  end;
  cluster z *' -> g_integer;
  coherence;
end;

registration
  let z be G_INTEG, n be Integer;
  cluster n*z -> g_integer;
  coherence;
end;

definition
  func G_INT_SET -> Subset of COMPLEX equals
  the set of all z where z is G_INTEG;
  correctness
  proof
    now let x be object;
      assume x in the set of all z where z is G_INTEG;
      then ex z be G_INTEG st x=z;
      hence x in COMPLEX by XCMPLX_0:def 2;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

registration
  cluster G_INT_SET -> non empty;
  coherence
  proof
    0 in G_INT_SET;
    hence thesis;
  end;
end;

Lm2: <i> in G_INT_SET;

registration
  let i be Integer;
  reduce In(i,G_INT_SET) to i;
  reducibility
  proof
    i in G_INT_SET;
    hence thesis by SUBSET_1:def 8;
  end;
end;

theorem Th2:
  for x be object st x in G_INT_SET holds x is G_INTEG
  proof
    let x be object;
    assume x in G_INT_SET;
    then ex z be G_INTEG st x=z;
    hence x is g_integer Complex;
end;

theorem Th3:
  for x be object st x is G_INTEG holds x in G_INT_SET;

definition
  func g_int_add -> BinOp of G_INT_SET equals
  addcomplex || G_INT_SET;
  correctness
  proof
    set ad = addcomplex||G_INT_SET;
    [:G_INT_SET,G_INT_SET:] c= [:COMPLEX,COMPLEX:] by ZFMISC_1:96;
    then [:G_INT_SET,G_INT_SET:] c= dom (addcomplex) by FUNCT_2:def 1;
    then A1: dom ad = [:G_INT_SET,G_INT_SET:] by RELAT_1:62;
    for z be object st z in [:G_INT_SET,G_INT_SET:] holds ad. z in G_INT_SET
    proof
      let z be object such that
      A2: z in [:G_INT_SET,G_INT_SET:];
      consider x, y be object such that
      A3: x in G_INT_SET & y in G_INT_SET & z = [x,y]
      by A2,ZFMISC_1:def 2;
      reconsider x1 = x, y1 = y as G_INTEG by Th2,A3;
      ad.z = addcomplex.(x1,y1) by A2,A3,FUNCT_1:49
      .= x1+y1 by BINOP_2:def 3;
      hence ad.z in G_INT_SET;
    end;
    hence thesis by A1,FUNCT_2:3;
  end;
end;

definition
  func g_int_mult -> BinOp of G_INT_SET equals
  multcomplex || G_INT_SET;
  correctness
  proof
    set mult = multcomplex||G_INT_SET;
    [:G_INT_SET,G_INT_SET:] c= [:COMPLEX,COMPLEX:] by ZFMISC_1:96;
    then [:G_INT_SET,G_INT_SET:] c= dom(multcomplex) by FUNCT_2:def 1;
    then A1: dom mult = [:G_INT_SET,G_INT_SET:] by RELAT_1:62;
    for z be object st z in [:G_INT_SET,G_INT_SET:] holds mult.z in G_INT_SET
    proof
      let z be object such that
      A2: z in [:G_INT_SET,G_INT_SET:];
      consider x,y be object such that
      A3: x in G_INT_SET & y in G_INT_SET & z = [x,y]
      by A2,ZFMISC_1:def 2;
      reconsider x1 = x, y1 = y as G_INTEG by Th2,A3;
      mult.z = multcomplex.(x1,y1) by A2,A3,FUNCT_1:49
      .= x1*y1 by BINOP_2:def 5;
      hence mult.z in G_INT_SET;
    end;
    hence thesis by A1,FUNCT_2:3;
  end;
end;

definition
  func Sc_Mult -> Function of [:the carrier of INT.Ring,G_INT_SET :],
    G_INT_SET equals
  multcomplex | [:the carrier of INT.Ring, G_INT_SET:];
  correctness
  proof
A0: INT = the carrier of INT.Ring by INT_3:def 3;
    set scmult = multcomplex| [:INT,G_INT_SET:];
    [:INT,G_INT_SET:] c= [:COMPLEX,COMPLEX:] by NUMBERS:16,ZFMISC_1:96;
    then [:INT,G_INT_SET:] c= dom(multcomplex) by FUNCT_2:def 1;
    then A1: dom scmult = [:INT,G_INT_SET:] by RELAT_1:62;
    for z be object st z in [:INT,G_INT_SET:] holds scmult.z in G_INT_SET
    proof
      let z be object such that
      A2: z in [:INT,G_INT_SET:];
      consider x, y be object such that
      A3: x in INT & y in G_INT_SET & z = [x,y] by A2,ZFMISC_1:def 2;
      reconsider x1 = x as Element of INT by A3;
      reconsider y1 = y as G_INTEG by Th2,A3;
      scmult.z = multcomplex.(x1,y1) by A2,A3,FUNCT_1:49
      .= x1*y1 by BINOP_2:def 5;
      hence scmult.z in G_INT_SET;
    end;
    hence thesis by A1,FUNCT_2:3,A0;
  end;
end;

theorem Th4:
  for z, w be G_INTEG holds g_int_add.(z,w) = z+w
  proof
    let z, w be G_INTEG;
    z in G_INT_SET & w in G_INT_SET;
    hence g_int_add.(z,w) = addcomplex.(z,w) by FUNCT_1:49,ZFMISC_1:87
    .= z+w by BINOP_2:def 3;
  end;

theorem Th5:
  for z be G_INTEG, i be Integer holds Sc_Mult.(i,z) = i*z
  proof
    let z be G_INTEG, i be Integer;
    set scmult = Sc_Mult;
    A1: i in INT & z in G_INT_SET by INT_1:def 2;
    the carrier of INT.Ring = INT by INT_3:def 3;
    hence Sc_Mult.(i,z) = multcomplex.(i,z) by A1,FUNCT_1:49,ZFMISC_1:87
    .= i*z by BINOP_2:def 5;
  end;

definition
  func Gauss_INT_Module -> strict non empty ModuleStr over INT.Ring equals
    ModuleStr(# G_INT_SET, g_int_add, In(0,G_INT_SET), Sc_Mult #);
  coherence;
end;

LmX: -1.INT.Ring = -1 by INT_3:def 3;

Lm3:
  Gauss_INT_Module is Z_Module
  proof
    reconsider ZS = ModuleStr (# G_INT_SET, g_int_add, In(0,G_INT_SET),
      Sc_Mult #) as non empty ModuleStr over INT.Ring;
    set AG = G_INT_SET;
    set ML = the lmult of ZS;
    set AD = the addF of ZS;
    set CA = the carrier of ZS;
    set Z0 = the ZeroF of ZS;
    set MLI = Sc_Mult;
    A1:for v, w being Element of ZS holds v + w = w + v
    proof
      let v, w be Element of ZS;
      reconsider v1 = v, w1 = w as G_INTEG by Th2;
      thus v + w = w1 + v1 by Th4
      .= w + v by Th4;
    end;
    A2:for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
    proof
      let u, v, w be Element of ZS;
      reconsider u1 = u, v1 = v, w1 = w as G_INTEG by Th2;
      A3: u + v = u1+v1 by Th4;
      A4: v + w = v1+w1 by Th4;
      thus (u + v) + w = u1+v1+w1 by Th4,A3
      .= u1+(v1+w1)
      .= u+(v+w) by Th4,A4;
    end;
    A5: for v being Element of ZS holds v + 0.ZS = v
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      thus v + 0.ZS = v1 + 0 by Th4
      .= v;
    end;
    A6: for v being Vector of ZS holds v is right_complementable
    proof
      let v be Vector of ZS;
      take (-1.INT.Ring) * v;
      reconsider v1 = v as G_INTEG by Th2;
      A7: (-1.INT.Ring) * v = (-1) * v1 by LmX,Th5
       .= -v1;
      thus v + ((-1.INT.Ring) * v) = v1 + -v1 by A7, Th4
      .= 0.ZS;
    end;
    A8: for a, b be Element of INT.Ring, v being Vector of ZS
    holds (a + b) * v = a * v + b * v
    proof
      let a, b be Element of INT.Ring;
      let v be Vector of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      A9: (a*v1 = a*v) & (b*v1 = b*v) by Th5;
      thus (a + b) * v = (a + b) * v1 by Th5
      .= a*v1 + b*v1
      .= a*v + b*v by A9, Th4;
    end;
    A10: for a be Element of INT.Ring, v, w being Vector of ZS
    holds a * (v + w) = a * v + a * w
    proof
      let a be Element of INT.Ring;
      let v, w be Vector of ZS;
      reconsider v1 = v, w1 = w as G_INTEG by Th2;
      A11: (v + w) = (v1 + w1) by Th4;
      A12: (a*v1 = a*v) & (a*w1 = a*w) by Th5;
      thus a * (v + w) = a * (v1 + w1) by A11, Th5
      .= a*v1 + a*w1
      .= a*v + a*w by A12, Th4;
    end;
    A13: for a, b be Element of INT.Ring for v being Vector of
    ZS holds (a * b) * v = a * (b * v)
    proof
      let a, b be Element of INT.Ring;
      let v be Vector of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      A14: b * v1 = b * v by Th5;
      thus (a * b) * v = (a * b) * v1 by Th5
      .= a * (b * v1)
      .= a * (b * v) by A14, Th5;
    end;
    for v being Vector of ZS holds 1.INT.Ring * v = v
    proof
      let v be Vector of ZS;
      set i = 1.INT.Ring;
      reconsider v1 = v as G_INTEG by Th2;
      thus 1.INT.Ring * v = 1*v1 by Th5,INT_3:def 3
       .= v;
    end;
    hence thesis by A1,A2,A5,A6,A8,A10,A13,
      VECTSP_1:def 14,def 15,def 16,def 17,
      RLVECT_1:def 2,def 3,def 4,ALGSTR_0:def 16;
  end;

registration
  cluster Gauss_INT_Module -> Abelian add-associative right_zeroed
  right_complementable scalar-distributive vector-distributive
  scalar-associative scalar-unital;
  coherence by Lm3;
end;

theorem Th6:
  for z,w be G_INTEG holds g_int_mult.(z,w) = z*w
  proof
    let z, w be G_INTEG;
    z in G_INT_SET & w in G_INT_SET;
    hence g_int_mult.(z,w) = multcomplex.(z,w) by FUNCT_1:49,ZFMISC_1:87
    .= z*w by BINOP_2:def 5;
  end;

definition
  func Gauss_INT_Ring -> strict non empty doubleLoopStr equals
  doubleLoopStr(# G_INT_SET, g_int_add, g_int_mult, In(1,G_INT_SET),
  In(0,G_INT_SET) #);
  coherence;
end;

Lm4:
Gauss_INT_Ring is Ring
  proof
    reconsider
    ZS = doubleLoopStr(# G_INT_SET, g_int_add, g_int_mult, In(1,G_INT_SET),
    In(0,G_INT_SET) #) as non empty doubleLoopStr;
    A1:for v, w being Element of ZS holds v + w = w + v
    proof
      let v, w be Element of ZS;
      reconsider v1 = v, w1 = w as G_INTEG by Th2;
      thus v + w = w1 + v1 by Th4
      .= w + v by Th4;
    end;
    A2: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
    proof
      let u, v, w be Element of ZS;
      reconsider u1 = u, v1 = v, w1 = w as G_INTEG by Th2;
      A3: u + v = u1+v1 by Th4;
      A4: v + w = v1+w1 by Th4;
      thus (u + v) + w = u1+v1+w1 by Th4,A3
      .= u1+(v1+w1)
      .= u+(v+w) by Th4,A4;
    end;
    A5: for v being Element of ZS holds v + 0.ZS = v
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      thus v + 0.ZS = v1 + 0 by Th4
      .= v;
    end;
    A6: for v being Element of ZS holds v is right_complementable
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      reconsider w1 = (-1) as Element of ZS by Th3;
      A7: w1 * v = (-1) * v1 by Th6;
      take (w1*v);
      thus v + (w1*v) = v1 + ((-1) * v1) by A7,Th4
      .= 0.ZS;
    end;
    A8: for a, b, v being Element of ZS holds (a + b) * v = a * v + b * v
    proof
      let a, b, v be Element of ZS;
      reconsider a1 = a, b1 = b, v1 = v as G_INTEG by Th2;
      reconsider ab = a+b as G_INTEG by Th2;
      A9: a1*v1 = a*v & (b1*v1 = b*v) by Th6;
      thus (a + b) * v = ab * v1 by Th6
      .= (a1 + b1) * v1 by Th4
      .= a1*v1 + b1*v1
      .= a*v + b*v by A9,Th4;
    end;
    A10: for a, v, w being Element of ZS
    holds a * (v + w) = a * v + a * w & (v + w)*a = v*a + w*a
    proof
      let a, v, w be Element of ZS;
      reconsider a1 = a, v1 = v, w1 = w as G_INTEG by Th2;
      reconsider vw = (v+w) as G_INTEG by Th2;
      A11: (a1*v1 = a*v) & (a1*w1 = a*w) by Th6;
      thus a * (v + w) = a1 * vw by Th6
      .= a1 * (v1 + w1) by Th4
      .= a1*v1 + a1*w1
      .= a*v + a*w by A11,Th4;
      thus (v + w) * a = v*a + w*a by A8;
    end;
    A12: for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)
    proof
      let a, b, v be Element of ZS;
      reconsider a1 = a, b1 = b, v1 = v as G_INTEG by Th2;
      reconsider ab = (a*b), bv = (b*v) as G_INTEG by Th2;
      thus (a * b) * v = ab * v1 by Th6
      .= (a1 * b1) * v1 by Th6
      .= a1 * (b1 * v1)
      .= a1 * bv by Th6
      .= a * (b * v) by Th6;
    end;
    for v being Element of ZS holds v *1.ZS = v & 1.ZS * v = v
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      thus v * 1.ZS = v1 * 1 by Th6
      .= v;
      thus 1.ZS * v = 1 * v1 by Th6
      .= v;
    end;
    hence thesis
    by A1,A2,A5,A6,A10,A12,VECTSP_1:def 6,VECTSP_1:def 7,
    GROUP_1:def 3, RLVECT_1:def 2,def 3,def 4,ALGSTR_0:def 16;
  end;

registration
  cluster Gauss_INT_Ring -> Abelian add-associative right_zeroed
    right_complementable associative well-unital distributive;
  coherence by Lm4;
end;

registration
  cluster Gauss_INT_Ring -> domRing-like;
  coherence
  proof
    set X = Gauss_INT_Ring;
    for x, y being Element of X holds
    x*y = 0.X implies x = 0.X or y = 0.X
    proof
      let x, y be Element of X;
      reconsider xx = x, yy = y as Element of G_INT_SET;
      assume A1: x*y = 0.X;
      xx is G_INTEG & yy is G_INTEG by Th2;
      then xx*yy = 0 by A1,Th6;
      hence thesis;
    end;
    hence thesis by VECTSP_2:def 1;
  end;
end;

registration
  cluster Gauss_INT_Ring -> commutative;
  coherence
  proof
    set X = Gauss_INT_Ring;
    let v, w be Element of X;
    reconsider v1=v, w1=w as G_INTEG by Th2;
    thus v * w = v1 * w1 by Th6
    .= w * v by Th6;
  end;
end;

theorem
  for x be Element of Gauss_INT_Ring holds x is G_INTEG by Th2;

theorem
  for x be G_INTEG holds x is Element of Gauss_INT_Ring by Th3;

begin :: 2. Z-Algebra

registration
  cluster non empty for AlgebraStr over INT.Ring;
  existence
  proof
    set X =the non empty set, m = the BinOp of X,
    M = the Function of [:the carrier of INT.Ring,X:],X,
    u = the Element of X;
    take AlgebraStr(#X,m,m,u,u,M#);
    thus the carrier of AlgebraStr(#X,m,m,u,u,M#) is non empty;
  end;
end;

definition
::$CD
end;

registration
  cluster AlgebraStr(# G_INT_SET, g_int_add, g_int_mult,
    In(0,G_INT_SET), In(1,G_INT_SET), Sc_Mult #) -> non empty;
  coherence;
end;

registration
  cluster AlgebraStr(# G_INT_SET, g_int_add, g_int_mult,
    In(0,G_INT_SET), In(1,G_INT_SET), Sc_Mult #) ->
  strict Abelian add-associative right_zeroed
  right_complementable commutative associative right_unital
  right-distributive mix-associative scalar-associative
  vector-distributive scalar-distributive;
  correctness
  proof
    set ZS = AlgebraStr(# G_INT_SET, g_int_add, g_int_mult,
    In(0,G_INT_SET), In(1,G_INT_SET), Sc_Mult #);
    A1: for v, w being Element of ZS holds v + w = w + v
    proof
      let v, w be Element of ZS;
      reconsider v1=v, w1=w as G_INTEG by Th2;
      thus v + w = v1 + w1 by Th4
      .= w + v by Th4;
    end;
    A2: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
    proof
      let u, v, w be Element of ZS;
      reconsider u1=u,v1=v,w1=w as G_INTEG by Th2;
      A3: u + v = u1+v1 by Th4;
      A4: v + w = v1+w1 by Th4;
      thus (u + v) + w
      = u1+v1+w1 by Th4,A3
      .= u1+(v1+w1)
      .= u+(v+w) by Th4,A4;
    end;
    A5: for v being Element of ZS holds v + 0.ZS = v
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      thus v + 0.ZS = v1 + 0 by Th4
      .= v;
    end;
    A6: for v being Vector of ZS holds v is right_complementable
    proof
      let v be Vector of ZS;
      take (-1.INT.Ring) * v;
      reconsider v1 = v as G_INTEG by Th2;
      (-1.INT.Ring) * v = (-1) * v1 by LmX,Th5
       .= -v1;
      hence v + ((-1.INT.Ring) * v) = v1 + (-v1) by Th4
      .= 0.ZS;
    end;
    A8: for a, b be Element of INT.Ring, v being Vector of ZS
    holds (a + b) * v = a * v + b * v
    proof
      let a, b be Element of INT.Ring;
      let v be Vector of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      A9: (a*v1 = a*v) & (b*v1 = b*v) by Th5;
      thus (a + b) * v
      = (a + b) * v1 by Th5
      .= a*v1 + b*v1
      .= a*v + b*v by A9, Th4;
    end;
    A10: for a be Element of INT.Ring, v, w being Vector of ZS
    holds a * (v + w) = a * v + a * w
    proof
      let a be Element of INT.Ring;
      let v, w be Vector of ZS;
      reconsider v1 = v, w1 = w as G_INTEG by Th2;
      A11: (v + w) = (v1 + w1) by Th4;
      A12: (a*v1 = a*v) & (a*w1 = a*w) by Th5;
      thus a * (v + w) = a * (v1 + w1) by A11,Th5
      .= a*v1 + a*w1
      .= a*v + a*w by A12,Th4;
    end;
    A13: for a, b be Element of INT.Ring for v being Vector of ZS
    holds (a * b) * v = a * (b * v)
    proof
      let a, b be Element of INT.Ring;
      let v be Vector of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      A14: b * v1 = b * v by Th5;
      thus (a * b) * v = (a * b) * v1 by Th5
      .= a * (b * v1)
      .= a * (b * v) by A14, Th5;
    end;
    A15: for v, w being Vector of ZS for a be Element of INT.Ring
    holds a * (v * w) = (a * v) * w
    proof
      let v, w be Vector of ZS;
      let a be Element of INT.Ring;
      reconsider v1 = v, w1 = w as G_INTEG by Th2;
      A16: a * v = a * v1 by Th5;
      reconsider vw = v*w as G_INTEG by Th2;
      thus a *(v*w) = a*vw by Th5
      .= a*(v1*w1) by Th6
      .= a*v1*w1
      .= (a*v)*w by Th6,A16;
    end;
    A17: for v, w being Element of ZS holds v * w = w * v
    proof
      let v, w be Element of ZS;
      reconsider v1 = v, w1 = w as G_INTEG by Th2;
      thus v * w = v1 * w1 by Th6
      .= w * v by Th6;
    end;
    A18: for a, b, v being Element of ZS holds (a + b) * v = a * v + b * v
    proof
      let a, b, v be Element of ZS;
      reconsider a1 = a, b1 = b, v1 = v as G_INTEG by Th2;
      reconsider ab = a+b as G_INTEG by Th2;
      A19: a1*v1 = a*v & b1*v1 = b*v by Th6;
      thus (a + b) * v = ab * v1 by Th6
      .= (a1 + b1) * v1 by Th4
      .= a1*v1 + b1*v1
      .= a*v + b*v by A19, Th4;
    end;
    A20: for a, v, w being Element of ZS
    holds a * (v + w) = a * v + a * w & (v + w)*a = v*a + w*a
    proof
      let a, v, w be Element of ZS;
      reconsider a1 = a, v1 = v, w1 = w as G_INTEG by Th2;
      reconsider vw = (v+w) as G_INTEG by Th2;
      A21: (a1*v1 = a*v) & (a1*w1 = a*w) by Th6;
      thus a * (v + w) = a1 * vw by Th6
      .= a1 * (v1 + w1) by Th4
      .= a1*v1 + a1*w1
      .= a*v + a*w by A21, Th4;
      thus (v + w) * a = v*a + w*a by A18;
    end;
    A22: for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)
    proof
      let a, b, v be Element of ZS;
      reconsider a1 = a, b1 = b, v1 = v as G_INTEG by Th2;
      reconsider ab = (a*b), bv = (b*v) as G_INTEG by Th2;
      thus (a * b) * v = ab * v1 by Th6
      .= (a1 * b1) * v1 by Th6
      .= a1 * (b1 * v1)
      .= a1 * bv by Th6
      .= a * (b * v) by Th6;
    end;
    for v being Element of ZS holds v * 1.ZS = v & 1.ZS * v = v
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_INTEG by Th2;
      thus v * 1.ZS = v1 * 1 by Th6
      .= v;
      thus 1.ZS * v = 1 * v1 by Th6
      .= v;
    end;
    hence thesis by A1,A2,A5,A6,A8,A10,A13,
    GROUP_1:def 3, RLVECT_1:def 2,def 3,def 4,
    A17,A22,A20,A15,GROUP_1:def 12;
  end;
end;

registration
  cluster strict Abelian add-associative right_zeroed right_complementable
  commutative associative right_unital right-distributive mix-associative
  scalar-associative vector-distributive scalar-distributive
  for non empty AlgebraStr over INT.Ring;
  existence
  proof
    take AlgebraStr(# G_INT_SET, g_int_add, g_int_mult,
       In(0,G_INT_SET), In(1,G_INT_SET), Sc_Mult #);
    thus thesis;
  end;
end;

definition
  mode Z_Algebra is Abelian add-associative right_zeroed right_complementable
  commutative associative right_unital right-distributive
  mix-associative scalar-associative vector-distributive
  scalar-distributive non empty AlgebraStr over INT.Ring;
end;

theorem
  AlgebraStr(# G_INT_SET, g_int_add, g_int_mult,
  In(0,G_INT_SET), In(1,G_INT_SET), Sc_Mult #) is
  right_complementable associative commutative right-distributive
  right_unital Abelian add-associative right_zeroed vector-distributive
  scalar-distributive scalar-associative strict mix-associative
  non empty AlgebraStr over INT.Ring;

begin :: 3. Denumerable set

registration
  cluster INT -> denumerable;
  coherence
  proof
    [:{0},NAT:] is countable by CARD_4:7;
    then (NAT \/ [:{0},NAT:]) is countable by CARD_2:85;
    hence thesis by NUMBERS:def 4;
  end;
end;

registration
  cluster G_INT_SET -> denumerable;
  coherence
  proof
    defpred P[object,object,object] means
    ex n,m be Integer st $1 = n & $2 = m & $3 = n+ <i> *m;
    A1: for x, y being object st x in INT & y in INT
    ex z being object st z in G_INT_SET & P[x,y,z]
    proof
      let x, y be object;
      assume x in INT & y in INT;
      then reconsider n = x, m = y as Integer;
      take n+ <i> *m;
      thus thesis;
    end;
    consider F being Function of [:INT,INT:], G_INT_SET such that
    A2: for x, y being object st x in INT & y in INT holds
    P[x,y,F.(x,y)] from BINOP_1:sch 1(A1);
    A3: dom F = [:INT,INT:] by FUNCT_2:def 1;
    A4: for n, m be Integer holds F.(n,m) = n+ <i> *m
    proof
      let n, m be Integer;
      n in INT & m in INT by INT_1:def 2;
      then ex n1, m1 be Integer
      st n = n1 & m = m1 & F.(n,m)= n1+ <i> *m1 by A2;
      hence thesis;
    end;
    now let x be object;
      assume x in G_INT_SET;
      then reconsider x1 = x as G_INTEG by Th2;
      A5: Re x1 in INT & Im x1 in INT by Def1;
      reconsider n = Re x1, m = Im x1 as Integer;
      A6: F.(n,m) = n+ <i> *m by A4
      .= x1 by COMPLEX1:13;
      [n,m] in [:INT,INT:] by A5,ZFMISC_1:87;
      hence x in rng F by A3,A6,FUNCT_1:3;
    end;
    then A7: G_INT_SET c= rng F;
    F in Funcs([:INT,INT:],G_INT_SET) by FUNCT_2:8;
    then ex f being Function st F = f & dom f = [:INT,INT:]
    & rng f c= G_INT_SET by FUNCT_2:def 2;
    then A8: rng F = G_INT_SET by A7,XBOOLE_0:def 10;
    for x1, x2 be object
    st x1 in dom F & x2 in dom F & F.x1 = F.x2 holds x1 = x2
    proof
      let x1, x2 be object;
      assume A9: x1 in dom F & x2 in dom F & F.x1 = F.x2;
      then consider n1, m1 be object such that
      A10: n1 in INT & m1 in INT & x1 = [n1,m1] by A3,ZFMISC_1:def 2;
      consider n2, m2 be object such that
      A11: n2 in INT & m2 in INT & x2 = [n2,m2] by A9,A3,ZFMISC_1:def 2;
      reconsider n1, m1, n2, m2 as Integer by A10,A11;
      A12: F.x1 =F.(n1,m1) by A10
      .=n1+ <i> *m1 by A4;
      A13: F.x2 = F.(n2,m2) by A11
      .= n2+ <i> *m2 by A4;
      A14: n1 = Re(n2+ <i> *m2) by A9,A12,A13,COMPLEX1:12
      .= n2 by COMPLEX1:12;
      m1 = Im(n2+ <i> *m2) by A9,A12,A13,COMPLEX1:12
      .= m2 by COMPLEX1:12;
      hence thesis by A10,A11,A14;
    end;
    then [:INT,INT:],G_INT_SET are_equipotent
    by A8,A3,FUNCT_1:def 4,WELLORD2:def 4;
    then A15: card([:INT,INT:]) = card(G_INT_SET) by CARD_1:5;
    [:INT,INT:] is infinite & [:INT,INT:] is countable by CARD_4:7;
    then card([:INT,INT:]) = omega by CARD_3:def 15;
    hence thesis by CARD_3:def 15,A15;
  end;
end;

registration
  cluster Gauss_INT_Ring -> non degenerated;
  correctness;
end;

begin :: 4. Quotient field of Gaussian integer ring

definition
  func Gauss_INT_Field -> strict non empty doubleLoopStr equals
  the_Field_of_Quotients (Gauss_INT_Ring);
  correctness;
end;

registration
  cluster Gauss_INT_Field -> non degenerated almost_left_invertible
    strict Abelian associative distributive;
  correctness;
end;

definition
  let z be Complex;
  attr z is g_rational means
  :Def10:
  Re z in RAT & Im z in RAT;
end;

registration
  cluster -> g_rational for Rational;
  coherence
  proof
    let c be Rational;
    Re c = c & Im c = 0 by COMPLEX1:def 1,def 2;
    hence Re c in RAT & Im c in RAT by RAT_1:def 2;
  end;
end;

definition
  mode G_RAT is g_rational Complex;
end;

registration
  let z be G_RAT;
  cluster Re z -> rational;
  coherence
  proof
    Re z in RAT by Def10;
    hence thesis;
  end;
  cluster Im z -> rational;
  coherence
  proof
    Im z in RAT by Def10;
    hence thesis;
  end;
end;

registration
  let z1, z2 be G_RAT;
  cluster z1+z2 -> g_rational;
  coherence
  proof
    reconsider Rz1=Re z1,Iz1 =Im z1 as Rational;
    reconsider Rz2=Re z2,Iz2 =Im z2 as Rational;
    Re(z1 + z2) = Rz1 + Rz2 &
    Im(z1 + z2) = Iz1 + Iz2 by COMPLEX1:8;
    hence thesis by RAT_1:def 2;
  end;
  cluster z1-z2 -> g_rational;
  coherence
  proof
    reconsider Rz1 = Re z1, Iz1 = Im z1 as Rational;
    reconsider Rz2 = Re z2, Iz2 = Im z2 as Rational;
    Re(z1 - z2) = Rz1 - Rz2 &
    Im(z1 - z2) = Iz1 - Iz2 by COMPLEX1:19;
    hence z1-z2 is g_rational by RAT_1:def 2;
  end;
  cluster z1*z2 -> g_rational;
  coherence
  proof
    reconsider Rz1 = Re z1,Iz1 = Im z1 as Rational;
    reconsider Rz2 = Re z2, Iz2 = Im z2 as Rational;
    (Re(z1 * z2) = Rz1 * Rz2 - Iz1 * Iz2) &
    (Im(z1 * z2) = Rz1 * Iz2 + Rz2 * Iz1) by COMPLEX1:9;
    hence z1*z2 is g_rational by RAT_1:def 2;
  end;
end;

registration
  let z be G_RAT, n be Rational;
  cluster n*z -> g_rational;
  coherence;
end;

registration
  let z be G_RAT;
  cluster -z -> g_rational;
  coherence
  proof
    (Re(-z) = -(Re z)) & (Im(-z) = -(Im z)) by COMPLEX1:17;
    hence thesis by RAT_1:def 2;
  end;
  cluster z" -> g_rational;
  coherence
  proof
    (Re(z ") = (Re z) / (((Re z) ^2) + ((Im z) ^2))) &
    (Im(z ") = (- (Im z)) / (((Re z) ^2) + ((Im z) ^2))) by COMPLEX1:20;
    hence thesis by RAT_1:def 2;
  end;
end;

definition
  func G_RAT_SET -> Subset of COMPLEX equals
  the set of all z where z is G_RAT;
  correctness
  proof
    now let x be object;
      assume x in the set of all z where z is G_RAT;
      then ex z be G_RAT st x=z;
      hence x in COMPLEX by XCMPLX_0:def 2;
    end;
    hence thesis by TARSKI:def 3;
  end;
end;

registration
  cluster G_RAT_SET -> non empty;
  coherence
  proof
    0 in G_RAT_SET;
    hence thesis;
  end;
end;

registration
  cluster -> g_rational for G_INTEG;
  coherence by NUMBERS:14,Def1;
end;

theorem Th10:
  for x be object st x in G_RAT_SET holds x is G_RAT
  proof
    let x be object;
    assume x in G_RAT_SET;
    then ex z be G_RAT st x=z;
    hence x is g_rational Complex;
  end;

theorem Th11:
  for x be object st x is G_RAT holds x in G_RAT_SET;

theorem Th12:
  for p be G_RAT ex x, y be G_INTEG st y <> 0 & p = x/y
  proof
    let p be G_RAT;
    reconsider Rp = Re p, Ip = Im p as Rational;
    consider m1, n1 be Integer such that
    A1: n1 <> 0 & Rp = m1/n1 by RAT_1:2;
    consider m2, n2 be Integer such that
    A2: n2 <> 0 & Ip = m2/n2 by RAT_1:2;
    set z = n1*n2;
    Re z = z & Im z = 0 by COMPLEX1:def 1,COMPLEX1:def 2;
    then A3: (Re(z * p) = z * Rp - 0 * Ip) & (Im(z * p) = z * Ip + Rp * 0)
    by COMPLEX1:9;
    A4: Re(z*p) = n1/n1*m1*n2 by A1,A3
    .= 1*m1*n2 by XCMPLX_1:60,A1
    .= m1*n2;
    A5: Im(z*p) = n2/n2*m2*n1 by A2,A3
    .= 1*m2*n1 by XCMPLX_1:60,A2
    .= m2*n1;
    reconsider x = z*p as G_INTEG by A4,A5,Lm1;
    take x,z;
    x/z = z/z * p
    .= 1*p by XCMPLX_1:60,A1,A2
    .= p;
    hence thesis by A1,A2;
  end;

Lm5:
for x1, y1, x2, y2 be G_INTEG, u1, u2 being Element of Q. (Gauss_INT_Ring)
st y1 <> 0 & y2 <> 0 & u1 = [x1,y1] & u2 = [x2,y2]
holds x1/y1 = x2/y2 iff QClass.u1 = QClass.u2
proof
  let x1, y1, x2, y2 be G_INTEG,
  u1, u2 being Element of Q.(Gauss_INT_Ring);
  assume A1: y1 <> 0 & y2 <> 0 & u1 = [x1,y1] & u2= [ x2,y2];
  A2: u1`1 * u2`2 = x1*y2 by Th6,A1;
  A3: u2`1 * u1`2 = x2*y1 by Th6,A1;
  A4: u1`1 * u2`2 = u2`1 * u1`2 iff u1 in QClass.u2 by QUOFIELD:def 4;
  QClass.u1 = QClass.u2 iff u1 in QClass.u2
  proof
    A5: u1 in QClass.u1 by QUOFIELD:5;
    thus QClass.u1 = QClass.u2 implies u1 in QClass.u2 by QUOFIELD:5;
    assume u1 in QClass.u2;
    then u1 in (QClass.u1) /\ (QClass.u2) by A5,XBOOLE_0:def 4;
    hence (QClass.u1) = (QClass.u2) by QUOFIELD:8,XBOOLE_0:def 7;
  end;
  hence thesis by A1,A2,A3,A4,XCMPLX_1:94,95;
end;

definition
  func g_rat_add -> BinOp of G_RAT_SET equals
  addcomplex || G_RAT_SET;
  correctness
  proof
    set ad = addcomplex||G_RAT_SET;
    [:G_RAT_SET,G_RAT_SET:] c= [:COMPLEX,COMPLEX:] by ZFMISC_1:96;
    then [:G_RAT_SET,G_RAT_SET:] c= dom (addcomplex) by FUNCT_2:def 1;
    then A1: dom ad = [:G_RAT_SET,G_RAT_SET:] by RELAT_1:62;
    for z be object st z in [:G_RAT_SET,G_RAT_SET:]
    holds ad.z in G_RAT_SET
    proof
      let z be object such that
      A2: z in [:G_RAT_SET,G_RAT_SET:];
      consider x,y be object such that
      A3:(x in G_RAT_SET) & y in G_RAT_SET & (z = [x,y])
      by A2,ZFMISC_1:def 2;
      reconsider x1=x,y1=y as G_RAT by Th10,A3;
      ad.z = addcomplex.(x1,y1) by A2,A3,FUNCT_1:49
      .= x1+y1 by BINOP_2:def 3;
      hence ad.z in G_RAT_SET;
    end;
    hence thesis by A1,FUNCT_2:3;
  end;
end;

definition
  func g_rat_mult -> BinOp of G_RAT_SET equals
  multcomplex || G_RAT_SET;
  correctness
  proof
    set mult = multcomplex||G_RAT_SET;
    [:G_RAT_SET,G_RAT_SET:] c= [:COMPLEX,COMPLEX:] by ZFMISC_1:96;
    then [:G_RAT_SET,G_RAT_SET:] c= dom(multcomplex) by FUNCT_2:def 1;
    then A1: dom mult = [:G_RAT_SET,G_RAT_SET:] by RELAT_1:62;
    for z be object st z in [:G_RAT_SET,G_RAT_SET:] holds mult.z in G_RAT_SET
    proof
      let z be object such that
      A2: z in [:G_RAT_SET,G_RAT_SET:];
      consider x,y be object such that
      A3: x in G_RAT_SET & y in G_RAT_SET & z = [x,y]
      by A2,ZFMISC_1:def 2;
      reconsider x1 = x, y1 = y as G_RAT by Th10,A3;
      mult.z = multcomplex.(x1,y1) by A2,A3,FUNCT_1:49
      .= x1*y1 by BINOP_2:def 5;
      hence mult.z in G_RAT_SET;
    end;
    hence thesis by A1,FUNCT_2:3;
  end;
end;

begin :: 5. Rational field

Lm6:
addreal||RAT = addrat
proof
  set ad = addreal||RAT;
  [:RAT,RAT:] c= [:REAL,REAL:] by NUMBERS:12,ZFMISC_1:96;
  then A1: [:RAT,RAT:] c= dom (addreal) by FUNCT_2:def 1;
  then A2: dom ad = [:RAT,RAT:] by RELAT_1:62;
  A3: dom (addrat) = [:RAT,RAT:] by FUNCT_2:def 1;
  for z be object st z in dom ad holds ad.z = addrat.z
  proof
    let z be object;
    assume A4: z in dom ad;
    then consider x, y be object such that
    A5: x in RAT & y in RAT & z = [x,y] by A2,ZFMISC_1:def 2;
    reconsider x1 = x, y1 = y as Rational by A5;
    thus ad.z = addreal.(x1,y1) by A4,A5,A2,FUNCT_1:49
    .= x1+y1 by BINOP_2:def 9
    .= addrat.(x1,y1) by BINOP_2:def 15
    .= addrat.z by A5;
  end;
  hence thesis by A1,A3,FUNCT_1:2,RELAT_1:62;
end;

Lm7:
multreal||RAT = multrat
proof
  set ad = multreal||RAT;
  [:RAT,RAT:] c= [:REAL,REAL:] by NUMBERS:12,ZFMISC_1:96;
  then A1: [:RAT,RAT:] c= dom (multreal) by FUNCT_2:def 1;
  then A2: dom ad = [:RAT,RAT:] by RELAT_1:62;
  A3: dom (multrat) = [:RAT,RAT:] by FUNCT_2:def 1;
  for z be object st z in dom ad holds ad.z = multrat.z
  proof
    let z be object;
    assume A4: z in dom ad;
    then consider x, y be object such that
    A5: x in RAT & y in RAT & z = [x,y] by A2,ZFMISC_1:def 2;
    reconsider x1 = x, y1 = y as Rational by A5;
    thus ad.z = multreal.(x1,y1) by A4,A5,A2,FUNCT_1:49
    .= x1*y1 by BINOP_2:def 11
    .= multrat.(x1,y1) by BINOP_2:def 17
    .= multrat.z by A5;
  end;
  hence thesis by A1,A3,FUNCT_1:2,RELAT_1:62;
end;

registration
  let i be Integer;
  reduce In(i,RAT) to i;
  reducibility by RAT_1:def 2,SUBSET_1:def 8;
end;

definition
  func F_Rat -> strict non empty doubleLoopStr equals
  doubleLoopStr (# RAT, addrat, multrat, In(1,RAT), In(0,RAT) #);
  correctness;
end;

theorem Th13:
  the carrier of F_Rat is Subset of the carrier of F_Real
  & the addF of F_Rat = (the addF of F_Real) || (the carrier of F_Rat)
  & the multF of F_Rat = (the multF of F_Real) || (the carrier of F_Rat)
  & 1.F_Rat = 1.F_Real & 0.F_Rat = 0.F_Real
  & F_Rat is right_complementable commutative almost_left_invertible
  non degenerated
  proof
    A1: for v being Element of F_Rat holds v is right_complementable
    proof
      let v be Element of F_Rat;
      reconsider v1 = v as Rational;
      set w1 = -v1;
      reconsider w = w1 as Element of F_Rat by RAT_1:def 2;
      v + w = v1+w1 by BINOP_2:def 15
      .= 0.F_Rat;
      hence v is right_complementable;
    end;
    A2:
    now let x, y be Element of F_Rat;
      reconsider x1 = x, y1 = y as Rational;
      thus x*y = x1*y1 by BINOP_2:def 17
      .= y*x by BINOP_2:def 17;
    end;
    for v being Element of F_Rat st v <> 0. F_Rat
    holds v is left_invertible
    proof
      let v be Element of F_Rat;
      assume A3: v <> 0. F_Rat;
      reconsider v1 = v as Rational;
      set w1 = v1";
      reconsider w = w1 as Element of F_Rat by RAT_1:def 2;
      w * v = w1*v1 by BINOP_2:def 17
      .= 1.F_Rat by A3,XCMPLX_0:def 7;
      hence v is left_invertible;
    end;
    hence thesis by A1,A2,Lm6,Lm7,GROUP_1:def 12,NUMBERS:12;
  end;

theorem
  F_Rat is Subfield of F_Real by EC_PF_1:2,Th13;

registration
  cluster F_Rat -> add-associative right_zeroed right_complementable Abelian
  commutative associative left_unital right_unital distributive
  almost_left_invertible non degenerated;
  correctness by EC_PF_1:2,Th13;
end;

registration
  cluster F_Rat -> well-unital;
  coherence
  proof
    let x be Element of F_Rat;
    reconsider x1 = x as Rational;
    thus x*1.F_Rat = x1 * 1 by BINOP_2:def 17
    .=x;
    thus 1.F_Rat *x = 1*x1 by BINOP_2:def 17
    .=x;
  end;
end;

registration
  cluster -> rational for Element of F_Rat;
  coherence;
end;

registration
  let x,y be Element of F_Rat, a,b be Rational;
  identify x+y with a+b when x = a, y = b;
  compatibility by BINOP_2:def 15;
  identify x*y with a*b when x = a, y = b;
  compatibility by BINOP_2:def 17;
end;

registration
  let x be Element of F_Rat, y be Rational;
  identify -x with -y when x = y;
  compatibility
  proof
    reconsider w = -y as Element of F_Rat by RAT_1:def 2;
    assume x = y;
    then x+w = 0.F_Rat;
    hence thesis by VECTSP_1:16;
  end;
end;

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

theorem Th15:
  for x be Element of F_Rat, x1 be Rational st x <> 0.F_Rat & x1 = x
  holds x" = x1"
  proof
    let x be Element of F_Rat, x1 be Rational;
    assume A1: x <> 0.F_Rat & x1 = x;
    reconsider w = x1" as Element of F_Rat by RAT_1:def 2;
    w * x = 1.F_Rat by A1,XCMPLX_0:def 7;
    hence thesis by A1,VECTSP_1:def 10;
  end;

theorem Th16:
  for x, y be Element of F_Rat, x1, y1 be Rational
  st x1 = x & y1 = y & y <> 0.F_Rat
  holds x/y = x1/y1
  proof
    let x, y be Element of F_Rat, x1, y1 be Rational;
    assume A1: x1 = x & y1 = y & y <> 0.F_Rat;
    then y" = y1" by Th15;
    hence x/y = x1/y1 by A1;
  end;

theorem Th17:
  for K be Field, K1 be Subfield of K, x, y be Element of K,
  x1, y1 be Element of K1 st x = x1 & y = y1 holds x+y = x1+y1
  proof
    let K be Field,
    K1 be Subfield of K,
    x, y be Element of K,
    x1, y1 be Element of K1;
    set C1 = the carrier of K1;
    the addF of K1 = (the addF of K) || C1 by EC_PF_1:def 1;
    hence thesis by FUNCT_1:49,ZFMISC_1:87;
  end;

theorem Th18:
  for K be Field, K1 be Subfield of K, x, y be Element of K,
  x1, y1 be Element of K1 st x = x1 & y = y1 holds x*y =x1*y1
  proof
    let K be Field,
    K1 be Subfield of K,
    x, y be Element of K,
    x1, y1 be Element of K1;
    set C = the carrier of K;
    set C1 = the carrier of K1;
    the multF of K1 = (the multF of K) || C1 by EC_PF_1:def 1;
    hence thesis by FUNCT_1:49,ZFMISC_1:87;
  end;

theorem Th19:
  for K be Field, K1 be Subfield of K, x be Element of K,
  x1 be Element of K1 st x = x1 holds -x = -x1
  proof
    let K be Field,
    K1 be Subfield of K,
    x be Element of K,
    x1 be Element of K1;
    set C = the carrier of K;
    set C1 = the carrier of K1;
    set hpd = -x1;
    assume A1: x = x1;
    C1 c= C by EC_PF_1:def 1;
    then reconsider g = hpd as Element of K;
    x + g = x1 + hpd by A1,Th17
    .= 0.K1 by VECTSP_1:19
    .= 0.K by EC_PF_1:def 1;
    hence thesis by VECTSP_1:16;
  end;

theorem
  for K be Field, K1 be Subfield of K, x, y be Element of K,
  x1, y1 be Element of K1 st x = x1 & y = y1
  holds x-y = x1-y1
  proof
    let K be Field,
    K1 be Subfield of K,
    x, y be Element of K,
    x1, y1 be Element of K1;
    set C1 = the carrier of K1;
    assume A1: x = x1 & y = y1;
    then A2: -y =-y1 by Th19;
    the addF of K1 = (the addF of K) || C1 by EC_PF_1:def 1;
    hence thesis by A1,A2,FUNCT_1:49,ZFMISC_1:87;
  end;

theorem Th21:
  for K be Field, K1 be Subfield of K, x, y be Element of K,
  x1, y1 be Element of K1 st x = x1 & x <> 0.K
  holds x" = x1"
  proof
    let K be Field,
    K1 be Subfield of K,
    x, y be Element of K,
    x1, y1 be Element of K1;
    set C = the carrier of K;
    set C1 = the carrier of K1;
    set hpd = x1";
    assume A1: x = x1 & x <> 0.K;
    then A2: x1 <> 0.K1 by EC_PF_1:def 1;
    C1 c= C by EC_PF_1:def 1;
    then reconsider g = hpd as Element of K;
    A3: x*g = x1*hpd by A1,Th18
    .= 1.K1 by A2,VECTSP_1:def 10;
    x*g = 1.K by A3,EC_PF_1:def 1;
    hence thesis by A1,VECTSP_1:def 10;
  end;

theorem
  for K be Field, K1 be Subfield of K, x, y be Element of K,
  x1, y1 be Element of K1 st x = x1 & y = y1 & y <> 0.K
  holds x/y =x1/y1
  proof
    let K be Field,
    K1 be Subfield of K,
    x, y be Element of K,
    x1, y1 be Element of K1;
    set C = the carrier of K;
    set C1 = the carrier of K1;
    assume A1: x = x1 & y = y1 & y <> 0.K;
    then y" = y1" by Th21;
    hence thesis by A1,Th18;
  end;

set K = F_Rat;
set C = the carrier of K;

theorem Th23:
  for K1 be Subfield of F_Rat holds NAT c= the carrier of K1
  proof
    let K1 be Subfield of F_Rat;
    set C1 = the carrier of K1;
    defpred P[Nat] means $1 in C1;
    0.K = 0;
    then 0.K1 = 0 by EC_PF_1:def 1;
    then A1: P[0];
    A2: now let n be Nat;
    assume A3: P[n];
    A4: 1.K1 = 1.K by EC_PF_1:def 1
    .= 1;
    A5: the addF of K1 = (the addF of K) || C1 by EC_PF_1:def 1;
    (the addF of K1).(1,n) = (addrat).(1,n) by A3,A4,A5,FUNCT_1:49,ZFMISC_1:87
    .= 1+n by BINOP_2:def 15;
    hence P[n+1] by A3,A4,BINOP_1:17;
  end;
  for n being Nat holds P[n] from NAT_1:sch 2(A1,A2);
  hence thesis;
end;

theorem Th24:
  for K1 be Subfield of F_Rat holds INT c= the carrier of K1
  proof
    let K1 be Subfield of F_Rat, m be object;
    assume m in INT;
    then reconsider m as Integer;
    set C1 = the carrier of K1;
A1: NAT c= C1 by Th23;
    per cases;
    suppose 0 <= m;
      hence thesis by A1,INT_1:3;
    end;
    suppose 0 > m;
      then reconsider mm = -m as Element of NAT by INT_1:3;
      reconsider mmm = mm as Element of K1 by A1;
      consider mm1 be Element of K1 such that
      A2: mmm+mm1 =0.K1 by ALGSTR_0:def 11;
      A3: C1 c= C by EC_PF_1:def 1;
      then reconsider mm2 = mm1 as Element of K;
      reconsider mm3 = mm as Element of K by A2,A3;
      mm3+mm2 = 0.K1 by A2,Th17
      .= 0.K by EC_PF_1:def 1;
      then mm2 = -mm;
      hence thesis;
    end;
  end;

theorem Th25:
  for K1 be Subfield of F_Rat holds
  the carrier of K1 = the carrier of F_Rat
  proof
    let K1 be Subfield of F_Rat;
    thus the carrier of K1 c= the carrier of F_Rat by EC_PF_1:def 1;
    let x be object;
    set C1 = the carrier of K1;
A1: INT c= C1 by Th24;
A2: NAT c= C1 by Th23;
    assume x in C;
    then reconsider x1 = x as Rational;
    consider m be Integer, k be Nat such that
    A3: k<>0 & x1 = m/k by RAT_1:8;
    A4: m in C1 by A1,INT_1:def 2;
    reconsider k2 = k, m2 = m as Element of F_Rat by RAT_1:def 2;
    reconsider k0 = k as Element of K1 by A2,ORDINAL1:def 12;
    A5: k0 <> 0.K by A3;
    then k0 <> 0.K1 by EC_PF_1:def 1;
    then consider k0i be Element of K1 such that
    A6: k0i*k0 = 1.K1 by VECTSP_1:def 9;
    C1 c= C by EC_PF_1:def 1;
    then reconsider kk0 = k0i as Element of K;
    kk0*k2 = 1.K1 by A6,Th18
    .= 1.K by EC_PF_1:def 1;
    then A7: kk0 = k2" by A5,VECTSP_1:def 10;
    A8:the multF of K1 = (the multF of K) || C1 by EC_PF_1:def 1;
    m/k = m2/k2 by Th16,A3
    .= (the multF of K1).(m2,k2") by A4,A7,A8,FUNCT_1:49,ZFMISC_1:87;
    hence thesis by A3,A4,A7,BINOP_1:17;
  end;

theorem
  for K1 being strict Subfield of F_Rat holds K1 = F_Rat
  proof
    let K1 be strict Subfield of F_Rat;
    K is Subfield of K by EC_PF_1:1;
    hence thesis by EC_PF_1:8,Th25;
  end;

registration
  cluster F_Rat -> prime;
  coherence
  proof
    now let K1 be strict Subfield of K;
      set C1 = the carrier of K1;
      A1: for x being set st x in K holds x in K1 by Th25;
      K is strict Subfield of K by EC_PF_1:1;
      then K is strict Subfield of K1 by A1,EC_PF_1:7;
      hence K1 = K by EC_PF_1:4;
    end;
    then for K1 being Field holds K1 is strict Subfield of K implies K1 = K;
    hence thesis by EC_PF_1:def 2;
  end;
end;

begin :: 6. Gaussian rational number field

registration
  let i be Rational;
  reduce In(i,G_RAT_SET) to i;
  reducibility
  proof
    i in G_RAT_SET;
    hence thesis by SUBSET_1:def 8;
  end;
end;

definition
  func RSc_Mult -> Function of [:the carrier of F_Rat,G_RAT_SET :], G_RAT_SET
  equals
  multcomplex | [:the carrier of F_Rat,G_RAT_SET:];
  coherence
  proof
    set scmult = multcomplex| [:the carrier of F_Rat,G_RAT_SET:];
    [:the carrier of F_Rat,G_RAT_SET:] c= [:COMPLEX,COMPLEX:]
    by NUMBERS:13,ZFMISC_1:96;
    then
    [:the carrier of F_Rat,G_RAT_SET:] c= dom(multcomplex) by FUNCT_2:def 1;
    then A1: dom scmult = [:the carrier of F_Rat,G_RAT_SET:] by RELAT_1:62;
    for z be object st z in [:the carrier of F_Rat,G_RAT_SET:]
    holds scmult.z in G_RAT_SET
    proof
      let z be object such that
      A2: z in [:the carrier of F_Rat,G_RAT_SET:];
      consider x, y be object such that
      A3: (x in the carrier of F_Rat) & y in G_RAT_SET & z = [x,y]
      by A2,ZFMISC_1:def 2;
      reconsider x1 = x as Element of RAT by A3;
      reconsider y1 = y as G_RAT by Th10,A3;
      scmult.z = multcomplex.(x1,y1) by A2,A3,FUNCT_1:49
      .= x1*y1 by BINOP_2:def 5;
      hence scmult.z in G_RAT_SET;
    end;
    hence thesis by A1,FUNCT_2:3;
  end;
end;

theorem Th27:
  for z, w be G_RAT holds g_rat_add.(z,w) = z+w
  proof
    let z, w be G_RAT;
    z in G_RAT_SET & w in G_RAT_SET;
    hence g_rat_add.(z,w) = addcomplex.(z,w) by FUNCT_1:49,ZFMISC_1:87
    .= z+w by BINOP_2:def 3;
  end;

theorem Th28:
  for z be G_RAT, i be Element of RAT holds RSc_Mult.(i,z) = i*z
  proof
    let z be G_RAT, i be Element of RAT;
    i in RAT & z in G_RAT_SET;
    hence RSc_Mult.(i,z) = multcomplex.(i,z) by FUNCT_1:49,ZFMISC_1:87
    .= i*z by BINOP_2:def 5;
  end;

definition
  func Gauss_RAT_Module -> strict non empty ModuleStr over F_Rat equals
  ModuleStr (# G_RAT_SET, g_rat_add, In(0,G_RAT_SET), RSc_Mult #);
  coherence;
end;

Lm8:
  Gauss_RAT_Module is
  scalar-distributive vector-distributive
  scalar-associative scalar-unital add-associative right_zeroed
  right_complementable Abelian
  proof
    set ZS = Gauss_RAT_Module;
    set AG = G_RAT_SET;
    set AD = the addF of ZS;
    set CA = the carrier of ZS;
    set Z0 = the ZeroF of ZS;
    set MLI = RSc_Mult;
    A1: for v, w being Element of ZS holds v + w = w + v
    proof
      let v, w be Element of ZS;
      reconsider v1 = v, w1 = w as G_RAT by Th10;
      thus v + w = v1 + w1 by Th27
      .= w + v by Th27;
    end;
    A2: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
    proof
      let u, v, w be Element of ZS;
      reconsider u1 = u, v1 = v, w1  =w as G_RAT by Th10;
      A3: u + v = u1+v1 by Th27;
      A4: v + w = v1+w1 by Th27;
      thus (u + v) + w = u1+v1+w1 by Th27,A3
      .= u1+(v1+w1)
      .= u+(v+w) by Th27,A4;
    end;
    A5: for v being Element of ZS holds v + 0.ZS = v
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_RAT by Th10;
      thus v + 0.ZS = v1 + 0 by Th27
      .= v;
    end;
    A6: for v being Element of ZS holds v is right_complementable
    proof
      let v be Element of ZS;
      reconsider m1 = -1 as Element of F_Rat by RAT_1:def 2;
      take m1 * v;
      reconsider v1 = v as G_RAT by Th10;
      A7: m1 * v = (-1) * v1 by Th28
      .= -v1;
      thus v + (m1 * v) = v1 + (-v1) by A7,Th27
      .= 0.ZS;
    end;
    A8: for a, b be Element of F_Rat, v being Element of ZS
    holds (a + b) * v = a * v + b * v
    proof
      let a, b be Element of F_Rat;
      let v be Element of ZS;
      reconsider v1 = v as G_RAT by Th10;
      reconsider a1 = a, b1 = b as Element of RAT;
      A10:(a1*v1 = a*v) & (b1*v1 = b*v) by Th28;
      thus (a + b) * v = (a1 + b1) * v1 by Th28
      .= a1*v1 + b1*v1
      .= a*v + b*v by A10,Th27;
    end;
    A11: for a be Element of F_Rat, v, w being Element of ZS
    holds a * (v + w) = a * v + a * w
    proof
      let a be Element of F_Rat;
      let v, w be Element of ZS;
      reconsider v1 = v, w1 = w as G_RAT by Th10;
      reconsider a1 = a as Element of RAT;
      A12: (v + w) = (v1 + w1) by Th27;
      A13: (a1*v1 = a*v) & (a1*w1 = a*w) by Th28;
      thus a * (v + w) = a1 * (v1 + w1) by A12,Th28
      .= a1*v1 + a1*w1
      .= a*v + a*w by A13,Th27;
    end;
    A14: for a, b be Element of F_Rat for v being Element of ZS
    holds (a * b) * v = a * (b * v)
    proof
      let a, b be Element of F_Rat;
      let v be Element of ZS;
      reconsider v1 = v as G_RAT by Th10;
      reconsider a1 = a, b1 = b as Element of RAT;
      A15: b1 * v1 = b * v by Th28;
      thus (a * b) * v
      = (a1 * b1) * v1 by Th28
      .= a1 * (b1 * v1)
      .= a * (b * v) by A15,Th28;
    end;
    for v being Element of ZS holds 1.F_Rat * v = v
    proof
      let v be Element of ZS;
      reconsider i = 1 as Element of F_Rat;
      reconsider v1 = v as G_RAT by Th10;
      thus 1.F_Rat * v = 1*v1 by Th28
      .= v;
    end;
    hence thesis by A1,A2,A5,A6,A8,A11,A14,RLVECT_1:def 2,def 3,def 4;
  end;

registration
  cluster Gauss_RAT_Module
  -> scalar-distributive vector-distributive scalar-associative
  scalar-unital add-associative right_zeroed right_complementable Abelian;
  coherence by Lm8;
end;

theorem Th29:
  for z, w be G_RAT holds g_rat_mult.(z,w) = z*w
  proof
    let z, w be G_RAT;
    z in G_RAT_SET & w in G_RAT_SET;
    hence g_rat_mult.(z,w) = multcomplex.(z,w) by FUNCT_1:49,ZFMISC_1:87
    .= z*w by BINOP_2:def 5;
  end;

definition
  func Gauss_RAT_Ring -> strict non empty doubleLoopStr equals
  doubleLoopStr(# G_RAT_SET, g_rat_add, g_rat_mult, In(1,G_RAT_SET),
  In(0,G_RAT_SET) #);
  coherence;
end;

Lm9:
  Gauss_RAT_Ring is Field
  proof
    set ZS = Gauss_RAT_Ring;
    A1: for v, w being Element of ZS holds v + w = w + v
    proof
      let v, w be Element of ZS;
      reconsider v1 = v, w1 = w as G_RAT by Th10;
      thus v + w = v1 + w1 by Th27
      .= w + v by Th27;
    end;
    A2: for u, v, w being Element of ZS holds (u + v) + w = u + (v + w)
    proof
      let u, v, w be Element of ZS;
      reconsider u1 = u, v1 = v, w1 = w as G_RAT by Th10;
      A3: u + v = u1+v1 by Th27;
      A4: v + w = v1+w1 by Th27;
      thus (u + v) + w = u1+v1+w1 by Th27,A3
      .= u1+(v1+w1)
      .= u+(v+w) by Th27,A4;
    end;
    A5: for v being Element of ZS holds v + 0.ZS = v
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_RAT by Th10;
      thus v + 0.ZS = v1 + 0 by Th27
      .= v;
    end;
    A6: for v being Element of ZS holds v is right_complementable
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_RAT by Th10;
      reconsider w1 = (-1) as Element of ZS by Th11;

      A7: w1 * v = (-1) * v1 by Th29;
      take (w1*v);
      thus v + (w1*v) = v1 + ((-1) * v1) by A7,Th27
      .= 0.ZS;
    end;
    A8: for a, b, v being Element of ZS holds (a + b) * v = a * v + b * v
    proof
      let a, b, v be Element of ZS;
      reconsider a1 = a, b1 = b, v1 = v as G_RAT by Th10;
      reconsider ab = (a+b) as G_RAT by Th10;

      A9: (a1*v1 = a*v) & (b1*v1 = b*v) by Th29;
      thus (a + b) * v = ab * v1 by Th29
      .= (a1 + b1) * v1 by Th27
      .= a1*v1 + b1*v1
      .= a*v + b*v by A9,Th27;
    end;
    A10: for a, v, w being Element of ZS
    holds a * (v + w) = a * v + a * w & (v + w)*a = v*a + w*a
    proof
      let a, v, w be Element of ZS;
      reconsider a1 = a, v1 = v, w1 = w as G_RAT by Th10;
      reconsider vw = (v+w) as G_RAT by Th10;

      A11: (a1*v1 = a*v) & (a1*w1 = a*w) by Th29;
      thus a * (v + w) = a1 * vw by Th29
      .= a1 * (v1 + w1) by Th27
      .= a1*v1 + a1*w1
      .= a*v + a*w by A11,Th27;
      thus (v + w) * a = v*a + w*a by A8;
    end;
    A12: for a, b being Element of ZS holds a * b = b * a
    proof
      let a, b be Element of ZS;
      reconsider a1 = a, b1 = b as G_RAT by Th10;
      thus a * b = a1*b1 by Th29
      .= b * a by Th29;
    end;
    A13: for a, b, v being Element of ZS holds (a * b) * v = a * (b * v)
    proof
      let a, b, v be Element of ZS;
      reconsider a1 = a, b1 = b, v1 = v as G_RAT by Th10;
      reconsider ab = (a*b), bv = (b*v) as G_RAT by Th10;
      thus (a * b) * v = ab * v1 by Th29
      .= (a1 * b1) * v1 by Th29
      .= a1 * (b1 * v1)
      .= a1 * bv by Th29
      .= a * (b * v) by Th29;
    end;
    A14: for v being Element of ZS holds v * 1.ZS = v & 1.ZS * v = v
    proof
      let v be Element of ZS;
      reconsider v1 = v as G_RAT by Th10;

      thus v * 1.ZS = v1 * 1 by Th29
      .= v;
      thus 1.ZS * v = 1 * v1 by Th29
      .= v;
    end;
    for v being Element of ZS st v <> 0.ZS holds v is left_invertible
    proof
      let v be Element of ZS;
      assume A15: v <> 0.ZS;
      reconsider v1 = v as G_RAT by Th10;
      reconsider w = (v1)" as Element of ZS by Th11;

      w*v = (v1)"*v1 by Th29
      .= 1.ZS by A15,XCMPLX_0:def 7;
      hence thesis;
    end;
    hence thesis by A1,A2,A5,A6,A10,A13,A14,A12,VECTSP_1:def 6,
    VECTSP_1:def 7,ALGSTR_0:def 39,
    GROUP_1:def 3, GROUP_1:def 12,STRUCT_0:def 8,
    RLVECT_1:def 2,def 3,def 4,ALGSTR_0:def 16;
  end;

registration
  cluster Gauss_RAT_Ring -> add-associative right_zeroed
  right_complementable Abelian commutative associative well-unital
  distributive almost_left_invertible non degenerated;
  coherence by Lm9;
end;

theorem
  ex I be Function of Gauss_INT_Field,Gauss_RAT_Ring
  st (for z be object st z in the carrier of Gauss_INT_Field
  ex x, y be G_INTEG, u being Element of Q.(Gauss_INT_Ring)
  st y <> 0 & u = [x,y] & z = QClass.u & I.z = x/y) &
  I is one-to-one onto &
  (for x, y be Element of Gauss_INT_Field
  holds I.(x+y) = I.x + I.y & I.(x*y) = I.x * I.y) &
  I.(0.Gauss_INT_Field) = 0.Gauss_RAT_Ring &
  I.(1.Gauss_INT_Field) = 1.Gauss_RAT_Ring
  proof
    defpred P[object,object] means
    ex x, y be G_INTEG, u being Element of Q.(Gauss_INT_Ring)
    st y <> 0 & u = [x,y] & $1 = QClass.u & $2 = x/y;
    A1: for z be object st z in the carrier of Gauss_INT_Field
    ex w be object st w in the carrier of Gauss_RAT_Ring & P[z,w]
    proof
      let z be object;
      assume z in the carrier of Gauss_INT_Field;
      then consider u being Element of Q.(Gauss_INT_Ring) such that
      A2: z = QClass.u by QUOFIELD:def 5;
      consider x1, y1 be Element of Gauss_INT_Ring such that
      A3: u = [x1,y1] & y1 <> 0.(Gauss_INT_Ring) by QUOFIELD:def 1;
      reconsider x = x1, y = y1 as G_INTEG by Th2;
      take x/y;
      thus thesis by A2,A3;
    end;
    consider I be Function of Gauss_INT_Field,Gauss_RAT_Ring such that
    A4: for z be object
    st z in the carrier of Gauss_INT_Field holds P[z,I.z]
    from FUNCT_2:sch 1(A1);
    A5:
    now let z1, z2 be object;
      assume A6: z1 in dom I & z2 in dom I & I.z1 = I.z2;
      then A7: z1 in the carrier of Gauss_INT_Field
      & z2 in the carrier of Gauss_INT_Field by FUNCT_2:def 1;
      then consider x1, y1 be G_INTEG, u1 being Element of Q.(Gauss_INT_Ring)
      such that
      A8: y1 <> 0 & u1 = [x1,y1] & z1 = QClass.u1 & I.z1 = x1/y1 by A4;
      consider x2, y2 be G_INTEG, u2 being Element of Q.(Gauss_INT_Ring)
      such that
      A9: y2 <> 0 & u2 = [x2,y2] & z2 = QClass.u2 & I.z2 = x2/y2 by A4,A7;
      thus z1 = z2 by A6,A8,A9,Lm5;
    end;
    then A10: I is one-to-one by FUNCT_1:def 4;
    now let p1 be object;
      assume p1 in the carrier of Gauss_RAT_Ring;
      then reconsider p = p1 as G_RAT by Th10;
      consider x, y be G_INTEG such that
      A11: y <> 0 & p = x/y by Th12;
      reconsider x1 = x, y1 = y as Element of Gauss_INT_Ring by Th3;
      y1 <> 0.(Gauss_INT_Ring) by A11;
      then reconsider u1 = [x1,y1] as Element of Q. (Gauss_INT_Ring)
      by QUOFIELD:def 1;
      set z1 = QClass.u1;
      consider x2, y2 be G_INTEG, u2 being Element of Q.(Gauss_INT_Ring)
      such that
      A12: y2 <> 0 & u2 = [x2,y2] & z1 = QClass.u2 & I.z1 = x2/y2 by A4;
      x/y = x2/y2 by Lm5,A12,A11;
      hence ex z1 be object st z1 in the carrier of Gauss_INT_Field
      & I.z1 = p1 by A12,A11;
    end;
    then rng I = the carrier of Gauss_RAT_Ring by FUNCT_2:10;
    then A13: I is onto by FUNCT_2:def 3;
    A14: for z1, z2 be Element of Gauss_INT_Field holds
    I.(z1+z2) = I.z1 + I.z2 & I.(z1*z2) = I.z1 * I.z2
    proof
      let z1, z2 be Element of Gauss_INT_Field;
      consider x1, y1 be G_INTEG,
      u1 being Element of Q.(Gauss_INT_Ring) such that
      A15: y1 <> 0 & u1 = [x1,y1] & z1 = QClass.u1 & I.z1 = x1/y1 by A4;
      consider x2, y2 be G_INTEG,
      u2 being Element of Q.(Gauss_INT_Ring) such that
      A16: y2 <> 0 & u2 = [x2,y2] & z2 = QClass.u2 & I.z2 = x2/y2 by A4;
      set z12 = z1+z2;
      consider x12, y12 be G_INTEG,
      u12 being Element of Q.(Gauss_INT_Ring) such that
      A17: y12 <> 0 & u12 = [x12,y12] & z12 = QClass.u12 & I.z12 = x12/y12
      by A4;
      A18: x1/y1 + x2/y2 = (x1*y2 + x2*y1)/(y1*y2) by A15,A16,XCMPLX_1:116;
      A19: u1`1*u2`2 = x1*y2 & u2`1*u1`2 = x2*y1 & u1`2*u2`2 = y1*y2
      by Th6,A15,A16;
      A20: padd (u1,u2) = [(x1*y2)+(x2*y1),y1*y2] by A19,Th4;
      z12 = qadd ((QClass.u1),(QClass.u2)) by A15,A16,QUOFIELD:def 12
      .= QClass.(padd (u1,u2)) by QUOFIELD:9;
      then A21: u12 in QClass.(padd (u1,u2)) by A17,QUOFIELD:5;
      A22:  u12`1 * (padd (u1,u2))`2 = x12*(y1*y2) by Th6,A17,A19;
      (padd (u1,u2))`1 * u12`2 = (x1*y2 + y1*x2) * y12 by Th6,A17,A20;
      then x12*(y1*y2 ) = (x1*y2 + y1*x2)*y12 by A22,A21,QUOFIELD:def 4;
      then A23: x12/y12 = (x1*y2 + x2*y1)/(y1*y2)
        by A15,A16,A17,XCMPLX_1:94;
      set z12 = z1*z2;
      consider x12, y12 be G_INTEG,
      u12 being Element of Q.(Gauss_INT_Ring) such that
      A24: y12 <> 0 & u12 = [x12,y12] & z12 = QClass.u12 & I.z12 = x12/y12
      by A4;
      A25: (x1/y1) * (x2/y2) = (x1*x2)/(y1*y2) by XCMPLX_1:76;
      A26: u1`1*u2`1 = x1*x2 & u2`2*u1`2 = y1*y2 by Th6,A15,A16;
      z12 = qmult ((QClass.u1),(QClass.u2)) by A15,A16,QUOFIELD:def 13
      .= QClass.(pmult (u1,u2)) by QUOFIELD:10;
      then A27: u12 in QClass.(pmult (u1,u2)) by A24,QUOFIELD:5;
      A28:  u12`1 * (pmult (u1,u2))`2 = x12*(y1*y2) by Th6,A24,A26;
      (pmult (u1,u2))`1 * u12`2 = (x1*x2) * y12 by Th6,A24,A26;
      then x12*(y1*y2 ) = (x1*x2)*y12 by A28,A27,QUOFIELD:def 4;
      then x12/y12 = (x1*x2)/(y1*y2) by A15,A16,A24,XCMPLX_1:94;
      hence thesis by A23,A25,A18,A24,A17,A15,A16,Th27,Th29;
    end;
    A29: I.(0.Gauss_INT_Field) = I.(0.Gauss_INT_Field + 0.Gauss_INT_Field)
    by RLVECT_1:4
    .= I.(0.Gauss_INT_Field) + I.(0.Gauss_INT_Field) by A14;
    A30: 0.Gauss_RAT_Ring = I.(0.Gauss_INT_Field) - I.(0.Gauss_INT_Field)
    by RLVECT_1:15
    .= I.(0.Gauss_INT_Field) + (I.(0.Gauss_INT_Field) - I.(0.Gauss_INT_Field))
    by A29,RLVECT_1:28
    .= I.(0.Gauss_INT_Field) + 0. Gauss_RAT_Ring by RLVECT_1:15
    .= I.(0.Gauss_INT_Field) by RLVECT_1:4;
    dom I = the carrier of (Gauss_INT_Field) by FUNCT_2:def 1;
    then A31: I.(1.Gauss_INT_Field) <> 0.Gauss_RAT_Ring by A5,A30;
    A32: I.(1.Gauss_INT_Field) = I.((1.Gauss_INT_Field)*(1.Gauss_INT_Field))
    by VECTSP_1:def 8
    .= I.(1.Gauss_INT_Field) * I.(1.Gauss_INT_Field) by A14;
    1.Gauss_RAT_Ring = (I.(1.Gauss_INT_Field))" * (I.(1.Gauss_INT_Field))
    by VECTSP_1:def 10,A31
    .= (I.(1.Gauss_INT_Field))" * (I.(1.Gauss_INT_Field))
    * (I.(1.Gauss_INT_Field)) by A32,GROUP_1:def 3
    .= (1. Gauss_RAT_Ring) * (I.(1.Gauss_INT_Field)) by VECTSP_1:def 10,A31
    .= I.(1.Gauss_INT_Field) by VECTSP_1:def 8;
    hence thesis by A4,A10,A13,A14,A30;
  end;

begin :: 7. Gaussian integer ring is Euclidian

definition
  let a,b be G_INTEG;
  pred a Divides b means
  ex c being G_INTEG st b = a * c;
  reflexivity
  proof
    let a be G_INTEG;
    take 1;
    thus a = a * 1;
  end;
end;

theorem
  for a, b be Element of Gauss_INT_Ring, aa, bb be G_INTEG st a = aa & b = bb
  holds a divides b implies aa Divides bb
  proof
    let a, b be Element of Gauss_INT_Ring, aa, bb be G_INTEG such that
    A1: a = aa & b = bb;
    assume a divides b;
    then consider c be Element of Gauss_INT_Ring such that
    A2: b = a * c by GCD_1:def 1;
    reconsider cc = c as G_INTEG by Th2;
    bb = aa*cc by A1,A2,Th6;
    hence thesis;
  end;

theorem
  for a, b be Element of Gauss_INT_Ring, aa, bb be G_INTEG st a = aa & b = bb
  holds aa Divides bb implies a divides b
  proof
    let a, b be Element of Gauss_INT_Ring, aa, bb be G_INTEG such that
A1: a = aa & b = bb;
    assume aa Divides bb; then
    consider cc be G_INTEG such that
A2: bb = aa * cc;
    reconsider c = cc as Element of Gauss_INT_Ring by Th3;
    b = a*c by A1,A2,Th6;
    hence thesis by GCD_1:def 1;
  end;

definition
  let z be G_RAT;
  redefine func z *' -> G_RAT;
  coherence;
end;

definition
  let z be G_RAT;
  func Norm(z) -> Rational equals
  z * (z *');
  correctness
  proof
    set Rez = Re z, Imz = Im z;
    (Re(Rez + ((-Imz) * <i>)) = Rez) &
    (Im(Rez + ((-Imz) * <i>)) = (-Imz)) by COMPLEX1:12;
    then A1: (Re(z * (z *')) = Rez * Rez - Imz * (-Imz)) &
    (Im(z * (z *')) = Rez * (-Imz) + Rez * Imz) by COMPLEX1:9;
    (z * (z *')) = (Re(z * (z *'))) + (Im(z * (z *'))*<i>) by COMPLEX1:13
    .= Re(z * (z *')) by A1;
    hence thesis;
  end;
end;

registration
  let z be G_RAT;
  cluster Norm(z) -> non negative;
  correctness
  proof
    set Rez = Re z, Imz = Im z;
    (Re(Rez + ((-Imz) * <i>)) = Rez) &
    (Im(Rez + ((-Imz) * <i>)) = (-Imz)) by COMPLEX1:12;
    then A1: (Re(z * (z *')) = Rez * Rez - Imz * (-Imz)) &
    (Im(z * (z *')) = Rez * (-Imz) + Rez * Imz) by COMPLEX1:9;
    A2: (z * (z *')) = (Re(z * (z *'))) + (Im(z * (z *'))*<i>) by COMPLEX1:13
    .= Re(z * (z *')) by A1;
    (Re z)^2 >= 0 & (Im z)^2 >= 0 by XREAL_1:63;
    hence thesis by A1,A2;
  end;
end;

registration
  let z be G_INTEG;
  cluster Norm(z) -> natural;
  coherence
  proof
    Re(Re z + ((-Im z) * <i>)) = Re z &
    Im(Re z + ((-Im z) * <i>)) = -Im z by COMPLEX1:12;
    then A1: Re(z * (z *')) = Re z * Re z - Im z * (-Im z) &
    Im(z * (z *')) = Re z * (-Im z) + Re z * Im z by COMPLEX1:9;
    A2: z * (z *') = (Re(z * (z *'))) + (Im(z * (z *'))*<i>) by COMPLEX1:13
    .= Re(z * (z *')) by A1;
    (Re z)^2 >= 0 & (Im z)^2 >= 0 by XREAL_1:63;
    then Re(z * (z *')) in NAT by A1,INT_1:3;
    hence thesis by A2;
  end;
end;

theorem
  for x be G_RAT holds Norm(x *') = Norm(x);

theorem Th34:
  for x, y be G_RAT holds Norm(x*y) = Norm(x)*Norm(y)
  proof
    let x, y be G_RAT;
    thus Norm(x*y) = (x * y) * ((x *') * (y *')) by COMPLEX1:35
    .= Norm(x) * Norm(y);
  end;

theorem Th35:
  for x be G_INTEG holds Norm(x) = 1 iff x = 1 or x = -1 or x = <i> or x = -<i>
  proof
    let x be G_INTEG;
    hereby
      assume A1: Norm(x) = 1;
      A2: x = Re x+Im x*<i> by COMPLEX1:13;
      A3: Norm(x) = (Re x+Im x*<i>)*(Re x-(Im x)*<i>) by COMPLEX1:13
      .= (Re x)^2 + (Im x)^2;
      reconsider Rx = (Re x), Ix = (Im x) as Element of INT by Def1;
      Rx^2 in NAT & Ix^2 in NAT by INT_1:3,XREAL_1:63;
      then ((Re x)^2 = 1 & (Im x)^2 = 0) or ((Re x)^2 = 0 & (Im x)^2 = 1)
      by A1,A3,Th1;
      then ((Rx = 1 or Rx = -1) & Im x = 0)
      or (Re x = 0 & (Ix = 1 or Ix = -1)) by XCMPLX_1:182;
      hence (x = 1 or x = -1) or (x = <i> or x = -<i>) by A2;
    end;
    assume A4: x = 1 or x = -1 or x = <i> or x = -<i>;
    per cases by A4;
    suppose x = 1;
      hence Norm(x) = 1 by COMPLEX1:30;
    end;
    suppose x = -1;
      hence Norm(x) = (-1)*(-1*') by COMPLEX1:33
      .= 1 by COMPLEX1:30;
    end;
    suppose x = <i>;
      hence Norm(x) = 1 by COMPLEX1:31;
    end;
    suppose x = -<i>;
      hence Norm(x) = 1 by COMPLEX1:31;
    end;
  end;

theorem Th36:
  for x be G_INTEG holds Norm(x) = 0 implies x = 0
  proof
    let x be G_INTEG;
A1: Norm(x)=(Re x+Im x*<i>)*(Re x-(Im x)*<i>) by COMPLEX1:13
    .= (Re x)^2 + (Im x)^2;
    assume Norm(x) = 0;
    hence thesis by A1,COMPLEX1:5;
  end;

definition
  let z be G_INTEG;
  attr z is g_int_unit means
  :Def20:
  Norm(z) = 1;
end;

definition
  let x,y be G_INTEG;
  pred x is_associated_to y means
  x Divides y & y Divides x;
  symmetry;
end;

theorem Th37:
  for a, b be Element of Gauss_INT_Ring, aa, bb be G_INTEG st a = aa & b = bb
  holds a is_associated_to b implies aa is_associated_to bb
  proof
    let a, b be Element of Gauss_INT_Ring, aa, bb be G_INTEG such that
    A1: a = aa & b = bb;
    assume a is_associated_to b;
    then A2: a divides b & b divides a by GCD_1:def 3;
    then consider ca be Element of Gauss_INT_Ring such that
    A3: b = a * ca by GCD_1:def 1;
    consider cb be Element of Gauss_INT_Ring such that
    A4: a = b * cb by A2,GCD_1:def 1;
    reconsider cca = ca as G_INTEG by Th2;
    reconsider ccb = cb as G_INTEG by Th2;
    bb = aa*cca by A1,A3,Th6;
    then A5: aa Divides bb;
    aa = bb*ccb by A1,A4,Th6;
    then bb Divides aa;
    hence thesis by A5;
  end;

theorem Th38:
  for a, b be Element of Gauss_INT_Ring, aa, bb be G_INTEG st a = aa & b = bb
  holds aa is_associated_to bb implies a is_associated_to b
  proof
    let a, b be Element of Gauss_INT_Ring, aa, bb be G_INTEG such that
    A1: a = aa & b = bb;
    assume aa is_associated_to bb;
    then A2: aa Divides bb & bb Divides aa;
    then consider cca be G_INTEG such that
    A3: bb = aa * cca;
    consider ccb be G_INTEG such that
    A4: aa = bb * ccb by A2;
    reconsider ca = cca as Element of Gauss_INT_Ring by Th3;
    reconsider cb = ccb as Element of Gauss_INT_Ring by Th3;
    b = a*ca by A1,A3,Th6;
    then A5: a divides b by GCD_1:def 1;
    a = b*cb by A1,A4,Th6;
    then b divides a by GCD_1:def 1;
    hence thesis by A5,GCD_1:def 3;
  end;

Lm10:
for x, y be G_INTEG
holds x is_associated_to y implies Norm(x) = Norm(y)
proof
  let x, y be G_INTEG;
  assume A1: x is_associated_to y;
  reconsider x1 = x, y1 = y as Element of Gauss_INT_Ring by Th3;
  A2: x1 is_associated_to y1 by A1,Th38;
  x1 divides y1 by A2,GCD_1:def 3;
  then consider z1 be Element of Gauss_INT_Ring such that
  A3: y1 = x1 * z1 by GCD_1:def 1;
  y1 divides x1 by A2,GCD_1:def 3;
  then consider z2 be Element of Gauss_INT_Ring such that
  A4: x1 = y1 * z2 by GCD_1:def 1;
  reconsider z3 = z1 * z2 as Element of Gauss_INT_Ring;
  per cases;
  suppose A5: x1 * y1 <> 0.Gauss_INT_Ring;
    x1 * y1 = ((x1 * z1) * y1) * z2 by A3,A4,GROUP_1:def 3
    .= ((x1 * y1) * z1) * z2 by GROUP_1:def 3
    .= (x1 * y1) * z3 by GROUP_1:def 3;
    then A6: z3 = 1.Gauss_INT_Ring by A5,GCD_1:17
    .= 1;
    reconsider zz1 = z1,zz2 = z2 as G_INTEG by Th2;
    reconsider zz3 = z3 as G_INTEG by Th2;
    A7: Norm(zz1) = 1
    proof
      zz3 = zz1*zz2 by Th6;
      then Norm(zz3) = Norm(zz1) * Norm(zz2) by Th34;
      hence Norm(zz1) = 1 by A6,COMPLEX1:30,NAT_1:15;
    end;
    y = x*zz1 by A3,Th6;
    hence Norm(y) = Norm(x) * Norm(zz1) by Th34
    .= Norm(x) by A7;
  end;
  suppose A8: x1 * y1 = 0.Gauss_INT_Ring;
    A9: x1 = 0.Gauss_INT_Ring
    proof
      assume A10: not x1 = 0.Gauss_INT_Ring;
      then y1 = 0.Gauss_INT_Ring by A8,VECTSP_2:def 1;
      hence contradiction by A10,A4;
    end;
    y1 = 0.Gauss_INT_Ring
    proof
      assume A11: not y1 = 0.Gauss_INT_Ring;
      then x1 = 0.Gauss_INT_Ring by A8,VECTSP_2:def 1;
      hence contradiction by A11,A3;
    end;
    hence Norm(x) = Norm(y) by A9;
  end;
end;

theorem Th39:
  for z be Element of Gauss_INT_Ring, zz be G_INTEG st zz = z holds
  z is unital iff zz is g_int_unit
  proof
    let z be Element of Gauss_INT_Ring, zz be G_INTEG such that
    A1: zz = z;
    hereby
      assume A2: z is unital;
      consider x be Element of Gauss_INT_Ring such that
      A3: 1.Gauss_INT_Ring = z * x by A2,GCD_1:def 1,def 2;
      reconsider xx = x as G_INTEG by Th2;
      A4: z * x = zz * xx by A1,Th6;
      reconsider gintone = In(1,G_INT_SET) as G_INTEG;
      Norm(zz) * Norm(xx) = Norm(gintone) by A3,A4,Th34
      .= 1 by COMPLEX1:30;
      hence zz is g_int_unit by NAT_1:15;
    end;
    assume A5: zz is g_int_unit;
    ex w being Element of Gauss_INT_Ring st 1.Gauss_INT_Ring = z * w
    proof
      per cases by A5,A1,Th35;
      suppose A6: z = 1;
        take w = z;
        thus 1.Gauss_INT_Ring = 1*1
        .= z * w by A6,Th6;
      end;
      suppose A7: z = -1;
        take w = z;
        thus 1.Gauss_INT_Ring = (-1)*(-1)
        .= z * w by A7,Th6;
      end;
      suppose A8: z = <i>;
        reconsider w = -<i> as Element of Gauss_INT_Ring by Th3;
        take w;
        thus 1.Gauss_INT_Ring = <i>*(-<i>)
        .= z * w by A8,Th6;
      end;
      suppose A9: z = -<i>;
        reconsider w = <i> as Element of Gauss_INT_Ring by Lm2;
        take w;
        thus 1.Gauss_INT_Ring = (-<i>)*<i>
        .= z * w by A9,Th6;
      end;
    end;
    hence z is unital by GCD_1:def 1,def 2;
  end;

theorem Th40:
  for x, y be G_INTEG holds
  x is_associated_to y iff ex c be G_INTEG st c is g_int_unit & x = c*y
  proof
    let x, y be G_INTEG;
    hereby assume A1:x is_associated_to y;
      reconsider x1 = x, y1 = y as Element of Gauss_INT_Ring by Th3;
      consider c1 be Element of Gauss_INT_Ring such that
      A2: c1 is unital & y1 * c1 = x1 by A1,Th38,GCD_1:18;
      reconsider c = c1 as G_INTEG by Th2;
      A3: c is g_int_unit by A2,Th39;
      c1 * y1 = c * y by Th6;
      hence ex c be G_INTEG st c is g_int_unit & x = c*y by A2,A3;
    end;
    given c0 be G_INTEG such that
    A4: c0 is g_int_unit & x = c0*y;
    reconsider xx = x as Element of Gauss_INT_Ring by Th3;
    reconsider yy = y as Element of Gauss_INT_Ring by Th3;
    reconsider c = c0 as Element of Gauss_INT_Ring by Th3;
    A5: c is unital by A4,Th39;
    c * yy = c0 * y by Th6;
    hence x is_associated_to y by A4,A5,Th37,GCD_1:18;
  end;

theorem Th41:
  for x be G_INTEG st
  Re x <> 0 & Im x <> 0 & Re x <> Im x & - Re x <> Im x holds
  not x*' is_associated_to x
  proof
    let x be G_INTEG such that
    A1: Re x <> 0 & Im x <> 0 & Re x <> Im x & - Re x <> Im x;
    assume x*' is_associated_to x;
    then consider d be G_INTEG such that
    A2: d is g_int_unit & x = d* x*' by Th40;
    A3: x*' = Re x+ (- Im x)*<i>;
    now per cases by A2,Th35;
      suppose d = 1;
        then (Im x) = (- Im x) by A2,A3,COMPLEX1:12;
        hence contradiction by A1;
      end;
      suppose d = -1;
        then (Re x) = (Re (-x*')) by A2
        .= - Re (x*') by COMPLEX1:17
        .= - ( Re x) by COMPLEX1:12,A3;
        hence contradiction by A1;
      end;
      suppose d = <i>;
        then (Im x) = Im (<i>*Re x+ (- Im x)*<i>*<i>) by A2
        .= Re x by COMPLEX1:12;
        hence contradiction by A1;
      end;
      suppose d = -<i>;
        then (Im x) = Im (<i>*(-Re x)+ (Im x)*(-1r)) by A2
        .= - Re x by COMPLEX1:12;
        hence contradiction by A1;
      end;
    end;
    hence contradiction;
  end;

theorem Th42:
  for x, y, z be G_INTEG holds
  x is_associated_to y & y is_associated_to z implies x is_associated_to z
  proof
    let x, y, z be G_INTEG;
    assume A1: x is_associated_to y & y is_associated_to z;
    consider c be G_INTEG such that
    A2: c is g_int_unit & x = c*y by A1,Th40;
    consider d be G_INTEG such that
    A3: d is g_int_unit & y = d*z by A1,Th40;
    A4: x = (c*d) * z by A2,A3;
    reconsider e = c*d as G_INTEG;
    Norm(e) = 1*Norm(d) by A2,Th34
    .= 1 by A3;
    hence thesis by A4,Def20,Th40;
  end;

theorem Th43:
  for x, y be G_INTEG holds
  x is_associated_to y implies x*' is_associated_to y*'
  proof
    let x, y be G_INTEG;
    assume x is_associated_to y;
    then consider c be G_INTEG such that
    A1: c is g_int_unit & x = c*y by Th40;
    A2: x*' = c*' * y*' by A1,COMPLEX1:35;
    Norm(c*') = 1 by A1;
    hence thesis by A2,Def20,Th40;
  end;

theorem
  for x, y be G_INTEG
  st Re y <> 0 & Im y <> 0 & Re y <> Im y & - Re y <> Im y
  & x*' is_associated_to y
  holds not x Divides y & not y Divides x
  proof
    let x, y be G_INTEG such that
    A1: Re y <> 0 & Im y <> 0 & Re y <> Im y & - Re y <> Im y and
    A2: x*' is_associated_to y;
    A3: x*' is_associated_to x implies y*' is_associated_to y
    proof
      assume A4: x*' is_associated_to x;
      then A5: x is_associated_to y by A2,Th42;
      then x*' is_associated_to y*' by Th43;
      then x is_associated_to y*' by A4,Th42;
      hence y*' is_associated_to y by A5,Th42;
    end;
    A6: Norm(x*') <> 0
    proof
      assume Norm(x*') = 0;
      then Norm(y) = 0 by A2,Lm10;
      hence contradiction by A1,Th36,COMPLEX1:4;
    end;
    hereby
      consider c being G_INTEG such that
      A7: c is g_int_unit and
      A8: x*' = c * y by A2,Th40;
      assume x Divides y;
      then consider d being G_INTEG such that
      A9: y = x * d;
      A10: x*' = (c*d) * x by A8,A9;
      reconsider e = c*d as G_INTEG;
      A11: Norm(e) = Norm(c)*Norm(d) by Th34
      .= Norm(d) by A7;
      per cases;
      suppose d is g_int_unit;
        hence contradiction
        by A3,A1,A10,A11,Def20,Th40,Th41;
      end;
      suppose A12: not d is g_int_unit;
        Norm(x*') = Norm(e) * Norm(x) by A10,Th34;
        hence contradiction by A11,A12,A6,XCMPLX_1:7;
      end;
    end;
    consider c being G_INTEG such that
    A13: c is g_int_unit and
    A14: y = c * x*' by A2,Th40;
    assume y Divides x;
    then consider d being G_INTEG such that
    A15: x = y * d;
    A16: x = (c*d) * x*' by A14,A15;
    reconsider e = c*d as G_INTEG;
    A17: Norm(e) = Norm(c)*Norm(d) by Th34
    .= Norm(d) by A13;
    per cases;
    suppose d is g_int_unit;
      hence contradiction
      by A3,A1,A16,A17,Def20,Th40,Th41;
    end;
    suppose A18: not d is g_int_unit;
      Norm(x) = Norm(e) * Norm(x*') by A16,Th34;
      hence contradiction by A17,A18,A6,XCMPLX_1:7;
    end;
  end;

definition
  let p be G_INTEG;
  attr p is g_prime means
  Norm(p) > 1 &
  for z being G_INTEG holds
  not z Divides p or z is g_int_unit or z is_associated_to p;
end;

Lm11:
for a be Integer holds not a*a is Prime
proof
  let a be Integer;
  reconsider b = |.a.| as Element of NAT;
  A1: a*a = a^2
  .= |.a.| ^2 by COMPLEX1:75
  .= b*b;
  per cases;
  suppose b < 2;
    then b = 0 or b = 1 by NAT_1:23;
    hence thesis by A1,INT_2:def 4;
  end;
  suppose 2 <= b;
    then 1 < b by XXREAL_0:2;
    then A2: b*1 < b*b by XREAL_1:68;
    b divides b*b by INT_1:def 3;
    hence thesis by A1,A2,INT_2:def 4;
  end;
end;

Lm12:
for a be Integer st |.a.| <> 1
holds not 2*a*a is Prime
proof
  let a be Integer;
  assume A1: |.a.| <> 1;
  reconsider b = |.a.| as Element of NAT;
  A2: a*a = a^2
  .= |.a.| ^2 by COMPLEX1:75
  .= b*b;
  per cases;
  suppose b < 2;
    then b = 0 or b = 1 by NAT_1:23;
    hence thesis by A1,A2;
  end;
  suppose A3: 2 <= b;
    1 < b by XXREAL_0:2,A3;
    then A4: b*(1 qua Real) < b*b by XREAL_1:68;
    A5: 1*(b*b) < 2*(b*b) by A3,XREAL_1:68;
    b divides 2*b*b by INT_1:def 3;
    hence thesis by A2,A5,A4,INT_2:def 4;
  end;
end;

theorem
  for q be G_INTEG st Norm(q) is Prime & Norm(q) <> 2 holds
  Re q <> 0 & Im q <> 0 & Re q <> Im q & - Re q <> Im q
  proof
    let q be G_INTEG;
    assume A1: Norm(q) is Prime & Norm(q) <> 2;
    A2: (Re q)*(Re q) = (Re q)^2
    .= |.(Re q).| ^2 by COMPLEX1:75
    .=|.(Re q).| * |.(Re q).|;
    A3: Norm(q)=(Re q+Im q*<i>)*(Re q-(Im q)*<i>) by COMPLEX1:13
    .= (Re q)^2 + (Im q)^2;
    assume A4: not (Re q <> 0 & Im q <> 0 & Re q <> Im q & - Re q <> Im q );
    per cases by A4;
    suppose Re q = 0;
      hence contradiction by A1,A3,Lm11;
    end;
    suppose Im q = 0;
      hence contradiction by A1,A3,Lm11;
    end;
    suppose A5: Re q = Im q; then
      A6: Norm(q) = 2*(Re q)*(Re q) by A3;
      |.Re q.| <> 1 by A1,A3,A5,A2;
      hence contradiction by A1,A6,Lm12;
    end;
    suppose A7: - Re q = Im q; then
      A8: Norm(q) = 2*(Re q)*(Re q) by A3;
      |.Re q.| <> 1 by A1,A3,A7,A2;
      hence contradiction by A1,A8,Lm12;
    end;
  end;

theorem
  for q be G_INTEG st Norm(q) is Prime holds q is g_prime
  proof
    let q be G_INTEG such that
    A1: Norm(q) is Prime;
    for z being G_INTEG holds
    not z Divides q or z is g_int_unit or z is_associated_to q
    proof
      let z be G_INTEG;
      per cases;
      suppose z is g_int_unit;
        hence thesis;
      end;
      suppose not z is g_int_unit & z is_associated_to q;
        hence thesis;
      end;
      suppose A2: not z is g_int_unit & not z is_associated_to q;
        not z Divides q
        proof
          assume A3: z Divides q;
          consider c being G_INTEG such that
          A4: q = z * c by A3;
          A5: Norm(q) = Norm(z)*Norm(c) by A4,Th34;
          then A6: Norm(z) divides Norm(q) by INT_1:def 3;
          A7: Norm(z) > 1
          proof
            Norm(z) <> 0
            proof
              assume Norm(z) = 0;
              then Norm(q) = 0*Norm(c) by A4,Th34
              .= 0;
              hence contradiction by A1;
            end;
            then Norm z >= 0+1 by NAT_1:13;
            hence thesis by A2,XXREAL_0:1;
          end;
          A8: Norm(c) <> 1 by A2,A4,Def20,Th40;
          Norm(q) <> Norm(z) by A1,A5,A8,XCMPLX_1:7;
          hence contradiction by A1,A6,A7,INT_2:def 4;
        end;
        hence thesis;
      end;
    end;
    hence thesis by A1,INT_2:def 4;
  end;

Lm13:
ex f being Function of Gauss_INT_Ring,NAT
st for x be G_INTEG holds f.x = Norm(x)
proof
  defpred P[object,object]
  means ex z be G_INTEG st $1 = z & $2 = Norm(z);

  A1: for x being Element of the carrier of Gauss_INT_Ring
  ex y being Element of NAT st P[x,y]
  proof
    let x being Element of the carrier of Gauss_INT_Ring;
    reconsider z = x as G_INTEG by Th2;
    Norm(z) is Element of NAT by ORDINAL1:def 12;
    hence thesis;
  end;
  consider f being Function of Gauss_INT_Ring, NAT such that
  A2: for x being Element of Gauss_INT_Ring
  holds P[x,f.x] from FUNCT_2:sch 3(A1);
  now let x be G_INTEG;
    x is Element of the carrier of Gauss_INT_Ring by Th3;
    then ex z be G_INTEG st x=z & f.x = Norm(z) by A2;
    hence f.x = Norm(x);
  end;
  hence thesis;
end;

theorem Th47:
  for q be G_RAT holds Norm(q) = |. Re q .|^2 + |. Im q .| ^2
  proof
    let q be G_RAT;
    A1: |. Re q .|^2 = (Re q)^2 by COMPLEX1:75;
    thus
    Norm(q)=(Re q+Im q*<i>)*(Re q-(Im q)*<i>) by COMPLEX1:13
    .= (Re q)^2 + (Im q)^2
    .= |. Re q .|^2 + |. Im q .| ^2 by A1,COMPLEX1:75;
  end;

theorem Th48:
  for q be Element of REAL ex m be Element of INT st |.q - m .| <= 1/2
  proof
    let q be Element of REAL;
    per cases;
    suppose A1: |.q - [\q/] .| <= 1/2;
      reconsider  m= [\q/] as Element of INT by INT_1:def 2;
      take m;
      thus |.q - m .| <= 1/2 by A1;
    end;
    suppose A2: not |.q - [\q/] .| <= 1/2;
      0 <= q - [\q/] by INT_1:def 6,XREAL_1:48;
      then 1/2 < q - [\q/] by A2,ABSVALUE:def 1;
      then 1/2 -1 <= q - [\q/] -1  by XREAL_1:9;
      then A3: -1/2 <= q - ([\q/] + 1 );
      q - ([\q/] + 1) <= ([\q/] + 1) -([\q/] + 1) by INT_1:29,XREAL_1:9;
      then A4: q - ([\q/] + 1) <= 0;
      reconsider m = [\q/] + 1 as Element of INT by INT_1:def 2;
      take m;
      thus |. q - m  .| <= 1/2 by A3,A4,ABSVALUE:5;
    end;
  end;

Lm14: for f being Function of Gauss_INT_Ring,NAT
st for x be G_INTEG holds f.x = Norm(x) holds
for a, b being Element of Gauss_INT_Ring st b <> 0. Gauss_INT_Ring
holds ex q, r being Element of Gauss_INT_Ring st
( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) )
proof
  let f be Function of Gauss_INT_Ring,NAT;
  assume A1: for x be G_INTEG holds f.x = Norm(x);
  let a, b being Element of Gauss_INT_Ring;
  assume A2: b <> 0. Gauss_INT_Ring;
  reconsider a0 = a, b0 = b as G_INTEG by Th2;
  reconsider x = a0/b0, b1 = b0 as G_RAT;
  consider m be Element of INT such that
  A3: |.(Re x) - m .| <= 1/2 by Th48;
  consider n be Element of INT such that
  A4: |.(Im x) - n .| <= 1/2 by Th48;
  set q0 = m+n*<i>;
  reconsider q0 as G_INTEG;
  reconsider q1 = q0 as G_RAT;
  reconsider r0 = a0 - q0*b0 as G_INTEG;
  A5: Re(x -q0) = (Re x) - (Re q0) by COMPLEX1:19
  .= (Re x) - m by COMPLEX1:12;
  A6: Im(x -q0) = (Im x) - (Im q0) by COMPLEX1:19
  .= (Im x) - n by COMPLEX1:12;
  reconsider xq1 = x-q1 as G_RAT;
  0 <= |.(Re x) - m .| by COMPLEX1:46;
  then A7: |.(Re x) - m .| ^2 <= (1/2)^2 by A3,SQUARE_1:15;
  0 <= |.(Im x) - n .| by COMPLEX1:46;
  then A8: |.(Im x) - n .| ^2 <= (1/2)^2 by A4,SQUARE_1:15;
  |.(Re x) - m .| ^2 + |. (Im x) - n .| ^2 <= (1/2)^2 + (1/2)^2
  by A7,A8,XREAL_1:7;
  then A9: Norm(xq1) <= 1/2 by A5,A6,Th47;
  reconsider bxq1 = b1*xq1 as G_RAT;
  A10: b1*xq1 = b0*(a0/b0) -b0*q0
  .= r0 by A2,XCMPLX_1:87;
  A11: Norm(bxq1) = Norm(b1)*Norm(xq1) by Th34;
  A12: Norm(r0) <= Norm(b1)/2 by A9,A10,A11,XREAL_1:64;
  Norm(b0) <> 0 by A2,Th36;
  then Norm(b1)/2 < Norm(b1) by XREAL_1:216;
  then A13: Norm(r0) < Norm(b1) by A12,XXREAL_0:2;
  reconsider q = q0, r = r0 as Element of Gauss_INT_Ring by Th3;
  A14: q * b = q0*b0 by Th6;
  a0 = q0*b0 + r0;
  then A15: a = (q * b) + r by A14,Th4;
  A16: f.r = Norm(r0) by A1;
  f.b = Norm(b0)  by A1;
  hence thesis by A13,A15,A16;
end;

registration
  cluster Gauss_INT_Ring -> Euclidian;
  coherence
proof
  consider f being Function of the carrier of Gauss_INT_Ring,NAT such that
  A1: for x be G_INTEG holds f.x = Norm(x) by Lm13;
  for a, b being Element of Gauss_INT_Ring st b <> 0. Gauss_INT_Ring holds
  ex q, r being Element of Gauss_INT_Ring st
  ( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) ) by Lm14,A1;
  hence thesis by INT_3:def 8;
end;
end;