:: Gaussian Integers
::  by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013-2021 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, XTUPLE_0, QUOFIELD, SQUARE_1, RAT_1, NAT_1, INT_3,
      ORDINAL1;
 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;


begin :: 1. Gaussian integer ring

theorem :: GAUSSINT:1
  for x,y be Nat st x+y = 1 holds (x = 1 & y = 0) or (x = 0 & y = 1);

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

registration
  cluster -> g_integer for Integer;
end;

definition
  mode G_INTEG is g_integer Complex;
end;

registration
  let z be G_INTEG;
  cluster Re z -> integer;
  cluster Im z -> integer;
end;

registration
  let z1, z2 be G_INTEG;
  cluster z1+z2 -> g_integer;
  cluster z1-z2 -> g_integer;
  cluster z1*z2 -> g_integer;
end;

registration
  cluster <i> -> g_integer;
end;

registration
  let z be G_INTEG;
  cluster -z -> g_integer;
  cluster z *' -> g_integer;
end;

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

definition
  func G_INT_SET -> Subset of COMPLEX equals
:: GAUSSINT:def 2
  the set of all z where z is G_INTEG;
end;

registration
  cluster G_INT_SET -> non empty;
end;

registration
  let i be Integer;
  reduce In(i,G_INT_SET) to i;
end;

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

theorem :: GAUSSINT:3
  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
:: GAUSSINT:def 3
  addcomplex || G_INT_SET;
end;

definition
  func g_int_mult -> BinOp of G_INT_SET equals
:: GAUSSINT:def 4
  multcomplex || G_INT_SET;
end;

definition
  func Sc_Mult -> Function of [:the carrier of INT.Ring,G_INT_SET :],
    G_INT_SET equals
:: GAUSSINT:def 5
  multcomplex | [:the carrier of INT.Ring, G_INT_SET:];
end;

theorem :: GAUSSINT:4
  for z, w be G_INTEG holds g_int_add.(z,w) = z+w;

theorem :: GAUSSINT:5
  for z be G_INTEG, i be Integer holds Sc_Mult.(i,z) = i*z;

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

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

theorem :: GAUSSINT:6
  for z,w be G_INTEG holds g_int_mult.(z,w) = z*w;

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

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

registration
  cluster Gauss_INT_Ring -> domRing-like;
end;

registration
  cluster Gauss_INT_Ring -> commutative;
end;

theorem :: GAUSSINT:7
  for x be Element of Gauss_INT_Ring holds x is G_INTEG;

theorem :: GAUSSINT:8
  for x be G_INTEG holds x is Element of Gauss_INT_Ring;

begin :: 2. Z-Algebra

registration
  cluster non empty for AlgebraStr over INT.Ring;
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;
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;
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;
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 :: GAUSSINT:9
  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;
end;

registration
  cluster G_INT_SET -> denumerable;
end;

registration
  cluster Gauss_INT_Ring -> non degenerated;
end;

begin :: 4. Quotient field of Gaussian integer ring

definition
  func Gauss_INT_Field -> strict non empty doubleLoopStr equals
:: GAUSSINT:def 9
  the_Field_of_Quotients (Gauss_INT_Ring);
end;

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

definition
  let z be Complex;
  attr z is g_rational means
:: GAUSSINT:def 10

  Re z in RAT & Im z in RAT;
end;

registration
  cluster -> g_rational for Rational;
end;

definition
  mode G_RAT is g_rational Complex;
end;

registration
  let z be G_RAT;
  cluster Re z -> rational;
  cluster Im z -> rational;
end;

registration
  let z1, z2 be G_RAT;
  cluster z1+z2 -> g_rational;
  cluster z1-z2 -> g_rational;
  cluster z1*z2 -> g_rational;
end;

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

registration
  let z be G_RAT;
  cluster -z -> g_rational;
  cluster z" -> g_rational;
end;

definition
  func G_RAT_SET -> Subset of COMPLEX equals
:: GAUSSINT:def 11
  the set of all z where z is G_RAT;
end;

registration
  cluster G_RAT_SET -> non empty;
end;

registration
  cluster -> g_rational for G_INTEG;
end;

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

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

theorem :: GAUSSINT:12
  for p be G_RAT ex x, y be G_INTEG st y <> 0 & p = x/y;

definition
  func g_rat_add -> BinOp of G_RAT_SET equals
:: GAUSSINT:def 12
  addcomplex || G_RAT_SET;
end;

definition
  func g_rat_mult -> BinOp of G_RAT_SET equals
:: GAUSSINT:def 13
  multcomplex || G_RAT_SET;
end;

begin

registration
  let i be Integer;
  reduce In(i,RAT) to i;
end;

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

theorem :: GAUSSINT:13
  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;

theorem :: GAUSSINT:14
  F_Rat is Subfield of F_Real;

registration
  cluster F_Rat -> add-associative right_zeroed right_complementable Abelian
  commutative associative left_unital right_unital distributive
  almost_left_invertible non degenerated;
end;

registration
  cluster F_Rat -> well-unital;
end;

registration
  cluster -> rational for Element of F_Rat;
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;
  identify x*y with a*b when x = a, y = b;
end;

registration
  let x be Element of F_Rat, y be Rational;
  identify -x with -y when x = y;
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;
end;

theorem :: GAUSSINT:15
  for x be Element of F_Rat, x1 be Rational st x <> 0.F_Rat & x1 = x
  holds x" = x1";

theorem :: GAUSSINT:16
  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;

theorem :: GAUSSINT:17
  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;

theorem :: GAUSSINT:18
  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;

theorem :: GAUSSINT:19
  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;

theorem :: GAUSSINT:20
  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;

theorem :: GAUSSINT:21
  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";

theorem :: GAUSSINT:22
  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;

theorem :: GAUSSINT:23
  for K1 be Subfield of F_Rat holds NAT c= the carrier of K1;

theorem :: GAUSSINT:24
  for K1 be Subfield of F_Rat holds INT c= the carrier of K1;

theorem :: GAUSSINT:25
  for K1 be Subfield of F_Rat holds
  the carrier of K1 = the carrier of F_Rat;

theorem :: GAUSSINT:26
  for K1 being strict Subfield of F_Rat holds K1 = F_Rat;

registration
  cluster F_Rat -> prime;
end;

begin :: 6. Gaussian rational number field

registration
  let i be Rational;
  reduce In(i,G_RAT_SET) to i;
end;

definition
  func RSc_Mult -> Function of [:the carrier of F_Rat,G_RAT_SET :], G_RAT_SET
  equals
:: GAUSSINT:def 15
  multcomplex | [:the carrier of F_Rat,G_RAT_SET:];
end;

theorem :: GAUSSINT:27
  for z, w be G_RAT holds g_rat_add.(z,w) = z+w;

theorem :: GAUSSINT:28
  for z be G_RAT, i be Element of RAT holds RSc_Mult.(i,z) = i*z;

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

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

theorem :: GAUSSINT:29
  for z, w be G_RAT holds g_rat_mult.(z,w) = z*w;

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

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

theorem :: GAUSSINT:30
  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;

begin :: 7. Gaussian integer ring is Euclidian

definition
  let a,b be G_INTEG;
  pred a Divides b means
:: GAUSSINT:def 18
  ex c being G_INTEG st b = a * c;
  reflexivity;
end;

theorem :: GAUSSINT:31
  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;

theorem :: GAUSSINT:32
  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;

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

definition
  let z be G_RAT;
  func Norm(z) -> Rational equals
:: GAUSSINT:def 19
  z * (z *');
end;

registration
  let z be G_RAT;
  cluster Norm(z) -> non negative;
end;

registration
  let z be G_INTEG;
  cluster Norm(z) -> natural;
end;

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

theorem :: GAUSSINT:34
  for x, y be G_RAT holds Norm(x*y) = Norm(x)*Norm(y);

theorem :: GAUSSINT:35
  for x be G_INTEG holds Norm(x) = 1 iff x = 1 or x = -1 or x = <i> or x = -<i>
;

theorem :: GAUSSINT:36
  for x be G_INTEG holds Norm(x) = 0 implies x = 0;

definition
  let z be G_INTEG;
  attr z is g_int_unit means
:: GAUSSINT:def 20

  Norm(z) = 1;
end;

definition
  let x,y be G_INTEG;
  pred x is_associated_to y means
:: GAUSSINT:def 21
  x Divides y & y Divides x;
  symmetry;
end;

theorem :: GAUSSINT:37
  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;

theorem :: GAUSSINT:38
  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;

theorem :: GAUSSINT:39
  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;

theorem :: GAUSSINT:40
  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;

theorem :: GAUSSINT:41
  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;

theorem :: GAUSSINT:42
  for x, y, z be G_INTEG holds
  x is_associated_to y & y is_associated_to z implies x is_associated_to z;

theorem :: GAUSSINT:43
  for x, y be G_INTEG holds
  x is_associated_to y implies x*' is_associated_to y*';

theorem :: GAUSSINT:44
  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;

definition
  let p be G_INTEG;
  attr p is g_prime means
:: GAUSSINT:def 22
  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;

theorem :: GAUSSINT:45
  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;

theorem :: GAUSSINT:46
  for q be G_INTEG st Norm(q) is Prime holds q is g_prime;

theorem :: GAUSSINT:47
  for q be G_RAT holds Norm(q) = |. Re q .|^2 + |. Im q .| ^2;

theorem :: GAUSSINT:48
  for q be Element of REAL ex m be Element of INT st |.q - m .| <= 1/2;

registration
  cluster Gauss_INT_Ring -> Euclidian;
end;