environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions TARSKI, XBOOLE_0, STRUCT_0, ALGSTR_0, VECTSP_1, GROUP_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;
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;
constructors HIDDEN, 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;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
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;
theorem Th1:
for
x,
y being
Nat holds
( not
x + y = 1 or (
x = 1 &
y = 0 ) or (
x = 0 &
y = 1 ) )
Lm1:
for z being Complex st Re z is integer & Im z is integer holds
z is g_integer
by INT_1:def 2;
Lm2:
<i> in G_INT_SET
;
LmX:
- (1. INT.Ring) = - 1
by INT_3:def 3;
Lm3:
Gauss_INT_Module is Z_Module
Lm4:
Gauss_INT_Ring is Ring
registration
correctness
coherence
( AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is strict & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is Abelian & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is add-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_zeroed & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_complementable & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is commutative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right_unital & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is right-distributive & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is mix-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is scalar-associative & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is vector-distributive & AlgebraStr(# G_INT_SET,g_int_add,g_int_mult,(In (0,G_INT_SET)),(In (1,G_INT_SET)),Sc_Mult #) is scalar-distributive );
end;
Lm5:
for x1, y1, x2, y2 being G_INTEG
for u1, u2 being Element of Q. Gauss_INT_Ring st y1 <> 0 & y2 <> 0 & u1 = [x1,y1] & u2 = [x2,y2] holds
( x1 / y1 = x2 / y2 iff QClass. u1 = QClass. u2 )
Lm6:
addreal || RAT = addrat
Lm7:
multreal || RAT = multrat
set K = F_Rat ;
set C = the carrier of F_Rat;
Lm8:
( Gauss_RAT_Module is scalar-distributive & Gauss_RAT_Module is vector-distributive & Gauss_RAT_Module is scalar-associative & Gauss_RAT_Module is scalar-unital & Gauss_RAT_Module is add-associative & Gauss_RAT_Module is right_zeroed & Gauss_RAT_Module is right_complementable & Gauss_RAT_Module is Abelian )
Lm9:
Gauss_RAT_Ring is Field
Lm10:
for x, y being G_INTEG st x is_associated_to y holds
Norm x = Norm y
Lm11:
for a being Integer holds a * a is not Prime
Lm12:
for a being Integer st |.a.| <> 1 holds
not (2 * a) * a is Prime
Lm13:
ex f being Function of Gauss_INT_Ring,NAT st
for x being G_INTEG holds f . x = Norm x
Lm14:
for f being Function of Gauss_INT_Ring,NAT st ( for x being G_INTEG holds f . x = Norm x ) holds
for a, b being Element of Gauss_INT_Ring st b <> 0. Gauss_INT_Ring holds
ex q, r being Element of Gauss_INT_Ring st
( a = (q * b) + r & ( r = 0. Gauss_INT_Ring or f . r < f . b ) )