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