:: Basic Properties of Primitive Root and Order Function
:: by Na Ma and Xiquan Liang
::
:: Received August 6, 2012
:: Copyright (c) 2012-2018 Association of Mizar Users

definition
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 ) } ;
correctness
coherence
{ k where k is Element of NAT : ( m,k are_coprime & 1 <= k & k <= m ) } is set
;
;
end;

:: deftheorem defines RelPrimes INT_8:def 1 :
for m being Nat holds RelPrimes m = { k where k is Element of NAT : ( m,k are_coprime & 1 <= k & k <= m ) } ;

theorem Th1: :: INT_8:1
for m being Nat holds RelPrimes m c= Seg m
proof end;

definition
let m be Nat;
:: original: RelPrimes
redefine func RelPrimes m -> Subset of NAT;
coherence
RelPrimes m is Subset of NAT
proof end;
end;

registration
let m be Nat;
cluster (m) -> finite ;
coherence
proof end;
end;

theorem :: INT_8:2
for m being Nat st 1 <= m holds
RelPrimes m <> {}
proof end;

theorem Th3: :: INT_8:3
for x being Integer
for X being Subset of INT
for a being Integer holds
( x in a ** X iff ex y being Integer st
( y in X & x = a * y ) )
proof end;

theorem Th4: :: INT_8:4
for s, t being Nat ex r being Nat st (1 + s) |^ t = ((1 + (t * s)) + ((t choose 2) * (s ^2))) + (r * (s ^3))
proof end;

theorem Th5: :: INT_8:5
for i, n being Nat st n > 1 & i,n are_coprime holds
i <> 0
proof end;

theorem Th6: :: INT_8:6
for a, b being Integer
for m being Nat st (a * b) mod m = 1 & a mod m = 1 holds
b mod m = 1
proof end;

Lm1: for x being Integer holds 2 divides x * (x + 1)
proof end;

theorem Th7: :: INT_8:7
for x being odd Integer
for k being Nat st k >= 3 holds
(x |^ (2 |^ (k -' 2))) mod (2 |^ k) = 1
proof end;

Lm2: for m, n, k being Nat st k <= n holds
m |^ k divides m |^ n

by NEWTON:89;

theorem Th8: :: INT_8:8
for m being Nat
for p being Prime st m >= 1 holds
Euler (p |^ m) = (p |^ m) - (p |^ (m -' 1))
proof end;

theorem :: INT_8:9
for i, n being Nat st n > 1 & i,n are_coprime holds
order (i,n) divides Euler n
proof end;

theorem Th10: :: INT_8:10
for s, t, i, n being Nat 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) )
proof end;

theorem :: INT_8:11
for s, i, n being Nat st n > 1 & i,n are_coprime holds
( i |^ s,1 are_congruent_mod n iff order (i,n) divides s )
proof end;

theorem :: INT_8:12
for i, n being Nat
for fn being FinSequence of NAT st n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) holds
for d, e being Element of NAT st d in dom fn & e in dom fn & d <> e holds
not fn . d,fn . e are_congruent_mod n
proof end;

theorem :: INT_8:13
for i, n being Nat
for fn being FinSequence of NAT st n > 1 & i,n are_coprime & len fn = order (i,n) & ( for d being Element of NAT st d in dom fn holds
fn . d = i |^ (d -' 1) ) holds
for d being Element of NAT st d in dom fn holds
((fn . d) |^ (order (i,n))) mod n = 1
proof end;

theorem Th14: :: INT_8:14
for i, s, n being Nat st n > 1 & i,n are_coprime holds
order ((i |^ s),n) = (order (i,n)) div ((order (i,n)) gcd s)
proof end;

theorem :: INT_8:15
for s, i, n being Nat st n > 1 & i,n are_coprime holds
( order (i,n),s are_coprime iff order ((i |^ s),n) = order (i,n) )
proof end;

theorem :: INT_8:16
for i, s, t, n being Nat st n > 1 & i,n are_coprime & order (i,n) = s * t holds
order ((i |^ s),n) = t
proof end;

theorem Th17: :: INT_8:17
for s, t, n being Nat st n > 1 & s,n are_coprime & t,n are_coprime & order (s,n), order (t,n) are_coprime holds
order ((s * t),n) = (order (s,n)) * (order (t,n))
proof end;

theorem :: INT_8:18
for s, t, n being Nat st n > 1 & s,n are_coprime & t,n are_coprime & order ((s * t),n) = (order (s,n)) * (order (t,n)) holds
order (s,n), order (t,n) are_coprime
proof end;

theorem :: INT_8:19
for s, t, n being Nat st n > 1 & s,n are_coprime & (s * t) mod n = 1 holds
order (s,n) = order (t,n)
proof end;

theorem Th20: :: INT_8:20
for i, m, n being Nat st n > 1 & m > 1 & i,n are_coprime & m divides n holds
order (i,m) divides order (i,n)
proof end;

theorem :: INT_8:21
for i, m, n being Nat st n > 1 & m > 1 & m,n are_coprime & i,m * n are_coprime holds
order (i,(m * n)) = (order (i,m)) lcm (order (i,n))
proof end;

definition
let X be set ;
let m be Nat;
pred X is_RRS_of m means :: INT_8:def 2
ex fp being FinSequence of INT st
( len fp = len (Sgm ()) & ( for d being Element of NAT st d in dom fp holds
fp . d in Class ((Cong m),((Sgm ()) . d)) ) & X = rng fp );
end;

:: deftheorem defines is_RRS_of INT_8:def 2 :
for X being set
for m being Nat holds
( X is_RRS_of m iff ex fp being FinSequence of INT st
( len fp = len (Sgm ()) & ( for d being Element of NAT st d in dom fp holds
fp . d in Class ((Cong m),((Sgm ()) . d)) ) & X = rng fp ) );

theorem Th22: :: INT_8:22
for m being Nat holds RelPrimes m is_RRS_of m
proof end;

theorem Th23: :: INT_8:23
for m being Nat
for d, e being Element of NAT st d in dom (Sgm ()) & e in dom (Sgm ()) & d <> e holds
not (Sgm ()) . d,(Sgm ()) . e are_congruent_mod m
proof end;

theorem Th24: :: INT_8:24
for m being Nat
for X being finite set st X is_RRS_of m holds
( card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) )
proof end;

Lm3: for X being finite set st card X = 0 holds
X = {}

;

theorem :: INT_8:25
for m being Nat holds
( {} is_RRS_of m iff m = 0 )
proof end;

theorem Th26: :: INT_8:26
for m being Nat
for X being finite Subset of INT st 1 < m & card X = Euler m & ( for x, y being Integer st x in X & y in X & x <> y holds
not x,y are_congruent_mod m ) & ( for x being Integer st x in X holds
x,m are_coprime ) holds
X is_RRS_of m
proof end;

theorem :: INT_8:27
for m being Nat
for X being finite Subset of INT
for a being Integer st m > 1 & a,m are_coprime & X is_RRS_of m holds
a ** X is_RRS_of m
proof end;

definition
let i, n be Nat;
pred i is_primitive_root_of n means :: INT_8:def 3
order (i,n) = Euler n;
end;

:: deftheorem defines is_primitive_root_of INT_8:def 3 :
for i, n being Nat holds
( i is_primitive_root_of n iff order (i,n) = Euler n );

theorem :: INT_8:28
for i, n being Nat st n > 1 & i,n are_coprime holds
( i is_primitive_root_of n iff for fn being FinSequence of NAT 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 )
proof end;

theorem :: INT_8:29
for i being Nat
for p being Prime st p > 2 & i,p are_coprime & i is_primitive_root_of p holds
for k being Nat holds not i |^ ((2 * k) + 1) is_quadratic_residue_mod p
proof end;

theorem :: INT_8:30
for k being Nat st k >= 3 holds
for m being Nat st m,2 |^ k are_coprime holds
not m is_primitive_root_of 2 |^ k
proof end;

theorem :: INT_8:31
for i, k being Nat
for p being Prime st p > 2 & k >= 2 & i,p are_coprime & i is_primitive_root_of p & (i |^ (p -' 1)) mod (p ^2) <> 1 holds
(i |^ (Euler (p |^ (k -' 1)))) mod (p |^ k) <> 1
proof end;

theorem :: INT_8:32
for n being Nat
for fp being FinSequence of NAT st n > 1 & len fp >= 2 & ( for d being Element of NAT st d in dom fp holds
fp . d,n are_coprime ) holds
for fr being FinSequence of NAT st len fr = len fp & ( for d being Element of NAT st d in dom fr holds
fr . d = order ((fp . d),n) ) & ( for d, e being Element of NAT 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
proof end;