let i, n, p be Nat; ( p > 1 & (i |^ n) mod p = 1 & i,p are_coprime implies order (i,p) divides n )
assume that
A1:
p > 1
and
A2:
(i |^ n) mod p = 1
and
A3:
i,p are_coprime
; 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 12;
((i |^ ((order (i,p)) * t)) * (i |^ (n mod (order (i,p))))) mod p = 1
by A2, A6, NEWTON:8;
then
(((i |^ (order (i,p))) |^ t) * (i |^ (n mod (order (i,p))))) mod p = 1
by NEWTON:9;
then
((((i |^ (order (i,p))) |^ t) mod p) * (i |^ (n mod (order (i,p))))) mod p = 1
by EULER_2:8;
then A8:
(1 * (i |^ (n mod (order (i,p))))) mod p = 1
by A1, A5, Th35;
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