let n, k be Nat; :: thesis: ( ( ( n >= k & k > 1 ) or ( k = 1 & n > k ) ) implies [\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k) )
set tb = tau_bar ;
set tk = tau to_power k;
set tbk = tau_bar to_power k;
set ts = tau to_power (n + k);
set tbs = tau_bar to_power (n + k);
set tn = tau to_power n;
set tbn = tau_bar to_power n;
assume A1: ( ( n >= k & k > 1 ) or ( k = 1 & n > k ) ) ; :: thesis: [\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k)
A2: (tau to_power k) * (Fib n) = (tau to_power k) * (((tau to_power n) - (tau_bar to_power n)) / (sqrt 5)) by FIB_NUM:7
.= ((tau to_power k) * ((tau to_power n) - (tau_bar to_power n))) / (sqrt 5) by XCMPLX_1:74
.= ((((tau to_power k) * (tau to_power n)) - (tau_bar to_power (n + k))) + ((tau_bar to_power (n + k)) - ((tau to_power k) * (tau_bar to_power n)))) / (sqrt 5)
.= (((tau to_power (n + k)) - (tau_bar to_power (n + k))) + ((tau_bar to_power (n + k)) - ((tau to_power k) * (tau_bar to_power n)))) / (sqrt 5) by Th2
.= (((tau to_power (n + k)) - (tau_bar to_power (n + k))) / (sqrt 5)) + (((tau_bar to_power (n + k)) - ((tau to_power k) * (tau_bar to_power n))) / (sqrt 5)) by XCMPLX_1:62
.= (Fib (n + k)) + (((tau_bar to_power (n + k)) - ((tau to_power k) * (tau_bar to_power n))) / (sqrt 5)) by FIB_NUM:7
.= (Fib (n + k)) + ((((tau_bar to_power n) * (tau_bar to_power k)) - ((tau to_power k) * (tau_bar to_power n))) / (sqrt 5)) by Th2
.= (Fib (n + k)) + (((- (tau_bar to_power n)) * ((tau to_power k) - (tau_bar to_power k))) / (sqrt 5))
.= (Fib (n + k)) + ((- (tau_bar to_power n)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5))) by XCMPLX_1:74
.= (Fib (n + k)) + ((- (tau_bar to_power n)) * (Fib k)) by FIB_NUM:7
.= (Fib (n + k)) - ((tau_bar to_power n) * (Fib k)) ;
A3: ((tau to_power k) * (Fib n)) + (1 / 2) >= Fib (n + k)

proof

(tau_bar to_power n) * (Fib k) <= 1 / 2

proof

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

suppose A4: n is even ; :: thesis: (tau_bar to_power n) * (Fib k) <= 1 / 2

consider m being Nat such that
A5: n = k + m by A1, NAT_1:10;
A6: sqrt 5 > 0 by SQUARE_1:25;
set tbm = tau_bar to_power m;
(tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2

proof

per cases ( k is even or k is odd ) ;

suppose A7: k is even ; :: thesis: (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2

tau_bar to_power (2 * k) > 0 by Th6;
then A8: (- (tau_bar to_power (2 * k))) + 1 < 0 + 1 by XREAL_1:6;
tau_bar to_power (2 * k) < 1 by Th8, A1, XXREAL_0:2;
then - (tau_bar to_power (2 * k)) > - 1 by XREAL_1:24;
then A9: (- (tau_bar to_power (2 * k))) + 1 > (- 1) + 1 by XREAL_1:6;
m is even by A4, A5, A7;
then A10: tau_bar to_power m > 0 by Th6;
tau_bar to_power m <= (sqrt 5) / 2

proof

A11: sqrt 5 > 2 by SQUARE_1:20, SQUARE_1:27;

per cases ( m = 0 or m > 0 ) ;

suppose A12: m = 0 ; :: thesis: tau_bar to_power m <= (sqrt 5) / 2

(sqrt 5) / 2 >= 2 / 2 by A11, XREAL_1:72;
hence tau_bar to_power m <= (sqrt 5) / 2 by A12, POWER:24; :: thesis: verum

end;

suppose A13: m > 0 ; :: thesis: tau_bar to_power m <= (sqrt 5) / 2

sqrt 5 >= 1 by A11, XXREAL_0:2;
then (sqrt 5) / 2 >= 1 / 2 by XREAL_1:72;
hence tau_bar to_power m <= (sqrt 5) / 2 by A13, Th8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then |.(tau_bar to_power m).| <= (sqrt 5) / 2 by A10, ABSVALUE:def 1;
then A14: |.(tau_bar to_power m).| * (1 - (tau_bar to_power (2 * k))) <= ((sqrt 5) / 2) * 1 by A8, A9, XREAL_1:66;
(tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))) <= |.(tau_bar to_power m).| * (1 - (tau_bar to_power (2 * k))) by A9, ABSVALUE:4, XREAL_1:64;
then (tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A14, XXREAL_0:2;
hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A7, FIB_NUM2:3; :: thesis: verum

end;

suppose A15: k is odd ; :: thesis: (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2

then A16: m is odd by A4, A5;
m <> 0 by A15, A4, A5;
then A17: m >= 1 by NAT_1:14;

per cases ( m = 1 or m > 1 ) by A17, XXREAL_0:1;

suppose A18: m = 1 ; :: thesis: (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2

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

proof

A19: tau_bar to_power (2 * k) > 0 by Th6;
tau_bar to_power (2 * k) < 1 / 2 by Th8, A1;
then (tau_bar to_power (2 * k)) + 1 < (1 / 2) + 1 by XREAL_1:6;
then (((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k))) < (6 / 10) * (3 / 2) by Lm23, Lm24, A19, XREAL_1:98;
then ( (((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k))) < 1 & sqrt 5 > 0 ) by SQUARE_1:25, XXREAL_0:2;
then ((((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k)))) * (sqrt 5) < 1 * (sqrt 5) by XREAL_1:68;
then ((((sqrt 5) - 1) * (1 / (sqrt 5))) * (1 + (tau_bar to_power (2 * k)))) * (sqrt 5) < sqrt 5 by XCMPLX_1:99;
then (((sqrt 5) - 1) * (1 + (tau_bar to_power (2 * k)))) * ((sqrt 5) * (1 / (sqrt 5))) < sqrt 5 ;
then ( (((sqrt 5) - 1) * (1 + (tau_bar to_power (2 * k)))) * ((sqrt 5) / (sqrt 5)) < 1 * (sqrt 5) & sqrt 5 > 0 ) by SQUARE_1:25, XCMPLX_1:99;
then (((sqrt 5) - 1) * (1 + (tau_bar to_power (2 * k)))) * 1 < sqrt 5 by XCMPLX_1:60;
then ((1 - (sqrt 5)) * ((- 1) - (tau_bar to_power (2 * k)))) / 2 < (sqrt 5) / 2 by XREAL_1:74;
hence tau_bar * ((- 1) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by FIB_NUM:def 2; :: thesis: verum

end;

then (tau_bar to_power m) * ((- 1) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A18;
hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A15, FIB_NUM2:2; :: thesis: verum

end;

suppose A20: m > 1 ; :: thesis: (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2

A21: tau_bar to_power m < 0 by A16, Th7;
A22: (tau_bar to_power m) * ((- 1) - (tau_bar to_power (2 * k))) = - ((tau_bar to_power m) * (1 + (tau_bar to_power (2 * k)))) ;
A23: tau_bar to_power (2 * k) > 0 by Th6;
tau_bar to_power (2 * k) <= 1 / 2 by A1, Th8;
then A24: (tau_bar to_power (2 * k)) + 1 <= (1 / 2) + 1 by XREAL_1:6;
tau_bar to_power m > - (1 / 2) by Th14, A20;
then - (tau_bar to_power m) < - (- (1 / 2)) by XREAL_1:24;
then (- (tau_bar to_power m)) * (1 + (tau_bar to_power (2 * k))) <= (1 / 2) * (3 / 2) by A21, A23, A24, XREAL_1:66;
then - ((tau_bar to_power m) * (1 + (tau_bar to_power (2 * k)))) <= (sqrt 5) / 2 by Lm25, XXREAL_0:2;
hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by A15, A22, FIB_NUM2:2; :: thesis: verum

end;

end;

end;

end;

end;

then (tau_bar to_power m) * (((tau to_power k) * (tau_bar to_power k)) - (tau_bar to_power (k + k))) <= (sqrt 5) / 2 by Lm3, NEWTON:7;
then (tau_bar to_power m) * (((tau to_power k) * (tau_bar to_power k)) - ((tau_bar to_power k) * (tau_bar to_power k))) <= (sqrt 5) / 2 by Th2;
then (((tau_bar to_power m) * (tau_bar to_power k)) * ((tau to_power k) - (tau_bar to_power k))) / (sqrt 5) <= ((sqrt 5) / 2) / (sqrt 5) by A6, XREAL_1:72;
then ((tau_bar to_power m) * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) <= ((sqrt 5) / 2) / (sqrt 5) by XCMPLX_1:74;
then ((tau_bar to_power m) * (tau_bar to_power k)) * (Fib k) <= ((sqrt 5) / 2) / (sqrt 5) by FIB_NUM:7;
then (tau_bar to_power n) * (Fib k) <= ((sqrt 5) / 2) / (sqrt 5) by A5, Th2;
then (tau_bar to_power n) * (Fib k) <= (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:78;
hence (tau_bar to_power n) * (Fib k) <= 1 / 2 by A6, XCMPLX_1:91; :: thesis: verum

end;

suppose n is odd ; :: thesis: (tau_bar to_power n) * (Fib k) <= 1 / 2

then tau_bar to_power n < 0 by Th7;
hence (tau_bar to_power n) * (Fib k) <= 1 / 2 ; :: thesis: verum

end;

end;

end;

then - ((tau_bar to_power n) * (Fib k)) >= - (1 / 2) by XREAL_1:24;
then (- ((tau_bar to_power n) * (Fib k))) + (1 / 2) >= (- (1 / 2)) + (1 / 2) by XREAL_1:6;
then ((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) + (Fib (n + k)) >= 0 + (Fib (n + k)) by XREAL_1:6;
hence ((tau to_power k) * (Fib n)) + (1 / 2) >= Fib (n + k) by A2; :: thesis: verum

end;

(((tau to_power k) * (Fib n)) + (1 / 2)) - 1 < Fib (n + k)

proof

(tau_bar to_power n) * (Fib k) > - (1 / 2)

proof

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

suppose n is even ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

then tau_bar to_power n > 0 by Th6;
hence (tau_bar to_power n) * (Fib k) > - (1 / 2) ; :: thesis: verum

end;

suppose A25: n is odd ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

consider m being Nat such that
A26: n = k + m by A1, NAT_1:10;
set tbm = tau_bar to_power m;

per cases ( k is even or k is odd ) ;

suppose A27: k is even ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

then A28: m is odd by A25, A26;
then A29: tau_bar to_power m < 0 by Th7;
A30: m >= 1 by A28, NAT_1:14;

per cases ( m = 1 or m > 1 ) by A30, XXREAL_0:1;

suppose A31: m = 1 ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

((3 - (sqrt 5)) / 2) to_power k < 1 to_power k by Lm29, Lm28, A1, POWER:37;
then ((3 - (sqrt 5)) / 2) to_power k < 1 ;
then - (((3 - (sqrt 5)) / 2) to_power k) > - 1 by XREAL_1:24;
then A32: (- (((3 - (sqrt 5)) / 2) to_power k)) + 1 > (- 1) + 1 by XREAL_1:6;
((3 - (sqrt 5)) / 2) to_power k > 0 by Lm28, POWER:34;
then A33: (- (((3 - (sqrt 5)) / 2) to_power k)) + 1 < 0 + 1 by XREAL_1:6;
A34: 1 - (tau_bar to_power (2 * k)) = ((- 1) to_power k) - (tau_bar to_power (2 * k)) by A27, FIB_NUM2:3
.= ((tau to_power k) * (tau_bar to_power k)) - (tau_bar to_power (k + k)) by Lm3, NEWTON:7
.= ((tau to_power k) * (tau_bar to_power k)) - ((tau_bar to_power k) * (tau_bar to_power k)) by Th2
.= (tau_bar to_power k) * ((tau to_power k) - (tau_bar to_power k)) ;
(((sqrt 5) - 1) / (sqrt 5)) * (1 - (((3 - (sqrt 5)) / 2) to_power k)) < 1 * 1 by Lm26, Lm27, A32, A33, XREAL_1:98;
then - ((((sqrt 5) - 1) / (sqrt 5)) * (1 - (((3 - (sqrt 5)) / 2) to_power k))) > - 1 by XREAL_1:24;
then (- (((sqrt 5) - 1) / (sqrt 5))) * (1 - (((3 - (sqrt 5)) / 2) to_power k)) > - 1 ;
then ((- ((sqrt 5) - 1)) / (sqrt 5)) * (1 - (((3 - (sqrt 5)) / 2) to_power k)) > - 1 by XCMPLX_1:187;
then ((1 - (sqrt 5)) / (sqrt 5)) * (1 - (tau_bar to_power (2 * k))) > - 1 by Lm7, NEWTON:9;
then (((1 - (sqrt 5)) / (sqrt 5)) * (1 - (tau_bar to_power (2 * k)))) / 2 > (- 1) / 2 by XREAL_1:74;
then ((1 - (sqrt 5)) / (sqrt 5)) * ((1 - (tau_bar to_power (2 * k))) / 2) > (- 1) / 2 ;
then ((1 - (sqrt 5)) * (1 / (sqrt 5))) * ((1 - (tau_bar to_power (2 * k))) * (1 / 2)) > (- 1) / 2 by XCMPLX_1:99;
then (tau_bar * (1 / (sqrt 5))) * (1 - (tau_bar to_power (2 * k))) > - (1 / 2) by FIB_NUM:def 2;
then (tau_bar * (1 / (sqrt 5))) * ((tau_bar to_power k) * ((tau to_power k) - (tau_bar to_power k))) > - (1 / 2) by A34;
then (tau_bar * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) * (1 / (sqrt 5))) > - (1 / 2) ;
then (tau_bar * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > - (1 / 2) by XCMPLX_1:99;
then ((tau_bar to_power 1) * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > - (1 / 2) ;
then (tau_bar to_power (1 + k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > - (1 / 2) by Th2;
hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by A31, A26, FIB_NUM:7; :: thesis: verum

end;

suppose m > 1 ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

then tau_bar to_power m > - (1 / 2) by Th14;
then A35: - (tau_bar to_power m) < - (- (1 / 2)) by XREAL_1:24;
sqrt 5 > 1 by SQUARE_1:18, SQUARE_1:27;
then - (sqrt 5) < - 1 by XREAL_1:24;
then A36: (- (sqrt 5)) / 2 < (- 1) / 2 by XREAL_1:74;
( tau_bar to_power (2 * k) > 0 & tau_bar to_power (2 * k) < 1 / 2 ) by Th6, Th8, A1;
then ( - (tau_bar to_power (2 * k)) < 0 & - (tau_bar to_power (2 * k)) > - (1 / 2) ) by XREAL_1:24;
then ( (- (tau_bar to_power (2 * k))) + 1 < 0 + 1 & (- (tau_bar to_power (2 * k))) + 1 > (- (1 / 2)) + 1 ) by XREAL_1:6;
then (- (tau_bar to_power m)) * (1 - (tau_bar to_power (2 * k))) < (1 / 2) * 1 by A35, A29, XREAL_1:98;
then - (- ((tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))))) > - (1 / 2) by XREAL_1:24;
then (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) > - (1 / 2) by A27, FIB_NUM2:3;
then (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) > - ((sqrt 5) / 2) by A36, XXREAL_0:2;
then (tau_bar to_power m) * (((tau to_power k) * (tau_bar to_power k)) - (tau_bar to_power (k + k))) > - ((sqrt 5) / 2) by Lm3, NEWTON:7;
then (tau_bar to_power m) * (((tau to_power k) * (tau_bar to_power k)) - ((tau_bar to_power k) * (tau_bar to_power k))) > - ((sqrt 5) / 2) by Th2;
then ((tau_bar to_power m) * (tau_bar to_power k)) * ((tau to_power k) - (tau_bar to_power k)) > - ((sqrt 5) / 2) ;
then ( (tau_bar to_power n) * ((tau to_power k) - (tau_bar to_power k)) > - ((sqrt 5) / 2) & sqrt 5 > 0 ) by Th2, A26, SQUARE_1:25;
then ((tau_bar to_power n) * ((tau to_power k) - (tau_bar to_power k))) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by XREAL_1:74;
then (tau_bar to_power n) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > (- ((sqrt 5) / 2)) / (sqrt 5) by XCMPLX_1:74;
then (tau_bar to_power n) * (Fib k) > ((- (sqrt 5)) / 2) / (sqrt 5) by FIB_NUM:7;
then ( (tau_bar to_power n) * (Fib k) > ((- 1) * (sqrt 5)) / (2 * (sqrt 5)) & sqrt 5 > 0 ) by SQUARE_1:25, XCMPLX_1:78;
then (tau_bar to_power n) * (Fib k) > (- 1) / 2 by XCMPLX_1:91;
hence (tau_bar to_power n) * (Fib k) > - (1 / 2) ; :: thesis: verum

end;

end;

end;

suppose A37: k is odd ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

then A38: m is even by A25, A26;

per cases ( m = 0 or m > 0 ) ;

suppose A39: m = 0 ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

per cases ( k = 1 or k > 1 ) by A1;

suppose k = 1 ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by A1, A39, A26; :: thesis: verum

end;

suppose k > 1 ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

then k >= 1 + 1 by NAT_1:13;
then ( k = 2 or k > 2 ) by XXREAL_0:1;
then k + 1 > 2 + 1 by A37, POLYFORM:5, XREAL_1:6;
then k >= 3 by NAT_1:13;
then k * 2 >= 3 * 2 by XREAL_1:64;
then tau_bar to_power (k * 2) <= tau_bar to_power (3 * 2) by Th11;
then A40: (tau_bar to_power (2 * k)) + 1 <= (9 - (4 * (sqrt 5))) + 1 by Lm9, XREAL_1:6;
sqrt ((20 / 9) ^2) < sqrt 5 by SQUARE_1:27;
then 20 / 9 < sqrt 5 by SQUARE_1:def 2;
then (20 / 9) * 9 < 9 * (sqrt 5) by XREAL_1:68;
then 20 - (8 * (sqrt 5)) < ((sqrt 5) + (8 * (sqrt 5))) - (8 * (sqrt 5)) by XREAL_1:9;
then (20 - (8 * (sqrt 5))) / 2 < (sqrt 5) / 2 by XREAL_1:74;
then (tau_bar to_power (2 * k)) + 1 < (sqrt 5) / 2 by A40, XXREAL_0:2;
then - ((tau_bar to_power (2 * k)) + 1) > - ((sqrt 5) / 2) by XREAL_1:24;
then (- (tau_bar to_power (2 * k))) + (- 1) > - ((sqrt 5) / 2) ;
then (- (tau_bar to_power (2 * k))) + ((- 1) to_power k) > - ((sqrt 5) / 2) by A37, FIB_NUM2:2;
then (- (tau_bar to_power (k + k))) + ((tau to_power k) * (tau_bar to_power k)) > - ((sqrt 5) / 2) by Lm3, NEWTON:7;
then (- ((tau_bar to_power k) * (tau_bar to_power k))) + ((tau to_power k) * (tau_bar to_power k)) > - ((sqrt 5) / 2) by Th2;
then ( (tau_bar to_power k) * ((- (tau_bar to_power k)) + (tau to_power k)) > - ((sqrt 5) / 2) & sqrt 5 > 0 ) by SQUARE_1:25;
then ((tau_bar to_power k) * ((- (tau_bar to_power k)) + (tau to_power k))) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by XREAL_1:74;
then (tau_bar to_power k) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > (- ((sqrt 5) / 2)) / (sqrt 5) by XCMPLX_1:74;
then (tau_bar to_power k) * (Fib k) > (- ((sqrt 5) / 2)) / (sqrt 5) by FIB_NUM:7;
then (tau_bar to_power k) * (Fib k) > - (((sqrt 5) / 2) / (sqrt 5)) by XCMPLX_1:187;
then ( (tau_bar to_power k) * (Fib k) > - (((sqrt 5) / (sqrt 5)) / 2) & sqrt 5 > 0 ) by SQUARE_1:25, XCMPLX_1:48;
hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by A39, A26, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

suppose m > 0 ; :: thesis: (tau_bar to_power n) * (Fib k) > - (1 / 2)

then A41: ( tau_bar to_power m > 0 & tau_bar to_power m < 1 / 2 ) by A38, Th6, Th8;
sqrt ((3 / 2) ^2) < sqrt 5 by SQUARE_1:27;
then 3 / 2 < sqrt 5 by SQUARE_1:def 2;
then (3 / 2) * 2 < (sqrt 5) * 2 by XREAL_1:68;
then A42: 3 / (2 * 2) < (2 * (sqrt 5)) / (2 * 2) by XREAL_1:74;
A43: ( tau_bar to_power (2 * k) < 1 / 2 & tau_bar to_power (2 * k) > 0 ) by Th8, A1, Th6;
then (tau_bar to_power (2 * k)) + 1 < (1 / 2) + 1 by XREAL_1:6;
then (tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1) < (1 / 2) * ((1 / 2) + 1) by A41, A43, XREAL_1:96;
then (tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1) < (sqrt 5) / 2 by A42, XXREAL_0:2;
then - ((tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1)) > - ((sqrt 5) / 2) by XREAL_1:24;
then (tau_bar to_power m) * ((- (tau_bar to_power (2 * k))) + (- 1)) > - ((sqrt 5) / 2) ;
then (tau_bar to_power m) * ((- (tau_bar to_power (2 * k))) + ((- 1) to_power k)) > - ((sqrt 5) / 2) by A37, FIB_NUM2:2;
then (tau_bar to_power m) * ((- (tau_bar to_power (k + k))) + ((tau to_power k) * (tau_bar to_power k))) > - ((sqrt 5) / 2) by Lm3, NEWTON:7;
then (tau_bar to_power m) * ((- ((tau_bar to_power k) * (tau_bar to_power k))) + ((tau to_power k) * (tau_bar to_power k))) > - ((sqrt 5) / 2) by Th2;
then ((tau_bar to_power m) * (tau_bar to_power k)) * ((tau to_power k) - (tau_bar to_power k)) > - ((sqrt 5) / 2) ;
then ( (tau_bar to_power n) * ((tau to_power k) - (tau_bar to_power k)) > - ((sqrt 5) / 2) & sqrt 5 > 0 ) by A26, Th2, SQUARE_1:25;
then ((tau_bar to_power n) * ((tau to_power k) - (tau_bar to_power k))) / (sqrt 5) > (- ((sqrt 5) / 2)) / (sqrt 5) by XREAL_1:74;
then (tau_bar to_power n) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > (- ((sqrt 5) / 2)) / (sqrt 5) by XCMPLX_1:74;
then (tau_bar to_power n) * (Fib k) > ((- (sqrt 5)) / 2) / (sqrt 5) by FIB_NUM:7;
then ( (tau_bar to_power n) * (Fib k) > ((- 1) * (sqrt 5)) / (2 * (sqrt 5)) & sqrt 5 > 0 ) by SQUARE_1:25, XCMPLX_1:78;
then (tau_bar to_power n) * (Fib k) > (- 1) / 2 by XCMPLX_1:91;
hence (tau_bar to_power n) * (Fib k) > - (1 / 2) ; :: thesis: verum

end;

end;

end;

end;

end;

end;

end;

then - ((tau_bar to_power n) * (Fib k)) < - (- (1 / 2)) by XREAL_1:24;
then (- ((tau_bar to_power n) * (Fib k))) + (1 / 2) < (1 / 2) + (1 / 2) by XREAL_1:6;
then ((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) - 1 < 1 - 1 by XREAL_1:9;
then (((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) - 1) + (Fib (n + k)) < 0 + (Fib (n + k)) by XREAL_1:6;
hence (((tau to_power k) * (Fib n)) + (1 / 2)) - 1 < Fib (n + k) by A2; :: thesis: verum

end;

hence [\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k) by A3, INT_1:def 6; :: thesis: verum