let n be Nat; :: thesis: ( n >= 2 & n is even implies Fib (n + 1) = [\((tau * (Fib n)) + 1)/] )
assume A1: ( n >= 2 & n is even ) ; :: thesis: Fib (n + 1) = [\((tau * (Fib n)) + 1)/]
set t = tau ;
set tb = tau_bar ;
A2: sqrt 5 > 0 by SQUARE_1:17, SQUARE_1:27;
A3: tau * tau_bar = ((1 ^2) - ((sqrt 5) ^2)) / 4 by FIB_NUM:def 1, FIB_NUM:def 2
.= (1 - 5) / 4 by SQUARE_1:def 2
.= - 1 ;
tau_bar to_power n = (- tau_bar) to_power n by A1, Th3;
then A4: tau_bar to_power n > 0 by POWER:34;
A5: (tau_bar to_power 2) + 1 = (tau_bar ^2) + 1 by POWER:46
.= ((((1 ^2) - ((2 * 1) * (sqrt 5))) + ((sqrt 5) ^2)) / 4) + 1 by FIB_NUM:def 2
.= (((1 - (2 * (sqrt 5))) + 5) / 4) + 1 by SQUARE_1:def 2
.= (5 - (sqrt 5)) / 2
.= (((sqrt 5) ^2) - (sqrt 5)) / 2 by SQUARE_1:def 2
.= - ((sqrt 5) * tau_bar) by FIB_NUM:def 2 ;
tau * (Fib n) = tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) by FIB_NUM:7
.= (tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74
.= ((tau * (tau to_power n)) - (tau * (tau_bar to_power n))) / (sqrt 5)
.= (((tau to_power 1) * (tau to_power n)) - (tau * (tau_bar to_power n))) / (sqrt 5)
.= ((tau to_power (n + 1)) - (tau * (tau_bar to_power ((n - 1) + 1)))) / (sqrt 5) by POWER:27
.= ((tau to_power (n + 1)) - (tau * ((tau_bar to_power (n - 1)) * (tau_bar to_power 1)))) / (sqrt 5) by Th2
.= ((tau to_power (n + 1)) - (tau * ((tau_bar to_power (n - 1)) * tau_bar))) / (sqrt 5)
.= ((tau to_power (n + 1)) - ((tau * tau_bar) * (tau_bar to_power (n - 1)))) / (sqrt 5)
.= ((((tau to_power (n + 1)) - ((- 1) * (tau_bar to_power (n - 1)))) + (tau_bar to_power (n - 1))) - (tau_bar to_power (n - 1))) / (sqrt 5) by A3
.= (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) + ((tau_bar to_power (n - 1)) + (tau_bar to_power (n + 1)))) / (sqrt 5)
.= (((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5)) + (((tau_bar to_power (n - 1)) + (tau_bar to_power ((n - 1) + 2))) / (sqrt 5)) by XCMPLX_1:62
.= (Fib (n + 1)) + (((tau_bar to_power (n - 1)) + (tau_bar to_power ((n - 1) + 2))) / (sqrt 5)) by FIB_NUM:7
.= (Fib (n + 1)) + ((((tau_bar to_power (n - 1)) * 1) + ((tau_bar to_power (n - 1)) * (tau_bar to_power 2))) / (sqrt 5)) by Th2
.= (Fib (n + 1)) + (((tau_bar to_power (n - 1)) * (1 + (tau_bar to_power 2))) / (sqrt 5))
.= (Fib (n + 1)) + (((tau_bar to_power (n - 1)) * (- ((sqrt 5) * tau_bar))) / (sqrt 5)) by A5
.= (Fib (n + 1)) + (((((- 1) * (tau_bar to_power (n - 1))) * tau_bar) * (sqrt 5)) / (sqrt 5))
.= (Fib (n + 1)) + (((- 1) * (tau_bar to_power (n - 1))) * tau_bar) by A2, XCMPLX_1:89
.= (Fib (n + 1)) - ((tau_bar to_power (n - 1)) * tau_bar)
.= (Fib (n + 1)) - ((tau_bar to_power (n - 1)) * (tau_bar to_power 1))
.= (Fib (n + 1)) - (tau_bar to_power ((n - 1) + 1)) by Th2
.= (Fib (n + 1)) - (tau_bar to_power n) ;
then A6: Fib (n + 1) = ((tau * (Fib n)) + 1) - (1 - (tau_bar to_power n)) ;
tau_bar to_power n < 1 by Th8, A1, XXREAL_0:2;
then - (tau_bar to_power n) > - 1 by XREAL_1:24;
then (- (tau_bar to_power n)) + 1 > (- 1) + 1 by XREAL_1:8;
then A7: Fib (n + 1) < (tau * (Fib n)) + 1 by A6, XREAL_1:44;
(tau * (Fib n)) + 1 < (Fib (n + 1)) + 1

proof

A8: tau * (Fib n) = tau * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) by FIB_NUM:7
.= (tau * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74
.= ((tau * (tau to_power n)) - (tau * (tau_bar to_power n))) / (sqrt 5)
.= (((tau to_power 1) * (tau to_power n)) - (tau * (tau_bar to_power n))) / (sqrt 5)
.= ((tau to_power (n + 1)) - (tau * (tau_bar to_power n))) / (sqrt 5) by POWER:27
.= ((tau to_power (n + 1)) / (sqrt 5)) - ((tau * (tau_bar to_power n)) / (sqrt 5)) by XCMPLX_1:120 ;
A9: Fib (n + 1) = ((tau to_power (n + 1)) - (tau_bar to_power (n + 1))) / (sqrt 5) by FIB_NUM:7
.= ((tau to_power (n + 1)) / (sqrt 5)) - ((tau_bar to_power (n + 1)) / (sqrt 5)) by XCMPLX_1:120 ;
(tau_bar to_power n) * tau > (tau_bar to_power n) * tau_bar by A4, XREAL_1:68;
then (tau_bar to_power n) * tau > (tau_bar to_power n) * (tau_bar to_power 1) ;
then (tau * (tau_bar to_power n)) / (sqrt 5) > ((tau_bar to_power n) * (tau_bar to_power 1)) / (sqrt 5) by A2, XREAL_1:74;
then (tau * (tau_bar to_power n)) / (sqrt 5) > (tau_bar to_power (n + 1)) / (sqrt 5) by Th2;
then - ((tau * (tau_bar to_power n)) / (sqrt 5)) < - ((tau_bar to_power (n + 1)) / (sqrt 5)) by XREAL_1:24;
then (- ((tau * (tau_bar to_power n)) / (sqrt 5))) + ((tau to_power (n + 1)) / (sqrt 5)) < (- ((tau_bar to_power (n + 1)) / (sqrt 5))) + ((tau to_power (n + 1)) / (sqrt 5)) by XREAL_1:8;
hence (tau * (Fib n)) + 1 < (Fib (n + 1)) + 1 by A8, A9, XREAL_1:8; :: thesis: verum

end;

then ((tau * (Fib n)) + 1) - 1 < ((Fib (n + 1)) + 1) - 1 by XREAL_1:9;
hence Fib (n + 1) = [\((tau * (Fib n)) + 1)/] by A7, INT_1:def 6; :: thesis: verum