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