let n, k be Nat; ( ( ( 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 ) )
; [\(((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
;
(tau_bar to_power n) * (Fib k) <= 1 / 2consider 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
;
(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
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;
verum 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;
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;
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 A25:
n is
odd
;
(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
;
(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
;
(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;
verum end; suppose
m > 1
;
(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)
;
verum end; end; end; suppose A37:
k is
odd
;
(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
m > 0
;
(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)
;
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;
verum
end;
hence
[\(((tau to_power k) * (Fib n)) + (1 / 2))/] = Fib (n + k)
by A3, INT_1:def 6; verum