theorem Th35: :: PEPIN:35

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