:: Uniqueness of factoring an integer and multiplicative group $Z/pZ^{*}$ :: by Hiroyuki Okazaki and Yasunari Shidama :: :: Received January 31, 2008 :: Copyright (c) 2008-2021 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; begin :: Uniqueness of factoring an integer reserve x,y for object, X for set; theorem :: INT_7:1 for p being ManySortedSet of X st support p = {x} holds p = (X--> 0)+*(x,p.x) ; theorem :: INT_7:2 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; theorem :: INT_7:3 for X be set,p,q be ManySortedSet of X st p| (support p) = q| ( support q) holds p = q; theorem :: INT_7:4 for X be set,p,q be bag of X st support p = {} & support q={} holds p = q; definition let p be bag of SetPrimes; attr p is prime-factorization-like means :: INT_7:def 1 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; end; theorem :: INT_7:5 for p,q be Prime,n,m be Nat st p divides m*(q|^n) & p <> q holds p divides m; theorem :: INT_7:6 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; theorem :: INT_7:7 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); theorem :: INT_7:8 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; theorem :: INT_7:9 for n,m,k be non zero Nat st k = n lcm m holds support ppf k=(support ppf n) \/ (support ppf m); theorem :: INT_7:10 for X being set,b1,b2 being bag of X holds support min(b1,b2) = support b1 /\ support b2; theorem :: INT_7:11 for n,m,k be non zero Nat st k = n gcd m holds support ppf k = (support ppf n) /\ (support ppf m); theorem :: INT_7:12 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; theorem :: INT_7:13 for p be bag of SetPrimes st p is prime-factorization-like holds Product p <> 0; theorem :: INT_7:14 for p be bag of SetPrimes st p is prime-factorization-like holds Product p = 1 iff support p = {}; ::$N Fundamental Theorem of Arithmetic (uniqueness) theorem :: INT_7:15 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; theorem :: INT_7:16 for p be bag of SetPrimes, n be non zero Nat st p is prime-factorization-like & n = Product p holds (ppf n) = p; theorem :: INT_7:17 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; begin ::multiplicative group definition let n be Nat; assume 1 < n; func Segm0(n) -> non empty finite Subset of NAT equals :: INT_7:def 2 Segm(n) \ {0}; end; theorem :: INT_7:18 for n be Nat st 1 < n holds card Segm0(n) = n-1; definition let n be Prime; func multint0(n) -> BinOp of Segm0(n) equals :: INT_7:def 3 (multint n) || Segm0 n; end; theorem :: INT_7:19 for p be Prime holds multMagma(#Segm0(p),multint0(p)#) is associative commutative Group-like; definition let p be Prime; func Z/Z*(p) -> commutative Group equals :: INT_7:def 4 multMagma(#Segm0(p),multint0(p)#); end; theorem :: INT_7:20 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; theorem :: INT_7:21 for p be Prime holds 1_Z/Z*(p) =1 & 1_Z/Z*(p) = 1.(INT.Ring(p)); theorem :: INT_7:22 for p be Prime, x be Element of Z/Z*(p), x1 be Element of INT.Ring(p) st x=x1 holds x" = x1"; registration let p be Prime; cluster Z/Z*(p) -> finite; end; theorem :: INT_7:23 for p be Prime holds card Z/Z*(p) = p-1; theorem :: INT_7:24 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; theorem :: INT_7:25 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; theorem :: INT_7:26 for L be non empty ZeroStr, p being Polynomial of L st 0 <= deg p holds p is non-zero; theorem :: INT_7:27 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 ; theorem :: INT_7:28 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); theorem :: INT_7:29 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}; theorem :: INT_7:30 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; theorem :: INT_7:31 for p be Prime holds Z/Z*(p) is cyclic Group;