:: Gaussian Integers
:: by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, NEWTON, ORDINAL1, SQUARE_1, ARYTM_3, CARD_1,
XXREAL_0, XCMPLX_0, FUNCT_1, FUNCT_2, XBOOLE_0, RELAT_1, REAL_1, INT_1,
ARYTM_1, COMPLEX1, GAUSSINT, ZFMISC_1, BINOP_1, BINOP_2, TARSKI,
ZMODUL01, STRUCT_0, ALGSTR_0, RLVECT_1, GCD_1, VECTMETR, INT_2, NAT_1,
SUPINF_2, MESFUNC1, FINSET_1, CARD_3, FUNCSDOM, VECTSP_1, VECTSP_2,
RAT_1, EC_PF_1, LATTICES, GROUP_1, QUOFIELD, REALSET1, MCART_1, FUNCT_7,
INT_3;
notations TARSKI, XBOOLE_0, ZFMISC_1, SUBSET_1, RELAT_1, FUNCT_1, ORDINAL1,
PARTFUN1, FUNCT_2, BINOP_1, DOMAIN_1, REALSET1, FINSET_1, CARD_1, CARD_3,
NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, INT_1, RAT_1, COMPLEX1,
INT_2, INT_3, BINOP_2, NEWTON, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1,
VECTSP_1, FUNCSDOM, VECTSP_2, GCD_1, QUOFIELD, EC_PF_1, ZMODUL01;
constructors REAL_1, SQUARE_1, MEMBERED, RELSET_1, NAT_1, BINOP_2, ZMODUL01,
FUNCSDOM, WELLORD2, CARD_3, QUOFIELD, REALSET1, EC_PF_1, GCD_1, RAT_1;
registrations XBOOLE_0, RELSET_1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
VECTSP_1, CARD_1, CARD_3, MEMBERED, SUBSET_1, INT_1, STRUCT_0, ALGSTR_0,
REALSET1, EC_PF_1, ZMODUL01, XTUPLE_0, QUOFIELD, SQUARE_1, RAT_1, NAT_1,
INT_3, ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions STRUCT_0, ALGSTR_0, VECTSP_1, GROUP_1;
equalities SQUARE_1, XCMPLX_0, COMPLEX1, BINOP_1, STRUCT_0, ALGSTR_0,
VECTSP_1, ZMODUL01, QUOFIELD, REALSET1;
expansions STRUCT_0, ALGSTR_0, VECTSP_1, ZMODUL01;
theorems FUNCT_2, XBOOLE_0, TARSKI, NUMBERS, INT_1, XCMPLX_0, XCMPLX_1,
XREAL_1, STRUCT_0, ALGSTR_0, XXREAL_0, COMPLEX1, ORDINAL1, RLVECT_1,
NAT_1, BINOP_1, BINOP_2, ZMODUL01, RELAT_1, ZFMISC_1, FUNCT_1, SQUARE_1,
ABSVALUE, VECTSP_1, GROUP_1, CARD_1, CARD_2, CARD_3, CARD_4, VECTSP_2,
RAT_1, EC_PF_1, QUOFIELD, WELLORD2, INT_2, INT_3, GCD_1, XREAL_0,
SUBSET_1;
schemes NAT_1, BINOP_1, FUNCT_2;
begin :: 1. Gaussian integer ring
theorem LMThNorm3:
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 AS: x+y = 1;
x <= 1
proof
assume not x <= 1; then
1 + 0 < x + y by XREAL_1:8;
hence contradiction by AS;
end;
then x=0 or x = 1 by NAT_1:25;
hence (x = 1 & y = 0) or (x = 0 & y = 1) by AS;
end;
definition
let z be Complex;
attr z is g_integer means :defg:
Re z in INT & Im z in INT;
end;
DEFG: for z being Complex st Re z is integer & Im z is integer
holds z is g_integer by INT_1:def 2;
registration
cluster -> g_integer for Integer;
coherence
proof
let c be Integer;
c in REAL by XREAL_0:def 1;
then Re c = c & Im c = 0 by COMPLEX1:def 1,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 defg;
hence thesis;
end;
cluster Im z -> integer;
coherence
proof
Im z in INT by defg;
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
func G_INT_SET -> Subset of COMPLEX equals
the set of all z where z is G_INTEG;
correctness
proof
now let x be element;
assume x in the set of all z where z is 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;
LM7i: ** 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 LM3:
for x be set st x in G_INT_SET holds x is G_INTEG
proof
let x be set;
assume x in G_INT_SET;
then ex z be G_INTEG st x=z;
hence x is g_integer Complex;
end;
theorem LM4:
for x be set st x is G_INTEG holds x in G_INT_SET;
definition
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 P1: dom ad = [:G_INT_SET,G_INT_SET:] by RELAT_1:62;
for z be element st z in [:G_INT_SET,G_INT_SET:] holds ad. z in G_INT_SET
proof
let z be element such that
P2: z in [:G_INT_SET,G_INT_SET:];
consider x, y be element such that
P3: x in G_INT_SET & y in G_INT_SET & z = [x,y]
by P2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as G_INTEG by LM3,P3;
ad.z = addcomplex.(x1,y1) by P2,P3,FUNCT_1:49
.= x1+y1 by BINOP_2:def 3;
hence ad.z in G_INT_SET;
end;
hence thesis by P1,FUNCT_2:3;
end;
end;
definition
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 P2: dom mult = [:G_INT_SET,G_INT_SET:] by RELAT_1:62;
for z be element st z in [:G_INT_SET,G_INT_SET:] holds mult.z in G_INT_SET
proof
let z be element such that
P3: z in [:G_INT_SET,G_INT_SET:];
consider x,y be element such that
P4: x in G_INT_SET & y in G_INT_SET & z = [x,y]
by P3,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as G_INTEG by LM3,P4;
mult.z = multcomplex.(x1,y1) by P3,P4,FUNCT_1:49
.= x1*y1 by BINOP_2:def 5;
hence mult.z in G_INT_SET;
end;
hence thesis by P2,FUNCT_2:3;
end;
end;
definition
func Sc_Mult -> Function of [:INT,G_INT_SET :], G_INT_SET equals
multcomplex | [:INT,G_INT_SET:];
correctness
proof
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 P2: dom scmult = [:INT,G_INT_SET:] by RELAT_1:62;
for z be element st z in [:INT,G_INT_SET:] holds scmult.z in G_INT_SET
proof
let z be element such that
P3: z in [:INT,G_INT_SET:];
consider x, y be element such that
P4: (x in INT) & (y in G_INT_SET) & (z = [x,y]) by P3,ZFMISC_1:def 2;
reconsider x1 = x as Element of INT by P4;
reconsider y1 = y as G_INTEG by LM3,P4;
scmult.z = multcomplex.(x1,y1) by P3,P4,FUNCT_1:49
.= x1*y1 by BINOP_2:def 5;
hence scmult.z in G_INT_SET;
end;
hence thesis by P2,FUNCT_2:3;
end;
end;
theorem LM5:
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 LM6:
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;
P2: i in INT & z in G_INT_SET by INT_1:def 2;
thus Sc_Mult.(i,z) = multcomplex.(i,z) by P2,FUNCT_1:49,ZFMISC_1:87
.= i*z by BINOP_2:def 5;
end;
definition
func Gauss_INT_Module -> strict non empty Z_ModuleStruct equals
Z_ModuleStruct(# G_INT_SET, In(0,G_INT_SET), g_int_add, Sc_Mult #);
correctness;
end;
Th1:
Gauss_INT_Module is Z_Module
proof
reconsider
ZS = Z_ModuleStruct(# G_INT_SET, In(0,G_INT_SET), g_int_add,
Sc_Mult #) as non empty Z_ModuleStruct;
set AG = G_INT_SET;
set ML = the Mult of ZS;
set AD = the addF of ZS;
set CA = the carrier of ZS;
set Z0 = the ZeroF of ZS;
set MLI = Sc_Mult;
P1:for v, w being 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 LM3;
thus v + w = w1 + v1 by LM5
.= w + v by LM5;
end;
P2:for u, v, w being 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 LM3;
X1: u + v = u1+v1 by LM5;
X2: v + w = v1+w1 by LM5;
thus (u + v) + w = u1+v1+w1 by LM5,X1
.= u1+(v1+w1)
.= u+(v+w) by LM5,X2;
end;
P3: for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
reconsider v1 = v as G_INTEG by LM3;
thus v + 0.ZS = v1 + 0 by LM5
.= v;
end;
P4: for v being VECTOR of ZS holds v is right_complementable
proof
let v be VECTOR of ZS;
take (-1) * v;
reconsider v1 = v as G_INTEG by LM3;
X3: (-1) * v = (-1) * v1 by LM6
.= (-v1);
thus v + ((-1) * v) = v1 + (-v1) by X3, LM5
.= 0.ZS;
end;
P5: for a, b be Integer, v being VECTOR of ZS
holds (a + b) * v = a * v + b * v
proof
let a, b be Integer;
let v be VECTOR of ZS;
reconsider v1 = v as G_INTEG by LM3;
X2: (a*v1 = a*v) & (b*v1 = b*v) by LM6;
thus (a + b) * v = (a + b) * v1 by LM6
.= a*v1 + b*v1
.= a*v + b*v by X2, LM5;
end;
P6: for a be Integer, v, w being VECTOR of ZS
holds a * (v + w) = a * v + a * w
proof
let a be Integer;
let v, w be VECTOR of ZS;
reconsider v1 = v, w1 = w as G_INTEG by LM3;
Y2: (v + w) = (v1 + w1) by LM5;
Z1: (a*v1 = a*v) & (a*w1 = a*w) by LM6;
thus a * (v + w) = a * (v1 + w1) by Y2, LM6
.= a*v1 + a*w1
.= a*v + a*w by Z1, LM5;
end;
P7: for a, b be Integer for v being VECTOR of
ZS holds (a * b) * v = a * (b * v)
proof
let a, b be Integer;
let v be VECTOR of ZS;
reconsider v1 = v as G_INTEG by LM3;
Y2: b * v1 = b * v by LM6;
thus (a * b) * v = (a * b) * v1 by LM6
.= a * (b * v1)
.= a * (b * v) by Y2, LM6;
end;
for v being VECTOR of ZS holds 1 * v = v
proof
let v be VECTOR of ZS;
reconsider i = 1 as Element of INT by INT_1:def 2;
reconsider v1 = v as G_INTEG by LM3;
thus 1 * v = i*v1 by LM6
.= v;
end;
hence thesis by P1,P2,P3,P4,P5,P6,P7,ZMODUL01:def 2,def 3,def 4,def 5,
RLVECT_1:def 2,def 3,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 Th1;
end;
theorem LM8:
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
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) #);
correctness;
end;
Th2:
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;
P1:for v, w being 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 LM3;
thus v + w = w1 + v1 by LM5
.= w + v by LM5;
end;
P2: for u, v, w being 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 LM3;
X1: u + v = u1+v1 by LM5;
X2: v + w = v1+w1 by LM5;
thus (u + v) + w = u1+v1+w1 by LM5,X1
.= u1+(v1+w1)
.= u+(v+w) by LM5,X2;
end;
P3: for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
reconsider v1 = v as G_INTEG by LM3;
thus v + 0.ZS = v1 + 0 by LM5
.= v;
end;
P4: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS;
reconsider v1 = v as G_INTEG by LM3;
reconsider w1 = (-1) as Element of ZS by LM4;
Y2: w1 * v = (-1) * v1 by LM8;
take (w1*v);
thus v + (w1*v) = v1 + ((-1) * v1) by Y2,LM5
.= 0.ZS;
end;
P5: for a, b, v being 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 LM3;
reconsider ab = a+b as G_INTEG by LM3;
Y2: a1*v1 = a*v & (b1*v1 = b*v) by LM8;
thus (a + b) * v = ab * v1 by LM8
.= (a1 + b1) * v1 by LM5
.= a1*v1 + b1*v1
.= a*v + b*v by Y2,LM5;
end;
P6: for a, v, w being 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 LM3;
reconsider vw = (v+w) as G_INTEG by LM3;
Y2: (a1*v1 = a*v) & (a1*w1 = a*w) by LM8;
thus a * (v + w) = a1 * vw by LM8
.= a1 * (v1 + w1) by LM5
.= a1*v1 + a1*w1
.= a*v + a*w by Y2,LM5;
thus (v + w) * a = v*a + w*a by P5;
end;
P7: for a, b, v being 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 LM3;
reconsider ab = (a*b), bv = (b*v) as G_INTEG by LM3;
thus (a * b) * v = ab * v1 by LM8
.= (a1 * b1) * v1 by LM8
.= a1 * (b1 * v1)
.= a1 * bv by LM8
.= a * (b * v) by LM8;
end;
for v being 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 LM3;
thus v * 1.ZS = v1 * 1 by LM8
.= v;
thus 1.ZS * v = 1 * v1 by LM8
.= v;
end;
hence thesis
by P1,P2,P3,P4,P6,P7,VECTSP_1:def 6,VECTSP_1:def 7,
GROUP_1:def 3, RLVECT_1:def 2,def 3,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 Th2;
end;
registration
cluster Gauss_INT_Ring -> domRing-like;
coherence
proof
set X = Gauss_INT_Ring;
for x, y being 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 AS: x*y = 0.X;
xx is G_INTEG & yy is G_INTEG by LM3;
then xx*yy = 0 by AS,LM8;
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 LM3;
thus v * w = v1 * w1 by LM8
.= w * v by LM8;
end;
end;
theorem
for x be Element of Gauss_INT_Ring holds x is G_INTEG by LM3;
theorem
for x be G_INTEG holds x is Element of Gauss_INT_Ring by LM4;
begin :: 2. Z-Algebra
definition
struct(doubleLoopStr,Z_ModuleStruct) Z_AlgebraStr
(# carrier -> set, multF,addF -> (BinOp of the carrier),
Mult -> (Function of [:INT,the carrier:],the carrier),
OneF,ZeroF -> Element of the carrier #);
correctness;
end;
registration
cluster non empty for Z_AlgebraStr;
existence
proof
set X =the non empty set, m = the BinOp of X,
M = the Function of [:INT,X:],X, u = the Element of X;
take Z_AlgebraStr(#X,m,m,M,u,u#);
thus the carrier of Z_AlgebraStr(#X,m,m,M,u,u#) is non empty;
end;
end;
definition
let IT be non empty Z_AlgebraStr;
attr IT is vector-associative means
for x,y being Element of IT for a be Integer
holds a*(x*y) = (a*x)*y;
end;
registration
cluster Z_AlgebraStr(# G_INT_SET, g_int_mult, g_int_add,Sc_Mult,
In(1,G_INT_SET), In(0,G_INT_SET) #) -> non empty;
correctness;
end;
registration
cluster Z_AlgebraStr(# G_INT_SET, g_int_mult, g_int_add, Sc_Mult,
In(1,G_INT_SET), In(0,G_INT_SET) #) ->
strict Abelian add-associative right_zeroed
right_complementable commutative associative right_unital
right-distributive vector-associative scalar-associative
vector-distributive scalar-distributive;
correctness
proof
set ZS = Z_AlgebraStr(# G_INT_SET, g_int_mult, g_int_add, Sc_Mult,
In(1,G_INT_SET), In(0,G_INT_SET) #);
P1: for v, w being 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 LM3;
thus v + w = v1 + w1 by LM5
.= w + v by LM5;
end;
P2: for u, v, w being 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 LM3;
X1: u + v = u1+v1 by LM5;
X2: v + w = v1+w1 by LM5;
thus (u + v) + w
= u1+v1+w1 by LM5,X1
.= u1+(v1+w1)
.= u+(v+w) by LM5,X2;
end;
P3: for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
reconsider v1 = v as G_INTEG by LM3;
thus v + 0.ZS = v1 + 0 by LM5
.= v;
end;
P4: for v being VECTOR of ZS holds v is right_complementable
proof
let v be VECTOR of ZS;
take (-1) * v;
reconsider v1 = v as G_INTEG by LM3;
X3: (-1) * v = (-1) * v1 by LM6
.= (-v1);
thus v + ((-1) * v) = v1 + (-v1) by X3, LM5
.= 0.ZS;
end;
P5: for a, b be Integer, v being VECTOR of ZS
holds (a + b) * v = a * v + b * v
proof
let a, b be Integer;
let v be VECTOR of ZS;
reconsider v1 = v as G_INTEG by LM3;
X2: (a*v1 = a*v) & (b*v1 = b*v) by LM6;
thus (a + b) * v
= (a + b) * v1 by LM6
.= a*v1 + b*v1
.= a*v + b*v by X2, LM5;
end;
P6: for a be Integer, v, w being VECTOR of ZS
holds a * (v + w) = a * v + a * w
proof
let a be Integer;
let v, w be VECTOR of ZS;
reconsider v1 = v, w1 = w as G_INTEG by LM3;
Y2: (v + w) = (v1 + w1) by LM5;
Z1: (a*v1 = a*v) & (a*w1 = a*w) by LM6;
thus a * (v + w) = a * (v1 + w1) by Y2,LM6
.= a*v1 + a*w1
.= a*v + a*w by Z1,LM5;
end;
P7: for a, b be Integer for v being VECTOR of ZS
holds (a * b) * v = a * (b * v)
proof
let a, b be Integer;
let v be VECTOR of ZS;
reconsider v1 = v as G_INTEG by LM3;
Y2: b * v1 = b * v by LM6;
thus (a * b) * v = (a * b) * v1 by LM6
.= a * (b * v1)
.= a * (b * v) by Y2, LM6;
end;
Q70: for v, w being VECTOR of ZS for a be Integer
holds a * (v * w) = (a * v) * w
proof
let v, w be VECTOR of ZS;
let a be Integer;
reconsider v1 = v, w1 = w as G_INTEG by LM3;
Z2: a * v = a * v1 by LM6;
reconsider vw = v*w as G_INTEG by LM3;
thus a *(v*w) = a*vw by LM6
.= a*(v1*w1) by LM8
.= a*v1*w1
.= (a*v)*w by LM8,Z2;
end;
Q1: for v, w being 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 LM3;
thus v * w = v1 * w1 by LM8
.= w * v by LM8;
end;
Q5: for a, b, v being 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 LM3;
reconsider ab = a+b as G_INTEG by LM3;
Y2: a1*v1 = a*v & b1*v1 = b*v by LM8;
thus (a + b) * v = ab * v1 by LM8
.= (a1 + b1) * v1 by LM5
.= a1*v1 + b1*v1
.= a*v + b*v by Y2, LM5;
end;
Q6: for a, v, w being 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 LM3;
reconsider vw = (v+w) as G_INTEG by LM3;
Y2: (a1*v1 = a*v) & (a1*w1 = a*w) by LM8;
thus a * (v + w) = a1 * vw by LM8
.= a1 * (v1 + w1) by LM5
.= a1*v1 + a1*w1
.= a*v + a*w by Y2, LM5;
thus (v + w) * a = v*a + w*a by Q5;
end;
Q7: for a, b, v being 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 LM3;
reconsider ab = (a*b), bv = (b*v) as G_INTEG by LM3;
thus (a * b) * v = ab * v1 by LM8
.= (a1 * b1) * v1 by LM8
.= a1 * (b1 * v1)
.= a1 * bv by LM8
.= a * (b * v) by LM8;
end;
for v being 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 LM3;
thus v * 1.ZS = v1 * 1 by LM8
.= v;
thus 1.ZS * v = 1 * v1 by LM8
.= v;
end;
hence thesis by P1,P2,P3,P4,P5,P6,P7,
GROUP_1:def 3, RLVECT_1:def 2,def 3,def 4,
Q1,Q7,Q6,Q70,GROUP_1:def 12;
end;
end;
registration
cluster strict Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive vector-associative
scalar-associative vector-distributive scalar-distributive
for non empty Z_AlgebraStr;
existence
proof
take Z_AlgebraStr(# G_INT_SET, g_int_mult, g_int_add, Sc_Mult,
In(1,G_INT_SET), In(0,G_INT_SET) #);
thus thesis;
end;
end;
definition
mode Z_Algebra is Abelian add-associative right_zeroed right_complementable
commutative associative right_unital right-distributive
vector-associative scalar-associative vector-distributive
scalar-distributive non empty Z_AlgebraStr;
end;
theorem
Z_AlgebraStr(# G_INT_SET, g_int_mult, g_int_add, Sc_Mult,
In(1,G_INT_SET), In(0,G_INT_SET) #) is
right_complementable associative commutative right-distributive
right_unital Abelian add-associative right_zeroed vector-distributive
scalar-distributive scalar-associative strict vector-associative
non empty Z_AlgebraStr;
::begin :: 3. Denumerable set
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[element,element,element] means
ex n,m be Integer st $1 = n & $2 = m & $3 = n+ ** *m;
P0A: for x, y being element st x in INT & y in INT
ex z being element st z in G_INT_SET & P[x,y,z]
proof
let x, y be element;
assume x in INT & y in INT;
then reconsider n = x, m = y as Integer;
take n+ ** *m;
thus thesis;
end;
consider F being Function of [:INT,INT:], G_INT_SET such that
P0B: for x, y being element st x in INT & y in INT holds
P[x,y,F.(x,y)] from BINOP_1:sch 1(P0A);
P2B: dom F = [:INT,INT:] by FUNCT_2:def 1;
P1: 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 P0B;
hence thesis;
end;
now let x be element;
assume x in G_INT_SET;
then reconsider x1 = x as G_INTEG by LM3;
Z1: Re x1 in INT & Im x1 in INT by defg;
reconsider n = Re x1, m = Im x1 as Integer;
Z2: F.(n,m) = n+ ** *m by P1
.= x1 by COMPLEX1:13;
[n,m] in [:INT,INT:] by Z1,ZFMISC_1:87;
hence x in rng F by P2B,Z2,FUNCT_1:3;
end;
then D1: G_INT_SET c= rng F by TARSKI:def 3;
F in Funcs([:INT,INT:],G_INT_SET) by FUNCT_2:8;
then ex f being Function st F = f & dom f = [:INT,INT:]
& rng f c= G_INT_SET by FUNCT_2:def 2;
then P2A: rng F = G_INT_SET by D1,XBOOLE_0:def 10;
for x1, x2 be element
st x1 in dom F & x2 in dom F & F.x1 = F.x2 holds x1 = x2
proof
let x1, x2 be element;
assume AS: x1 in dom F & x2 in dom F & F.x1 = F.x2;
then consider n1, m1 be element such that
X2: n1 in INT & m1 in INT & x1 = [n1,m1] by P2B,ZFMISC_1:def 2;
consider n2, m2 be element such that
X3: n2 in INT & m2 in INT & x2 = [n2,m2] by AS,P2B,ZFMISC_1:def 2;
reconsider n1, m1, n2, m2 as Integer by X2,X3;
X4: F.x1 =F.(n1,m1) by X2
.=n1+ ** *m1 by P1;
X5: F.x2 = F.(n2,m2) by X3
.= n2+ ** *m2 by P1;
X6: n1 = Re(n2+ ** *m2) by AS,X4,X5,COMPLEX1:12
.= n2 by COMPLEX1:12;
m1 = Im(n2+ ** *m2) by AS,X4,X5,COMPLEX1:12
.= m2 by COMPLEX1:12;
hence thesis by X2,X3,X6;
end;
then [:INT,INT:],G_INT_SET are_equipotent
by P2A,P2B,FUNCT_1:def 4,WELLORD2:def 4;
then P5: 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,P5;
end;
end;
registration
cluster Gauss_INT_Ring -> non degenerated;
correctness;
end;
begin :: 4. Quotient field of Gaussian integer ring
definition
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;
attr z is g_rational means
:rdefg:
Re z in RAT & Im z in RAT;
end;
registration
cluster -> g_rational for Rational;
coherence
proof
let c be Rational;
c in REAL by XREAL_0:def 1;
then Re c = c & Im c = 0 by COMPLEX1:def 1,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 rdefg;
hence thesis;
end;
cluster Im z -> rational;
coherence
proof
Im z in RAT by rdefg;
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
func G_RAT_SET -> Subset of COMPLEX equals
the set of all z where z is G_RAT;
correctness
proof
now let x be element;
assume x in the set of all z where z is 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
proof
let x be G_INTEG;
Re x in INT & Im x in INT by defg;
hence thesis by NUMBERS:14;
end;
end;
theorem RLM3:
for x be set st x in G_RAT_SET holds x is G_RAT
proof
let x be set;
assume x in G_RAT_SET;
then ex z be G_RAT st x=z;
hence x is g_rational Complex;
end;
theorem RLM4:
for x be set st x is G_RAT holds x in G_RAT_SET;
theorem Rth3LM2:
for p be G_RAT 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
P1: n1 <> 0 & Rp = m1/n1 by RAT_1:2;
consider m2, n2 be Integer such that
P2: n2 <> 0 & Ip = m2/n2 by RAT_1:2;
set z = n1*n2;
z in REAL by XREAL_0:def 1;
then Re z = z & Im z = 0 by COMPLEX1:def 1,COMPLEX1:def 2;
then X1: (Re(z * p) = z * Rp - 0 * Ip) & (Im(z * p) = z * Ip + Rp * 0)
by COMPLEX1:9;
P4: Re(z*p) = n1/n1*m1*n2 by P1,X1
.= 1*m1*n2 by XCMPLX_1:60,P1
.= m1*n2;
P5: Im(z*p) = n2/n2*m2*n1 by P2,X1
.= 1*m2*n1 by XCMPLX_1:60,P2
.= m2*n1;
reconsider x = z*p as G_INTEG by P4,P5,DEFG;
take x,z;
x/z = z/z * p
.= 1*p by XCMPLX_1:60,P1,P2
.= p;
hence thesis by P1,P2;
end;
Rth3LM3:
for x1, y1, x2, y2 be G_INTEG, 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
let x1, y1, x2, y2 be G_INTEG,
u1, u2 being Element of Q.(Gauss_INT_Ring);
assume AS: y1 <> 0 & y2 <> 0 & u1 = [x1,y1] & u2= [ x2,y2];
P6: u1`1 * u2`2 = x1*y2 by LM8,AS;
P7: u2`1 * u1`2 = x2*y1 by LM8,AS;
P9: 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
P1: 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 P1,XBOOLE_0:def 4;
hence (QClass.u1) = (QClass.u2) by QUOFIELD:8,XBOOLE_0:def 7;
end;
hence thesis by AS,P6,P7,P9,XCMPLX_1:94,95;
end;
definition
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 P1: dom ad = [:G_RAT_SET,G_RAT_SET:] by RELAT_1:62;
for z be element st z in [:G_RAT_SET,G_RAT_SET:]
holds ad.z in G_RAT_SET
proof
let z be element such that
P2: z in [:G_RAT_SET,G_RAT_SET:];
consider x,y be element such that
P3:(x in G_RAT_SET) & y in G_RAT_SET & (z = [x,y])
by P2,ZFMISC_1:def 2;
reconsider x1=x,y1=y as G_RAT by RLM3,P3;
ad.z = addcomplex.(x1,y1) by P2,P3,FUNCT_1:49
.= x1+y1 by BINOP_2:def 3;
hence ad.z in G_RAT_SET;
end;
hence thesis by P1,FUNCT_2:3;
end;
end;
definition
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 P2: dom mult = [:G_RAT_SET,G_RAT_SET:] by RELAT_1:62;
for z be element st z in [:G_RAT_SET,G_RAT_SET:] holds mult.z in G_RAT_SET
proof
let z be element such that
P3: z in [:G_RAT_SET,G_RAT_SET:];
consider x,y be element such that
P4: x in G_RAT_SET & y in G_RAT_SET & z = [x,y]
by P3,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as G_RAT by RLM3,P4;
mult.z = multcomplex.(x1,y1) by P3,P4,FUNCT_1:49
.= x1*y1 by BINOP_2:def 5;
hence mult.z in G_RAT_SET;
end;
hence thesis by P2,FUNCT_2:3;
end;
end;
begin :: 5. Rational field
Defadd:
addreal||RAT = addrat
proof
set ad = addreal||RAT;
[:RAT,RAT:] c= [:REAL,REAL:] by NUMBERS:12,ZFMISC_1:96;
then Q20: [:RAT,RAT:] c= dom (addreal) by FUNCT_2:def 1;
then Q2: dom ad = [:RAT,RAT:] by RELAT_1:62;
Q3: dom (addrat) = [:RAT,RAT:] by FUNCT_2:def 1;
for z be element st z in dom ad holds ad.z = addrat.z
proof
let z be element;
assume P3: z in dom ad;
then consider x, y be element such that
P4: x in RAT & y in RAT & z = [x,y] by Q2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Rational by P4;
thus ad.z = addreal.(x1,y1) by P3,P4,Q2,FUNCT_1:49
.= x1+y1 by BINOP_2:def 9
.= addrat.(x1,y1) by BINOP_2:def 15
.= addrat.z by P4;
end;
hence thesis by Q20,Q3,FUNCT_1:2,RELAT_1:62;
end;
Defmult:
multreal||RAT = multrat
proof
set ad = multreal||RAT;
[:RAT,RAT:] c= [:REAL,REAL:] by NUMBERS:12,ZFMISC_1:96;
then Q20: [:RAT,RAT:] c= dom (multreal) by FUNCT_2:def 1;
then Q2: dom ad = [:RAT,RAT:] by RELAT_1:62;
Q3: dom (multrat) = [:RAT,RAT:] by FUNCT_2:def 1;
for z be element st z in dom ad holds ad.z = multrat.z
proof
let z be element;
assume P3: z in dom ad;
then consider x, y be element such that
P4: x in RAT & y in RAT & z = [x,y] by Q2,ZFMISC_1:def 2;
reconsider x1 = x, y1 = y as Rational by P4;
thus ad.z = multreal.(x1,y1) by P3,P4,Q2,FUNCT_1:49
.= x1*y1 by BINOP_2:def 11
.= multrat.(x1,y1) by BINOP_2:def 17
.= multrat.z by P4;
end;
hence thesis by Q20,Q3,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
func F_Rat -> strict non empty doubleLoopStr equals
doubleLoopStr (# RAT, addrat, multrat, In(1,RAT), In(0,RAT) #);
correctness;
end;
theorem RATLM10:
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
P2: for v being 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;
P3:
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 being Element of F_Rat st v <> 0. F_Rat
holds v is left_invertible
proof
let v be Element of F_Rat;
assume AS0: 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 AS0,XCMPLX_0:def 7;
hence v is left_invertible;
end;
hence thesis by P2,P3,Defadd,Defmult,GROUP_1:def 12,NUMBERS:12;
end;
theorem
F_Rat is Subfield of F_Real by EC_PF_1:2,RATLM10;
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,RATLM10;
end;
registration
cluster F_Rat -> well-unital;
coherence
proof
let x be Element of F_Rat;
reconsider x1 = x as Rational;
thus x*1.F_Rat = x1 * 1 by BINOP_2:def 17
.=x;
thus 1.F_Rat *x = 1*x1 by BINOP_2:def 17
.=x;
end;
end;
registration
cluster -> rational for Element of F_Rat;
coherence;
end;
registration
let x be Element of F_Rat, y be Rational;
identify -x with -y when x = y;
compatibility
proof
reconsider w = -y as Element of F_Rat by RAT_1:def 2;
assume x = y;
then x+w = y + -y by BINOP_2:def 15
.= 0.F_Rat;
hence thesis by VECTSP_1:16;
end;
end;
theorem RATLM40:
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 AS: x <> 0.F_Rat & x1 = x;
reconsider w = x1" as Element of F_Rat by RAT_1:def 2;
w * x = x1" * x1 by AS,BINOP_2:def 17
.= 1.F_Rat by AS,XCMPLX_0:def 7;
hence thesis by AS,VECTSP_1:def 10;
end;
theorem RATLM60:
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
proof
let x, y be Element of F_Rat, x1, y1 be Rational;
assume AS: x1 = x & y1 = y & y <> 0.F_Rat;
then y" = y1" by RATLM40;
hence x/y = x1/y1 by AS,BINOP_2:def 17;
end;
theorem RATLM70:
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 RATLM80:
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 RATLM90:
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 AS: x = x1;
B1: hpd in C1;
C1 c= C by EC_PF_1:def 1;
then reconsider g = hpd as Element of K by B1;
x + g = x1 + hpd by AS,RATLM70
.= 0.K1 by VECTSP_1:19
.= 0.K by EC_PF_1:def 1;
hence thesis by VECTSP_1:16;
end;
theorem
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 AS: x = x1 & y = y1;
then P2: -y =-y1 by RATLM90;
the addF of K1 = (the addF of K) || C1 by EC_PF_1:def 1;
hence thesis by AS,P2,FUNCT_1:49,ZFMISC_1:87;
end;
theorem RATLM110:
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 AS: x = x1 & x <> 0.K;
then B2: x1 <> 0.K1 by EC_PF_1:def 1;
B3: hpd in C1;
C1 c= C by EC_PF_1:def 1;
then reconsider g = hpd as Element of K by B3;
B4: x*g = x1*hpd by AS,RATLM80
.= 1.K1 by B2,VECTSP_1:def 10;
x*g = 1.K by B4,EC_PF_1:def 1;
hence thesis by AS,VECTSP_1:def 10;
end;
theorem
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 AS: x = x1 & y = y1 & y <> 0.K;
then y" = y1" by RATLM110;
hence thesis by AS,RATLM80;
end;
set K = F_Rat;
theorem RATLM130:
for K1 be Subfield of F_Rat, n be Nat holds n in the carrier of K1
proof
let K1 be Subfield of F_Rat, n be Nat;
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 A2: P[0];
A3: now let n be Nat;
assume B1: P[n];
B2: 1.K1 = 1.K by EC_PF_1:def 1
.= 1;
B4: 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 B1,B2,B4,FUNCT_1:49,ZFMISC_1:87
.= 1+n by BINOP_2:def 15;
hence P[n+1] by B1,B2,BINOP_1:17;
end;
for n being Nat holds P[n] from NAT_1:sch 2(A2,A3);
hence thesis;
end;
theorem RATLM140:
for K1 be Subfield of F_Rat, m be Integer holds m in the carrier of K1
proof
let K1 be Subfield of F_Rat, m be Integer;
set C = the carrier of K;
set C1 = the carrier of K1;
per cases;
suppose 0 <= m;
then m in NAT by INT_1:3;
hence m in C1 by RATLM130;
end;
suppose 0 > m;
then reconsider mm = -m as Element of NAT by INT_1:3;
reconsider mmm = mm as Element of K1 by RATLM130;
consider mm1 be Element of K1 such that
X0: mmm+mm1 =0.K1 by ALGSTR_0:def 11;
XX: C1 c= C by EC_PF_1:def 1;
then reconsider mm2 = mm1 as Element of K by TARSKI:def 3;
reconsider mm3 = mm as Element of K by X0,XX,TARSKI:def 3;
WW: -mm = -mm3;
mm3+mm2 = 0.K1 by X0,RATLM70
.= 0.K by EC_PF_1:def 1;
then mm2 = -mm by WW,VECTSP_1:16;
hence m in C1;
end;
end;
theorem RATLM150:
for K1 be Subfield of F_Rat, x be set st x in F_Rat holds x in K1
proof
let K1 be Subfield of F_Rat, x be set;
set C = the carrier of K;
set C1 = the carrier of K1;
assume x in K;
then reconsider x1 = x as Rational;
consider m be Integer, k be Nat such that
B1: k<>0 & x1 = m/k by RAT_1:8;
B2: m in C1 by RATLM140;
reconsider k2 = k, m2 = m as Element of F_Rat by RAT_1:def 2;
reconsider k0 = k as Element of K1 by RATLM130;
B5: k0 <> 0.K by B1;
then k0 <> 0.K1 by EC_PF_1:def 1;
then consider k0i be Element of K1 such that
B6: k0i*k0 = 1.K1 by VECTSP_1:def 9;
B7: k0i in C1;
C1 c= C by EC_PF_1:def 1;
then reconsider kk0 = k0i as Element of K by B7;
kk0*k2 = 1.K1 by B6,RATLM80
.= 1.K by EC_PF_1:def 1;
then B8: kk0 = k2" by B5,VECTSP_1:def 10;
B10:the multF of K1 = (the multF of K) || C1 by EC_PF_1:def 1;
m/k = m2/k2 by RATLM60,B1
.= (the multF of K1).(m2,k2") by B2,B8,B10,FUNCT_1:49,ZFMISC_1:87;
hence x in K1 by B1,B2,B8,BINOP_1:17;
end;
registration
cluster F_Rat -> prime;
coherence
proof
now let K1 be strict Subfield of K;
set C = the carrier of K;
set C1 = the carrier of K1;
A1: for x being set st x in K holds x in K1 by RATLM150;
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 being Field holds K1 is strict Subfield of K implies K1 = K;
hence thesis by EC_PF_1:def 2;
end;
end;
begin :: 6. Gaussian rational number field
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
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 P2: dom scmult = [:the carrier of F_Rat,G_RAT_SET:] by RELAT_1:62;
for z be element st z in [:the carrier of F_Rat,G_RAT_SET:]
holds scmult.z in G_RAT_SET
proof
let z be element such that
P3: z in [:the carrier of F_Rat,G_RAT_SET:];
consider x, y be element such that
P4: (x in the carrier of F_Rat) & y in G_RAT_SET & z = [x,y]
by P3,ZFMISC_1:def 2;
reconsider x1 = x as Element of RAT by P4;
reconsider y1 = y as G_RAT by RLM3,P4;
scmult.z = multcomplex.(x1,y1) by P3,P4,FUNCT_1:49
.= x1*y1 by BINOP_2:def 5;
hence scmult.z in G_RAT_SET;
end;
hence thesis by P2,FUNCT_2:3;
end;
end;
theorem RLM5:
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 RLM6:
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
func Gauss_RAT_Module -> strict non empty VectSpStr over F_Rat equals
VectSpStr (# G_RAT_SET, g_rat_add, In(0,G_RAT_SET), RSc_Mult #);
coherence;
end;
RTh1:
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;
P1: for v, w being 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 RLM3;
thus v + w = v1 + w1 by RLM5
.= w + v by RLM5;
end;
P2: for u, v, w being 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 RLM3;
X1: u + v = u1+v1 by RLM5;
X2: v + w = v1+w1 by RLM5;
thus (u + v) + w = u1+v1+w1 by RLM5,X1
.= u1+(v1+w1)
.= u+(v+w) by RLM5,X2;
end;
P3: for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
reconsider v1 = v as G_RAT by RLM3;
thus v + 0.ZS = v1 + 0 by RLM5
.= v;
end;
P4: for v being 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 RLM3;
X3: m1 * v = (-1) * v1 by RLM6
.= -v1;
thus v + (m1 * v) = v1 + (-v1) by X3,RLM5
.= 0.ZS;
end;
P5: for a, b be Element of F_Rat, v being 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 RLM3;
reconsider a1 = a, b1 = b as Element of RAT;
Y1: a+b = a1+b1 by BINOP_2:def 15;
X2:(a1*v1 = a*v) & (b1*v1 = b*v) by RLM6;
thus (a + b) * v = (a1 + b1) * v1 by Y1,RLM6
.= a1*v1 + b1*v1
.= a*v + b*v by X2,RLM5;
end;
P6: for a be Element of F_Rat, v, w being 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 RLM3;
reconsider a1 = a as Element of RAT;
Y2: (v + w) = (v1 + w1) by RLM5;
Z1: (a1*v1 = a*v) & (a1*w1 = a*w) by RLM6;
thus a * (v + w) = a1 * (v1 + w1) by Y2,RLM6
.= a1*v1 + a1*w1
.= a*v + a*w by Z1,RLM5;
end;
P7: for a, b be Element of F_Rat for v being 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 RLM3;
reconsider a1 = a, b1 = b as Element of RAT;
Y2: b1 * v1 = b * v by RLM6;
Y3: a*b = a1*b1 by BINOP_2:def 17;
thus (a * b) * v
= (a1 * b1) * v1 by RLM6,Y3
.= a1 * (b1 * v1)
.= a * (b * v) by Y2,RLM6;
end;
for v being 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 RLM3;
thus 1.F_Rat * v = 1*v1 by RLM6
.= v;
end;
hence thesis by P1,P2,P3,P4,P5,P6,P7,RLVECT_1:def 2,def 3,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 RTh1;
end;
theorem RLM8:
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
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;
RTh2:
Gauss_RAT_Ring is Field
proof
set ZS = Gauss_RAT_Ring;
P1: for v, w being 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 RLM3;
thus v + w = v1 + w1 by RLM5
.= w + v by RLM5;
end;
P2: for u, v, w being 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 RLM3;
X1: u + v = u1+v1 by RLM5;
X2: v + w = v1+w1 by RLM5;
thus (u + v) + w = u1+v1+w1 by RLM5,X1
.= u1+(v1+w1)
.= u+(v+w) by RLM5,X2;
end;
P3: for v being Element of ZS holds v + 0.ZS = v
proof
let v be Element of ZS;
reconsider v1 = v as G_RAT by RLM3;
thus v + 0.ZS = v1 + 0 by RLM5
.= v;
end;
P4: for v being Element of ZS holds v is right_complementable
proof
let v be Element of ZS;
reconsider v1 = v as G_RAT by RLM3;
reconsider w1 = (-1) as Element of ZS by RLM4;
Y2: w1 * v = (-1) * v1 by RLM8;
take (w1*v);
thus v + (w1*v) = v1 + ((-1) * v1) by Y2,RLM5
.= 0.ZS;
end;
P5: for a, b, v being 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 RLM3;
reconsider ab = (a+b) as G_RAT by RLM3;
Y2: (a1*v1 = a*v) & (b1*v1 = b*v) by RLM8;
thus (a + b) * v = ab * v1 by RLM8
.= (a1 + b1) * v1 by RLM5
.= a1*v1 + b1*v1
.= a*v + b*v by Y2,RLM5;
end;
P6: for a, v, w being 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 RLM3;
reconsider vw = (v+w) as G_RAT by RLM3;
Y2: (a1*v1 = a*v) & (a1*w1 = a*w) by RLM8;
thus a * (v + w) = a1 * vw by RLM8
.= a1 * (v1 + w1) by RLM5
.= a1*v1 + a1*w1
.= a*v + a*w by Y2,RLM5;
thus (v + w) * a = v*a + w*a by P5;
end;
P700: for a, b being 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 RLM3;
thus a * b = a1*b1 by RLM8
.= b * a by RLM8;
end;
P7: for a, b, v being 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 RLM3;
reconsider ab = (a*b), bv = (b*v) as G_RAT by RLM3;
thus (a * b) * v = ab * v1 by RLM8
.= (a1 * b1) * v1 by RLM8
.= a1 * (b1 * v1)
.= a1 * bv by RLM8
.= a * (b * v) by RLM8;
end;
P8: for v being 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 RLM3;
thus v * 1.ZS = v1 * 1 by RLM8
.= v;
thus 1.ZS * v = 1 * v1 by RLM8
.= v;
end;
for v being Element of ZS st v <> 0.ZS holds v is left_invertible
proof
let v be Element of ZS;
assume A1: v <> 0.ZS;
reconsider v1 = v as G_RAT by RLM3;
reconsider w = (v1)" as Element of ZS by RLM4;
w*v = (v1)"*v1 by RLM8
.= 1.ZS by A1,XCMPLX_0:def 7;
hence thesis;
end;
hence thesis by P1,P2,P3,P4,P6,P7,P8,P700,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,def 3,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 RTh2;
end;
theorem
ex I be Function of Gauss_INT_Field,Gauss_RAT_Ring
st (for z be element st z in the carrier of Gauss_INT_Field
ex x, y be G_INTEG, u being Element of Q.(Gauss_INT_Ring)
st y <> 0 & u = [x,y] & z = QClass.u & I.z = x/y) &
I is one-to-one onto &
(for x, y be Element of Gauss_INT_Field
holds I.(x+y) = I.x + I.y & I.(x*y) = I.x * I.y) &
I.(0.Gauss_INT_Field) = 0.Gauss_RAT_Ring &
I.(1.Gauss_INT_Field) = 1.Gauss_RAT_Ring
proof
defpred P[element,element] means
ex x, y be G_INTEG, u being Element of Q.(Gauss_INT_Ring)
st y <> 0 & u = [x,y] & $1 = QClass.u & $2 = x/y;
P1: for z be element st z in the carrier of Gauss_INT_Field
ex w be element st w in the carrier of Gauss_RAT_Ring & P[z,w]
proof
let z be element;
assume z in the carrier of Gauss_INT_Field;
then consider u being 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 LM3;
take x/y;
thus thesis by A2,A3;
end;
consider I be Function of Gauss_INT_Field,Gauss_RAT_Ring such that
P2: for z be element
st z in the carrier of Gauss_INT_Field holds P[z,I.z]
from FUNCT_2:sch 1(P1);
P3:
now let z1, z2 be element;
assume P31: z1 in dom I & z2 in dom I & I.z1 = I.z2;
then P32: 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 being Element of Q.(Gauss_INT_Ring)
such that
P33: y1 <> 0 & u1 = [x1,y1] & z1 = QClass.u1 & I.z1 = x1/y1 by P2;
consider x2, y2 be G_INTEG, u2 being Element of Q.(Gauss_INT_Ring)
such that
P34: y2 <> 0 & u2 = [x2,y2] & z2 = QClass.u2 & I.z2 = x2/y2 by P2,P32;
thus z1 = z2 by P31,P33,P34,Rth3LM3;
end;
then P3X: I is one-to-one by FUNCT_1:def 4;
now let p1 be element;
assume p1 in the carrier of Gauss_RAT_Ring;
then reconsider p = p1 as G_RAT by RLM3;
consider x, y be G_INTEG such that
P41: y <> 0 & p = x/y by Rth3LM2;
reconsider x1 = x, y1 = y as Element of Gauss_INT_Ring by LM4;
y1 <> 0.(Gauss_INT_Ring) by P41;
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 being Element of Q.(Gauss_INT_Ring)
such that
P34: y2 <> 0 & u2 = [x2,y2] & z1 = QClass.u2 & I.z1 = x2/y2 by P2;
x/y = x2/y2 by Rth3LM3,P34,P41;
hence ex z1 be element st z1 in the carrier of Gauss_INT_Field
& I.z1 = p1 by P34,P41;
end;
then rng I = the carrier of Gauss_RAT_Ring by FUNCT_2:10;
then P4: I is onto by FUNCT_2:def 3;
P5: 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 being Element of Q.(Gauss_INT_Ring) such that
P33: y1 <> 0 & u1 = [x1,y1] & z1 = QClass.u1 & I.z1 = x1/y1 by P2;
consider x2, y2 be G_INTEG,
u2 being Element of Q.(Gauss_INT_Ring) such that
P34: y2 <> 0 & u2 = [x2,y2] & z2 = QClass.u2 & I.z2 = x2/y2 by P2;
set z12 = z1+z2;
consider x12, y12 be G_INTEG,
u12 being Element of Q.(Gauss_INT_Ring) such that
P3312X: y12 <> 0 & u12 = [x12,y12] & z12 = QClass.u12 & I.z12 = x12/y12
by P2;
Q1X: x1/y1 + x2/y2 = (x1*y2 + x2*y1)/(y1*y2) by P33,P34,XCMPLX_1:116;
AA1: u1`1*u2`2 = x1*y2 & u2`1*u1`2 = x2*y1 & u1`2*u2`2 = y1*y2
by LM8,P33,P34;
Q12: padd (u1,u2) = [(x1*y2)+(x2*y1),y1*y2] by AA1,LM5;
z12 = qadd ((QClass.u1),(QClass.u2)) by P33,P34,QUOFIELD:def 12
.= QClass.(padd (u1,u2)) by QUOFIELD:9;
then AA4: u12 in QClass.(padd (u1,u2)) by P3312X,QUOFIELD:5;
AA6: u12`1 * (padd (u1,u2))`2 = x12*(y1*y2) by LM8,P3312X,AA1;
(padd (u1,u2))`1 * u12`2 = (x1*y2 + y1*x2) * y12 by LM8,P3312X,Q12;
then x12*(y1*y2 ) = (x1*y2 + y1*x2)*y12 by AA6,AA4,QUOFIELD:def 4;
then X1: x12/y12 = (x1*y2 + x2*y1)/(y1*y2)
by P33,P34,P3312X,XCMPLX_1:94;
set z12 = z1*z2;
consider x12, y12 be G_INTEG,
u12 being Element of Q.(Gauss_INT_Ring) such that
P3312: y12 <> 0 & u12 = [x12,y12] & z12 = QClass.u12 & I.z12 = x12/y12
by P2;
Q1: (x1/y1) * (x2/y2) = (x1*x2)/(y1*y2) by XCMPLX_1:76;
AA1: u1`1*u2`1 = x1*x2 & u2`2*u1`2 = y1*y2 by LM8,P33,P34;
z12 = qmult ((QClass.u1),(QClass.u2)) by P33,P34,QUOFIELD:def 13
.= QClass.(pmult (u1,u2)) by QUOFIELD:10;
then AA4: u12 in QClass.(pmult (u1,u2)) by P3312,QUOFIELD:5;
AA6: u12`1 * (pmult (u1,u2))`2 = x12*(y1*y2) by LM8,P3312,AA1;
(pmult (u1,u2))`1 * u12`2 = (x1*x2) * y12 by LM8,P3312,AA1;
then x12*(y1*y2 ) = (x1*x2)*y12 by AA6,AA4,QUOFIELD:def 4;
then x12/y12 = (x1*x2)/(y1*y2) by P33,P34,P3312,XCMPLX_1:94;
hence thesis by X1,Q1,Q1X,P3312,P3312X,P33,P34,RLM5,RLM8;
end;
X1: 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 P5;
P6: 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 X1,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 X3: I.(1.Gauss_INT_Field) <> 0.Gauss_RAT_Ring by P3,P6;
X4: I.(1.Gauss_INT_Field) = I.((1.Gauss_INT_Field)*(1.Gauss_INT_Field))
by VECTSP_1:def 8
.= I.(1.Gauss_INT_Field) * I.(1.Gauss_INT_Field) by P5;
1.Gauss_RAT_Ring = (I.(1.Gauss_INT_Field))" * (I.(1.Gauss_INT_Field))
by VECTSP_1:def 10,X3
.= (I.(1.Gauss_INT_Field))" * (I.(1.Gauss_INT_Field))
* (I.(1.Gauss_INT_Field)) by X4,GROUP_1:def 3
.= (1. Gauss_RAT_Ring) * (I.(1.Gauss_INT_Field)) by VECTSP_1:def 10,X3
.= I.(1.Gauss_INT_Field) by VECTSP_1:def 8;
hence thesis by P2,P3X,P4,P5,P6;
end;
begin :: 7. Gaussian integer ring is Euclidian
definition
let a,b be G_INTEG;
pred a Divides b means
ex c being G_INTEG st b = a * c;
reflexivity
proof
let a be G_INTEG;
take 1;
thus a = a * 1;
end;
end;
theorem
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 LM3;
bb = aa*cc by A1,A2,LM8;
hence thesis;
end;
theorem
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 LM4;
b = a*c by A1,A2,LM8;
hence thesis by GCD_1:def 1;
end;
definition
let z be G_RAT;
redefine func z *' -> G_RAT;
coherence;
end;
definition
let z be G_RAT;
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 A3: (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 A3;
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 A3: (Re(z * (z *')) = Rez * Rez - Imz * (-Imz)) &
(Im(z * (z *')) = Rez * (-Imz) + Rez * Imz) by COMPLEX1:9;
A4: (z * (z *')) = (Re(z * (z *'))) + (Im(z * (z *'))***) by COMPLEX1:13
.= Re(z * (z *')) by A3;
(Re z)^2 >= 0 & (Im z)^2 >= 0 by XREAL_1:63;
hence thesis by A3,A4;
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 A3: 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;
A4: z * (z *') = (Re(z * (z *'))) + (Im(z * (z *'))***) by COMPLEX1:13
.= Re(z * (z *')) by A3;
(Re z)^2 >= 0 & (Im z)^2 >= 0 by XREAL_1:63;
then Re(z * (z *')) in NAT by A3,INT_1:3;
hence thesis by A4;
end;
end;
theorem
for x be G_RAT holds Norm(x *') = Norm(x);
theorem ThNorm2:
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 ThNorm3:
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 AS: Norm(x) = 1;
A1: x = Re x+Im x*** by COMPLEX1:13;
A2: 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 defg;
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 AS,A2,LMThNorm3;
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 A1;
end;
assume AS: x = 1 or x = -1 or x = ** or x = -**;
per cases by AS;
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 ThNorm4:
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;
attr z is g_int_unit means
:defGintunit:
Norm(z) = 1;
end;
definition
let x,y be G_INTEG;
pred x is_associated_to y means
x Divides y & y Divides x;
symmetry;
end;
theorem ThGIR2GIE3:
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 LM3;
reconsider ccb = cb as G_INTEG by LM3;
bb = aa*cca by A1,A3,LM8;
then A7: aa Divides bb;
aa = bb*ccb by A1,A4,LM8;
then bb Divides aa;
hence thesis by A7;
end;
theorem ThGIE2GIR3:
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 LM4;
reconsider cb = ccb as Element of Gauss_INT_Ring by LM4;
b = a*ca by A1,A3,LM8;
then A7: a divides b by GCD_1:def 1;
a = b*cb by A1,A4,LM8;
then b divides a by GCD_1:def 1;
hence thesis by A7,GCD_1:def 3;
end;
LmAssociates:
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 AS: x is_associated_to y;
reconsider x1 = x, y1 = y as Element of Gauss_INT_Ring by LM4;
B3: x1 is_associated_to y1 by AS,ThGIE2GIR3;
x1 divides y1 by B3,GCD_1:def 3;
then consider z1 be Element of Gauss_INT_Ring such that
A1: y1 = x1 * z1 by GCD_1:def 1;
y1 divides x1 by B3,GCD_1:def 3;
then consider z2 be Element of Gauss_INT_Ring such that
A2: x1 = y1 * z2 by GCD_1:def 1;
reconsider z3 = z1 * z2 as Element of Gauss_INT_Ring;
per cases;
suppose A3X: x1 * y1 <> 0.Gauss_INT_Ring;
x1 * y1 = ((x1 * z1) * y1) * z2 by A1,A2,GROUP_1:def 3
.= ((x1 * y1) * z1) * z2 by GROUP_1:def 3
.= (x1 * y1) * z3 by GROUP_1:def 3;
then A4: z3 = 1.Gauss_INT_Ring by A3X,GCD_1:17
.= 1;
reconsider zz1 = z1,zz2 = z2 as G_INTEG by LM3;
reconsider zz3 = z3 as G_INTEG by LM3;
A5: Norm(zz1) = 1
proof
zz3 = zz1*zz2 by LM8;
then Norm(zz3) = Norm(zz1) * Norm(zz2) by ThNorm2;
hence Norm(zz1) = 1 by A4,COMPLEX1:30,NAT_1:15;
end;
y = x*zz1 by A1,LM8;
hence Norm(y) = Norm(x) * Norm(zz1) by ThNorm2
.= Norm(x) by A5;
end;
suppose A3Z: x1 * y1 = 0.Gauss_INT_Ring;
NX1: x1 = 0.Gauss_INT_Ring
proof
assume NA1: not x1 = 0.Gauss_INT_Ring;
then y1 = 0.Gauss_INT_Ring by A3Z,VECTSP_2:def 1;
hence contradiction by NA1,A2;
end;
y1 = 0.Gauss_INT_Ring
proof
assume NA1: not y1 = 0.Gauss_INT_Ring;
then x1 = 0.Gauss_INT_Ring by A3Z,VECTSP_2:def 1;
hence contradiction by NA1,A1;
end;
hence Norm(x) = Norm(y) by NX1;
end;
end;
theorem ThGintunit:
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 AS: z is unital;
consider x be Element of Gauss_INT_Ring such that
B1: 1.Gauss_INT_Ring = z * x by AS,GCD_1:def 1,def 2;
reconsider xx = x as G_INTEG by LM3;
B3: z * x = zz * xx by A1,LM8;
reconsider gintone = In(1,G_INT_SET) as G_INTEG;
Norm(zz) * Norm(xx) = Norm(gintone) by B1,B3,ThNorm2
.= 1 by COMPLEX1:30;
hence zz is g_int_unit by NAT_1:15;
end;
assume AS: zz is g_int_unit;
ex w being Element of Gauss_INT_Ring st 1.Gauss_INT_Ring = z * w
proof
per cases by AS,A1,ThNorm3;
suppose V1: z = 1;
take w = z;
thus 1.Gauss_INT_Ring = 1*1
.= z * w by V1,LM8;
end;
suppose V2: z = -1;
take w = z;
thus 1.Gauss_INT_Ring = (-1)*(-1)
.= z * w by V2,LM8;
end;
suppose V3: z = **;
reconsider w = -** as Element of Gauss_INT_Ring by LM4;
take w;
thus 1.Gauss_INT_Ring = ***(-**)
.= z * w by V3,LM8;
end;
suppose V4: z = -**;
reconsider w = ** as Element of Gauss_INT_Ring by LM7i;
take w;
thus 1.Gauss_INT_Ring = (-**)***
.= z * w by V4,LM8;
end;
end;
hence z is unital by GCD_1:def 1,def 2;
end;
theorem ThAssociates0:
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 LM4;
consider c1 be Element of Gauss_INT_Ring such that
A12: c1 is unital & y1 * c1 = x1 by A1,ThGIE2GIR3,GCD_1:18;
reconsider c = c1 as G_INTEG by LM3;
A13: c is g_int_unit by A12,ThGintunit;
c1 * y1 = c * y by LM8;
hence ex c be G_INTEG st c is g_int_unit & x = c*y by A12,A13;
end;
given c0 be G_INTEG such that
A21: c0 is g_int_unit & x = c0*y;
reconsider xx = x as Element of Gauss_INT_Ring by LM4;
reconsider yy = y as Element of Gauss_INT_Ring by LM4;
reconsider c = c0 as Element of Gauss_INT_Ring by LM4;
A22: c is unital by A21,ThGintunit;
c * yy = c0 * y by LM8;
hence x is_associated_to y by A21,A22,ThGIR2GIE3,GCD_1:18;
end;
theorem ThAssociates1:
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
P1: d is g_int_unit & x = d* x*' by ThAssociates0;
P4: x*' = Re x+ (- Im x)***;
now per cases by P1,ThNorm3;
suppose d = 1;
then (Im x) = (- Im x) by P1,P4,COMPLEX1:12;
hence contradiction by A1;
end;
suppose d = -1;
then (Re x) = (Re (-x*')) by P1
.= - Re (x*') by COMPLEX1:17
.= - ( Re x) by COMPLEX1:12,P4;
hence contradiction by A1;
end;
suppose d = **;
then (Im x) = Im (***Re x+ (- Im x)******) by P1
.= Re x by COMPLEX1:12;
hence contradiction by A1;
end;
suppose d = -**;
then (Im x) = Im (***(-Re x)+ (Im x)*(-1r)) by P1
.= - Re x by COMPLEX1:12;
hence contradiction by A1;
end;
end;
hence contradiction;
end;
theorem ThAssociates2:
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 AS: x is_associated_to y & y is_associated_to z;
consider c be G_INTEG such that
A1: c is g_int_unit & x = c*y by AS,ThAssociates0;
consider d be G_INTEG such that
A2: d is g_int_unit & y = d*z by AS,ThAssociates0;
A3: x = (c*d) * z by A1,A2;
reconsider e = c*d as G_INTEG;
Norm(e) = 1*Norm(d) by A1,ThNorm2
.= 1 by A2;
hence thesis by A3,defGintunit,ThAssociates0;
end;
theorem ThAssociates3:
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 ThAssociates0;
A2: x*' = c*' * y*' by A1,COMPLEX1:35;
Norm(c*') = 1 by A1;
hence thesis by A2,defGintunit,ThAssociates0;
end;
theorem
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;
AA: x*' is_associated_to x implies y*' is_associated_to y
proof
assume B1: x*' is_associated_to x;
then B2: x is_associated_to y by A2,ThAssociates2;
then x*' is_associated_to y*' by ThAssociates3;
then x is_associated_to y*' by B1,ThAssociates2;
hence y*' is_associated_to y by B2,ThAssociates2;
end;
AB: Norm(x*') <> 0
proof
assume Norm(x*') = 0;
then Norm(y) = 0 by A2,LmAssociates;
hence contradiction by A1,ThNorm4,COMPLEX1:4;
end;
hereby
consider c being G_INTEG such that
A3: c is g_int_unit and
A4: x*' = c * y by A2,ThAssociates0;
assume x Divides y;
then consider d being G_INTEG such that
A5: y = x * d;
A6: x*' = (c*d) * x by A4,A5;
reconsider e = c*d as G_INTEG;
A7: Norm(e) = Norm(c)*Norm(d) by ThNorm2
.= Norm(d) by A3;
per cases;
suppose d is g_int_unit;
hence contradiction
by AA,A1,A6,A7,defGintunit,ThAssociates0,ThAssociates1;
end;
suppose A8: not d is g_int_unit;
Norm(x*') = Norm(e) * Norm(x) by A6,ThNorm2;
hence contradiction by A7,A8,AB,XCMPLX_1:7;
end;
end;
consider c being G_INTEG such that
A3: c is g_int_unit and
A4: y = c * x*' by A2,ThAssociates0;
assume y Divides x;
then consider d being G_INTEG such that
A5: x = y * d;
A6: x = (c*d) * x*' by A4,A5;
reconsider e = c*d as G_INTEG;
A7: Norm(e) = Norm(c)*Norm(d) by ThNorm2
.= Norm(d) by A3;
per cases;
suppose d is g_int_unit;
hence contradiction
by AA,A1,A6,A7,defGintunit,ThAssociates0,ThAssociates1;
end;
suppose A8: not d is g_int_unit;
Norm(x) = Norm(e) * Norm(x*') by A6,ThNorm2;
hence contradiction by A7,A8,AB,XCMPLX_1:7;
end;
end;
definition
let p be G_INTEG;
attr p is g_prime means
Norm(p) > 1 &
for z being G_INTEG holds
not z Divides p or z is g_int_unit or z is_associated_to p;
end;
LMPRM1:
for a be Integer holds not a*a is Prime
proof
let a be Integer;
reconsider b = |.a.| as Element of NAT;
A0: 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 A0,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 A0,A2,INT_2:def 4;
end;
end;
LMPRM2:
for a be Integer st |.a.| <> 1
holds not 2*a*a is Prime
proof
let a be Integer;
assume AS: |.a.| <> 1;
reconsider b = |.a.| as Element of NAT;
A0: 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 AS,A0;
end;
suppose A1: 2 <= b;
1 < b by XXREAL_0:2,A1;
then A3: b*(1 qua Real) < b*b by XREAL_1:68;
A2: 1*(b*b) < 2*(b*b) by A1,XREAL_1:68;
b divides 2*b*b by INT_1:def 3;
hence thesis by A0,A2,A3,INT_2:def 4;
end;
end;
theorem
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 A0: Norm(q) is Prime & Norm(q) <> 2;
AX: (Re q)*(Re q) = (Re q)^2
.= |.(Re q).| ^2 by COMPLEX1:75
.=|.(Re q).| * |.(Re q).|;
A2: Norm(q)=(Re q+Im q***)*(Re q-(Im q)***) by COMPLEX1:13
.= (Re q)^2 + (Im q)^2;
assume N1: not (Re q <> 0 & Im q <> 0 & Re q <> Im q & - Re q <> Im q );
per cases by N1;
suppose Re q = 0;
hence contradiction by A0,A2,LMPRM1;
end;
suppose Im q = 0;
hence contradiction by A0,A2,LMPRM1;
end;
suppose C3: Re q = Im q; then
C30: Norm(q) = 2*(Re q)*(Re q) by A2;
|.Re q.| <> 1 by A0,A2,C3,AX;
hence contradiction by A0,C30,LMPRM2;
end;
suppose C4: - Re q = Im q; then
C40: Norm(q) = 2*(Re q)*(Re q) by A2;
|.Re q.| <> 1 by A0,A2,C4,AX;
hence contradiction by A0,C40,LMPRM2;
end;
end;
theorem
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 being 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 B1: not z is g_int_unit & not z is_associated_to q;
not z Divides q
proof
assume AS: z Divides q;
consider c being G_INTEG such that
B2: q = z * c by AS;
B6: Norm(q) = Norm(z)*Norm(c) by B2,ThNorm2;
then B3: Norm(z) divides Norm(q) by INT_1:def 3;
B4: Norm(z) > 1
proof
Norm(z) <> 0
proof
assume Norm(z) = 0;
then Norm(q) = 0*Norm(c) by B2,ThNorm2
.= 0;
hence contradiction by A1;
end;
then Norm z >= 0+1 by NAT_1:13;
hence thesis by B1,XXREAL_0:1;
end;
B421: Norm(c) <> 1 by B1,B2,defGintunit,ThAssociates0;
Norm(q) <> Norm(z) by A1,B6,B421,XCMPLX_1:7;
hence contradiction by A1,B3,B4,INT_2:def 4;
end;
hence thesis;
end;
end;
hence thesis by A1,INT_2:def 4;
end;
LM010:
ex f being Function of Gauss_INT_Ring,NAT
st for x be G_INTEG holds f.x = Norm(x)
proof
defpred P[element,element]
means ex z be G_INTEG st $1 = z & $2 = Norm(z);
P1: for x being Element of the carrier of Gauss_INT_Ring
ex y being Element of NAT st P[x,y]
proof
let x being Element of the carrier of Gauss_INT_Ring;
reconsider z = x as G_INTEG by LM3;
Norm(z) is Element of NAT by ORDINAL1:def 12;
hence thesis;
end;
consider f being Function of Gauss_INT_Ring, NAT such that
P2: for x being Element of Gauss_INT_Ring
holds P[x,f.x] from FUNCT_2:sch 3(P1);
now let x be G_INTEG;
x is Element of the carrier of Gauss_INT_Ring by LM4;
then ex z be G_INTEG st x=z & f.x = Norm(z) by P2;
hence f.x = Norm(x);
end;
hence thesis;
end;
theorem Norm4:
for q be G_RAT holds Norm(q) = |. Re q .|^2 + |. Im q .| ^2
proof
let q be G_RAT;
X1: |. 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 X1,COMPLEX1:75;
end;
theorem LM032:
for q be Element of REAL ex m be Element of INT st |.q - m .| <= 1/2
proof
let q be Element of REAL;
per cases;
suppose C1: |.q - [\q/] .| <= 1/2;
reconsider m= [\q/] as Element of INT by INT_1:def 2;
take m;
thus |.q - m .| <= 1/2 by C1;
end;
suppose C3: not |.q - [\q/] .| <= 1/2;
0 <= q - [\q/] by INT_1:def 6,XREAL_1:48;
then 1/2 < q - [\q/] by C3,ABSVALUE:def 1;
then 1/2 -1 <= q - [\q/] -1 by XREAL_1:9;
then C4: -1/2 <= q - ([\q/] + 1 );
q - ([\q/] + 1) <= ([\q/] + 1) -([\q/] + 1) by INT_1:29,XREAL_1:9;
then C5: 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 C4,C5,ABSVALUE:5;
end;
end;
LM030: for f being Function of Gauss_INT_Ring,NAT
st for x be 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
let f be Function of Gauss_INT_Ring,NAT;
assume P1: for x be G_INTEG holds f.x = Norm(x);
let a, b being Element of Gauss_INT_Ring;
assume Q1: b <> 0. Gauss_INT_Ring;
reconsider a0 = a, b0 = b as G_INTEG by LM3;
reconsider x = a0/b0, b1 = b0 as G_RAT;
consider m be Element of INT such that
P4: |.(Re x) - m .| <= 1/2 by LM032;
consider n be Element of INT such that
P5: |.(Im x) - n .| <= 1/2 by LM032;
set q0 = m+n***;
reconsider q0 as G_INTEG;
reconsider q1 = q0 as G_RAT;
reconsider r0 = a0 - q0*b0 as G_INTEG;
P6: Re(x -q0) = (Re x) - (Re q0) by COMPLEX1:19
.= (Re x) - m by COMPLEX1:12;
P7: 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 P81: |.(Re x) - m .| ^2 <= (1/2)^2 by P4,SQUARE_1:15;
0 <= |.(Im x) - n .| by COMPLEX1:46;
then P82: |.(Im x) - n .| ^2 <= (1/2)^2 by P5,SQUARE_1:15;
|.(Re x) - m .| ^2 + |. (Im x) - n .| ^2 <= (1/2)^2 + (1/2)^2
by P81,P82,XREAL_1:7;
then P8: Norm(xq1) <= 1/2 by P6,P7,Norm4;
reconsider bxq1 = b1*xq1 as G_RAT;
P9: b1*xq1 = b0*(a0/b0) -b0*q0
.= r0 by Q1,XCMPLX_1:87;
P14: Norm(bxq1) = Norm(b1)*Norm(xq1) by ThNorm2;
P11: Norm(r0) <= Norm(b1)/2 by P8,P9,P14,XREAL_1:64;
Norm(b0) <> 0 by Q1,ThNorm4;
then Norm(b1)/2 < Norm(b1) by XREAL_1:216;
then P10: Norm(r0) < Norm(b1) by P11,XXREAL_0:2;
reconsider q = q0, r = r0 as Element of Gauss_INT_Ring by LM4;
P13: q * b = q0*b0 by LM8;
a0 = q0*b0 + r0;
then P11: a = (q * b) + r by P13,LM5;
P12: f.r = Norm(r0) by P1;
f.b = Norm(b0) by P1;
hence thesis by P10,P11,P12;
end;
registration
cluster Gauss_INT_Ring -> Euclidian;
coherence
proof
consider f being Function of the carrier of Gauss_INT_Ring,NAT such that
P1: for x be G_INTEG holds f.x = Norm(x) by LM010;
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 ) ) by LM030,P1;
hence thesis by INT_3:def 8;
end;
end;
*