let n be Nat; :: thesis: ( n >= 2 implies Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] )
assume A1: n >= 2 ; :: thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]
A2: sqrt 5 > 0 by SQUARE_1:25;
set tn = tau to_power n;
set tb = tau_bar ;
set s5 = sqrt 5;
set tbn = tau_bar to_power n;
per cases ( n is even or n is odd ) ;
suppose A3: n is even ; :: thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]
then A4: tau_bar to_power n > 0 by Th6;
A5: (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1)
proof
tau_bar to_power n <= 1 / 2 by Th8, A1;
then 2 * (tau_bar to_power n) <= 2 * (1 / 2) by XREAL_1:64;
then (2 * (tau_bar to_power n)) / (tau_bar to_power n) <= 1 / (tau_bar to_power n) by A4, XREAL_1:72;
then 2 <= 1 / (tau_bar to_power n) by A4, XCMPLX_1:89;
then 2 * (sqrt 5) <= (1 / (tau_bar to_power n)) * (sqrt 5) by A2, XREAL_1:64;
then (sqrt 5) + (sqrt 5) <= (1 * (sqrt 5)) / (tau_bar to_power n) by XCMPLX_1:74;
then ((sqrt 5) + (sqrt 5)) - (sqrt 5) <= ((1 * (sqrt 5)) / (tau_bar to_power n)) - (sqrt 5) by XREAL_1:9;
then - (sqrt 5) >= - (((sqrt 5) / (tau_bar to_power n)) - (sqrt 5)) by XREAL_1:24;
then (- (sqrt 5)) + 1 >= ((- ((sqrt 5) / (tau_bar to_power n))) + (sqrt 5)) + 1 by XREAL_1:6;
then tau_bar >= (((sqrt 5) + 1) - ((sqrt 5) / (tau_bar to_power n))) / 2 by FIB_NUM:def 2, XREAL_1:72;
then tau_bar * (tau_bar to_power n) >= (tau - (((sqrt 5) / (tau_bar to_power n)) / 2)) * (tau_bar to_power n) by A4, FIB_NUM:def 1, XREAL_1:64;
then tau_bar * (tau_bar to_power n) >= (tau - (((sqrt 5) / 2) / (tau_bar to_power n))) * (tau_bar to_power n) by XCMPLX_1:48;
then tau_bar * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((((sqrt 5) / 2) / (tau_bar to_power n)) * (tau_bar to_power n)) ;
then tau_bar * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) by A4, XCMPLX_1:87;
then (tau_bar to_power 1) * (tau_bar to_power n) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) ;
then tau_bar to_power (n + 1) >= (tau * (tau_bar to_power n)) - ((sqrt 5) / 2) by Th2;
then - (tau_bar to_power (n + 1)) <= - ((tau * (tau_bar to_power n)) - ((sqrt 5) / 2)) by XREAL_1:24;
then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= ((- (tau * (tau_bar to_power n))) + ((sqrt 5) / 2)) + (tau to_power (n + 1)) by XREAL_1:6;
then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= ((tau to_power (n + 1)) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) ;
then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= (((tau to_power n) * (tau to_power 1)) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) by Th2;
then (- (tau_bar to_power (n + 1))) + (tau to_power (n + 1)) <= (((tau to_power n) * tau) - (tau * (tau_bar to_power n))) + ((sqrt 5) / 2) ;
then ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) + ((sqrt 5) / 2)) / (sqrt 5) by A2, XREAL_1:72;
then Fib (n + 1) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) + ((sqrt 5) / 2)) / (sqrt 5) by FIB_NUM:7;
then Fib (n + 1) <= ((tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5)) + (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:62;
then Fib (n + 1) <= (tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5))) + (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:74;
then Fib (n + 1) <= (tau * (Fib n)) + (((sqrt 5) / 2) / (sqrt 5)) by FIB_NUM:7;
then Fib (n + 1) <= (tau * (Fib n)) + (((sqrt 5) / (sqrt 5)) / 2) by XCMPLX_1:48;
then Fib (n + 1) <= (tau * (Fib n)) + (1 / 2) by A2, XCMPLX_1:60;
hence (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1) by FIB_NUM:def 1; :: thesis: verum
end;
((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1)
proof
Fib (n + 1) = [\((tau * (Fib n)) + 1)/] by A1, A3, Th22;
then A6: ((tau * (Fib n)) + 1) - 1 < Fib (n + 1) by INT_1:def 6;
((Fib n) + ((sqrt 5) * (Fib n))) + 1 <= ((Fib n) + ((sqrt 5) * (Fib n))) + 2 by XREAL_1:6;
then (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 <= (((Fib n) + ((sqrt 5) * (Fib n))) + 2) / 2 by XREAL_1:72;
then ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 <= ((tau * (Fib n)) + 1) - 1 by FIB_NUM:def 1, XREAL_1:9;
hence ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) by A6, XXREAL_0:2; :: thesis: verum
end;
hence Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] by A5, INT_1:def 6; :: thesis: verum
end;
suppose A7: n is odd ; :: thesis: Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/]
A8: (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1)
proof
Fib (n + 1) = [/((tau * (Fib n)) - 1)\] by A1, A7, Th23;
then A9: ((tau * (Fib n)) - 1) + 1 > Fib (n + 1) by INT_1:def 7;
1 + ((Fib n) + ((sqrt 5) * (Fib n))) > 0 + ((Fib n) + ((sqrt 5) * (Fib n))) by XREAL_1:6;
then (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 > ((Fib n) + ((sqrt 5) * (Fib n))) / 2 by XREAL_1:74;
hence (((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2 >= Fib (n + 1) by A9, FIB_NUM:def 1, XXREAL_0:2; :: thesis: verum
end;
((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1)
proof
n > 1 by A1, XXREAL_0:2;
then (2 * (sqrt 5)) * (tau_bar to_power n) > (2 * (sqrt 5)) * (- (1 / 2)) by A2, Th14, XREAL_1:68;
then - ((2 * (sqrt 5)) * (tau_bar to_power n)) < - ((2 * (sqrt 5)) * (- (1 / 2))) by XREAL_1:24;
then ((((((1 * (tau to_power n)) + ((sqrt 5) * (tau to_power n))) - ((2 * tau) * (tau to_power n))) + ((2 * tau_bar) * (tau_bar to_power n))) - ((sqrt 5) * (tau_bar to_power n))) - (1 * (tau_bar to_power n))) + ((2 * tau) * (tau to_power n)) < (sqrt 5) + ((2 * tau) * (tau to_power n)) by FIB_NUM:def 1, FIB_NUM:def 2, XREAL_1:6;
then (((((tau to_power n) + ((sqrt 5) * (tau to_power n))) + ((2 * tau_bar) * (tau_bar to_power n))) - ((sqrt 5) * (tau_bar to_power n))) - (tau_bar to_power n)) - ((2 * tau_bar) * (tau_bar to_power n)) < ((sqrt 5) + ((2 * tau) * (tau to_power n))) - ((2 * tau_bar) * (tau_bar to_power n)) by XREAL_1:9;
then ((1 + (sqrt 5)) * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) < (((sqrt 5) + ((2 * tau) * (tau to_power n))) - ((2 * tau_bar) * (tau_bar to_power n))) / (sqrt 5) by A2, XREAL_1:74;
then (1 + (sqrt 5)) * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) < (((sqrt 5) + (2 * (tau * (tau to_power n)))) - ((2 * tau_bar) * (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau * (tau to_power n)))) - ((2 * tau_bar) * (tau_bar to_power n))) / (sqrt 5) by FIB_NUM:7;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * ((tau to_power 1) * (tau to_power n)))) - ((2 * tau_bar) * (tau_bar to_power n))) / (sqrt 5) ;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * (tau_bar * (tau_bar to_power n)))) / (sqrt 5) by Th2;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * ((tau_bar to_power 1) * (tau_bar to_power n)))) / (sqrt 5) ;
then (1 + (sqrt 5)) * (Fib n) < (((sqrt 5) + (2 * (tau to_power (n + 1)))) - (2 * (tau_bar to_power (n + 1)))) / (sqrt 5) by Th2;
then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) + (2 * ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))))) / (sqrt 5) ;
then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + ((2 * ((tau to_power (n + 1)) - (tau_bar to_power (n + 1)))) / (sqrt 5)) by XCMPLX_1:62;
then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + (2 * (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5))) by XCMPLX_1:74;
then (1 + (sqrt 5)) * (Fib n) < ((sqrt 5) / (sqrt 5)) + (2 * (Fib (n + 1))) by FIB_NUM:7;
then (1 + (sqrt 5)) * (Fib n) < 1 + (2 * (Fib (n + 1))) by A2, XCMPLX_1:60;
then ((1 + (sqrt 5)) * (Fib n)) / 2 < (1 + (2 * (Fib (n + 1)))) / 2 by XREAL_1:74;
then (((1 + (sqrt 5)) * (Fib n)) / 2) - (1 / 2) < ((1 / 2) + (Fib (n + 1))) - (1 / 2) by XREAL_1:9;
hence ((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2) - 1 < Fib (n + 1) ; :: thesis: verum
end;
hence Fib (n + 1) = [\((((Fib n) + ((sqrt 5) * (Fib n))) + 1) / 2)/] by A8, INT_1:def 6; :: thesis: verum
end;
end;