let n be natural number ; :: thesis: ( n <> 0 implies [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n) )
assume a0: n <> 0 ; :: thesis: [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n)
A3: ((tau to_power (2 * n)) / (sqrt 5)) - 1 < Fib (2 * n)

proof

d2: 2 to_power (2 * n) > 0 by POWER:39;
((1 - (sqrt 5)) to_power 2) to_power n < (2 to_power 2) to_power n by a0, d1, xx, POWER:42;
then ((1 - (sqrt 5)) to_power 2) to_power n < 2 to_power (2 * n) by POWER:38;
then (1 - (sqrt 5)) to_power (2 * n) < 2 to_power (2 * n) by NEWTON:14;
then ((1 - (sqrt 5)) to_power (2 * n)) / (2 to_power (2 * n)) < (2 to_power (2 * n)) / (2 to_power (2 * n)) by d2, XREAL_1:76;
then ((1 - (sqrt 5)) to_power (2 * n)) / (2 to_power (2 * n)) < 1 by d2, XCMPLX_1:60;
then tau_bar to_power (2 * n) < 1 by JakPower36, FIB_NUM:def 2;
then tau_bar to_power (2 * n) < sqrt 5 by d0, XXREAL_0:2;
then (tau_bar to_power (2 * n)) / (sqrt 5) < (sqrt 5) / (sqrt 5) by d3, XREAL_1:76;
then (tau_bar to_power (2 * n)) / (sqrt 5) < 1 by d3, XCMPLX_1:60;
then - ((tau_bar to_power (2 * n)) / (sqrt 5)) > - 1 by XREAL_1:26;
then (- ((tau_bar to_power (2 * n)) / (sqrt 5))) + ((tau to_power (2 * n)) / (sqrt 5)) > (- 1) + ((tau to_power (2 * n)) / (sqrt 5)) by XREAL_1:10;
then ((tau to_power (2 * n)) / (sqrt 5)) - ((tau_bar to_power (2 * n)) / (sqrt 5)) > (- 1) + ((tau to_power (2 * n)) / (sqrt 5)) ;
then ((tau to_power (2 * n)) - (tau_bar to_power (2 * n))) / (sqrt 5) > (- 1) + ((tau to_power (2 * n)) / (sqrt 5)) by XCMPLX_1:121;
hence ((tau to_power (2 * n)) / (sqrt 5)) - 1 < Fib (2 * n) by FIB_NUM:7; :: thesis: verum

end;

tau_bar to_power (2 * n) = (tau_bar to_power 2) |^ n by NEWTON:14
.= (tau_bar ^2) to_power n by POWER:53 ;
then tau_bar to_power (2 * n) > 0 by POWER:39;
then (- ((tau_bar to_power (2 * n)) / (sqrt 5))) + ((tau to_power (2 * n)) / (sqrt 5)) < 0 + ((tau to_power (2 * n)) / (sqrt 5)) by d3, XREAL_1:10;
then ((tau to_power (2 * n)) / (sqrt 5)) - ((tau_bar to_power (2 * n)) / (sqrt 5)) < (tau to_power (2 * n)) / (sqrt 5) ;
then ((tau to_power (2 * n)) - (tau_bar to_power (2 * n))) / (sqrt 5) < (tau to_power (2 * n)) / (sqrt 5) by XCMPLX_1:121;
then Fib (2 * n) <= (tau to_power (2 * n)) / (sqrt 5) by FIB_NUM:7;
hence [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n) by A3, INT_1:def 4; :: thesis: verum