:: Uniqueness of factoring an integer and multiplicative group $Z/pZ^{*}$
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received January 31, 2008
:: Copyright (c) 2008 Association of Mizar Users
environ
vocabularies BOOLE, TARSKI, BINOP_1, INT_1, CARD_1, FUNCT_1, VECTSP_1,
RELAT_1, ARYTM_1, GR_CY_1, FUNCT_7, RLVECT_1, ABSVALUE, NAT_1, NAT_3,
ARYTM_3, INT_2, ORDINAL2, NAT_LAT, ALGSTR_0, INT_3, ARYTM, GROUP_1,
GROUP_2, GROUP_4, PBOOLE, POWER, INT_7, REALSET1, COMPLEX1, FINSET_1,
GRAPH_1, FINSEQ_4, RFINSEQ, FINSEQ_1, POLYNOM1, POLYNOM2, ALGSEQ_1,
POLYNOM3, POLYNOM5, SQUARE_1, SGRAPH1, SEQ_1, FUNCT_2, HURWITZ, FILTER_0,
CARD_3, UPROOTS, VALUED_0, FUNCT_4, FUNCOP_1, ANPROJ_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, FINSET_1, RVSUM_1,
CARD_1, DOMAIN_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, POWER, RELAT_1,
FUNCT_1, RELSET_1, PARTFUN1, FUNCT_2, FUNCOP_1, FINSEQ_1, POLYNOM1,
FUNCT_4, STRUCT_0, ALGSTR_0, RLVECT_1, GROUP_1, VECTSP_1, BINOP_1,
RFINSEQ, PBOOLE, GROUP_2, BHSP_1, ALGSEQ_1, POLYNOM2, WSIERP_1, POLYNOM3,
POLYNOM4, UPROOTS, NAT_3, POLYNOM5, GROUP_4, GR_CY_1, INT_1, FUNCT_7,
NEWTON, INT_2, INT_3, HURWITZ, VALUED_0, REALSET1, RECDEF_1;
constructors REAL_1, NAT_D, NAT_3, SEQ_1, PEPIN, EUCLID, REALSET1, GROUP_4,
GR_CY_1, INT_3, WSIERP_1, BINARITH, BHSP_1, POLYNOM2, POLYNOM4, POLYNOM5,
WELLORD2, POWER, RFINSEQ, ALGSTR_1, HURWITZ, UPROOTS, FUNCT_4, 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, POLYNOM1, NAT_3, VALUED_0, POLYNOM3, POLYNOM4, POLYNOM5,
UPROOTS;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions STRUCT_0, GROUP_1, INT_3, CARD_1, ALGSTR_0, BINOP_1, FINSEQ_1,
POLYNOM3, HURWITZ, 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, CARD_4, STRUCT_0, WELLORD2, XREAL_1, NEWTON, XXREAL_0,
GR_CY_2, POWER, VALUED_0, ALGSEQ_1, POLYNOM1, NAT_3, PBOOLE, UPROOTS,
RVSUM_1, RFINSEQ, BAGORDER, FINSEQ_4, FINSEQ_5, POLYNOM3, POLYNOM4,
POLYNOM5, CARD_2, EULER_1, EULER_2, XBOOLE_1, FINSET_1, FINSEQ_1,
HURWITZ, GROUP_8, REALSET1, RELSET_1, FUNCT_4, FUNCOP_1;
schemes NAT_1, PRE_CIRC, FUNCT_2, RECDEF_1;
begin :: Uniqueness of factoring an integer
reserve x,X,y for set;
Lm1: for z be set st z<> x holds (X-->0)+*(x,y).z=0
proof
let z be set;
assume
A1: z <>x;
A2: dom (X-->0)=X by FUNCOP_1:19;
per cases;
suppose
A3: z in X;
(X-->0)+*(x,y).z=(X--> 0).z by A1,FUNCT_7:34
.=0 by A3,FUNCOP_1:13;
hence thesis;
end;
suppose
A4: not z in X;
(X-->0)+*(x,y).z=(X--> 0).z by A1,FUNCT_7:34
.=0 by A2,A4,FUNCT_1:def 4;
hence thesis;
end;
end;
theorem Th1:
for p being ManySortedSet of X st support p = {x} holds p = (X-->0)+*(x,p.x)
proof
let p be ManySortedSet of X;
assume
A1: support p = {x};
dom ((X-->0)+*(x,p.x)) = dom (X-->0) by FUNCT_7:32
.= X by FUNCOP_1:19;
then
A2: dom p = dom ((X-->0)+*(x,p.x)) by PBOOLE:def 3;
for y st y in dom p holds p.y=(X-->0)+*(x,p.x).y
proof
let y be set;
assume y in dom p;
then y in X by PBOOLE:def 3;
then
A3: y in dom (X-->0) by FUNCOP_1:19;
per cases;
suppose x=y;
hence thesis by A3,FUNCT_7:33;
end;
suppose
A4: x<>y;
then not y in support p by A1,TARSKI:def 1;
then p.y=0 by POLYNOM1:def 7;
hence thesis by A4,Lm1;
end;
end;
hence thesis by A2,FUNCT_1:9;
end;
theorem Th2:
for X be set,p,q,r be real-valued ManySortedSet of X
st (support p) /\ (support q) = {} & (support p) \/ (support q) =(support r)
& p|(support p) = r | (support p) & q|(support q) = r | (support q) holds
p+q = r
proof
let X be set, p,q,r be real-valued ManySortedSet of X;
assume
A1: (support p) /\ (support q) = {} & (support p) \/ (support q) =(support r)
& p|(support p) = r | (support p) & q|(support q) = r | (support q);
for x being set st x in X holds r.x=p.x+q.x
proof
let x being set;
assume x in X;
per cases;
suppose
A2: x in (support p) \/ (support q);
now per cases by A2,XBOOLE_0:def 2;
suppose
A3: x in support p;
then
A4: not x in support q by A1,XBOOLE_0:def 3;
thus r.x=r|(support p).x by A3,FUNCT_1:72
.=p.x +0 by A1,A3,FUNCT_1:72
.=p.x + q.x by A4,POLYNOM1:def 7;
end;
suppose
A5: x in (support q);
then
A6: not x in support p by A1,XBOOLE_0:def 3;
thus r.x=r|(support q).x by A5,FUNCT_1:72
.=0 +q.x by A1,A5,FUNCT_1:72
.=p.x + q.x by A6,POLYNOM1:def 7;
end;
end;
hence r.x=p.x + q.x;
end;
suppose
A7: not x in (support p) \/ (support q);
then
A8: not x in (support p) & not x in (support q) by XBOOLE_0:def 2;
thus r.x = 0 by A1,A7,POLYNOM1:def 7
.= 0 + q.x by A8,POLYNOM1:def 7
.=p.x+q.x by A8,POLYNOM1:def 7;
end;
end;
hence r=p+q by POLYNOM1:37;
end;
theorem Th3:
for X be set,p,q be ManySortedSet of X
st p|(support p) = q|(support q) holds p = q
proof
let X be set,p,q be ManySortedSet of X;
assume
A1: p|(support p) = q| (support q);
A2: dom (p| (support p)) = dom p /\ (support p) by FUNCT_1:68
.=support p by POLYNOM1:41,XBOOLE_1:28;
A3: dom (q| (support q)) =dom q /\ (support q) by FUNCT_1:68
.=support q by POLYNOM1:41,XBOOLE_1:28;
A4: for x being set st x in X holds p.x=q.x
proof
let x being set;
assume x in X;
per cases;
suppose
A5: x in support p;
thus p.x=p|(support p).x by A5,FUNCT_1:72
.=q.x by A1,A2,A3,A5,FUNCT_1:72;
end;
suppose
A6: not x in support p;
thus p.x = 0 by A6,POLYNOM1:def 7
.=q.x by A1,A2,A3,A6,POLYNOM1:def 7;
end;
end;
dom p = X& dom q = X by PBOOLE:def 3;
hence thesis by A4,FUNCT_1:9;
end;
theorem Th4:
for X be set,p,q be bag of X st support p = {} & support q={} holds p = q
proof
let X be set,p,q be bag of X;
assume
A1: support p = {} & support q={};
A2: dom (p| (support p)) =dom p /\ (support p) by FUNCT_1:68
.= {} by A1;
A3: {} = dom q /\ {}
.= dom (q| (support q)) by A1,FUNCT_1:68;
A4: for x be set st x in dom (p| (support p))
holds (p| (support p)).x = (q| (support q)).x by A2;
p| (support p) = q| (support q) by A2,A3,A4,FUNCT_1:9;
hence p = q by Th3;
end;
Lm2: for p,q be bag of SetPrimes
st (support p) c= (support q) & p | (support p)=q | (support p) holds
ex r be bag of SetPrimes st (support r) = (support q) \ (support p) &
(support p) misses (support r) & r | (support r) = q | (support r) & p+r = q
proof
let p,q be bag of SetPrimes;
assume
A1: (support p) c= (support q) & p | (support p) =q | (support p);
defpred C[set] means $1 in (support q) \ (support p);
deffunc F(set) = q.$1;
deffunc G(set) = 0;
A2: for x be set st x in SetPrimes holds
(C[ x] implies F(x) in NAT) & (not C[ x] implies G(x) in NAT);
consider f being Function of SetPrimes,NAT such that
A3: for x be set st x in SetPrimes holds
(C[ x] implies f.x = F(x)) & (not C[ x] implies f.x = G(x))
from FUNCT_2:sch 5(A2);
A4: for x be set st x in SetPrimes holds
x in (support q) \ (support p) implies f.x<>0
proof
let x be set;
assume
A5: x in SetPrimes & x in (support q) \ (support p);
then x in support q by XBOOLE_0:def 4;
then q.x<>0 by POLYNOM1:def 7;
hence thesis by A3,A5;
end;
A6: for x being set st not x in SetPrimes holds f.x=0
proof
let x be set;
assume not x in SetPrimes;
then not x in dom f;
hence thesis by FUNCT_1:def 4;
end;
A7: for x being set holds x in (support q) \ (support p) iff f.x<>0
proof
let x be set;
per cases;
suppose x in SetPrimes;
hence thesis by A3,A4;
end;
suppose not x in SetPrimes;
hence thesis by A6;
end;
end;
A8: (support f)=(support q) \ (support p) by A7,POLYNOM1:def 7;
A9: (support p) misses (support f)
proof
assume (support p) meets (support f);
then consider x be set such that
A10: x in support p & x in support f by XBOOLE_0:3;
thus contradiction by A8,A10,XBOOLE_0:def 4;
end;
then
A11: (support p) /\ (support f) = {} by XBOOLE_0:def 7;
A12: f | (support f) =q | (support f)
proof
A13: dom (f|(support f)) =(dom f)/\ support f by FUNCT_1:68
.=support f by POLYNOM1:41,XBOOLE_1:28;
A14: dom (q|(support f)) =(dom q)/\ support f by FUNCT_1:68
.=(dom q)/\ ((support q) \ (support p)) by A7,POLYNOM1:def 7
.= ((dom q)/\ (support q)) \ (support p) by XBOOLE_1:49
.= (support q) \ (support p) by POLYNOM1:41,XBOOLE_1:28
.=support f by A7,POLYNOM1:def 7;
for x be set st x in dom (f|(support f))
holds (f|(support f)).x =(q|(support f)).x
proof
let x be set;
assume
A15: x in dom (f|(support f));
then (f|(support f)).x=f.x & (q|(support f)).x=q.x by A13,FUNCT_1:72;
hence thesis by A3,A8,A13,A15;
end;
hence thesis by A13,A14,FUNCT_1:def 17;
end;
A16: support f is finite by A7,POLYNOM1:def 7;
A17: dom f = SetPrimes
proof
f in Funcs(SetPrimes,NAT) by FUNCT_2:11;
hence thesis by FUNCT_2:169;
end;
reconsider r = f as bag of SetPrimes by A16,A17,PBOOLE:def 3,POLYNOM1:def 8;
(support p) \/ (support r)
=(support p) \/ ((support q) \ (support p)) by A7,POLYNOM1:def 7
.=(support p) \/ (support q) by XBOOLE_1:39
.=(support q) by A1,XBOOLE_1:12;
then p+r = q by A1,A11,A12,Th2;
hence thesis by A8,A9,A12;
end;
Lm3: for p be bag of SetPrimes, X be set st X c= (support p) holds
ex q,r be 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
proof
let p be bag of SetPrimes,X be set;
assume
A1: X c= (support p);
defpred C[set] means $1 in X;
deffunc F(set) = p.$1;
deffunc G(set) = 0;
set fq =p +* (X --> 0);
A2: dom(X --> 0) = X by FUNCOP_1:19;
then
A3: dom fq = dom p \/ X by FUNCT_4:def 1
.= SetPrimes \/ X by PBOOLE:def 3
.= SetPrimes by A1,XBOOLE_1:1,12;
A4: rng p c= NAT by VALUED_0:def 6;
A5: rng p \/ rng(X --> 0) c= NAT by A4,XBOOLE_1:8;
rng fq c= rng p \/ rng(X --> 0) by FUNCT_4:18;
then rng fq c= NAT by A5,XBOOLE_1:1;
then reconsider fq as Function of SetPrimes,NAT
by A3,FUNCT_2:def 1,RELSET_1:11;
A6: x in X implies fq.x = 0
proof
assume
A7: x in X;
hence fq.x = (X --> 0).x by A2,FUNCT_4:14
.= 0 by A7,FUNCOP_1:13;
end;
set fr = p +* (SetPrimes \X -->0);
A8: dom fr = dom p \/ dom (SetPrimes \ X -->0) by FUNCT_4:def 1
.=dom p \/ (SetPrimes \ X) by FUNCOP_1:19
.= SetPrimes \/ (SetPrimes \X) by PBOOLE:def 3
.= SetPrimes by XBOOLE_1:12,36;
A9: rng p \/ rng(SetPrimes \X --> 0) c= NAT by A4,XBOOLE_1:8;
rng fr c= rng p \/ rng(SetPrimes \ X --> 0) by FUNCT_4:18;
then rng fr c= NAT by A9,XBOOLE_1:1;
then reconsider fr as Function of SetPrimes,NAT
by A8,FUNCT_2:def 1,RELSET_1:11;
A10: x in X implies fr.x =p.x
proof
assume
A11: x in X;
not x in dom(SetPrimes \ X --> 0) by A11,XBOOLE_0:def 4;
hence thesis by FUNCT_4:12;
end;
A12: not x in X & x in SetPrimes implies fr.x = 0
proof
assume not x in X & x in SetPrimes;
then
A13: x in SetPrimes \ X by XBOOLE_0:def 4;
then x in dom(SetPrimes \ X --> 0) by FUNCOP_1:19;
then fr.x = (SetPrimes \ X --> 0).x by FUNCT_4:14;
hence thesis by A13,FUNCOP_1:13;
end;
A14: for x be set st x in SetPrimes & x in X holds fr.x<>0
proof
let x be set;
assume
A15: x in SetPrimes & x in X;
then p.x<>0 by A1,POLYNOM1:def 7;
hence thesis by A10,A15;
end;
A16: for x being set st not x in SetPrimes holds fr.x=0 &fq.x=0
proof
let x be set;
assume not x in SetPrimes;
then not x in dom fq ¬ x in dom fr;
hence thesis by FUNCT_1:def 4;
end;
A17: for x being set holds x in X iff fr.x<>0
proof
let x be set;
now per cases;
suppose x in SetPrimes;
hence thesis by A12,A14;
end;
suppose
A18: not x in SetPrimes;
X c= SetPrimes by A1,XBOOLE_1:1;
hence thesis by A16,A18;
end;
end;
hence thesis;
end;
then
A19: (support fr) = X by POLYNOM1:def 7;
A20: for x be set holds x in (support p) \ X iff fq.x<>0
proof
let x be set;
per cases;
suppose x in X;
hence thesis by A6,XBOOLE_0:def 4;
end;
suppose
A21: not x in X;
then
A22: fq.x=p.x by A2,FUNCT_4:12;
per cases;
suppose x in support p;
hence thesis by A21,A22,POLYNOM1:def 7,XBOOLE_0:def 4;
end;
suppose not x in support p;
hence thesis by A22,POLYNOM1:def 7,XBOOLE_0:def 4;
end;
end;
end;
A23: support fq = support p \ X by A20,POLYNOM1:def 7;
A24: (support fq) /\ (support fr) = {}
proof
(support p \ X) misses X by XBOOLE_1:79;
hence thesis by A19,A23,XBOOLE_0:def 7;
end;
then
A25: (support fq) misses (support fr) by XBOOLE_0:def 7;
A26: fq|(support fq)=p|(support fq)
proof
A27: dom (fq|(support fq)) =(dom fq)/\ support fq by FUNCT_1:68
.=support fq by POLYNOM1:41,XBOOLE_1:28;
A28: dom (p|(support fq)) =(dom p)/\ support fq by FUNCT_1:68
.=(dom p)/\ (support p \ X) by A20,POLYNOM1:def 7
.= ((dom p)/\ (support p)) \ X by XBOOLE_1:49
.= (support p) \ X by POLYNOM1:41,XBOOLE_1:28
.=support fq by A20,POLYNOM1:def 7;
A29: for x be set st x in SetPrimes & x in (support fq) holds p.x=fq.x
proof
let x be set;
assume x in SetPrimes & x in (support fq);
then not x in X by A19,A24,XBOOLE_0:def 3;
hence thesis by A2,FUNCT_4:12;
end;
for x be set st x in dom (fq|(support fq))
holds (fq|(support fq)).x =(p|(support fq)).x
proof
let x be set;
assume
A30: x in dom (fq|(support fq));
then (fq|(support fq)).x=fq.x &
(p|(support fq)).x=p.x by A27,FUNCT_1:72;
hence thesis by A27,A29,A30;
end;
hence thesis by A27,A28,FUNCT_1:def 17;
end;
A31: fr | (support fr) =p | (support fr)
proof
A32: support fr c= dom fr & support p c= dom p by POLYNOM1:41;
A33: dom (fr|(support fr)) =(dom fr)/\ support fr by FUNCT_1:68
.=support fr by POLYNOM1:41,XBOOLE_1:28
.= X by A17,POLYNOM1:def 7;
A34: dom (p|(support fr)) =(dom p)/\ support fr by FUNCT_1:68
.=(dom p)/\ X by A17,POLYNOM1:def 7
.=X by A1,A32,XBOOLE_1:1,28;
for x be set st x in dom (fr|(support fr))
holds (fr|(support fr)).x =(p|(support fr)).x
proof
let x be set;
assume
A35: x in dom (fr|(support fr));
then (fr|(support fr)).x=fr.x &
(p|(support fr)).x=p.x by A19,A33,FUNCT_1:72;
hence thesis by A10,A33,A35;
end;
hence thesis by A33,A34,FUNCT_1:def 17;
end;
A36: support fq is finite & support fr is finite
by A1,A19,A20,FINSET_1:13,POLYNOM1:def 7;
A37: dom fr = SetPrimes
proof
fr in Funcs(SetPrimes,NAT) by FUNCT_2:11;
hence thesis by FUNCT_2:169;
end;
reconsider q = fq as bag of SetPrimes by A3,A23,PBOOLE:def 3,POLYNOM1:def 8;
reconsider r = fr as bag of SetPrimes by A36,A37,PBOOLE:def 3
,POLYNOM1:def 8;
(support fr) \/ (support fq)
=(support fr) \/(support p \ support fr) by A17,A23,POLYNOM1:def 7
.=(support fr) \/(support p) by XBOOLE_1:39
.= support p by A1,A19,XBOOLE_1:12;
then q+r=p by A24,A26,A31,Th2;
hence thesis by A19,A23,A25,A26,A31;
end;
definition
let p be bag of SetPrimes;
attr p is prime-factorization-like means
:Def1:
for x being Prime st x in support p
ex n be natural number st 0 < n & p.x = x |^n;
end;
registration
let n be non empty natural number;
cluster ppf n -> prime-factorization-like;
coherence
proof
let p be Prime;
assume
A1: p in support ppf n;
then
A2: p in support pfexp n by NAT_3:def 9;
take k=p |-count n;
p |-count n <>0
proof
assume p |-count n =0;
then (ppf n).p=0 by NAT_3:55;
hence contradiction by A1,POLYNOM1:def 7;
end;
hence thesis by A2,NAT_3:def 9;
end;
end;
theorem Th5:
for p,q be Prime,n,m be natural number
st p divides m*(q|^n) & p <> q holds p divides m
proof
let p,q be Prime;
let n,m be natural number;
assume
A1: p divides m*(q|^n) & p <> q;
p divides m or p divides (q|^n) by A1,NEWTON:98;
hence thesis by A1,NAT_3:6;
end;
Lm4: for a be Prime, b be bag of SetPrimes
st b is prime-factorization-like & a in support b holds a divides Product b &
ex n be natural number st a|^n divides Product b
proof
let a be Prime, b be bag of SetPrimes;
assume
A1: b is prime-factorization-like & a in support b;
consider f being FinSequence of COMPLEX such that
A2: Product b = Product f & f = b*canFS(support b) by NAT_3:def 5;
A3: rng b c= NAT by VALUED_0:def 6;
rng f c= rng b by A2,RELAT_1:45;
then rng f c= NAT by A3,XBOOLE_1:1;
then
reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
A4: support b c= dom b by POLYNOM1:41;
rng canFS(support b) = support b by UPROOTS:5;
then
A5: dom f = dom canFS(support b) by A2,A4,RELAT_1:46;
A6: a in rng canFS(support b) by A1,UPROOTS:5;
consider n be natural number such that
A7: 0 < n & b.a = a |^n by A1,Def1;
consider d be set such that
A8: d in dom canFS(support b) & a=(canFS(support b)).d by A6,FUNCT_1:def 5;
b.a=(b*(canFS(support b))).d by A2,A5,A8,FUNCT_1:22;
then b.a in rng f by A2,A5,A8,FUNCT_1:12;
then
A9: (a |^n) divides (Product f) by A7,NAT_3:7;
a divides b.a by A7,NAT_3:3;
hence thesis by A2,A7,A9,NAT_D:4;
end;
Lm5: for p be FinSequence of NAT,x be Element of NAT, b be bag of SetPrimes
st b is prime-factorization-like & (p^<*x*>) = b*canFS(support b) holds
ex p1 being FinSequence of NAT, q be Prime,n be Element of NAT,
b1 be 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)
proof
let p be FinSequence of NAT,x be Element of NAT, b be bag of SetPrimes;
assume
A1: b is prime-factorization-like & ( p^<*x*>) = b*canFS(support b);
p = (b*canFS(support b))| (dom p) by A1,FINSEQ_1:33;
then
A2: dom p = dom (b*canFS(support b)) /\ (dom p) by FUNCT_1:68;
A3: rng canFS(support b) = support b by UPROOTS:5;
dom b = SetPrimes by PBOOLE:def 3;
then
A4: dom (b*canFS(support b)) = dom (canFS(support b)) by A3,RELAT_1:46;
A5: rng canFS(support b) =support b by UPROOTS:5;
A6: len <*x*> = 1 by FINSEQ_1:57;
then
A7: len (p^<*x*>) = len p + 1 by FINSEQ_1:35;
len p + 1 in Seg (len p + 1) by FINSEQ_1:6;
then
A8: (len p + 1) in dom (b*canFS(support b)) by A1,A7,FINSEQ_1:def 3;
A9: x =(p^<*x*>) .(len p + 1) by FINSEQ_1:59
.= b.((canFS(support b)).(len p + 1)) by A1,A4,A8,FUNCT_1:23;
A10: (canFS(support b)).(len p + 1) in support b by A4,A5,A8,FUNCT_1:12;
then
reconsider q=(canFS(support b)).(len p + 1) as Prime by NEWTON:def 6;
consider n be natural number such that
A11: 0 < n & b.q = q |^n by A1,A10,Def1;
reconsider n as Element of NAT by ORDINAL1:def 13;
defpred P[set] means $1 in support b \ {q};
deffunc F(set) = b.$1;
deffunc G(set) = 0;
consider b1 being ManySortedSet of SetPrimes such that
A12: for i being Element of SetPrimes st i in SetPrimes
holds (P[i] implies b1.i = F(i)) & (not P[i] implies b1.i = G(i))
from PRE_CIRC:sch 2;
A13: support b1 = (support b) \ {q}
proof
now
let z be set;
assume
A14: z in support b1;
z in dom b1
proof
assume not z in dom b1;
then b1.z = {} by FUNCT_1:def 4;
hence contradiction by A14,POLYNOM1:def 7;
end;
then
reconsider y = z as Element of SetPrimes by PBOOLE:def 3;
A15: b1.y <> 0 by A14,POLYNOM1:def 7;
assume not z in (support b) \ {q};
hence contradiction by A12,A15;
end;
then
A16: support b1 c= (support b) \ {q} by TARSKI:def 3;
now
let z be set;
assume
A17: z in (support b) \ {q};
then
A18: z in support b by XBOOLE_0:def 4;
reconsider y = z as Element of SetPrimes by A17;
b1.y =b.y by A12,A17;
then
b1. y <> 0 by A18,POLYNOM1:def 7;
hence z in support b1 by POLYNOM1:def 7;
end;
then
(support b) \ {q} c= support b1 by TARSKI:def 3;
hence thesis by A16,XBOOLE_0:def 10;
end;
rng b1 c= NAT
proof
let y be set;
assume y in rng b1;
then consider x be set such that
A19: x in dom b1 & y=b1.x by FUNCT_1:def 5;
reconsider x as Element of SetPrimes by A19,PBOOLE:def 3;
b1.x in NAT
proof
per cases;
suppose x in support b \ {q};
then b1.x = b.x by A12;
hence b1.x in NAT;
end;
suppose not x in support b \ {q};
then b1.x = 0 by A12;
hence b1.x in NAT;
end;
end;
hence y in NAT by A19;
end;
then
reconsider b1 as bag of SetPrimes by A13,POLYNOM1:def 8,VALUED_0:def 6;
A20: now
let x be Prime;
assume
A21: x in support b1;
support b \ {q} c= support b by XBOOLE_1:36;
then consider m be natural number such that
A22: 0 < m & b.x = x |^m by A1,A13,A21,Def1;
take m;
thus 0 < m by A22;
thus b1.x=x |^m by A12,A13,A21,A22;
end;
dom b = SetPrimes by PBOOLE:def 3;
then
dom (b*canFS(support b)) = dom (canFS(support b)) by A3,RELAT_1:46;
then
A23: dom ((canFS(support b)) | (dom p)) = dom p by A2,RELAT_1:91,XBOOLE_1:17;
A24: SetPrimes = dom b by PBOOLE:def 3;
A25: rng canFS(support b) =support b by UPROOTS:5;
A26: card dom (b*canFS(support b))
=card dom (canFS(support b)) by A24,A25,RELAT_1:46
.=card Seg len (canFS(support b)) by FINSEQ_1:def 3
.= card len (canFS(support b)) by FINSEQ_1:76
.= len (canFS(support b));
A27: len canFS(support b) = card Seg len ((p^<*x*>)) by A1,A26,FINSEQ_1:def 3
.= card len ((p^<*x*>)) by FINSEQ_1:76
.= len p + 1 by A6,FINSEQ_1:35;
A28: dom canFS(support b1) = dom p
proof
A29: card( (support b) \ {q})
=card( (support b)) - card({q}) by A4,A5,A8,EULER_1:5,FUNCT_1:12
.=card( (support b)) - 1 by CARD_1:79;
A30: card (support b) = len canFS(support b) by UPROOTS:def 1;
len (canFS(support b1)) =len p by A13,A27,A29,A30,UPROOTS:def 1;
then dom (canFS(support b1)) = Seg len p by FINSEQ_1:def 3;
hence thesis by FINSEQ_1:def 3;
end;
per cases;
suppose
A31: dom p = {};
set p1=b1*canFS(support b1);
A32: p = {} by A31,RELAT_1:64;
Seg len canFS(support b1) = dom canFS(support b1) by FINSEQ_1:def 3
.= Seg len p by A28,FINSEQ_1:def 3
.= Seg 0 by A32,CARD_1:47;
then len canFS(support b1) = 0 by FINSEQ_1:8;
then
A33: p1 = b1*{} by CARD_2:59
.= <*>NAT;
then reconsider p1 as FinSequence;
reconsider p1 as FinSequence of NAT by A33;
take p1,q,n,b1;
thus thesis
by A4,A5,A8,A9,A11,A13,A20,A31,A33,Def1,RELAT_1:64,FUNCT_1:12;
end;
suppose
A34: dom p <> {};
A35: (support b) \ {q} <> {}
proof
assume (support b) \ {q} = {};
then
A36: rng canFS(support b1) = {} by A13,UPROOTS:5;
dom p ={}
proof
assume dom p <> {};
then consider x be set such that
A37: x in dom p by XBOOLE_0:def 1;
thus contradiction by A28,A36,A37,FUNCT_1:12;
end;
hence contradiction by A34;
end;
A38: rng ((canFS(support b)) | (dom p))= ((support b) \ {q})
proof
now
let y be set;
assume y in rng ((canFS(support b)) | (dom p));
then
consider x be set such that
A39: x in dom ((canFS(support b)) | (dom p))
& y=((canFS(support b)) | (dom p)).x by FUNCT_1:def 5;
A40: y= (canFS(support b)).x by A39,FUNCT_1:70;
A41: x in dom (canFS(support b)) /\ (dom p) by A39,FUNCT_1:68;
then
A42: x in dom (canFS(support b)) by XBOOLE_0:def 3;
A43: x in dom p by A41,XBOOLE_0:def 3;
A44: y in rng (canFS(support b)) by A40,A42,FUNCT_1:12;
A45: (canFS(support b)) is one-to-one by UPROOTS:4;
y <> q
proof
assume
A46: y=q;
len p + 1 in Seg (len p + 1) by FINSEQ_1:6;
then len p + 1 in dom canFS(support b) by A27,FINSEQ_1:def 3;
then len p+1 = x by A40,A42,A45,A46,FUNCT_1:def 8;
then
A47: len p + 1 in Seg len p by A43,FINSEQ_1:def 3;
len p + 0 < 1+ len p by XREAL_1:10;
hence contradiction by A47,FINSEQ_1:3;
end;
then
not y in {q} by TARSKI:def 1;
hence y in (support b) \ {q} by A44,XBOOLE_0:def 4;
end;
then
A48: rng ((canFS(support b)) | (dom p)) c= ((support b) \ {q})
by TARSKI:def 3;
A49: rng canFS(support b) = support b by UPROOTS:5;
now
let y be set;
assume
A50: y in ((support b) \ {q});
then y in rng canFS(support b) by A49,XBOOLE_0:def 4;
then consider x be set such that
A51: x in dom (canFS(support b)) & y=(canFS(support b)).x by FUNCT_1:def 5;
A52: x in dom p
proof
assume not x in dom p;
then
A53: not x in Seg len p by FINSEQ_1:def 3;
A54: x in Seg (len p + 1) by A27,A51,FINSEQ_1:def 3;
reconsider x as Element of NAT by A51;
A55: 1 <=x & x <= len p + 1 by A54,FINSEQ_1:3;
len p < x by A53,A55;
then len p+ 1 <= x by NAT_1:13;
then x = len p + 1 by A55,XXREAL_0:1;
then y in {q} by A51,TARSKI:def 1;
hence contradiction by A50,XBOOLE_0:def 4;
end;
then
A56: y = ((canFS(support b)) | (dom p)).x by A51,FUNCT_1:72;
x in dom (canFS(support b)) /\ (dom p) by A51,A52,XBOOLE_0:def 3;
then
x in dom ((canFS(support b)) | (dom p)) by FUNCT_1:68;
hence y in rng ((canFS(support b)) | (dom p)) by A56,FUNCT_1:12;
end;
then
((support b) \ {q}) c= rng ((canFS(support b)) | (dom p))
by TARSKI:def 3;
hence thesis by A48,XBOOLE_0:def 10;
end;
reconsider L0=
(canFS(support b)) | (dom p) as Function of (dom p),((support b) \ {q})
by A23,A38,FUNCT_2:3;
A57: rng L0 = (support b) \ {q} & dom L0 = dom p by A35,A38,FUNCT_2:def 1;
A58: canFS(support b) is one-to-one by UPROOTS:4;
A59: canFS(support b1) is one-to-one by UPROOTS:4;
A60: L0 is one-to-one by A58,FUNCT_1:84;
then L0" is one-to-one by FUNCT_1:62;
then
A61: L0"*canFS(support b1) is one-to-one by A59,FUNCT_1:46;
L0 is one-to-one by A58,FUNCT_1:84;
then
A62: dom (L0") = (support b) \ {q} & rng (L0") = dom p by A57,FUNCT_1:55;
then
reconsider LL1 = L0" as Function of (support b) \ {q},dom p by FUNCT_2:3;
A63: rng canFS(support b1) =support b1 by UPROOTS:5;
canFS(support b1) is Function of (dom p),(support b) \ {q}
by A13,A28,A63,FUNCT_2:3;
then
reconsider L0L=LL1*canFS(support b1)
as Function of (dom p),(dom p) by A35,FUNCT_2:19;
rng L0L = dom p by A13,A62,A63,RELAT_1:47;
then L0L is onto by FUNCT_2:def 3;
then reconsider LL = L0L as Permutation of (dom p) by A61,FUNCT_2:def 4;
( (canFS(support b))| dom p) * LL
= ( ( (canFS(support b)) | dom p) * LL1)*canFS(support b1) by RELAT_1:55
.= (id (support b1)) * canFS(support b1) by A13,A35,A38,A60,FUNCT_2:35
.=canFS(support b1) by FUNCT_2:23;
then
A64: canFS(support b1)*LL" =( (canFS(support b))| dom p)* (LL*LL")
by RELAT_1:55;
rng LL= dom p by FUNCT_2:def 3;
then
A65: canFS(support b1)*LL" =( (canFS(support b))| dom p)* (id (dom p))
by A34,A64,FUNCT_2:35;
reconsider L= LL" as Permutation of dom p;
reconsider FS=canFS(support b1) as FinSequence;
A66: rng L = dom FS by A28,FUNCT_2:def 3;
then
A67: dom (FS*L) = dom L by RELAT_1:46
.=dom p by A34,FUNCT_2:def 1;
A68: SetPrimes = dom b1 by PBOOLE:def 3;
rng canFS(support b1) =support b1 by UPROOTS:5;
then
A69: dom (b1*FS) =dom p by A28,A68,RELAT_1:46;
A70: rng (FS*L) = rng FS by A66,RELAT_1:47
.= (support b) \ {q} by A13,UPROOTS:5;
SetPrimes = dom b1 by PBOOLE:def 3;
then
A71: dom p = dom (b1*(FS*L)) by A67,A70,RELAT_1:46;
A72: now
let k be set;
assume
A73: k in dom p;
A74: dom p c=dom (p^<*x*>) by FINSEQ_1:39;
A75: k is Element of NAT by A73;
A76: (FS*L).k in support b \ {q} by A67,A70,A73,FUNCT_1:12;
thus p.k = (p^<*x*>).k by A73,A75,FINSEQ_1:def 7
.=b.((canFS(support b)).k) by A1,A73,A74,FUNCT_1:22
.=b.(((canFS(support b)) |(dom p)).k) by A73,FUNCT_1:72
.=b.((FS*L).k) by A65,FUNCT_2:23
.=b1.((FS*L).k) by A12,A76
.= (b1*(FS*L)).k by A71,A73,FUNCT_1:22;
end;
set p1=b1*FS;
A77: p=b1*(FS*L) by A71,A72,FUNCT_1:9
.=p1*L by RELAT_1:55;
A78: p,p1 are_fiberwise_equipotent by A69,A77,RFINSEQ:6;
dom p1 = Seg len p by A69,FINSEQ_1:def 3;
then
A79: p1 is FinSequence by FINSEQ_1:def 2;
rng p1 c= NAT by VALUED_0:def 6;
then reconsider p1 as FinSequence of NAT by A79,FINSEQ_1:def 4;
A80: Seg len p1 =dom p by A69,FINSEQ_1:def 3;
take p1,q,n,b1;
thus thesis by A4,A5,A8,A9,A11,A13,A20,A78,A80,Def1,EULER_2:25
,FINSEQ_1:def 3,FUNCT_1:12;
end;
end;
Lm6: for i be Element of NAT,f be FinSequence of NAT,
b be bag of SetPrimes,a be 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
proof
defpred P[Element of NAT] means
for f be FinSequence of NAT, b be bag of SetPrimes,
a be Prime st len f =$1 & 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;
A1: P[ 0 ] by FINSEQ_1:32,RVSUM_1:124;
A2: for k being Element of NAT st P[k] holds P[k+1]
proof
let k be Element of NAT;
assume
A3: P[k];
thus P[k+1]
proof
let f be FinSequence of NAT, b be bag of SetPrimes, a be Prime;
assume
A4: len f =k+1 & b is prime-factorization-like &
Product b <> 1 & a divides Product b &
Product b = Product f & f = b*canFS(support b);
reconsider x=f.(k+1) as Element of NAT;
reconsider p=f|k as FinSequence of NAT;
A5: 1<= (k+1) & k+1 <= len f by A4,NAT_1:11;
A6: f = (f|k)^<*f/.len f*> by A4,FINSEQ_5:24
.= p^ <*x*> by A4,A5,FINSEQ_4:24;
A7: len p = k by A4,FINSEQ_1:80,NAT_1:11;
consider p1 being FinSequence of NAT, q be Prime,n be Element of NAT,
b1 be bag of SetPrimes such that
A8: 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) by A4,A6,Lm5;
A9: Product(f)=Product (p1) * x by A6,A8,RVSUM_1:126;
rng p1 c= COMPLEX by NUMBERS:20,XBOOLE_1:1;
then p1 is FinSequence of COMPLEX by FINSEQ_1:def 4;
then
A10: Product (b1) = Product p1 by A8,NAT_3:def 5;
now per cases;
suppose
A11: Product (p1) = 1;
A12: a <> 1 & q <> 1 by INT_2:def 5;
then ex k being Element of NAT st a = q*k by A4,A8,A9,A11,PEPIN:33;
then
q divides a by INT_1:def 9;
hence a in support b by A8,A12,INT_2:def 5;
end;
suppose
A13: Product (p1) <> 1;
per cases;
suppose a=q;
hence a in support b by A8;
end;
suppose
A14: a<>q;
A15: a in support b1 by A3,A4,A7,A8,A9,A10,A13,A14,Th5;
support b1 c= support b by A8,XBOOLE_1:36;
hence a in support b by A15;
end;
end;
end;
hence thesis;
end;
end;
for k be Element of NAT holds P[k] from NAT_1:sch 1(A1,A2);
hence thesis;
end;
theorem Th6:
for f be FinSequence of NAT, b be bag of SetPrimes,a be Prime
st 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
proof
let f be FinSequence of NAT, b be bag of SetPrimes, a be Prime;
assume
A1: b is prime-factorization-like & Product b <> 1 &
a divides Product b & Product b = Product f & f = b*canFS(support b);
len f is Element of NAT;
hence thesis by A1,Lm6;
end;
Lm7: for a be Prime, b be bag of SetPrimes
st b is prime-factorization-like & a divides Product b holds a in support b
proof
let a be Prime, b be bag of SetPrimes;
assume
A1: b is prime-factorization-like & a divides Product b;
per cases;
suppose
A2: Product b = 1;
A3: a <> 1 by INT_2:def 5;
a is Element of NAT by ORDINAL1:def 13;
hence thesis by A1,A2,A3,WSIERP_1:20;
end;
suppose
A4: Product b <> 1;
consider f being FinSequence of COMPLEX such that
A5: Product b = Product f & f = b*canFS(support b) by NAT_3:def 5;
A6: rng b c= NAT by VALUED_0:def 6;
rng f c= rng b by A5,RELAT_1:45;
then rng f c= NAT by A6,XBOOLE_1:1;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
b is prime-factorization-like & Product b <> 1 & a divides Product b &
Product b = Product f & f = b*canFS(support b) by A1,A4,A5;
hence a in support b by Th6;
end;
end;
theorem Th7:
for p,q be bag of SetPrimes
st (support p) c= (support q) & p | (support p) = q | (support p) holds
(Product p) divides (Product q)
proof
let p,q be bag of SetPrimes;
assume
A1: (support p) c= (support q) & p | (support p) =q | (support p);
consider r be bag of SetPrimes such that
A2: support r =(support q) \ (support p) & (support p) misses (support r) &
r |(support r) = q|( support r) & p+r = q by A1,Lm2;
(Product p)*(Product r) = Product (q) by A2,NAT_3:19;
hence (Product p) divides (Product q) by INT_1:def 9;
end;
theorem
for p be bag of SetPrimes,x be Prime st p is prime-factorization-like holds
x divides Product p iff x in support p by Lm4,Lm7;
theorem Th9:
for n,m,k be non empty natural number st k = n lcm m holds
support ppf k=(support ppf n) \/ (support ppf m)
proof
let n,m,k be non empty natural number;
assume
A1: k = n lcm m;
A2: support ppf k =support pfexp k by NAT_3:def 9
.=support max(pfexp n,pfexp m) by A1,NAT_3:54;
A3: support ppf n = support pfexp n by NAT_3:def 9;
A4: support ppf m = support pfexp m by NAT_3:def 9;
A5: support ppf k c= (support ppf n) \/ (support ppf m) by A2,A3,A4,NAT_3:18;
support pfexp n \/ support pfexp m c= support max(pfexp n,pfexp m)
proof
let x be set;
assume
A6: x in support pfexp n \/ support pfexp m;
per cases by A6,XBOOLE_0:def 2;
suppose x in support pfexp n;
then
(pfexp n).x <> 0 by POLYNOM1:def 7;
then
A7: 0 < (pfexp n).x;
(pfexp n).x <=max(pfexp n,pfexp m).x
proof
per cases;
suppose (pfexp n).x <= (pfexp m).x;
hence thesis by NAT_3:def 4;
end;
suppose (pfexp n).x > (pfexp m).x;
hence thesis by NAT_3:def 4;
end;
end;
hence x in support max(pfexp n,pfexp m) by A7,POLYNOM1:def 7;
end;
suppose x in support pfexp m;
then
(pfexp m).x <> 0 by POLYNOM1:def 7;
then
A8: 0 < (pfexp m).x;
(pfexp m).x <=max(pfexp n,pfexp m).x
proof
per cases;
suppose (pfexp n).x <= (pfexp m).x;
hence thesis by NAT_3:def 4;
end;
suppose (pfexp n).x > (pfexp m).x;
hence thesis by NAT_3:def 4;
end;
end;
hence x in support max(pfexp n,pfexp m) by A8,POLYNOM1:def 7;
end;
end;
hence thesis by A2,A3,A4,A5,XBOOLE_0:def 10;
end;
theorem Th10:
for X being set,b1,b2 being bag of X
holds support min(b1,b2) = support b1 /\ support b2
proof
let X be set;
let b1,b2 be bag of X;
set f = min(b1,b2);
A1: for x be set holds
x in support b1 & x in support b2 implies x in support min(b1,b2)
proof
let x be set;
assume (x in support b1) & (x in support b2);
then
A2: b1.x<>0 & b2.x<>0 by POLYNOM1:def 7;
b1.x <= b2.x or b1.x > b2.x;
then f.x = b1.x or f.x = b2.x by NAT_3:def 3;
hence thesis by A2,POLYNOM1:def 7;
end;
for x be set holds x in support min(b1,b2)
implies x in support b1 & x in support b2
proof
let x be set;
assume
A3: x in support min(b1,b2);
assume
A4: not( x in support b1) or not ( x in support b2);
now per cases;
case
A5: b1.x<=b2.x;
A6: not( x in support b1)
proof
assume x in support b1;
then b1.x<>0 & b2.x=0 by A4,POLYNOM1:def 7;
hence contradiction by A5;
end;
f.x = b1.x by A5,NAT_3:def 3
.=0 by A6,POLYNOM1:def 7;
hence contradiction by A3,POLYNOM1:def 7;
end;
case
A7: b2.x 0 ex p1 be bag of SetPrimes st
p1 = (SetPrimes --> 0)+*(q,g) & support p1 = {q} & Product p1 = g
proof
let q be Prime,g be Element of NAT;
assume
A1: g <> 0;
set p = (SetPrimes --> 0)+*(q,g);
A2: dom(SetPrimes --> 0) = SetPrimes by FUNCOP_1:19;
then dom p = SetPrimes by FUNCT_7:32;
then reconsider p as ManySortedSet of SetPrimes by PBOOLE:def 3;
q in dom(SetPrimes --> 0) by A2,NEWTON:def 6;
then
A3: p.q = g by FUNCT_7:33;
A4: for x st not x in {q} holds p.x=0
proof
let x be set;
assume not x in {q};
then x <> q by TARSKI:def 1;
hence thesis by Lm1;
end;
A5: support p = {q}
proof
now
let z be set;
assume
A6: z in support p;
z in dom p
proof
assume not z in dom p;
then p.z = {} by FUNCT_1:def 4;
hence contradiction by A6,POLYNOM1:def 7;
end;
then reconsider y = z as Element of SetPrimes by A2,FUNCT_7:32;
A7: p.y <> 0 by A6,POLYNOM1:def 7;
assume not z in {q};
thus z in {q} by A4,A7;
end;
then for z be set st z in support p holds z in {q};
then
A8: support p c= {q} by TARSKI:def 3;
now
let z be set;
assume z in {q};
then
A9: z=q by TARSKI:def 1;
then
reconsider y = z as Element of SetPrimes by NEWTON:def 6;
thus z in support p by A1,A3,A9,POLYNOM1:def 7;
end;
then
{q} c= support p by TARSKI:def 3;
hence thesis by A8,XBOOLE_0:def 10;
end;
reconsider p as bag of SetPrimes by A5,POLYNOM1:def 8;
take p;
consider f being FinSequence of COMPLEX such that
A10: Product p = Product f & f = p*canFS(support p) by NAT_3:def 5;
A11: q in support p by A5,TARSKI:def 1;
A12: q in dom p
proof
assume not q in dom p;
then
p.q = {} by FUNCT_1:def 4;
hence contradiction by A11,POLYNOM1:def 7;
end;
f = p*(<*q*>) by A5,A10,UPROOTS:6;
then f = <*(p.q)*> by A12,BAGORDER:3;
hence thesis by A3,A5,A10,RVSUM_1:125;
end;
Lm9: for p be bag of SetPrimes, x be Prime st p is prime-factorization-like &
x in support p & p.x = x holds ex p1,r1 be 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
proof
let p be bag of SetPrimes,x be Prime;
assume
A1: p is prime-factorization-like & x in support p & p.x = x;
then
{x} c= support p by ZFMISC_1:37;
then
consider q,r be bag of SetPrimes such that
A2: (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 by Lm3;
A3: (Product q)*(Product r) = Product p by A2,NAT_3:19;
defpred C[set] means $1 in {x};
deffunc F(set) = x;
deffunc G(set) = 0;
consider nx be natural number such that
A4: 0 < nx & p.x =x |^ nx by A1,Def1;
consider mx be Nat such that
A5: nx=mx + 1 by A4,NAT_1:6;
A6: mx = 0
proof
assume mx <> 0;
then 0 < mx;
then
A7: 0+1 < mx+ 1 by XREAL_1:10;
1 < x by INT_2:def 5;
then
A8: x to_power 1 < x to_power nx by A5,A7,POWER:44;
x|^1 < x to_power nx by A8,POWER:46;
then
x|^1 < x |^ nx by POWER:46;
hence contradiction by A1,A4,NEWTON:10;
end;
A9: q is prime-factorization-like
proof
now
let z be Prime;
assume
A10: z in support q;
A11: (support q) c= (support p) by A2,XBOOLE_1:36;
consider n be natural number such that
A12: 0 < n & p.z =z |^ n by A1,A10,A11,Def1;
take n;
q.z = (q|support q).z by A10,FUNCT_1:72
.= p.z by A2,A10,FUNCT_1:72;
hence 0 < n & q.z =z |^ n by A12;
end;
hence thesis by Def1;
end;
A13: x in (support r) by A2,TARSKI:def 1;
A14: r.x =(r | (support r)).x by A13,FUNCT_1:72
.= p.x by A2,A13,FUNCT_1:72
.= x by A4,A5,A6,NEWTON:10;
r = (SetPrimes --> 0)+*(x,r.x) by A2,Th1;
then ex rr1 be bag of SetPrimes st rr1=r & support rr1 = {x} &
Product rr1 = x by A14,Lm8;
hence thesis by A2,A3,A9;
end;
Lm10: for p be bag of SetPrimes,x be Prime st
p is prime-factorization-like & x in support p & p.x <> x holds
ex p1,r1 be 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
proof
let p be bag of SetPrimes,x be Prime;
assume
A1: p is prime-factorization-like& x in support p & p.x <> x;
then
A2: {x} c= support p by ZFMISC_1:37;
then
consider q,r be bag of SetPrimes such that
A3: (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 by Lm3;
defpred C[set] means $1 in {x};
deffunc F(set) = x;
deffunc G(set) = 0;
A4: (support q) /\ (support r) = {} by A3,XBOOLE_0:def 7;
set r10 = (SetPrimes --> 0)+*(x,x);
consider nx be natural number such that
A5: 0 < nx & p.x =x |^ nx by A1,Def1;
consider mx be Nat such that
A6: nx=mx + 1 by A5,NAT_1:6;
A7: mx <> 0 by A1,A5,A6,NEWTON:10;
A8: x in (support r) by A3,TARSKI:def 1;
A9: r.x =(r | (support r)).x by A8,FUNCT_1:72
.=p.x by A3,A8,FUNCT_1:72;
A10: (r.x)/x =((x |^ mx)*x)/x by A5,A6,A9,NEWTON:11
.= x |^mx by XCMPLX_1:90;
reconsider rxx= (r.x)/x as Element of NAT by A10,ORDINAL1:def 13;
defpred C2[set] means $1 in {x};
deffunc F2(set) =rxx;
deffunc G2(set) = 0;
set r20 = (SetPrimes --> 0)+*(x,rxx);
x is Element of NAT & x <> 0 by ORDINAL1:def 13;
then consider r1 be bag of SetPrimes such that
A11: r1=r10 & support r1 = {x} & Product r1 = x by Lm8;
rxx <> 0
proof
assume
A12: rxx=0;
r.x= rxx*x by XCMPLX_1:88
.=0 by A12;
hence contradiction by A5,A9;
end;
then
consider r2 be bag of SetPrimes such that
A13: r2=r20 & support r2 = {x} & Product r2 = rxx by Lm8;
A14: r.x= rxx*x by XCMPLX_1:88;
r = (SetPrimes --> 0)+*(x,r.x) by A3,Th1;
then
A15: ex rr1 be bag of SetPrimes st rr1=r & support rr1 = {x} &
Product rr1 = rxx*x by A5,A9,A14,Lm8;
A16: dom(SetPrimes-->0) = SetPrimes by FUNCOP_1:19;
then
A17: x in dom(SetPrimes-->0) by NEWTON:def 6;
set p1=q+r2;
x in {x} by TARSKI:def 1;
then
A18: not x in support q by A3,XBOOLE_0:def 4;
p1.x= q.x + r2.x by POLYNOM1:def 5
.= 0 + r2.x by A18,POLYNOM1:def 7
.= rxx by A13,A17,FUNCT_7:33;
then
A19: p.x =(p1.x)*x by A9,XCMPLX_1:88;
A20: Product p = (Product q)*((Product r2)*x) by A3,A13,A15,NAT_3:19
.= ((Product q)*(Product r2))*x
.= (Product p1)*x by A3,A13,NAT_3:19;
A21: p1 is prime-factorization-like
proof
now
let z be Prime;
assume z in support p1;
then
A22: z in support q \/ support r2 by POLYNOM1:42;
A23: p1.z= q.z + r2.z by POLYNOM1:def 5;
per cases by A22,XBOOLE_0:def 2;
suppose
A24: z in support q;
(support q) c= (support p) by A3,XBOOLE_1:36;
then
consider n be natural number such that
A25: 0 < n & p.z =z |^ n by A1,A24,Def1;
A26: q.z = (q|support q).z by A24,FUNCT_1:72
.= p.z by A3,A24,FUNCT_1:72;
not z in {x} by A3,A24,XBOOLE_0:def 4;
then
A27: r2.z = 0 by A13,POLYNOM1:def 7; thus
ex n be natural number st 0 < n & p1.z =z |^ n by A23,A25,A26,A27;
end;
suppose
A28: z in support r2;
then
A29: z = x by A13,TARSKI:def 1;
A30: not z in support q by A3,A4,A13,A28,XBOOLE_0:def 3;
take mx;
thus 0 < mx by A7;
p1.z= q.z + r2.z by POLYNOM1:def 5
.= 0 + r2.z by A30,POLYNOM1:def 7
.= z |^ mx by A10,A13,A16,A28,A29,FUNCT_7:33;
hence p1.z = z |^ mx;
end;
end;
hence thesis by Def1;
end;
A31: dom p1= SetPrimes by PBOOLE:def 3
.= dom p by PBOOLE:def 3;
now
let z be set;
assume
A32: z in (support p1) \ {x};
then z in support p1 by XBOOLE_0:def 4;
then z in support q \/ support r2 by POLYNOM1:42;
then
A33: z in support q or z in support r2 by XBOOLE_0:def 2;
A34: p1.z= q.z + r2.z by POLYNOM1:def 5;
A35: q.z = (q|support q).z by A13,A32,A33,FUNCT_1:72,XBOOLE_0:def 4
.= p.z by A3,A13,A32,A33,FUNCT_1:72,XBOOLE_0:def 4;
not z in {x} by A32,XBOOLE_0:def 4;
then r2.z = 0 by A13,POLYNOM1:def 7;
hence p1.z =p.z by A34,A35;
end;
then
A36: p1 | ((support p1) \ {x}) =p | ((support p1) \{x}) by A31,FUNCT_1:166;
support p1 = ( (support p) \ {x}) \/ {x} by A3,A13,POLYNOM1:42
.= (support p) \/ {x} by XBOOLE_1:39
.= support p by A2,XBOOLE_1:12;
hence thesis by A11,A19,A20,A21,A36;
end;
theorem Th13:
for p be bag of SetPrimes st p is prime-factorization-like holds
Product p <> 0
proof
let p be bag of SetPrimes;
assume
A1: p is prime-factorization-like;
consider f being FinSequence of COMPLEX such that
A2: Product p = Product f & f = p*canFS(support p) by NAT_3:def 5;
reconsider f as complex-yielding FinSequence;
assume Product p = 0;
then
consider k be Nat such that
A3: k in dom f&f.k = 0 by A2,RVSUM_1:133;
A4: rng canFS(support p) = support p by UPROOTS:5;
k in dom (canFS(support p)) by A2,A3,FUNCT_1:21;
then
A5: (canFS(support p)).k in support p by A4,FUNCT_1:12;
then reconsider q= (canFS(support p)).k as Prime by NEWTON:def 6;
consider n be natural number such that
A6: 0 < n & p.q = q|^n by A1,A5,Def1;
thus contradiction by A2,A3,A6,FUNCT_1:22;
end;
theorem Th14:
for p be bag of SetPrimes st p is prime-factorization-like holds
Product p = 1 iff support p = {}
proof
let p be bag of SetPrimes;
assume
A1: p is prime-factorization-like;
A2: now
assume
A3: Product p = 1;
thus support p = {}
proof
assume support p <> {};
then
consider q be set such that
A4: q in support p by XBOOLE_0:def 1;
q in SetPrimes by A4;
then
reconsider q as Element of NAT;
reconsider q as Prime by A4,NEWTON:def 6;
q divides Product p by A1,A4,Lm4;
then
q =1 by A3,WSIERP_1:20;
hence contradiction by INT_2:def 5;
end;
end;
now
assume
A5: support p = {};
consider f being FinSequence of COMPLEX such that
A6: Product p = Product f & f = p*canFS(support p) by NAT_3:def 5;
A7: rng p c= NAT by VALUED_0:def 6;
rng f c= rng p by A6,RELAT_1:45;
then rng f c= NAT by A7,XBOOLE_1:1;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
len canFS(support p) = 0 by A5,CARD_1:78,UPROOTS:def 1;
then
f = p*{} by A6,CARD_2:59
.= {};
hence Product p =1 by A6,RVSUM_1:124;
end;
hence thesis by A2;
end;
Lm11: for n be Element of NAT, p,q be 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
proof
defpred P[Element of NAT] means for p,q be bag of SetPrimes st
p is prime-factorization-like & q is prime-factorization-like &
Product p <= 2|^ $1 & Product p = Product q holds p=q;
A1: P[ 0 ]
proof
let p,q be bag of SetPrimes;
assume
A2: p is prime-factorization-like & q is prime-factorization-like &
Product p <= 2|^0 & Product p = Product q;
A3: Product p <= 1 by A2,NEWTON:9;
Product p <> 0 by A2,Th13;
then 0 < Product p;
then 0 +1 <= Product p by NAT_1:13;
then
A4: Product p =1 by A3,XXREAL_0:1;
then
A5: support p={} by A2,Th14;
support q ={} by A2,A4,Th14;
hence p=q by A5,Th4;
end;
A6: now
let k be Element of NAT;
assume
A7: P[k];
now
let p,q be bag of SetPrimes;
assume
A8: p is prime-factorization-like &
q is prime-factorization-like & Product p <= 2|^ (k+1) &
Product p = Product q;
now per cases;
suppose
A9: support p={};
then Product p =1 by A8,Th14;
then support q ={} by A8,Th14;
hence p=q by A9,Th4;
end;
suppose support p<>{};
then
consider x be set such that
A10: x in support p by XBOOLE_0:def 1;
x is Element of SetPrimes by A10;
then reconsider x as Prime by NEWTON:def 6;
x divides Product p by A8,A10,Lm4;
then
A11: x in support q by A8,Lm7;
per cases;
suppose p.x <> x;
then
consider p1,r1 be bag of SetPrimes such that
A12: 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 by A8,A10,Lm10;
per cases;
suppose q.x <> x;
then consider q1,r2 be bag of SetPrimes such that
A13: q1 is prime-factorization-like & (support r2) = {x} &
Product r2 = x & support q1 = support q &
q1 | ((support q1) \ {x}) =q | ((support q1) \{x}) &
q.x =(q1.x)*x & Product q= (Product q1)*x by A8,A11,Lm10;
A14: 1 < x by INT_2:def 5;
A15: 1+1 <= x by A14,NAT_1:13;
A16: ((Product p1)*x) /x <= (2|^(k+1)) /x by A8,A12,XREAL_1:74;
(2|^(k+1)) /x <= (2|^(k+1)) /2 by A15,XREAL_1:120;
then
((Product p1)*x) /x <= (2|^(k+1)) /2 by A16,XXREAL_0:2;
then
Product p1 <= (2|^(k+1)) /2 by XCMPLX_1:90;
then
Product p1 <= (2|^k*2|^1) /2 by NEWTON:13;
then
A17: Product p1 <= (2|^k*2) /2 by NEWTON:10;
A18: p1=q1 by A7,A8,A12,A13,A17,XCMPLX_1:5;
A19: support p = support q by A7,A8,A12,A13,A17,XCMPLX_1:5;
A20: dom p= SetPrimes by PBOOLE:def 3
.= dom q by PBOOLE:def 3;
now
let z be set;
assume
A21: z in support p;
per cases;
suppose not z in {x};
then
A22: z in (support p1) \ {x} by A12,A21,XBOOLE_0:def 4;
thus p.z = ( p| ((support p1) \ {x})).z by A22,FUNCT_1:72
.= q.z by A12,A13,A18,A22,FUNCT_1:72;
end;
suppose
A23: z in {x};
thus p.z = (p1.x)*x by A12,A23,TARSKI:def 1
.= (q1.x)*x by A7,A8,A12,A13,A17,XCMPLX_1:5
.= q.z by A13,A23,TARSKI:def 1;
end;
end;
then p| (support p) =q| (support q) by A19,A20,FUNCT_1:166;
hence p=q by Th3;
end;
suppose q.x = x;
then
consider q1,r2 be bag of SetPrimes such that
A24: q1 is prime-factorization-like &
(support r2) = {x} & Product r2 = x &
(support q1) = (support q) \ {x} &
q1 | (support q1) =q | (support q1) &
Product q= (Product q1)*x by A8,A11,Lm9;
A25: 1 < x by INT_2:def 5;
A26: 1+1 <= x by A25,NAT_1:13;
A27: ((Product p1)*x) /x <= (2|^(k+1)) /x by A8,A12,XREAL_1:74;
(2|^(k+1)) /x <= (2|^(k+1)) /2 by A26,XREAL_1:120;
then
((Product p1)*x) /x <= (2|^(k+1)) /2 by A27,XXREAL_0:2;
then
Product p1 <= (2|^(k+1)) /2 by XCMPLX_1:90;
then
Product p1 <= (2|^k*2|^1) /2 by NEWTON:13;
then
A28: Product p1 <= (2|^k*2) /2 by NEWTON:10;
A29: support p = support q \ {x} by A7,A8,A12,A24,A28,XCMPLX_1:5;
x in support q & not x in {x} by A10,A29,XBOOLE_0:def 4;
hence p=q by TARSKI:def 1;
end;
end;
suppose
A30: p.x = x;
then consider p1,r1 be bag of SetPrimes such that
A31: 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 by A8,A10,Lm9;
per cases;
suppose q.x <> x;
then consider q1,r2 be bag of SetPrimes such that
A32: q1 is prime-factorization-like &
(support r2) = {x} & Product r2 = x & support q1 = support q &
q1 | ((support q1) \ {x}) =q | ((support q1) \{x}) &
q.x =(q1.x)*x & Product q= (Product q1)*x by A8,A11,Lm10;
A33: 1 < x by INT_2:def 5;
A34: 1+1 <= x by A33,NAT_1:13;
A35: ((Product p1)*x) /x <= (2|^(k+1)) /x by A8,A31,XREAL_1:74;
(2|^(k+1)) /x <= (2|^(k+1)) /2 by A34,XREAL_1:120;
then
((Product p1)*x) /x <= (2|^(k+1)) /2 by A35,XXREAL_0:2;
then
Product p1 <= (2|^(k+1)) /2 by XCMPLX_1:90;
then
Product p1 <= (2|^k*2|^1) /2 by NEWTON:13;
then
A36: Product p1 <= (2|^k*2) /2 by NEWTON:10;
A37: support p \ {x} = support q by A7,A8,A31,A32,A36,XCMPLX_1:5;
x in support p & not x in {x} by A11,A37,XBOOLE_0:def 4;
hence p=q by TARSKI:def 1;
end;
suppose
A38: q.x = x;
then consider q1,r2 be bag of SetPrimes such that
A39: q1 is prime-factorization-like &
(support r2) = {x} & Product r2 = x &
(support q1) = (support q) \ {x} &
q1 | (support q1) =q | (support q1) &
Product q= (Product q1)*x by A8,A11,Lm9;
A40: 1 < x by INT_2:def 5;
A41: 1+1 <= x by A40,NAT_1:13;
A42: ((Product p1)*x) /x <= (2|^(k+1)) /x by A8,A31,XREAL_1:74;
(2|^(k+1)) /x <= (2|^(k+1)) /2 by A41,XREAL_1:120;
then ((Product p1)*x) /x <= (2|^(k+1)) /2 by A42,XXREAL_0:2;
then Product p1 <= (2|^(k+1)) /2 by XCMPLX_1:90;
then Product p1 <= (2|^k*2|^1) /2 by NEWTON:13;
then
A43: Product p1 <= (2|^k*2) /2 by NEWTON:10;
A44: p1=q1 by A7,A8,A31,A39,A43,XCMPLX_1:5;
support p \ {x}
= support q \ {x} by A7,A8,A31,A39,A43,XCMPLX_1:5;
then
(support p) \/ {x} = (support q \ {x}) \/ {x} by XBOOLE_1:39;
then
A45: (support p) \/ {x} = (support q) \/ {x} by XBOOLE_1:39;
A46: {x} c= support p by A10,ZFMISC_1:37;
A47: {x} c= support q by A11,ZFMISC_1:37;
A48: support p = (support q) \/ {x} by A45,A46,XBOOLE_1:12;
A49: dom p= SetPrimes by PBOOLE:def 3
.= dom q by PBOOLE:def 3;
now
let z be set;
assume
A50: z in (support p);
per cases;
suppose not z in {x};
then
A51: z in support p1 by A31,A50,XBOOLE_0:def 4;
thus p.z = ( p1| (support p1)).z by A31,A51,FUNCT_1:72
.= q.z by A39,A44,A51,FUNCT_1:72;
end;
suppose
A52: z in {x};
thus p.z = x by A30,A52,TARSKI:def 1
.= q.z by A38,A52,TARSKI:def 1;
end;
end;
then
p| (support p) = q| (support p) by A49,FUNCT_1:166
.=q| (support q) by A47,A48,XBOOLE_1:12;
hence p=q by Th3;
end;
end;
end;
end;
hence p=q;
end;
hence P[k+1];
end;
for k be Element of NAT holds P[k] from NAT_1:sch 1(A1,A6);
hence thesis;
end;
theorem Th15:
for p,q be bag of SetPrimes st
p is prime-factorization-like &q is prime-factorization-like&
Product p = Product q holds p=q
proof
let p,q be bag of SetPrimes;
assume
A1: p is prime-factorization-like &
q is prime-factorization-like & Product p = Product q;
reconsider n=Product p as Element of NAT;
n <=2|^n by NEWTON:105;
hence p=q by A1,Lm11;
end;
theorem
for p be bag of SetPrimes, n be non empty natural number st
p is prime-factorization-like & n = Product p holds (ppf n) = p
proof
let p be bag of SetPrimes, n be non empty natural number;
assume
A1: p is prime-factorization-like & n=Product p;
Product ppf n = Product p by A1,NAT_3:61;
hence thesis by A1,Th15;
end;
theorem Th17:
for n,m be Element of NAT st 1<=n & 1 <=m holds
ex m0,n0 be Element of NAT st n lcm m =n0*m0 & n0 gcd m0 = 1 &
n0 divides n & m0 divides m & n0 <> 0 & m0 <> 0
proof
let n1,m1 be Element of NAT;
assume
A1: 1<=n1 & 1 <=m1;
set nm1 = n1 lcm m1;
reconsider n=n1,m=m1 as non empty natural number by A1;
reconsider nm=nm1 as non empty natural number by A1,INT_2:4;
set N1={p where p is Element of NAT:
p in (support (ppf n)) & (pfexp nm).p = (pfexp n). p };
set N2= (support (ppf nm)) \ N1;
A2: support ppf nm = support ppf n \/ support ppf m by Th9;
then
A3: support ppf n c= support ppf nm by XBOOLE_1:7;
A4: N1 c= support ppf n
proof
let x be set;
assume x in N1;
then ex p be Element of NAT st x=p & p in (support (ppf n)) &
(pfexp nm).p = (pfexp n). p;
hence x in support ppf n;
end;
then
A5: N1 c= support ppf nm by A3,XBOOLE_1:1;
N1 \/ N2 = support ppf nm by A3,A4,XBOOLE_1:1,45;
then
A6: N2 c= support ppf nm by XBOOLE_1:7;
A7: N2 c= support ppf m
proof
let x be set;
assume
A8: x in N2;
then
A9: x in (support (ppf nm))& not x in N1 by XBOOLE_0:def 4;
A10: support ppf m = support pfexp m by NAT_3:def 9;
not x in support ppf n or x in support ppf m
proof
x in SetPrimes by A8;
then
A11: not x in (support (ppf n)) or (pfexp nm).x <> (pfexp n). x by A9;
A12: ((pfexp n).x <= (pfexp m).x
implies max(pfexp n,pfexp m).x = (pfexp m).x) &
((pfexp n).x > (pfexp m).x implies
max(pfexp n,pfexp m).x = (pfexp n).x) by NAT_3:def 4;
x in support pfexp nm by A9,NAT_3:def 9;
then (pfexp nm).x = (pfexp m). x implies
(pfexp m).x <> 0 by POLYNOM1:def 7;
hence not x in (support (ppf n)) or
x in support ppf m by A10,A11,A12,NAT_3:54,POLYNOM1:def 7;
end;
hence x in support ppf m by A2,A9,XBOOLE_0:def 2;
end;
A13: for x be set st x in N1 holds (pfexp nm).x = (pfexp n). x
proof
let x be set;
assume x in N1;
then
ex p be Element of NAT st x=p & p in (support (ppf n)) &
(pfexp nm).p = (pfexp n). p;
hence thesis;
end;
A14: for x be set st x in N2 holds (pfexp nm).x = (pfexp m).x
proof
let x be set;
assume x in N2;
then
A15: x in (support (ppf nm)) & not x in N1 by XBOOLE_0:def 4;
A16: support ppf n = support pfexp n by NAT_3:def 9;
A17: ((pfexp n).x <= (pfexp m).x
implies max(pfexp n,pfexp m).x = (pfexp m).x) &
((pfexp n).x > (pfexp m).x implies
max(pfexp n,pfexp m).x = (pfexp n).x) by NAT_3:def 4;
not (pfexp n).x > (pfexp m).x
proof
assume
A18: (pfexp n).x > (pfexp m).x;
then
A19: (pfexp nm).x = (pfexp n). x by A17,NAT_3:54;
A20: x in support (pfexp n) by A18,POLYNOM1:def 7;
then
x in SetPrimes;
hence contradiction by A15,A16,A19,A20;
end;
hence thesis by A17,NAT_3:54;
end;
A21: Product (ppf n)=n by NAT_3:61;
A22: Product (ppf m)=m by NAT_3:61;
consider ppm,ppn be bag of SetPrimes such that
A23: (support ppm) = (support (ppf nm)) \ N1 & (support ppn) = N1 &
(support ppm) misses (support ppn) &
ppm | (support ppm) =(ppf nm) | (support ppm) &
ppn | (support ppn) =(ppf nm) | (support ppn) &
ppm+ppn = (ppf nm) by A5,Lm3;
reconsider n0=Product ppn, m0=Product ppm as Element of NAT;
A24: dom (ppf nm)= SetPrimes by PBOOLE:def 3
.= dom (ppf n) by PBOOLE:def 3;
A25: now
let x1 be set;
assume
A26: x1 in N1;
then
A27: x1 in (support (ppf nm)) by A5;
then
A28: x1 in (support pfexp nm) by NAT_3:def 9;
x1 in support ppf n by A4,A26;
then
A29: x1 in support pfexp n by NAT_3:def 9;
x1 is Element of SetPrimes by A27;
then
reconsider x=x1 as Prime by NEWTON:def 6;
thus (ppf nm).x1= x |^ (x |-count nm) by A28,NAT_3:def 9
.= x |^ ((pfexp nm).x) by NAT_3:def 8
.= x |^ ((pfexp n).x) by A13,A26
.= x |^ (x |-count n) by NAT_3:def 8
.= (ppf n).x1 by A29,NAT_3:def 9;
end;
A30: ppn|N1=(ppf n)|N1 by A23,A24,A25,FUNCT_1:166;
A31: dom (ppf nm)= SetPrimes by PBOOLE:def 3
.= dom (ppf m) by PBOOLE:def 3;
A32: now
let x2 be set;
assume
A33: x2 in N2;
then
x2 in (support (ppf nm)) by A6;
then
A34: x2 in (support pfexp nm) by NAT_3:def 9;
x2 in support ppf m by A7,A33;
then
A35: x2 in support pfexp m by NAT_3:def 9;
x2 is Element of SetPrimes by A33;
then
reconsider x=x2 as Prime by NEWTON:def 6;
thus (ppf nm).x2 = x |^ (x |-count nm) by A34,NAT_3:def 9
.= x |^ ((pfexp nm).x) by NAT_3:def 8
.= x |^ ((pfexp m).x) by A14,A33
.= x |^ (x |-count m) by NAT_3:def 8
.= (ppf m).x2 by A35,NAT_3:def 9;
end;
A36: ppm|N2 = (ppf m)|N2 by A23,A31,A32,FUNCT_1:166;
A37: n0*m0 = Product (ppf nm) by A23,NAT_3:19
.=nm by NAT_3:61;
A38: m0 divides m by A7,A22,A23,A36,Th7;
A39: n0 <> 0 by A37;
A40: m0 <> 0 by A37;
now
let x being Prime;
assume
A41: x in support ppm;
then
x in (support (ppf nm)) by A23,XBOOLE_0:def 4;
then
A42: x in (support pfexp nm) & x is natural number by NAT_3:def 9;
then
A43: (ppf nm) .x = x |^ (x |-count nm) by NAT_3:def 9;
(pfexp nm).x <> 0 by A42,NAT_3:36,38;
then
0 <> (x |-count nm) by NAT_3:def 8;
then
A44: 0 < (x |-count nm);
ppm.x =(ppm | (support ppm)).x by A41,FUNCT_1:72
.= (ppf nm).x by A23,A41,FUNCT_1:72;
hence
ex m be natural number st 0 < m & (ppm).x = x |^m by A43,A44;
end;
then
A45: ppm is prime-factorization-like by Def1;
now
let x being Prime;
assume
A46: x in support (ppn);
then x in (support (ppf nm)) by A5,A23;
then
A47: x in (support pfexp nm) & x is natural number by NAT_3:def 9;
then
A48: (ppf nm) .x = x |^ (x |-count nm) by NAT_3:def 9;
(pfexp nm).x <> 0 by A47,NAT_3:36,38;
then 0 <> (x |-count nm) by NAT_3:def 8;
then
A49: 0 < (x |-count nm);
ppn.x =(ppn | (support ppn)).x by A46,FUNCT_1:72
.= (ppf nm).x by A23,A46,FUNCT_1:72;
hence ex n be natural number st 0 < n & (ppn).x = x |^n by A48,A49;
end;
then ppn is prime-factorization-like by Def1;
then
A50: n0,m0 are_relative_prime by A23,A45,Th12;
A51: n0 gcd m0 = 1 by A50,INT_2:def 4;
thus thesis by A4,A21,A23,A30,A37,A38,A39,A40,A51,Th7;
end;
begin ::multiplicative group
definition
let n be natural number;
assume
A1: 1 < n;
func Segm0(n) -> non empty finite Subset of NAT equals
:Def2:
Segm(n) \ {0};
correctness
proof
A2: 1 in Segm(n) by A1,GR_CY_1:10;
not 1 in {0} by TARSKI:def 1;
hence thesis by A2,FINSET_1:16,XBOOLE_0:def 4;
end;
end;
theorem Th18:
for n be natural number st 1 < n holds Card Segm0(n) = n-1
proof
let n be natural number;
assume
A1: 1 < n;
A2: Segm0(n) = Segm(n) \{0} by A1,Def2;
A3: Segm(n) is finite & Card (Segm(n)) = n by CARD_1:66;
A4: 0 in Segm(n) by A1,NAT_1:45;
Card {0} = 1 by CARD_1:50;
hence thesis by A2,A3,A4,EULER_1:5;
end;
definition
let n be Prime;
func multint0(n) -> BinOp of Segm0(n) equals
(multint n) || Segm0 n;
coherence
proof
A1: 1 0 by TARSKI:def 1;
then
A7: a <> 0.(INT.Ring(n)) by A6,FUNCT_7:def 1;
not b in {0} by A4,XBOOLE_0:def 4;
then
b <> 0 by TARSKI:def 1;
then
A8: b <> 0.(INT.Ring(n)) by A6,FUNCT_7:def 1;
y <> In (0,Segm(n)) by A5,A7,A8,VECTSP_1:44;
then
y <> 0 by A5,FUNCT_7:def 1;
then
not y in {0} by TARSKI:def 1;
then
y in Segm(n)\{0} by A5,XBOOLE_0:def 4;
hence (multint n).x in S by A1,A2,Def2;
end;
hence (multint n) || Segm0 n is BinOp of Segm0(n) by REALSET1:9;
end;
end;
Lm12: for p be Prime, a,b be Element of multMagma(#Segm0(p),multint0(p)#),
x,y be Element of INT.Ring(p) st a=x & y=b holds x*y = a*b
proof
let p be Prime, a,b be Element of multMagma(#Segm0(p),multint0(p)#),
x,y be Element of INT.Ring(p);
assume
A1: a=x& y=b;
thus a*b = (multint(p)).([a,b]) by FUNCT_1:72
.=x*y by A1;
end;
theorem Th19:
for p be Prime holds multMagma(#Segm0(p),multint0(p)#)
is associative commutative Group-like
proof
let p be Prime;
A1: 1 < p by INT_2:def 5;
set Zp= multMagma(#Segm0(p),multint0(p)#);
A2: 1 in Segm(p) by A1,GR_CY_1:10;
not 1 in {0} by TARSKI:def 1;
then
1 in Segm(p)\{0} by A2,XBOOLE_0:def 4;
then
1 in Segm0(p) by A1,Def2;
then
reconsider e=1.(INT.Ring(p)) as Element of Zp by A1,INT_3:24;
A3: now
let h be Element of Zp;
h in Segm0(p);
then
A4: h in Segm(p)\{0} by A1,Def2;
then
reconsider hp=h as Element of INT.Ring(p) by XBOOLE_0:def 4;
thus h * e = hp*1_(INT.Ring(p)) by Lm12
.= h by GROUP_1:def 5;
thus e * h = 1_(INT.Ring(p))*hp by Lm12
.= h by GROUP_1:def 5;
not h in {0} by A4,XBOOLE_0:def 4;
then
A5: hp <> 0 by TARSKI:def 1;
0 in Segm(p) by GR_CY_1:10;
then hp <> 0.(INT.Ring(p)) by A5,FUNCT_7:def 1;
then consider hpd be Element of INT.Ring(p) such that
A6: hpd*hp=1.(INT.Ring(p)) by VECTSP_1:def 20;
hpd <> 0.(INT.Ring(p)) by A6,VECTSP_1:36;
then hpd <> 0 by FUNCT_7:def 1;
then not hpd in {0} by TARSKI:def 1;
then hpd in Segm(p)\{0} by XBOOLE_0:def 4;
then reconsider g=hpd as Element of Zp by A1,Def2;
A7: h*g=e by A6,Lm12;
g * h = e by A6,Lm12;
hence ex g be Element of Zp st h*g = e & g*h = e by A7;
end;
A8: Zp is associative
proof
let x,y,z being Element of Zp;
x in Segm0(p);
then
x in Segm(p)\{0} by A1,Def2;
then
reconsider x1=x as Element of INT.Ring(p) by XBOOLE_0:def 4;
y in Segm0(p);
then
y in Segm(p)\{0} by A1,Def2;
then
reconsider y1=y as Element of INT.Ring(p) by XBOOLE_0:def 4;
z in Segm0(p);
then
z in Segm(p)\{0} by A1,Def2;
then
reconsider z1=z as Element of INT.Ring(p) by XBOOLE_0:def 4;
A9: x*y=x1*y1 by Lm12;
A10: y*z=y1*z1 by Lm12;
(x*y)*z =(x1*y1)*z1 by A9,Lm12
.=x1*(y1*z1) by GROUP_1:def 4
.= x*(y*z) by A10,Lm12;
hence thesis;
end;
Zp is commutative
proof
let x,y being Element of Zp;
x in Segm0(p);
then x in Segm(p)\{0} by A1,Def2;
then reconsider x1=x as Element of INT.Ring(p) by XBOOLE_0:def 4;
y in Segm0(p);
then y in Segm(p)\{0} by A1,Def2;
then reconsider y1=y as Element of INT.Ring(p) by XBOOLE_0:def 4;
x*y = x1*y1 by Lm12
.= y*x by Lm12;
hence thesis;
end;
hence thesis by A3,A8,GROUP_1:def 3;
end;
definition
let p be Prime;
func Z/Z*(p) -> commutative Group equals
multMagma(#Segm0(p),multint0(p)#);
correctness by Th19;
end;
theorem
for p be Prime,x,y be Element of Z/Z*(p),
x1,y1 be Element of INT.Ring(p) st x=x1 & y=y1 holds x*y = x1*y1 by Lm12;
theorem Th21:
for p be Prime holds 1_Z/Z*(p) =1 & 1_Z/Z*(p) = 1.(INT.Ring(p))
proof
let p be Prime;
A1: 1 < p by INT_2:def 5;
A2: 1 in Segm(p) by A1,GR_CY_1:10;
not 1 in {0} by TARSKI:def 1;
then 1 in Segm(p)\{0} by A2,XBOOLE_0:def 4;
then 1 in Segm0(p) by A1,Def2;
then reconsider e=1.(INT.Ring(p)) as Element of Z/Z*(p) by A1,INT_3:24;
now
let h being Element of Z/Z*(p);
h in Segm0(p);
then
h in Segm(p)\{0} by A1,Def2;
then
reconsider hp=h as Element of INT.Ring(p) by XBOOLE_0:def 4;
thus h * e = hp*1_(INT.Ring(p)) by Lm12
.= h by GROUP_1:def 5;
thus e * h = 1_(INT.Ring(p))*hp by Lm12
.= h by GROUP_1:def 5;
end;
then e=1_(Z/Z*(p)) by GROUP_1:def 5;
hence thesis by A1,INT_3:24;
end;
theorem
for p be Prime, x be Element of Z/Z*(p),
x1 be Element of INT.Ring(p) st x=x1 holds x" = x1"
proof
let p be Prime, h be Element of Z/Z*(p), hp be Element of INT.Ring(p);
assume
A1: h=hp;
A2: 1 < p by INT_2:def 5;
h in Segm0(p);
then
A3: h in Segm(p)\{0} by A2,Def2;
not h in {0} by A3,XBOOLE_0:def 4;
then
A4: hp <> 0 by A1,TARSKI:def 1;
0 in Segm(p) by GR_CY_1:10;
then
A5: hp <> 0.(INT.Ring(p)) by A4,FUNCT_7:def 1;
set hpd=hp";
A6: hp*hpd =1.(INT.Ring(p)) by A5,VECTSP_1:def 22;
hpd <> 0.(INT.Ring(p)) by A6,VECTSP_1:36;
then hpd <> 0 by FUNCT_7:def 1;
then not hpd in {0} by TARSKI:def 1;
then hpd in Segm(p)\{0} by XBOOLE_0:def 4;
then reconsider g=hpd as Element of Z/Z*(p) by A2,Def2;
h*g=hp*hpd by A1,Lm12
.=1.(INT.Ring(p)) by A5,VECTSP_1:def 22
.=1_(Z/Z*(p)) by Th21;
hence thesis by GROUP_1:def 6;
end;
registration
let p be Prime;
cluster Z/Z*(p) -> finite;
coherence by STRUCT_0:def 11;
end;
theorem
for p be Prime holds ord Z/Z*(p) = p-1
proof
let p be Prime;
1 < p by INT_2:def 5;
hence thesis by Th18;
end;
theorem
for G be Group,a be Element of G, i be Integer st a is_not_of_order_0 holds
ex n,k be Element of NAT st a|^i=a|^n & n=k*ord(a) +i
proof
let G be Group,a be Element of G,i be Integer;
assume
A1: a is_not_of_order_0;
ord a<>0 by A1,GROUP_1:def 12;
then
A2: abs(i)<=abs(i)*ord(a) by NAT_1:14,XREAL_1:153;
0<=abs(i)*ord(a)+i
proof
per cases;
suppose i<0;
then
A3: abs(i)=-i by ABSVALUE:def 1;
abs(i)+i<=abs(i)*ord(a)+i by A2,XREAL_1:8;
hence thesis by A3;
end;
suppose 0<=i;
hence thesis by XREAL_1:35;
end;
end;
then
A4: abs(i)*ord(a)+i is Element of NAT by INT_1:16;
a|^(abs(i)*ord(a)+i)=a|^(abs(i)*ord(a))*(a|^i) by GROUP_1:64
.=(a|^(ord(a))|^abs(i))*(a|^i) by GROUP_1:50
.=((1_G)|^abs(i))*(a|^i) by GROUP_1:82
.=(1_G)*(a|^i) by GROUP_1:42
.=a|^i by GROUP_1:def 5;
hence thesis by A4;
end;
theorem Th25:
for G be commutative Group,a,b be Element of G, n,m be natural number
st G is finite & ord a=n & ord b= m & n gcd m = 1 holds ord (a*b) = n*m
proof
let G be commutative Group,a,b be Element of G, n,m be natural number;
assume
A1: G is finite & ord a=n & ord b= m & n gcd m = 1;
reconsider n1=n, m1=m as Integer;
a is_not_of_order_0 & b is_not_of_order_0 by A1,GR_CY_1:26;
then
A2: n <> 0 & m <> 0 by A1,GROUP_1:def 12;
then
A3: n*m <> 0 by XCMPLX_1:6;
A4: a*b is_not_of_order_0 by A1,GR_CY_1:26;
A5: n1,m1 are_relative_prime & m1,n1 are_relative_prime by A1,INT_2:def 4;
A6: (a*b)|^(n*m) = a |^ (n*m) * (b |^ (n*m)) by GROUP_1:95
.= (a |^ n)|^m * (b |^ (n*m)) by GROUP_1:50
.= (a |^ n)|^m * ((b |^ m)|^n) by GROUP_1:50
.= (1_G)|^m * ((b |^ m)|^n) by A1,GROUP_1:82
.= (1_G)|^m * ((1_G)|^n) by A1,GROUP_1:82
.= (1_G) * ((1_G)|^n) by GROUP_1:42
.= (1_G) * (1_G) by GROUP_1:42
.= 1_G by GROUP_1:def 5;
A7: (m*n) is Element of NAT by ORDINAL1:def 13;
A8: now
let k be Nat;
assume
A9: (a*b)|^k =1_G & k <> 0;
reconsider k1=k as Integer;
1_G =(1_G)|^n by GROUP_1:42
.= (a*b)|^(k*n) by A9,GROUP_1:50
.= a |^ (k*n) * (b |^ (k*n)) by GROUP_1:95
.= (a |^ n)|^k * (b |^ (k*n)) by GROUP_1:50
.= (1_G)|^k * (b |^ (k*n)) by A1,GROUP_1:82
.= (1_G) * (b |^ (k*n)) by GROUP_1:42
.= b |^ (k*n) by GROUP_1:def 5;
then
A10: m1 divides k1 by A1,A5,GROUP_1:86,INT_2:40;
1_G =(1_G)|^m by GROUP_1:42
.= (a*b)|^(k*m) by A9,GROUP_1:50
.= a |^ (k*m) * (b |^ (k*m)) by GROUP_1:95
.= a |^ (k*m) * (b |^ m)|^k by GROUP_1:50
.= a |^ (k*m) * (1_G)|^k by A1,GROUP_1:82
.= a |^ (k*m) * (1_G) by GROUP_1:42
.= a |^ (k*m) by GROUP_1:def 5;
then
A11: n1 divides k1 by A1,A5,GROUP_1:86,INT_2:40;
consider i be Integer such that
A12: k1 =m1*i by A10,INT_1:def 9;
n1 divides i by A5,A11,A12,INT_2:40;
then consider j be Integer such that
A13: i =n1*j by INT_1:def 9;
A14: k1 =(m1*n1)*j by A12,A13;
k/(m*n) = j by A2,A14,XCMPLX_1:6,90;
then
A15: j is Element of NAT by INT_1:16;
j <> 0 by A9,A12,A13;
then (m*n)*1 <=(m*n)*j by A15,NAT_1:14,XREAL_1:66;
hence (m*n) <= k by A12,A13;
end;
thus thesis by A3,A4,A6,A7,A8,GROUP_1:def 12;
end;
Lm13: for L be Field, n be Element of NAT, f be non-zero Polynomial of L
st deg f = n ex m be Element of NAT st m=Card(Roots(f)) & m <= n
proof
let L be Field;
defpred P[Nat] means for f be non-zero Polynomial of L st deg f = $1
ex m be Element of NAT st m=Card(Roots(f)) & m <= $1;
A1: P[ 0 ]
proof
let f be non-zero Polynomial of L;
assume
A2: deg f = 0;
A3: f <> 0_.(L) by UPROOTS:def 5;
A4: f.0 <> 0.L
proof
assume f.0 =0.L;
then f =<%0.L%> by A2,ALGSEQ_1:def 6;
hence contradiction by A3,POLYNOM5:35;
end;
reconsider x=f.0 as Element of L;
A5: f =<%x%> by A2,ALGSEQ_1:def 6;
A6: now
let z be Element of L;
eval(<%x%>,z) =eval(<%x,0.L%>,z) by POLYNOM5:44
.=x by POLYNOM5:46;
hence eval(<%x%>,z) <> 0.L by A4;
end;
Roots(f) = {}
proof
assume Roots(f) <> {};
then consider z be set such that
A7: z in Roots(f) by XBOOLE_0:def 1;
reconsider z as Element of L by A7;
z is_a_root_of f by A7,POLYNOM5:def 9;
then eval(<%x%>,z) = 0.L by A5,POLYNOM5:def 6;
hence contradiction by A6;
end;
hence thesis by CARD_2:19;
end;
A8: now
let k be Element of NAT;
assume
A9: P[k];
now
let f be non-zero Polynomial of L;
A10: f <> 0_.(L) by UPROOTS:def 5;
assume
A11: deg f = k+1;
thus ex m be Element of NAT st m=Card(Roots(f)) & m <= k+1
proof
per cases;
suppose Roots(f) = {};
hence thesis by CARD_2:19;
end;
suppose Roots(f) <> {};
then consider z be set such that
A12: z in Roots(f) by XBOOLE_0:def 1;
reconsider z as Element of L by A12;
A13: z is_a_root_of f by A12,POLYNOM5:def 9;
then
A14: rpoly(1,z) divides f by HURWITZ:35;
set g = f div rpoly(1,z);
0_.(L) =f mod rpoly(1,z) by A14,HURWITZ:def 7;
then
(g *' rpoly(1,z)) = f-g *' rpoly(1,z) + g *' rpoly(1,z)
by POLYNOM3:29;
then
(g *' rpoly(1,z)) = f+(-g *' rpoly(1,z) + g *' rpoly(1,z))
by POLYNOM3:26;
then
(g *' rpoly(1,z)) = f+(g *' rpoly(1,z) - g *' rpoly(1,z));
then
(g *' rpoly(1,z)) = f+ 0_.(L) by POLYNOM3:30;
then
A15: f = g *' rpoly(1,z) by POLYNOM3:29;
g <> 0_.(L) by A10,A15,POLYNOM3:35;
then reconsider g as non-zero Polynomial of L by UPROOTS:def 5;
A16: deg (g) = k+1 -1 by A10,A11,A13,HURWITZ:36
.= k;
set RG = Roots g;
consider m1 be Element of NAT such that
A17: m1=Card(Roots(g)) & m1 <= k by A9,A16;
A18: Roots(f) c= Roots(g) \/ {z}
proof
let y be set;
assume
A19: y in Roots(f);
then
reconsider y1=y as Element of L;
y1 is_a_root_of f by A19,POLYNOM5:def 9;
then eval(f,y1) = 0.L by POLYNOM5:def 6;
then eval(g,y1)* eval(rpoly(1,z),y1)= 0.L by A15,POLYNOM4:27;
then
A20: eval(g,y1)* (y1-z) = 0.L by HURWITZ:29;
now per cases;
suppose y1=z;
then
y in {z} by TARSKI:def 1;
hence y in Roots(g) \/ {z} by XBOOLE_0:def 2;
end;
suppose y1<> z;
then
y1-z <> 0.L by RLVECT_1:35;
then eval(g,y1) = 0.L by A20,VECTSP_1:44;
then y1 is_a_root_of g by POLYNOM5:def 6;
then y1 in Roots(g) by POLYNOM5:def 9;
hence y in Roots(g) \/ {z} by XBOOLE_0:def 2;
end;
end;
hence y in Roots(g) \/ {z};
end;
set RF=Roots f;
card (RG \/ {z}) <= card RG + card {z} by CARD_2:62;
then
A21: card (RG \/ {z}) <= card RG + 1 by CARD_2:60;
card RF <= card (RG \/ {z}) by A18,NAT_1:44;
then
A22: card RF <= card(RG)+1 by A21,XXREAL_0:2;
card(RG)+1 <= k + 1 by A17,XREAL_1:8;
hence ex m be Element of NAT
st m=Card(Roots(f)) & m <= k+1 by A22,XXREAL_0:2;
end;
end;
end;
hence P[k+1];
end;
for k be Element of NAT holds P[k] from NAT_1:sch 1(A1,A8);
hence thesis;
end;
theorem Th26:
for L be non empty ZeroStr, p being Polynomial of L st 0 <= deg p
holds p is non-zero
proof
let L be non empty ZeroStr, p being Polynomial of L;
assume 0 <=deg p;
then deg p <> -1;
then p <>0_.L by HURWITZ:20;
hence p is non-zero by UPROOTS:def 5;
end;
theorem Th27:
for L be Field,f be Polynomial of L st 0 <= deg f holds
Roots(f) is finite set &
:: ex m,n be Element of NAT st n=deg f & m=Card(Roots(f)) & m <= n
Card Roots f <= deg f
proof
let L be Field,f be Polynomial of L;
assume
A1: 0 <=deg f;
then reconsider n = deg f as Element of NAT by INT_1:16;
reconsider f as non-zero Polynomial of L by A1,Th26;
ex m be Element of NAT st m=Card(Roots(f)) & m <= n by Lm13;
hence thesis;
end;
theorem Th28:
for p be Prime, z be Element of Z/Z*(p),
y be Element of INT.Ring(p) st z=y holds for n be Element of NAT holds
(power Z/Z*(p)).(z,n) = (power INT.Ring(p)).(y,n)
proof
let p be Prime, z be Element of Z/Z*(p), y be Element of INT.Ring(p);
assume
A1: z=y;
defpred P[Nat] means (power Z/Z*(p)).(z,$1) =(power INT.Ring(p)).(y,$1);
A2: P[ 0 ]
proof
thus (power Z/Z*(p)).(z,0)=1_(Z/Z*(p)) by GROUP_1:def 8
.= 1_(INT.Ring(p)) by Th21
.= (power INT.Ring(p)).(y,0) by GROUP_1:def 8;
end;
A3: now
let k be Element of NAT;
assume
A4: P[k];
(power Z/Z*(p)).(z,k+1) = (power Z/Z*(p)).(z,k)*z by GROUP_1:def 8
.=(power INT.Ring(p)).(y,k)*y by A1,A4,Lm12
.=(power INT.Ring(p)).(y,k+1) by GROUP_1:def 8;
hence P[k+1];
end;
for k be Element of NAT holds P[k] from NAT_1:sch 1(A2,A3);
hence thesis;
end;
Lm14: for p be Prime,L be Field, n be natural number st 0)`^n0-1_.(L);
set pp= (<%0.L,1.L%>)`^n0;
set qq=1_.(L);
A3: now
let x be Element of L, xz be Element of Z/Z*(p),
xn be Element of INT.Ring(p);
assume
A4: x=xz & xn =xz|^n;
A5: xn =xz|^n0 by A4
.=(power L).(x,n0) by A1,A4,Th28;
thus eval(f,x)=eval(pp,x)-eval(qq,x) by POLYNOM4:24
.= eval((<%0.L,1.L%>)`^n0,x)-1.L by POLYNOM4:21
.= (power L).(eval(<%0.L,1.L%>,x),n0)-1.L by POLYNOM5:23
.= xn -1_(INT.Ring(p)) by A1,A5,POLYNOM5:49;
end;
A6: len <%0.L,1.L%> = 2 by POLYNOM5:41;
A7: len((<%0.L,1.L%>)`^n0) = n*2-n+1 by A6,POLYNOM5:24
.=n+1;
A8: len(1_.(L)) =1 by POLYNOM4:7;
then
A9: len((<%0.L,1.L%>)`^n0) <> len(-1_.(L)) by A2,A7,POLYNOM4:11;
len (f)=max(len((<%0.L,1.L%>)`^n0),len(-1_.(L))) by A9,POLYNOM4:10
.=max(n+1,1) by A7,A8,POLYNOM4:11
.=n+1 by A2,XXREAL_0:def 9;
then deg f =n;
hence thesis by A3;
end;
theorem Th29:
for p be Prime, a,b be Element of Z/Z*(p),
n be natural number st 0< n & ord a=n & b |^n =1 holds
b is Element of gr {a}
proof
let p be Prime, a,b be Element of Z/Z*(p), n be natural number;
assume
A1: 0 < n & ord a=n & b |^n =1;
A2: 1 < p by INT_2:def 5;
assume
A3: not b is Element of gr {a};
reconsider L = INT.Ring(p) as unital (non empty doubleLoopStr);
consider f be Polynomial of L such that
A4: deg f = n & for x be Element of L, xz be Element of Z/Z*(p),
xn be Element of INT.Ring(p) st x=xz & xn =xz|^n holds
eval(f,x) = xn -1_(INT.Ring(p)) by A1,Lm14;
A5: for x be Element of Z/Z*(p) st x |^n =1 holds x in Roots(f)
proof
let x1 be Element of Z/Z*(p);
assume
A6: x1 |^n =1;
x1 in Segm0(p);
then
x1 in Segm(p) \ {0} by A2,Def2;
then
reconsider x3=x1 as Element of L by XBOOLE_0:def 4;
A7: x1|^n = 1_(Z/Z*(p)) by A6,Th21
.= 1_(INT.Ring(p)) by Th21;
x1|^n in Segm0(p);
then
x1|^n in Segm(p) \ {0} by A2,Def2;
then
reconsider x2=x1|^n as Element of INT.Ring(p) by XBOOLE_0:def 4;
eval(f,x3) = x2 - 1_(INT.Ring(p)) by A4
.=0.L by A7,RLVECT_1:28;
then
x3 is_a_root_of f by POLYNOM5:def 6;
hence x1 in Roots(f) by POLYNOM5:def 9;
end;
A8: the carrier of gr {a} c= Roots(f)
proof
let x be set;
assume
A9: x in the carrier of gr {a};
then x in gr {a} by STRUCT_0:def 5;
then x in Z/Z*(p) by GROUP_2:49;
then reconsider x1=x as Element of Z/Z*(p) by STRUCT_0:def 5;
x1 in gr {a} by A9,STRUCT_0:def 5;
then consider j be Integer such that
A10: x1 = a|^j by GR_CY_1:25;
x1|^n =a|^(j*n) by A10,GROUP_1:69
.=(a|^n)|^j by GROUP_1:68
.=(1_(Z/Z*(p))) |^j by A1,GROUP_1:82
.= 1_(Z/Z*(p)) by GROUP_1:61
.= 1 by Th21;
hence x in Roots(f) by A5;
end;
reconsider RF =Roots(f) as finite set by A4,Th27;
consider m,n0 be Element of NAT such that
A11: n0=deg f & m=Card(Roots(f)) & m <= n0 by A4,Th27;
A12: ex D being finite set st D = the carrier of (gr {a})
& ord (gr {a}) = card D;
b in Roots(f) by A1,A5;
then
{b} c= Roots(f) by ZFMISC_1:37;
then
A13: (the carrier of gr {a}) \/ {b} c= Roots(f) by A8,XBOOLE_1:8;
reconsider XX=the carrier of gr {a} as finite set;
A14: Card ( (the carrier of gr {a}) \/ {b}) =card ( XX) + 1 by A3,CARD_2:54
.=n0+1 by A1,A4,A11,A12,GR_CY_1:27;
A15: Card ( (the carrier of gr {a}) \/ {b}) <=`
Card (Roots(f)) by A13,CARD_1:27;
A16: Card m = Card (Roots(f)) by A11;
Card (n0 + 1)=Card ( (the carrier of gr {a}) \/ {b}) by A14;
then
n0 + 1 c= m by A15,A16,CARD_1:72;
then
n0 + 1 <= m by NAT_1:40;
hence contradiction by A11,NAT_1:16,XXREAL_0:2;
end;
theorem Th30:
for G be Group, z be Element of G, d,l be Element of NAT
st G is finite & ord z=d*l holds ord (z|^d)=l
proof
let G be Group, z be Element of G, d,l be Element of NAT;
assume
A1: G is finite & ord z=d*l;
reconsider H=gr {z} as strict Subgroup of G;
set m = d*l;
reconsider H as finite strict Subgroup of G by A1,GROUP_2:48;
A2: ord H = m by A1,GR_CY_1:27;
z in gr{z} by GR_CY_2:8;
then
reconsider z1=z as Element of H by STRUCT_0:def 5;
gr{z} =gr{z1} by GR_CY_2:9;
then ord (z1|^d) = l by A2,GR_CY_2:14;
hence ord (z|^d) = l by A1,GROUP_8:3,5;
end;
theorem
for p be Prime holds Z/Z*(p) is cyclic Group
proof
let p be Prime;
assume
A2: not Z/Z*(p) is cyclic Group;
A3: for x be Element of Z/Z*(p) holds ord x < ord (Z/Z*(p))
proof
let x be Element of Z/Z*(p);
A5: ord x <= ord (Z/Z*(p)) by GR_CY_1:28,NAT_D:7;
ord x <> ord (Z/Z*(p)) by A2,GR_CY_1:43;
hence thesis by A5,XXREAL_0:1;
end;
consider a be Element of Z/Z*(p);
set ZP=Z/Z*(p);
defpred P[natural number,Element of ZP,Element of ZP] means ord $2 < ord $3;
A6: for n being Element of NAT for x being Element of ZP
ex y being Element of ZP st P[n,x,y]
proof
let n being Element of NAT, x being Element of ZP;
set n=ord x;
A7: n < ord Z/Z*(p) by A3;
A8: the carrier of (gr {x}) c= the carrier of Z/Z*(p) by GROUP_2:def 5;
A9: ord gr {x} <> ord Z/Z*(p) by A7,GR_CY_1:27;
the carrier of (gr {x}) c< the carrier of Z/Z*(p) by A8,A9,XBOOLE_0:def 8;
then
(the carrier of Z/Z*(p)) \ (the carrier of (gr {x})) <> {}
by XBOOLE_1:105;
then
consider z be set such that
A10: z in (the carrier of Z/Z*(p))
\ (the carrier of (gr {x})) by XBOOLE_0:def 1;
1_(gr {x}) in the carrier of (gr {x});
then
1_ZP in the carrier of (gr {x}) by GROUP_2:53;
then
A11: 1 in the carrier of (gr {x}) by Th21;
reconsider z as Element of ZP by A10;
set m=ord z;
reconsider d= m gcd n as Nat;
A12: z <> 1 by A10,A11,XBOOLE_0:def 4;
reconsider H=gr {z } as strict Subgroup of ZP;
A13: 1 <=ord H by GROUP_1:90;
A14: ord H = m by GR_CY_1:27;
z <> 1_ZP by A12,Th21;
then
A15: 1 < m by A13,A14,GROUP_1:85,XXREAL_0:1;
now per cases;
suppose
A16: d = 1;
take y=x*z;
1 <=ord gr {x} by GROUP_1:90;
then
1 <= n by GR_CY_1:27;
then
1*n < m*n by A15,XREAL_1:70;
hence n < ord y by A16,Th25;
end;
suppose d <> 1;
1 <=ord gr {x} by GROUP_1:90;
then
A17: 1 <= n by GR_CY_1:27;
1 <=ord gr {z} by GROUP_1:90;
then
A18: 1 <= m by GR_CY_1:27;
set l= m lcm n;
consider m0,n0 be Element of NAT such that
A19: l=n0*m0 & n0 gcd m0 = 1 & n0 divides n
& m0 divides m & n0 <> 0 & m0 <> 0 by A17,A18,Th17;
consider j be Integer such that
A20: n=n0* j by A19,INT_1:def 9;
A21: n/n0= j by A19,A20,XCMPLX_1:90;
reconsider d1=n/n0 as Element of NAT by A21,INT_1:16;
consider u be Integer such that
A22: m=m0* u by A19,INT_1:def 9;
A23: m/m0 = u by A19,A22,XCMPLX_1:90;
reconsider d2=m/m0 as Element of NAT by A23,INT_1:16;
take y =(x|^d1)*(z|^d2);
n=(n/n0)*n0 by A19,XCMPLX_1:88;
then
A24: ord (x|^d1) = n0 by Th30;
m=(m/m0)*m0 by A19,XCMPLX_1:88;
then
ord (z|^d2) = m0 by Th30;
then
A25: ord y = m0*n0 by A19,A24,Th25;
A26: not m divides n
proof
assume
A27: m divides n;
consider j be Integer such that
A28: n=m* j by A27,INT_1:def 9;
A29: z |^n =(z |^m)|^j by A28,GROUP_1:68
.= (1_(Z/Z*(p)))|^j by GROUP_1:82
.= 1_(Z/Z*(p)) by GROUP_1:61
.= 1 by Th21;
z is Element of gr {x} by A17,A29,Th29;
hence contradiction by A10,XBOOLE_0:def 4;
end;
A30: n <> l by A26,INT_2:25;
A31: n divides (m lcm n) by INT_2:25;
consider j be Integer such that
A32: l=n* j by A31,INT_1:def 9;
l/n = j by A17,A32,XCMPLX_1:90;
then
A33: j is Element of NAT by INT_1:16;
j <> 0 by A17,A18,A32,INT_2:4;
then n*1 <=n*j by A33,NAT_1:14,XREAL_1:66;
hence n < ord y by A19,A25,A30,A32,XXREAL_0:1;
end;
end;
hence thesis;
end;
consider f being Function of NAT,the carrier of ZP such that
A34: f.0 = a & for n being Element of NAT holds P[n,f.n,f.(n+1)]
from RECDEF_1:sch 2(A6);
deffunc F(Element of NAT) =ord (f.$1);
consider g be Function of NAT,NAT such that
A35: for k be Element of NAT holds g.k=F(k) from FUNCT_2:sch 4;
A36: now
let k be Element of NAT;
A37: g.k = ord (f.k) by A35;
g.(k+1) = ord (f.(k+1)) by A35;
hence g.k < g.(k+1) by A34,A37;
end;
A38: for k,m be Element of NAT holds g.k< g.(k+1+m)
proof
let k be Element of NAT;
defpred P[Nat] means g.k< g.(k+1+$1);
A39: P[ 0 ] by A36;
A40: now
let m be Element of NAT;
assume
A41: P[m];
g.(k+1+m) < g.((k+1+m) + 1) by A36;
hence P[m+1] by A41,XXREAL_0:2;
end;
for m be Element of NAT holds P[m] from NAT_1:sch 1(A39,A40);
hence thesis;
end;
A42: for k,m be Element of NAT st k < m holds g.k< g.m
proof
let k,m be Element of NAT;
assume
A43: k < m;
m-k is Element of NAT by A43,INT_1:18;
then reconsider mk=m-k as Nat;
m-k <> 0 by A43;
then
consider n0 be Nat such that
A44: mk=n0+1 by NAT_1:6;
reconsider n=n0 as Element of NAT by ORDINAL1:def 13;
m=k+1+n by A44;
hence thesis by A38;
end;
g is one-to-one
proof
now
let x1,x2 be set;
assume
A45: x1 in NAT & x2 in NAT & g.x1 = g.x2;
then
reconsider xx1=x1,xx2=x2 as Element of NAT;
A46: xx1 <= xx2 by A42,A45;
xx2 <= xx1 by A42,A45;
hence x2=x1 by A46,XXREAL_0:1;
end;
hence thesis by FUNCT_2:25;
end;
then dom g,rng g are_equipotent by WELLORD2:def 4;
then
A47: Card (dom g) = Card (rng g) by CARD_1:21;
A48: rng g c= Segm(ord ZP)
proof
let y be set;
assume y in rng g;
then consider x be set such that
A49: x in NAT & y=g.x by FUNCT_2:17;
reconsider x as Element of NAT by A49;
reconsider gg=g.x as Element of NAT;
g.x =ord (f.x) by A35;
then
gg < ord ZP by A3;
hence y in Segm(ord ZP) by A49,ALGSEQ_1:10;
end;
A50: rng g is finite by A48,FINSET_1:13;
Card rng g = Card NAT by A47,FUNCT_2:def 1;
then not Card rng g is finite by CARD_4:1;
hence contradiction by A50,CARD_4:1;
end;