let n be Nat; :: thesis: ( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 & ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 )
set b = (1 - (sqrt 5)) / 2;
A1: |.((1 - (sqrt 5)) / 2).| = - ((1 - (sqrt 5)) / 2) by ABSVALUE:def 1, FIB_NUM:def 2;
A2: (|.((1 - (sqrt 5)) / 2).| to_power n) * (1 / (sqrt 5)) < 1 / 2 by Lm11, FIB_NUM:def 2;
( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 )

proof

per cases ( n is even or n is odd ) ;

suppose n is even ; :: thesis: ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 )

then |.((1 - (sqrt 5)) / 2).| to_power n = ((1 - (sqrt 5)) / 2) to_power n by Th3, A1, FIB_NUM:def 2;
then ( (((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5)) > 0 & (((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5)) < 1 / 2 ) by Lm10, Lm11, FIB_NUM:def 2;
then ( (((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5)) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < (1 / 2) + (1 / 2) ) by XREAL_1:8;
hence ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 ) ; :: thesis: verum

end;

suppose n is odd ; :: thesis: ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 )

then |.((1 - (sqrt 5)) / 2).| to_power n = - (((1 - (sqrt 5)) / 2) to_power n) by Th4, A1, FIB_NUM:def 2;
then ( (- (((1 - (sqrt 5)) / 2) to_power n)) * (1 / (sqrt 5)) > 0 & - ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) < 1 / 2 ) by Lm10, A2, FIB_NUM:def 2;
then ( - ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) > 0 & - ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) < 1 / 2 ) by XCMPLX_1:99;
then ( (((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5) < 0 & - (- ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5))) > - (1 / 2) ) by XREAL_1:24;
then ( ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) + (1 / 2) < 0 + (1 / 2) & ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) + (1 / 2) > (- (1 / 2)) + (1 / 2) ) by XREAL_1:8;
then ( ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) + (1 / 2) < 1 & ((((1 - (sqrt 5)) / 2) to_power n) / (sqrt 5)) + (1 / 2) > 0 ) by XXREAL_0:2;
hence ( ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) > 0 & ((((1 - (sqrt 5)) / 2) to_power n) * (1 / (sqrt 5))) + (1 / 2) < 1 ) by XCMPLX_1:99; :: thesis: verum

end;

end;

end;

hence ( ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) > 0 & ((tau_bar to_power n) / (sqrt 5)) + (1 / 2) < 1 ) by FIB_NUM:def 2, XCMPLX_1:99; :: thesis: verum