1 < sqrt 5
by SQUARE_1:18, SQUARE_1:27;
then A1:
1 - (sqrt 5) < (sqrt 5) - (sqrt 5)
by XREAL_1:9;
thus tau_bar to_power 3 =
((1 - (sqrt 5)) / 2) to_power (2 + 1)
by FIB_NUM:def 2
.=
(((1 - (sqrt 5)) / 2) to_power 2) * (((1 - (sqrt 5)) / 2) to_power 1)
by Th2, A1
.=
(((1 - (sqrt 5)) / 2) to_power 2) * ((1 - (sqrt 5)) / 2)
.=
(((1 - (sqrt 5)) / 2) ^2) * ((1 - (sqrt 5)) / 2)
by POWER:46
.=
(((1 - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) * (1 - (sqrt 5))) / 8
.=
(((1 - (2 * (sqrt 5))) + 5) * (1 - (sqrt 5))) / 8
by SQUARE_1:def 2
.=
((6 - (8 * (sqrt 5))) + (2 * ((sqrt 5) ^2))) / 8
.=
((6 - (8 * (sqrt 5))) + (2 * 5)) / 8
by SQUARE_1:def 2
.=
2 - (sqrt 5)
; verum