:: by Na Ma and Xiquan Liang

::

:: Received August 6, 2012

:: Copyright (c) 2012-2016 Association of Mizar Users

definition

let m be Nat;

coherence

{ k where k is Element of NAT : ( m,k are_coprime & 1 <= k & k <= m ) } is set ;

;

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

coherence

{ k where k is Element of NAT : ( m,k are_coprime & 1 <= k & k <= m ) } is set ;

;

:: 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 ) } ;

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

definition

let m be Nat;

:: original: RelPrimes

redefine func RelPrimes m -> Subset of NAT;

coherence

RelPrimes m is Subset of NAT

end;
:: original: RelPrimes

redefine func RelPrimes m -> Subset of NAT;

coherence

RelPrimes m is Subset of NAT

proof end;

registration
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 ) )

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;

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

proof end;

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

m |^ k divides m |^ n

by NEWTON:89;

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) )

( 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 )

( 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

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

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)

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) )

( 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

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))

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

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)

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)

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))

order (i,(m * n)) = (order (i,m)) lcm (order (i,n))

proof 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 ) );

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 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

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 ) )

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 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

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

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
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 );

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 )

( 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

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

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

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

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;