theorem Th27: :: NUMBER15:27

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