A1: 1 - (sqrt 5) <> 0 by SQUARE_1:85, SQUARE_1:95;
- (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:92
.= - (1 * ((2 * (1 - (sqrt 5))) / (1 - ((sqrt 5) ^2 ))))
.= - (1 * ((2 * (1 - (sqrt 5))) / (1 - 5))) by SQUARE_1:def 4
.= (1 - (sqrt 5)) / 2 ;
hence - (1 / tau ) = tau_bar by FIB_NUM:def 2; :: thesis: verum