let p, i be Nat; :: thesis: ( p is prime & i,p are_relative_prime implies order i,p divides p -' 1 )
assume A1: ( p is prime & i,p are_relative_prime ) ; :: thesis: order i,p divides p -' 1
then A2: (i |^ (p -' 1)) mod p = 1 by Th38;
A3: p > 1 by A1, INT_2:def 5;
then p - 1 > 1 - 1 by XREAL_1:11;
then p -' 1 > 0 by XREAL_0:def 2;
hence order i,p divides p -' 1 by A1, A2, A3, Th52; :: thesis: verum