let n be Nat; :: thesis: ( n > 2 implies Lucas n = [\((1 / tau) * ((Lucas (n + 1)) + (1 / 2)))/] )
assume A1: n > 2 ; :: thesis: Lucas n = [\((1 / tau) * ((Lucas (n + 1)) + (1 / 2)))/]
then A2: n > 1 by XXREAL_0:2;
A3: sqrt 5 > 0 by SQUARE_1:25;
set tbn = tau_bar to_power n;
A4: (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 n is odd ) ;
suppose A5: n is even ; :: thesis: tau_bar to_power n <= 1 / (2 * (sqrt 5))
n >= 2 + 1 by A1, 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 A6: tau_bar to_power n <= tau_bar to_power 4 by Th11, A5, POLYFORM:6;
A7: tau_bar to_power (3 + 1) = (tau_bar to_power 3) * (tau_bar to_power 1) by Th2
.= (2 - (sqrt 5)) * tau_bar by Lm8
.= (((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 2
.= (7 - (3 * (sqrt 5))) / 2 ;
sqrt 5 <= sqrt ((16 / 7) ^2) by SQUARE_1:26;
then sqrt 5 <= 16 / 7 by SQUARE_1:def 2;
then 7 * (sqrt 5) <= (16 / 7) * 7 by XREAL_1:64;
then (7 * (sqrt 5)) - (3 * 5) <= 16 - (3 * 5) by XREAL_1:9;
then (7 * (sqrt 5)) - (3 * ((sqrt 5) ^2)) <= 1 by SQUARE_1:def 2;
then ((7 - (3 * (sqrt 5))) * (sqrt 5)) / (sqrt 5) <= 1 / (sqrt 5) by A3, XREAL_1:72;
then 7 - (3 * (sqrt 5)) <= 1 / (sqrt 5) by A3, XCMPLX_1:89;
then (7 - (3 * (sqrt 5))) / 2 <= (1 / (sqrt 5)) / 2 by XREAL_1:72;
then tau_bar to_power 4 <= 1 / (2 * (sqrt 5)) by A7, XCMPLX_1:78;
hence tau_bar to_power n <= 1 / (2 * (sqrt 5)) by A6, XXREAL_0:2; :: thesis: verum
end;
end;
end;
then (tau_bar to_power n) * (sqrt 5) <= (1 / (2 * (sqrt 5))) * (sqrt 5) by A3, XREAL_1:64;
then (tau_bar to_power n) * (sqrt 5) <= 1 / 2 by A3, XCMPLX_1:92;
then - ((tau_bar to_power n) * (sqrt 5)) >= - (1 / 2) by XREAL_1:24;
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:6;
then ((tau_bar * (tau_bar to_power n)) + (1 / 2)) / tau >= ((tau_bar to_power n) * tau) / tau by XREAL_1:72;
then ((tau_bar * (tau_bar to_power n)) + (1 / 2)) / tau >= tau_bar to_power n by XCMPLX_1:89;
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:6;
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:62;
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) ;
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 Th2;
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 Th2;
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) ;
then ((Lucas (n + 1)) + (1 / 2)) / tau >= (tau_bar to_power n) + (tau to_power n) by XCMPLX_1:89;
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:99; :: thesis: verum
end;
((1 / tau) * ((Lucas (n + 1)) + (1 / 2))) - 1 < Lucas n
proof
tau_bar to_power n > - (1 / 2) by Th14, A2;
then - (tau_bar to_power n) < - (- (1 / 2)) by XREAL_1:24;
then (- (tau_bar to_power n)) * (sqrt 5) < (1 / 2) * (sqrt 5) by A3, XREAL_1:68;
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:6;
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:9;
then ((((tau_bar to_power n) * tau_bar) + (1 / 2)) - tau) / tau < ((tau_bar to_power n) * tau) / tau by XREAL_1:74;
then ((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) - (tau / tau) < ((tau_bar to_power n) * tau) / tau by XCMPLX_1:124;
then ((((tau_bar to_power n) * tau_bar) / tau) + ((1 / 2) / tau)) - (tau / tau) < tau_bar to_power n by XCMPLX_1:89;
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:6;
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:74;
then (((((tau_bar to_power n) * tau_bar) + (1 / 2)) + ((tau to_power n) * tau)) / tau) - 1 < Lucas n by XCMPLX_1:63;
then (((((tau_bar to_power n) * (tau_bar to_power 1)) + (1 / 2)) + ((tau to_power n) * tau)) / tau) - 1 < Lucas n ;
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 ;
then ((((tau_bar to_power (n + 1)) + (1 / 2)) + ((tau to_power n) * (tau to_power 1))) / tau) - 1 < Lucas n by Th2;
then ((((tau_bar to_power (n + 1)) + (1 / 2)) + (tau to_power (n + 1))) / tau) - 1 < Lucas n by Th2;
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:99; :: thesis: verum
end;
hence Lucas n = [\((1 / tau) * ((Lucas (n + 1)) + (1 / 2)))/] by A4, INT_1:def 6; :: thesis: verum