[\(((tau to_power 5) / (sqrt 5)) + (1 / 2))/] = 5
by FIB_NUM4:18, LFIB5;
then
5 - (1 / 2) <= (((tau to_power 5) / (sqrt 5)) + (1 / 2)) - (1 / 2)
by XREAL_1:9, INT_1:def 6;
then
(9 / 2) * (sqrt 5) <= ((tau to_power 5) / (sqrt 5)) * (sqrt 5)
by XREAL_1:64;
then
(9 / 2) * (sqrt 5) <= (tau to_power 5) / ((sqrt 5) / (sqrt 5))
by XCMPLX_1:81;
then WEQ:
(9 / 2) * (sqrt 5) <= (tau to_power 5) / 1
by XCMPLX_1:60;
((9 / 2) * (sqrt 5)) - 10 =
(((9 * (sqrt 5)) - 20) / 2) / (((9 * (sqrt 5)) + 20) / ((9 * (sqrt 5)) + 20))
by XCMPLX_1:51
.=
(((9 * (sqrt 5)) - 20) / (((9 * (sqrt 5)) + 20) / ((9 * (sqrt 5)) + 20))) / 2
by XCMPLX_1:48
.=
((((9 * (sqrt 5)) - 20) * ((9 * (sqrt 5)) + 20)) / ((9 * (sqrt 5)) + 20)) / 2
by XCMPLX_1:77
.=
(((81 * ((sqrt 5) ^2)) - 400) / ((9 * (sqrt 5)) + 20)) / 2
.=
(((81 * 5) - 400) / ((9 * (sqrt 5)) + 20)) / 2
by SQUARE_1:def 2
.=
(5 / ((9 * (sqrt 5)) + 20)) / 2
;
then
10 < (((9 / 2) * (sqrt 5)) - 10) + 10
by XREAL_1:29;
then
10 < tau to_power 5
by WEQ, XXREAL_0:2;
then
log (tau,10) < log (tau,(tau to_power 5))
by POWER:57, THTU;
then
log (tau,10) < 5 * (log (tau,tau))
by POWER:55, THTU;
then
log (tau,10) < 5 * 1
by POWER:52, THTU;
hence
log (tau,10) < 5
; verum