let n be Nat; :: thesis: ( n >= 2 & n is even implies Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\] )
set tn = tau_bar to_power n;
assume A1: ( n >= 2 & n is even ) ; :: thesis: Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\]
A2: Lucas (n + 1) = (tau to_power (n + 1)) + (tau_bar to_power (n + 1)) by FIB_NUM3:21;
A3: tau * (Lucas n) = tau * ((tau to_power n) + (tau_bar to_power n)) by FIB_NUM3:21
.= (tau * (tau to_power n)) + (tau * (tau_bar to_power n))
.= ((tau to_power 1) * (tau to_power n)) + (tau * (tau_bar to_power n))
.= (tau to_power (n + 1)) + (tau * (tau_bar to_power n)) by Th2 ;
A4: (tau * (Lucas n)) - 1 <= Lucas (n + 1)

proof

(tau * (tau_bar to_power n)) - 1 <= tau_bar to_power (n + 1)

proof

A5: tau_bar to_power n > 0 by Th6, A1;
tau_bar to_power n <= 1 / (sqrt 5) by Th16, A1;
then 1 / (tau_bar to_power n) >= 1 / (1 / (sqrt 5)) by Th6, A1, XREAL_1:118;
then 1 / (tau_bar to_power n) >= sqrt 5 by XCMPLX_1:52;
then (1 / (tau_bar to_power n)) * 2 >= (sqrt 5) * 2 by XREAL_1:64;
then ((1 / (tau_bar to_power n)) * 2) + 1 >= (2 * (sqrt 5)) + 1 by XREAL_1:6;
then (((1 / (tau_bar to_power n)) * 2) + 1) - (sqrt 5) >= ((2 * (sqrt 5)) + 1) - (sqrt 5) by XREAL_1:13;
then (((1 / (tau_bar to_power n)) * 2) + (1 - (sqrt 5))) / 2 >= ((sqrt 5) + 1) / 2 by XREAL_1:72;
then ((1 / (tau_bar to_power n)) + tau_bar) * (tau_bar to_power n) >= tau * (tau_bar to_power n) by A5, FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1:64;
then ((1 / (tau_bar to_power n)) * (tau_bar to_power n)) + (tau_bar * (tau_bar to_power n)) >= tau * (tau_bar to_power n) ;
then ((1 / (tau_bar to_power n)) * (tau_bar to_power n)) + ((tau_bar to_power 1) * (tau_bar to_power n)) >= tau * (tau_bar to_power n) ;
then 1 + ((tau_bar to_power 1) * (tau_bar to_power n)) >= tau * (tau_bar to_power n) by A5, XCMPLX_1:87;
then 1 + (tau_bar to_power (n + 1)) >= tau * (tau_bar to_power n) by Th2;
then (1 + (tau_bar to_power (n + 1))) - 1 >= (tau * (tau_bar to_power n)) - 1 by XREAL_1:9;
hence (tau * (tau_bar to_power n)) - 1 <= tau_bar to_power (n + 1) ; :: thesis: verum

end;

then (tau to_power (n + 1)) + ((tau * (tau_bar to_power n)) - 1) <= (tau to_power (n + 1)) + (tau_bar to_power (n + 1)) by XREAL_1:6;
hence (tau * (Lucas n)) - 1 <= Lucas (n + 1) by A3, FIB_NUM3:21; :: thesis: verum

end;

((tau * (Lucas n)) - 1) + 1 > Lucas (n + 1)

proof

tau_bar to_power n = (- tau_bar) to_power n by A1, Th3;
then tau_bar to_power n > 0 by POWER:34;
then tau * (tau_bar to_power n) > tau_bar * (tau_bar to_power n) by XREAL_1:68;
then tau * (tau_bar to_power n) > (tau_bar to_power 1) * (tau_bar to_power n) ;
then tau * (tau_bar to_power n) > tau_bar to_power (n + 1) by Th2;
hence ((tau * (Lucas n)) - 1) + 1 > Lucas (n + 1) by A2, A3, XREAL_1:6; :: thesis: verum

end;

hence Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\] by A4, INT_1:def 7; :: thesis: verum