let n be Nat; :: thesis: ( n <> 0 implies [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n) )
assume A1: n <> 0 ; :: thesis: [\((tau to_power (2 * n)) / (sqrt 5))/] = Fib (2 * n)
A2: ((tau to_power (2 * n)) / (sqrt 5)) - 1 < Fib (2 * n)

proof

A3: 2 to_power (2 * n) > 0 by POWER:34;
((1 - (sqrt 5)) to_power 2) to_power n < (2 to_power 2) to_power n by A1, Lm17, Lm19, POWER:37;
then ((1 - (sqrt 5)) to_power 2) to_power n < 2 to_power (2 * n) by POWER:33;
then (1 - (sqrt 5)) to_power (2 * n) < 2 to_power (2 * n) by NEWTON:9;
then ((1 - (sqrt 5)) to_power (2 * n)) / (2 to_power (2 * n)) < (2 to_power (2 * n)) / (2 to_power (2 * n)) by A3, XREAL_1:74;
then ((1 - (sqrt 5)) to_power (2 * n)) / (2 to_power (2 * n)) < 1 by A3, XCMPLX_1:60;
then tau_bar to_power (2 * n) < 1 by Th1, FIB_NUM:def 2;
then tau_bar to_power (2 * n) < sqrt 5 by Lm16, XXREAL_0:2;
then (tau_bar to_power (2 * n)) / (sqrt 5) < (sqrt 5) / (sqrt 5) by Lm18, XREAL_1:74;
then (tau_bar to_power (2 * n)) / (sqrt 5) < 1 by Lm18, XCMPLX_1:60;
then - ((tau_bar to_power (2 * n)) / (sqrt 5)) > - 1 by XREAL_1:24;
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:8;
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:120;
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:9
.= (tau_bar ^2) to_power n by POWER:46 ;
then tau_bar to_power (2 * n) > 0 by POWER:34;
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 Lm18, XREAL_1:8;
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:120;
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 A2, INT_1:def 6; :: thesis: verum