:: by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama

::

:: Received May 19, 2013

:: Copyright (c) 2013-2019 Association of Mizar Users

definition
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 ) );

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
end;

registration

let z1, z2 be G_INTEG;

coherence

z1 + z2 is g_integer

z1 - z2 is g_integer

z1 * z2 is g_integer

end;
coherence

z1 + z2 is g_integer

proof end;

coherence z1 - z2 is g_integer

proof end;

coherence z1 * z2 is g_integer

proof end;

registration
end;

registration
end;

definition
end;

Lm2: <i> in G_INT_SET

;

registration
end;

definition

coherence

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

end;

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 multcomplex | [: the carrier of INT.Ring,G_INT_SET:];

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;

:: deftheorem defines Sc_Mult GAUSSINT:def 5 :

Sc_Mult = multcomplex | [: the carrier of INT.Ring,G_INT_SET:];

Sc_Mult = multcomplex | [: the carrier of INT.Ring,G_INT_SET:];

definition

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

end;

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 #);

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

:: 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 #);

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

( 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;

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;

definition

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;

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)) #);

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 ;

:: 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)) #);

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

( 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;

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;

registration
end;

definition
end;

registration

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;

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 ;

registration

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 );

end;

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;

registration

ex b_{1} being non empty AlgebraStr over INT.Ring st

( b_{1} is strict & b_{1} is Abelian & b_{1} is add-associative & b_{1} is right_zeroed & b_{1} is right_complementable & b_{1} is commutative & b_{1} is associative & b_{1} is right_unital & b_{1} is right-distributive & b_{1} is mix-associative & b_{1} is scalar-associative & b_{1} is vector-distributive & b_{1} is scalar-distributive )
end;

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

( b

proof 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 ;

definition

coherence

the_Field_of_Quotients Gauss_INT_Ring is non empty strict doubleLoopStr ;

;

end;

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

the_Field_of_Quotients Gauss_INT_Ring;

correctness the_Field_of_Quotients Gauss_INT_Ring;

coherence

the_Field_of_Quotients Gauss_INT_Ring is non empty strict doubleLoopStr ;

;

:: deftheorem defines Gauss_INT_Field GAUSSINT:def 9 :

Gauss_INT_Field = the_Field_of_Quotients Gauss_INT_Ring;

Gauss_INT_Field = the_Field_of_Quotients Gauss_INT_Ring;

registration

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;

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 );

;

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

for z being Complex holds

( z is g_rational iff ( Re z in RAT & Im z in RAT ) );

registration
end;

registration

let z1, z2 be G_RAT;

coherence

z1 + z2 is g_rational

z1 - z2 is g_rational

z1 * z2 is g_rational

end;
coherence

z1 + z2 is g_rational

proof end;

coherence z1 - z2 is g_rational

proof end;

coherence z1 * z2 is g_rational

proof end;

registration
end;

registration
end;

definition
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;

Lm6: addreal || RAT = addrat

proof end;

Lm7: multreal || RAT = multrat

proof end;

definition

coherence

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

;

end;

func F_Rat -> non empty strict doubleLoopStr equals :: GAUSSINT:def 14

doubleLoopStr(# RAT,addrat,multrat,(In (1,RAT)),(In (0,RAT)) #);

correctness doubleLoopStr(# RAT,addrat,multrat,(In (1,RAT)),(In (0,RAT)) #);

coherence

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

;

:: deftheorem defines F_Rat GAUSSINT:def 14 :

F_Rat = doubleLoopStr(# RAT,addrat,multrat,(In (1,RAT)),(In (0,RAT)) #);

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;

registration

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;

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;

registration
end;

registration

let x, y be Element of F_Rat;

let a, b be Rational;

compatibility

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

compatibility

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

end;
let a, b be Rational;

compatibility

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

compatibility

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

registration
end;

registration

let x, y be Element of F_Rat;

let a, b be Rational;

compatibility

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

end;
let a, b be Rational;

compatibility

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

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

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

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

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

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

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 "

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

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;

registration
end;

definition

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

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

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;

:: deftheorem defines RSc_Mult GAUSSINT:def 15 :

RSc_Mult = multcomplex | [: the carrier of F_Rat,G_RAT_SET:];

RSc_Mult = multcomplex | [: the carrier of F_Rat,G_RAT_SET:];

definition

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

end;

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 #);

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

:: 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 #);

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

( 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;

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;

definition

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;

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)) #);

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 ;

:: 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)) #);

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

( 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;

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;

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 )

( ( 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
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 );

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

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

for aa, bb being G_INTEG st a = aa & b = bb & aa Divides bb holds

a divides b

proof end;

registration
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 );

for z being G_INTEG holds

( z is g_int_unit iff Norm z = 1 );

definition

let x, y be G_INTEG;

symmetry

for x, y being G_INTEG st x Divides y & y Divides x holds

( y Divides x & x Divides y ) ;

end;
symmetry

for x, y being G_INTEG st x Divides y & y Divides x holds

( y Divides x & x Divides y ) ;

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

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

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

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 )

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

( 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

not x *' is_associated_to x

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 )

( not x Divides y & not y Divides x )

proof end;

definition

let p be G_INTEG;

end;
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 ) ) );

( 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 ) ) );

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

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 )

( Re q <> 0 & Im q <> 0 & Re q <> Im q & - (Re q) <> Im q )

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;

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;