let i, n be Nat; :: thesis: ( n > 1 & i,n are_coprime implies order (i,n) divides Euler n )
assume A1: ( n > 1 & i,n are_coprime ) ; :: thesis: order (i,n) divides Euler n
(i |^ (Euler n)) mod n = 1 by Th5, A1, EULER_2:18;
hence order (i,n) divides Euler n by A1, PEPIN:47; :: thesis: verum