A1: 1 - (sqrt 5) <> 0 by SQUARE_1:20, SQUARE_1:27;
- (1 / tau) = - (1 * (2 / (1 + (sqrt 5)))) by FIB_NUM:def 1, XCMPLX_1:57
.= - (1 * ((2 * (1 - (sqrt 5))) / ((1 + (sqrt 5)) * (1 - (sqrt 5))))) by A1, XCMPLX_1:91
.= - (1 * ((2 * (1 - (sqrt 5))) / (1 - ((sqrt 5) ^2))))
.= - (1 * ((2 * (1 - (sqrt 5))) / (1 - 5))) by SQUARE_1:def 2
.= (1 - (sqrt 5)) / 2 ;
hence - (1 / tau) = tau_bar by FIB_NUM:def 2; :: thesis: verum