theorem Th18: :: NUMBER15:18

for p being Prime
for m, n being Nat st p mod 4 = 3 holds
( (divisors ((p |^ n),4,1)) \/ (divisors ((p |^ n),4,3)) = { k where k is Nat : k divides p |^ n } & ( n = 2 * m implies ( card (divisors ((p |^ n),4,1)) = m + 1 & card (divisors ((p |^ n),4,3)) = m ) ) & ( n = (2 * m) + 1 implies ( card (divisors ((p |^ n),4,1)) = m + 1 & card (divisors ((p |^ n),4,3)) = m + 1 ) ) )