let p, i, n be Nat; ( p > 1 & (i |^ n) mod p = 1 & i,p are_relative_prime implies order i,p divides n )
assume that
A1:
p > 1
and
A2:
(i |^ n) mod p = 1
and
A3:
i,p are_relative_prime
; order i,p divides n
A4:
order i,p <> 0
by A1, A3, Def2;
A5:
(i |^ (order i,p)) mod p = 1
by A1, A3, Def2;
n mod (order i,p) = 0
proof
set I =
n mod (order i,p);
consider t being
Nat such that A6:
n = ((order i,p) * t) + (n mod (order i,p))
and A7:
n mod (order i,p) < order i,
p
by A4, 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 A2, A6, 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 A8:
(1 * (i |^ (n mod (order i,p)))) mod p = 1
by A1, A5, Th36;
assume
n mod (order i,p) <> 0
;
contradiction
hence
contradiction
by A1, A3, A7, A8, Def2;
verum
end;
hence
order i,p divides n
by A4, Th6; verum