let n be natural number ; :: thesis: ( n >= 2 & n is even implies Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\] )
set tn = tau_bar to_power n;
assume A0: ( n >= 2 & n is even ) ; :: thesis: Lucas (n + 1) = [/((tau * (Lucas n)) - 1)\]
A1: Lucas (n + 1) = (tau to_power (n + 1)) + (tau_bar to_power (n + 1)) by FIB_NUM3:21;
A2: 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)) by POWER:30
.= (tau to_power (n + 1)) + (tau * (tau_bar to_power n)) by JakPower32 ;
A3: (tau * (Lucas n)) - 1 <= Lucas (n + 1)

proof

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

proof

e1: tau_bar to_power n > 0 by pom1, A0;
tau_bar to_power n <= 1 / (sqrt 5) by mag2, A0;
then 1 / (tau_bar to_power n) >= 1 / (1 / (sqrt 5)) by pom1, A0, XREAL_1:120;
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:66;
then ((1 / (tau_bar to_power n)) * 2) + 1 >= (2 * (sqrt 5)) + 1 by XREAL_1:8;
then (((1 / (tau_bar to_power n)) * 2) + 1) - (sqrt 5) >= ((2 * (sqrt 5)) + 1) - (sqrt 5) by XREAL_1:15;
then (((1 / (tau_bar to_power n)) * 2) + (1 - (sqrt 5))) / 2 >= ((sqrt 5) + 1) / 2 by XREAL_1:74;
then ((1 / (tau_bar to_power n)) + tau_bar) * (tau_bar to_power n) >= tau * (tau_bar to_power n) by e1, FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1:66;
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) by POWER:30;
then 1 + ((tau_bar to_power 1) * (tau_bar to_power n)) >= tau * (tau_bar to_power n) by e1, XCMPLX_1:88;
then 1 + (tau_bar to_power (n + 1)) >= tau * (tau_bar to_power n) by JakPower32;
then (1 + (tau_bar to_power (n + 1))) - 1 >= (tau * (tau_bar to_power n)) - 1 by XREAL_1:11;
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:8;
hence (tau * (Lucas n)) - 1 <= Lucas (n + 1) by A2, 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 A0, pomoc1;
then tau_bar to_power n > 0 by POWER:39;
then tau * (tau_bar to_power n) > tau_bar * (tau_bar to_power n) by XREAL_1:70;
then tau * (tau_bar to_power n) > (tau_bar to_power 1) * (tau_bar to_power n) by POWER:30;
then tau * (tau_bar to_power n) > tau_bar to_power (n + 1) by JakPower32;
hence ((tau * (Lucas n)) - 1) + 1 > Lucas (n + 1) by A1, A2, XREAL_1:8; :: thesis: verum

end;

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