:: Uniqueness of factoring an integer and multiplicative group $Z/pZ^{*}$ :: by Hiroyuki Okazaki and Yasunari Shidama :: :: Received January 31, 2008 :: Copyright (c) 2008-2012 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, RVSUM_1, 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; notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, ORDINAL1, FINSET_1, RVSUM_1, CARD_1, CLASSES1, DOMAIN_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, 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, FUNCT_7, NEWTON, INT_2, INT_3, HURWITZ, VALUED_0, REALSET1, RECDEF_1, PRE_POLY, POLYNOM2; constructors REAL_1, NAT_D, NAT_3, SEQ_1, 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; 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 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, STRUCT_0, 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; 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: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 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; 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 set st x in X holds r.x=p.x+q.x proof let x being set; 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 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; 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 set 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(set) = 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(set) = q.$1; defpred C[set] means $1 in (support q) \ (support p); A3: 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 A4: 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(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 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 2; end; A8: 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 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 set st x in dom (f| (support f)) holds (f| (support f)).x =(q| ( support f)).x proof let x be set; 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 set 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); A1: rng fq c= rng p \/ rng(X --> 0) by FUNCT_4:17; A2: rng(X --> 0) c= NAT by RELAT_1:def 19; A3: rng p c= NAT by VALUED_0:def 6; then rng p \/ rng(X --> 0) c= NAT by A2,XBOOLE_1:8; then A4: rng fq c= NAT by A1,XBOOLE_1:1; set fr = p +* (SetPrimes \X -->0); A5: 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; A6: rng fr c= rng p \/ rng(SetPrimes \ X --> 0) by FUNCT_4:17; rng(SetPrimes \X --> 0) c= NAT by RELAT_1:def 19; then rng p \/ rng(SetPrimes \X --> 0) c= NAT by A3,XBOOLE_1:8; then rng fr c= NAT by A6,XBOOLE_1:1; then reconsider fr as Function of SetPrimes,NAT by A5,FUNCT_2:def 1 ,RELSET_1:4; assume A7: X c= support p; A8: not x in X & x in SetPrimes implies fr.x = 0 proof assume that A9: not x in X and A10: x in SetPrimes; A11: x in SetPrimes \ X by A9,A10,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 A11,FUNCOP_1:7; end; A12: 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 A7,XBOOLE_1:1,12; then reconsider fq as Function of SetPrimes,NAT by A4,FUNCT_2:def 1 ,RELSET_1:4; A13: dom (fq| (support fq)) =(dom fq)/\ support fq by RELAT_1:61 .=support fq by PRE_POLY:37,XBOOLE_1:28; A14: for x being set st not x in SetPrimes holds fr.x=0 &fq.x=0 proof let x be set; assume A15: not x in SetPrimes; then A16: not x in dom fr; not x in dom fq by A15; hence thesis by A16,FUNCT_1:def 2; end; A17: 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; A18: for x be set st x in SetPrimes & x in X holds fr.x<>0 proof let x be set; assume that x in SetPrimes and A19: x in X; p.x<>0 by A7,A19,PRE_POLY:def 7; hence thesis by A17,A19; end; A20: 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 A8,A18; end; suppose A21: not x in SetPrimes; X c= SetPrimes by A7,XBOOLE_1:1; hence thesis by A14,A21; end; end; hence thesis; end; then A22: (support fr) = X by PRE_POLY:def 7; then reconsider r = fr as bag of SetPrimes by A7,PRE_POLY:def 8; A23: support p c= dom p by PRE_POLY:37; A24: dom (fr| (support fr)) =(dom fr)/\ support fr by RELAT_1:61 .=support fr by PRE_POLY:37,XBOOLE_1:28 .= X by A20,PRE_POLY:def 7; A25: 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 A26: x in dom (fr| (support fr)); then A27: (p| (support fr)).x=p.x by A22,A24,FUNCT_1:49; (fr| (support fr)).x=fr.x by A22,A24,A26,FUNCT_1:49; hence thesis by A17,A24,A26,A27; end; dom (p| (support fr)) =(dom p)/\ support fr by RELAT_1:61 .=(dom p)/\ X by A20,PRE_POLY:def 7 .=X by A7,A23,XBOOLE_1:1,28; then A28: fr | (support fr) =p | (support fr) by A24,A25,FUNCT_1:def 11; A29: x in X implies fq.x = 0 proof assume A30: x in X; hence fq.x = (X --> 0).x by A12,FUNCT_4:13 .= 0 by A30,FUNCOP_1:7; end; A31: 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 A29,XBOOLE_0:def 5; end; suppose A32: not x in X; then A33: fq.x=p.x by A12,FUNCT_4:11; per cases; suppose x in support p; hence thesis by A32,A33,PRE_POLY:def 7,XBOOLE_0:def 5; end; suppose not x in support p; hence thesis by A33,PRE_POLY:def 7,XBOOLE_0:def 5; end; end; end; then A34: support fq = support p \ X by PRE_POLY:def 7; then reconsider q = fq as bag of SetPrimes by PRE_POLY:def 8; A35: dom (p| (support fq)) =(dom p)/\ support fq by RELAT_1:61 .=(dom p)/\ (support p \ X) by A31,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 A31,PRE_POLY:def 7; (support p \ X) misses X by XBOOLE_1:79; then A36: (support fq) /\ (support fr) = {} by A22,A34,XBOOLE_0:def 7; A37: 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 A38: x in (support fq); not x in X by A22,A36,A38,XBOOLE_0:def 4; hence thesis by A12,FUNCT_4:11; 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 A39: x in dom (fq| (support fq)); then A40: (p| (support fq)).x=p.x by A13,FUNCT_1:49; (fq| (support fq)).x=fq.x by A13,A39,FUNCT_1:49; hence thesis by A13,A37,A39,A40; end; then A41: fq| (support fq)=p| (support fq) by A13,A35,FUNCT_1:def 11; (support fr) \/ (support fq) =(support fr) \/(support p \ support fr) by A20,A34,PRE_POLY:def 7 .=(support fr) \/(support p) by XBOOLE_1:39 .= support p by A7,A22,XBOOLE_1:12; then q+r=p by A36,A41,A28,Th2; hence thesis by A22,A34,A41,A28,XBOOLE_1:79; 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 Nat st 0 < n & p.x = x |^n; end; registration let n be non empty 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,Def1; A5: a divides b.a by A3,A4,NAT_3:3; A6: rng b c= NAT by VALUED_0:def 6; a in rng canFS(support b) by A2,FUNCT_2:def 3; then consider d be set 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,XBOOLE_1:1; 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 UPROOTS:3; 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 set; assume y in rng b1; then consider x be set 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 set; 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} by TARSKI:def 3; now let z be set; 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 by TARSKI:def 3; 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,Def1; 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,UPROOTS:3; 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,Def1; 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,Def1,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 set; assume A41: y in ((support b) \ {q}); then y in rng canFS(support b) by A40,XBOOLE_0:def 5; then consider x be set 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)) by TARSKI:def 3; now let y be set; assume y in rng ((canFS(support b)) | (dom p)); then consider x be set 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}) by TARSKI:def 3; 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 set; 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 by VALUED_0:def 6; 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,Def1,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[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: for k being Element of NAT st P[k] holds P[k+1] proof let k be Element of 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,XBOOLE_1:1; 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 Element of NAT holds P[k] from NAT_1:sch 1(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 by VALUED_0:def 6; 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,XBOOLE_1:1; 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 empty Nat st k = n lcm m holds support ppf k=(support ppf n) \/ (support ppf m) proof let n,m,k be non empty 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 set; 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 set holds x in support min(b1,b2) implies x in support b1 & x in support b2 proof let x be set; 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.x0 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 empty Nat st k = n gcd m holds support ppf k = (support ppf n) /\ (support ppf m) proof let n,m,k be non empty 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_relative_prime 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_relative_prime; then consider x be prime Nat 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 be set; 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 set st z in support p holds z in {q}; then A4: support p c= {q} by TARSKI:def 3; assume A5: g <> 0; now let z be set; 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 by TARSKI:def 3; 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,UPROOTS:4; 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,Def1; 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,NEWTON:5; 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,Def1; 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 by Def1; 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,NEWTON:5; 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,Def1; consider mx be Nat such that A6: nx=mx + 1 by A4,NAT_1:6; A7: mx <> 0 by A3,A5,A6,NEWTON:5; 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,Def1; 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 by Def1; 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-yielding 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,Def1; 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 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 =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[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: now let k be Element of 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 set 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 by NEWTON:5; 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 by NEWTON:5; 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 by NEWTON:5; 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 by NEWTON:5; 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 Element of NAT holds P[k] from NAT_1:sch 1(A56,A1); hence thesis; end; ::$N Fundamental Theorem of Arithmetic (uniqueness) 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 empty Nat st p is prime-factorization-like & n = Product p holds (ppf n) = p proof let p be bag of SetPrimes, n be non empty 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 empty Nat by A1,A2; set nm1 = n1 lcm m1; reconsider nm=nm1 as non empty 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 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; 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 set; 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 by Def1; A42: N1 c= support ppf nm by A14,A3,XBOOLE_1:1; 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 by Def1; then n0,m0 are_relative_prime 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 by CARD_1:def 2; 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 0 by TARSKI:def 1; then A7: b <> 0.(INT.Ring(n)) by A2,FUNCT_7:def 1; 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,FUNCT_7:def 1; then y <> In (0,Segm(n)) by A9,A7,VECTSP_1:12; then y <> 0 by A9,FUNCT_7:def 1; 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 by GROUP_1:def 4; thus e * h = 1_(INT.Ring(p))*hp by Lm12 .= h by GROUP_1:def 4; 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,FUNCT_7:def 1; 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,VECTSP_1:6; 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 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,GROUP_1:def 2; 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 by GROUP_1:def 4; thus e * h = 1_(INT.Ring(p))*hp by Lm12 .= h by GROUP_1:def 4; 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,FUNCT_7:def 1; then hp*hpd =1.(INT.Ring(p)) by VECTSP_1:def 10; then hpd <> 0.(INT.Ring(p)) by VECTSP_1:6; 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 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 proof let p be Prime; 1 < p by INT_2:def 4; hence thesis by Th18; end; 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: abs(i)<=abs(i)*ord(a) by NAT_1:14,XREAL_1:151; 0<=abs(i)*ord(a)+i proof per cases; suppose A2: i<0; A3: abs(i)+i<=abs(i)*ord(a)+i by A1,XREAL_1:6; abs(i)=-i by A2,ABSVALUE:def 1; hence thesis by A3; end; suppose 0<=i; hence thesis; end; end; then A4: abs(i)*ord(a)+i is Element of NAT by INT_1:3; a|^(abs(i)*ord(a)+i)=a|^(abs(i)*ord(a))*(a|^i) by GROUP_1:33 .=(a|^(ord(a)) |^abs(i))*(a|^i) by GROUP_1:35 .=((1_G) |^abs(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_relative_prime 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 Element of 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 set 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 9; then rpoly(1,z) divides f by HURWITZ:35; then 0_.(L) =f mod rpoly(1,z) by HURWITZ:def 7; 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 set; assume A10: y in Roots(f); then reconsider y1=y as Element of L; y1 is_a_root_of f by A10,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 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 6; then y1 in Roots(g) by POLYNOM5:def 9; 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 set 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 9; then eval(<%x%>,z) = 0.L by A18,POLYNOM5:def 6; hence contradiction by A17; end; hence thesis; end; for k be Element of NAT holds P[k] from NAT_1:sch 1(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 Element of 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 Element of NAT holds P[k] from NAT_1:sch 1(A4,A2); hence thesis; end; Lm14: for p be Prime,L be Field, n be Nat st 0)`^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 6; hence thesis by POLYNOM5:def 9; end; A14: the carrier of gr {a} c= Roots(f) proof let x be set; assume A15: 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:40; then reconsider x1=x as Element of Z/Z*(p) by STRUCT_0:def 5; x1 in gr {a} by A15,STRUCT_0:def 5; 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 n0 + 1 c= m by A17,A10,CARD_1:41; 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 by STRUCT_0:def 5; 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 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; 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 set 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 Function of NAT,the carrier of ZP such that A23: f.0 = a & for n being Element of NAT holds P[n,f.n,f.(n+1)] from RECDEF_1:sch 2(A4); deffunc F(Element of NAT) =ord (f.$1); consider g be Function of NAT,NAT such that A24: for k be Element of NAT holds g.k=F(k) from FUNCT_2:sch 4; A25: now let k be Element of NAT; A26: g.(k+1) = ord (f.(k+1)) by A24; g.k = ord (f.k) by A24; hence g.k < g.(k+1) by A23,A26; end; A27: 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); A28: now let m be Element of NAT; assume A29: P[m]; g.(k+1+m) < g.((k+1+m) + 1) by A25; hence P[m+1] by A29,XXREAL_0:2; end; A30: P[ 0 ] by A25; for m be Element of NAT holds P[m] from NAT_1:sch 1(A30,A28); hence thesis; end; A31: for k,m be Element of NAT st k < m holds g.k< g.m proof let k,m be Element of NAT; assume A32: k < m; then m-k is Element of NAT by INT_1:5; then reconsider mk=m-k as Nat; m-k <> 0 by A32; then consider n0 be Nat such that A33: mk=n0+1 by NAT_1:6; reconsider n=n0 as Element of NAT by ORDINAL1:def 12; m=k+1+n by A33; hence thesis by A27; end; now let x1,x2 be set; assume that A34: x1 in NAT and A35: x2 in NAT and A36: g.x1 = g.x2; reconsider xx1=x1,xx2=x2 as Element of NAT by A34,A35; A37: xx2 <= xx1 by A31,A36; xx1 <= xx2 by A31,A36; hence x2=x1 by A37,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 A38: card rng g = card NAT by FUNCT_2:def 1; rng g c= Segm(card ZP) proof let y be set; assume y in rng g; then consider x be set such that A39: x in NAT and A40: y=g.x by FUNCT_2:11; reconsider x as Element of NAT by A39; reconsider gg=g.x as Element of NAT; g.x =ord (f.x) by A24; then gg < card ZP by A2; hence thesis by A40,ALGSEQ_1:1; end; hence contradiction by A38; end;