theorem Th48: :: PEPIN:48

for i, n, p being Nat st p > 1 & i,p are_coprime & order (i,p) divides n holds
(i |^ n) mod p = 1