:: Gaussian Integers :: by Yuichi Futa , Hiroyuki Okazaki , Daichi Mizushima and Yasunari Shidama :: :: Received May 19, 2013 :: Copyright (c) 2013-2018 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, NEWTON, 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, ZMODUL01, 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, VECTSP_1, GROUP_1, POLYALG1; equalities SQUARE_1, XCMPLX_0, COMPLEX1, BINOP_1, STRUCT_0, ALGSTR_0, VECTSP_1, ZMODUL01, QUOFIELD, REALSET1; expansions TARSKI, STRUCT_0, ALGSTR_0, VECTSP_1, ZMODUL01, 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 -> 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: 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+ *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+ *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+ *m proof let n, m be Integer; n in INT & m in INT by INT_1:def 2; then ex n1, m1 be Integer st n = n1 & m = m1 & F.(n,m)= n1+ *m1 by A2; hence thesis; end; now let x be object; assume x in G_INT_SET; then reconsider x1 = x as G_INTEG by Th2; A5: Re x1 in INT & Im x1 in INT by Def1; reconsider n = Re x1, m = Im x1 as Integer; A6: F.(n,m) = n+ *m by A4 .= x1 by COMPLEX1:13; [n,m] in [:INT,INT:] by A5,ZFMISC_1:87; hence x in rng F by A3,A6,FUNCT_1:3; end; then A7: G_INT_SET c= rng F; F in Funcs([:INT,INT:],G_INT_SET) by FUNCT_2:8; then ex f 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+ *m1 by A4; A13: F.x2 = F.(n2,m2) by A11 .= n2+ *m2 by A4; A14: n1 = Re(n2+ *m2) by A9,A12,A13,COMPLEX1:12 .= n2 by COMPLEX1:12; m1 = Im(n2+ *m2) by A9,A12,A13,COMPLEX1:12 .= m2 by COMPLEX1:12; hence thesis by A10,A11,A14; end; then [:INT,INT:],G_INT_SET are_equipotent by A8,A3,FUNCT_1:def 4,WELLORD2:def 4; then A15: card([:INT,INT:]) = card(G_INT_SET) by CARD_1:5; [:INT,INT:] is infinite & [:INT,INT:] is countable by CARD_4:7; then card([:INT,INT:]) = omega by CARD_3:def 15; hence thesis by CARD_3:def 15,A15; end; end; registration cluster Gauss_INT_Ring -> non degenerated; correctness; end; begin :: 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; 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 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 proof let x be Element of F_Rat; reconsider x1 = x as Rational; thus x*1.F_Rat = x1 * 1 .=x; thus 1.F_Rat *x = 1*x1 .=x; end; 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 proof let x, y be Element of F_Rat, x1, y1 be Rational; assume A1: x1 = x & y1 = y & y <> 0.F_Rat; then y" = y1" by Th15; hence x/y = x1/y1 by A1; end; 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; 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 A1: (Re(z * (z *')) = Rez * Rez - Imz * (-Imz)) & (Im(z * (z *')) = Rez * (-Imz) + Rez * Imz) by COMPLEX1:9; (z * (z *')) = (Re(z * (z *'))) + (Im(z * (z *'))*) by COMPLEX1:13 .= Re(z * (z *')) by A1; hence thesis; end; end; registration let z be G_RAT; cluster Norm(z) -> non negative; correctness proof set Rez = Re z, Imz = Im z; (Re(Rez + ((-Imz) * )) = Rez) & (Im(Rez + ((-Imz) * )) = (-Imz)) by COMPLEX1:12; then A1: (Re(z * (z *')) = Rez * Rez - Imz * (-Imz)) & (Im(z * (z *')) = Rez * (-Imz) + Rez * Imz) by COMPLEX1:9; A2: (z * (z *')) = (Re(z * (z *'))) + (Im(z * (z *'))*) by COMPLEX1:13 .= Re(z * (z *')) by A1; (Re z)^2 >= 0 & (Im z)^2 >= 0 by XREAL_1:63; hence thesis by A1,A2; end; end; registration let z be G_INTEG; cluster Norm(z) -> natural; coherence proof Re(Re z + ((-Im z) * )) = Re z & Im(Re z + ((-Im z) * )) = -Im z by COMPLEX1:12; then A1: Re(z * (z *')) = Re z * Re z - Im z * (-Im z) & Im(z * (z *')) = Re z * (-Im z) + Re z * Im z by COMPLEX1:9; A2: z * (z *') = (Re(z * (z *'))) + (Im(z * (z *'))*) by COMPLEX1:13 .= Re(z * (z *')) by A1; (Re z)^2 >= 0 & (Im z)^2 >= 0 by XREAL_1:63; then Re(z * (z *')) in NAT by A1,INT_1:3; hence thesis by A2; end; end; theorem 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 = or x = - proof let x be G_INTEG; hereby assume A1: Norm(x) = 1; A2: x = Re x+Im x* by COMPLEX1:13; A3: Norm(x) = (Re x+Im x*)*(Re x-(Im x)*) by COMPLEX1:13 .= (Re x)^2 + (Im x)^2; reconsider Rx = (Re x), Ix = (Im x) as Element of INT by Def1; Rx^2 in NAT & Ix^2 in NAT by INT_1:3,XREAL_1:63; then ((Re x)^2 = 1 & (Im x)^2 = 0) or ((Re x)^2 = 0 & (Im x)^2 = 1) by A1,A3,Th1; then ((Rx = 1 or Rx = -1) & Im x = 0) or (Re x = 0 & (Ix = 1 or Ix = -1)) by XCMPLX_1:182; hence (x = 1 or x = -1) or (x = or x = -) by A2; end; assume A4: x = 1 or x = -1 or x = or x = -; per cases by A4; suppose x = 1; hence Norm(x) = 1 by COMPLEX1:30; end; suppose x = -1; hence Norm(x) = (-1)*(-1*') by COMPLEX1:33 .= 1 by COMPLEX1:30; end; suppose x = ; hence Norm(x) = 1 by COMPLEX1:31; end; suppose x = -; hence Norm(x) = 1 by COMPLEX1:31; end; end; theorem Th36: for x be G_INTEG holds Norm(x) = 0 implies x = 0 proof let x be G_INTEG; A1: Norm(x)=(Re x+Im x*)*(Re x-(Im x)*) by COMPLEX1:13 .= (Re x)^2 + (Im x)^2; assume Norm(x) = 0; hence thesis by A1,COMPLEX1:5; end; definition let z be G_INTEG; 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 2; reconsider xx = x as G_INTEG by Th2; A4: z * x = zz * xx by A1,Th6; reconsider gintone = In(1,G_INT_SET) as G_INTEG; Norm(zz) * Norm(xx) = Norm(gintone) by A3,A4,Th34 .= 1 by COMPLEX1:30; hence zz is g_int_unit by NAT_1:15; end; assume A5: zz is g_int_unit; ex w 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 = ; reconsider w = - as Element of Gauss_INT_Ring by Th3; take w; thus 1.Gauss_INT_Ring = *(-) .= z * w by A8,Th6; end; suppose A9: z = -; reconsider w = as Element of Gauss_INT_Ring by Lm2; take w; thus 1.Gauss_INT_Ring = (-)* .= z * w by A9,Th6; end; end; hence z is unital by GCD_1:def 1,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)*; now per cases by A2,Th35; suppose d = 1; then (Im x) = (- Im x) by A2,A3,COMPLEX1:12; hence contradiction by A1; end; suppose d = -1; then (Re x) = (Re (-x*')) by A2 .= - Re (x*') by COMPLEX1:17 .= - ( Re x) by COMPLEX1:12,A3; hence contradiction by A1; end; suppose d = ; then (Im x) = Im (*Re x+ (- Im x)**) by A2 .= Re x by COMPLEX1:12; hence contradiction by A1; end; suppose d = -; then (Im x) = Im (*(-Re x)+ (Im x)*(-1r)) by A2 .= - Re x by COMPLEX1:12; hence contradiction by A1; end; end; hence contradiction; end; theorem 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*)*(Re q-(Im q)*) by COMPLEX1:13 .= (Re q)^2 + (Im q)^2; assume A4: not (Re q <> 0 & Im q <> 0 & Re q <> Im q & - Re q <> Im q ); per cases by A4; suppose Re q = 0; hence contradiction by A1,A3,Lm11; end; suppose Im q = 0; hence contradiction by A1,A3,Lm11; end; suppose A5: Re q = Im q; then A6: Norm(q) = 2*(Re q)*(Re q) by A3; |.Re q.| <> 1 by A1,A3,A5,A2; hence contradiction by A1,A6,Lm12; end; suppose A7: - Re q = Im q; then A8: Norm(q) = 2*(Re q)*(Re q) by A3; |.Re q.| <> 1 by A1,A3,A7,A2; hence contradiction by A1,A8,Lm12; end; end; theorem 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*)*(Re q-(Im q)*) by COMPLEX1:13 .= (Re q)^2 + (Im q)^2 .= |. Re q .|^2 + |. Im q .| ^2 by A1,COMPLEX1:75; end; theorem 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*; 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;