theorem Th25: :: NAT_4:25

for n, f, d, n1, a, q being Element of NAT st n - 1 = (q |^ n1) * d & q |^ n1 > d & d > 0 & q is prime & (a |^ (n -' 1)) mod n = 1 & ((a |^ ((n -' 1) div q)) -' 1) gcd n = 1 holds
n is prime