theorem Th21: :: NAT_6:21

for n being 2 _greater Nat
for s being non trivial Divisor of n - 1 st s > sqrt n & ex a being Nat st
( a |^ (n - 1),1 are_congruent_mod n & ( for q being prime Divisor of s holds ((a |^ ((n - 1) / q)) - 1) gcd n = 1 ) ) holds
n is prime