let n, k be natural number ; :: 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 A0: ( ( n >= k & k > 1 ) or ( k = 1 & n > k ) ) ; :: thesis: [\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k)
B0: (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:75
.= ((((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 JakPower32
.= (((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:63
.= (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 JakPower32
.= (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:75
.= (Fib (n + k)) + ((- (tau_bar to_power n)) * (Fib k)) by FIB_NUM:7
.= (Fib (n + k)) - ((tau_bar to_power n) * (Fib k)) ;
A1: ((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 not n is even ) ;

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

consider m being Nat such that
T2: n = k + m by A0, NAT_1:10;
T3: sqrt 5 > 0 by SQUARE_1:93;
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 not k is even ) ;

suppose S1: 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 pom1;
then S2: (- (tau_bar to_power (2 * k))) + 1 < 0 + 1 by XREAL_1:8;
tau_bar to_power (2 * k) < 1 by hop8, A0, XXREAL_0:2;
then - (tau_bar to_power (2 * k)) > - 1 by XREAL_1:26;
then S3: (- (tau_bar to_power (2 * k))) + 1 > (- 1) + 1 by XREAL_1:8;
m is even by T1, T2, S1;
then s4: tau_bar to_power m > 0 by pom1;
tau_bar to_power m <= (sqrt 5) / 2

proof

G1: sqrt 5 > 2 by SQUARE_1:85, SQUARE_1:95;

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

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

(sqrt 5) / 2 >= 2 / 2 by G1, XREAL_1:74;
hence tau_bar to_power m <= (sqrt 5) / 2 by g2, POWER:29; :: thesis: verum

end;

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

sqrt 5 >= 1 by G1, XXREAL_0:2;
then (sqrt 5) / 2 >= 1 / 2 by XREAL_1:74;
hence tau_bar to_power m <= (sqrt 5) / 2 by P2, hop8, XXREAL_0:2; :: thesis: verum

end;

end;

end;

then abs (tau_bar to_power m) <= (sqrt 5) / 2 by s4, ABSVALUE:def 1;
then S5: (abs (tau_bar to_power m)) * (1 - (tau_bar to_power (2 * k))) <= ((sqrt 5) / 2) * 1 by S2, S3, XREAL_1:68;
(tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))) <= (abs (tau_bar to_power m)) * (1 - (tau_bar to_power (2 * k))) by S3, ABSVALUE:11, XREAL_1:66;
then (tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by S5, XXREAL_0:2;
hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by S1, FIB_NUM2:5; :: thesis: verum

end;

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

then S2: not m is even by T1, T2;
m <> 0 by S1, T1, T2;
then pc: m >= 1 by NAT_1:14;

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

suppose Y1: 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

y4: tau_bar to_power (2 * k) > 0 by pom1;
tau_bar to_power (2 * k) < 1 / 2 by hop8, A0;
then (tau_bar to_power (2 * k)) + 1 < (1 / 2) + 1 by XREAL_1:8;
then (((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k))) < (6 / 10) * (3 / 2) by y2, Y3, y4, XREAL_1:100;
then ( (((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k))) < 1 & sqrt 5 > 0 ) by SQUARE_1:93, XXREAL_0:2;
then ((((sqrt 5) - 1) / (sqrt 5)) * (1 + (tau_bar to_power (2 * k)))) * (sqrt 5) < 1 * (sqrt 5) by XREAL_1:70;
then ((((sqrt 5) - 1) * (1 / (sqrt 5))) * (1 + (tau_bar to_power (2 * k)))) * (sqrt 5) < sqrt 5 by XCMPLX_1:100;
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:93, XCMPLX_1:100;
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:76;
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 Y1, POWER:30;
hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by S1, FIB_NUM2:3; :: thesis: verum

end;

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

G1: tau_bar to_power m < 0 by S2, pom2;
G4: (tau_bar to_power m) * ((- 1) - (tau_bar to_power (2 * k))) = - ((tau_bar to_power m) * (1 + (tau_bar to_power (2 * k)))) ;
G5: tau_bar to_power (2 * k) > 0 by pom1;
tau_bar to_power (2 * k) <= 1 / 2 by A0, hop8;
then g7: (tau_bar to_power (2 * k)) + 1 <= (1 / 2) + 1 by XREAL_1:8;
tau_bar to_power m > - (1 / 2) by hop9, G0;
then - (tau_bar to_power m) < - (- (1 / 2)) by XREAL_1:26;
then (- (tau_bar to_power m)) * (1 + (tau_bar to_power (2 * k))) <= (1 / 2) * (3 / 2) by G1, G5, g7, XREAL_1:68;
then - ((tau_bar to_power m) * (1 + (tau_bar to_power (2 * k)))) <= (sqrt 5) / 2 by g8, XXREAL_0:2;
hence (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) <= (sqrt 5) / 2 by S1, G4, FIB_NUM2:3; :: 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 albet3, NEWTON:12;
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 JakPower32;
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 T3, XREAL_1:74;
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:75;
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 T2, JakPower32;
then (tau_bar to_power n) * (Fib k) <= (1 * (sqrt 5)) / (2 * (sqrt 5)) by XCMPLX_1:79;
hence (tau_bar to_power n) * (Fib k) <= 1 / 2 by T3, XCMPLX_1:92; :: thesis: verum

end;

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

then tau_bar to_power n < 0 by pom2;
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:26;
then (- ((tau_bar to_power n) * (Fib k))) + (1 / 2) >= (- (1 / 2)) + (1 / 2) by XREAL_1:8;
then ((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) + (Fib (n + k)) >= 0 + (Fib (n + k)) by XREAL_1:8;
hence ((tau to_power k) * (Fib n)) + (1 / 2) >= Fib (n + k) by B0; :: 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 not n is even ) ;

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

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

end;

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

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

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

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

then P2: not m is even by T1, T2;
then P3: tau_bar to_power m < 0 by pom2;
pc: m >= 1 by P2, NAT_1:14;

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

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

((3 - (sqrt 5)) / 2) to_power k < 1 to_power k by xx, rt, A0, POWER:42;
then ((3 - (sqrt 5)) / 2) to_power k < 1 by POWER:31;
then - (((3 - (sqrt 5)) / 2) to_power k) > - 1 by XREAL_1:26;
then R4: (- (((3 - (sqrt 5)) / 2) to_power k)) + 1 > (- 1) + 1 by XREAL_1:8;
((3 - (sqrt 5)) / 2) to_power k > 0 by rt, POWER:39;
then R5: (- (((3 - (sqrt 5)) / 2) to_power k)) + 1 < 0 + 1 by XREAL_1:8;
R6: 1 - (tau_bar to_power (2 * k)) = ((- 1) to_power k) - (tau_bar to_power (2 * k)) by P1, FIB_NUM2:5
.= ((tau to_power k) * (tau_bar to_power k)) - (tau_bar to_power (k + k)) by albet3, NEWTON:12
.= ((tau to_power k) * (tau_bar to_power k)) - ((tau_bar to_power k) * (tau_bar to_power k)) by JakPower32
.= (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 r2, R3, R4, R5, XREAL_1:100;
then - ((((sqrt 5) - 1) / (sqrt 5)) * (1 - (((3 - (sqrt 5)) / 2) to_power k))) > - 1 by XREAL_1:26;
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:188;
then ((1 - (sqrt 5)) / (sqrt 5)) * (1 - (tau_bar to_power (2 * k))) > - 1 by beta2, NEWTON:14;
then (((1 - (sqrt 5)) / (sqrt 5)) * (1 - (tau_bar to_power (2 * k)))) / 2 > (- 1) / 2 by XREAL_1:76;
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:100;
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 R6;
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:100;
then ((tau_bar to_power 1) * (tau_bar to_power k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > - (1 / 2) by POWER:30;
then (tau_bar to_power (1 + k)) * (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) > - (1 / 2) by JakPower32;
hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by r1, T2, 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 hop9;
then r1: - (tau_bar to_power m) < - (- (1 / 2)) by XREAL_1:26;
sqrt 5 > 1 by SQUARE_1:83, SQUARE_1:95;
then - (sqrt 5) < - 1 by XREAL_1:26;
then r0: (- (sqrt 5)) / 2 < (- 1) / 2 by XREAL_1:76;
( tau_bar to_power (2 * k) > 0 & tau_bar to_power (2 * k) < 1 / 2 ) by pom1, hop8, A0;
then ( - (tau_bar to_power (2 * k)) < 0 & - (tau_bar to_power (2 * k)) > - (1 / 2) ) by XREAL_1:26;
then ( (- (tau_bar to_power (2 * k))) + 1 < 0 + 1 & (- (tau_bar to_power (2 * k))) + 1 > (- (1 / 2)) + 1 ) by XREAL_1:8;
then (- (tau_bar to_power m)) * (1 - (tau_bar to_power (2 * k))) < (1 / 2) * 1 by r1, P3, XREAL_1:100;
then - (- ((tau_bar to_power m) * (1 - (tau_bar to_power (2 * k))))) > - (1 / 2) by XREAL_1:26;
then (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) > - (1 / 2) by P1, FIB_NUM2:5;
then (tau_bar to_power m) * (((- 1) to_power k) - (tau_bar to_power (2 * k))) > - ((sqrt 5) / 2) by r0, 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 albet3, NEWTON:12;
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 JakPower32;
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 JakPower32, T2, SQUARE_1:93;
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:76;
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:75;
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:93, XCMPLX_1:79;
then (tau_bar to_power n) * (Fib k) > (- 1) / 2 by XCMPLX_1:92;
hence (tau_bar to_power n) * (Fib k) > - (1 / 2) ; :: thesis: verum

end;

end;

end;

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

then P2: m is even by T1, T2;

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

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

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

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

hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by A0, p3, T2; :: 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 P1, POLYFORM:5, XREAL_1:8;
then k >= 3 by NAT_1:13;
then k * 2 >= 3 * 2 by XREAL_1:66;
then tau_bar to_power (k * 2) <= tau_bar to_power (3 * 2) by hopp10;
then F2: (tau_bar to_power (2 * k)) + 1 <= (9 - (4 * (sqrt 5))) + 1 by beta6, XREAL_1:8;
sqrt ((20 / 9) ^2 ) < sqrt 5 by SQUARE_1:95;
then 20 / 9 < sqrt 5 by SQUARE_1:def 4;
then (20 / 9) * 9 < 9 * (sqrt 5) by XREAL_1:70;
then 20 - (8 * (sqrt 5)) < ((sqrt 5) + (8 * (sqrt 5))) - (8 * (sqrt 5)) by XREAL_1:11;
then (20 - (8 * (sqrt 5))) / 2 < (sqrt 5) / 2 by XREAL_1:76;
then (tau_bar to_power (2 * k)) + 1 < (sqrt 5) / 2 by F2, XXREAL_0:2;
then - ((tau_bar to_power (2 * k)) + 1) > - ((sqrt 5) / 2) by XREAL_1:26;
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 P1, FIB_NUM2:3;
then (- (tau_bar to_power (k + k))) + ((tau to_power k) * (tau_bar to_power k)) > - ((sqrt 5) / 2) by albet3, NEWTON:12;
then (- ((tau_bar to_power k) * (tau_bar to_power k))) + ((tau to_power k) * (tau_bar to_power k)) > - ((sqrt 5) / 2) by JakPower32;
then ( (tau_bar to_power k) * ((- (tau_bar to_power k)) + (tau to_power k)) > - ((sqrt 5) / 2) & sqrt 5 > 0 ) by SQUARE_1:93;
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:76;
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:75;
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:188;
then ( (tau_bar to_power k) * (Fib k) > - (((sqrt 5) / (sqrt 5)) / 2) & sqrt 5 > 0 ) by SQUARE_1:93, XCMPLX_1:48;
hence (tau_bar to_power n) * (Fib k) > - (1 / 2) by p3, T2, XCMPLX_1:60; :: thesis: verum

end;

end;

end;

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

then R1: ( tau_bar to_power m > 0 & tau_bar to_power m < 1 / 2 ) by P2, pom1, hop8;
sqrt ((3 / 2) ^2 ) < sqrt 5 by SQUARE_1:95;
then 3 / 2 < sqrt 5 by SQUARE_1:def 4;
then (3 / 2) * 2 < (sqrt 5) * 2 by XREAL_1:70;
then r3: 3 / (2 * 2) < (2 * (sqrt 5)) / (2 * 2) by XREAL_1:76;
R2: ( tau_bar to_power (2 * k) < 1 / 2 & tau_bar to_power (2 * k) > 0 ) by hop8, A0, pom1;
then (tau_bar to_power (2 * k)) + 1 < (1 / 2) + 1 by XREAL_1:8;
then (tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1) < (1 / 2) * ((1 / 2) + 1) by R1, R2, XREAL_1:98;
then (tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1) < (sqrt 5) / 2 by r3, XXREAL_0:2;
then - ((tau_bar to_power m) * ((tau_bar to_power (2 * k)) + 1)) > - ((sqrt 5) / 2) by XREAL_1:26;
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 P1, FIB_NUM2:3;
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 albet3, NEWTON:12;
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 JakPower32;
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 T2, JakPower32, SQUARE_1:93;
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:76;
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:75;
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:93, XCMPLX_1:79;
then (tau_bar to_power n) * (Fib k) > (- 1) / 2 by XCMPLX_1:92;
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:26;
then (- ((tau_bar to_power n) * (Fib k))) + (1 / 2) < (1 / 2) + (1 / 2) by XREAL_1:8;
then ((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) - 1 < 1 - 1 by XREAL_1:11;
then (((- ((tau_bar to_power n) * (Fib k))) + (1 / 2)) - 1) + (Fib (n + k)) < 0 + (Fib (n + k)) by XREAL_1:8;
hence (((tau to_power k) * (Fib n)) + (1 / 2)) - 1 < Fib (n + k) by B0; :: thesis: verum

end;

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