:: Basic Properties of Primitive Root and Order Function :: by Na Ma and Xiquan Liang :: :: Received August 6, 2012 :: Copyright (c) 2012-2019 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, INT_1, NAT_1, SUBSET_1, EQREL_1, EULER_1, FINSEQ_1, INT_4, MEMBER_1, TARSKI, REAL_1, ARYTM_3, FUNCT_1, RELAT_1, FINSET_1, CARD_1, XBOOLE_0, ARYTM_1, INT_2, XXREAL_0, COMPLEX1, NEWTON, SQUARE_1, PARTFUN1, INT_8, PEPIN, INT_5, POLYEQ_3, ABIAN, CARD_3, ORDINAL4, XCMPLX_0; notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, INT_1, NAT_1, INT_2, NAT_D, FUNCT_1, FINSEQ_1, RELSET_1, EULER_1, TREES_4, EQREL_1, PARTFUN1, FINSET_1, WSIERP_1, NEWTON, MEMBER_1, ABIAN, PEPIN, INT_4, INT_5, POLYEQ_3; constructors EULER_1, WSIERP_1, PEPIN, NAT_3, NAT_D, INTEGRA2, RELSET_1, ABIAN, INT_4, INT_5, POLYEQ_3; registrations RELAT_1, FINSEQ_1, CARD_1, NAT_1, INT_1, MEMBERED, FINSET_1, NEWTON, NAT_3, XXREAL_0, NUMBERS, XBOOLE_0, XREAL_0, ORDINAL1, VALUED_0, ABIAN, MEMBER_1, XCMPLX_0, WSIERP_1, INT_4; requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve i,s,t,m,n,k for Nat, c,d,e for Element of NAT, fn for FinSequence of NAT, x,y for Integer; definition ::: should be moved to EULER_1 let m be Nat; func RelPrimes(m) -> set equals :: INT_8:def 1 {k where k is Element of NAT:m,k are_coprime & 1<=k & k<=m}; end; theorem :: INT_8:1 RelPrimes(m) c= Seg m; definition let m be Nat; redefine func RelPrimes(m) -> Subset of NAT; end; registration let m be Nat; cluster RelPrimes(m) -> finite; end; theorem :: INT_8:2 1<=m implies RelPrimes(m) <> {}; theorem :: INT_8:3 for X being Subset of INT, a being Integer holds x in a ** X iff ex y being Integer st y in X & x = a * y; theorem :: INT_8:4 ex r be Nat st (1+s)|^t = 1 + t*s + (t choose 2)*s^2+r*s^3; theorem :: INT_8:5 n>1 & i,n are_coprime implies i <> 0; theorem :: INT_8:6 for a,b be Integer,m be Nat st a*b mod m = 1 & a mod m = 1 holds b mod m = 1; theorem :: INT_8:7 for x be odd Integer,k be Nat st k>=3 holds x|^(2|^(k-'2)) mod 2|^k = 1; reserve p for Prime; theorem :: INT_8:8 m>=1 implies Euler(p|^m) = p|^m - p|^(m-'1); theorem :: INT_8:9 n>1 & i,n are_coprime implies order(i,n) divides Euler n; theorem :: INT_8:10 for i,n st n>1 & i,n are_coprime holds i|^s,i|^t are_congruent_mod n iff s,t are_congruent_mod order(i,n); theorem :: INT_8:11 for i,n st n>1 & i,n are_coprime holds i|^s,1 are_congruent_mod n iff order(i,n) divides s; theorem :: INT_8:12 n>1 & i,n are_coprime & len fn = order(i,n) & (for d st d in dom fn holds fn.d =i|^(d-'1)) implies (for d,e st d in dom fn & e in dom fn & d<>e holds not fn.d,fn.e are_congruent_mod n); theorem :: INT_8:13 n>1 & i,n are_coprime & len fn = order(i,n) & (for d st d in dom fn holds fn.d = i|^(d-'1)) implies (for d st d in dom fn holds fn.d|^order(i,n) mod n = 1); theorem :: INT_8:14 n>1 & i,n are_coprime implies order(i|^s,n) = order(i,n) div (order(i,n) gcd s); theorem :: INT_8:15 for i,n st n>1 & i,n are_coprime holds order(i,n),s are_coprime iff order(i|^s,n) = order(i,n); theorem :: INT_8:16 n>1 & i,n are_coprime & order(i,n) = s*t implies order(i|^s,n) = t; theorem :: INT_8:17 n>1 & s,n are_coprime & t,n are_coprime & order(s,n),order(t,n) are_coprime implies order(s*t,n) = order(s,n)*order(t,n); reserve fp,fr for FinSequence of NAT; theorem :: INT_8:18 n>1 & s,n are_coprime & t,n are_coprime & order(s*t,n) = order(s,n)*order(t,n) implies order(s,n),order(t,n) are_coprime; theorem :: INT_8:19 n>1 & s,n are_coprime & s*t mod n = 1 implies order(s,n)=order(t,n); theorem :: INT_8:20 n>1 & m>1 & i,n are_coprime & m divides n implies order(i,m) divides order(i,n); theorem :: INT_8:21 n>1 & m>1 & m,n are_coprime & i,m*n are_coprime implies order(i,m*n) = order(i,m) lcm order(i,n); definition let X be set,m be Nat; pred X is_RRS_of m means :: INT_8:def 2 ex fp be FinSequence of INT st len fp = len(Sgm RelPrimes(m)) & (for d st d in dom fp holds fp.d in Class(Cong m,(Sgm RelPrimes(m)).d)) & X = rng fp; end; theorem :: INT_8:22 RelPrimes(m) is_RRS_of m; theorem :: INT_8:23 d in dom Sgm RelPrimes(m) & e in dom Sgm RelPrimes(m) & d<>e implies not (Sgm RelPrimes(m)).d,(Sgm RelPrimes(m)).e are_congruent_mod m; theorem :: INT_8:24 for X be finite set st X is_RRS_of m holds card X = Euler m & (for x,y be Integer st x in X & y in X & x<>y holds not x,y are_congruent_mod m) & (for x be Integer st x in X holds x,m are_coprime); theorem :: INT_8:25 {} is_RRS_of m iff m = 0; theorem :: INT_8:26 for X be finite Subset of INT st ( 1y holds not x,y are_congruent_mod m) & (for x be Integer st x in X holds x,m are_coprime)) holds X is_RRS_of m; theorem :: INT_8:27 for X be finite Subset of INT,a be Integer st (m>1 & a,m are_coprime & X is_RRS_of m) holds (a ** X) is_RRS_of m; definition let i,n; pred i is_primitive_root_of n means :: INT_8:def 3 order(i,n) = Euler n; end; theorem :: INT_8:28 n>1 & i,n are_coprime implies (i is_primitive_root_of n iff for fn st len fn = Euler n & (for d being Nat st d in dom fn holds fn.d = i|^d) holds rng fn is_RRS_of n); theorem :: INT_8:29 p>2 & i,p are_coprime & i is_primitive_root_of p implies (for k be Nat holds not i|^(2*k+1) is_quadratic_residue_mod p); theorem :: INT_8:30 for k be Nat st k>=3 holds (for m st m,2|^k are_coprime holds not m is_primitive_root_of 2|^k); theorem :: INT_8:31 p>2 & k>=2 & i,p are_coprime & i is_primitive_root_of p & i|^(p-'1) mod p^2 <> 1 implies i|^(Euler(p|^(k-'1))) mod p|^k <> 1; theorem :: INT_8:32 n>1 & len fp>=2 & (for d st d in dom fp holds fp.d,n are_coprime) implies for fr st len fr = len fp & (for d st d in dom fr holds fr.d = order(fp.d,n)) & (for d,e st d in dom fr & e in dom fr & d <> e holds fr.d,fr.e are_coprime) holds order((Product fp),n) = Product fr;