theorem Th25: :: NUMBER15:25

for n being Nat holds divisors ((3 |^ ((2 * n) + 1)),4,1) = { (3 |^ m) where m is Nat : ( m is even & m <= (2 * n) + 1 ) }