theorem Th17: :: FIB_NUM4:17

for n being Nat holds
( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 & ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 )