let i, s, n be Nat; ( n > 1 & i,n are_coprime implies order ((i |^ s),n) = (order (i,n)) div ((order (i,n)) gcd s) )
assume A1:
( n > 1 & i,n are_coprime )
; order ((i |^ s),n) = (order (i,n)) div ((order (i,n)) gcd s)
then A2:
( i <> 0 & n <> 0 )
by Th5;
i gcd n = 1
by A1, INT_2:def 3;
then
(i |^ s) gcd n = 1
by A2, NAT_4:10;
then A3:
i |^ s,n are_coprime
by INT_2:def 3;
A4:
order (i,n) > 0
by A1, PEPIN:def 2;
set K1 = (order (i,n)) gcd s;
set K2 = (order (i,n)) div ((order (i,n)) gcd s);
per cases
( s = 0 or s > 0 )
;
suppose A5:
s = 0
;
order ((i |^ s),n) = (order (i,n)) div ((order (i,n)) gcd s)then
(order (i,n)) gcd s = order (
i,
n)
by NEWTON:52;
then A6:
(order (i,n)) div ((order (i,n)) gcd s) = 1
by A4, NAT_2:3;
i |^ s = 1
by A5, NEWTON:4;
hence
order (
(i |^ s),
n)
= (order (i,n)) div ((order (i,n)) gcd s)
by A1, A6, PEPIN:46;
verum end; suppose A7:
s > 0
;
order ((i |^ s),n) = (order (i,n)) div ((order (i,n)) gcd s)
(
(order (i,n)) gcd s divides order (
i,
n) &
(order (i,n)) gcd s divides s )
by NAT_D:def 5;
then A8:
(
order (
i,
n)
= ((order (i,n)) div ((order (i,n)) gcd s)) * ((order (i,n)) gcd s) &
s = (s div ((order (i,n)) gcd s)) * ((order (i,n)) gcd s) )
by NAT_D:3;
then A9:
(
(order (i,n)) div ((order (i,n)) gcd s) <> 0 &
(order (i,n)) gcd s <> 0 &
s div ((order (i,n)) gcd s) <> 0 )
by A1, A7, PEPIN:def 2;
A10:
(order (i,n)) div ((order (i,n)) gcd s),
s div ((order (i,n)) gcd s) are_coprime
by A8, A9, EULER_1:6;
s * ((order (i,n)) div ((order (i,n)) gcd s)) = (s div ((order (i,n)) gcd s)) * (order (i,n))
by A8;
then
order (
i,
n)
divides s * ((order (i,n)) div ((order (i,n)) gcd s))
by NAT_D:def 3;
then
(i |^ (s * ((order (i,n)) div ((order (i,n)) gcd s)))) mod n = 1
by A1, PEPIN:48;
then A11:
((i |^ s) |^ ((order (i,n)) div ((order (i,n)) gcd s))) mod n = 1
by NEWTON:9;
for
k being
Nat st
k > 0 &
((i |^ s) |^ k) mod n = 1 holds
(
0 < (order (i,n)) div ((order (i,n)) gcd s) &
(order (i,n)) div ((order (i,n)) gcd s) <= k )
proof
let k be
Nat;
( k > 0 & ((i |^ s) |^ k) mod n = 1 implies ( 0 < (order (i,n)) div ((order (i,n)) gcd s) & (order (i,n)) div ((order (i,n)) gcd s) <= k ) )
reconsider k1 =
k as
Element of
NAT by ORDINAL1:def 12;
assume A12:
(
k > 0 &
((i |^ s) |^ k) mod n = 1 )
;
( 0 < (order (i,n)) div ((order (i,n)) gcd s) & (order (i,n)) div ((order (i,n)) gcd s) <= k )
then
(i |^ (s * k)) mod n = 1
by NEWTON:9;
then
((order (i,n)) div ((order (i,n)) gcd s)) * ((order (i,n)) gcd s) divides ((s div ((order (i,n)) gcd s)) * k1) * ((order (i,n)) gcd s)
by A8, A1, PEPIN:47;
then
(order (i,n)) div ((order (i,n)) gcd s) divides (s div ((order (i,n)) gcd s)) * k1
by A9, PYTHTRIP:7;
hence
(
0 < (order (i,n)) div ((order (i,n)) gcd s) &
(order (i,n)) div ((order (i,n)) gcd s) <= k )
by A9, A12, A10, PEPIN:3, NAT_D:7;
verum
end; hence
order (
(i |^ s),
n)
= (order (i,n)) div ((order (i,n)) gcd s)
by A1, A3, A9, A11, PEPIN:def 2;
verum