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