:: Uniqueness of factoring an integer and multiplicative group $Z/pZ^{*}$
:: by Hiroyuki Okazaki and Yasunari Shidama
::
:: Received January 31, 2008
:: Copyright (c) 2008-2018 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;