let p, i, n be Nat; :: thesis: ( p > 1 & i,p are_relative_prime & order i,p divides n implies (i |^ n) mod p = 1 )
assume A1: ( p > 1 & i,p are_relative_prime & order i,p divides n ) ; :: thesis: (i |^ n) mod p = 1
then consider t being Nat such that
A2: n = (order i,p) * t by NAT_D:def 3;
reconsider t = t as Element of NAT by ORDINAL1:def 13;
(i |^ n) mod p = ((i |^ (order i,p)) |^ t) mod p by A2, NEWTON:14
.= (((i |^ (order i,p)) mod p) |^ t) mod p by Th12
.= (1 |^ t) mod p by A1, Def2
.= 1 mod p by NEWTON:15
.= 1 by A1, NAT_D:24 ;
hence (i |^ n) mod p = 1 ; :: thesis: verum