let p, n, i be Nat; :: thesis: ( p > 1 & n > 0 & (i |^ n) mod p = 1 & i,p are_relative_prime implies order i,p divides n )
assume A1:
( p > 1 & n > 0 & (i |^ n) mod p = 1 & i,p are_relative_prime )
; :: thesis: order i,p divides n
then A2:
(i |^ (order i,p)) mod p = 1
by Def2;
A3:
order i,p <> 0
by A1, Def2;
n mod (order i,p) = 0
proof
assume A4:
n mod (order i,p) <> 0
;
:: thesis: contradiction
set I =
n mod (order i,p);
consider t being
Nat such that A5:
(
n = ((order i,p) * t) + (n mod (order i,p)) &
n mod (order i,p) < order i,
p )
by A3, NAT_D:def 2;
reconsider t =
t as
Element of
NAT by ORDINAL1:def 13;
((i |^ ((order i,p) * t)) * (i |^ (n mod (order i,p)))) mod p = 1
by A1, A5, NEWTON:13;
then
(((i |^ (order i,p)) |^ t) * (i |^ (n mod (order i,p)))) mod p = 1
by NEWTON:14;
then
((((i |^ (order i,p)) |^ t) mod p) * (i |^ (n mod (order i,p)))) mod p = 1
by EULER_2:10;
then A6:
(1 * (i |^ (n mod (order i,p)))) mod p = 1
by A1, A2, Th36;
n mod (order i,p) > 0
by A4;
hence
contradiction
by A1, A5, A6, Def2;
:: thesis: verum
end;
hence
order i,p divides n
by A3, Th6; :: thesis: verum