let i, s, n be Nat; :: thesis: ( 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 ) ; :: thesis: 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 ; :: thesis: 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; :: thesis: verum

end;

suppose A7: s > 0 ; :: thesis: 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
(order (i,n)) div ((order (i,n)) gcd s) <= k

proof

let k be Nat; :: thesis: ( k > 0 & ((i |^ s) |^ k) mod n = 1 implies (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 ) ; :: thesis: (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 (order (i,n)) div ((order (i,n)) gcd s) <= k by A12, A10, PEPIN:3, NAT_D:7; :: thesis: verum

end;

hence order ((i |^ s),n) = (order (i,n)) div ((order (i,n)) gcd s) by A1, A3, A9, A11, PEPIN:def 2; :: thesis: verum

end;

end;