:: Basic Properties of Primitive Root and Order Function
:: by Na Ma and Xiquan Liang
::
:: Received August 6, 2012
:: Copyright (c) 2012-2021 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 RelPrimes m -> finite ;

coherence
RelPrimes m is finite

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 (RelPrimes m)) & ( for d being Element of NAT st d in dom fp holds
fp . d in Class ((Cong m),((Sgm (RelPrimes m)) . 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 (RelPrimes m)) & ( for d being Element of NAT st d in dom fp holds
fp . d in Class ((Cong m),((Sgm (RelPrimes m)) . 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 (RelPrimes m)) & e in dom (Sgm (RelPrimes m)) & d <> e holds
not (Sgm (RelPrimes m)) . d,(Sgm (RelPrimes m)) . 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;