let n be Nat; :: thesis: ( n >= 2 & n is odd implies Lucas (n + 1) = [\((tau * (Lucas n)) + 1)/] )
set tn = tau_bar to_power n;
assume A1: ( n >= 2 & n is odd ) ; :: thesis: Lucas (n + 1) = [\((tau * (Lucas n)) + 1)/]
A2: (tau * (Lucas n)) + 1 >= Lucas (n + 1)

proof

per cases ( n = 2 or n > 2 ) by A1, XXREAL_0:1;

suppose A3: n = 2 ; :: thesis: (tau * (Lucas n)) + 1 >= Lucas (n + 1)

sqrt 5 >= 1 by SQUARE_1:18, SQUARE_1:26;
then (sqrt 5) * 3 >= 1 * 3 by XREAL_1:64;
then 5 + ((sqrt 5) * 3) >= 3 + 5 by XREAL_1:6;
then (5 + ((sqrt 5) * 3)) / 2 >= 8 / 2 by XREAL_1:72;
hence (tau * (Lucas n)) + 1 >= Lucas (n + 1) by A3, FIB_NUM:def 1, FIB_NUM3:14, FIB_NUM3:15; :: thesis: verum

end;

suppose A4: n > 2 ; :: thesis: (tau * (Lucas n)) + 1 >= Lucas (n + 1)

A5: sqrt 5 > 0 by SQUARE_1:25;
( tau_bar to_power n >= - (1 / (sqrt 5)) & sqrt 5 > 0 ) by Th15, A4, SQUARE_1:25;
then (tau_bar to_power n) * (sqrt 5) >= (- (1 / (sqrt 5))) * (sqrt 5) by XREAL_1:64;
then (tau_bar to_power n) * (sqrt 5) >= (sqrt 5) * ((- 1) / (sqrt 5)) by XCMPLX_1:187;
then (tau_bar to_power n) * (sqrt 5) >= ((sqrt 5) * (- 1)) / (sqrt 5) by XCMPLX_1:74;
then (tau_bar to_power n) * (sqrt 5) >= ((sqrt 5) / (sqrt 5)) * (- 1) by XCMPLX_1:74;
then (tau_bar to_power n) * (sqrt 5) >= 1 * (- 1) by A5, XCMPLX_1:60;
then - ((tau_bar to_power n) * (sqrt 5)) <= - (- 1) by XREAL_1:24;
then ((tau_bar to_power n) * tau_bar) - ((tau_bar to_power n) * tau) <= 1 by FIB_NUM:def 1, FIB_NUM:def 2;
then ((tau_bar to_power n) * (tau_bar to_power 1)) - ((tau_bar to_power n) * tau) <= 1 ;
then (tau_bar to_power (n + 1)) - ((tau_bar to_power n) * tau) <= 1 by Th2;
then ((tau_bar to_power (n + 1)) - ((tau_bar to_power n) * tau)) + ((tau_bar to_power n) * tau) <= 1 + ((tau_bar to_power n) * tau) by XREAL_1:6;
then (((tau_bar to_power n) * tau) + 1) + (tau to_power (n + 1)) >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) by XREAL_1:6;
then (((tau_bar to_power n) * tau) + 1) + ((tau to_power n) * (tau to_power 1)) >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) by Th2;
then (((tau_bar to_power n) * tau) + 1) + ((tau to_power n) * tau) >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) ;
then (((tau_bar to_power n) + (tau to_power n)) * tau) + 1 >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) ;
then ((Lucas n) * tau) + 1 >= (tau_bar to_power (n + 1)) + (tau to_power (n + 1)) by FIB_NUM3:21;
hence (tau * (Lucas n)) + 1 >= Lucas (n + 1) by FIB_NUM3:21; :: thesis: verum

end;

end;

end;

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

proof

A6: Lucas (n + 1) = (tau to_power (n + 1)) + (tau_bar to_power (n + 1)) by FIB_NUM3:21;
A7: 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 ;
tau_bar to_power n < 0 by Th7, A1;
then tau * (tau_bar to_power n) < tau_bar * (tau_bar to_power n) by XREAL_1:69;
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 A6, A7, XREAL_1:6; :: thesis: verum

end;

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