:: Gaussian Integers
:: by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama
::
:: Received May 19, 2013
:: Copyright (c) 2013-2026 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, POLYALG1;
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, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1,
VECTSP_1, FUNCSDOM, VECTSP_2, GCD_1, QUOFIELD, EC_PF_1, ZMODUL01,
POLYALG1;
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,
POLYALG1;
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, XTUPLE_0, QUOFIELD, SQUARE_1, RAT_1, NAT_1, INT_3,
ORDINAL1;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, XBOOLE_0, STRUCT_0, ALGSTR_0, GROUP_1;
equalities SQUARE_1, XCMPLX_0, COMPLEX1, BINOP_1, STRUCT_0, ALGSTR_0,
VECTSP_1, QUOFIELD, REALSET1;
expansions TARSKI, STRUCT_0, ALGSTR_0, VECTSP_1, POLYALG1;
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, 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 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;
attr z is g_integer means :Def1:
Re z in INT & Im z in INT;
end;
Lm1: for z being Complex st Re z is integer & Im z is integer
holds z is g_integer by INT_1:def 2;
registration
cluster -> g_integer for Integer;
coherence
proof
let c be Integer;
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 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 <i> -> 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 object;
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;
Lm2: <i> 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 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 Th3:
for x be object 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 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
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
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 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 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
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 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 Th2;
thus v + w = w1 + v1 by Th4
.= w + v by Th4;
end;
A2: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 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 being 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 being 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 being 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 being 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 for v being 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 being 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,def 15,def 16,def 17,
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 Lm3;
end;
theorem 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
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 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 Th2;
thus v + w = w1 + v1 by Th4
.= w + v by Th4;
end;
A2: 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 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 being 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 being 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 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 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 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 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 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 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 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 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,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 Lm4;
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 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
for x be Element of Gauss_INT_Ring holds x is G_INTEG by Th2;
theorem
for x be G_INTEG holds x is Element of Gauss_INT_Ring by Th3;
begin :: 2. Z-Algebra
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
::$CD
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 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 Th2;
thus v + w = v1 + w1 by Th4
.= w + v by Th4;
end;
A2: 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 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 being 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 being 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 being 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 being 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 for v being 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 being Vector of ZS 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 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 Th2;
thus v * w = v1 * w1 by Th6
.= w * v by Th6;
end;
A18: 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 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 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 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 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 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 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 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,def 3,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
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 :: 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[object,object,object] means
ex n,m be Integer st $1 = n & $2 = m & $3 = n+ <i> *m;
A1: for x, y being object st x in INT & y in INT
ex z being 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+ <i> *m;
thus thesis;
end;
consider F being Function of [:INT,INT:], G_INT_SET such that
A2: for x, y being 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+ <i> *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+ <i> *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+ <i> *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 being 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+ <i> *m1 by A4;
A13: F.x2 = F.(n2,m2) by A11
.= n2+ <i> *m2 by A4;
A14: n1 = Re(n2+ <i> *m2) by A9,A12,A13,COMPLEX1:12
.= n2 by COMPLEX1:12;
m1 = Im(n2+ <i> *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 :: 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
: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,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
func G_RAT_SET -> Subset of COMPLEX equals
the set of all z where z is G_RAT;
correctness
proof
now let x be object;
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 by NUMBERS:14,Def1;
end;
theorem 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 Th11:
for x be object st x is G_RAT holds x in G_RAT_SET;
theorem Th12:
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
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 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 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,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 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
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 :: 5. Rational field
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;
definition
func F_Rat -> strict non empty doubleLoopStr equals
doubleLoopStr (# RAT, addrat, multrat, In(1,RAT), In(0,RAT) #);
correctness;
end;
theorem 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 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;
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 being 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
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 x+y with a+b when x = a, y = b;
compatibility by BINOP_2:def 15;
identify x*y with a*b when x = a, y = b;
compatibility by BINOP_2:def 17;
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 = 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 x-y with a-b when x = a, y = b;
compatibility;
end;
theorem 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 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 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 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 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
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 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
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 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 being Nat holds P[n] from NAT_1:sch 2(A1,A2);
hence thesis;
end;
theorem 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 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
for K1 being 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 being 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 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 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 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 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
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 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 Th10;
thus v + w = v1 + w1 by Th27
.= w + v by Th27;
end;
A2: 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 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 being 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 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 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 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 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 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 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 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 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 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 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,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 Lm8;
end;
theorem 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
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 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 Th10;
thus v + w = v1 + w1 by Th27
.= w + v by Th27;
end;
A2: 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 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 being 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 being 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 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 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 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 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 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 Th10;
thus a * b = a1*b1 by Th29
.= b * a by Th29;
end;
A13: 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 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 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 Th10;
thus v * 1.ZS = v1 * 1 by Th29
.= v;
thus 1.ZS * v = 1 * v1 by Th29
.= 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 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,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 Lm9;
end;
theorem
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
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[object,object] 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;
A1: for z be object st z in the carrier of Gauss_INT_Field
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 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 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 being 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 being 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 being 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 being 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 being 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 being 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 being 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 :: 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 Th2;
bb = aa*cc by A1,A2,Th6;
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 Th3;
b = a*c by A1,A2,Th6;
hence thesis by GCD_1:def 1;
end;
definition
let z be G_RAT;
redefine func z *' -> G_RAT; :: redefines *' (COMPLEX1, definition)
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) * <i>)) = Rez) &
(Im(Rez + ((-Imz) * <i>)) = (-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 *'))*<i>) 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) * <i>)) = Rez) &
(Im(Rez + ((-Imz) * <i>)) = (-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 *'))*<i>) 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) * <i>)) = Re z &
Im(Re z + ((-Im z) * <i>)) = -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 *'))*<i>) 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
for x be G_RAT holds Norm(x *') = Norm(x);
theorem 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 Th35:
for x be G_INTEG holds Norm(x) = 1 iff x = 1 or x = -1 or x = <i> or x = -<i>
proof
let x be G_INTEG;
hereby
assume A1: Norm(x) = 1;
A2: x = Re x+Im x*<i> by COMPLEX1:13;
A3: Norm(x) = (Re x+Im x*<i>)*(Re x-(Im x)*<i>) 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 = <i> or x = -<i>) by A2;
end;
assume A4: x = 1 or x = -1 or x = <i> or x = -<i>;
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 = <i>;
hence Norm(x) = 1 by COMPLEX1:31;
end;
suppose x = -<i>;
hence Norm(x) = 1 by COMPLEX1:31;
end;
end;
theorem 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*<i>)*(Re x-(Im x)*<i>) 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
:Def20:
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 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 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 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,def 20;
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 being 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 = <i>;
reconsider w = -<i> as Element of Gauss_INT_Ring by Th3;
take w;
thus 1.Gauss_INT_Ring = <i>*(-<i>)
.= z * w by A8,Th6;
end;
suppose A9: z = -<i>;
reconsider w = <i> as Element of Gauss_INT_Ring by Lm2;
take w;
thus 1.Gauss_INT_Ring = (-<i>)*<i>
.= z * w by A9,Th6;
end;
end;
hence z is unital by GCD_1:def 2;
end;
theorem 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 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)*<i>;
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 = <i>;
then (Im x) = Im (<i>*Re x+ (- Im x)*<i>*<i>) by A2
.= Re x by COMPLEX1:12;
hence contradiction by A1;
end;
suppose d = -<i>;
then (Im x) = Im (<i>*(-Re x)+ (Im x)*(-1r)) by A2
.= - Re x by COMPLEX1:12;
hence contradiction by A1;
end;
end;
hence contradiction;
end;
theorem 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 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
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 being 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 being 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 being 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 being 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;
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;
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
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*<i>)*(Re q-(Im q)*<i>) 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
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 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 being 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 being 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 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 Th2;
Norm(z) is Element of NAT by ORDINAL1:def 12;
hence thesis;
end;
consider f being Function of Gauss_INT_Ring, NAT such that
A2: for x being 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 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*<i>)*(Re q-(Im q)*<i>) by COMPLEX1:13
.= (Re q)^2 + (Im q)^2
.= |. Re q .|^2 + |. Im q .| ^2 by A1,COMPLEX1:75;
end;
theorem Th48:
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 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 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 A1: for x be G_INTEG holds f.x = Norm(x);
let a, b being 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*<i>;
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 being 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 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 Lm14,A1;
hence thesis by INT_3:def 8;
end;
end;