A1: 1 - (sqrt 5) <> 0 by SQUARE_1:20, SQUARE_1:27;
(- tau) to_power (- 1) = (((- 1) - (sqrt 5)) / 2) #Z (- 1) by FIB_NUM:def 1, POWER:def 2
.= 1 / ((((- 1) - (sqrt 5)) / 2) #Z 1) by PREPOWER:41
.= 1 / (((- 1) - (sqrt 5)) / 2) by PREPOWER:35
.= 2 / (- (1 + (sqrt 5))) by XCMPLX_1:57
.= - (2 / (1 + (sqrt 5))) by XCMPLX_1:188
.= (- 2) / (1 + (sqrt 5)) by XCMPLX_1:187
.= ((- 2) * (1 - (sqrt 5))) / ((1 + (sqrt 5)) * (1 - (sqrt 5))) by A1, XCMPLX_1:91
.= ((- 2) * (1 - (sqrt 5))) / ((1 ^2) - ((sqrt 5) ^2))
.= ((- 2) * (1 - (sqrt 5))) / (1 - 5) by SQUARE_1:def 2
.= tau_bar by FIB_NUM:def 2 ;
hence tau_bar = (- tau) to_power (- 1) ; :: thesis: verum