gaussint.miz

begin

 theorem :: GAUSSINT:1



 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;

 :: GAUSSINT:def1

 attr z is g_integer means

 : Def1: ( Re z) in INT & ( Im z) in INT ;

 end



 Lm1: for z be 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, COMPLEX1: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 -> 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

 :: GAUSSINT:def2

 func G_INT_SET -> Subset of COMPLEX equals the set of all z where z be G_INTEG;

 correctness

 proof

 now

 let x be object;

 assume x in the set of all z where z be 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: 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 :: GAUSSINT:2



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



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

 definition

 :: GAUSSINT:def3

 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

 :: GAUSSINT:def4

 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

 :: GAUSSINT:def5

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



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



 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

 :: GAUSSINT:def6

 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 be 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 be 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 be 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 be 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 be 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 be 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 holds for v be 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 be 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, VECTSP_1:def 15, VECTSP_1:def 16, VECTSP_1:def 17, RLVECT_1:def 2, RLVECT_1:def 3, RLVECT_1: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 :: GAUSSINT:6



 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

 :: GAUSSINT:def7

 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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, RLVECT_1:def 3, RLVECT_1: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 be 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 :: GAUSSINT:7

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

 theorem :: GAUSSINT:8

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

 begin

 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

 ::$Canceled

 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 be 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 be 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 be 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 be 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 be 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 be 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 holds for v be 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 be Vector of ZS holds 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 be 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 be 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 be 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 be 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 be 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, RLVECT_1:def 3, RLVECT_1: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 :: 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

 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 + ( * m));



 A1: for x,y be object st x in INT & y in INT holds ex z be 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 + ( * m));

 thus thesis;

 end;

 consider F be Function of [: INT , INT :], G_INT_SET such that

 A2: for x,y be 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 + ( * 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 + ( * 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 + ( * 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 be 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 + ( * m1)) by A4;



 A13: (F . x2) = (F . (n2,m2)) by A11

 .= (n2 + ( * m2)) by A4;



 A14: n1 = ( Re (n2 + ( * m2))) by A9, A12, A13, COMPLEX1: 12

 .= n2 by COMPLEX1: 12;

 m1 = ( Im (n2 + ( * 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

 definition

 :: GAUSSINT:def9

 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;

 :: GAUSSINT:def10

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

 :: GAUSSINT:def11

 func G_RAT_SET -> Subset of COMPLEX equals the set of all z where z be G_RAT;

 correctness

 proof

 now

 let x be object;

 assume x in the set of all z where z be 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 :: GAUSSINT:10



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



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

 theorem :: GAUSSINT:12



 Th12: for p be G_RAT holds 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 be 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 be 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, XCMPLX_1: 95;

 end;

 definition

 :: GAUSSINT:def12

 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

 :: GAUSSINT:def13

 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



 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

 :: GAUSSINT:def14

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

 correctness ;

 end

 theorem :: GAUSSINT:13



 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 be 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 be 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 :: GAUSSINT:14

 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 ;

 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 a + b with x + y when x = a, y = b;

 compatibility by BINOP_2:def 15;

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

 compatibility by BINOP_2:def 17;

 end

 registration

 let x be Element of F_Rat , y be Rational;

 identify - y with - x 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 a - b with x - y when x = a, y = b;

 compatibility ;

 end

 theorem :: GAUSSINT:15



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



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

 theorem :: GAUSSINT:17



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



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



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

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



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

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



 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 be Nat holds P[n] from NAT_1:sch 2( A1, A2);

 hence thesis;

 end;

 theorem :: GAUSSINT:24



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



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

 for K1 be 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 be 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 be Field holds K1 is strict Subfield of K implies K1 = K;

 hence thesis by EC_PF_1:def 2;

 end;

 end

 begin

 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

 :: GAUSSINT:def15

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



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



 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

 :: GAUSSINT:def16

 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 be 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 be 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 be 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 be 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 be 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 be 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 holds for v be 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 be 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, RLVECT_1:def 3, RLVECT_1: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 :: GAUSSINT:29



 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

 :: GAUSSINT:def17

 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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, RLVECT_1:def 3, RLVECT_1: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 :: 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 holds ex x,y be G_INTEG, u be 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 be 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 holds 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 be 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 )))

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

 hence thesis by A4, A10, A13, A14, A30;

 end;

 begin

 definition

 let a,b be G_INTEG;

 :: GAUSSINT:def18

 pred a Divides b means ex c be G_INTEG st b = (a * c);

 reflexivity

 proof

 let a be G_INTEG;

 take 1;

 thus a = (a * 1);

 end;

 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

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

 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;

 :: original: *'

 redefine

 func z *' -> G_RAT ;

 coherence ;

 end

 definition

 let z be G_RAT;

 :: GAUSSINT:def19

 func Norm (z) -> Rational equals (z * (z *' ));

 correctness

 proof

 set Rez = ( Re z), Imz = ( Im z);

 (( Re (Rez + (( - Imz) * ))) = Rez) & (( Im (Rez + (( - Imz) * ))) = ( - 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 *' ))) * )) 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) * ))) = Rez) & (( Im (Rez + (( - Imz) * ))) = ( - 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 *' ))) * )) 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)) * ))) = ( Re z) & ( Im (( Re z) + (( - ( Im z)) * ))) = ( - ( 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 *' ))) * )) 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 :: GAUSSINT:33

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

 theorem :: GAUSSINT:34



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



 Th35: for x be G_INTEG holds ( Norm x) = 1 iff x = 1 or x = ( - 1) or x = or x = ( - )

 proof

 let x be G_INTEG;

 hereby

 assume

 A1: ( Norm x) = 1;



 A2: x = (( Re x) + (( Im x) * )) by COMPLEX1: 13;



 A3: ( Norm x) = ((( Re x) + (( Im x) * )) * (( Re x) - (( Im x) * ))) 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 = or x = ( - )) by A2;

 end;

 assume

 A4: x = 1 or x = ( - 1) or x = or x = ( - );

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

 hence ( Norm x) = 1 by COMPLEX1: 31;

 end;

 suppose x = ( - );

 hence ( Norm x) = 1 by COMPLEX1: 31;

 end;

 end;

 theorem :: GAUSSINT:36



 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) * )) * (( Re x) - (( Im x) * ))) 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;

 :: GAUSSINT:def20

 attr z is g_int_unit means

 : Def20: ( Norm z) = 1;

 end

 definition

 let x,y be G_INTEG;

 :: GAUSSINT:def21

 pred x is_associated_to y means x Divides y & y Divides x;

 symmetry ;

 end

 theorem :: GAUSSINT:37



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



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



 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, GCD_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 be 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 = ;

 reconsider w = ( - ) as Element of Gauss_INT_Ring by Th3;

 take w;



 thus ( 1. Gauss_INT_Ring ) = ( * ( - ))

 .= (z * w) by A8, Th6;

 end;

 suppose

 A9: z = ( - );

 reconsider w = as Element of Gauss_INT_Ring by Lm2;

 take w;



 thus ( 1. Gauss_INT_Ring ) = (( - ) * )

 .= (z * w) by A9, Th6;

 end;

 end;

 hence z is unital by GCD_1:def 1, GCD_1:def 2;

 end;

 theorem :: GAUSSINT:40



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



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

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



 then ( Im x) = ( Im (( * ( Re x)) + ((( - ( Im x)) * ) * ))) by A2

 .= ( Re x) by COMPLEX1: 12;

 hence contradiction by A1;

 end;

 suppose d = ( - );



 then ( Im x) = ( Im (( * ( - ( Re x))) + (( Im x) * ( - 1r )))) by A2

 .= ( - ( Re x)) by COMPLEX1: 12;

 hence contradiction by A1;

 end;

 end;

 hence contradiction;

 end;

 theorem :: GAUSSINT:42



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



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

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

 :: GAUSSINT:def22

 attr p is g_prime means ( Norm p) > 1 & for z be 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 :: 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)

 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) * )) * (( Re q) - (( Im q) * ))) 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 :: GAUSSINT:46

 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 be 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 be 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 be 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 be Element of the carrier of Gauss_INT_Ring holds ex y be Element of NAT st P[x, y]

 proof

 let x be 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 be Function of Gauss_INT_Ring , NAT such that

 A2: for x be 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 :: GAUSSINT:47



 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) * )) * (( Re q) - (( Im q) * ))) by COMPLEX1: 13

 .= ((( Re q) ^2 ) + (( Im q) ^2 ))

 .= (( |.( Re q).| ^2 ) + ( |.( Im q).| ^2 )) by A1, COMPLEX1: 75;

 end;

 theorem :: GAUSSINT:48



 Th48: for q be Element of REAL holds 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 be Function of Gauss_INT_Ring , NAT st for x be G_INTEG holds (f . x) = ( Norm x) holds for a,b be Element of Gauss_INT_Ring st b <> ( 0. Gauss_INT_Ring ) holds ex q,r be 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 be 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 * ));

 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 be 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 be Element of Gauss_INT_Ring st b <> ( 0. Gauss_INT_Ring ) holds ex q,r be 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