let n be natural number ; :: thesis: ( n >= 2 & n is even implies Fib (n + 1) = [\((tau * (Fib n)) + 1)/] )
assume A0: ( n >= 2 & n is even ) ; :: thesis: Fib (n + 1) = [\((tau * (Fib n)) + 1)/]
set t = tau ;
set tb = tau_bar ;
B0: sqrt 5 > 0 by SQUARE_1:82, SQUARE_1:95;
B2: 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 4
.= - 1 ;
tau_bar to_power n = (- tau_bar) to_power n by A0, pomoc1;
then H1: tau_bar to_power n > 0 by POWER:39;
B3: (tau_bar to_power 2) + 1 = (tau_bar ^2) + 1 by POWER:53
.= ((((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 4
.= (5 - (sqrt 5)) / 2
.= (((sqrt 5) ^2) - (sqrt 5)) / 2 by SQUARE_1:def 4
.= - ((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:75
.= ((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) by POWER:30
.= ((tau to_power (n + 1)) - (tau * (tau_bar to_power ((n - 1) + 1)))) / (sqrt 5) by POWER:32
.= ((tau to_power (n + 1)) - (tau * ((tau_bar to_power (n - 1)) * (tau_bar to_power 1)))) / (sqrt 5) by JakPower32
.= ((tau to_power (n + 1)) - (tau * ((tau_bar to_power (n - 1)) * tau_bar))) / (sqrt 5) by POWER:30
.= ((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 B2
.= (((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:63
.= (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 JakPower32
.= (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 B3
.= (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 B0, XCMPLX_1:90
.= (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)) by POWER:30
.= (Fib (n + 1)) - (tau_bar to_power ((n - 1) + 1)) by JakPower32
.= (Fib (n + 1)) - (tau_bar to_power n) ;
then C2: Fib (n + 1) = ((tau * (Fib n)) + 1) - (1 - (tau_bar to_power n)) ;
tau_bar to_power n < 1 by hop8, A0, XXREAL_0:2;
then - (tau_bar to_power n) > - 1 by XREAL_1:26;
then (- (tau_bar to_power n)) + 1 > (- 1) + 1 by XREAL_1:10;
then D1: Fib (n + 1) < (tau * (Fib n)) + 1 by C2, XREAL_1:46;
(tau * (Fib n)) + 1 < (Fib (n + 1)) + 1

proof

M1: 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:75
.= ((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) by POWER:30
.= ((tau to_power (n + 1)) - (tau * (tau_bar to_power n))) / (sqrt 5) by POWER:32
.= ((tau to_power (n + 1)) / (sqrt 5)) - ((tau * (tau_bar to_power n)) / (sqrt 5)) by XCMPLX_1:121 ;
M2: 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:121 ;
(tau_bar to_power n) * tau > (tau_bar to_power n) * tau_bar by H1, XREAL_1:70;
then (tau_bar to_power n) * tau > (tau_bar to_power n) * (tau_bar to_power 1) by POWER:30;
then (tau * (tau_bar to_power n)) / (sqrt 5) > ((tau_bar to_power n) * (tau_bar to_power 1)) / (sqrt 5) by B0, XREAL_1:76;
then (tau * (tau_bar to_power n)) / (sqrt 5) > (tau_bar to_power (n + 1)) / (sqrt 5) by JakPower32;
then - ((tau * (tau_bar to_power n)) / (sqrt 5)) < - ((tau_bar to_power (n + 1)) / (sqrt 5)) by XREAL_1:26;
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:10;
hence (tau * (Fib n)) + 1 < (Fib (n + 1)) + 1 by M1, M2, XREAL_1:10; :: thesis: verum

end;

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