environ
vocabularies HIDDEN, NUMBERS, FUNCOP_1, CARD_1, FUNCT_4, FUNCT_1, RELAT_1, PBOOLE, PRE_POLY, VALUED_0, XBOOLE_0, ARYTM_3, NEWTON, TARSKI, FINSET_1, NAT_3, CARD_3, UPROOTS, FINSEQ_1, SUBSET_1, ORDINAL4, ARYTM_1, XXREAL_0, FUNCT_2, CLASSES1, PARTFUN1, INT_2, NAT_1, POWER, BINOP_1, BINOP_2, REALSET1, ZFMISC_1, INT_3, SUPINF_2, FUNCT_7, ALGSTR_0, GROUP_1, MESFUNC1, INT_1, COMPLEX1, VECTSP_1, POLYNOM1, HURWITZ, POLYNOM5, POLYNOM3, POLYNOM2, AFINSQ_1, STRUCT_0, GROUP_4, GROUP_2, GRAPH_1, INT_7, XCMPLX_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, FINSET_1, RVSUM_1, CARD_1, CLASSES1, DOMAIN_1, NUMBERS, XCMPLX_0, XXREAL_0, POWER, RELAT_1, FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSEQ_1, FUNCT_4, STRUCT_0, ALGSTR_0, VFUNCT_1, GROUP_1, VECTSP_1, BINOP_1, PBOOLE, GROUP_2, ALGSEQ_1, WSIERP_1, POLYNOM3, POLYNOM4, UPROOTS, NAT_3, POLYNOM5, GROUP_4, GR_CY_1, INT_1, NAT_1, FUNCT_7, NEWTON, INT_2, INT_3, HURWITZ, VALUED_0, REALSET1, RECDEF_1, PRE_POLY, POLYNOM2;
definitions GROUP_1, REALSET1, TARSKI;
theorems TARSKI, XBOOLE_0, ZFMISC_1, ORDINAL1, FUNCT_1, FUNCT_2, VECTSP_1, INT_1, RELAT_1, RLVECT_1, ABSVALUE, GR_CY_1, FUNCT_7, NAT_1, INT_2, INT_3, PEPIN, NAT_D, XCMPLX_1, NUMBERS, PYTHTRIP, WSIERP_1, CARD_1, GROUP_1, GROUP_2, WELLORD2, XREAL_1, NEWTON, XXREAL_0, GR_CY_2, POWER, VALUED_0, ALGSEQ_1, NAT_3, UPROOTS, RVSUM_1, FINSEQ_4, FINSEQ_5, POLYNOM3, POLYNOM4, POLYNOM5, CARD_2, EULER_1, EULER_2, XBOOLE_1, FINSEQ_1, HURWITZ, GROUP_8, REALSET1, RELSET_1, FUNCT_4, FUNCOP_1, CLASSES1, PARTFUN1, PRE_POLY, FINSEQ_2, SUBSET_1;
schemes NAT_1, PRE_CIRC, FUNCT_2, RECDEF_1;
registrations XBOOLE_0, STRUCT_0, FUNCT_1, XREAL_0, ORDINAL1, NAT_1, INT_1, GROUP_1, GROUP_2, FINSET_1, FINSEQ_1, FUNCT_2, GR_CY_1, ALGSTR_0, MEMBERED, VECTSP_1, INT_3, XXREAL_0, NEWTON, SUBSET_1, RELAT_1, CARD_1, ALGSTR_1, NAT_3, VALUED_0, POLYNOM3, POLYNOM4, POLYNOM5, UPROOTS, RELSET_1, PRE_POLY, VFUNCT_1;
constructors HIDDEN, REAL_1, NAT_D, NAT_3, EUCLID, REALSET1, GROUP_4, GR_CY_1, INT_3, WSIERP_1, POLYNOM2, POLYNOM4, POLYNOM5, WELLORD2, POWER, ALGSTR_1, HURWITZ, UPROOTS, FUNCT_4, RECDEF_1, BINOP_2, CLASSES1, RELSET_1, PBOOLE, FUNCT_7, VFUNCT_1, ALGSEQ_1, BINOP_1;
requirements HIDDEN, REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities STRUCT_0, GROUP_1, INT_3, CARD_1, ALGSTR_0, BINOP_1, FINSEQ_1, POLYNOM3, HURWITZ, REALSET1, ORDINAL1;
expansions STRUCT_0, GROUP_1, HURWITZ, TARSKI;
Lm1:
for x, y being object
for X being set
for z being object st z <> x holds
((X --> 0) +* (x,y)) . z = 0
Lm2:
for p, q being bag of SetPrimes st support p c= support q & p | (support p) = q | (support p) holds
ex r being bag of SetPrimes st
( support r = (support q) \ (support p) & support p misses support r & r | (support r) = q | (support r) & p + r = q )
Lm3:
for p being bag of SetPrimes
for X being set st X c= support p holds
ex q, r being bag of SetPrimes st
( support q = (support p) \ X & support r = X & support q misses support r & q | (support q) = p | (support q) & r | (support r) = p | (support r) & q + r = p )
Lm4:
for a being Prime
for b being bag of SetPrimes st b is prime-factorization-like & a in support b holds
( a divides Product b & ex n being Nat st a |^ n divides Product b )
Lm5:
for p being FinSequence of NAT
for x being Element of NAT
for b being bag of SetPrimes st b is prime-factorization-like & p ^ <*x*> = b * (canFS (support b)) holds
ex p1 being FinSequence of NAT ex q being Prime ex n being Element of NAT ex b1 being bag of SetPrimes st
( 0 < n & b1 is prime-factorization-like & q in support b & support b1 = (support b) \ {q} & x = q |^ n & len p1 = len p & Product p = Product p1 & p1 = b1 * (canFS (support b1)) )
Lm6:
for i being Element of NAT
for f being FinSequence of NAT
for b being bag of SetPrimes
for a being Prime st len f = i & b is prime-factorization-like & Product b <> 1 & a divides Product b & Product b = Product f & f = b * (canFS (support b)) holds
a in support b
Lm7:
for a being Prime
for b being bag of SetPrimes st b is prime-factorization-like & a divides Product b holds
a in support b
Lm8:
for q being Prime
for g being Element of NAT st g <> 0 holds
ex p1 being bag of SetPrimes st
( p1 = (SetPrimes --> 0) +* (q,g) & support p1 = {q} & Product p1 = g )
Lm9:
for p being bag of SetPrimes
for x being Prime st p is prime-factorization-like & x in support p & p . x = x holds
ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = (support p) \ {x} & p1 | (support p1) = p | (support p1) & Product p = (Product p1) * x )
Lm10:
for p being bag of SetPrimes
for x being Prime st p is prime-factorization-like & x in support p & p . x <> x holds
ex p1, r1 being bag of SetPrimes st
( p1 is prime-factorization-like & support r1 = {x} & Product r1 = x & support p1 = support p & p1 | ((support p1) \ {x}) = p | ((support p1) \ {x}) & p . x = (p1 . x) * x & Product p = (Product p1) * x )
Lm11:
for n being Element of NAT
for p, q being bag of SetPrimes st p is prime-factorization-like & q is prime-factorization-like & Product p <= 2 |^ n & Product p = Product q holds
p = q
Lm12:
for p being Prime
for a, b being Element of multMagma(# (Segm0 p),(multint0 p) #)
for x, y being Element of (INT.Ring p) st a = x & y = b holds
x * y = a * b
Lm13:
for L being Field
for n being Element of NAT
for f being non-zero Polynomial of L st deg f = n holds
ex m being Element of NAT st
( m = card (Roots f) & m <= n )
Lm14:
for p being Prime
for L being Field
for n being Nat st 0 < n & L = INT.Ring p holds
ex f being Polynomial of L st
( deg f = n & ( for x being Element of L
for xz being Element of (Z/Z* p)
for xn being Element of (INT.Ring p) st x = xz & xn = xz |^ n holds
eval (f,x) = xn - (1_ (INT.Ring p)) ) )