let i, n, p be Nat; :: thesis: ( 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 ; :: thesis: 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 (1 * (i |^ (n mod (order (i,p))))) mod p = 1 by A1, A5, Th35;
hence n mod (order (i,p)) = 0 by A1, A3, A7, Def2; :: thesis: verum

end;

hence order (i,p) divides n by A4, Th6; :: thesis: verum