let i, n be Nat; :: thesis: ( n > 1 & i,n are_coprime implies ( 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 ) )
assume A1: ( n > 1 & i,n are_coprime ) ; :: thesis: ( 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 )
then A2: i <> 0 by Th5;
reconsider z = 0 , j = 1 as Element of REAL by XREAL_0:def 1;
i - 1 >= 0 by A2, INT_1:52;
then A3: (i - 1) + j >= z + j by XREAL_1:7;
A4: i gcd n = 1 by A1, INT_2:def 3;
thus ( i is_primitive_root_of n implies 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 ) :: thesis: ( ( 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 ) implies i is_primitive_root_of n )
proof
assume i is_primitive_root_of n ; :: thesis: 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
then A5: order (i,n) = Euler n ;
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
let fn be FinSequence of NAT ; :: thesis: ( len fn = Euler n & ( for d being Nat st d in dom fn holds
fn . d = i |^ d ) implies rng fn is_RRS_of n )
assume A6: ( len fn = Euler n & ( for d being Nat st d in dom fn holds
fn . d = i |^ d ) ) ; :: thesis: rng fn is_RRS_of n
fn is one-to-one
proof
per cases ( i = 1 or i > 1 ) by A3, XXREAL_0:1;
suppose A8: i > 1 ; :: thesis: fn is one-to-one
for x1, x2 being object st x1 in dom fn & x2 in dom fn & fn . x1 = fn . x2 holds
x1 = x2
proof
let x1, x2 be object ; :: thesis: ( x1 in dom fn & x2 in dom fn & fn . x1 = fn . x2 implies x1 = x2 )
assume A9: ( x1 in dom fn & x2 in dom fn & fn . x1 = fn . x2 ) ; :: thesis: x1 = x2
then reconsider x1 = x1, x2 = x2 as Element of NAT ;
i |^ x1 = fn . x2 by A9, A6
.= i |^ x2 by A9, A6 ;
hence x1 = x2 by A8, PEPIN:30; :: thesis: verum
end;
hence fn is one-to-one by FUNCT_1:def 4; :: thesis: verum
end;
end;
end;
then A10: card (rng fn) = Euler n by A6, FINSEQ_4:62;
A11: for x, y being Integer st x in rng fn & y in rng fn & x <> y holds
not x,y are_congruent_mod n
proof
let x, y be Integer; :: thesis: ( x in rng fn & y in rng fn & x <> y implies not x,y are_congruent_mod n )
assume A12: ( x in rng fn & y in rng fn & x <> y & x,y are_congruent_mod n ) ; :: thesis: contradiction
then consider s being Nat such that
A13: ( s in dom fn & fn . s = x ) by FINSEQ_2:10;
consider t being Nat such that
A14: ( t in dom fn & fn . t = y ) by A12, FINSEQ_2:10;
A15: ( x = i |^ s & y = i |^ t ) by A13, A14, A6;
A16: ( 1 <= s & s <= order (i,n) & 1 <= t & t <= order (i,n) ) by A13, A14, A5, A6, FINSEQ_3:25;
per cases ( s > t or s < t ) by A12, A13, A14, XXREAL_0:1;
suppose s > t ; :: thesis: contradiction
then A17: s - t > 0 by XREAL_1:50;
then reconsider k = s - t as Element of NAT by INT_1:3;
(i |^ s) - (i |^ t) = (i |^ (t + k)) - (i |^ t)
.= ((i |^ t) * (i |^ k)) - ((i |^ t) * 1) by NEWTON:8
.= (i |^ t) * ((i |^ k) - 1) ;
then A18: n divides (i |^ t) * ((i |^ k) - 1) by A15, A12, INT_2:15;
(i |^ t) gcd n = 1 by A2, A4, A1, NAT_4:10;
then n divides (i |^ k) - 1 by A18, WSIERP_1:29;
then i |^ k,1 are_congruent_mod n by INT_2:15;
then (i |^ k) mod n = 1 mod n by NAT_D:64
.= 1 by A1, PEPIN:5 ;
then A19: order (i,n) <= k by A17, A1, PEPIN:47, NAT_D:7;
( k <= (order (i,n)) - 1 & (order (i,n)) - 1 < order (i,n) ) by A16, XREAL_1:13, XREAL_1:146;
hence contradiction by A19, XXREAL_0:2; :: thesis: verum
end;
suppose s < t ; :: thesis: contradiction
then A20: t - s > 0 by XREAL_1:50;
then reconsider k = t - s as Element of NAT by INT_1:3;
A21: (i |^ t) - (i |^ s) = (i |^ (s + k)) - (i |^ s)
.= ((i |^ s) * (i |^ k)) - ((i |^ s) * 1) by NEWTON:8
.= (i |^ s) * ((i |^ k) - 1) ;
i |^ t,i |^ s are_congruent_mod n by A15, A12, INT_1:14;
then A22: n divides (i |^ s) * ((i |^ k) - 1) by A21, INT_2:15;
(i |^ s) gcd n = 1 by A2, A4, A1, NAT_4:10;
then n divides (i |^ k) - 1 by A22, WSIERP_1:29;
then i |^ k,1 are_congruent_mod n by INT_2:15;
then (i |^ k) mod n = 1 mod n by NAT_D:64
.= 1 by A1, PEPIN:5 ;
then A23: order (i,n) <= k by A20, A1, PEPIN:47, NAT_D:7;
( k <= (order (i,n)) - 1 & (order (i,n)) - 1 < order (i,n) ) by A16, XREAL_1:13, XREAL_1:146;
hence contradiction by A23, XXREAL_0:2; :: thesis: verum
end;
end;
end;
A24: for x being Integer st x in rng fn holds
x,n are_coprime
proof
let x be Integer; :: thesis: ( x in rng fn implies x,n are_coprime )
assume x in rng fn ; :: thesis: x,n are_coprime
then consider s being Nat such that
A25: ( s in dom fn & fn . s = x ) by FINSEQ_2:10;
A26: x = i |^ s by A25, A6;
(i |^ s) gcd n = 1 by A2, A4, A1, NAT_4:10;
hence x,n are_coprime by A26, INT_2:def 3; :: thesis: verum
end;
rng fn c= INT by RELAT_1:def 19;
hence rng fn is_RRS_of n by A1, A10, A11, A24, Th26; :: thesis: verum
end;
hence 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 ; :: thesis: verum
end;
assume A27: 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 ; :: thesis: i is_primitive_root_of n
deffunc H1( Nat) -> set = i |^ $1;
consider f being FinSequence such that
A28: ( len f = Euler n & ( for d being Nat st d in dom f holds
f . d = H1(d) ) ) from FINSEQ_1:sch 2();
 for s being Nat st s in dom f holds
f . s in NAT
proof
let s be Nat; :: thesis: ( s in dom f implies f . s in NAT )
assume A29: s in dom f ; :: thesis: f . s in NAT
f . s = i |^ s by A28, A29;
hence f . s in NAT by ORDINAL1:def 12; :: thesis: verum
end;
then reconsider f = f as FinSequence of NAT by FINSEQ_2:12;
A30: rng f is_RRS_of n by A28, A27;
then ( card (rng f) = Euler n & ( for x, y being Integer st x in rng f & y in rng f & x <> y holds
not x,y are_congruent_mod n ) ) by Th24;
then A31: f is one-to-one by A28, FINSEQ_4:62;
Euler n <> 0 by A1, PEPIN:42;
then A33: Euler n > 0 ;
A34: Euler n >= 1 by A1, PEPIN:42, NAT_1:14;
A35: (i |^ (Euler n)) mod n = 1 by A1, Th5, EULER_2:18;
for s being Nat st s > 0 & (i |^ s) mod n = 1 holds
Euler n <= s
proof
let s be Nat; :: thesis: ( s > 0 & (i |^ s) mod n = 1 implies Euler n <= s )
assume A36: ( s > 0 & (i |^ s) mod n = 1 ) ; :: thesis: Euler n <= s
now :: thesis: not s < Euler n
assume s < Euler n ; :: thesis: contradiction
then A37: (Euler n) - s > 0 by XREAL_1:50;
then reconsider k = (Euler n) - s as Element of NAT by INT_1:3;
A38: ( k < Euler n & k >= 1 ) by A36, A37, XREAL_1:44, NAT_1:14;
then A39: ( k in dom f & Euler n in dom f ) by A28, A34, FINSEQ_3:25;
then A40: ( f . k in rng f & f . (Euler n) in rng f ) by FUNCT_1:3;
f . k <> f . (Euler n) by A39, A31, A38, FUNCT_1:def 4;
then not f . k,f . (Euler n) are_congruent_mod n by A40, A30, Th24;
then not i |^ k,f . (Euler n) are_congruent_mod n by A39, A28;
then A41: not i |^ k,i |^ (Euler n) are_congruent_mod n by A39, A28;
i |^ (Euler n),i |^ s are_congruent_mod n by A36, A35, A1, NAT_D:64;
then A42: n divides (i |^ (Euler n)) - (i |^ s) by INT_2:15;
A43: (i |^ (Euler n)) - (i |^ s) = (i |^ (s + k)) - (i |^ s)
.= ((i |^ s) * (i |^ k)) - ((i |^ s) * 1) by NEWTON:8
.= (i |^ s) * ((i |^ k) - 1) ;
(i |^ s) gcd n = 1 by A2, A4, A1, NAT_4:10;
then A44: n divides (i |^ k) - 1 by A42, A43, WSIERP_1:29;
(i |^ (Euler n)) mod n = 1 mod n by A1, A35, PEPIN:5;
then i |^ (Euler n),1 are_congruent_mod n by A1, NAT_D:64;
then n divides (i |^ (Euler n)) - 1 by INT_2:15;
then n divides ((i |^ k) - 1) - ((i |^ (Euler n)) - 1) by A44, INT_5:1;
then n divides (i |^ k) - (i |^ (Euler n)) ;
hence contradiction by A41, INT_2:15; :: thesis: verum
end;
hence Euler n <= s ; :: thesis: verum
end;
then order (i,n) = Euler n by A1, A33, A35, PEPIN:def 2;
hence i is_primitive_root_of n ; :: thesis: verum