let n be natural number ; :: thesis: ( n > 2 implies Lucas n = [\((1 / tau ) * ((Lucas (n + 1)) + (1 / 2)))/] )
assume A0: n > 2 ; :: thesis: Lucas n = [\((1 / tau ) * ((Lucas (n + 1)) + (1 / 2)))/]
then B0: n > 1 by XXREAL_0:2;
B2: sqrt 5 > 0 by SQUARE_1:93;
set tbn = tau_bar to_power n;
A1: (1 / tau ) * ((Lucas (n + 1)) + (1 / 2)) >= Lucas n

proof

tau_bar to_power n <= 1 / (2 * (sqrt 5))

proof

per cases ( n is even or not n is even ) ;

suppose B4: n is even ; :: thesis: tau_bar to_power n <= 1 / (2 * (sqrt 5))

n >= 2 + 1 by A0, NAT_1:13;
then ( n = 3 or n > 3 ) by XXREAL_0:1;
then ( n = 3 or n >= 3 + 1 ) by NAT_1:8;
then B6: tau_bar to_power n <= tau_bar to_power 4 by hopp10, B4, POLYFORM:6;
B7: tau_bar to_power (3 + 1) = (tau_bar to_power 3) * (tau_bar to_power 1) by JakPower32
.= (2 - (sqrt 5)) * tau_bar by beta3, POWER:30
.= (((2 - (2 * (sqrt 5))) - (sqrt 5)) + ((sqrt 5) ^2 )) / 2 by FIB_NUM:def 2
.= ((2 - (3 * (sqrt 5))) + 5) / 2 by SQUARE_1:def 4
.= (7 - (3 * (sqrt 5))) / 2 ;
sqrt 5 <= sqrt ((16 / 7) ^2 ) by SQUARE_1:94;
then sqrt 5 <= 16 / 7 by SQUARE_1:def 4;
then 7 * (sqrt 5) <= (16 / 7) * 7 by XREAL_1:66;
then (7 * (sqrt 5)) - (3 * 5) <= 16 - (3 * 5) by XREAL_1:11;
then (7 * (sqrt 5)) - (3 * ((sqrt 5) ^2 )) <= 1 by SQUARE_1:def 4;
then ((7 - (3 * (sqrt 5))) * (sqrt 5)) / (sqrt 5) <= 1 / (sqrt 5) by B2, XREAL_1:74;
then 7 - (3 * (sqrt 5)) <= 1 / (sqrt 5) by B2, XCMPLX_1:90;
then (7 - (3 * (sqrt 5))) / 2 <= (1 / (sqrt 5)) / 2 by XREAL_1:74;
then tau_bar to_power 4 <= 1 / (2 * (sqrt 5)) by B7, XCMPLX_1:79;
hence tau_bar to_power n <= 1 / (2 * (sqrt 5)) by B6, XXREAL_0:2; :: thesis: verum

end;

suppose not n is even ; :: thesis: tau_bar to_power n <= 1 / (2 * (sqrt 5))

then tau_bar to_power n < 0 by pom2;
hence tau_bar to_power n <= 1 / (2 * (sqrt 5)) by B2; :: thesis: verum

end;

end;

end;

then (tau_bar to_power n) * (sqrt 5) <= (1 / (2 * (sqrt 5))) * (sqrt 5) by B2, XREAL_1:66;
then (tau_bar to_power n) * (sqrt 5) <= 1 / 2 by B2, XCMPLX_1:93;
then - ((tau_bar to_power n) * (sqrt 5)) >= - (1 / 2) by XREAL_1:26;
then ((tau_bar * (tau_bar to_power n)) - (tau * (tau_bar to_power n))) + ((1 / 2) + (tau * (tau_bar to_power n))) >= (- (1 / 2)) + ((1 / 2) + (tau * (tau_bar to_power n))) by FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1:8;
then ((tau_bar * (tau_bar to_power n)) + (1 / 2)) / tau >= ((tau_bar to_power n) * tau ) / tau by XREAL_1:74;
then ((tau_bar * (tau_bar to_power n)) + (1 / 2)) / tau >= tau_bar to_power n by XCMPLX_1:90;
then (((tau_bar * (tau_bar to_power n)) + (1 / 2)) / tau ) + ((tau to_power (n + 1)) / tau ) >= (tau_bar to_power n) + ((tau to_power (n + 1)) / tau ) by XREAL_1:8;
then (((tau_bar * (tau_bar to_power n)) + (1 / 2)) + (tau to_power (n + 1))) / tau >= (tau_bar to_power n) + ((tau to_power (n + 1)) / tau ) by XCMPLX_1:63;
then ((((tau_bar to_power 1) * (tau_bar to_power n)) + (1 / 2)) + (tau to_power (n + 1))) / tau >= (tau_bar to_power n) + ((tau to_power (n + 1)) / tau ) by POWER:30;
then ((((tau_bar to_power 1) * (tau_bar to_power n)) + (tau to_power (n + 1))) + (1 / 2)) / tau >= (tau_bar to_power n) + (((tau to_power n) * (tau to_power 1)) / tau ) by JakPower32;
then (((tau_bar to_power (1 + n)) + (tau to_power (n + 1))) + (1 / 2)) / tau >= (tau_bar to_power n) + (((tau to_power n) * (tau to_power 1)) / tau ) by JakPower32;
then ((Lucas (n + 1)) + (1 / 2)) / tau >= (tau_bar to_power n) + (((tau to_power n) * (tau to_power 1)) / tau ) by FIB_NUM3:21;
then ((Lucas (n + 1)) + (1 / 2)) / tau >= (tau_bar to_power n) + (((tau to_power n) * tau ) / tau ) by POWER:30;
then ((Lucas (n + 1)) + (1 / 2)) / tau >= (tau_bar to_power n) + (tau to_power n) by XCMPLX_1:90;
then ((Lucas (n + 1)) + (1 / 2)) / tau >= Lucas n by FIB_NUM3:21;
hence (1 / tau ) * ((Lucas (n + 1)) + (1 / 2)) >= Lucas n by XCMPLX_1:100; :: thesis: verum

end;

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

proof

tau_bar to_power n > - (1 / 2) by hop9, B0;
then - (tau_bar to_power n) < - (- (1 / 2)) by XREAL_1:26;
then (- (tau_bar to_power n)) * (sqrt 5) < (1 / 2) * (sqrt 5) by B2, XREAL_1:70;
then (((tau_bar to_power n) * tau_bar ) - ((tau_bar to_power n) * tau )) + (((tau_bar to_power n) * tau ) + (1 / 2)) < (tau - (1 / 2)) + (((tau_bar to_power n) * tau ) + (1 / 2)) by FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1:8;
then (((tau_bar to_power n) * tau_bar ) + (1 / 2)) - tau < (((tau - (1 / 2)) + ((tau_bar to_power n) * tau )) + (1 / 2)) - tau by XREAL_1:11;
then ((((tau_bar to_power n) * tau_bar ) + (1 / 2)) - tau ) / tau < ((tau_bar to_power n) * tau ) / tau by XREAL_1:76;
then ((((tau_bar to_power n) * tau_bar ) / tau ) + ((1 / 2) / tau )) - (tau / tau ) < ((tau_bar to_power n) * tau ) / tau by XCMPLX_1:125;
then ((((tau_bar to_power n) * tau_bar ) / tau ) + ((1 / 2) / tau )) - (tau / tau ) < tau_bar to_power n by XCMPLX_1:90;
then ((((tau_bar to_power n) * tau_bar ) / tau ) + ((1 / 2) / tau )) - 1 < tau_bar to_power n by XCMPLX_1:60;
then (((((tau_bar to_power n) * tau_bar ) / tau ) + ((1 / 2) / tau )) - 1) + (tau to_power n) < (tau_bar to_power n) + (tau to_power n) by XREAL_1:8;
then (((((tau_bar to_power n) * tau_bar ) / tau ) + ((1 / 2) / tau )) + ((tau to_power n) * 1)) - 1 < Lucas n by FIB_NUM3:21;
then (((((tau_bar to_power n) * tau_bar ) / tau ) + ((1 / 2) / tau )) + ((tau to_power n) * (tau / tau ))) - 1 < Lucas n by XCMPLX_1:60;
then (((((tau_bar to_power n) * tau_bar ) / tau ) + ((1 / 2) / tau )) + (((tau to_power n) * tau ) / tau )) - 1 < Lucas n by XCMPLX_1:75;
then (((((tau_bar to_power n) * tau_bar ) + (1 / 2)) + ((tau to_power n) * tau )) / tau ) - 1 < Lucas n by XCMPLX_1:64;
then (((((tau_bar to_power n) * (tau_bar to_power 1)) + (1 / 2)) + ((tau to_power n) * tau )) / tau ) - 1 < Lucas n by POWER:30;
then (((((tau_bar to_power n) * (tau_bar to_power 1)) + (1 / 2)) + ((tau to_power n) * (tau to_power 1))) / tau ) - 1 < Lucas n by POWER:30;
then ((((tau_bar to_power (n + 1)) + (1 / 2)) + ((tau to_power n) * (tau to_power 1))) / tau ) - 1 < Lucas n by JakPower32;
then ((((tau_bar to_power (n + 1)) + (1 / 2)) + (tau to_power (n + 1))) / tau ) - 1 < Lucas n by JakPower32;
then ((((tau_bar to_power (n + 1)) + (tau to_power (n + 1))) + (1 / 2)) / tau ) - 1 < Lucas n ;
then (((Lucas (n + 1)) + (1 / 2)) / tau ) - 1 < Lucas n by FIB_NUM3:21;
hence ((1 / tau ) * ((Lucas (n + 1)) + (1 / 2))) - 1 < Lucas n by XCMPLX_1:100; :: thesis: verum

end;

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