:: Uniqueness of factoring an integer and multiplicative group $Z/pZ^{*}$
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received January 31, 2008
:: Copyright (c) 2008-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, 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 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;
constructors 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;
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;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions GROUP_1, REALSET1, TARSKI;
equalities STRUCT_0, GROUP_1, INT_3, ALGSTR_0, BINOP_1, FINSEQ_1, POLYNOM3,
HURWITZ, REALSET1, ORDINAL1;
expansions STRUCT_0, GROUP_1, HURWITZ, 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;
begin :: Uniqueness of factoring an integer
reserve x,y for object, X for set;
Lm1: for z be object st z<> x holds (X-->0)+*(x,y).z=0
proof
let z be object;
assume
A1: z <>x;
A2: dom (X-->0)=X by FUNCOP_1:13;
per cases;
suppose
A3: z in X;
(X-->0)+*(x,y).z=(X--> 0).z by A1,FUNCT_7:32
.=0 by A3,FUNCOP_1:7;
hence thesis;
end;
suppose
A4: not z in X;
(X-->0)+*(x,y).z=(X--> 0).z by A1,FUNCT_7:32
.=0 by A2,A4,FUNCT_1:def 2;
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};
A2: for y being object st y in dom p holds p.y=(X-->0)+*(x,p.x).y
proof
let y be object;
assume y in dom p;
then y in X;
then
A3: y in dom (X-->0) by FUNCOP_1:13;
per cases;
suppose
x=y;
hence thesis by A3,FUNCT_7:31;
end;
suppose
A4: x<>y;
then not y in support p by A1,TARSKI:def 1;
then p.y=0 by PRE_POLY:def 7;
hence thesis by A4,Lm1;
end;
end;
dom ((X-->0)+*(x,p.x)) = dom (X-->0) by FUNCT_7:30
.= X by FUNCOP_1:13;
then dom p = dom ((X-->0)+*(x,p.x)) by PARTFUN1:def 2;
hence thesis by A2,FUNCT_1:2;
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 that
A1: (support p) /\ (support q) = {} and
A2: (support p) \/ (support q) =(support r) and
A3: p| (support p) = r | (support p) and
A4: q| (support q) = r | (support q);
for x being object st x in X holds r.x=p.x+q.x
proof
let x being object;
assume x in X;
per cases;
suppose
A5: x in (support p) \/ (support q);
now
per cases by A5,XBOOLE_0:def 3;
suppose
A6: x in support p;
then
A7: not x in support q by A1,XBOOLE_0:def 4;
thus r.x=r| (support p).x by A6,FUNCT_1:49
.=p.x +0 by A3,A6,FUNCT_1:49
.=p.x + q.x by A7,PRE_POLY:def 7;
end;
suppose
A8: x in (support q);
then
A9: not x in support p by A1,XBOOLE_0:def 4;
thus r.x=r| (support q).x by A8,FUNCT_1:49
.=0 +q.x by A4,A8,FUNCT_1:49
.=p.x + q.x by A9,PRE_POLY:def 7;
end;
end;
hence thesis;
end;
suppose
A10: not x in (support p) \/ (support q);
then
A11: not x in (support q) by XBOOLE_0:def 3;
A12: not x in (support p) by A10,XBOOLE_0:def 3;
thus r.x = 0 by A2,A10,PRE_POLY:def 7
.= 0 + q.x by A11,PRE_POLY:def 7
.=p.x+q.x by A12,PRE_POLY:def 7;
end;
end;
hence r=p+q by PRE_POLY:33;
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;
A1: dom (p| (support p)) = dom p /\ (support p) by RELAT_1:61
.=support p by PRE_POLY:37,XBOOLE_1:28;
A2: dom (q| (support q)) =dom q /\ (support q) by RELAT_1:61
.=support q by PRE_POLY:37,XBOOLE_1:28;
assume
A3: p| (support p) = q| (support q);
A4: for x being object st x in X holds p.x=q.x
proof
let x being object;
assume x in X;
per cases;
suppose
A5: x in support p;
hence p.x=p| (support p).x by FUNCT_1:49
.=q.x by A3,A1,A2,A5,FUNCT_1:49;
end;
suppose
A6: not x in support p;
hence p.x = 0 by PRE_POLY:def 7
.=q.x by A3,A1,A2,A6,PRE_POLY:def 7;
end;
end;
A7: dom q = X by PARTFUN1:def 2;
dom p = X by PARTFUN1:def 2;
hence thesis by A4,A7,FUNCT_1:2;
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 that
A1: support p = {} and
A2: support q={};
A3: {} = dom q /\ {} .= dom (q| (support q)) by A2;
A4: dom (p| (support p)) =dom p /\ (support p) by RELAT_1:61
.= {} by A1;
then
for x be object st x in dom (p| (support p)) holds (p| (support p)).x = (q|
(support q)).x;
hence thesis by A4,A3,Th3,FUNCT_1:2;
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
deffunc G(object) = 0;
let p,q be bag of SetPrimes;
assume that
A1: (support p) c= (support q) and
A2: p | (support p) =q | (support p);
deffunc F(object) = q.$1;
defpred C[object] means $1 in (support q) \ (support p);
A3: for x be object st x in SetPrimes holds
(C[ x] implies F(x) in NAT) & (not C[ x] implies G(x) in NAT)
by ORDINAL1:def 12;
consider f being Function of SetPrimes,NAT such that
A4: for x be object 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(A3);
A5: 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 that
x in SetPrimes and
A6: x in (support q) \ (support p);
x in support q by A6,XBOOLE_0:def 5;
then q.x<>0 by PRE_POLY:def 7;
hence thesis by A4,A6;
end;
A7: for x st not x in SetPrimes holds f.x=0
proof
let x;
assume not x in SetPrimes;
then not x in dom f;
hence thesis by FUNCT_1:def 2;
end;
A8: for x holds x in (support q) \ (support p) iff f.x<>0
proof
let x;
per cases;
suppose
x in SetPrimes;
hence thesis by A4,A5;
end;
suppose
not x in SetPrimes;
hence thesis by A7;
end;
end;
then support f is finite by PRE_POLY:def 7;
then reconsider r = f as bag of SetPrimes by PRE_POLY:def 8;
A9: (support p) \/ (support r) =(support p) \/ ((support q) \ (support p))
by A8,PRE_POLY:def 7
.=(support p) \/ (support q) by XBOOLE_1:39
.=(support q) by A1,XBOOLE_1:12;
A10: dom (f| (support f)) =(dom f)/\ support f by RELAT_1:61
.=support f by PRE_POLY:37,XBOOLE_1:28;
A11: (support f)=(support q) \ (support p) by A8,PRE_POLY:def 7;
A12: for x be object st x in dom (f| (support f))
holds (f|support f).x =(q|support f).x
proof
let x be object;
assume
A13: x in dom (f| (support f));
then
A14: (q| (support f)).x=q.x by A10,FUNCT_1:49;
(f| (support f)).x=f.x by A10,A13,FUNCT_1:49;
hence thesis by A4,A11,A10,A13,A14;
end;
dom (q| (support f)) =(dom q)/\ support f by RELAT_1:61
.=(dom q)/\ ((support q) \ (support p)) by A8,PRE_POLY:def 7
.= ((dom q)/\ (support q)) \ (support p) by XBOOLE_1:49
.= (support q) \ (support p) by PRE_POLY:37,XBOOLE_1:28
.=support f by A8,PRE_POLY:def 7;
then
A15: f | (support f) =q | (support f) by A10,A12,FUNCT_1:def 11;
A16: (support p) misses (support f)
proof
assume (support p) meets (support f);
then ex x be object st x in support p & x in support f by XBOOLE_0:3;
hence contradiction by A11,XBOOLE_0:def 5;
end;
then (support p) /\ (support f) = {} by XBOOLE_0:def 7;
then p+r = q by A2,A15,A9,Th2;
hence thesis by A11,A16,A15;
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;
set fq =p +* (X --> 0);
A3: rng fq c= NAT;
set fr = p +* (SetPrimes \X -->0);
A4: dom fr = dom p \/ dom (SetPrimes \ X -->0) by FUNCT_4:def 1
.=dom p \/ (SetPrimes \ X) by FUNCOP_1:13
.= SetPrimes \/ (SetPrimes \X) by PARTFUN1:def 2
.= SetPrimes by XBOOLE_1:12,36;
rng fr c= NAT;
then reconsider fr as Function of SetPrimes,NAT by A4,FUNCT_2:def 1
,RELSET_1:4;
assume
A6: X c= support p;
A7: not x in X & x in SetPrimes implies fr.x = 0
proof
assume that
A8: not x in X and
A9: x in SetPrimes;
A10: x in SetPrimes \ X by A8,A9,XBOOLE_0:def 5;
then x in dom(SetPrimes \ X --> 0) by FUNCOP_1:13;
then fr.x = (SetPrimes \ X --> 0).x by FUNCT_4:13;
hence thesis by A10,FUNCOP_1:7;
end;
A11: dom(X --> 0) = X by FUNCOP_1:13;
then dom fq = dom p \/ X by FUNCT_4:def 1
.= SetPrimes \/ X by PARTFUN1:def 2
.= SetPrimes by A6,XBOOLE_1:1,12;
then reconsider fq as Function of SetPrimes,NAT by A3,FUNCT_2:def 1
,RELSET_1:4;
A12: dom (fq| (support fq)) =(dom fq)/\ support fq by RELAT_1:61
.=support fq by PRE_POLY:37,XBOOLE_1:28;
A13: for x st not x in SetPrimes holds fr.x=0 &fq.x=0
proof
let x;
assume
A14: not x in SetPrimes;
then
A15: not x in dom fr;
not x in dom fq by A14;
hence thesis by A15,FUNCT_1:def 2;
end;
A16: x in X implies fr.x =p.x
proof
assume x in X;
then not x in dom(SetPrimes \ X --> 0) by XBOOLE_0:def 5;
hence thesis by FUNCT_4:11;
end;
A17: for x st x in SetPrimes & x in X holds fr.x<>0
proof
let x;
assume that
x in SetPrimes and
A18: x in X;
p.x<>0 by A6,A18,PRE_POLY:def 7;
hence thesis by A16,A18;
end;
A19: for x holds x in X iff fr.x<>0
proof
let x;
now
per cases;
suppose
x in SetPrimes;
hence thesis by A7,A17;
end;
suppose
A20: not x in SetPrimes;
X c= SetPrimes by A6,XBOOLE_1:1;
hence thesis by A13,A20;
end;
end;
hence thesis;
end;
then
A21: (support fr) = X by PRE_POLY:def 7;
then reconsider r = fr as bag of SetPrimes by A6,PRE_POLY:def 8;
A22: support p c= dom p by PRE_POLY:37;
A23: dom (fr| (support fr)) =(dom fr)/\ support fr by RELAT_1:61
.=support fr by PRE_POLY:37,XBOOLE_1:28
.= X by A19,PRE_POLY:def 7;
A24: for x be object st x in dom (fr| (support fr))
holds (fr|support fr).x =(p|support fr).x
proof
let x be object;
assume
A25: x in dom (fr| (support fr));
then
A26: (p| (support fr)).x=p.x by A21,A23,FUNCT_1:49;
(fr| (support fr)).x=fr.x by A21,A23,A25,FUNCT_1:49;
hence thesis by A16,A23,A25,A26;
end;
dom (p| (support fr)) =(dom p)/\ support fr by RELAT_1:61
.=(dom p)/\ X by A19,PRE_POLY:def 7
.=X by A6,A22,XBOOLE_1:1,28;
then
A27: fr | (support fr) =p | (support fr) by A23,A24,FUNCT_1:def 11;
A28: x in X implies fq.x = 0
proof
assume
A29: x in X;
hence fq.x = (X --> 0).x by A11,FUNCT_4:13
.= 0 by A29,FUNCOP_1:7;
end;
A30: for x holds x in (support p) \ X iff fq.x<>0
proof
let x;
per cases;
suppose
x in X;
hence thesis by A28,XBOOLE_0:def 5;
end;
suppose
A31: not x in X;
then
A32: fq.x=p.x by A11,FUNCT_4:11;
per cases;
suppose
x in support p;
hence thesis by A31,A32,PRE_POLY:def 7,XBOOLE_0:def 5;
end;
suppose
not x in support p;
hence thesis by A32,PRE_POLY:def 7,XBOOLE_0:def 5;
end;
end;
end;
then
A33: support fq = support p \ X by PRE_POLY:def 7;
then reconsider q = fq as bag of SetPrimes by PRE_POLY:def 8;
A34: dom (p| (support fq)) =(dom p)/\ support fq by RELAT_1:61
.=(dom p)/\ (support p \ X) by A30,PRE_POLY:def 7
.= ((dom p)/\ (support p)) \ X by XBOOLE_1:49
.= (support p) \ X by PRE_POLY:37,XBOOLE_1:28
.=support fq by A30,PRE_POLY:def 7;
(support p \ X) misses X by XBOOLE_1:79;
then
A35: (support fq) /\ (support fr) = {} by A21,A33,XBOOLE_0:def 7;
A36: for x be set st x in SetPrimes & x in (support fq) holds p.x=fq.x
proof
let x be set;
assume that
x in SetPrimes and
A37: x in (support fq);
not x in X by A21,A35,A37,XBOOLE_0:def 4;
hence thesis by A11,FUNCT_4:11;
end;
for x be object st x in dom (fq| (support fq))
holds (fq| (support fq)).x =(p| (support fq)).x
proof
let x be object;
assume
A38: x in dom (fq| (support fq));
then
A39: (p| (support fq)).x=p.x by A12,FUNCT_1:49;
(fq| (support fq)).x=fq.x by A12,A38,FUNCT_1:49;
hence thesis by A12,A36,A38,A39;
end;
then
A40: fq| (support fq)=p| (support fq) by A12,A34,FUNCT_1:def 11;
(support fr) \/ (support fq) =(support fr) \/(support p \ support fr)
by A19,A33,PRE_POLY:def 7
.=(support fr) \/(support p) by XBOOLE_1:39
.= support p by A6,A21,XBOOLE_1:12;
then q+r=p by A35,A40,A27,Th2;
hence thesis by A21,A33,A40,A27,XBOOLE_1:79;
end;
definition
let p be bag of SetPrimes;
attr p is prime-factorization-like means
for x being Prime st x in
support p ex n be Nat st 0 < n & p.x = x |^n;
end;
registration
let n be non zero Nat;
cluster ppf n -> prime-factorization-like;
coherence
proof
let p be Prime;
assume
A1: p in support ppf n;
A2: p |-count n <>0
proof
assume p |-count n =0;
then (ppf n).p=0 by NAT_3:55;
hence contradiction by A1,PRE_POLY:def 7;
end;
take p |-count n;
p in support pfexp n by A1,NAT_3:def 9;
hence thesis by A2,NAT_3:def 9;
end;
end;
theorem Th5:
for p,q be Prime,n,m be Nat st p divides m*(q|^n) & p
<> q holds p divides m
proof
let p,q be Prime;
let n,m be Nat;
assume that
A1: p divides m*(q|^n) and
A2: p <> q;
p divides m or p divides (q|^n) by A1,NEWTON:80;
hence thesis by A2,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 Nat st a|^n
divides Product b
proof
let a be Prime, b be bag of SetPrimes;
assume that
A1: b is prime-factorization-like and
A2: a in support b;
consider n be Nat such that
A3: 0 < n and
A4: b.a = a |^n by A1,A2;
A5: a divides b.a by A3,A4,NAT_3:3;
A6: rng b c= NAT;
a in rng canFS(support b) by A2,FUNCT_2:def 3;
then consider d be object such that
A7: d in dom canFS(support b) and
A8: a=(canFS(support b)).d by FUNCT_1:def 3;
consider f being FinSequence of COMPLEX such that
A9: Product b = Product f and
A10: f = b*canFS(support b) by NAT_3:def 5;
rng f c= rng b by A10,RELAT_1:26;
then rng f c= NAT by A6;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
A11: rng canFS(support b) = support b by FUNCT_2:def 3;
support b c= dom b by PRE_POLY:37;
then
A12: dom f = dom canFS(support b) by A10,A11,RELAT_1:27;
then b.a=(b*(canFS(support b))).d by A10,A7,A8,FUNCT_1:12;
then b.a in rng f by A10,A12,A7,FUNCT_1:3;
then (a |^n) divides (Product f) by A4,NAT_3:7;
hence thesis by A9,A4,A5,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
deffunc G(set) = 0;
let p be FinSequence of NAT,x be Element of NAT, b be bag of SetPrimes;
assume that
A1: b is prime-factorization-like and
A2: ( p^<*x*>) = b*canFS(support b);
A3: rng canFS(support b) = support b by FUNCT_2:def 3;
dom b = SetPrimes by PARTFUN1:def 2;
then
A4: dom (b*canFS(support b)) = dom (canFS(support b)) by A3,RELAT_1:27;
p = (b*canFS(support b)) | (dom p) by A2,FINSEQ_1:21;
then dom p = dom (b*canFS(support b)) /\ (dom p) by RELAT_1:61;
then
A5: dom ((canFS(support b)) | (dom p)) = dom p by A4,RELAT_1:62,XBOOLE_1:17;
deffunc F(set) = b.$1;
A6: card (support b) = len canFS(support b) by FINSEQ_1:93;
dom b = SetPrimes by PARTFUN1:def 2;
then
A7: dom (b*canFS(support b)) = dom (canFS(support b)) by A3,RELAT_1:27;
A8: len p + 1 in Seg (len p + 1) by FINSEQ_1:4;
A9: len <*x*> = 1 by FINSEQ_1:40;
then len (p^<*x*>) = len p + 1 by FINSEQ_1:22;
then
A10: (len p + 1) in dom (b*canFS(support b)) by A2,A8,FINSEQ_1:def 3;
A11: x =(p^<*x*>) .(len p + 1) by FINSEQ_1:42
.= b.((canFS(support b)).(len p + 1)) by A2,A7,A10,FUNCT_1:13;
A12: rng canFS(support b) =support b by FUNCT_2:def 3;
then
A13: (canFS(support b)).(len p + 1) in support b by A7,A10,FUNCT_1:3;
then reconsider q=(canFS(support b)).(len p + 1) as Prime by NEWTON:def 6;
defpred P[set] means $1 in support b \ {q};
consider b1 being ManySortedSet of SetPrimes such that
A14: 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;
A15: rng b1 c= NAT
proof
let y be object;
assume y in rng b1;
then consider x be object such that
A16: x in dom b1 and
A17: y=b1.x by FUNCT_1:def 3;
reconsider x as Element of SetPrimes by A16;
b1.x in NAT
proof
per cases;
suppose
x in support b \ {q};
then b1.x = b.x by A14;
hence thesis;
end;
suppose
not x in support b \ {q};
then b1.x = 0 by A14;
hence thesis;
end;
end;
hence thesis by A17;
end;
now
let z be object;
assume
A18: z in support b1;
z in dom b1
proof
assume not z in dom b1;
then b1.z = {} by FUNCT_1:def 2;
hence contradiction by A18,PRE_POLY:def 7;
end;
then reconsider y = z as Element of SetPrimes;
assume
A19: not z in (support b) \ {q};
b1.y <> 0 by A18,PRE_POLY:def 7;
hence contradiction by A14,A19;
end;
then
A20: support b1 c= (support b) \ {q};
now
let z be object;
assume
A21: z in (support b) \ {q};
then
A22: z in support b by XBOOLE_0:def 5;
reconsider y = z as Element of SetPrimes by A21;
b1.y =b.y by A14,A21;
then b1. y <> 0 by A22,PRE_POLY:def 7;
hence z in support b1 by PRE_POLY:def 7;
end;
then
A23: (support b) \ {q} c= support b1;
then
A24: support b1 = (support b) \ {q} by A20,XBOOLE_0:def 10;
reconsider b1 as bag of SetPrimes by A20,A15,PRE_POLY:def 8,VALUED_0:def 6;
consider n be Nat such that
A25: 0 < n and
A26: b.q = q |^n by A1,A13;
reconsider n as Element of NAT by ORDINAL1:def 12;
A27: rng canFS(support b) =support b by FUNCT_2:def 3;
SetPrimes = dom b by PARTFUN1:def 2;
then card dom (b*canFS(support b)) =card dom (canFS(support b)) by A27,
RELAT_1:27
.=card Seg len (canFS(support b)) by FINSEQ_1:def 3
.= card len (canFS(support b)) by FINSEQ_1:55
.= len (canFS(support b));
then
A28: len canFS(support b) = card Seg len ((p^<*x*>)) by A2,FINSEQ_1:def 3
.= card len ((p^<*x*>)) by FINSEQ_1:55
.= len p + 1 by A9,FINSEQ_1:22;
card( (support b) \ {q}) =card( (support b)) - card({q}) by A7,A12,A10,
EULER_1:4,FUNCT_1:3
.=card( (support b)) - 1 by CARD_1:30;
then
A29: len (canFS(support b1)) =len p by A24,A28,A6,FINSEQ_1:93;
then
A30: dom (canFS(support b1)) = Seg len p by FINSEQ_1:def 3;
then
A31: dom canFS(support b1) = dom p by FINSEQ_1:def 3;
A32: now
let x be Prime;
assume
A33: x in support b1;
support b \ {q} c= support b by XBOOLE_1:36;
then consider m be Nat such that
A34: 0 < m and
A35: b.x = x |^m by A1,A24,A33;
take m;
thus 0 < m by A34;
thus b1.x=x |^m by A14,A20,A33,A35;
end;
per cases;
suppose
A36: dom p = {};
set p1=b1*canFS(support b1);
A37: p = {} by A36;
Seg len canFS(support b1) = dom canFS(support b1) by FINSEQ_1:def 3
.= Seg len p by A29,FINSEQ_1:def 3
.= Seg 0 by A37;
then canFS(support b1) = {};
then
A38: p1 = <*>NAT;
then reconsider p1 as FinSequence of NAT;
take p1,q,n,b1;
thus thesis by A7,A12,A10,A11,A25,A26,A20,A23,A32,A36,A38,FUNCT_1:3
,RELAT_1:41,XBOOLE_0:def 10;
end;
suppose
A39: dom p <> {};
A40: rng canFS(support b) = support b by FUNCT_2:def 3;
now
let y be object;
assume
A41: y in ((support b) \ {q});
then y in rng canFS(support b) by A40,XBOOLE_0:def 5;
then consider x be object such that
A42: x in dom (canFS(support b)) and
A43: y=(canFS(support b)).x by FUNCT_1:def 3;
A44: x in dom p
proof
assume not x in dom p;
then
A45: not x in Seg len p by FINSEQ_1:def 3;
A46: x in Seg (len p + 1) by A28,A42,FINSEQ_1:def 3;
reconsider x as Element of NAT by A42;
1 <=x by A46,FINSEQ_1:1;
then len p < x by A45;
then
A47: len p+ 1 <= x by NAT_1:13;
x <= len p + 1 by A46,FINSEQ_1:1;
then x = len p + 1 by A47,XXREAL_0:1;
then y in {q} by A43,TARSKI:def 1;
hence contradiction by A41,XBOOLE_0:def 5;
end;
then x in dom (canFS(support b)) /\ (dom p) by A42,XBOOLE_0:def 4;
then
A48: x in dom ((canFS(support b)) | (dom p)) by RELAT_1:61;
y = ((canFS(support b)) | (dom p)).x by A43,A44,FUNCT_1:49;
hence y in rng ((canFS(support b)) | (dom p)) by A48,FUNCT_1:3;
end;
then
A49: ((support b) \ {q}) c= rng ((canFS(support b)) | (dom p));
now
let y be object;
assume y in rng ((canFS(support b)) | (dom p));
then consider x be object such that
A50: x in dom ((canFS(support b)) | (dom p)) and
A51: y=((canFS(support b)) | (dom p)).x by FUNCT_1:def 3;
A52: y= (canFS(support b)).x by A50,A51,FUNCT_1:47;
A53: x in dom (canFS(support b)) /\ (dom p) by A50,RELAT_1:61;
then
A54: x in dom (canFS(support b)) by XBOOLE_0:def 4;
A55: x in dom p by A53,XBOOLE_0:def 4;
y <> q
proof
len p + 1 in Seg (len p + 1) by FINSEQ_1:4;
then
A56: len p + 1 in dom canFS(support b) by A28,FINSEQ_1:def 3;
assume y=q;
then len p+1 = x by A52,A54,A56,FUNCT_1:def 4;
then
A57: len p + 1 in Seg len p by A55,FINSEQ_1:def 3;
len p + 0 < 1+ len p by XREAL_1:8;
hence contradiction by A57,FINSEQ_1:1;
end;
then
A58: not y in {q} by TARSKI:def 1;
y in rng (canFS(support b)) by A52,A54,FUNCT_1:3;
hence y in (support b) \ {q} by A58,XBOOLE_0:def 5;
end;
then rng ((canFS(support b)) | (dom p)) c= ((support b) \ {q});
then
A59: rng ((canFS(support b)) | (dom p))= ((support b) \ {q}) by A49,
XBOOLE_0:def 10;
then reconsider L0= (canFS(support b)) | (dom p) as Function of (dom p),((
support b) \ {q}) by A5,FUNCT_2:1;
A60: L0 is one-to-one by FUNCT_1:52;
then
A61: dom (L0") = (support b) \ {q} by A59,FUNCT_1:33;
A62: (support b) \ {q} <> {} by A20,A30,A39,FINSEQ_1:def 3;
then dom L0 = dom p by FUNCT_2:def 1;
then
A63: rng (L0") = dom p by A60,FUNCT_1:33;
then reconsider LL1 = L0" as Function of (support b) \ {q},dom p by A61,
FUNCT_2:1;
A64: rng canFS(support b1) =support b1 by FUNCT_2:def 3;
then canFS(support b1) is Function of (dom p),(support b) \ {q} by A24,A31,
FUNCT_2:1;
then reconsider
L0L=LL1*canFS(support b1) as Function of (dom p),(dom p) by A62,FUNCT_2:13;
A65: L0 is one-to-one by FUNCT_1:52;
rng L0L = dom p by A23,A61,A63,A64,RELAT_1:28;
then L0L is onto by FUNCT_2:def 3;
then reconsider LL = L0L as Permutation of (dom p) by A65;
( (canFS(support b)) | dom p) * LL = ( ( (canFS(support b)) | dom p)
* LL1)*canFS(support b1) by RELAT_1:36
.= (id (support b1)) * canFS(support b1) by A24,A62,A59,A65,FUNCT_2:29
.=canFS(support b1) by FUNCT_2:17;
then
A66: canFS(support b1)*LL" =( (canFS(support b)) | dom p)* (LL*LL") by
RELAT_1:36;
reconsider FS=canFS(support b1) as FinSequence;
reconsider L= LL" as Permutation of dom p;
A67: rng L = dom FS by A31,FUNCT_2:def 3;
then
A68: dom (FS*L) = dom L by RELAT_1:27
.=dom p by A39,FUNCT_2:def 1;
set p1=b1*FS;
A69: rng canFS(support b1) =support b1 by FUNCT_2:def 3;
SetPrimes = dom b1 by PARTFUN1:def 2;
then
A70: dom (b1*FS) =dom p by A31,A69,RELAT_1:27;
then dom p1 = Seg len p by FINSEQ_1:def 3;
then
A71: p1 is FinSequence by FINSEQ_1:def 2;
A72: rng (FS*L) = rng FS by A67,RELAT_1:28
.= (support b) \ {q} by A24,FUNCT_2:def 3;
SetPrimes = dom b1 by PARTFUN1:def 2;
then
A73: dom p = dom (b1*(FS*L)) by A68,A72,RELAT_1:27;
rng LL= dom p by FUNCT_2:def 3;
then
A74: canFS(support b1)*LL" =( (canFS(support b)) | dom p)* (id (dom p)) by A39
,A66,FUNCT_2:29;
now
let k be object;
A75: dom p c=dom (p^<*x*>) by FINSEQ_1:26;
assume
A76: k in dom p;
then
A77: (FS*L).k in support b \ {q} by A68,A72,FUNCT_1:3;
thus p.k = (p^<*x*>).k by A76,FINSEQ_1:def 7
.=b.((canFS(support b)).k) by A2,A76,A75,FUNCT_1:12
.=b.(((canFS(support b)) | (dom p)).k) by A76,FUNCT_1:49
.=b.((FS*L).k) by A74,FUNCT_2:17
.=b1.((FS*L).k) by A14,A77
.= (b1*(FS*L)).k by A73,A76,FUNCT_1:12;
end;
then p=b1*(FS*L) by A73,FUNCT_1:2
.=p1*L by RELAT_1:36;
then
A78: p,p1 are_fiberwise_equipotent by A70,CLASSES1:80;
rng p1 c= NAT;
then reconsider p1 as FinSequence of NAT by A71,FINSEQ_1:def 4;
take p1,q,n,b1;
Seg len p1 =dom p by A70,FINSEQ_1:def 3;
hence thesis by A7,A12,A10,A11,A25,A26,A20,A23,A32,A78,EULER_2:10
,FINSEQ_1:def 3,FUNCT_1:3,XBOOLE_0:def 10;
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[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: for k being Nat st P[k] holds P[k+1]
proof
let k be Nat;
assume
A2: P[k];
thus P[k+1]
proof
A3: 1<= (k+1) by NAT_1:11;
let f be FinSequence of NAT, b be bag of SetPrimes, a be Prime;
assume that
A4: len f =k+1 and
A5: b is prime-factorization-like and
Product b <> 1 and
A6: a divides Product b and
A7: Product b = Product f and
A8: f = b*canFS(support b);
reconsider p=f|k as FinSequence of NAT;
reconsider x=f.(k+1) as Element of NAT;
A9: len p = k by A4,FINSEQ_1:59,NAT_1:11;
A10: f = (f|k)^<*f/.len f*> by A4,FINSEQ_5:21
.= p^ <*x*> by A4,A3,FINSEQ_4:15;
then consider
p1 being FinSequence of NAT, q be Prime,n be Element of NAT, b1
be bag of SetPrimes such that
0 < n and
A11: b1 is prime-factorization-like and
A12: q in support b and
A13: support b1 = support b \ {q} and
A14: x= q|^n and
A15: len p1=len p and
A16: Product p = Product p1 and
A17: p1=b1*canFS(support b1) by A5,A8,Lm5;
A18: Product(f)=Product (p1) * x by A10,A16,RVSUM_1:96;
rng p1 c= COMPLEX by NUMBERS:20;
then p1 is FinSequence of COMPLEX by FINSEQ_1:def 4;
then
A19: Product (b1) = Product p1 by A17,NAT_3:def 5;
now
per cases;
suppose
A20: Product (p1) = 1;
a <> 1 by INT_2:def 4;
then ex k being Element of NAT st a = q*k by A6,A7,A14,A18,A20,
PEPIN:32;
then
A21: q divides a by INT_1:def 3;
q <> 1 by INT_2:def 4;
hence thesis by A12,A21,INT_2:def 4;
end;
suppose
A22: Product (p1) <> 1;
per cases;
suppose
a=q;
hence thesis by A12;
end;
suppose
A23: a<>q;
A24: support b1 c= support b by A13,XBOOLE_1:36;
a in support b1 by A2,A6,A7,A9,A11,A14,A15,A17,A18,A19,A22,A23,Th5;
hence thesis by A24;
end;
end;
end;
hence thesis;
end;
end;
A25: P[ 0 ]
proof let f be FinSequence of NAT, b be bag of SetPrimes, a be Prime;
assume len f =0;
then f =<*>NAT;
hence thesis by RVSUM_1:94;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A25,A1);
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 that
A1: b is prime-factorization-like and
A2: Product b <> 1 and
A3: a divides Product b and
A4: Product b = Product f and
A5: f = b*canFS(support b);
len f is Element of NAT;
hence thesis by A1,A2,A3,A4,A5,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 that
A1: b is prime-factorization-like and
A2: a divides Product b;
per cases;
suppose
A3: Product b = 1;
a <> 1 by INT_2:def 4;
hence thesis by A2,A3,WSIERP_1:15;
end;
suppose
A4: Product b <> 1;
A5: rng b c= NAT;
consider f being FinSequence of COMPLEX such that
A6: Product b = Product f and
A7: f = b*canFS(support b) by NAT_3:def 5;
rng f c= rng b by A7,RELAT_1:26;
then rng f c= NAT by A5;
then reconsider f as FinSequence of NAT by FINSEQ_1:def 4;
Product b = Product f by A6;
hence thesis by A1,A2,A4,A7,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 that
A1: (support p) c= (support q) and
A2: p | (support p) =q | (support p);
consider r be bag of SetPrimes such that
support r =(support q) \ (support p) and
A3: (support p) misses (support r) and
r | (support r) = q| ( support r) and
A4: p+r = q by A1,A2,Lm2;
(Product p)*(Product r) = Product (q) by A3,A4,NAT_3:19;
hence thesis by INT_1:def 3;
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 zero Nat st k = n lcm m holds
support ppf k=(support ppf n) \/ (support ppf m)
proof
let n,m,k be non zero Nat;
assume
A1: k = n lcm m;
A2: support ppf n = support pfexp n by NAT_3:def 9;
A3: support pfexp n \/ support pfexp m c= support max(pfexp n,pfexp m)
proof
let x be object;
assume
A4: x in support pfexp n \/ support pfexp m;
per cases by A4,XBOOLE_0:def 3;
suppose
A5: x in support pfexp n;
A6: (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;
(pfexp n).x <> 0 by A5,PRE_POLY:def 7;
then 0 < (pfexp n).x;
hence thesis by A6,PRE_POLY:def 7;
end;
suppose
A7: x in support pfexp m;
A8: (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;
(pfexp m).x <> 0 by A7,PRE_POLY:def 7;
then 0 < (pfexp m).x;
hence thesis by A8,PRE_POLY:def 7;
end;
end;
A9: support ppf m = support pfexp m by NAT_3:def 9;
A10: support ppf k =support pfexp k by NAT_3:def 9
.=support max(pfexp n,pfexp m) by A1,NAT_3:54;
then support ppf k c= (support ppf n) \/ (support ppf m) by A2,A9,NAT_3:18;
hence thesis by A10,A2,A9,A3,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 object holds x in support min(b1,b2) implies x in support b1 & x
in support b2
proof
let x be object;
assume
A2: x in support min(b1,b2);
assume
A3: not x in support b1 or not x in support b2;
now
per cases;
case
A4: b1.x<=b2.x;
A5: not x in support b1
proof
assume
A6: x in support b1;
then
A7: b1.x<>0 by PRE_POLY:def 7;
b2.x=0 by A3,A6,PRE_POLY:def 7;
hence contradiction by A4,A7;
end;
f.x = b1.x by A4,NAT_3:def 3
.=0 by A5,PRE_POLY:def 7;
hence contradiction by A2,PRE_POLY:def 7;
end;
case
A8: b2.x<b1.x;
then f.x = b2.x by NAT_3:def 3
.=0 by A3,A8,PRE_POLY:def 7;
hence contradiction by A2,PRE_POLY:def 7;
end;
end;
hence thesis;
end;
for x be object holds x in support b1 & x in support b2 implies x in
support min(b1,b2)
proof
let x be object;
assume that
A9: x in support b1 and
A10: x in support b2;
A11: b2.x<>0 by A10,PRE_POLY:def 7;
A12: f.x = b1.x or f.x = b2.x by NAT_3:def 3;
b1.x<>0 by A9,PRE_POLY:def 7;
hence thesis by A11,A12,PRE_POLY:def 7;
end;
hence thesis by A1,XBOOLE_0:def 4;
end;
theorem
for n,m,k be non zero Nat st k = n gcd m holds support ppf
k = (support ppf n) /\ (support ppf m)
proof
let n,m,k be non zero Nat;
assume
A1: k = n gcd m;
A2: support ppf n = support pfexp n by NAT_3:def 9;
A3: support ppf m = support pfexp m by NAT_3:def 9;
support ppf k =support pfexp k by NAT_3:def 9
.=support min(pfexp n,pfexp m) by A1,NAT_3:53;
hence thesis by A2,A3,Th10;
end;
theorem Th12:
for p,q be bag of SetPrimes st p is prime-factorization-like & q
is prime-factorization-like & (support p) misses (support q) holds Product p,
Product q are_coprime
proof
let p,q be bag of SetPrimes;
assume that
A1: p is prime-factorization-like and
A2: q is prime-factorization-like and
A3: (support p) misses (support q);
assume not Product p,Product q are_coprime;
then consider x be Prime such that
A4: x divides (Product p) and
A5: x divides (Product q) by PYTHTRIP:def 2;
A6: x in (support q) by A2,A5,Lm7;
x in (support p) by A1,A4,Lm7;
hence contradiction by A3,A6,XBOOLE_0:3;
end;
Lm8: for q be Prime,g be Element of NAT st g <> 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;
set p = (SetPrimes --> 0)+*(q,g);
reconsider p as ManySortedSet of SetPrimes;
dom(SetPrimes --> 0) = SetPrimes by FUNCOP_1:13;
then q in dom(SetPrimes --> 0) by NEWTON:def 6;
then
A1: p.q = g by FUNCT_7:31;
A2: for x st not x in {q} holds p.x=0
proof
let x;
assume not x in {q};
then x <> q by TARSKI:def 1;
hence thesis by Lm1;
end;
now
let z be set;
assume
A3: z in support p;
z in dom p
proof
assume not z in dom p;
then p.z = {} by FUNCT_1:def 2;
hence contradiction by A3,PRE_POLY:def 7;
end;
then reconsider y = z as Element of SetPrimes;
assume not z in {q};
p.y <> 0 by A3,PRE_POLY:def 7;
hence z in {q} by A2;
end;
then for z be object st z in support p holds z in {q};
then
A4: support p c= {q};
assume
A5: g <> 0;
now
let z be object;
assume z in {q};
then
A6: z=q by TARSKI:def 1;
thus z in support p by A5,A1,A6,PRE_POLY:def 7;
end;
then
A7: {q} c= support p;
then
A8: support p = {q} by A4,XBOOLE_0:def 10;
reconsider p as bag of SetPrimes by A4,PRE_POLY:def 8;
A9: q in support p by A8,TARSKI:def 1;
A10: q in dom p
proof
assume not q in dom p;
then p.q = {} by FUNCT_1:def 2;
hence contradiction by A9,PRE_POLY:def 7;
end;
take p;
consider f being FinSequence of COMPLEX such that
A11: Product p = Product f and
A12: f = p*canFS(support p) by NAT_3:def 5;
f = p*(<*q*>) by A8,A12,FINSEQ_1:94;
then f = <*(p.q)*> by A10,FINSEQ_2:34;
hence thesis by A1,A4,A7,A11,RVSUM_1:95,XBOOLE_0:def 10;
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 that
A1: p is prime-factorization-like and
A2: x in support p and
A3: p.x = x;
consider nx be Nat such that
A4: 0 < nx and
A5: p.x =x |^ nx by A1,A2;
consider mx be Nat such that
A6: nx=mx + 1 by A4,NAT_1:6;
A7: mx = 0
proof
assume mx <> 0;
then
A8: 0+1 < mx+ 1 by XREAL_1:8;
1 < x by INT_2:def 4;
then x to_power 1 < x to_power nx by A6,A8,POWER:39;
then x|^1 < x to_power nx by POWER:41;
then x|^1 < x |^ nx by POWER:41;
hence contradiction by A3,A5;
end;
{x} c= support p by A2,ZFMISC_1:31;
then consider q,r be bag of SetPrimes such that
A9: (support q) = (support p) \ {x} and
A10: (support r) = {x} and
A11: (support q) misses (support r) and
A12: q | (support q) =p | (support q) and
A13: r | (support r) =p | (support r) and
A14: q+r = p by Lm3;
A15: r = (SetPrimes --> 0)+*(x,r.x) by A10,Th1;
now
let z be Prime;
assume
A16: z in support q;
(support q) c= (support p) by A9,XBOOLE_1:36;
then consider n be Nat such that
A17: 0 < n and
A18: p.z =z |^ n by A1,A16;
take n;
q.z = (q|support q).z by A16,FUNCT_1:49
.= p.z by A12,A16,FUNCT_1:49;
hence 0 < n & q.z =z |^ n by A17,A18;
end;
then
A19: q is prime-factorization-like;
A20: x in (support r) by A10,TARSKI:def 1;
then r.x =(r | (support r)).x by FUNCT_1:49
.= p.x by A13,A20,FUNCT_1:49
.= x by A5,A6,A7;
then
A21: ex rr1 be bag of SetPrimes st rr1=r & support rr1 = {x} & Product rr1 =
x by A15,Lm8;
(Product q)*(Product r) = Product p by A11,A14,NAT_3:19;
hence thesis by A9,A12,A19,A21;
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 that
A1: p is prime-factorization-like and
A2: x in support p and
A3: p.x <> x;
consider nx be Nat such that
A4: 0 < nx and
A5: p.x =x |^ nx by A1,A2;
consider mx be Nat such that
A6: nx=mx + 1 by A4,NAT_1:6;
A7: mx <> 0 by A3,A5,A6;
A8: dom(SetPrimes-->0) = SetPrimes by FUNCOP_1:13;
then
A9: x in dom(SetPrimes-->0) by NEWTON:def 6;
set r10 = (SetPrimes --> 0)+*(x,x);
x is Element of NAT by ORDINAL1:def 12;
then
A10: ex r1 be bag of SetPrimes st r1=r10 & support r1 = {x} & Product r1
= x by Lm8;
A11: {x} c= support p by A2,ZFMISC_1:31;
then consider q,r be bag of SetPrimes such that
A12: (support q) = (support p) \ {x} and
A13: (support r) = {x} and
A14: (support q) misses (support r) and
A15: q | (support q) =p | (support q) and
A16: r | (support r) =p | (support r) and
A17: q+r = p by Lm3;
A18: x in (support r) by A13,TARSKI:def 1;
then
A19: r.x =(r | (support r)).x by FUNCT_1:49
.=p.x by A16,A18,FUNCT_1:49;
then
A20: (r.x)/x =((x |^ mx)*x)/x by A5,A6,NEWTON:6
.= x |^mx by XCMPLX_1:89;
then reconsider rxx= (r.x)/x as Element of NAT by ORDINAL1:def 12;
set r20 = (SetPrimes --> 0)+*(x,rxx);
rxx <> 0
proof
assume
A21: rxx=0;
r.x= rxx*x by XCMPLX_1:87
.=0 by A21;
hence contradiction by A5,A19;
end;
then consider r2 be bag of SetPrimes such that
A22: r2=r20 and
A23: support r2 = {x} and
A24: Product r2 = rxx by Lm8;
set p1=q+r2;
A25: r = (SetPrimes --> 0)+*(x,r.x) by A13,Th1;
A26: now
let z be set;
A27: p1.z= q.z + r2.z by PRE_POLY:def 5;
assume
A28: z in (support p1) \ {x};
then not z in {x} by XBOOLE_0:def 5;
then
A29: r2.z = 0 by A23,PRE_POLY:def 7;
z in support p1 by A28,XBOOLE_0:def 5;
then z in support q \/ support r2 by PRE_POLY:38;
then
A30: z in support q or z in support r2 by XBOOLE_0:def 3;
then q.z = (q|support q).z by A23,A28,FUNCT_1:49,XBOOLE_0:def 5
.= p.z by A15,A23,A28,A30,FUNCT_1:49,XBOOLE_0:def 5;
hence p1.z =p.z by A27,A29;
end;
dom p1= SetPrimes by PARTFUN1:def 2
.= dom p by PARTFUN1:def 2;
then
A31: p1 | ((support p1) \ {x}) =p | ((support p1) \{x}) by A26,FUNCT_1:96;
A32: (support q) /\ (support r) = {} by A14,XBOOLE_0:def 7;
now
let z be Prime;
A33: p1.z= q.z + r2.z by PRE_POLY:def 5;
assume z in support p1;
then
A34: z in support q \/ support r2 by PRE_POLY:38;
per cases by A34,XBOOLE_0:def 3;
suppose
A35: z in support q;
then not z in {x} by A12,XBOOLE_0:def 5;
then
A36: r2.z = 0 by A23,PRE_POLY:def 7;
A37: (support q) c= (support p) by A12,XBOOLE_1:36;
q.z = (q|support q).z by A35,FUNCT_1:49
.= p.z by A15,A35,FUNCT_1:49;
hence ex n be Nat st 0 < n & p1.z =z |^ n by A1,A33,A35,A37,A36;
end;
suppose
A38: z in support r2;
take mx;
thus 0 < mx by A7;
A39: z = x by A23,A38,TARSKI:def 1;
A40: not z in support q by A13,A32,A23,A38,XBOOLE_0:def 4;
p1.z= q.z + r2.z by PRE_POLY:def 5
.= 0 + r2.z by A40,PRE_POLY:def 7
.= z |^ mx by A20,A22,A8,A38,A39,FUNCT_7:31;
hence p1.z = z |^ mx;
end;
end;
then
A41: p1 is prime-factorization-like;
x in {x} by TARSKI:def 1;
then
A42: not x in support q by A12,XBOOLE_0:def 5;
p1.x= q.x + r2.x by PRE_POLY:def 5
.= 0 + r2.x by A42,PRE_POLY:def 7
.= rxx by A22,A9,FUNCT_7:31;
then
A43: p.x =(p1.x)*x by A19,XCMPLX_1:87;
r.x= rxx*x by XCMPLX_1:87;
then
ex rr1 be bag of SetPrimes st rr1=r & support rr1 = {x} & Product rr1 =
rxx*x by A5,A19,A25,Lm8;
then
A44: Product p = (Product q)*((Product r2)*x) by A14,A17,A24,NAT_3:19
.= ((Product q)*(Product r2))*x
.= (Product p1)*x by A13,A14,A23,NAT_3:19;
support p1 = ( (support p) \ {x}) \/ {x} by A12,A23,PRE_POLY:38
.= (support p) \/ {x} by XBOOLE_1:39
.= support p by A11,XBOOLE_1:12;
hence thesis by A10,A43,A44,A41,A31;
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;
A2: rng canFS(support p) = support p by FUNCT_2:def 3;
consider f being FinSequence of COMPLEX such that
A3: Product p = Product f and
A4: f = p*canFS(support p) by NAT_3:def 5;
reconsider f as complex-valued FinSequence;
assume Product p = 0;
then consider k be Nat such that
A5: k in dom f and
A6: f.k = 0 by A3,RVSUM_1:103;
k in dom (canFS(support p)) by A4,A5,FUNCT_1:11;
then
A7: (canFS(support p)).k in support p by A2,FUNCT_1:3;
then reconsider q= (canFS(support p)).k as Prime by NEWTON:def 6;
ex n be Nat st 0 < n & p.q = q|^n by A1,A7;
hence contradiction by A4,A5,A6,FUNCT_1:12;
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 object 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 =1 by A1,A3,A4,Lm4,WSIERP_1:15;
hence contradiction by INT_2:def 4;
end;
end;
now
consider f being FinSequence of COMPLEX such that
A5: Product p = Product f and
A6: f = p*canFS(support p) by NAT_3:def 5;
assume support p = {};
hence Product p =1 by A5,A6,RVSUM_1:94;
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[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: now
let k be Nat;
assume
A2: P[k];
now
let p,q be bag of SetPrimes;
assume that
A3: p is prime-factorization-like and
A4: q is prime-factorization-like and
A5: Product p <= 2|^ (k+1) and
A6: Product p = Product q;
now
per cases;
suppose
A7: support p={};
then Product p =1 by A3,Th14;
then support q ={} by A4,A6,Th14;
hence p=q by A7,Th4;
end;
suppose
support p<>{};
then consider x be object such that
A8: x in support p by XBOOLE_0:def 1;
reconsider x as Prime by A8,NEWTON:def 6;
A9: x divides Product p by A3,A8,Lm4;
then
A10: x in support q by A4,A6,Lm7;
per cases;
suppose
p.x <> x;
then consider p1,r1 be bag of SetPrimes such that
A11: p1 is prime-factorization-like and
(support r1) = {x} and
Product r1 = x and
A12: support p1 = support p and
A13: p1 | ((support p1) \ {x}) =p | ((support p1) \{x}) and
A14: p.x =(p1.x)*x and
A15: Product p= (Product p1)*x by A3,A8,Lm10;
per cases;
suppose
A16: q.x <> x;
1 < x by INT_2:def 4;
then 1+1 <= x by NAT_1:13;
then
A17: (2|^(k+1)) /x <= (2|^(k+1)) /2 by XREAL_1:118;
consider q1,r2 be bag of SetPrimes such that
A18: q1 is prime-factorization-like and
(support r2) = {x} and
Product r2 = x and
A19: support q1 = support q and
A20: q1 | ((support q1) \ {x}) =q | ((support q1) \{x}) and
A21: q.x =(q1.x)*x and
A22: Product q= (Product q1)*x by A4,A6,A9,A16,Lm7,Lm10;
((Product p1)*x) /x <= (2|^(k+1)) /x by A5,A15,XREAL_1:72;
then ((Product p1)*x) /x <= (2|^(k+1)) /2 by A17,XXREAL_0:2;
then Product p1 <= (2|^(k+1)) /2 by XCMPLX_1:89;
then Product p1 <= (2|^k*2|^1) /2 by NEWTON:8;
then
A23: Product p1 <= (2|^k*2) /2;
then
A24: p1=q1 by A2,A6,A11,A15,A18,A22,XCMPLX_1:5;
A25: now
let z be set;
assume
A26: z in support p;
per cases;
suppose
not z in {x};
then
A27: z in (support p1) \ {x} by A12,A26,XBOOLE_0:def 5;
hence p.z = ( p| ((support p1) \ {x})).z by FUNCT_1:49
.= q.z by A13,A20,A24,A27,FUNCT_1:49;
end;
suppose
A28: z in {x};
hence p.z = (p1.x)*x by A14,TARSKI:def 1
.= (q1.x)*x by A2,A6,A11,A15,A18,A22,A23,XCMPLX_1:5
.= q.z by A21,A28,TARSKI:def 1;
end;
end;
A29: dom p= SetPrimes by PARTFUN1:def 2
.= dom q by PARTFUN1:def 2;
support p = support q by A2,A6,A11,A12,A15,A18,A19,A22,A23,
XCMPLX_1:5;
then p| (support p) =q| (support q) by A29,A25,FUNCT_1:96;
hence p=q by Th3;
end;
suppose
A30: q.x = x;
1 < x by INT_2:def 4;
then 1+1 <= x by NAT_1:13;
then
A31: (2|^(k+1)) /x <= (2|^(k+1)) /2 by XREAL_1:118;
((Product p1)*x) /x <= (2|^(k+1)) /x by A5,A15,XREAL_1:72;
then ((Product p1)*x) /x <= (2|^(k+1)) /2 by A31,XXREAL_0:2;
then Product p1 <= (2|^(k+1)) /2 by XCMPLX_1:89;
then Product p1 <= (2|^k*2|^1) /2 by NEWTON:8;
then
A32: Product p1 <= (2|^k*2) /2;
ex q1,r2 be bag of SetPrimes st 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 A4,A6,A9,A30,Lm7,Lm9;
then support p = support q \ {x} by A2,A6,A11,A12,A15,A32,
XCMPLX_1:5;
then not x in {x} by A8,XBOOLE_0:def 5;
hence p=q by TARSKI:def 1;
end;
end;
suppose
A33: p.x = x;
then consider p1,r1 be bag of SetPrimes such that
A34: p1 is prime-factorization-like and
(support r1) = {x} and
Product r1 = x and
A35: (support p1) = (support p) \ {x} and
A36: p1 | (support p1) =p | (support p1) and
A37: Product p= (Product p1)*x by A3,A8,Lm9;
per cases;
suppose
A38: q.x <> x;
1 < x by INT_2:def 4;
then 1+1 <= x by NAT_1:13;
then
A39: (2|^(k+1)) /x <= (2|^(k+1)) /2 by XREAL_1:118;
((Product p1)*x) /x <= (2|^(k+1)) /x by A5,A37,XREAL_1:72;
then ((Product p1)*x) /x <= (2|^(k+1)) /2 by A39,XXREAL_0:2;
then Product p1 <= (2|^(k+1)) /2 by XCMPLX_1:89;
then Product p1 <= (2|^k*2|^1) /2 by NEWTON:8;
then
A40: Product p1 <= (2|^k*2) /2;
ex q1,r2 be bag of SetPrimes st 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 A4,A6,A9,A38,Lm7,Lm10;
then support p \ {x} = support q by A2,A6,A34,A35,A37,A40,
XCMPLX_1:5;
then not x in {x} by A10,XBOOLE_0:def 5;
hence p=q by TARSKI:def 1;
end;
suppose
A41: q.x = x;
1 < x by INT_2:def 4;
then 1+1 <= x by NAT_1:13;
then
A42: (2|^(k+1)) /x <= (2|^(k+1)) /2 by XREAL_1:118;
consider q1,r2 be bag of SetPrimes such that
A43: q1 is prime-factorization-like and
(support r2) = {x} and
Product r2 = x and
A44: (support q1) = (support q) \ {x} and
A45: q1 | (support q1) =q | (support q1) and
A46: Product q= (Product q1)*x by A4,A6,A9,A41,Lm7,Lm9;
((Product p1)*x) /x <= (2|^(k+1)) /x by A5,A37,XREAL_1:72;
then ((Product p1)*x) /x <= (2|^(k+1)) /2 by A42,XXREAL_0:2;
then Product p1 <= (2|^(k+1)) /2 by XCMPLX_1:89;
then Product p1 <= (2|^k*2|^1) /2 by NEWTON:8;
then
A47: Product p1 <= (2|^k*2) /2;
then support p \ {x} = support q \ {x} by A2,A6,A34,A35,A37,A43
,A44,A46,XCMPLX_1:5;
then (support p) \/ {x} = (support q \ {x}) \/ {x} by XBOOLE_1:39
;
then
A48: (support p) \/ {x} = (support q) \/ {x} by XBOOLE_1:39;
A49: p1=q1 by A2,A6,A34,A37,A43,A46,A47,XCMPLX_1:5;
A50: now
let z be set;
assume
A51: z in (support p);
per cases;
suppose
not z in {x};
then
A52: z in support p1 by A35,A51,XBOOLE_0:def 5;
hence p.z = ( p1| (support p1)).z by A36,FUNCT_1:49
.= q.z by A45,A49,A52,FUNCT_1:49;
end;
suppose
A53: z in {x};
hence p.z = x by A33,TARSKI:def 1
.= q.z by A41,A53,TARSKI:def 1;
end;
end;
A54: {x} c= support q by A10,ZFMISC_1:31;
{x} c= support p by A8,ZFMISC_1:31;
then
A55: support p = (support q) \/ {x} by A48,XBOOLE_1:12;
dom p= SetPrimes by PARTFUN1:def 2
.= dom q by PARTFUN1:def 2;
then p| (support p) = q| (support p) by A50,FUNCT_1:96
.=q| (support q) by A54,A55,XBOOLE_1:12;
hence p=q by Th3;
end;
end;
end;
end;
hence p=q;
end;
hence P[k+1];
end;
A56: P[ 0 ]
proof
let p,q be bag of SetPrimes;
assume that
A57: p is prime-factorization-like and
A58: q is prime-factorization-like and
A59: Product p <= 2|^0 and
A60: Product p = Product q;
Product p <> 0 by A57,Th13;
then
A61: 0 +1 <= Product p by NAT_1:13;
Product p <= 1 by A59,NEWTON:4;
then
A62: Product p =1 by A61,XXREAL_0:1;
then
A63: support p={} by A57,Th14;
support q ={} by A58,A60,A62,Th14;
hence thesis by A63,Th4;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A56,A1);
hence thesis;
end;
::$N Fundamental Theorem of Arithmetic (uniqueness)
::$L https://en.wikipedia.org/wiki/Fundamental_theorem_of_arithmetic Fundamental Theorem of Arithmetic
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 that
A1: p is prime-factorization-like and
A2: q is prime-factorization-like and
A3: Product p = Product q;
reconsider n=Product p as Element of NAT;
n <=2|^n by NEWTON:86;
hence thesis by A1,A2,A3,Lm11;
end;
theorem
for p be bag of SetPrimes, n be non zero Nat st p is
prime-factorization-like & n = Product p holds (ppf n) = p
proof
let p be bag of SetPrimes, n be non zero Nat;
assume that
A1: p is prime-factorization-like and
A2: n=Product p;
Product ppf n = Product p by A2,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 that
A1: 1<=n1 and
A2: 1 <=m1;
reconsider n=n1,m=m1 as non zero Nat by A1,A2;
set nm1 = n1 lcm m1;
reconsider nm=nm1 as non zero Nat by A1,A2,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;
A3: N1 c= support ppf n
proof
let x be object;
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;
A4: for x be set st x in N2 holds (pfexp nm).x = (pfexp m).x
proof
let x be set;
A5: (pfexp n).x > (pfexp m).x implies max(pfexp n,pfexp m).x = (pfexp n).
x by NAT_3:def 4;
assume x in N2;
then
A6: not x in N1 by XBOOLE_0:def 5;
A7: support ppf n = support pfexp n by NAT_3:def 9;
A8: not (pfexp n).x > (pfexp m).x
proof
assume
A9: (pfexp n).x > (pfexp m).x;
then
A10: (pfexp nm).x = (pfexp n). x by A5,NAT_3:54;
A11: x in support (pfexp n) by A9,PRE_POLY:def 7;
then x in SetPrimes;
hence contradiction by A6,A7,A10,A11;
end;
(pfexp n).x <= (pfexp m).x implies max(pfexp n,pfexp m).x = (pfexp m)
. x by NAT_3:def 4;
hence thesis by A8,NAT_3:54;
end;
A12: Product (ppf m)=m by NAT_3:61;
A13: support ppf nm = support ppf n \/ support ppf m by Th9;
then
A14: support ppf n c= support ppf nm by XBOOLE_1:7;
then consider ppm,ppn be bag of SetPrimes such that
A15: (support ppm) = (support (ppf nm)) \ N1 and
A16: (support ppn) = N1 and
A17: (support ppm) misses (support ppn) and
A18: ppm | (support ppm) =(ppf nm) | (support ppm) and
A19: ppn | (support ppn) =(ppf nm) | (support ppn) and
A20: ppm+ppn = (ppf nm) by A3,Lm3,XBOOLE_1:1;
reconsider n0=Product ppn, m0=Product ppm as Element of NAT;
A21: Product (ppf n)=n by NAT_3:61;
A22: N2 c= support ppf m
proof
let x be object;
A23: (pfexp n).x <= (pfexp m).x implies max(pfexp n,pfexp m).x = (pfexp m)
. x by NAT_3:def 4;
A24: (pfexp n).x > (pfexp m).x implies max(pfexp n,pfexp m).x = (pfexp n).
x by NAT_3:def 4;
assume
A25: x in N2;
then
A26: x in SetPrimes;
A27: x in (support (ppf nm)) by A25,XBOOLE_0:def 5;
then x in support pfexp nm by NAT_3:def 9;
then
A28: (pfexp nm).x = (pfexp m). x implies (pfexp m).x <> 0 by PRE_POLY:def 7;
not x in N1 by A25,XBOOLE_0:def 5;
then
A29: not x in (support (ppf n)) or (pfexp nm).x <> (pfexp n). x by A26;
support ppf m = support pfexp m by NAT_3:def 9;
hence thesis by A13,A27,A29,A23,A24,A28,NAT_3:54,PRE_POLY:def 7
,XBOOLE_0:def 3;
end;
N1 \/ N2 = support ppf nm by A14,A3,XBOOLE_1:1,45;
then
A30: N2 c= support ppf nm by XBOOLE_1:7;
A31: now
let x2 be set;
assume
A32: x2 in N2;
then reconsider x=x2 as Prime by NEWTON:def 6;
x2 in support ppf m by A22,A32;
then
A33: x2 in support pfexp m by NAT_3:def 9;
x2 in (support (ppf nm)) by A30,A32;
then x2 in (support pfexp nm) by NAT_3:def 9;
hence (ppf nm).x2 = x |^ (x |-count nm) by NAT_3:def 9
.= x |^ ((pfexp nm).x) by NAT_3:def 8
.= x |^ ((pfexp m).x) by A4,A32
.= x |^ (x |-count m) by NAT_3:def 8
.= (ppf m).x2 by A33,NAT_3:def 9;
end;
dom (ppf nm)= SetPrimes by PARTFUN1:def 2
.= dom (ppf m) by PARTFUN1:def 2;
then ppm|N2 = (ppf m) | N2 by A15,A18,A31,FUNCT_1:96;
then
A34: m0 divides m by A22,A12,A15,Th7;
A35: n0*m0 = Product (ppf nm) by A17,A20,NAT_3:19
.=nm by NAT_3:61;
then
A36: m0 <> 0;
now
let x being Prime;
assume
A37: x in support ppm;
then x in (support (ppf nm)) by A15,XBOOLE_0:def 5;
then
A38: x in (support pfexp nm) by NAT_3:def 9;
then
A39: (ppf nm) .x = x |^ (x |-count nm) by NAT_3:def 9;
(pfexp nm).x <> 0 by A38,NAT_3:36,38;
then
A40: 0 < (x |-count nm) by NAT_3:def 8;
ppm.x =(ppm | (support ppm)).x by A37,FUNCT_1:49
.= (ppf nm).x by A18,A37,FUNCT_1:49;
hence ex m be Nat st 0 < m & (ppm).x = x |^m by A39,A40;
end;
then
A41: ppm is prime-factorization-like;
A42: N1 c= support ppf nm by A14,A3;
now
let x being Prime;
assume
A43: x in support (ppn);
then x in (support (ppf nm)) by A42,A16;
then
A44: x in (support pfexp nm) by NAT_3:def 9;
then
A45: (ppf nm) .x = x |^ (x |-count nm) by NAT_3:def 9;
(pfexp nm).x <> 0 by A44,NAT_3:36,38;
then
A46: 0 < (x |-count nm) by NAT_3:def 8;
ppn.x =(ppn | (support ppn)).x by A43,FUNCT_1:49
.= (ppf nm).x by A19,A43,FUNCT_1:49;
hence ex n be Nat st 0 < n & (ppn).x = x |^n by A45,A46;
end;
then ppn is prime-factorization-like;
then n0,m0 are_coprime by A17,A41,Th12;
then
A47: n0 gcd m0 = 1 by INT_2:def 3;
A48: 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;
A49: now
let x1 be set;
assume
A50: x1 in N1;
then
A51: x1 in (support (ppf nm)) by A42;
then reconsider x=x1 as Prime by NEWTON:def 6;
x1 in support ppf n by A3,A50;
then
A52: x1 in support pfexp n by NAT_3:def 9;
x1 in (support pfexp nm) by A51,NAT_3:def 9;
hence (ppf nm).x1= x |^ (x |-count nm) by NAT_3:def 9
.= x |^ ((pfexp nm).x) by NAT_3:def 8
.= x |^ ((pfexp n).x) by A48,A50
.= x |^ (x |-count n) by NAT_3:def 8
.= (ppf n).x1 by A52,NAT_3:def 9;
end;
dom (ppf nm)= SetPrimes by PARTFUN1:def 2
.= dom (ppf n) by PARTFUN1:def 2;
then
A53: ppn|N1=(ppf n) |N1 by A16,A19,A49,FUNCT_1:96;
n0 <> 0 by A35;
hence thesis by A3,A21,A16,A53,A35,A34,A36,A47,Th7;
end;
begin ::multiplicative group
definition
let n be Nat;
assume
A1: 1 < n;
func Segm0(n) -> non empty finite Subset of NAT equals
:Def2:
Segm(n) \ {0};
correctness
proof
A2: not 1 in {0} by TARSKI:def 1;
1 in Segm(n) by A1,NAT_1:44;
hence thesis by A2,XBOOLE_0:def 5;
end;
end;
theorem Th18:
for n be Nat st 1 < n holds card Segm0(n) = n-1
proof
let n be Nat;
A1: card (Segm(n)) = n;
assume
A2: 1 < n;
then
A3: 0 in Segm(n) by NAT_1:44;
A4: card {0} = 1 by CARD_1:30;
Segm0(n) = Segm(n) \{0} by A2,Def2;
hence thesis by A1,A3,A4,EULER_1:4;
end;
definition
let n be Prime;
func multint0(n) -> BinOp of Segm0(n) equals
(multint n) || Segm0 n;
coherence
proof
A1: 1<n by INT_2:def 4;
then Segm0(n) = Segm(n) \{0} by Def2;
then reconsider S = Segm0 n as Subset of Segm n by XBOOLE_1:36;
multint n is S-subsetpreserving
proof
let x be set;
A2: 0 in Segm(n) by NAT_1:44;
assume x in [:S,S:];
then consider a,b be object such that
A3: a in Segm0(n) and
A4: b in Segm0(n) and
A5: x=[a,b] by ZFMISC_1:def 2;
A6: b in Segm(n)\{0} by A1,A4,Def2;
then reconsider b1 = b as Element of INT.Ring(n) by XBOOLE_0:def 5;
not b in {0} by A6,XBOOLE_0:def 5;
then b <> 0 by TARSKI:def 1;
then
A7: b <> 0.(INT.Ring(n)) by A2,SUBSET_1:def 8;
A8: a in Segm(n)\{0} by A1,A3,Def2;
then reconsider a1 = a as Element of INT.Ring(n) by XBOOLE_0:def 5;
set y = (multint n).(a,b);
A9: y = a1*b1;
not a in {0} by A8,XBOOLE_0:def 5;
then a <> 0 by TARSKI:def 1;
then a <> 0.(INT.Ring(n)) by A2,SUBSET_1:def 8;
then y <> In (0,Segm(n)) by A9,A7,VECTSP_1:12;
then y <> 0 by A9;
then not y in {0} by TARSKI:def 1;
then y in Segm(n)\{0} by A9,XBOOLE_0:def 5;
hence (multint n).x in S by A1,A5,Def2;
end;
hence thesis by REALSET1:6;
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 that
A1: a=x and
A2: y=b;
thus a*b = (multint(p)).([a,b]) by FUNCT_1:49
.=x*y by A1,A2;
end;
theorem Th19:
for p be Prime holds multMagma(#Segm0(p),multint0(p)#) is
associative commutative Group-like
proof
let p be Prime;
set Zp= multMagma(#Segm0(p),multint0(p)#);
A1: not 1 in {0} by TARSKI:def 1;
A2: 1 < p by INT_2:def 4;
then 1 in Segm(p) by NAT_1:44;
then 1 in Segm(p)\{0} by A1,XBOOLE_0:def 5;
then 1 in Segm0(p) by A2,Def2;
then reconsider e=1.(INT.Ring(p)) as Element of Zp by A2,INT_3:14;
A3: Zp is associative
proof
let x,y,z being Element of Zp;
x in Segm0(p);
then x in Segm(p)\{0} by A2,Def2;
then reconsider x1=x as Element of INT.Ring(p) by XBOOLE_0:def 5;
y in Segm0(p);
then y in Segm(p)\{0} by A2,Def2;
then reconsider y1=y as Element of INT.Ring(p) by XBOOLE_0:def 5;
z in Segm0(p);
then z in Segm(p)\{0} by A2,Def2;
then reconsider z1=z as Element of INT.Ring(p) by XBOOLE_0:def 5;
A4: y*z=y1*z1 by Lm12;
x*y=x1*y1 by Lm12;
then (x*y)*z =(x1*y1)*z1 by Lm12
.=x1*(y1*z1) by GROUP_1:def 3
.= x*(y*z) by A4,Lm12;
hence thesis;
end;
A5: now
let h be Element of Zp;
h in Segm0(p);
then
A6: h in Segm(p)\{0} by A2,Def2;
then reconsider hp=h as Element of INT.Ring(p) by XBOOLE_0:def 5;
thus h * e = hp*1_(INT.Ring(p)) by Lm12
.= h;
thus e * h = 1_(INT.Ring(p))*hp by Lm12
.= h;
not h in {0} by A6,XBOOLE_0:def 5;
then
A7: hp <> 0 by TARSKI:def 1;
0 in Segm(p) by NAT_1:44;
then hp <> 0.(INT.Ring(p)) by A7,SUBSET_1:def 8;
then consider hpd be Element of INT.Ring(p) such that
A8: hpd*hp=1.(INT.Ring(p)) by VECTSP_1:def 9;
hpd <> 0.(INT.Ring(p)) by A8;
then hpd <> 0;
then not hpd in {0} by TARSKI:def 1;
then hpd in Segm(p)\{0} by XBOOLE_0:def 5;
then reconsider g=hpd as Element of Zp by A2,Def2;
A9: g * h = e by A8,Lm12;
h*g=e by A8,Lm12;
hence ex g be Element of Zp st h*g = e & g*h = e by A9;
end;
Zp is commutative
proof
let x,y being Element of Zp;
x in Segm0(p);
then x in Segm(p)\{0} by A2,Def2;
then reconsider x1=x as Element of INT.Ring(p) by XBOOLE_0:def 5;
y in Segm0(p);
then y in Segm(p)\{0} by A2,Def2;
then reconsider y1=y as Element of INT.Ring(p) by XBOOLE_0:def 5;
x*y = x1*y1 by Lm12
.= y*x by Lm12;
hence thesis;
end;
hence thesis by A5,A3;
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: not 1 in {0} by TARSKI:def 1;
A2: 1 < p by INT_2:def 4;
then 1 in Segm(p) by NAT_1:44;
then 1 in Segm(p)\{0} by A1,XBOOLE_0:def 5;
then 1 in Segm0(p) by A2,Def2;
then reconsider e=1.(INT.Ring(p)) as Element of Z/Z*(p) by A2,INT_3:14;
now
let h being Element of Z/Z*(p);
h in Segm0(p);
then h in Segm(p)\{0} by A2,Def2;
then reconsider hp=h as Element of INT.Ring(p) by XBOOLE_0:def 5;
thus h * e = hp*1_(INT.Ring(p)) by Lm12
.= h;
thus e * h = 1_(INT.Ring(p))*hp by Lm12
.= h;
end;
then e=1_(Z/Z*(p)) by GROUP_1:def 4;
hence thesis by A2,INT_3:14;
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: 0 in Segm(p) by NAT_1:44;
set hpd=hp";
A3: 1 < p by INT_2:def 4;
h in Segm0(p);
then h in Segm(p)\{0} by A3,Def2;
then not h in {0} by XBOOLE_0:def 5;
then hp <> 0 by A1,TARSKI:def 1;
then
A4: hp <> 0.(INT.Ring(p)) by A2,SUBSET_1:def 8;
then hp*hpd =1.(INT.Ring(p)) by VECTSP_1:def 10;
then hpd <> 0.(INT.Ring(p));
then hpd <> 0;
then not hpd in {0} by TARSKI:def 1;
then hpd in Segm(p)\{0} by XBOOLE_0:def 5;
then reconsider g=hpd as Element of Z/Z*(p) by A3,Def2;
h*g=hp*hpd by A1,Lm12
.=1.(INT.Ring(p)) by A4,VECTSP_1:def 10
.=1_(Z/Z*(p)) by Th21;
hence thesis by GROUP_1:def 5;
end;
registration
let p be Prime;
cluster Z/Z*(p) -> finite;
coherence;
end;
theorem
for p be Prime holds card Z/Z*(p) = p-1
by INT_2:def 4,Th18;
theorem
for G be Group,a be Element of G, i be Integer st a is not
being_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 a is not being_of_order_0;
then ord a<>0 by GROUP_1:def 11;
then
A1: |.i.|<=|.i.|*ord(a) by NAT_1:14,XREAL_1:151;
0<=|.i.|*ord(a)+i
proof
per cases;
suppose
A2: i<0;
A3: |.i.|+i<=|.i.|*ord(a)+i by A1,XREAL_1:6;
|.i.|=-i by A2,ABSVALUE:def 1;
hence thesis by A3;
end;
suppose
0<=i;
hence thesis;
end;
end;
then
A4: |.i.|*ord(a)+i is Element of NAT by INT_1:3;
a|^(|.i.|*ord(a)+i)=a|^(|.i.|*ord(a))*(a|^i) by GROUP_1:33
.=(a|^(ord(a)) |^|.i.|)*(a|^i) by GROUP_1:35
.=((1_G) |^|.i.|)*(a|^i) by GROUP_1:41
.=(1_G)*(a|^i) by GROUP_1:31
.=a|^i by GROUP_1:def 4;
hence thesis by A4;
end;
theorem Th25:
for G be commutative Group,a,b be Element of G, n,m be Nat
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 Nat;
assume that
A1: G is finite and
A2: ord a=n and
A3: ord b= m and
A4: n gcd m = 1;
b is not being_of_order_0 by A1,GR_CY_1:6;
then
A5: m <> 0 by A3,GROUP_1:def 11;
A6: a*b is not being_of_order_0 by A1,GR_CY_1:6;
A7: (a*b) |^(n*m) = a |^ (n*m) * (b |^ (n*m)) by GROUP_1:48
.= (a |^ n) |^m * (b |^ (n*m)) by GROUP_1:35
.= (a |^ n) |^m * ((b |^ m) |^n) by GROUP_1:35
.= (1_G) |^m * ((b |^ m) |^n) by A2,GROUP_1:41
.= (1_G) |^m * ((1_G) |^n) by A3,GROUP_1:41
.= (1_G) * ((1_G) |^n) by GROUP_1:31
.= (1_G) * (1_G) by GROUP_1:31
.= 1_G by GROUP_1:def 4;
A8: m*n is Element of NAT by ORDINAL1:def 12;
reconsider n1=n, m1=m as Integer;
A9: n1,m1 are_coprime by A4,INT_2:def 3;
a is not being_of_order_0 by A1,GR_CY_1:6;
then
A10: n <> 0 by A2,GROUP_1:def 11;
A11: now
let k be Nat;
assume that
A12: (a*b) |^k =1_G and
A13: k <> 0;
reconsider k1=k as Integer;
1_G =(1_G) |^n by GROUP_1:31
.= (a*b) |^(k*n) by A12,GROUP_1:35
.= a |^ (k*n) * (b |^ (k*n)) by GROUP_1:48
.= (a |^ n) |^k * (b |^ (k*n)) by GROUP_1:35
.= (1_G) |^k * (b |^ (k*n)) by A2,GROUP_1:41
.= (1_G) * (b |^ (k*n)) by GROUP_1:31
.= b |^ (k*n) by GROUP_1:def 4;
then m1 divides k1 by A3,A9,GROUP_1:44,INT_2:25;
then consider i be Integer such that
A14: k1 =m1*i by INT_1:def 3;
1_G =(1_G) |^m by GROUP_1:31
.= (a*b) |^(k*m) by A12,GROUP_1:35
.= a |^ (k*m) * (b |^ (k*m)) by GROUP_1:48
.= a |^ (k*m) * (b |^ m) |^k by GROUP_1:35
.= a |^ (k*m) * (1_G) |^k by A3,GROUP_1:41
.= a |^ (k*m) * (1_G) by GROUP_1:31
.= a |^ (k*m) by GROUP_1:def 4;
then n1 divides k1 by A2,A9,GROUP_1:44,INT_2:25;
then n1 divides i by A9,A14,INT_2:25;
then consider j be Integer such that
A15: i =n1*j by INT_1:def 3;
k1 =(m1*n1)*j by A14,A15;
then k/(m*n) = j by A10,A5,XCMPLX_1:6,89;
then
A16: j is Element of NAT by INT_1:3;
j <> 0 by A13,A14,A15;
then (m*n)*1 <=(m*n)*j by A16,NAT_1:14,XREAL_1:64;
hence (m*n) <= k by A14,A15;
end;
n*m <> 0 by A10,A5,XCMPLX_1:6;
hence thesis by A6,A7,A8,A11,GROUP_1:def 11;
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: now
let k be Nat;
assume
A2: P[k];
now
let f be non-zero Polynomial of L;
A3: f <> 0_.(L) by UPROOTS:def 5;
assume
A4: 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;
end;
suppose
A5: Roots(f) <> {};
set RF=Roots f;
consider z be object such that
A6: z in Roots(f) by A5,XBOOLE_0:def 1;
reconsider z as Element of L by A6;
set g = f div rpoly(1,z);
A7: z is_a_root_of f by A6,POLYNOM5:def 10;
then rpoly(1,z) divides f by HURWITZ:35;
then 0_.(L) =f mod rpoly(1,z);
then (g *' rpoly(1,z)) = f-g *' rpoly(1,z) + g *' rpoly(1,z) by
POLYNOM3:28;
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:29;
then
A8: f = g *' rpoly(1,z) by POLYNOM3:28;
then g <> 0_.(L) by A3,POLYNOM3:34;
then reconsider g as non-zero Polynomial of L by UPROOTS:def 5;
set RG = Roots g;
deg (g) = k+1 -1 by A3,A4,A7,HURWITZ:36
.= k;
then ex m1 be Element of NAT st m1=card(Roots(g)) & m1 <= k by A2;
then
A9: card(RG)+1 <= k + 1 by XREAL_1:6;
Roots(f) c= Roots(g) \/ {z}
proof
let y be object;
assume
A10: y in Roots(f);
then reconsider y1=y as Element of L;
y1 is_a_root_of f by A10,POLYNOM5:def 10;
then eval(f,y1) = 0.L by POLYNOM5:def 7;
then eval(g,y1)* eval(rpoly(1,z),y1)= 0.L by A8,POLYNOM4:24;
then
A11: 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 thesis by XBOOLE_0:def 3;
end;
suppose
y1<> z;
then y1-z <> 0.L by RLVECT_1:21;
then eval(g,y1) = 0.L by A11,VECTSP_1:12;
then y1 is_a_root_of g by POLYNOM5:def 7;
then y1 in Roots(g) by POLYNOM5:def 10;
hence thesis by XBOOLE_0:def 3;
end;
end;
hence thesis;
end;
then
A12: card RF <= card (RG \/ {z}) by NAT_1:43;
card (RG \/ {z}) <= card RG + card {z} by CARD_2:43;
then card (RG \/ {z}) <= card RG + 1 by CARD_2:42;
then card RF <= card(RG)+1 by A12,XXREAL_0:2;
hence thesis by A9,XXREAL_0:2;
end;
end;
end;
hence P[k+1];
end;
A13: P[ 0 ]
proof
let f be non-zero Polynomial of L;
assume
A14: deg f = 0;
reconsider x=f.0 as Element of L;
A15: f <> 0_.(L) by UPROOTS:def 5;
A16: f.0 <> 0.L
proof
assume f.0 =0.L;
then f =<%0.L%> by A14,ALGSEQ_1:def 5;
hence contradiction by A15,POLYNOM5:34;
end;
A17: now
let z be Element of L;
eval(<%x%>,z) =eval(<%x,0.L%>,z) by POLYNOM5:43
.=x by POLYNOM5:45;
hence eval(<%x%>,z) <> 0.L by A16;
end;
A18: f =<%x%> by A14,ALGSEQ_1:def 5;
Roots(f) = {}
proof
assume Roots(f) <> {};
then consider z be object such that
A19: z in Roots(f) by XBOOLE_0:def 1;
reconsider z as Element of L by A19;
z is_a_root_of f by A19,POLYNOM5:def 10;
then eval(<%x%>,z) = 0.L by A18,POLYNOM5:def 7;
hence contradiction by A17;
end;
hence thesis;
end;
for k be Nat holds P[k] from NAT_1:sch 2(A13,A1);
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 thesis 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
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:3;
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);
defpred P[Nat] means (power Z/Z*(p)).(z,$1) =(power INT.Ring(p)).(y,$1);
assume
A1: z=y;
A2: now
let k be Nat;
assume
A3: P[k];
(power Z/Z*(p)).(z,k+1) = (power Z/Z*(p)).(z,k)*z by GROUP_1:def 7
.=(power INT.Ring(p)).(y,k)*y by A1,A3,Lm12
.=(power INT.Ring(p)).(y,k+1) by GROUP_1:def 7;
hence P[k+1];
end;
(power Z/Z*(p)).(z,0)=1_(Z/Z*(p)) by GROUP_1:def 7
.= 1_(INT.Ring(p)) by Th21
.= (power INT.Ring(p)).(y,0) by GROUP_1:def 7;
then
A4: P[ 0 ];
for k be Nat holds P[k] from NAT_1:sch 2(A4,A2);
hence thesis;
end;
Lm14: for p be Prime,L be Field, n be Nat st 0<n & L=INT.Ring(p)
holds ex f be Polynomial of L st 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))
proof
let p be Prime, L be Field, n be Nat;
assume that
A1: 0<n and
A2: L=INT.Ring(p);
set qq=1_.(L);
reconsider n0=n as Element of NAT by ORDINAL1:def 12;
set f = (<%0.L,1.L%>)`^n0-1_.(L);
set pp= (<%0.L,1.L%>)`^n0;
A3: now
let x be Element of L, xz be Element of Z/Z*(p), xn be Element of INT.Ring
(p);
assume that
A4: x=xz and
A5: xn =xz|^n;
A6: xn =xz|^n0 by A5
.=(power L).(x,n0) by A2,A4,Th28;
thus eval(f,x)=eval(pp,x)-eval(qq,x) by POLYNOM4:21
.= eval((<%0.L,1.L%>)`^n0,x)-1.L by POLYNOM4:18
.= (power L).(eval(<%0.L,1.L%>,x),n0)-1.L by POLYNOM5:22
.= xn -1_(INT.Ring(p)) by A2,A6,POLYNOM5:48;
end;
A7: len(1_.(L)) =1 by POLYNOM4:4;
len <%0.L,1.L%> = 2 by POLYNOM5:40;
then
A8: len((<%0.L,1.L%>)`^n0) = n*2-n+1 by POLYNOM5:23
.=n+1;
A9: 0+1 < n+1 by A1,XREAL_1:8;
then len((<%0.L,1.L%>)`^n0) <> len(-1_.(L)) by A8,A7,POLYNOM4:8;
then len (f)=max(len((<%0.L,1.L%>)`^n0),len(-1_.(L))) by POLYNOM4:7
.=max(n+1,1) by A8,A7,POLYNOM4:8
.=n+1 by A9,XXREAL_0:def 10;
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 Nat
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 Nat;
assume that
A1: 0 < n and
A2: ord a=n and
A3: b |^n =1;
reconsider XX=the carrier of gr {a} as finite set;
A4: ex D being finite set st D = the carrier of (gr {a}) & card (gr {a}) =
card D;
reconsider L = INT.Ring(p) as unital non empty doubleLoopStr;
consider f be Polynomial of L such that
A5: deg f = n and
A6: 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;
consider m,n0 be Element of NAT such that
A7: n0=deg f and
A8: m=card(Roots(f)) and
A9: m <= n0 by A5,Th27;
assume not b is Element of gr {a};
then card ( (the carrier of gr {a}) \/ {b}) =card ( XX) + 1 by CARD_2:41
.=n0+1 by A2,A5,A7,A4,GR_CY_1:7;
then
A10: card (n0 + 1)=card ( (the carrier of gr {a}) \/ {b});
A11: 1 < p by INT_2:def 4;
A12: 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 x1 |^n =1;
then
A13: x1|^n = 1_(Z/Z*(p)) by Th21
.= 1_(INT.Ring(p)) by Th21;
x1|^n in Segm0(p);
then x1|^n in Segm(p) \ {0} by A11,Def2;
then reconsider x2=x1|^n as Element of INT.Ring(p) by XBOOLE_0:def 5;
x1 in Segm0(p);
then x1 in Segm(p) \ {0} by A11,Def2;
then reconsider x3=x1 as Element of L by XBOOLE_0:def 5;
eval(f,x3) = x2 - 1_(INT.Ring(p)) by A6
.=0.L by A13,RLVECT_1:15;
then x3 is_a_root_of f by POLYNOM5:def 7;
hence thesis by POLYNOM5:def 10;
end;
A14: the carrier of gr {a} c= Roots(f)
proof
let x be object;
assume
A15: x in the carrier of gr {a};
then x in gr {a};
then x in Z/Z*(p) by GROUP_2:40;
then reconsider x1=x as Element of Z/Z*(p);
x1 in gr {a} by A15;
then consider j be Integer such that
A16: x1 = a|^j by GR_CY_1:5;
x1|^n =a|^(j*n) by A16,GROUP_1:35
.=(a|^n) |^j by GROUP_1:35
.=(1_(Z/Z*(p))) |^j by A2,GROUP_1:41
.= 1_(Z/Z*(p)) by GROUP_1:31
.= 1 by Th21;
hence thesis by A12;
end;
b in Roots(f) by A3,A12;
then {b} c= Roots(f) by ZFMISC_1:31;
then (the carrier of gr {a}) \/ {b} c= Roots(f) by A14,XBOOLE_1:8;
then
A17: card ( (the carrier of gr {a}) \/ {b}) c= card (Roots(f)) by CARD_1:11;
card m = card (Roots(f)) by A8;
then Segm(n0 + 1) c= Segm m by A17,A10;
then n0 + 1 <= m by NAT_1:39;
hence contradiction by A9,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 that
A1: G is finite and
A2: ord z=d*l;
set m = d*l;
reconsider H=gr {z} as strict Subgroup of G;
reconsider H as finite strict Subgroup of G by A1;
z in gr{z} by GR_CY_2:2;
then reconsider z1=z as Element of H;
A3: gr{z} =gr{z1} by GR_CY_2:3;
card H = m by A1,A2,GR_CY_1:7;
then ord (z1|^d) = l by A3,GR_CY_2:8;
hence thesis by A1,GROUP_8:3,5;
end;
theorem
for p be Prime holds Z/Z*(p) is cyclic Group
proof
let p be Prime;
set a = the Element of Z/Z*(p);
set ZP=Z/Z*(p);
defpred P[Nat,Element of ZP,Element of ZP] means ord $2 < ord $3;
assume
A1: not Z/Z*(p) is cyclic Group;
A2: for x be Element of Z/Z*(p) holds ord x < card (Z/Z*(p))
proof
let x be Element of Z/Z*(p);
A3: ord x <= card (Z/Z*(p)) by GR_CY_1:8,NAT_D:7;
ord x <> card (Z/Z*(p)) by A1,GR_CY_1:19;
hence thesis by A3,XXREAL_0:1;
end;
A4: for n being Nat for x being Element of ZP ex y being Element
of ZP st P[n,x,y]
proof
let n being Nat, x being Element of ZP;
set n=ord x;
n < card Z/Z*(p) by A2;
then
A5: card gr {x} <> card Z/Z*(p) by GR_CY_1:7;
the carrier of (gr {x}) c= the carrier of Z/Z*(p) by GROUP_2:def 5;
then the carrier of (gr {x}) c< the carrier of Z/Z*(p) by A5,XBOOLE_0:def 8
;
then (the carrier of Z/Z*(p)) \ (the carrier of (gr {x})) <> {} by
XBOOLE_1:105;
then consider z be object such that
A6: z in (the carrier of Z/Z*(p)) \ (the carrier of (gr {x}))
by XBOOLE_0:def 1;
reconsider z as Element of ZP by A6;
set m=ord z;
now
set l= m lcm n;
1 <=card gr {x} by GROUP_1:45;
then
A7: 1 <= n by GR_CY_1:7;
not m divides n
proof
assume m divides n;
then consider j be Integer such that
A8: n=m* j by INT_1:def 3;
z |^n =(z |^m) |^j by A8,GROUP_1:35
.= (1_(Z/Z*(p))) |^j by GROUP_1:41
.= 1_(Z/Z*(p)) by GROUP_1:31
.= 1 by Th21;
then z is Element of gr {x} by A7,Th29;
hence contradiction by A6,XBOOLE_0:def 5;
end;
then
A9: n <> l by INT_2:18;
1 <=card gr {z} by GROUP_1:45;
then
A10: 1 <= m by GR_CY_1:7;
then consider m0,n0 be Element of NAT such that
A11: l=n0*m0 and
A12: n0 gcd m0 = 1 and
A13: n0 divides n and
A14: m0 divides m and
A15: n0 <> 0 and
A16: m0 <> 0 by A7,Th17;
consider j be Integer such that
A17: n=n0* j by A13,INT_1:def 3;
consider u be Integer such that
A18: m=m0* u by A14,INT_1:def 3;
m/m0 = u by A16,A18,XCMPLX_1:89;
then reconsider d2=m/m0 as Element of NAT by INT_1:3;
m=(m/m0)*m0 by A16,XCMPLX_1:87;
then
A19: ord (z|^d2) = m0 by Th30;
n/n0= j by A15,A17,XCMPLX_1:89;
then reconsider d1=n/n0 as Element of NAT by INT_1:3;
n divides (m lcm n) by INT_2:18;
then consider j be Integer such that
A20: l=n* j by INT_1:def 3;
take y =(x|^d1)*(z|^d2);
n=(n/n0)*n0 by A15,XCMPLX_1:87;
then ord (x|^d1) = n0 by Th30;
then
A21: ord y = m0*n0 by A12,A19,Th25;
l/n = j by A7,A20,XCMPLX_1:89;
then
A22: j is Element of NAT by INT_1:3;
j <> 0 by A7,A10,A20,INT_2:4;
then n*1 <=n*j by A22,NAT_1:14,XREAL_1:64;
hence n < ord y by A11,A21,A9,A20,XXREAL_0:1;
end;
hence thesis;
end;
consider f being sequence of the carrier of ZP such that
A23: f.0 = a & for n being Nat holds P[n,f.n,f.(n+1)] from
RECDEF_1:sch 2(A4);
deffunc F(Nat) =ord (f.$1);
consider g be sequence of NAT such that
A24: for k be Element of NAT holds g.k=F(k) from FUNCT_2:sch 4;
A25: for k be Nat holds g.k=F(k)
proof let k be Nat;
k in NAT by ORDINAL1:def 12;
hence thesis by A24;
end;
A26: now
let k be Nat;
A27: g.(k+1) = ord (f.(k+1)) by A25;
g.k = ord (f.k) by A25;
hence g.k < g.(k+1) by A23,A27;
end;
A28: 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);
A29: now
let m be Nat;
assume
A30: P[m];
g.(k+1+m) < g.((k+1+m) + 1) by A26;
hence P[m+1] by A30,XXREAL_0:2;
end;
A31: P[ 0 ] by A26;
for m be Nat holds P[m] from NAT_1:sch 2(A31,A29);
hence thesis;
end;
A32: for k,m be Element of NAT st k < m holds g.k< g.m
proof
let k,m be Element of NAT;
assume
A33: k < m;
then m-k is Element of NAT by INT_1:5;
then reconsider mk=m-k as Nat;
m-k <> 0 by A33;
then consider n0 be Nat such that
A34: mk=n0+1 by NAT_1:6;
reconsider n=n0 as Element of NAT by ORDINAL1:def 12;
m=k+1+n by A34;
hence thesis by A28;
end;
now
let x1,x2 be object;
assume that
A35: x1 in NAT and
A36: x2 in NAT and
A37: g.x1 = g.x2;
reconsider xx1=x1,xx2=x2 as Element of NAT by A35,A36;
A38: xx2 <= xx1 by A32,A37;
xx1 <= xx2 by A32,A37;
hence x2=x1 by A38,XXREAL_0:1;
end;
then g is one-to-one by FUNCT_2:19;
then dom g,rng g are_equipotent by WELLORD2:def 4;
then card (dom g) = card (rng g) by CARD_1:5;
then
A39: card rng g = card NAT by FUNCT_2:def 1;
rng g c= Segm(card ZP)
proof
let y be object;
assume y in rng g;
then consider x be object such that
A40: x in NAT and
A41: y=g.x by FUNCT_2:11;
reconsider x as Element of NAT by A40;
reconsider gg=g.x as Element of NAT;
g.x =ord (f.x) by A25;
then gg < card ZP by A2;
hence thesis by A41,NAT_1:44;
end;
hence contradiction by A39;
end;