:: Gaussian Integers
:: by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama
::
:: Copyright (c) 2013-2017 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
coherence
for b1 being Integer holds b1 is g_integer
proof end;
end;

definition 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
coherence by ;
end;

registration
let z be G_INTEG;
coherence
- z is g_integer
proof end;
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:
;

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
correctness
coherence ;
proof end;
end;

:: deftheorem defines g_int_add GAUSSINT:def 3 :

definition
correctness
coherence ;
proof end;
end;

:: deftheorem defines g_int_mult GAUSSINT:def 4 :

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 :

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

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

Lm3:
proof end;

registration
coherence 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
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:
proof end;

registration
coherence by Lm4;
end;

registration
coherence
proof end;
end;

registration
coherence
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 b1 being AlgebraStr over INT.Ring holds b1 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
correctness
coherence
;
proof end;
end;

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

definition end;

theorem :: GAUSSINT:9

registration
coherence
proof end;
end;

registration
coherence
proof end;
end;

registration
correctness
coherence ;
;
end;

definition
correctness
coherence ;
;
end;

:: deftheorem defines Gauss_INT_Field GAUSSINT:def 9 :

registration
correctness
coherence ;
;
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
coherence
for b1 being Rational holds b1 is g_rational
proof end;
end;

definition end;

registration
let z be G_RAT;
coherence
Re z is rational
proof end;
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;
coherence
- z is g_rational
proof end;
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
coherence
for b1 being G_INTEG holds b1 is g_rational
by ;
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
correctness
coherence ;
proof end;
end;

:: deftheorem defines g_rat_add GAUSSINT:def 12 :

definition
correctness
coherence ;
proof end;
end;

:: deftheorem defines g_rat_mult GAUSSINT:def 13 :

Lm6:
proof end;

Lm7:
proof end;

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

definition
func F_Rat -> non empty strict doubleLoopStr equals :: GAUSSINT:def 14
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 ;

registration
correctness
coherence ;
by ;
end;

registration
coherence
proof end;
end;

registration
cluster -> rational for Element of the carrier of F_Rat;
coherence
for b1 being Element of F_Rat holds b1 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
proof end;

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
coherence
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 :

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

Lm8:
proof end;

registration
coherence 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
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:
proof end;

registration
coherence 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_RAT_Ring & I . = 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;
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
coherence
proof end;
end;