theorem OnlyOddPrimeX: :: NUMBER18:39

for m, n being Nat st PrimeDivisors n = {m} holds
( m |-count n >= 1 & n = m |^ (m |-count n) )