:: Gaussian Integers
:: by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013-2021 Association of Mizar Users

theorem Th1: :: GAUSSINT:1

for x, y being Nat holds
( not x + y = 1 or ( x = 1 & y = 0 ) or ( x = 0 & y = 1 ) )

proof end;

definition

let z be Complex;

attr z is g_integer means :Def1: :: GAUSSINT:def 1
( Re z in INT & Im z in INT );

end;

:: deftheorem Def1 defines g_integer GAUSSINT:def 1 :
for z being Complex holds
( z is g_integer iff ( Re z in INT & Im z in INT ) );

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 integer -> g_integer for object ;

coherence
for b₁ being Integer holds b₁ is g_integer

proof end;

end;

definition

mode G_INTEG is g_integer Complex;

end;

registration

let z be G_INTEG;

cluster Re z -> integer ;

coherence
Re z is integer

proof end;

cluster Im z -> integer ;

coherence
Im z is integer

proof end;

end;

registration

let z1, z2 be G_INTEG;

cluster z1 + z2 -> g_integer ;

coherence
z1 + z2 is g_integer

proof end;

cluster z1 - z2 -> g_integer ;

coherence
z1 - z2 is g_integer

proof end;

cluster z1 * z2 -> g_integer ;

coherence
z1 * z2 is g_integer

proof end;

end;

registration

cluster <i> -> g_integer ;

coherence
<i> is g_integer by COMPLEX1:7, INT_1:def 2;

end;

registration

let z be G_INTEG;

cluster - z -> g_integer ;

coherence
- z is g_integer

proof end;

cluster z *' -> g_integer ;

coherence
z *' is g_integer ;

end;

registration

let z be G_INTEG;
let n be Integer;

cluster n * z -> g_integer ;

coherence
n * z is g_integer ;

end;

definition

func G_INT_SET -> Subset of COMPLEX equals :: GAUSSINT:def 2
{ z where z is G_INTEG : verum } ;

correctness
coherence
{ z where z is G_INTEG : verum } is Subset of COMPLEX;

proof end;

end;

:: deftheorem defines G_INT_SET GAUSSINT:def 2 :
G_INT_SET = { z where z is G_INTEG : verum } ;

registration

cluster G_INT_SET -> non empty ;

coherence
not G_INT_SET is empty

proof end;

end;

Lm2: <i> in G_INT_SET
;

registration

let i be Integer;

reduce In (i,G_INT_SET) to i;

reducibility
In (i,G_INT_SET) = i

proof end;

end;

theorem Th2: :: GAUSSINT:2

for x being object st x in G_INT_SET holds
x is G_INTEG

proof end;

theorem Th3: :: GAUSSINT:3

for x being 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;

correctness
coherence
addcomplex || G_INT_SET is BinOp of G_INT_SET;

proof end;

end;

:: deftheorem defines g_int_add GAUSSINT:def 3 :
g_int_add = addcomplex || G_INT_SET;

definition

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

correctness
coherence
multcomplex || G_INT_SET is BinOp of G_INT_SET;

proof end;

end;

:: deftheorem defines g_int_mult GAUSSINT:def 4 :
g_int_mult = multcomplex || G_INT_SET;

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:];

correctness
coherence
multcomplex | [: the carrier of INT.Ring,G_INT_SET:] is Function of [: the carrier of INT.Ring,G_INT_SET:],G_INT_SET;

proof end;

end;

:: deftheorem defines Sc_Mult GAUSSINT:def 5 :
Sc_Mult = multcomplex | [: the carrier of INT.Ring,G_INT_SET:];

theorem Th4: :: GAUSSINT:4

for z, w being G_INTEG holds g_int_add . (z,w) = z + w

proof end;

theorem Th5: :: GAUSSINT:5

for z being G_INTEG
for i being Integer holds Sc_Mult . (i,z) = i * z

proof end;

definition

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

coherence
ModuleStr(# G_INT_SET,g_int_add,(In (0,G_INT_SET)),Sc_Mult #) is non empty strict ModuleStr over INT.Ring ;

end;

:: deftheorem defines Gauss_INT_Module GAUSSINT:def 6 :
Gauss_INT_Module = ModuleStr(# G_INT_SET,g_int_add,(In (0,G_INT_SET)),Sc_Mult #);

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

Lm3: Gauss_INT_Module is Z_Module

proof end;

registration

cluster Gauss_INT_Module -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( Gauss_INT_Module is Abelian & Gauss_INT_Module is add-associative & Gauss_INT_Module is right_zeroed & Gauss_INT_Module is right_complementable & Gauss_INT_Module is scalar-distributive & Gauss_INT_Module is vector-distributive & Gauss_INT_Module is scalar-associative & Gauss_INT_Module is scalar-unital ) by Lm3;

end;

theorem Th6: :: GAUSSINT:6

for z, w being G_INTEG holds g_int_mult . (z,w) = z * w

proof end;

definition

func Gauss_INT_Ring -> non empty strict 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)) #);

coherence
doubleLoopStr(# G_INT_SET,g_int_add,g_int_mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #) is non empty strict doubleLoopStr ;

end;

:: deftheorem defines Gauss_INT_Ring GAUSSINT:def 7 :
Gauss_INT_Ring = doubleLoopStr(# G_INT_SET,g_int_add,g_int_mult,(In (1,G_INT_SET)),(In (0,G_INT_SET)) #);

Lm4: Gauss_INT_Ring is Ring

proof end;

registration

cluster Gauss_INT_Ring -> non empty right_complementable strict associative Abelian add-associative right_zeroed well-unital distributive ;

coherence
( Gauss_INT_Ring is Abelian & Gauss_INT_Ring is add-associative & Gauss_INT_Ring is right_zeroed & Gauss_INT_Ring is right_complementable & Gauss_INT_Ring is associative & Gauss_INT_Ring is well-unital & Gauss_INT_Ring is distributive ) by Lm4;

end;

registration

cluster Gauss_INT_Ring -> non empty strict domRing-like ;

coherence
Gauss_INT_Ring is domRing-like

proof end;

end;

registration

cluster Gauss_INT_Ring -> non empty strict commutative ;

coherence
Gauss_INT_Ring is commutative

proof end;

end;

theorem :: GAUSSINT:7

for x being Element of Gauss_INT_Ring holds x is G_INTEG by Th2;

theorem :: GAUSSINT:8

for x being G_INTEG holds x is Element of Gauss_INT_Ring by Th3;

registration

cluster non empty for AlgebraStr over INT.Ring ;

existence
not for b₁ being AlgebraStr over INT.Ring holds b₁ is empty

proof end;

end;

definition

end;

:: deftheorem GAUSSINT:def 8 :
canceled;

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
not AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is 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 #) -> right_complementable associative commutative Abelian add-associative right_zeroed right-distributive right_unital vector-distributive scalar-distributive scalar-associative mix-associative ;

correctness
coherence
( AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is strict & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is Abelian & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is add-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_zeroed & 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 & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is commutative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_unital & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right-distributive & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is mix-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is scalar-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is vector-distributive & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is scalar-distributive );

proof end;

end;

registration

cluster non empty right_complementable associative commutative Abelian add-associative right_zeroed right-distributive right_unital vector-distributive scalar-distributive scalar-associative strict mix-associative for AlgebraStr over INT.Ring ;

existence
ex b₁ being non empty AlgebraStr over INT.Ring st
( b₁ is strict & b₁ is Abelian & b₁ is add-associative & b₁ is right_zeroed & b₁ is right_complementable & b₁ is commutative & b₁ is associative & b₁ is right_unital & b₁ is right-distributive & b₁ is mix-associative & b₁ is scalar-associative & b₁ is vector-distributive & b₁ is scalar-distributive )

proof end;

end;

definition

mode Z_Algebra is non empty right_complementable associative commutative Abelian add-associative right_zeroed right-distributive right_unital vector-distributive scalar-distributive scalar-associative mix-associative 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 non empty right_complementable associative commutative Abelian add-associative right_zeroed right-distributive right_unital vector-distributive scalar-distributive scalar-associative strict mix-associative AlgebraStr over INT.Ring ;

registration

cluster INT -> denumerable ;

coherence
INT is denumerable

proof end;

end;

registration

cluster G_INT_SET -> denumerable ;

coherence
G_INT_SET is denumerable

proof end;

end;

registration

cluster Gauss_INT_Ring -> non empty non degenerated strict ;

correctness
coherence
not Gauss_INT_Ring is degenerated ;
;

end;

definition

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

correctness
coherence
the_Field_of_Quotients Gauss_INT_Ring is non empty strict doubleLoopStr ;
;

end;

:: deftheorem defines Gauss_INT_Field GAUSSINT:def 9 :
Gauss_INT_Field = the_Field_of_Quotients Gauss_INT_Ring;

registration

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

correctness
coherence
( not Gauss_INT_Field is degenerated & Gauss_INT_Field is almost_left_invertible & Gauss_INT_Field is strict & Gauss_INT_Field is Abelian & Gauss_INT_Field is associative & Gauss_INT_Field is distributive );
;

end;

definition

let z be Complex;

attr z is g_rational means :Def10: :: GAUSSINT:def 10
( Re z in RAT & Im z in RAT );

end;

:: deftheorem Def10 defines g_rational GAUSSINT:def 10 :
for z being Complex holds
( z is g_rational iff ( Re z in RAT & Im z in RAT ) );

registration

cluster rational -> g_rational for object ;

coherence
for b₁ being Rational holds b₁ is g_rational

proof end;

end;

definition

mode G_RAT is g_rational Complex;

end;

registration

let z be G_RAT;

cluster Re z -> rational ;

coherence
Re z is rational

proof end;

cluster Im z -> rational ;

coherence
Im z is rational

proof end;

end;

registration

let z1, z2 be G_RAT;

cluster z1 + z2 -> g_rational ;

coherence
z1 + z2 is g_rational

proof end;

cluster z1 - z2 -> g_rational ;

coherence
z1 - z2 is g_rational

proof end;

cluster z1 * z2 -> g_rational ;

coherence
z1 * z2 is g_rational

proof end;

end;

registration

let z be G_RAT;
let n be Rational;

cluster n * z -> g_rational ;

coherence
n * z is g_rational ;

end;

registration

let z be G_RAT;

cluster - z -> g_rational ;

coherence
- z is g_rational

proof end;

cluster z " -> g_rational ;

coherence
z " is g_rational

proof end;

end;

definition

func G_RAT_SET -> Subset of COMPLEX equals :: GAUSSINT:def 11
{ z where z is G_RAT : verum } ;

correctness
coherence
{ z where z is G_RAT : verum } is Subset of COMPLEX;

proof end;

end;

:: deftheorem defines G_RAT_SET GAUSSINT:def 11 :
G_RAT_SET = { z where z is G_RAT : verum } ;

registration

cluster G_RAT_SET -> non empty ;

coherence
not G_RAT_SET is empty

proof end;

end;

registration

cluster complex g_integer -> g_rational for object ;

coherence
for b₁ being G_INTEG holds b₁ is g_rational by NUMBERS:14, Def1;

end;

theorem Th10: :: GAUSSINT:10

for x being object st x in G_RAT_SET holds
x is G_RAT

proof end;

theorem Th11: :: GAUSSINT:11

for x being object st x is G_RAT holds
x in G_RAT_SET ;

theorem Th12: :: GAUSSINT:12

for p being G_RAT ex x, y being G_INTEG st
( y <> 0 & p = x / y )

proof end;

Lm5: for x1, y1, x2, y2 being G_INTEG
for 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 end;

definition

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

correctness
coherence
addcomplex || G_RAT_SET is BinOp of G_RAT_SET;

proof end;

end;

:: deftheorem defines g_rat_add GAUSSINT:def 12 :
g_rat_add = addcomplex || G_RAT_SET;

definition

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

correctness
coherence
multcomplex || G_RAT_SET is BinOp of G_RAT_SET;

proof end;

end;

:: deftheorem defines g_rat_mult GAUSSINT:def 13 :
g_rat_mult = multcomplex || G_RAT_SET;

Lm6: addreal || RAT = addrat

proof end;

Lm7: multreal || RAT = multrat

proof end;

registration

let i be Integer;

reduce In (i,RAT) to i;

reducibility
In (i,RAT) = i by RAT_1:def 2, SUBSET_1:def 8;

end;

definition

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

correctness
coherence
doubleLoopStr(# RAT,addrat,multrat,(In (1,RAT)),(In (0,RAT)) #) is non empty strict doubleLoopStr ;
;

end;

:: deftheorem defines F_Rat GAUSSINT:def 14 :
F_Rat = doubleLoopStr(# RAT,addrat,multrat,(In (1,RAT)),(In (0,RAT)) #);

theorem Th13: :: 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 & F_Rat is commutative & F_Rat is almost_left_invertible & not F_Rat is degenerated )

proof end;

theorem :: GAUSSINT:14

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

registration

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

correctness
coherence
( F_Rat is add-associative & F_Rat is right_zeroed & F_Rat is right_complementable & F_Rat is Abelian & F_Rat is commutative & F_Rat is associative & F_Rat is left_unital & F_Rat is right_unital & F_Rat is distributive & F_Rat is almost_left_invertible & not F_Rat is degenerated );
by EC_PF_1:2, Th13;

end;

registration

cluster F_Rat -> non empty strict well-unital ;

coherence
F_Rat is well-unital ;

end;

registration

cluster -> rational for Element of the carrier of F_Rat;

coherence
for b₁ being Element of F_Rat holds b₁ is rational ;

end;

registration

let x, y be Element of F_Rat;
let a, b be Rational;

identify x + y with a + b when x = a, y = b;

compatibility
( x = a & y = b implies x + y = a + b ) by BINOP_2:def 15;

identify x * y with a * b when x = a, y = b;

compatibility
( x = a & y = b implies x * y = a * b ) by BINOP_2:def 17;

end;

registration

let x be Element of F_Rat;
let y be Rational;

identify - x with - y when x = y;

compatibility
( x = y implies - x = - y )

proof end;

end;

registration

let x, y be Element of F_Rat;
let a, b be Rational;

identify x - y with a - b when x = a, y = b;

compatibility
( x = a & y = b implies x - y = a - b ) ;

end;

theorem Th15: :: GAUSSINT:15

for x being Element of F_Rat
for x1 being Rational st x <> 0. F_Rat & x1 = x holds
x " = x1 "

proof end;

theorem Th16: :: GAUSSINT:16

for x, y being Element of F_Rat
for x1, y1 being Rational st x1 = x & y1 = y & y <> 0. F_Rat holds
x / y = x1 / y1 by Th15;

theorem Th17: :: GAUSSINT:17

for K being Field
for K1 being Subfield of K
for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x + y = x1 + y1

proof end;

theorem Th18: :: GAUSSINT:18

for K being Field
for K1 being Subfield of K
for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x * y = x1 * y1

proof end;

theorem Th19: :: GAUSSINT:19

for K being Field
for K1 being Subfield of K
for x being Element of K
for x1 being Element of K1 st x = x1 holds
- x = - x1

proof end;

theorem :: GAUSSINT:20

for K being Field
for K1 being Subfield of K
for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & y = y1 holds
x - y = x1 - y1

proof end;

theorem Th21: :: GAUSSINT:21

for K being Field
for K1 being Subfield of K
for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & x <> 0. K holds
x " = x1 "

proof end;

theorem :: GAUSSINT:22

for K being Field
for K1 being Subfield of K
for x, y being Element of K
for x1, y1 being Element of K1 st x = x1 & y = y1 & y <> 0. K holds
x / y = x1 / y1

proof end;

set K = F_Rat ;

set C = the carrier of F_Rat;

theorem Th23: :: GAUSSINT:23

for K1 being Subfield of F_Rat holds NAT c= the carrier of K1

proof end;

theorem Th24: :: GAUSSINT:24

for K1 being Subfield of F_Rat holds INT c= the carrier of K1

proof end;

theorem Th25: :: GAUSSINT:25

for K1 being Subfield of F_Rat holds the carrier of K1 = the carrier of F_Rat

proof end;

theorem :: GAUSSINT:26

for K1 being strict Subfield of F_Rat holds K1 = F_Rat

proof end;

registration

cluster F_Rat -> non empty strict prime ;

coherence
F_Rat is prime

proof end;

end;

registration

let i be Rational;

reduce In (i,G_RAT_SET) to i;

reducibility
In (i,G_RAT_SET) = i

proof end;

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:];

coherence
multcomplex | [: the carrier of F_Rat,G_RAT_SET:] is Function of [: the carrier of F_Rat,G_RAT_SET:],G_RAT_SET

proof end;

end;

:: deftheorem defines RSc_Mult GAUSSINT:def 15 :
RSc_Mult = multcomplex | [: the carrier of F_Rat,G_RAT_SET:];

theorem Th27: :: GAUSSINT:27

for z, w being G_RAT holds g_rat_add . (z,w) = z + w

proof end;

theorem Th28: :: GAUSSINT:28

for z being G_RAT
for i being Element of RAT holds RSc_Mult . (i,z) = i * z

proof end;

definition

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

coherence
ModuleStr(# G_RAT_SET,g_rat_add,(In (0,G_RAT_SET)),RSc_Mult #) is non empty strict ModuleStr over F_Rat ;

end;

:: deftheorem defines Gauss_RAT_Module GAUSSINT:def 16 :
Gauss_RAT_Module = ModuleStr(# G_RAT_SET,g_rat_add,(In (0,G_RAT_SET)),RSc_Mult #);

Lm8: ( Gauss_RAT_Module is scalar-distributive & Gauss_RAT_Module is vector-distributive & Gauss_RAT_Module is scalar-associative & Gauss_RAT_Module is scalar-unital & Gauss_RAT_Module is add-associative & Gauss_RAT_Module is right_zeroed & Gauss_RAT_Module is right_complementable & Gauss_RAT_Module is Abelian )

proof end;

registration

cluster Gauss_RAT_Module -> non empty right_complementable Abelian add-associative right_zeroed strict vector-distributive scalar-distributive scalar-associative scalar-unital ;

coherence
( Gauss_RAT_Module is scalar-distributive & Gauss_RAT_Module is vector-distributive & Gauss_RAT_Module is scalar-associative & Gauss_RAT_Module is scalar-unital & Gauss_RAT_Module is add-associative & Gauss_RAT_Module is right_zeroed & Gauss_RAT_Module is right_complementable & Gauss_RAT_Module is Abelian ) by Lm8;

end;

theorem Th29: :: GAUSSINT:29

for z, w being G_RAT holds g_rat_mult . (z,w) = z * w

proof end;

definition

func Gauss_RAT_Ring -> non empty strict 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)) #);

coherence
doubleLoopStr(# G_RAT_SET,g_rat_add,g_rat_mult,(In (1,G_RAT_SET)),(In (0,G_RAT_SET)) #) is non empty strict doubleLoopStr ;

end;

:: deftheorem defines Gauss_RAT_Ring GAUSSINT:def 17 :
Gauss_RAT_Ring = doubleLoopStr(# G_RAT_SET,g_rat_add,g_rat_mult,(In (1,G_RAT_SET)),(In (0,G_RAT_SET)) #);

Lm9: Gauss_RAT_Ring is Field

proof end;

registration

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

coherence
( Gauss_RAT_Ring is add-associative & Gauss_RAT_Ring is right_zeroed & Gauss_RAT_Ring is right_complementable & Gauss_RAT_Ring is Abelian & Gauss_RAT_Ring is commutative & Gauss_RAT_Ring is associative & Gauss_RAT_Ring is well-unital & Gauss_RAT_Ring is distributive & Gauss_RAT_Ring is almost_left_invertible & not Gauss_RAT_Ring is degenerated ) by Lm9;

end;

theorem :: GAUSSINT:30

ex I being Function of Gauss_INT_Field,Gauss_RAT_Ring st
( ( for z being object st z in the carrier of Gauss_INT_Field holds
ex x, y being G_INTEG ex 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 & I is onto & ( for x, y being 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 end;

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
for a being G_INTEG ex c being G_INTEG st a = a * c

proof end;

end;

:: deftheorem defines Divides GAUSSINT:def 18 :
for a, b being G_INTEG holds
( a Divides b iff ex c being G_INTEG st b = a * c );

theorem :: GAUSSINT:31

for a, b being Element of Gauss_INT_Ring
for aa, bb being G_INTEG st a = aa & b = bb & a divides b holds
aa Divides bb

proof end;

theorem :: GAUSSINT:32

for a, b being Element of Gauss_INT_Ring
for aa, bb being G_INTEG st a = aa & b = bb & aa Divides bb holds
a divides b

proof end;

definition

let z be G_RAT;
:: original: *'
redefine func z *' -> G_RAT;
coherence
z *' is G_RAT ;

end;

definition

let z be G_RAT;

func Norm z -> Rational equals :: GAUSSINT:def 19
z * (z *');

correctness
coherence
z * (z *') is Rational;

proof end;

end;

:: deftheorem defines Norm GAUSSINT:def 19 :
for z being G_RAT holds Norm z = z * (z *');

registration

let z be G_RAT;

cluster Norm z -> non negative ;

correctness
coherence
not Norm z is negative ;

proof end;

end;

registration

let z be G_INTEG;

cluster Norm z -> natural ;

coherence
Norm z is natural

proof end;

end;

theorem :: GAUSSINT:33

for x being G_RAT holds Norm (x *') = Norm x ;

theorem Th34: :: GAUSSINT:34

for x, y being G_RAT holds Norm (x * y) = (Norm x) * (Norm y)

proof end;

theorem Th35: :: GAUSSINT:35

for x being G_INTEG holds
( Norm x = 1 iff ( x = 1 or x = - 1 or x = <i> or x = - <i> ) )

proof end;

theorem Th36: :: GAUSSINT:36

for x being G_INTEG st Norm x = 0 holds
x = 0

proof end;

definition

let z be G_INTEG;

attr z is g_int_unit means :Def20: :: GAUSSINT:def 20
Norm z = 1;

end;

:: deftheorem Def20 defines g_int_unit GAUSSINT:def 20 :
for z being G_INTEG holds
( z is g_int_unit iff Norm z = 1 );

definition

let x, y be G_INTEG;

pred x is_associated_to y means :: GAUSSINT:def 21
( x Divides y & y Divides x );

symmetry
for x, y being G_INTEG st x Divides y & y Divides x holds
( y Divides x & x Divides y ) ;

end;

:: deftheorem defines is_associated_to GAUSSINT:def 21 :
for x, y being G_INTEG holds
( x is_associated_to y iff ( x Divides y & y Divides x ) );

theorem Th37: :: GAUSSINT:37

for a, b being Element of Gauss_INT_Ring
for aa, bb being G_INTEG st a = aa & b = bb & a is_associated_to b holds
aa is_associated_to bb

proof end;

theorem Th38: :: GAUSSINT:38

for a, b being Element of Gauss_INT_Ring
for aa, bb being G_INTEG st a = aa & b = bb & aa is_associated_to bb holds
a is_associated_to b

proof end;

Lm10: for x, y being G_INTEG st x is_associated_to y holds
Norm x = Norm y

proof end;

theorem Th39: :: GAUSSINT:39

for z being Element of Gauss_INT_Ring
for zz being G_INTEG st zz = z holds
( z is unital iff zz is g_int_unit )

proof end;

theorem Th40: :: GAUSSINT:40

for x, y being G_INTEG holds
( x is_associated_to y iff ex c being G_INTEG st
( c is g_int_unit & x = c * y ) )

proof end;

theorem Th41: :: GAUSSINT:41

for x being 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 end;

theorem Th42: :: GAUSSINT:42

for x, y, z being G_INTEG st x is_associated_to y & y is_associated_to z holds
x is_associated_to z

proof end;

theorem Th43: :: GAUSSINT:43

for x, y being G_INTEG st x is_associated_to y holds
x *' is_associated_to y *'

proof end;

theorem :: GAUSSINT:44

for x, y being 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 end;

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;

:: deftheorem defines g_prime GAUSSINT:def 22 :
for p being G_INTEG holds
( p is g_prime iff ( 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 ) ) ) );

Lm11: for a being Integer holds a * a is not Prime

proof end;

Lm12: for a being Integer st |.a.| <> 1 holds
not (2 * a) * a is Prime

proof end;

theorem :: GAUSSINT:45

for q being 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 end;

theorem :: GAUSSINT:46

for q being G_INTEG st Norm q is Prime holds
q is g_prime

proof end;

Lm13: ex f being Function of Gauss_INT_Ring,NAT st
for x being G_INTEG holds f . x = Norm x

proof end;

theorem Th47: :: GAUSSINT:47

for q being G_RAT holds Norm q = (|.(Re q).| ^2) + (|.(Im q).| ^2)

proof end;

theorem Th48: :: GAUSSINT:48

for q being Element of REAL ex m being Element of INT st |.(q - m).| <= 1 / 2

proof end;

Lm14: for f being Function of Gauss_INT_Ring,NAT st ( for x being 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 end;

registration

cluster Gauss_INT_Ring -> non empty strict Euclidian ;

coherence
Gauss_INT_Ring is Euclidian

proof end;

end;