:: Representation of the {F}ibonacci and {L}ucas Numbers in Terms of
:: the Floor and Ceiling Functor
:: by Magdalena Jastrz\c{e}bska
::
:: Received November 30, 2009
:: Copyright (c) 2009-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies ARYTM_1, ARYTM_3, SQUARE_1, PRE_FF, NAT_1, FIB_NUM, POWER, INT_1,
FIB_NUM3, CARD_1, NUMBERS, ABIAN, XXREAL_0, RELAT_1, NEWTON, PREPOWER,
COMPLEX1, ZFMISC_1, SUBSET_1, REAL_1, XCMPLX_0;
notations ORDINAL1, SUBSET_1, XBOOLE_0, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0,
SQUARE_1, INT_1, NAT_D, PRE_FF, ZFMISC_1, NEWTON, POWER, FIB_NUM3,
PREPOWER, ABIAN, COMPLEX1, FIB_NUM, PEPIN;
constructors REAL_1, NAT_1, NAT_D, NEWTON, PREPOWER, POWER, PRE_FF, ABIAN,
PEPIN, FIB_NUM, FIB_NUM3;
registrations ORDINAL1, XXREAL_0, XREAL_0, SQUARE_1, NAT_1, INT_1, XCMPLX_0,
COMPLEX1, FIB_NUM3, POWER, NEWTON, PREPOWER, ABIAN, NAT_2;
requirements SUBSET, NUMERALS, REAL, ARITHM;
equalities SQUARE_1;
theorems NAT_1, PRE_FF, SQUARE_1, POWER, NEWTON, PREPOWER, XCMPLX_1, NAT_2,
FIB_NUM, ABIAN, XXREAL_0, INT_1, FIB_NUM3, FIB_NUM2, XREAL_1, NAT_D,
ABSVALUE, SERIES_1, POLYFORM, ORDINAL1, MEASURE6;
schemes NAT_1, NAT_2;
begin :: Preliminaries
Lm1:
for m,n being Nat holds -m <= m * (-1) to_power n
proof
let m,n be Nat;
n is even or n is odd; then
(-1) to_power n = 1 or (-1) to_power n = -1 by FIB_NUM2:2,3;
hence thesis;
end;
Lm2:
for m,n being Nat holds -m * (-1) to_power n >= -m
proof
let m,n be Nat;
n is even or n is odd; then
(-1) to_power n = 1 or (-1) to_power n = -1 by FIB_NUM2:2,3;
hence thesis;
end;
theorem Th1:
for a,b being Real, c being Nat holds
(a / b) to_power c = (a to_power c) / (b to_power c)
proof
let a,b be Real;
let c be Nat;
(a / b) to_power c = (a*(1/b)) |^ c by XCMPLX_1:99
.= a to_power c * (1/b) |^ c by NEWTON:7
.= a to_power c * (1/ b |^ c) by PREPOWER:7
.= (a to_power c) / (b |^ c) by XCMPLX_1:99;
hence thesis;
end;
theorem Th2:
for a being Real, b,c being Integer st a <> 0 holds
a to_power (b+c) = a to_power b * a to_power c
proof
let a be Real;
let b,c be Integer;
assume A1: a <> 0;
thus a to_power b * a to_power c = a #Z b * a to_power c by POWER:43
.= a #Z b * a #Z c by POWER:43
.= a #Z (b+c) by A1,PREPOWER:44
.= a to_power (b+c) by POWER:43;
end;
theorem Th3:
for n being Nat, a being Real st n is even & a <> 0 holds
(-a) to_power n = a to_power n by POWER:47;
theorem Th4:
for n being Nat, a being Real st n is odd & a <> 0 holds
(-a) to_power n = -(a to_power n) by POWER:48;
Lm3:
tau * tau_bar = -1
proof
tau * tau_bar = (1^2 - (sqrt 5)^2) / 4 by FIB_NUM:def 1,def 2
.= (1 - 5) / 4 by SQUARE_1:def 2;
hence thesis;
end;
Lm4:
tau_bar / tau = (sqrt 5 - 3)/2
proof
sqrt 5 > 1 by SQUARE_1:18,27; then
- sqrt 5 < - 1 by XREAL_1:24; then
A1: - sqrt 5 + 1 < -1 + 1 by XREAL_1:6;
tau_bar / tau = ((1-sqrt 5)*2) / ((1+sqrt 5)*2)
by FIB_NUM:def 1,def 2,XCMPLX_1:84
.= (1-sqrt 5) / (1+sqrt 5) by XCMPLX_1:91
.= ((1-sqrt 5) * (1-sqrt 5)) / ((1+sqrt 5) * (1-sqrt 5)) by A1,XCMPLX_1:91
.= (1 - 2*sqrt 5 + (sqrt 5)^2) / (1^2 - (sqrt 5)^2)
.= (1 - 2*sqrt 5 + 5) / (1^2 - (sqrt 5)^2) by SQUARE_1:def 2
.= (6 - 2*sqrt 5)/ (1^2 - 5) by SQUARE_1:def 2
.= (2 * (3 - sqrt 5)) / ((-2) * 2);
hence thesis;
end;
Lm5:
tau / tau_bar = (-3-sqrt 5)/2
proof
A1: sqrt 5 > 0 by SQUARE_1:25;
tau / tau_bar = ((1+sqrt 5) * 2) / ((1-sqrt 5) * 2)
by FIB_NUM:def 1,def 2,XCMPLX_1:84
.= (1 + sqrt 5) / (1 - sqrt 5) by XCMPLX_1:91
.= ((1+sqrt 5) * (1+sqrt 5)) / ((1-sqrt 5) * (1+sqrt 5)) by A1,XCMPLX_1:91
.= ((1+sqrt 5) * (1+sqrt 5)) / (1 - (sqrt 5)^2)
.= ((1+sqrt 5) * (1+sqrt 5)) / (1 - 5) by SQUARE_1:def 2
.= (1 + 2*sqrt 5 + (sqrt 5)^2) / (-4)
.= (1 + 2*sqrt 5 + 5) / (-4) by SQUARE_1:def 2;
hence thesis;
end;
Lm6:
tau to_power 2 = (3 + sqrt 5) / 2
proof
tau to_power 2 = ((1+sqrt 5) / 2) ^2 by FIB_NUM:def 1,POWER:46
.= (1^2 + 2 * 1 * sqrt 5 + (sqrt 5)^2) / 4
.= (1 + 2 * sqrt 5 + 5) / 4 by SQUARE_1:def 2
.= (2 * (3 + sqrt 5)) / (2 * 2);
hence thesis;
end;
Lm7:
tau_bar to_power 2 = (3 - sqrt 5) / 2
proof
tau_bar to_power 2 = ((1 - sqrt 5) / 2) ^2 by FIB_NUM:def 2,POWER:46
.= (1^2 - 2 * 1 * sqrt 5 + (sqrt 5)^2) / 4
.= (1 - 2 * sqrt 5 + 5) / 4 by SQUARE_1:def 2
.= (2 * (3 - sqrt 5)) / (2 * 2);
hence thesis;
end;
Lm8:
tau_bar to_power 3 = 2 - sqrt 5
proof
1 < sqrt 5 by SQUARE_1:18,27; then
A1: 1 - sqrt 5 < sqrt 5 - sqrt 5 by XREAL_1:9;
thus tau_bar to_power 3 = ((1-sqrt 5) / 2) to_power (2+1) by FIB_NUM:def 2
.= ((1-sqrt 5)/2) to_power 2 * ((1-sqrt 5)/2) to_power 1 by Th2,A1
.= ((1-sqrt 5)/2) to_power 2 * ((1-sqrt 5)/2)
.= ((1-sqrt 5)/2) ^2 * ((1-sqrt 5) / 2) by POWER:46
.= ((1 - 2 * 1 * sqrt 5 + (sqrt 5) ^2) * (1 - sqrt 5)) / 8
.= ((1 - 2 * sqrt 5 + 5) * (1 - sqrt 5)) / 8 by SQUARE_1:def 2
.= (6 - 8 * sqrt 5 + 2 * (sqrt 5) ^2) / 8
.= (6 - 8 * sqrt 5 + 2 * 5) / 8 by SQUARE_1:def 2
.= 2 - sqrt 5;
end;
Lm9:
tau_bar to_power 6 = 9 - 4 * sqrt 5
proof
thus tau_bar to_power 6 = tau_bar to_power (3*2)
.= (2 - sqrt 5) to_power 2 by Lm8,NEWTON:9
.= (2 - sqrt 5) ^2 by POWER:46
.= 2 ^2 - 2 * 2 * sqrt 5 + (sqrt 5) ^2
.= 4 - 4 * sqrt 5 + 5 by SQUARE_1:def 2
.= 9 - 4 * sqrt 5;
end;
theorem Th5:
|.tau_bar.| < 1
proof
sqrt 5 < sqrt (3 ^2) by SQUARE_1:27; then
sqrt 5 < 3 by SQUARE_1:def 2; then
sqrt 5 - 1 < 2 + 1 - 1 by XREAL_1:9; then
- (sqrt 5 - 1) > -2 by XREAL_1:24; then
(1 - sqrt 5) / 2 > (-2) / 2 by XREAL_1:74; then
A1: |.tau_bar.| < |.-1 .| + |.0 .| by FIB_NUM:def 2,MEASURE6:37;
|.-1 .| = - -1 by ABSVALUE:def 1; then
|.tau_bar.| < 1 + 0 by A1;
hence thesis;
end;
Lm10:
for n being Nat holds ((|.tau_bar.|) to_power n) * (1/sqrt 5) > 0
proof
let n be Nat;
set b = tau_bar;
sqrt 5 > 0 by SQUARE_1:25;
then |.b.| to_power n > 0 & 1 / sqrt 5 > 0 by POWER:34;
hence thesis;
end;
Lm11:
for n being Nat holds
((|.tau_bar.|) to_power n) * (1/sqrt 5) < 1/2
proof
let n be Nat;
A1: 2 < sqrt 5 by SQUARE_1:20,27; then
A2: 2 / 2 < sqrt 5 / 2 by XREAL_1:74;
set b = tau_bar;
A3: sqrt 5 <> 0 by SQUARE_1:17,27;
A4: sqrt 5 > 0 by SQUARE_1:25;
per cases;
suppose A5: n <> 0;
|.b.| < 1 & |.b.| > 0 by Th5; then
|.b.| to_power n < 1 to_power n by A5,POWER:37; then
|.b.| to_power n < 1; then
|.b.| to_power n < sqrt 5 / 2 by A2,XXREAL_0:2; then
(|.b.| to_power n) / (sqrt 5 / 1) <
(sqrt 5 / 2) / (sqrt 5 / 1) by A4,XREAL_1:74; then
(|.b.| to_power n) / (sqrt 5) <
(1 * sqrt 5) / (2 * sqrt 5) by XCMPLX_1:84; then
(|.b.| to_power n) * (1/sqrt 5) < (1 * sqrt 5) / (2 * sqrt 5)
by XCMPLX_1:99;
hence thesis by A3,XCMPLX_1:91;
end;
suppose n = 0; then
(|.tau_bar.|) to_power n = 1 by POWER:24;
hence thesis by A1,XREAL_1:76;
end;
end;
theorem Th6:
for n being Nat, r being non zero Real st n is even holds
r to_power n > 0
proof
let n be Nat;
let r be non zero Real;
assume A1: n is even;
per cases;
suppose r > 0;
hence thesis by POWER:34;
end;
suppose A2: r < 0;
r to_power n = (-r) to_power n by Th3,A1;
hence thesis by A2,POWER:34;
end;
end;
theorem Th7:
for n being Nat, r being Real st n is odd & r < 0 holds
r to_power n < 0
proof
let n be Nat;
let r be Real;
assume A1: n is odd;
assume A2: r < 0;
A3: r to_power n = (--r) to_power n .= - ((-r) to_power n) by Th4,A1,A2;
(-r) to_power n > 0 by A2,POWER:34;
hence thesis by A3;
end;
theorem Th8:
for n being Nat st n <> 0 holds tau_bar to_power n < 1/2
proof
let n be Nat;
assume n <> 0; then
n + 1 > 0 + 1 by XREAL_1:8; then
n + 1 >= 1 + 1 by NAT_1:13; then
A1: n + 1 = 2 or n >= 2 by NAT_1:8;
per cases by A1;
suppose n = 1;
hence thesis;
end;
suppose n >= 2; then
n <> 0 & n <> 1; then
A2: n is non trivial Nat by NAT_2:def 1;
(tau_bar) to_power n < 1/2
proof
defpred P[Nat] means (|.tau_bar.|) to_power $1 < 1/2;
A3: (|.tau_bar.|) to_power 2 = (- tau_bar) to_power 2 by ABSVALUE:def 1
.= (- tau_bar) ^2 by POWER:46
.= (1 ^2 - 2 * 1 * sqrt 5 + (sqrt 5) ^2) / 4 by FIB_NUM:def 2
.= (1 - 2 * sqrt 5 + 5) / 4 by SQUARE_1:def 2
.= (3 - sqrt 5) / 2;
sqrt 5 > 2 by SQUARE_1:20,27; then
- sqrt 5 < - 2 by XREAL_1:24; then
- sqrt 5 + 3 < - 2 + 3 by XREAL_1:8; then
A4: P[2] by A3,XREAL_1:74;
A5: for k being non trivial Nat st P[k] holds P[k+1]
proof
let k be non trivial Nat;
assume P[k]; then
(|.tau_bar.| to_power k) * (|.tau_bar.|) < (1/2) * (|.tau_bar.|)
by XREAL_1:68; then
A6: (|.tau_bar.| to_power k) * (|.tau_bar.| to_power 1) <
(1/2) * (|.tau_bar.|);
(1/2) * (|.tau_bar.|) < (1/2)*1 by Th5,XREAL_1:68; then
(|.tau_bar.| to_power k) * (|.tau_bar.| to_power 1) < 1/2
by A6,XXREAL_0:2;
hence thesis by Th2;
end;
A7: for n being non trivial Nat holds P[n] from NAT_2:sch 2(A4, A5);
for n being non trivial Nat holds tau_bar to_power n < 1/2
proof
let n be non trivial Nat;
(|.tau_bar.|) to_power n < 1/2 by A7; then
|.tau_bar to_power n.| < 1/2 &
tau_bar to_power n <= |.tau_bar to_power n.|
by ABSVALUE:4,SERIES_1:2;
hence thesis by XXREAL_0:2;
end;
hence thesis by A2;
end;
hence thesis;
end;
end;
theorem
for n,m being Nat, r being Real st
m is odd & n >= m & r < 0 & r > -1 holds
r to_power n >= r to_power m
proof
let n,m be Nat;
let r be Real;
assume A1: m is odd;
assume A2: n >= m;
assume A3: r < 0 & r > -1;
A4: n + 1 > m + 0 by A2,XREAL_1:8;
per cases by A4,NAT_1:22;
suppose n = m;
hence thesis;
end;
suppose A5: n > m;
then reconsider t = n-m as Nat by NAT_1:21;
A6: r to_power n - r to_power m = r to_power (t + m) - r to_power m
.= r to_power t * r to_power m - 1 * r to_power m by Th2,A3
.= (r to_power t - 1) * r to_power m;
A7: r to_power m <= 0 by Th7,A3,A1;
A8: t <> 0 by A5;
A9: |.r.| <= 1 by A3,ABSVALUE:5;
|.r.| <> 1
proof
assume |.r.| = 1; then
|.r.| = |.1 .|;
hence thesis by A3,ABSVALUE:28;
end; then
A10: |.r.| < 1 by A9,XXREAL_0:1;
|.r.| > 0 & t > 0 by A8,A3; then
(|.r.|) to_power t < 1 to_power t by A10,POWER:37; then
(|.r.|) to_power t < 1; then
|.r to_power t.| < 1 & r to_power t <=
|.r to_power t.| by ABSVALUE:4,SERIES_1:2; then
r to_power t < 1 by XXREAL_0:2; then
r to_power t - 1 <= 1 - 1 by XREAL_1:9; then
r to_power n - r to_power m + r to_power m >=
0 + r to_power m by A6,A7,XREAL_1:6;
hence thesis;
end;
end;
theorem Th10:
for n,m being Nat st m is odd & n >= m holds
tau_bar to_power n >= tau_bar to_power m
proof
let n,m be Nat;
assume A1: m is odd;
assume n >= m; then
A2: n + 1 > m + 0 by XREAL_1:8;
per cases by A2,NAT_1:22;
suppose n = m;
hence thesis;
end;
suppose A3: n > m; then
reconsider t = n-m as Nat by NAT_1:21;
A4: tau_bar to_power n - tau_bar to_power m =
tau_bar to_power (t + m) - tau_bar to_power m
.= tau_bar to_power t * tau_bar to_power m - 1 * tau_bar to_power m
by Th2
.= (tau_bar to_power t - 1) * tau_bar to_power m;
A5: tau_bar to_power m <= 0 by Th7,A1;
t <> 0 by A3;
then |.tau_bar.| > 0 & t > 0; then
(|.tau_bar.|) to_power t < 1 to_power t by Th5,POWER:37; then
(|.tau_bar.|) to_power t < 1; then
|.tau_bar to_power t.| < 1 & tau_bar to_power t <=
|.tau_bar to_power t.| by ABSVALUE:4,SERIES_1:2; then
tau_bar to_power t < 1 by XXREAL_0:2; then
tau_bar to_power t - 1 <= 1 - 1 by XREAL_1:9; then
tau_bar to_power n - tau_bar to_power m + tau_bar to_power m >=
0 + tau_bar to_power m by A4,A5,XREAL_1:6;
hence thesis;
end;
end;
theorem Th11:
for n,m being Nat st n is even & m is even & n >= m holds
tau_bar to_power n <= tau_bar to_power m
proof
let n,m be Nat;
assume A1: n is even & m is even & n >= m; then
A2: n + 1 > m + 0 by XREAL_1:8;
per cases by A2,NAT_1:22;
suppose n = m;
hence thesis;
end;
suppose A3: n > m; then
reconsider t = n - m as Nat by NAT_1:21;
A4: tau_bar to_power n - tau_bar to_power m =
tau_bar to_power (t+m) - tau_bar to_power m
.= tau_bar to_power t * tau_bar to_power m - 1 * tau_bar to_power m
by Th2
.= (tau_bar to_power t - 1) * tau_bar to_power m;
A5: tau_bar to_power m > 0 by Th6,A1;
n - m > m - m by A3,XREAL_1:9; then
tau_bar to_power t < 1 by Th8,XXREAL_0:2; then
tau_bar to_power t - 1 < 1 - 1 by XREAL_1:9; then
tau_bar to_power n - tau_bar to_power m + tau_bar to_power m <
0 + tau_bar to_power m by A4,A5,XREAL_1:6;
hence thesis;
end;
end;
theorem Th12:
for m,n being non zero Nat st m >= n holds Lucas m >= Lucas n
proof
let m,n be non zero Nat;
assume A1: m >= n;
per cases by A1,XXREAL_0:1;
suppose m = n;
hence thesis;
end;
suppose A2: m > n;
then consider k being Nat such that A3: m = n + k by NAT_1:10;
A4: for k, n being non zero Nat holds Lucas (n+k) >= Lucas (n)
proof
defpred P[Nat] means
for n being non zero Nat holds Lucas (n+$1) >= Lucas (n);
A5: P[1]
proof
let n be non zero Nat;
n - 0 is Element of NAT & n+1 is Element of NAT by ORDINAL1:def 12;
hence thesis by FIB_NUM3:18;
end;
A6: for k being non zero Nat st P[k] holds P[k + 1]
proof
let k be non zero Nat;
assume A7: P[k];
for n being non zero Nat holds Lucas (n + (k + 1)) >= Lucas n
proof
let n be non zero Nat;
reconsider p = n + k as Element of NAT by ORDINAL1:def 12;
p is non zero Element of NAT; then
Lucas (n + k) >= Lucas n & Lucas (n + k + 1) >= Lucas (n + k)
by A7,FIB_NUM3:18;
hence thesis by XXREAL_0:2;
end;
hence thesis;
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A5,A6);
hence thesis;
end;
k is non zero Nat & n is non zero Nat by A3,A2;
hence thesis by A3,A4;
end;
end;
Lm12: tau_bar ^2 = (3 - sqrt 5) / 2 by Lm7,POWER:46;
Lm13: sqrt 5 > 0 by SQUARE_1:25; then
sqrt 5 + 3 > -sqrt 5 + 3 by XREAL_1:6; then
(sqrt 5 + 3) / 2 > (-sqrt 5 + 3) / 2 by XREAL_1:74; then
Lm14: tau ^2 > tau_bar ^2 by Lm6,Lm12,POWER:46;
sqrt 5 < sqrt (3 ^2) by SQUARE_1:27; then
sqrt 5 < 3 by SQUARE_1:def 2; then
sqrt 5 - 3 < 3 - 3 by XREAL_1:9; then
Lm15: (sqrt 5 - 3) / 2 < 0;
theorem
for n being non zero Nat holds
tau to_power n > tau_bar to_power n
proof
let n be non zero Nat;
set tb = tau_bar;
per cases;
suppose A1: n is even;
consider k being Nat such that A2: n = 2*k by A1,ABIAN:def 2;
A3: k > 0 by A2;
A4: tau to_power n = (tau to_power 2) to_power k by A2,NEWTON:9
.= (tau ^2) to_power k by POWER:46;
tau_bar to_power n = (tau_bar to_power 2) to_power k by A2,NEWTON:9
.= (tau_bar)^2 to_power k by POWER:46;
hence thesis by A3,A4,Lm14,POWER:37;
end;
suppose n is odd;
then
consider k being Nat such that A5: n = 2*k+1 by ABIAN:9;
set kk = tau to_power (2*k);
A6: (tau/tb) to_power (2*k) = (tau/tb) to_power 2 to_power k by NEWTON:9
.= ((tau/tb) ^2) to_power k by POWER:46;
tb to_power (2 * k) = (tb to_power 2) to_power k by NEWTON:9
.= (tau_bar ^2) to_power k by POWER:46; then
A7: tb to_power (2 * k) > 0 by POWER:34;
(tau / tb) to_power (2*k) > (sqrt 5 - 3)/2 by A6,Lm15,POWER:34; then
(tau / tb) to_power (2*k) * ((-3-sqrt 5)/2) < (tb/tau) * ((-3-sqrt 5)/2)
by Lm13,Lm4,XREAL_1:69; then
(tau/tb) to_power (2*k) * (tau/tb) < 1 by Lm5,XCMPLX_1:112; then
(kk/tb to_power (2*k)) * (tau/tb) < 1 by Th1; then
kk * (1/tb to_power (2*k)) * (tau/tb) < 1 by XCMPLX_1:99; then
kk*(1/tb to_power (2*k)) * (tau/tb)*tb to_power (2*k) <
1 * (tb to_power (2*k)) by A7,XREAL_1:68; then
kk * (tau/tb)*(tb to_power (2*k) *(1/tb to_power (2*k)))
< 1 * (tb to_power (2*k)); then
kk * (tau/tb)*(tb to_power (2*k)/tb to_power (2*k)) <
1 * (tb to_power (2*k)) by XCMPLX_1:99; then
kk*(tau/tb)*1 < tb to_power (2*k) by A7,XCMPLX_1:60; then
kk * (tau *(1/tb))*1 < tb to_power (2*k) by XCMPLX_1:99; then
kk * (tau *(1/tb)) * 1 * tb > tb to_power (2*k) * tb by XREAL_1:69; then
kk * tau * ((1/tb) *1 *tb) > tb to_power (2*k) * tb; then
kk * tau * (tb / tb) > tb to_power (2*k) * tb by XCMPLX_1:99; then
kk *tau*1 > tb to_power (2*k) * tb by XCMPLX_1:60; then
kk*tau > tb to_power (2*k)*tb to_power 1;then
kk * tau > tb to_power (2*k+1) by Th2; then
kk * tau to_power 1 > tb to_power (2*k+1);
hence thesis by A5,Th2;
end;
end;
theorem Th14:
for n being Nat st n > 1 holds -1/2 < tau_bar to_power n
proof
let n be Nat;
assume A1: n > 1;
A2: n + 1 > 1 + 1 by A1,XREAL_1:8;
per cases;
suppose n is even; then
consider k being Nat such that
A3: n = 2 * k by ABIAN:def 2;
A4: 0^2 = 0;
tau_bar to_power n = tau_bar to_power k to_power 2 by A3,NEWTON:9
.= (tau_bar to_power k) ^2 by POWER:46;
hence thesis by A4,SQUARE_1:12;
end;
suppose A5: n is odd;
n >= 2 by A2,NAT_1:13; then
n = 2 or n > 2 by XXREAL_0:1; then
n + 1 > 2 + 1 by A5,POLYFORM:5,XREAL_1:6; then
n >= 3 by NAT_1:13; then
A6: tau_bar to_power n >= tau_bar to_power 3 by Th10,POLYFORM:6;
sqrt 5 < sqrt ((5 / 2) ^2) by SQUARE_1:27; then
sqrt 5 < 5 / 2 by SQUARE_1:def 2; then
2 * sqrt 5 < 2 * (5 / 2) by XREAL_1:68; then
-2 * sqrt 5 > - 5 by XREAL_1:24; then
- 2 * sqrt 5 + 4 > -5 + 4 by XREAL_1:6; then
(2 * (2 - sqrt 5)) / 2 > (-1) / 2 by XREAL_1:74;
hence thesis by A6,Lm8,XXREAL_0:2;
end;
end;
theorem Th15:
for n being Nat st n > 2 holds tau_bar to_power n >= - 1/sqrt 5
proof
let n be Nat;
assume n > 2;
then n >= 2+1 by NAT_1:13; then
A1: tau_bar to_power n >= tau_bar to_power 3 by Th10,POLYFORM:6;
A2: sqrt 5 > 0 by SQUARE_1:25;
sqrt 5 >= 2 by SQUARE_1:20,26; then
2 * sqrt 5 >= 2 * 2 by XREAL_1:64; then
2 * sqrt 5 - 5 >= 4 - 5 by XREAL_1:9; then
2 * sqrt 5 - (sqrt 5)^2 >= -1 by SQUARE_1:def 2; then
((2 - sqrt 5) * sqrt 5) / sqrt 5 >= (-1) / sqrt 5 by A2,XREAL_1:72; then
((2 - sqrt 5) * sqrt 5) / sqrt 5 >= -1 / sqrt 5 by XCMPLX_1:187; then
2 - sqrt 5 >= -1 / sqrt 5 by A2,XCMPLX_1:89;
hence thesis by A1,Lm8,XXREAL_0:2;
end;
theorem Th16:
for n being Nat st n >= 2 holds tau_bar to_power n <= 1/sqrt 5
proof
let n be Nat;
assume A1: n >= 2;
per cases;
suppose A2: n is even;
A3: sqrt 5 > 0 by SQUARE_1:25;
A4: tau_bar to_power n <= (3 - sqrt 5) / 2 by Lm7,A1,A2,Th11,POLYFORM:5;
sqrt 5 <= sqrt ((7/3) ^2) by SQUARE_1:26; then
sqrt 5 <= 7/3 by SQUARE_1:def 2; then
3 * sqrt 5 <= (7 / 3) * 3 by XREAL_1:64; then
3 * sqrt 5 - 5 <= 7 - 5 by XREAL_1:9; then
3 * sqrt 5 - (sqrt 5) ^2 <= 2 by SQUARE_1:def 2; then
(3 * sqrt 5 - sqrt 5 * sqrt 5) / 2 <= 2 / 2 by XREAL_1:72; then
(((3-sqrt 5) / 2) * sqrt 5) / sqrt 5 <= 1 / sqrt 5 by A3,XREAL_1:72; then
(3 - sqrt 5) / 2 <= 1 / sqrt 5 by A3,XCMPLX_1:89;
hence thesis by A4,XXREAL_0:2;
end;
suppose n is odd; then
A5: tau_bar to_power n < 0 by Th7;
sqrt 5 >= sqrt 0 by SQUARE_1:26;
hence thesis by A5;
end;
end;
theorem Th17:
for n being Nat holds (tau_bar to_power n)/sqrt 5 + 1/2 > 0 &
(tau_bar to_power n)/sqrt 5 + 1/2 < 1
proof
let n be Nat;
set b = (1-sqrt 5)/2;
A1: |.b.| = -b by ABSVALUE:def 1,FIB_NUM:def 2;
A2: (|.b.| to_power n) * (1/sqrt 5) < 1/2 by Lm11,FIB_NUM:def 2;
(b to_power n)*(1/sqrt 5) + 1/2 > 0 & (b to_power n)*(1/sqrt 5) + 1/2 < 1
proof
per cases;
suppose n is even;
then
|.b.| to_power n = b to_power n by Th3,A1,FIB_NUM:def 2; then
(b to_power n)*(1/sqrt 5) > 0 & (b to_power n)*(1/sqrt 5) < 1/2
by Lm10,Lm11,FIB_NUM:def 2; then
(b to_power n) * (1/sqrt 5) > 0 &
(b to_power n) * (1/sqrt 5) + 1/2 < 1/2 + 1/2 by XREAL_1:8;
hence thesis;
end;
suppose n is odd; then
|.b.| to_power n = - (b to_power n) by Th4,A1,FIB_NUM:def 2; then
(-(b to_power n))*(1/sqrt 5) > 0 & - (b to_power n)*(1/sqrt 5) < 1/2
by Lm10,A2,FIB_NUM:def 2; then
-(b to_power n)/sqrt 5 > 0 & - (b to_power n)/sqrt 5 < 1/2
by XCMPLX_1:99; then
(b to_power n)/sqrt 5 < 0 & - -(b to_power n)/sqrt 5 > - (1/2)
by XREAL_1:24; then
(b to_power n)/sqrt 5 + 1/2 < 0 + 1/2 &
(b to_power n)/sqrt 5 + 1/2 > -1/2 + 1/2 by XREAL_1:8; then
(b to_power n)/sqrt 5 + 1/2 < 1 & (b to_power n)/sqrt 5 + 1/2 > 0
by XXREAL_0:2;
hence thesis by XCMPLX_1:99;
end;
end;
hence thesis by FIB_NUM:def 2,XCMPLX_1:99;
end;
begin :: Formulas for the Fibonacci Numbers
theorem
for n being Nat holds [\ (tau to_power n )/sqrt 5 + 1/2 /] = Fib n
proof
let n be Nat;
set tn = tau_bar to_power n;
A1: Fib n = ((tau to_power n) - tn)/(sqrt 5) + 1/2 - 1/2 by FIB_NUM:7
.= (tau to_power n)/sqrt 5 - tn / sqrt 5 + 1/2 - 1/2 by XCMPLX_1:120
.= ((tau to_power n)/sqrt 5 + 1/2) - (tn/sqrt 5 + 1/2);
tn/sqrt 5 + 1/2 > 0 by Th17; then
A2: tn/sqrt 5 + 1/2 + Fib n > 0 + Fib n by XREAL_1:6;
tn/sqrt 5 + 1/2 < 1 by Th17; then
tn/sqrt 5 + 1/2 - 1/2 < 1 - 1/2 by XREAL_1:9; then
- (tn/sqrt 5) > - (1/2) by XREAL_1:24; then
- (tn/sqrt 5) + (tau to_power n)/sqrt 5 >
- (1/2) + (tau to_power n)/sqrt 5 by XREAL_1:6; then
(tau to_power n)/sqrt 5 - (tn/sqrt 5) >
- (1/2) + (tau to_power n)/sqrt 5; then
((tau to_power n) - tn)/sqrt 5 >
- (1/2) + (tau to_power n)/sqrt 5 by XCMPLX_1:120; then
Fib n > (tau to_power n )/sqrt 5 + 1/2 - 1 by FIB_NUM:7;
hence thesis by A2,A1,INT_1:def 6;
end;
theorem
for n being Nat st n <> 0 holds
[/ (tau to_power n)/sqrt 5 - 1/2 \] = Fib n
proof
let n be Nat;
set tn = tau to_power n;
set tbn = tau_bar to_power n;
assume A1: n <> 0;
A2: sqrt 5 > 0 by SQUARE_1:25;
A3: tn / sqrt 5 - 1/2 <= Fib n
proof
1 <= sqrt 5 by SQUARE_1:18,26; then
1 / 2 <= sqrt 5 / 2 by XREAL_1:72;
then tbn <= sqrt 5 / 2 by A1,Th8,XXREAL_0:2; then
tbn / sqrt 5 <= sqrt 5 / 2 / sqrt 5 by A2,XREAL_1:72; then
tbn / sqrt 5 <= sqrt 5 / sqrt 5 / 2 by XCMPLX_1:48; then
tbn / sqrt 5 <= 1 / 2 by A2,XCMPLX_1:60; then
-tbn / sqrt 5 >= -1 / 2 by XREAL_1:24; then
-tbn / sqrt 5 + tn/sqrt 5 >= -1/2 + tn / sqrt 5 by XREAL_1:6; then
tn / sqrt 5 - tbn / sqrt 5 >= -1/2 + tn / sqrt 5; then
(tn - tbn) / sqrt 5 >= tn / sqrt 5 - 1/2 by XCMPLX_1:120;
hence thesis by FIB_NUM:7;
end;
tn / sqrt 5 - 1 / 2 + 1 > Fib n
proof
n+1 > 0+1 by A1,XREAL_1:6; then
A4: n >= 1 by NAT_1:13;
per cases by A4,XXREAL_0:1;
suppose A5: n = 1; then
A6: tn / sqrt 5 - 1/2 + 1 = tau / sqrt 5 - 1/2 + 1
.= (1 + sqrt 5) / 2 / sqrt 5 + (1 - 1/2) by FIB_NUM:def 1
.= (1 + sqrt 5) / sqrt 5 / 2 + 1 / 2 by XCMPLX_1:48
.= ((1 + sqrt 5) / sqrt 5 + 1) / 2
.= (1 / sqrt 5 + sqrt 5 / sqrt 5 + 1) / 2 by XCMPLX_1:62
.= (1 / sqrt 5 + 1 + 1) / 2 by A2,XCMPLX_1:60
.= 1 / sqrt 5 / 2 + 2 / 2;
1/sqrt 5/2 + 1 > 0 + 1 by A2,XREAL_1:6;
hence thesis by A5,A6,PRE_FF:1;
end;
suppose A7: n > 1;
1 < sqrt 5 by SQUARE_1:18,27; then
1 / 2 < sqrt 5 / 2 by XREAL_1:74; then
A8: - 1 / 2 > - sqrt 5 / 2 by XREAL_1:24;
tbn > - 1 / 2 by A7,Th14; then
tbn > - sqrt 5 / 2 by A8,XXREAL_0:2; then
tbn / sqrt 5 > (-sqrt 5 / 2) / sqrt 5 by A2,XREAL_1:74; then
tbn / sqrt 5 > - (sqrt 5 / 2 / sqrt 5) by XCMPLX_1:187; then
tbn / sqrt 5 > - (sqrt 5 / sqrt 5 / 2) by XCMPLX_1:48; then
tbn / sqrt 5 > - 1 / 2 by A2,XCMPLX_1:60; then
-tbn / sqrt 5 < - -1 / 2 by XREAL_1:24; then
- tbn / sqrt 5 + tn / sqrt 5 < 1 / 2 + tn / sqrt 5 by XREAL_1:6; then
tn / sqrt 5 - tbn / sqrt 5 < 1 / 2 + tn / sqrt 5; then
(tn - tbn) / sqrt 5 < 1 / 2 + tn / sqrt 5 by XCMPLX_1:120;
hence thesis by FIB_NUM:7;
end;
end;
hence thesis by A3,INT_1:def 7;
end;
set s5 = sqrt 5;
Lm16: 1 < s5 by SQUARE_1:18,27;
1 - s5 <> 0 by SQUARE_1:18,27; then
(1 - s5) ^2 > 0 by SQUARE_1:12; then
Lm17: (1 - s5) to_power 2 > 0 by POWER:46;
Lm18: s5 > 0 by SQUARE_1:25;
2 * 1 < 2 * s5 by Lm16,XREAL_1:68; then
- 2 * s5 < - 2 by XREAL_1:24; then
- 2 * s5 + 6 < - 2 + 6 by XREAL_1:8; then
1 - 2 * s5 + 5 < 4; then
1 ^2 - 2 * 1 * s5 + s5 ^2 < 4 by SQUARE_1:def 2; then
(1 - s5) ^2 < 2 ^2; then
(1 - s5) ^2 < 2 to_power 2 by POWER:46; then
Lm19: (1 - s5) to_power 2 < 2 to_power 2 by POWER:46;
theorem
for n being Nat st n <> 0 holds
[\ (tau to_power (2*n)) / sqrt 5 /] = Fib (2*n)
proof
let n be Nat;
assume A1: n <> 0;
A2: (tau to_power (2*n)) / s5 - 1 < Fib (2*n)
proof
A3: 2 to_power (2*n) > 0 by POWER:34;
(1 - s5) to_power 2 to_power n < (2 to_power 2) to_power n
by A1,Lm17,Lm19,POWER:37; then
((1-s5) to_power 2) to_power n < 2 to_power (2*n) by POWER:33; then
(1 - s5) to_power (2*n) < 2 to_power (2*n) by NEWTON:9; then
((1 - s5) to_power (2*n)) / (2 to_power (2*n)) <
(2 to_power (2*n)) / (2 to_power (2*n)) by A3,XREAL_1:74; then
((1 - s5) to_power (2*n)) / (2 to_power (2*n)) < 1
by A3,XCMPLX_1:60; then
tau_bar to_power (2*n) < 1 by Th1,FIB_NUM:def 2; then
tau_bar to_power (2*n) < s5 by Lm16,XXREAL_0:2; then
(tau_bar to_power (2*n))/s5 < s5 /s5 by Lm18,XREAL_1:74; then
(tau_bar to_power (2*n)) / s5 < 1 by Lm18,XCMPLX_1:60; then
- ((tau_bar to_power (2*n)) / s5) > -1 by XREAL_1:24; then
- ((tau_bar to_power (2*n))/s5) + (tau to_power (2*n)) / s5 >
-1 + (tau to_power (2*n)) / s5 by XREAL_1:8; then
(tau to_power (2*n)) / s5 - ((tau_bar to_power (2*n))/s5) >
-1 + (tau to_power (2*n)) / s5; then
(tau to_power (2*n) - tau_bar to_power (2*n)) / s5 >
-1 + (tau to_power (2*n)) / sqrt 5 by XCMPLX_1:120;
hence thesis by FIB_NUM:7;
end;
tau_bar to_power (2*n) = tau_bar to_power 2 |^ n by NEWTON:9
.= tau_bar ^2 to_power n by POWER:46; then
tau_bar to_power (2*n) > 0 by POWER:34; then
- (tau_bar to_power (2*n)) / sqrt 5 + (tau to_power (2*n)) / s5 <
0 + (tau to_power (2*n)) / s5 by Lm18,XREAL_1:8; then
(tau to_power (2*n)) / s5 - (tau_bar to_power (2*n)) / s5 <
(tau to_power (2*n)) / s5; then
(tau to_power (2*n) - tau_bar to_power (2*n)) / s5 <
(tau to_power (2*n)) / s5 by XCMPLX_1:120; then
Fib (2*n) <= (tau to_power (2*n)) / s5 by FIB_NUM:7;
hence thesis by A2,INT_1:def 6;
end;
theorem
for n being Nat holds
[/ (tau to_power (2*n+1)) / sqrt 5 \] = Fib (2*n+1)
proof
let n be Nat;
A1: Fib (2 * n + 1) =
((tau to_power (2*n+1)) - (tau_bar to_power (2*n+1)))/(sqrt 5) by FIB_NUM:7
.= (tau to_power (2*n+1))/sqrt 5 - (tau_bar to_power (2*n+1))/sqrt 5
by XCMPLX_1:120;
A2: sqrt 5 > 0 by SQUARE_1:17,27;
tau_bar to_power (2*n+1) < 0
proof
set t = - tau_bar;
A3: tau_bar to_power (2*n+1) = (-t) to_power (2*n+1)
.= - (t to_power (2*n+1)) by Th4;
t to_power (2*n+1) > 0 by POWER:34;
hence thesis by A3;
end; then
A4:(tau to_power (2*n+1)) / sqrt 5 <= Fib (2*n+1) by A1,A2,XREAL_1:46;
(tau_bar to_power (2*n+1)) / sqrt 5 + 1 / 2 > 0 by Th17; then
(tau_bar to_power (2*n+1)) / sqrt 5 + 1/2 - 1/2 > 0 - 1/2 by XREAL_1:9;
then (tau_bar to_power (2*n+1)) / sqrt 5 > -1 by XXREAL_0:2; then
- ((tau_bar to_power (2*n+1)) / sqrt 5) < - -1 by XREAL_1:24; then
- ((tau_bar to_power (2*n+1)) / sqrt 5) + (tau to_power (2*n+1)) / sqrt 5 <
1 + (tau to_power (2*n+1)) / sqrt 5 by XREAL_1:8; then
(tau to_power (2*n+1)) / sqrt 5 - ((tau_bar to_power (2*n+1)) / sqrt 5) <
1 + (tau to_power (2*n+1)) / sqrt 5; then
(tau to_power (2*n+1) - tau_bar to_power (2*n+1)) / sqrt 5 <
1 + (tau to_power (2*n+1)) / sqrt 5 by XCMPLX_1:120; then
Fib (2*n+1) < (tau to_power (2*n+1)) / sqrt 5 + 1 by FIB_NUM:7;
hence thesis by A4,INT_1:def 7;
end;
theorem Th22:
for n being Nat st n >= 2 & n is even holds
Fib (n+1) = [\ tau * Fib n + 1 /]
proof
let n be Nat;
assume A1: n >= 2 & n is even;
set t = tau;
set tb = tau_bar;
A2: sqrt 5 > 0 by SQUARE_1:17,27;
A3: t * tb = (1 ^2 - (sqrt 5) ^2) / 4 by FIB_NUM:def 1,def 2
.= (1-5)/4 by SQUARE_1:def 2
.= -1;
tb to_power n = (-tb) to_power n by A1,Th3; then
A4: tb to_power n > 0 by POWER:34;
A5: tb to_power 2 + 1 = tb ^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) * tb by FIB_NUM:def 2;
t * Fib n = t * ((t to_power n - tb to_power n) / sqrt 5) by FIB_NUM:7
.= (t * (t to_power n - tb to_power n)) / sqrt 5 by XCMPLX_1:74
.= (t * (t to_power n) - t * (tb to_power n)) / sqrt 5
.= ((t to_power 1) * (t to_power n) - t * (tb to_power n)) / sqrt 5
.= (t to_power (n+1) - t * (tb to_power ((n-1)+1))) / sqrt 5 by POWER:27
.= (t to_power (n+1) - t * ((tb to_power (n-1)) * (tb to_power 1))) /sqrt 5
by Th2
.= (t to_power (n+1) - t * ((tb to_power (n-1)) * tb)) / sqrt 5
.= (t to_power (n+1) - t * tb * (tb to_power (n-1))) / sqrt 5
.= (t to_power (n+1) - (-1) * (tb to_power (n-1))+
tb to_power (n-1) - tb to_power (n-1)) / sqrt 5 by A3
.= (((t to_power (n+1) - tb to_power (n+1))) + (tb to_power (n-1) +
tb to_power (n+1))) / sqrt 5
.= ((t to_power (n+1) - tb to_power (n+1))) / sqrt 5 + (tb to_power (n-1) +
tb to_power ((n-1)+2)) / sqrt 5 by XCMPLX_1:62
.= Fib (n+1) + (tb to_power (n-1) +
tb to_power ((n-1)+2)) / sqrt 5 by FIB_NUM:7
.= Fib (n+1) + ((tb to_power (n-1)) * 1 +
(tb to_power (n-1)) * (tb to_power 2)) / sqrt 5 by Th2
.= Fib (n+1) + ((tb to_power (n-1)) * (1 + (tb to_power 2))) / sqrt 5
.= Fib (n+1) + ((tb to_power (n-1)) * (-(sqrt 5) * tb)) / sqrt 5 by A5
.= Fib (n+1) + ((-1) * (tb to_power (n-1)) * tb * (sqrt 5)) / sqrt 5
.= Fib (n+1) + ((-1) * (tb to_power (n-1))*tb) by A2,XCMPLX_1:89
.= Fib (n+1) - ((tb to_power (n-1)) * tb)
.= Fib (n+1) - ((tb to_power (n-1)) * (tb to_power 1))
.= Fib (n+1) - (tb to_power (n-1+1)) by Th2
.= Fib (n+1) - (tb to_power n); then
A6: Fib (n+1) = (t * Fib n + 1) - (1 - (tb to_power n));
tb to_power n < 1 by Th8,A1,XXREAL_0:2; then
- (tb to_power n) > - 1 by XREAL_1:24; then
- (tb to_power n) + 1 > - 1 + 1 by XREAL_1:8; then
A7: Fib (n+1) < t * Fib n + 1 by A6,XREAL_1:44;
t * Fib n + 1 < Fib (n+1) + 1
proof
A8: t * Fib n = t * ((t to_power n - tb to_power n) / sqrt 5) by FIB_NUM:7
.= (t*(t to_power n - tb to_power n)) / sqrt 5 by XCMPLX_1:74
.= (t*t to_power n - t * tb to_power n) / sqrt 5
.= (t to_power 1 * t to_power n - t * tb to_power n) /sqrt 5
.= (t to_power (n+1) - t * tb to_power n) / sqrt 5 by POWER:27
.= t to_power (n+1)/sqrt 5 - (t * tb to_power n) /sqrt 5 by XCMPLX_1:120;
A9: Fib (n+1) = (t to_power (n+1) - tb to_power (n+1)) / sqrt 5 by FIB_NUM:7
.= t to_power (n+1) / sqrt 5 - tb to_power (n+1) /sqrt 5 by XCMPLX_1:120;
(tb to_power n * t) > (tb to_power n * tb) by A4,XREAL_1:68; then
(tb to_power n * t) > (tb to_power n * tb to_power 1); then
(t * tb to_power n)/sqrt 5 > (tb to_power n * tb to_power 1) / sqrt 5
by A2,XREAL_1:74; then
(t * tb to_power n)/sqrt 5 > tb to_power (n+1)/sqrt 5 by Th2; then
- (t * tb to_power n)/sqrt 5 < - tb to_power (n+1) /sqrt 5 by XREAL_1:24;
then - (t * tb to_power n) / sqrt 5 + t to_power (n+1) / sqrt 5 <
- tb to_power (n+1) / sqrt 5 + t to_power (n+1) / sqrt 5 by XREAL_1:8;
hence thesis by A8,A9,XREAL_1:8;
end; then
t * Fib n + 1 - 1 < Fib (n+1) + 1 - 1 by XREAL_1:9;
hence thesis by A7,INT_1:def 6;
end;
theorem Th23:
for n being Nat st n >= 2 & n is odd holds
Fib (n+1) = [/ tau * Fib n - 1 \]
proof
let n be Nat;
assume A1: n >= 2 & n is odd;
A2: sqrt 5 > 0 by SQUARE_1:17,27;
tau * tau_bar to_power n + sqrt 5 >= tau_bar to_power (n+1)
proof
set tbn = tau_bar to_power n;
A3: tbn < 0 by A1,Th7;
tau + sqrt 5 / tbn <= tau_bar
proof
n > 1 by A1,XXREAL_0:2; then
tbn >= - 1 / 2 by Th14; then
tbn > -1 by XXREAL_0:2; then
tbn + 1 >= - 1 + 1 by XREAL_1:6; then
(tbn + 1) / tbn <= 0 / tbn by A3; then
tbn / tbn + 1/ tbn <= 0 by XCMPLX_1:62; then
1 + 1 / tbn <= 0 by A3,XCMPLX_1:60; then
(1 + 1 / tbn) * sqrt 5 <= 0 * sqrt 5 by A2; then
1 * sqrt 5 + (1 / tbn) * sqrt 5 <= 0; then
sqrt 5 + sqrt 5 / tbn <= 0 by XCMPLX_1:74; then
sqrt 5 / 2 + sqrt 5 / tbn + sqrt 5 / 2 - sqrt 5 / 2 <= 0 - sqrt 5 / 2
by XREAL_1:9; then
sqrt 5 / 2 + sqrt 5 / tbn + 1/2 <= - sqrt 5 / 2 + 1/2 by XREAL_1:6;
hence thesis by FIB_NUM:def 1,def 2;
end; then
(tau + sqrt 5 / tbn) * tbn >= tau_bar * tbn by A3,XREAL_1:65; then
(tau + sqrt 5 / tbn) * tbn >= tau_bar to_power 1 * tbn; then
tau *tbn + (sqrt 5 / tbn) * tbn >= tau_bar to_power (n+1) by Th2;
hence thesis by A3,XCMPLX_1:87;
end; then
- (tau * tau_bar to_power n + sqrt 5) <= - tau_bar to_power (n+1)
by XREAL_1:24; then
- tau * tau_bar to_power n - sqrt 5 + tau to_power (n+1) <=
- tau_bar to_power (n+1) + tau to_power (n+1) by XREAL_1:6; then
tau to_power (n+1) - tau * tau_bar to_power n - sqrt 5 <=
tau to_power (n+1) - tau_bar to_power (n+1); then
tau to_power 1 * tau to_power n - tau * tau_bar to_power n - sqrt 5 <=
tau to_power (n+1) - tau_bar to_power (n+1) by POWER:27; then
tau * tau to_power n - tau * tau_bar to_power n - sqrt 5 <=
(tau to_power (n+1) - tau_bar to_power (n+1)); then
(tau * (tau to_power n - tau_bar to_power n) - sqrt 5) / sqrt 5 <=
(tau to_power (n+1)-tau_bar to_power (n+1))/sqrt 5 by A2,XREAL_1:72; then
(tau * (tau to_power n - tau_bar to_power n))/sqrt 5 - sqrt 5 / sqrt 5 <=
(tau to_power (n+1) - tau_bar to_power (n+1))/sqrt 5 by XCMPLX_1:120; then
tau * ((tau to_power n - tau_bar to_power n)/sqrt 5) - sqrt 5 / sqrt 5 <=
(tau to_power (n+1) - tau_bar to_power (n+1))/sqrt 5 by XCMPLX_1:74; then
tau * ((tau to_power n - tau_bar to_power n) / sqrt 5) - 1 <=
(tau to_power (n+1) - tau_bar to_power (n+1)) / sqrt 5
by A2,XCMPLX_1:60; then
tau * ((tau to_power n - tau_bar to_power n) / sqrt 5) - 1 <= Fib (n+1)
by FIB_NUM:7; then
A4: tau * Fib n - 1 <= Fib (n+1) by FIB_NUM:7;
tau * Fib n - 1 + 1 > Fib (n+1)
proof
set tn = tau to_power n;
set tbn = tau_bar to_power n;
A5: tau * Fib n = tau * ((tn - tbn) / sqrt 5) by FIB_NUM:7
.= (tau * (tn - tbn)) / sqrt 5 by XCMPLX_1:74;
A6: tbn < 0 by Th7,A1;
tau * tbn < tau_bar to_power 1 * tbn by A6,XREAL_1:69; then
tau * tbn < tau_bar to_power (n+1) by Th2; then
- tau * tbn > - tau_bar to_power (n+1) by XREAL_1:24; then
- tau * tbn + tau to_power (n+1) >
- tau_bar to_power (n+1) + tau to_power (n+1) by XREAL_1:6; then
tau to_power (n+1) - tau * tbn >
tau to_power (n+1) - tau_bar to_power (n+1); then
tau to_power 1 * tn - tau * tbn >
tau to_power (n+1) - tau_bar to_power (n+1) by Th2; then
tau * tn - tau * tbn > tau to_power (n+1) - tau_bar to_power (n+1); then
(tau * (tn - tbn)) / sqrt 5 >
(tau to_power (n+1) - tau_bar to_power (n+1)) / sqrt 5 by A2,XREAL_1:74;
hence thesis by A5,FIB_NUM:7;
end;
hence thesis by A4,INT_1:def 7;
end;
theorem Th24:
for n being Nat st n >= 2 holds
Fib (n+1) = [\ (Fib n + sqrt 5 * Fib n + 1) / 2 /]
proof
let n be Nat;
assume A1: n >= 2;
A2: sqrt 5 > 0 by SQUARE_1:25;
set tn = tau to_power n;
set tb = tau_bar; set s5 = sqrt 5;
set tbn = tb to_power n;
per cases;
suppose A3: n is even; then
A4: tbn > 0 by Th6;
A5: (Fib n + sqrt 5 * Fib n + 1) / 2 >= Fib (n+1)
proof
tbn <= 1/2 by Th8,A1; then
2 * tbn <= 2 * (1/2) by XREAL_1:64; then
(2 * tbn) / tbn <= 1 / tbn by A4,XREAL_1:72; then
2 <= 1 / tbn by A4,XCMPLX_1:89; then
2 * s5 <= (1 / tbn) * s5 by A2,XREAL_1:64; then
s5 + s5 <= (1 * s5) / tbn by XCMPLX_1:74; then
s5 + s5 - s5 <= (1*s5)/tbn - s5 by XREAL_1:9; then
- s5 >= -(s5/tbn - s5) by XREAL_1:24; then
- s5 + 1 >= - s5 / tbn + s5 + 1 by XREAL_1:6; then
tau_bar >= ((s5+1)-s5/tbn)/2 by FIB_NUM:def 2,XREAL_1:72; then
tau_bar * tbn >= (tau - (s5 / tbn) / 2) * tbn
by A4,FIB_NUM:def 1,XREAL_1:64; then
tb * tbn >= (tau - (sqrt 5 / 2) / tbn) * tbn by XCMPLX_1:48; then
tb * tbn >= tau * tbn - ((s5 / 2) / tbn) * tbn; then
tb * tbn >= tau * tbn - (s5 / 2) by A4,XCMPLX_1:87; then
tb to_power 1 * tbn >= tau * tbn - (s5/2); then
tb to_power (n+1) >= tau * tbn - (s5/2) by Th2; then
- tb to_power (n+1) <= -(tau*tbn - (s5/2)) by XREAL_1:24; then
- tb to_power (n+1) + tau to_power (n+1) <=
- tau * tbn + (sqrt 5/2) + tau to_power (n+1) by XREAL_1:6; then
-tb to_power (n+1) + tau to_power (n+1) <=
tau to_power (n+1) - tau * tbn + (s5/2); then
- tb to_power (n+1) + tau to_power (n+1) <=
tn*tau to_power 1-tau * tbn+(s5/2) by Th2; then
- tb to_power (n+1) + tau to_power (n+1) <=
tn * tau - tau * tbn + (s5/2); then
(tau to_power (n+1)-tau_bar to_power (n+1))/sqrt 5 <=
(tau*(tn - tbn) + (s5/2))/s5 by A2,XREAL_1:72; then
Fib (n+1) <= (tau * (tn - tbn) + (s5/2)) / s5 by FIB_NUM:7; then
Fib (n+1) <= (tau * (tn - tbn))/s5 + (s5/2)/s5 by XCMPLX_1:62; then
Fib (n+1) <= tau * ((tn - tbn)/s5) + (s5/2)/s5 by XCMPLX_1:74; then
Fib (n+1) <= tau * Fib n + (s5 / 2) / sqrt 5 by FIB_NUM:7; then
Fib (n+1) <= tau * Fib n + (s5 / s5) / 2 by XCMPLX_1:48; then
Fib (n+1) <= tau * Fib n + 1 / 2 by A2,XCMPLX_1:60;
hence thesis by FIB_NUM:def 1;
end;
(Fib n + s5 * Fib n + 1) / 2 - 1 < Fib (n+1)
proof
Fib (n+1) = [\ tau * Fib n + 1 /] by A1,A3,Th22; then
A6: tau * Fib n + 1 - 1 < Fib (n+1) by INT_1:def 6;
(Fib n+s5*Fib n+1) <= (Fib n+s5 * Fib n + 2) by XREAL_1:6; then
(Fib n+s5*Fib n+1)/2 <= (Fib n+s5*Fib n+2)/2 by XREAL_1:72;then
(Fib n+s5 * Fib n + 1)/2-1 <= tau * Fib n + 1 - 1
by FIB_NUM:def 1,XREAL_1:9;
hence thesis by A6,XXREAL_0:2;
end;
hence thesis by A5,INT_1:def 6;
end;
suppose A7: n is odd;
A8: (Fib n + sqrt 5 * Fib n + 1) / 2 >= Fib (n+1)
proof
Fib (n+1) = [/ tau * Fib n - 1 \] by A1,A7,Th23; then
A9: tau * Fib n - 1 + 1 > Fib (n+1) by INT_1:def 7;
1 + (Fib n+sqrt 5*Fib n) > 0 + (Fib n+sqrt 5*Fib n) by XREAL_1:6; then
(Fib n+sqrt 5 * Fib n + 1)/2 > (Fib n+sqrt 5 * Fib n)/2 by XREAL_1:74;
hence thesis by A9,FIB_NUM:def 1,XXREAL_0:2;
end;
(Fib n + (sqrt 5) * Fib n + 1) / 2 - 1 < Fib (n+1)
proof
n > 1 by A1,XXREAL_0:2; then
(2 * sqrt 5) * tbn > (2 * sqrt 5) * (-1/2) by A2,Th14,XREAL_1:68; then
- (2 * sqrt 5) * tbn < - (2 * sqrt 5) * (-1/2) by XREAL_1:24; then
1*tn +sqrt 5*tn - 2*tau*tn + 2*tb*tbn - sqrt 5*tbn - 1*tbn + 2*tau*tn <
sqrt 5 + 2 * tau * tn by FIB_NUM:def 1,def 2,XREAL_1:6; then
tn + sqrt 5 * tn + 2 * tb * tbn - sqrt 5 * tbn - tbn - 2 * tb * tbn <
sqrt 5 + 2 * tau * tn - 2 * tb * tbn by XREAL_1:9; then
((1+sqrt 5) * (tn-tbn)) /sqrt 5 < (sqrt 5 + 2*tau*tn - 2*tb*tbn)/sqrt 5
by A2,XREAL_1:74; then
(1 + sqrt 5) * ((tn - tbn) / sqrt 5) <
(sqrt 5 + 2 * (tau * tn) - 2 * tb * tbn) / sqrt 5 by XCMPLX_1:74; then
(1 + sqrt 5) * Fib n < (sqrt 5 + 2 * (tau*tn) - 2 * tb * tbn) / sqrt 5
by FIB_NUM:7; then
(1 + sqrt 5) * Fib n <
(sqrt 5 + 2 * (tau to_power 1*tn) - 2*tb*tbn) /sqrt 5; then
(1 + sqrt 5) * Fib n <
(sqrt 5 + 2*tau to_power (n+1) - 2*(tb*tbn))/sqrt 5 by Th2; then
(1+sqrt 5) * Fib n < (sqrt 5 + 2 * tau to_power (n+1) -
2 * (tb to_power 1 * tbn)) / sqrt 5; then
(1 + sqrt 5) * Fib n < (sqrt 5 + 2 * tau to_power (n+1) -
2 * tb to_power (n+1)) / sqrt 5 by Th2; then
(1 + sqrt 5) * Fib n <
(sqrt 5 + 2 * (tau to_power (n+1) - tb to_power (n+1))) / sqrt 5; then
(1+sqrt 5) * Fib n < sqrt 5 / sqrt 5 + (2 * (tau to_power (n+1) -
tb to_power (n+1))) / sqrt 5 by XCMPLX_1:62; then
(1 + sqrt 5) * Fib n < sqrt 5 / sqrt 5 + 2 * ((tau to_power (n+1) -
tb to_power (n+1)) / sqrt 5) by XCMPLX_1:74; then
(1+sqrt 5) * Fib n < sqrt 5 / sqrt 5 + 2 * Fib (n+1) by FIB_NUM:7; then
(1 + sqrt 5) * Fib n < 1 + 2 * Fib (n+1) by A2,XCMPLX_1:60; then
((1 +sqrt 5) * Fib n) / 2 < (1 + 2 * Fib (n+1)) / 2 by XREAL_1:74; then
((1+sqrt 5) * Fib n) / 2 -1/2 < 1/2 + Fib (n+1) - 1/2 by XREAL_1:9;
hence thesis;
end;
hence thesis by A8,INT_1:def 6;
end;
end;
theorem
for n being Nat st n >= 2 holds
Fib (n+1) = [/ (Fib n + sqrt 5 * Fib n - 1)/2 \]
proof
let n be Nat;
assume A1: n >= 2;
then Fib (n+1) = [\ (Fib n + sqrt 5 * Fib n + 1) / 2 /] by Th24; then
A2: (Fib n + sqrt 5 * Fib n + 1)/2 - 1 < Fib (n+1) by INT_1:def 6;
(Fib n + sqrt 5 * Fib n - 1)/2 + 1 > Fib (n+1)
proof
Fib (n+1) = [\ (Fib n + sqrt 5 * Fib n + 1) / 2 /] by Th24,A1; then
A3: (Fib n + sqrt 5 * Fib n - 1)/2 + 1 >= Fib (n+1) by INT_1:def 6;
(Fib n + sqrt 5 * Fib n - 1)/2 + 1 <> Fib (n+1)
proof
set tn = tau to_power n;
set tbn = tau_bar to_power n;
set t1 = tau to_power (n+1);
set t2 = tau_bar to_power (n+1);
set s5 = sqrt 5;
A4: s5 > 0 by SQUARE_1:25;
assume (Fib n + s5 * Fib n - 1)/2 + 1 = Fib (n+1); then
Fib n * (1 + s5) + 1 = 2 * Fib (n+1); then
((tn - tbn)/s5) * (1+s5) + 1 = 2 * Fib (n+1) by FIB_NUM:7; then
((((tn - tbn)/s5) * (1+s5)) + 1) * s5 =
(2 * ((t1-t2)/s5))*s5 by FIB_NUM:7; then
((tn - tbn) / s5 * (1+s5)) * s5 + 1 * s5 = 2*(((t1-t2)/s5)*s5); then
((tn - tbn) / s5 * (1+s5)) * s5 + s5 =
2 * (t1-t2) by A4,XCMPLX_1:87; then
(((tn-tbn)*(1+s5))/s5)*s5+s5 = 2 * t1 - 2 * t2 by XCMPLX_1:74; then
(tn - tbn) * (1 + s5) + s5 = 2 * t1 - 2 * t2 by A4,XCMPLX_1:87; then
tn*(1+s5)-(tbn+tbn*s5)+s5=2*(tn*tau to_power 1)
- 2 * t2 by Th2; then
tn*(1+s5)-tbn*(1+s5)+s5= 2*(tn*tau to_power 1)
-2*(tbn*tau_bar to_power 1) by Th2;then
tn*(1+s5)-tbn*(1+s5) + s5 = 2 * (tn * tau) -
2 * (tbn * tau_bar to_power 1); then
(tn - tbn) * (1+s5) + s5 = 2 * (tn * tau) -
2 * (tbn * tau_bar); then
tn*(1+s5 - 2*tau) + tbn* (2*tau_bar - (1+s5))+s5 = 0; then
(-2 * tbn + 1)*sqrt 5 = 0 by FIB_NUM:def 1,def 2; then
-2 * tbn + 1 = 0 by A4;
hence contradiction by Th8,A1;
end;
hence thesis by A3,XXREAL_0:1;
end;
hence thesis by A2,INT_1:def 7;
end;
theorem
for n being Nat holds
Fib (n+1) = (Fib n + sqrt(5*(Fib n)^2 + 4*(-1) to_power n))/2
proof
let n be Nat;
A1: n - 0 is Element of NAT by NAT_1:21;
A2: 2 * Fib (n+1) = Fib n + Lucas n by FIB_NUM3:24;
A3: (Lucas n)^2 - 5*(Fib n)^2 = (Lucas n) to_power 2 - 5*(Fib n)^2 by POWER:46
.= (Lucas n) to_power 2 - 5 * (Fib n) to_power 2 by POWER:46
.= - (5 * (Fib n) |^2 - (Lucas n) |^2)
.= - (4 * (-1) to_power (n+1)) by A1,FIB_NUM3:30
.= (-1) * ((-1) to_power (n+1) * 4)
.= (-1) to_power 1 * ((-1) to_power (n+1) * 4)
.= ((-1) to_power 1 * (-1) to_power (n+1)) * 4
.= (-1) to_power (n + 1 + 1) * 4 by Th2
.= (-1) to_power (n + 2) * 4
.= (-1) to_power n * (-1) to_power 2 * 4 by Th2
.= (-1) to_power n * 1 * 4 by FIB_NUM2:3,POLYFORM:5;
Fib (n+1) = (Fib n + Lucas n) / 2 by A2;
hence thesis by A3,SQUARE_1:def 2;
end;
theorem
for n being Nat st n >= 2 holds
Fib (n+1) = [\ (Fib(n) + 1 + sqrt(5*(Fib(n))^2 - 2 * Fib(n) + 1) )/2 /]
proof
let n be Nat;
assume A1: n >= 2;
A2: n - 0 is Element of NAT by NAT_1:21;
A3: n - 1 >= 2 - 1 by A1,XREAL_1:9;
(n + 1 -' 1) + 1 = (n + 1 - 1) + 1 by NAT_D:37
.= (n - 1 + 1) + 1
.= (n -' 1 + 1) + 1 by A3,NAT_D:39;
then A4: Fib (n+1) = Fib (((n-'1)+1)+1) by NAT_D:34
.= Fib (n-'1) + Fib (n-'1+1) by PRE_FF:1
.= Fib (n-'1) + Fib (n+1-'1) by A1,NAT_D:38,XXREAL_0:2
.= Fib (n -' 1) + Fib (n) by NAT_D:34;
n + 2 >= 2 + 2 by A1,XREAL_1:6; then
reconsider p = n + 2 - 1 as Nat by NAT_1:21,XXREAL_0:2;
A5: Lucas (n) - Fib(n) = Lucas (n+1-'1) - Fib (n) by NAT_D:34
.= Lucas (n-'1+1) - Fib n by A1,NAT_D:38,XXREAL_0:2
.= Fib(n-'1) + Fib((n-'1)+2) - Fib(n) by FIB_NUM3:20
.= Fib (n-'1) + Fib (n+2-'1) - Fib (n) by A1,NAT_D:38,XXREAL_0:2
.= Fib (n-'1) + Fib p - Fib (n) by NAT_D:37
.= 2 * Fib (n-'1) by A4;
A6: (Lucas (n))^2 - 5 * (Fib n) ^2 =
(Lucas (n))^2 - 5 * (Fib n) to_power 2 by POWER:46
.= (Lucas n) to_power 2 - 5 * (Fib n) |^2 by POWER:46
.= (-1) * (5 * (Fib (n)) |^2 - (Lucas (n)) |^2)
.= (-1) * (4 * (-1) to_power (n+1)) by A2,FIB_NUM3:30
.= 4 * ((-1) * (-1) to_power (n+1))
.= 4 * ((-1) to_power 1 * (-1) to_power (n+1))
.= 4 * (-1) to_power (1+(n+1)) by Th2
.= 4 * (-1) to_power (n+2)
.= 4 * ((-1) to_power n * (-1) to_power 2) by Th2
.= 4 * ((-1) to_power n * (-1) ^2) by POWER:46
.= 4 * (-1) to_power n;
n -' 1 >= 2 -'1 & 2-1>= 1 by A1,NAT_D:42; then
n -'1 >= 2-1 by NAT_D:39; then
A7: Fib (n-'1) >= 1 by FIB_NUM2:45,PRE_FF:1;
1 >= (-1) to_power n
proof
per cases;
suppose n is even;
hence thesis by FIB_NUM2:3;
end;
suppose n is odd;
hence thesis by FIB_NUM2:2;
end;
end; then
(-1) to_power n <= Fib (n-'1) by A7,XXREAL_0:2; then
(Lucas n)^2 - 5 * (Fib n)^2 <= 2 * 2 * Fib (n-'1) by A6,XREAL_1:64; then
(Lucas n)^2 - 5 * (Fib n)^2 - 2 * Lucas (n) <=
2 * Lucas (n) - 2 * Fib (n) - 2 * Lucas (n)
by A5,XREAL_1:9; then
(Lucas n)^2 - 5 * (Fib n)^2 - 2 * Lucas (n) + 1 <= - 2 * Fib (n) + 1
by XREAL_1:6; then
A8: (Lucas n)^2 - 5 * (Fib n)^2 - 2 * Lucas (n) + 1 + 5 * (Fib n)^2 <=
- 2 * Fib (n) + 1 + 5 * (Fib n)^2 by XREAL_1:6;
A9: n + 2 -' 1 = n + 2 - 1 by NAT_D:37 .= n + 1;
A10: Lucas n = Lucas (n+1-'1) by NAT_D:34
.= Lucas (n -' 1 + 1) by A1,NAT_D:38,XXREAL_0:2
.= Fib (n -' 1) + Fib ((n -' 1) + 2) by FIB_NUM3:20
.= Fib (n -' 1) + Fib (n + 2 -' 1) by A1,NAT_D:38,XXREAL_0:2
.= 2 * Fib (n + 1) - Fib n by A4,A9;
A11: 2 * Fib (n-'1) >= 2 * 0;
n >= 1 by A1,XXREAL_0:2; then
A12: Fib n >= 1 by FIB_NUM2:45,PRE_FF:1; then
-Fib n <= -1 by XREAL_1:24; then
-Fib n + 1 <= -1 + 1 by XREAL_1:6; then
2 * Fib (n -'1) + Fib n >= - Fib n + 1 + Fib n by A11,XREAL_1:6; then
A13: 2 * Fib (n-'1) + Fib n - 1 >= 1 - 1 by XREAL_1:9;
sqrt ((2 * Fib (n+1) - Fib n - 1) ^2) <= sqrt (5*(Fib n)^2 - 2 * Fib n + 1)
by A10,A8,SQUARE_1:26; then
2 * Fib (n+1) - Fib n - 1 <= sqrt (5*(Fib n) ^2 - 2 * Fib n + 1)
by A4,A13,SQUARE_1:22; then
2 * Fib (n+1) - Fib n - 1 + Fib n <=
sqrt (5 * (Fib n) ^2 - 2 * Fib n + 1) + Fib n by XREAL_1:6; then
2 * Fib (n+1) - Fib n - 1 + Fib n + 1 <=
sqrt (5*(Fib n) ^2 - 2 * Fib n + 1) + Fib n + 1 by XREAL_1:6; then
A14: (2 * Fib (n+1)) / 2 <=
(sqrt (5*(Fib n) ^2 - 2 * Fib n + 1) + Fib n + 1) / 2 by XREAL_1:72;
A15: 5 * (Fib n) ^2 - 2 * Fib n = (5 * Fib n - 2) * Fib n;
5 * Fib n >= 5 * 1 by A12,XREAL_1:64; then
5 * Fib n - 2 >= 5 - 2 by XREAL_1:9; then
A16: 5 * Fib n - 2 >= 0 by XXREAL_0:2;
A17: Fib (n+1) + Fib (n+1) - Fib n + 1 = Fib (n+1) + Fib (n-'1) + 1 by A4;
(Lucas n) ^2 - 5*(Fib n) ^2 > -2 * (Lucas n + Fib n)
proof
A18: Fib n > 0 by A1,FIB_NUM2:21,45;
Lucas n >= n by FIB_NUM3:17; then
Lucas n >= 2 by A1,XXREAL_0:2; then
Lucas n + Fib n > 0 + 2 by A18,XREAL_1:8; then
(Lucas n + Fib n) * 2 > 2 * 2 by XREAL_1:68; then
A19: -(Lucas n + Fib n) * 2 < -4 by XREAL_1:24;
-4 <= 4 * (-1) to_power n by Lm1;
hence thesis by A6,A19,XXREAL_0:2;
end; then
(Lucas n) ^2 - 5*(Fib n) ^2 + 2 * Lucas (n) >
-2 * (Lucas n + Fib n) + 2 * Lucas (n) by XREAL_1:6; then
(Lucas n) ^2 - 5 * (Fib n) ^2 + 2 * Lucas n + 5 * (Fib n) ^2 >
-2 * Fib n + 5 * (Fib n) ^2 by XREAL_1:6; then
(Lucas n) ^2 + 2* Lucas (n) * 1 + 1 ^2 > -2 * Fib n + 5 * (Fib n) ^2 + 1 ^2
by XREAL_1:6; then
sqrt((2 * Fib (n+1)- Fib n + 1) ^2) > sqrt(-2 * Fib n + 5*(Fib n) ^2 + 1)
by A16,A15,A10,SQUARE_1:27; then
2*Fib (n+1)-Fib n+1 > sqrt(-2*Fib n+5*(Fib n)^2+1) by A17,SQUARE_1:22;
then
2*Fib (n+1)-Fib n+1-1 > sqrt(-2*Fib n+5*(Fib n)^2+1)-1 by XREAL_1:9; then
2 * Fib (n+1) - Fib n + Fib n >
sqrt(-2 * Fib n + 5 * (Fib n) ^2 + 1) - 1 + Fib n by XREAL_1:6; then
(2 * Fib (n+1) ) / 2 >
(sqrt(-2 * Fib n + 5*(Fib n)^2 + 1) - 1 + Fib n) / 2 by XREAL_1:74; then
(Fib n + 1 + sqrt (5*(Fib(n)) ^2 - 2 * Fib n + 1)) / 2 - 1 < Fib (n+1);
hence thesis by A14,INT_1:def 6;
end;
Lm20: sqrt 5 > 0 by SQUARE_1:25;
Lm21: sqrt 5 / ((sqrt 5 - 5) * tau) = sqrt 5 / ((sqrt 5 - (sqrt 5) ^2) * tau)
by SQUARE_1:def 2
.= sqrt 5 / (sqrt 5 * ((1 - sqrt 5) * tau))
.= sqrt 5 / sqrt 5 / ((1 - sqrt 5) * tau) by XCMPLX_1:78
.= 1 / (((1 - sqrt 5) * (1+sqrt 5)) /2) by Lm20,FIB_NUM:def 1,XCMPLX_1:60
.= (1 * 2) / ((1 - sqrt 5) * (1 + sqrt 5)) by XCMPLX_1:77
.= 2 / (1 ^2 - (sqrt 5) ^2)
.= 2 / (1 ^2 - 5) by SQUARE_1:def 2
.= -1/2;
theorem
for n being Nat st n >= 2 holds
Fib n = [\ (1/tau) * (Fib (n+1) + 1/2)/]
proof
let n be Nat;
assume A1: n >= 2; then
A2: n > 1 by XXREAL_0:2;
set tbn = tau_bar to_power n;
sqrt 5 < sqrt (5 ^2) by SQUARE_1:27; then
sqrt 5 < 5 by SQUARE_1:def 2; then
A3: sqrt 5 - 5 < 5 - 5 by XREAL_1:9;
A4: (1 / tau) * (Fib (n+1) + 1/2) >= Fib n
proof
set tbm = tau_bar to_power (n+1);
set tn = tau to_power n;
tbm / tau - sqrt 5 / (2 * tau) <= tbn
proof
per cases;
suppose A5: n is even;
sqrt 5 / ((sqrt 5 - 5) * tau) <= tbn by Lm21,A2,Th14; then
(sqrt 5 / ((sqrt 5 - 5) * tau)) * ((sqrt 5 - 5) * tau) >=
tbn * ((sqrt 5 - 5) * tau) by A3,XREAL_1:65; then
A6: sqrt 5 >= tbn * ((sqrt 5 - 5) * tau) by A3,XCMPLX_1:87;
A7: tbn > 0 by Th6,A5; then
sqrt 5 / tbn >= (tau *(sqrt 5 - 5)*tbn) / tbn by A6,XREAL_1:72; then
sqrt 5 / tbn >= tau * (sqrt 5 - 5) by A7,XCMPLX_1:89; then
(sqrt 5/tbn) / tau >= ((sqrt 5 - 5)*tau) / tau by XREAL_1:72; then
(sqrt 5 / tbn) / tau >= sqrt 5 - 5 by XCMPLX_1:89; then
sqrt 5 / (tbn * tau) >= sqrt 5 - 5 by XCMPLX_1:78; then
sqrt 5 /(tbn*tau)+(-sqrt 5+5)>=sqrt 5-5+(-sqrt 5+5) by XREAL_1:6;then
- (sqrt 5 / (tbn * tau) - sqrt 5 + 5) <= 0; then
- (sqrt 5 / (tbn*tau)) + sqrt 5 - 5 + 2 <= 0 + 2 by XREAL_1:6; then
(- sqrt 5/(tbn*tau) + (sqrt 5 - 3)) / 2 <= 2 / 2 by XREAL_1:72; then
- sqrt 5 / (tbn * tau) / 2 + tau_bar / tau <= 1 by Lm4; then
- sqrt 5 / (tbn * tau * 2) + tau_bar / tau <= 1 by XCMPLX_1:78; then
(tau_bar/tau-sqrt 5/(2*tbn*tau))*tbn <= 1*tbn by A7,XREAL_1:64; then
(tau_bar/tau) * tbn - (sqrt 5/(2*tbn*tau)) * tbn <= tbn; then
(tau_bar*tbn)/tau-(sqrt 5/(2*tbn*tau))*tbn <= tbn by XCMPLX_1:74;then
(tau_bar to_power 1 * tbn) / tau - (sqrt 5/(2*tbn*tau)) * tbn <= tbn;
then
tau_bar to_power (n+1) / tau - (sqrt 5 / ((2*tau)*tbn)) * tbn <= tbn
by Th2; then
tau_bar to_power (n+1) / tau - ((sqrt 5/(2*tau))/tbn) * tbn <= tbn
by XCMPLX_1:78;
hence thesis by A7,XCMPLX_1:87;
end;
suppose n is odd; then
A8: tbn < 0 by Th7;
sqrt 5 / (tau * (sqrt 5-5)) <= tbn by Lm21,A2,Th14; then
(sqrt 5 / (tau * (sqrt 5-5))) * (sqrt 5 - 5) >= tbn * (sqrt 5 - 5)
by A3,XREAL_1:65; then
(sqrt 5 / tau / (sqrt 5-5)) * (sqrt 5 - 5) >= tbn * (sqrt 5 - 5)
by XCMPLX_1:78; then
(sqrt 5/ tau) >= tbn * (sqrt 5 - 5) by A3,XCMPLX_1:87; then
(sqrt 5/ tau)/tbn <= (tbn * (sqrt 5 - 5))/tbn by A8,XREAL_1:73; then
sqrt 5 / (tau * tbn) <= (tbn * (sqrt 5 - 5))/tbn by XCMPLX_1:78; then
sqrt 5 / (tau * tbn) <= sqrt 5 - 5 by A8,XCMPLX_1:89; then
- (sqrt 5 / (tau * tbn)) >= -(sqrt 5 - 5) by XREAL_1:24; then
- (sqrt 5 / (tau * tbn)) + (sqrt 5-3)>= - sqrt 5 + 5 + (sqrt 5-3)
by XREAL_1:6; then
(-(sqrt 5 / (tau * tbn)) + (sqrt 5-3)) /2 >= 2 /2 by XREAL_1:72; then
tau_bar /tau - (sqrt 5 / (tau * tbn)) / 2 >= 1 by Lm4; then
tau_bar /tau - (sqrt 5 / (tau * tbn*2)) >= 1 by XCMPLX_1:78; then
(tau_bar/tau-sqrt 5/(tau*tbn*2))*tbn <= 1*tbn by A8,XREAL_1:65; then
(tau_bar/tau)*tbn - (sqrt 5/(tau*2*tbn))*tbn <= tbn; then
(tau_bar/tau)*tbn-(sqrt 5/(tau*2)/tbn)*tbn <= tbn by XCMPLX_1:78;then
(tau_bar /tau)*tbn - sqrt 5 / (tau*2) <= tbn by A8,XCMPLX_1:87; then
tau_bar * tbn/tau - sqrt 5 / (tau * 2) <= tbn by XCMPLX_1:74; then
tau_bar to_power 1 * tbn/tau - sqrt 5 / (tau * 2) <= tbn;
hence thesis by Th2;
end;
end; then
- (tbm / tau - (sqrt 5 / (2 * tau))) >= - tbn by XREAL_1:24; then
- tbm/tau + sqrt 5/(2*tau) + (tn*tau)/tau >= - tbn + (tn*tau)/tau
by XREAL_1:6; then
(tn*tau)/tau - tbm/tau + sqrt 5/(2*tau) >= -tbn + (tn*tau)/tau; then
(tn*tau-tbm)/tau+sqrt 5/(2*tau) >= -tbn+(tn*tau)/tau by XCMPLX_1:120;then
(tn*tau - tbm)/tau + sqrt 5/(2*tau) >= -tbn + tn by XCMPLX_1:89; then
(tn*tau to_power 1-tbm)/tau + sqrt 5/(2*tau) >= tn-tbn; then
(tau to_power (n+1) - tbm) / tau + sqrt 5 / (2 * tau) >= tn - tbn
by Th2; then
((tau to_power (n+1) - tbm) / tau + sqrt 5 / (2 * tau)) / sqrt 5 >=
(tn - tbn) / sqrt 5 by Lm20,XREAL_1:72; then
((tau to_power (n+1) - tbm) /tau + sqrt 5 /(2*tau)) /sqrt 5 >= Fib n
by FIB_NUM:7; then
((tau to_power (n+1) - tbm) /tau) /sqrt 5 + (sqrt 5 /(2*tau)) /sqrt 5 >=
Fib n by XCMPLX_1:62; then
((tau to_power (n+1) - tbm)/sqrt 5) /tau + (sqrt 5/(2*tau)) /sqrt 5 >=
Fib n by XCMPLX_1:48; then
Fib (n+1)/tau + (sqrt 5/(2*tau))/sqrt 5 >= Fib n by FIB_NUM:7; then
Fib (n+1)/tau + 1/(2*tau)*(sqrt 5/sqrt 5) >= Fib n by XCMPLX_1:104; then
Fib (n+1)/tau + 1/(2*tau) * 1 >= Fib n by Lm20,XCMPLX_1:60; then
Fib (n+1) / tau + (1/2) / tau >= Fib n by XCMPLX_1:78; then
(Fib (n+1) + 1/2) / tau >= Fib n by XCMPLX_1:62;
hence thesis by XCMPLX_1:99;
end;
(1/tau) * (Fib (n+1) + 1/2) - 1 < Fib n
proof
1 < sqrt 5 by SQUARE_1:18,27; then
1 / 2 < sqrt 5 / 2 by XREAL_1:74; then
tbn < sqrt 5 / 2 by Th8,A1,XXREAL_0:2; then
tbn * sqrt 5 < (tau - 1/2) * sqrt 5 by Lm20,FIB_NUM:def 1,XREAL_1:68;
then
tbn * tau - tbn * tau_bar < tau * sqrt 5 - ((1*sqrt 5) / 2)
by FIB_NUM:def 1,def 2; then
tbn*tau-tbn*tau_bar to_power 1 < tau*sqrt 5-(sqrt 5/2); then
tbn*tau-tau_bar to_power (n+1) < tau*sqrt 5-(sqrt 5/2) by Th2;then
tbn * tau - tau_bar to_power (n+1) + sqrt 5 /2 <
tau * sqrt 5 - (sqrt 5/2) + sqrt 5/2 by XREAL_1:6; then
tbn * tau - tau_bar to_power (n+1) + sqrt 5 / 2 - tbn * tau <
tau * sqrt 5 - tbn * tau by XREAL_1:9; then
- tau_bar to_power (n+1) + sqrt 5 /2 - tau * sqrt 5 <
tau * sqrt 5 - tbn * tau - tau * sqrt 5 by XREAL_1:9; then
(- tau_bar to_power (n+1) + (sqrt 5 / 2) - (tau * sqrt 5)) / tau <
(- tbn * tau) / tau by XREAL_1:74; then
(-tau_bar to_power (n+1))/tau + (sqrt 5/2)/tau - (tau*sqrt 5)/tau <
(-tbn * tau) / tau by XCMPLX_1:124; then
-tau_bar to_power (n+1)/tau + (sqrt 5/2)/tau - tau*sqrt 5/tau <
((-tbn) * tau) / tau by XCMPLX_1:187; then
- tau_bar to_power (n+1) /tau + (sqrt 5/2) /tau - tau*sqrt 5 /tau < -tbn
by XCMPLX_1:89; then
- tau_bar to_power (n+1) /tau + (sqrt 5/2) /tau - sqrt 5 < -tbn
by XCMPLX_1:89; then
- tau_bar to_power (n+1)/tau+(sqrt 5/2)/tau- sqrt 5+ tau to_power n * 1 <
- tbn + tau to_power n by XREAL_1:6; then
(-tau_bar to_power (n+1)/tau + (sqrt 5/2)/tau-sqrt 5+tau to_power n*1)/
sqrt 5 < (tau to_power n - tbn)/sqrt 5 by Lm20,XREAL_1:74; then
( -tau_bar to_power (n+1)/tau + (sqrt 5/2)/tau - sqrt 5 +
tau to_power n * 1)/sqrt 5 < Fib n by FIB_NUM:7; then
( -tau_bar to_power (n+1)/tau + (sqrt 5/2)/tau - sqrt 5 +
tau to_power n * (tau/tau))/sqrt 5 < Fib n by XCMPLX_1:60; then
( -tau_bar to_power (n+1)/tau + (sqrt 5/2)/tau +
tau to_power n * (tau/tau) - sqrt 5)/sqrt 5 < Fib n; then
( -tau_bar to_power (n+1)/tau + (sqrt 5/2)/tau +
(tau to_power n * tau)/tau - sqrt 5)/sqrt 5 < Fib n
by XCMPLX_1:74; then
( -tau_bar to_power (n+1)/tau + (sqrt 5/2)/tau +
(tau to_power n * tau)/tau)/sqrt 5 - sqrt 5/sqrt 5 < Fib n
by XCMPLX_1:120; then
( -tau_bar to_power (n+1)/tau + (sqrt 5/2)/tau +
(tau to_power n * tau)/tau)/sqrt 5 - 1 < Fib n by Lm20,XCMPLX_1:60; then
(( -tau_bar to_power (n+1))/tau + (sqrt 5/2)/tau +
(tau to_power n * tau)/tau)/sqrt 5 - 1 < Fib n by XCMPLX_1:187; then
((-tau_bar to_power (n+1) + (sqrt 5/2) +
(tau to_power n * tau))/tau)/sqrt 5 - 1 < Fib n by XCMPLX_1:63; then
((-tau_bar to_power (n+1) + (sqrt 5/2) +
(tau to_power n * tau))/sqrt 5)/tau - 1 < Fib n by XCMPLX_1:48; then
((-tau_bar to_power (n+1) + (tau to_power n * tau) +
sqrt 5/2)/sqrt 5)*(1/tau) - 1 < Fib n by XCMPLX_1:99; then
((-tau_bar to_power (n+1) + (tau to_power n * tau))/sqrt 5 +
(sqrt 5/2)/sqrt 5)*(1/tau) - 1 < Fib n by XCMPLX_1:62; then
((-tau_bar to_power (n+1) + (tau to_power n * tau to_power 1))/sqrt 5 +
(sqrt 5/2)/sqrt 5)*(1/tau) - 1 < Fib n; then
(( -tau_bar to_power (n+1)+ tau to_power (n+1))/sqrt 5 +
(sqrt 5/2)/sqrt 5)*(1/tau) - 1 < Fib n by Th2; then
((tau to_power (n+1) -tau_bar to_power (n+1))/sqrt 5 +
(sqrt 5/2)/sqrt 5)*(1/tau) - 1 < Fib n; then
(Fib (n+1) + (sqrt 5/2)/sqrt 5)*(1/tau) - 1 < Fib n by FIB_NUM:7; then
(Fib (n+1) + (sqrt 5/sqrt 5)/2)*(1/tau) - 1 < Fib n by XCMPLX_1:48;
hence thesis by Lm20,XCMPLX_1:60;
end;
hence thesis by A4,INT_1:def 6;
end;
Lm22: sqrt 5 > 1 by SQUARE_1:18,27; then
Lm23: sqrt 5 - 1 > 1 - 1 & sqrt 5 > 0 by XREAL_1:9;
sqrt 5 > 2 by SQUARE_1:20,27; then
- sqrt 5 < -2 by XREAL_1:24; then
- sqrt 5 + 5 < - 2 + 5 by XREAL_1:6; then
- sqrt 5 + (sqrt 5) ^2 < 3 by SQUARE_1:def 2; then
(sqrt 5 * (sqrt 5 - 1)) / 5 < 3 / 5 by XREAL_1:74; then
(sqrt 5 - 1) * (sqrt 5 / 5) < 6 / 10; then
(sqrt 5-1)*(sqrt 5/(sqrt 5)^2) < 6/10 by SQUARE_1:def 2; then
(sqrt 5-1)*((1*sqrt 5)/(sqrt 5*sqrt 5)) < 6/10 & sqrt 5 > 0
by SQUARE_1:25; then
(sqrt 5 - 1) * (1 / sqrt 5) < 6 / 10 by XCMPLX_1:91; then
Lm24: (sqrt 5 - 1) / sqrt 5 < 6 / 10 by XCMPLX_1:99;
sqrt ((3/2) ^2) <= sqrt 5 by SQUARE_1:26; then
3 / 2 <= sqrt 5 by SQUARE_1:def 2; then
(3 / 2) * 2 <= sqrt 5 * 2 by XREAL_1:64; then
Lm25: 3/4 <= (2 * sqrt 5) / (2 * 2) by XREAL_1:72;
Lm26: sqrt 5 - 1 > 1 - 1 & sqrt 5 > 0 by Lm22,XREAL_1:9;
-1+sqrt 5 < 0+sqrt 5 & sqrt 5 > 0 by SQUARE_1:25,XREAL_1:6; then
(sqrt 5 - 1) / sqrt 5 < sqrt 5 / sqrt 5 & sqrt 5 > 0 by XREAL_1:74; then
Lm27: (sqrt 5 - 1) / sqrt 5 < 1 by XCMPLX_1:60;
sqrt 5 < sqrt (3 ^2) by SQUARE_1:27; then
sqrt 5 < 3 by SQUARE_1:def 2; then
- sqrt 5 > - 3 by XREAL_1:24; then
Lm28: - sqrt 5 + 3 > -3 + 3 by XREAL_1:6;
- sqrt 5 < - 1 by Lm22,XREAL_1:24; then
- sqrt 5 + 3 < - 1 + 3 by XREAL_1:6; then
Lm29: (3 - sqrt 5) / 2 < 2 / 2 by XREAL_1:74;
theorem
for n,k being Nat st (n >= k & k > 1) or (k = 1 & n > k) holds
[\ tau to_power k * Fib n + 1/2 /] = Fib (n + k)
proof
let n,k be Nat;
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);
A2: tk * Fib n = tk * ((tn - tbn) / sqrt 5) by FIB_NUM:7
.= (tk * (tn - tbn)) / sqrt 5 by XCMPLX_1:74
.= ((tk * tn - tbs) + (tbs - tk * tbn)) / sqrt 5
.= ((ts - tbs) + (tbs - tk * tbn)) / sqrt 5 by Th2
.= (ts - tbs) / sqrt 5 + (tbs - tk * tbn) / sqrt 5 by XCMPLX_1:62
.= Fib (n+k) + (tbs - tk * tbn) / sqrt 5 by FIB_NUM:7
.= Fib (n+k) + (tbn * tbk - tk * tbn) / sqrt 5 by Th2
.= Fib (n+k) + (( - tbn) * (tk - tbk)) / sqrt 5
.= Fib (n+k) + (- tbn) * ((tk - tbk) / sqrt 5) by XCMPLX_1:74
.= Fib (n+k) + (- tbn) * Fib k by FIB_NUM:7
.= Fib (n+k) - tbn * Fib k;
A3: tk * Fib n + 1/2 >= Fib (n+k)
proof
tbn * Fib k <= 1/2
proof
per cases;
suppose A4: n is even;
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;
tbm * ((-1) to_power k - tb to_power (2*k)) <= sqrt 5 / 2
proof
per cases;
suppose A7: k is even;
tb to_power (2*k) > 0 by Th6; then
A8: - tb to_power (2*k) + 1 < 0 + 1 by XREAL_1:6;
tb to_power (2*k) < 1 by Th8,A1,XXREAL_0:2; then
- tb to_power (2*k) > - 1 by XREAL_1:24; then
A9: - tb to_power (2*k) + 1 > - 1 + 1 by XREAL_1:6;
m is even by A4,A5,A7; then
A10: tbm > 0 by Th6;
tbm <= sqrt 5 / 2
proof
A11: sqrt 5 > 2 by SQUARE_1:20,27;
per cases;
suppose A12: m = 0;
sqrt 5 / 2 >= 2 / 2 by A11,XREAL_1:72;
hence thesis by A12,POWER:24;
end;
suppose A13: m > 0;
sqrt 5 >= 1 by A11,XXREAL_0:2; then
sqrt 5 / 2 >= 1 / 2 by XREAL_1:72;
hence thesis by A13,Th8,XXREAL_0:2;
end;
end; then
|.tbm.| <= sqrt 5/2 by A10,ABSVALUE:def 1; then
A14: |.tbm.| * (1 - tb to_power (2*k)) <= (sqrt 5/2) * 1
by A8,A9,XREAL_1:66;
tbm * (1 - tb to_power (2*k)) <= |.tbm.| * (1 -tb to_power (2*k))
by A9,ABSVALUE:4,XREAL_1:64; then
tbm * (1 - tb to_power (2*k)) <= sqrt 5 / 2 by A14,XXREAL_0:2;
hence thesis by A7,FIB_NUM2:3;
end;
suppose A15: k is odd; then
A16: m is odd by A4,A5;
m <> 0 by A15,A4,A5; then
A17: m >= 1 by NAT_1:14;
per cases by A17,XXREAL_0:1;
suppose A18: m = 1;
tb * (- 1 - tb to_power (2*k)) <= sqrt 5 / 2
proof
A19: tb to_power (2*k) > 0 by Th6;
tb to_power (2*k) < 1 / 2 by Th8,A1; then
tb to_power (2*k) + 1 < 1 / 2 + 1 by XREAL_1:6; then
((sqrt 5 - 1) / sqrt 5) * (1 + tb to_power (2*k)) <
(6 / 10) * (3 / 2) by Lm23,Lm24,A19,XREAL_1:98; then
(((sqrt 5 - 1) / sqrt 5) * (1 + tb to_power (2*k))) < 1 &
sqrt 5 > 0 by SQUARE_1:25,XXREAL_0:2; then
(((sqrt 5 - 1) / sqrt 5) * (1 + tb to_power (2*k))) *sqrt 5 <
1 * sqrt 5 by XREAL_1:68; then
((sqrt 5-1) * (1/sqrt 5)) * (1+tb to_power (2*k)) * sqrt 5 <
sqrt 5 by XCMPLX_1:99; then
(sqrt 5 - 1)* (1+tb to_power (2*k)) * (sqrt 5 *(1/sqrt 5)) <
sqrt 5; then
(sqrt 5-1)* (1+tb 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+tb to_power (2*k))*1<sqrt 5 by XCMPLX_1:60;then
((1 - sqrt 5) * ( - 1 - tb to_power (2*k))) / 2 < sqrt 5 / 2
by XREAL_1:74;
hence thesis by FIB_NUM:def 2;
end; then
tbm * (- 1 - tb to_power (2*k)) <= sqrt 5 / 2 by A18;
hence thesis by A15,FIB_NUM2:2;
end;
suppose A20: m > 1;
A21: tbm < 0 by A16,Th7;
A22: tbm * (-1-tb to_power (2*k)) = -tbm * (1+tb to_power (2*k));
A23: tb to_power (2*k) > 0 by Th6;
tb to_power (2*k) <= 1 / 2 by A1,Th8; then
A24: tb to_power (2*k) + 1 <= 1/2 + 1 by XREAL_1:6;
tbm > -1/2 by Th14,A20; then
- tbm < - -1/2 by XREAL_1:24; then
(-tbm) * (1 + tb to_power (2*k)) <= (1 / 2) * (3 / 2)
by A21,A23,A24,XREAL_1:66; then
-tbm * (1 + tb to_power (2*k)) <= sqrt 5 / 2 by Lm25,XXREAL_0:2
;
hence thesis by A15,A22,FIB_NUM2:2;
end;
end;
end; then
tbm*(tk*tbk-tb to_power (k+k)) <= sqrt 5/2 by Lm3,NEWTON:7; then
tbm * (tk * tbk - tbk * tbk) <= sqrt 5 / 2 by Th2; then
((tbm * tbk) * (tk - tbk)) / sqrt 5 <= (sqrt 5 / 2) / sqrt 5
by A6,XREAL_1:72; then
(tbm*tbk) * ((tk - tbk) / sqrt 5) <= (sqrt 5 / 2)/sqrt 5
by XCMPLX_1:74; then
(tbm * tbk) * Fib k <= (sqrt 5 / 2) / sqrt 5 by FIB_NUM:7; then
tbn * Fib k <= (sqrt 5 / 2) / sqrt 5 by A5,Th2; then
tbn * Fib k <= (1 * sqrt 5) / (2 * sqrt 5) by XCMPLX_1:78;
hence thesis by A6,XCMPLX_1:91;
end;
suppose n is odd; then
tbn < 0 by Th7;
hence thesis;
end;
end; then
- tbn * Fib k >= - 1/2 by XREAL_1:24; then
- tbn * Fib k + 1/2 >= - 1/2 + 1/2 by XREAL_1:6; then
- tbn * Fib k + 1/2 + Fib (n+k) >= 0 + Fib (n+k) by XREAL_1:6;
hence thesis by A2;
end;
tk * Fib n + 1/2 - 1 < Fib (n+k)
proof
tbn * Fib k > - 1/2
proof
per cases;
suppose n is even; then
tbn > 0 by Th6;
hence thesis;
end;
suppose A25: n is odd;
consider m being Nat such that A26: n = k + m by A1,NAT_1:10;
set tbm = tau_bar to_power m;
per cases;
suppose A27: k is even; then
A28: m is odd by A25,A26; then
A29: tbm < 0 by Th7;
A30: m >= 1 by A28,NAT_1:14;
per cases by A30,XXREAL_0:1;
suppose A31: m = 1;
((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 - tb to_power (2*k) = (-1) to_power k - tb to_power (2*k)
by A27,FIB_NUM2:3
.= tk * tbk - tb to_power (k+k) by Lm3,NEWTON:7
.= tk * tbk - tbk * tbk by Th2
.= tbk * (tk - tbk);
((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 - tb to_power (2*k)) > - 1
by Lm7,NEWTON:9; then
(((1-sqrt 5) / sqrt 5) * (1-tb to_power (2*k))) / 2 > (-1) / 2
by XREAL_1:74; then
((1-sqrt 5) /sqrt 5) * ((1-tb to_power (2*k)) / 2) > (-1)/2; then
((1-sqrt 5)*(1/sqrt 5)) * ((1-tb to_power (2*k))*(1/2)) > (-1)/2
by XCMPLX_1:99; then
tb*(1/sqrt 5)*(1-tb to_power (2*k)) > -1/2 by FIB_NUM:def 2; then
tb*(1/sqrt 5) * (tbk * (tk-tbk)) > - 1/2 by A34; then
tb * tbk * ((tk-tbk) * (1/sqrt 5)) > - 1/2; then
tb * tbk * ((tk-tbk)/sqrt 5) > -1/2 by XCMPLX_1:99; then
tb to_power 1 * tbk * ((tk-tbk)/sqrt 5) > - 1/2; then
tb to_power (1+k) * ((tk-tbk) / sqrt 5) > - 1/2 by Th2;
hence thesis by A31,A26,FIB_NUM:7;
end;
suppose m > 1; then
tbm > - 1/2 by Th14; then
A35: - tbm < - -1/2 by XREAL_1:24;
sqrt 5 > 1 by SQUARE_1:18,27; then
- sqrt 5 < - 1 by XREAL_1:24; then
A36: (- sqrt 5) / 2 < (-1) / 2 by XREAL_1:74;
tb to_power (2*k) > 0 & tb to_power (2*k) < 1/2
by Th6,Th8,A1; then
- tb to_power (2*k) < 0 & - tb to_power (2*k) > - 1/2
by XREAL_1:24; then
- tb to_power (2*k) + 1 < 0+1 & -tb to_power (2*k) + 1 > -1/2 + 1
by XREAL_1:6; then
(-tbm) * (1-tb to_power (2*k)) < (1/2) * 1
by A35,A29,XREAL_1:98; then
- -tbm * (1 - tb to_power (2*k)) > - 1/2 by XREAL_1:24; then
tbm * ((-1) to_power k - tb to_power (2*k)) > - 1/2
by A27,FIB_NUM2:3; then
tbm * ((-1) to_power k - tb to_power (2*k)) > -sqrt 5/2
by A36,XXREAL_0:2; then
tbm * (tk * tbk - tb to_power (k+k)) > - sqrt 5 / 2
by Lm3,NEWTON:7; then
tbm * (tk * tbk - tbk * tbk) > - sqrt 5 / 2 by Th2; then
(tbm * tbk) * (tk - tbk) > - sqrt 5 / 2; then
tbn * (tk - tbk) > - sqrt 5 / 2 & sqrt 5 > 0
by Th2,A26,SQUARE_1:25; then
(tbn*(tk-tbk))/sqrt 5 > (-sqrt 5/2)/sqrt 5 by XREAL_1:74; then
tbn * ((tk-tbk)/sqrt 5) > (-sqrt 5/2)/sqrt 5 by XCMPLX_1:74; then
tbn * Fib k > ((-sqrt 5)/2)/sqrt 5 by FIB_NUM:7; then
tbn * Fib k > ((-1) * sqrt 5) / (2 * sqrt 5) & sqrt 5 > 0
by SQUARE_1:25,XCMPLX_1:78; then
tbn * Fib k > (-1) / 2 by XCMPLX_1:91;
hence thesis;
end;
end;
suppose A37: k is odd; then
A38: m is even by A25,A26;
per cases;
suppose A39: m = 0;
per cases by A1;
suppose k = 1;
hence thesis by A1,A39,A26;
end;
suppose k > 1; 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
tb to_power (k*2) <= tb to_power (3*2) by Th11; then
A40: tb 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
tb to_power (2*k) + 1 < sqrt 5 / 2 by A40,XXREAL_0:2; then
- (tb to_power (2*k) + 1) > - sqrt 5 / 2 by XREAL_1:24; then
- tb to_power (2*k) + - 1 > - sqrt 5 / 2; then
- tb to_power (2*k) + (-1) to_power k > - sqrt 5 / 2
by A37,FIB_NUM2:2; then
- tb to_power (k+k) + tk * tbk >
- sqrt 5 / 2 by Lm3,NEWTON:7; then
- tbk * tbk + tk * tbk > - sqrt 5 / 2 by Th2; then
tbk * (-tbk + tk) > -sqrt 5/2 & sqrt 5 > 0 by SQUARE_1:25; then
(tbk * ( - tbk + tk)) / sqrt 5 >
(- sqrt 5 / 2) / sqrt 5 by XREAL_1:74; then
tbk*((tk-tbk)/sqrt 5) > (-sqrt 5/2)/sqrt 5 by XCMPLX_1:74; then
tbk * Fib k > (- sqrt 5 / 2) / sqrt 5 by FIB_NUM:7; then
tbk * Fib k > - (sqrt 5 / 2) / sqrt 5 by XCMPLX_1:187; then
tbk * Fib k > - (sqrt 5 / sqrt 5) / 2 & sqrt 5 > 0
by SQUARE_1:25,XCMPLX_1:48;
hence thesis by A39,A26,XCMPLX_1:60;
end;
end;
suppose m > 0; then
A41: tbm > 0 & tbm < 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: tb to_power (2*k) < 1/2 & tb to_power (2*k) > 0
by Th8,A1,Th6; then
tb to_power (2*k) + 1 < 1/2 + 1 by XREAL_1:6; then
tbm*(tb to_power (2*k)+1) < 1/2*(1/2+1) by A41,A43,XREAL_1:96;
then
tbm * (tb to_power (2*k) + 1) < sqrt 5/2 by A42,XXREAL_0:2; then
- tbm * (tb to_power (2*k) + 1) > - sqrt 5/2 by XREAL_1:24; then
tbm * (- tb to_power (2*k) +- 1) > - sqrt 5/2; then
tbm * (- tb to_power (2*k) + (-1) to_power k) > - sqrt 5/2
by A37,FIB_NUM2:2; then
tbm * (- tb to_power (k+k) + tk * tbk) > - sqrt 5/2
by Lm3,NEWTON:7; then
tbm * (- tbk * tbk + tk * tbk) > - sqrt 5/2 by Th2; then
(tbm * tbk) * (tk - tbk) > - sqrt 5/2; then
tbn * (tk - tbk) > - sqrt 5 / 2 & sqrt 5 > 0
by A26,Th2,SQUARE_1:25; then
(tbn * (tk-tbk)) /sqrt 5 > (-sqrt 5/2)/sqrt 5 by XREAL_1:74; then
tbn*((tk - tbk)/sqrt 5) > (-sqrt 5/2)/sqrt 5 by XCMPLX_1:74; then
tbn * Fib k > ((-sqrt 5)/2)/sqrt 5 by FIB_NUM:7; then
tbn * Fib k > ((-1) * sqrt 5) / (2 * sqrt 5) & sqrt 5 > 0
by SQUARE_1:25,XCMPLX_1:78; then
tbn * Fib k > (-1)/2 by XCMPLX_1:91;
hence thesis;
end;
end;
end;
end; then
- tbn * Fib k < - -1/2 by XREAL_1:24; then
- tbn * Fib k + 1/2 < 1/2 + 1/2 by XREAL_1:6; then
- tbn * Fib k + 1/2 - 1 < 1 - 1 by XREAL_1:9; then
- tbn * Fib k + 1/2 - 1 + Fib (n+k) < 0 + Fib (n+k) by XREAL_1:6;
hence thesis by A2;
end;
hence thesis by A3,INT_1:def 6;
end;
begin :: Formulas for the Lucas Numbers
theorem
for n being Nat st n >= 2 holds
Lucas(n) = [\ tau to_power n + 1/2 /]
proof
let n be Nat;
assume A1: n >= 2;
then 1/2 >= tau_bar to_power n by Th8; then
tau to_power n+1/2 >= tau to_power n + tau_bar to_power n by XREAL_1:6;
then
A2: tau to_power n + 1/2 >= Lucas n by FIB_NUM3:21;
n > 1 by A1,XXREAL_0:2; then
1/2 - 1 < tau_bar to_power n by Th14; then
tau to_power n+(1/2-1)< tau to_power n+tau_bar to_power n by XREAL_1:6;
then tau to_power n + 1/2 - 1 < Lucas n by FIB_NUM3:21;
hence thesis by A2,INT_1:def 6;
end;
theorem
for n being Nat st n >= 2 holds
Lucas (n) = [/ tau to_power n - 1/2 \]
proof
let n be Nat;
assume A1: n >= 2; then
n > 1 by XXREAL_0:2; then
-1/2 <= tau_bar to_power n by Th14; then
-1/2+tau to_power n <= tau_bar to_power n+tau to_power n by XREAL_1:6; then
A2: tau to_power n - 1/2 <= Lucas (n) by FIB_NUM3:21;
tau_bar to_power n < 1/2 by Th8,A1; then
tau_bar to_power n+tau to_power n < 1/2 + tau to_power n by XREAL_1:6;then
tau to_power n - 1/2 + 1 > Lucas n by FIB_NUM3:21;
hence thesis by A2,INT_1:def 7;
end;
theorem
for n being Nat st n >= 2 holds
Lucas (2*n) = [/ tau to_power (2*n) \]
proof
let n be Nat;
assume A1: n >= 2;
A2: tau_bar to_power (2*n) = (tau_bar to_power n) to_power 2 by NEWTON:9
.= (tau_bar to_power n) ^2 by POWER:46;
n - 0 is Element of NAT by NAT_1:21;
then tau_bar to_power n <> 0 by FIB_NUM3:1; then
tau_bar to_power (2*n) > 0 by A2,SQUARE_1:12; then
0 + tau to_power (2*n) <= tau to_power (2*n) + tau_bar to_power (2*n)
by XREAL_1:6; then
A3: tau to_power (2*n) <= Lucas (2*n) by FIB_NUM3:21;
tau_bar to_power (2*n) < 1 by Th8,A1,XXREAL_0:2; then
tau_bar to_power (2*n) + tau to_power (2*n) < 1 + tau to_power (2*n)
by XREAL_1:6; then
tau to_power (2*n) + 1 > Lucas (2*n) by FIB_NUM3:21;
hence thesis by A3,INT_1:def 7;
end;
theorem
for n being Nat st n >= 2 holds
Lucas (2*n+1) = [\ tau to_power (2*n+1) /]
proof
let n be Nat;
assume n >= 2; then
2 * n >= 2 * 2 by XREAL_1:64; then
2 * n + 1 >= 4 + 1 by XREAL_1:6; then
A1: 2 * n + 1 > 1 by XXREAL_0:2;
tau_bar to_power (2*n+1) <= 0 by Th7; then
tau to_power (2*n+1) + 0 >= tau to_power (2*n+1) + tau_bar to_power (2*n+1)
by XREAL_1:6; then
A2: tau to_power (2*n+1) >= Lucas (2*n+1) by FIB_NUM3:21;
-1/2 <= tau_bar to_power (2 * n +1 ) by Th14,A1; then
tau_bar to_power (2 * n + 1) > -1 by XXREAL_0:2; then
-1 + tau to_power (2*n+1) < tau to_power (2*n+1) + tau_bar to_power (2*n+1)
by XREAL_1:6; then
tau to_power (2*n+1) - 1 < Lucas (2*n+1) by FIB_NUM3:21;
hence thesis by A2,INT_1:def 6;
end;
theorem
for n being Nat st n >= 2 & n is odd holds
Lucas (n+1) = [\ tau * Lucas (n) + 1 /]
proof
let n be Nat;
set tn = tau_bar to_power n;
assume A1: n >= 2 & n is odd;
A2: tau * Lucas (n) + 1 >= Lucas (n+1)
proof
per cases by A1,XXREAL_0:1;
suppose A3: n = 2;
sqrt 5 >= 1 by SQUARE_1:18,26; then
sqrt 5 * 3 >= 1 * 3 by XREAL_1:64; then
5 + sqrt 5 * 3 >= 3 + 5 by XREAL_1:6; then
(5 + sqrt 5 * 3) / 2 >= 8 / 2 by XREAL_1:72;
hence thesis by A3,FIB_NUM:def 1,FIB_NUM3:14,15;
end;
suppose A4: n > 2;
A5: sqrt 5 > 0 by SQUARE_1:25;
tn>= -1/sqrt 5 & sqrt 5 > 0 by Th15,A4,SQUARE_1:25;then
tn*(sqrt 5) >= (-1/sqrt 5)*(sqrt 5) by XREAL_1:64; then
tn * (sqrt 5) >= sqrt 5 * ((-1)/sqrt 5) by XCMPLX_1:187; then
tn*(sqrt 5) >=(sqrt 5*(-1))/sqrt 5 by XCMPLX_1:74; then
tn*(sqrt 5)>= (sqrt 5/sqrt 5)*(-1) by XCMPLX_1:74; then
tn * (sqrt 5) >= 1 * (-1) by A5,XCMPLX_1:60; then
- (tau_bar to_power n * sqrt 5) <= -(-1) by XREAL_1:24; then
tn * tau_bar - tn * tau <= 1 by FIB_NUM:def 1,def 2; then
tn * tau_bar to_power 1-tn * tau <= 1; then
tau_bar to_power (n+1)- tn*tau <= 1 by Th2; then
tau_bar to_power (n+1) - tn * tau +
tn*tau <= 1 + tn*tau by XREAL_1:6; then
tn * tau + 1 + tau to_power (n+1) >=
tau_bar to_power (n+1) + tau to_power (n+1) by XREAL_1:6; then
tn * tau + 1 + tau to_power n * tau to_power 1 >=
tau_bar to_power (n+1)+tau to_power (n+1) by Th2; then
tn * tau + 1 + tau to_power n * tau >=
tau_bar to_power (n+1) + tau to_power (n+1); then
(tn + tau to_power n) * tau + 1 >=
tau_bar to_power (n+1) + tau to_power (n+1); then
Lucas (n) * tau + 1 >=
tau_bar to_power (n+1) + tau to_power (n+1) by FIB_NUM3:21;
hence thesis by FIB_NUM3:21;
end;
end;
tau * Lucas n + 1 - 1 < Lucas (n+1)
proof
A6: Lucas (n+1) = tau to_power (n+1) + tau_bar to_power (n+1) by FIB_NUM3:21;
A7: tau*Lucas n = tau * (tau to_power n + tn) by FIB_NUM3:21
.= tau * tau to_power n + tau * tau_bar to_power n
.= tau to_power 1 * tau to_power n + tau * tau_bar to_power n
.= tau to_power (n+1) + tau * tau_bar to_power n by Th2;
tn < 0 by Th7,A1;
then tau*tn < tau_bar*tn by XREAL_1:69;then
tau * tn < tau_bar to_power 1 * tn; then
tau * tn < tau_bar to_power (n+1) by Th2;
hence thesis by A6,A7,XREAL_1:6;
end;
hence thesis by A2,INT_1:def 6;
end;
theorem
for n being Nat st n >= 2 & n is even holds
Lucas (n+1) = [/ tau * Lucas n - 1 \]
proof
let n be Nat;
set tn = tau_bar to_power n;
assume A1: n >= 2 & n is even;
A2: Lucas (n+1) = tau to_power (n+1) + tau_bar to_power (n+1) by FIB_NUM3:21;
A3: tau * Lucas n = tau * (tau to_power n + tau_bar to_power n) by FIB_NUM3:21
.= tau * tau to_power n + tau * tau_bar to_power n
.= tau to_power 1 * tau to_power n + tau * tau_bar to_power n
.= tau to_power (n+1) + tau * tn by Th2;
A4: tau * Lucas n - 1 <= Lucas (n+1)
proof
tau * tn - 1 <= tau_bar to_power (n+1)
proof
A5: tn > 0 by Th6,A1;
tn <= 1 / sqrt 5 by Th16,A1; then
1 / tn >= 1 / (1/sqrt 5) by Th6,A1,XREAL_1:118; then
1 / tn >= sqrt 5 by XCMPLX_1:52; then
(1 / tn) * 2 >= (sqrt 5) * 2 by XREAL_1:64; then
(1 / tn) * 2 + 1 >= 2 * sqrt 5 + 1 by XREAL_1:6; then
(1 / tn) * 2 + 1 - sqrt 5 >= 2 * sqrt 5 + 1 - sqrt 5
by XREAL_1:13; then
((1 / tn) * 2 + (1 - sqrt 5)) / 2 >= (sqrt 5 + 1)/2 by XREAL_1:72; then
((1 / tn) + tau_bar) * tn >=
tau * tn by A5,FIB_NUM:def 1,def 2,XREAL_1:64; then
(1 / tn) * tn + tau_bar * tn >= tau * tn; then
(1 / tn) * tn + tau_bar to_power 1 * tn >= tau * tn; then
1 + tau_bar to_power 1 * tn >= tau * tn by A5,XCMPLX_1:87; then
1 + tau_bar to_power (n+1) >= tau*tn by Th2; then
1 + tau_bar to_power (n+1) - 1 >= tau * tn - 1 by XREAL_1:9;
hence thesis;
end; then
tau to_power (n+1) + (tau * tn - 1) <=
tau to_power (n+1) + tau_bar to_power (n+1) by XREAL_1:6;
hence thesis by A3,FIB_NUM3:21;
end;
tau * Lucas n - 1 + 1 > Lucas (n+1)
proof
tn = (- tau_bar) to_power n by A1,Th3; then
tn > 0 by POWER:34;
then tau * tn > tau_bar * tn by XREAL_1:68; then
tau * tn > tau_bar to_power 1 * tn; then
tau * tn > tau_bar to_power (n+1) by Th2;
hence thesis by A2,A3,XREAL_1:6;
end;
hence thesis by A4,INT_1:def 7;
end;
theorem
for n being Nat st n <> 1 holds
Lucas (n+1) = (Lucas n + sqrt(5*((Lucas n)^2 - 4*(-1) to_power n)))/2
proof
let n be Nat;
assume A1: n <> 1;
A2: (Lucas n)^2 - (-1) to_power n * 4 >= 0
proof
per cases by A1,NAT_1:25;
suppose n = 0; then
(Lucas n)^2 - (-1) to_power n * 4 = 2*2 - 1*4 by FIB_NUM3:11,POWER:24;
hence thesis;
end;
suppose n > 1; then
n + 1 > 1 + 1 by XREAL_1:8; then
n >= 2 & Lucas n >= n by FIB_NUM3:17,NAT_1:13; then
Lucas n >= 2 by XXREAL_0:2; then
(Lucas n) ^2 >= 2 ^2 by SQUARE_1:15; then
(Lucas n) ^2 >= 2*2 & - 4*(-1) to_power n >= -4 by Lm2; then
(Lucas n) ^2 +(- 4 * (-1) to_power n) >= 2 * 2 + (-4) by XREAL_1:7;
hence thesis;
end;
end;
A3: n - 0 is Element of NAT by NAT_1:21; then
2 * Lucas (n+1) = Lucas n*1 + 5 * Fib n*1 by FIB_NUM3:11,26,PRE_FF:1; then
A4: Lucas (n+1) = (5 * Fib n + Lucas n) / 2;
(Lucas n)^2 - 5*(Fib n)^2 = (Lucas n) to_power 2 - 5*(Fib n)^2 by POWER:46
.= (Lucas n) to_power 2 - 5 * (Fib n) to_power 2 by POWER:46
.= - (5 * (Fib n) |^2 - (Lucas n) |^2)
.= - (4 * (-1) to_power (n+1)) by A3,FIB_NUM3:30
.= (-1) * ((-1) to_power (n+1) * 4)
.= (-1) to_power 1 * ((-1) to_power (n+1) * 4)
.= ((-1) to_power 1 * (-1) to_power (n+1)) * 4
.= (-1) to_power (n + 1 + 1) * 4 by Th2
.= (-1) to_power (n + 2) * 4
.= (-1) to_power n * (-1) to_power 2 * 4 by Th2
.= (-1) to_power n * 1 * 4 by FIB_NUM2:3,POLYFORM:5;
then Fib n = sqrt (((Lucas n)^2 - (-1) to_power n * 4)/5)
by SQUARE_1:def 2;then
Lucas (n+1) = (5 * (sqrt ((Lucas n)^2 - (-1) to_power n * 4)/(sqrt 5)) +
Lucas n)/2 by A2,A4,SQUARE_1:30
.= ((sqrt ((Lucas n)^2 - (-1) to_power n * 4) * 5)/(sqrt 5) + Lucas n)/2
by XCMPLX_1:74
.= (sqrt ((Lucas n)^2 - (-1) to_power n * 4) * (5/(sqrt 5)) + Lucas n)/2
by XCMPLX_1:74
.= (sqrt ((Lucas n)^2-(-1) to_power n*4)*sqrt 5+Lucas n)/2 by SQUARE_1:34
.= (sqrt (((Lucas n)^2-(-1) to_power n*4)*5)+Lucas n)/2 by A2,SQUARE_1:29;
hence thesis;
end;
theorem
for n being Nat st n >= 4 holds
Lucas (n+1) = [\ (Lucas n + 1 + sqrt(5*(Lucas n)^2 - 2*Lucas n + 1))/2 /]
proof
let n be Nat;
set tb = tau_bar;
set tbn = tau_bar to_power n;
set tn = tau to_power n;
assume A1: n >= 4;
A2: sqrt 5 > 0 by SQUARE_1:25;
A3: (Lucas n + 1 + sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1)) /2 >= Lucas (n+1)
proof
A4: n - 0 is non zero Element of NAT by A1,NAT_1:21;
Lucas (n+1) >= n + 1 & n + 1 >= 0 + 1 by FIB_NUM3:17,XREAL_1:6; then
Lucas (n+1) >= Lucas n & Lucas (n+1) >= 1
by A4,FIB_NUM3:18,XXREAL_0:2; then
Lucas (n+1) + Lucas (n+1) >= Lucas n + 1 by XREAL_1:7; then
Lucas (n+1)+Lucas (n+1)-Lucas n >= Lucas n+1-Lucas n by XREAL_1:9; then
A5: 2 * Lucas (n+1) - Lucas n - 1 >= 1 - 1 by XREAL_1:9;
2*Lucas (n+1)-Lucas n - 1 = 2 * Lucas (n+1) - (tn+tbn) - 1 by FIB_NUM3:21
.= 2 * (tau to_power (n+1) + tau_bar to_power (n+1)) - (tn + tbn) - 1
by FIB_NUM3:21
.= 2 *(tn*tau to_power 1+tau_bar to_power (n+1))-(tn+tbn)-1 by Th2
.= 2 * (tn*tau + tau_bar to_power (n+1)) - (tn+tbn) - 1
.= 2 * (tn*tau + tbn * tb to_power 1) - (tn+tbn) - 1 by Th2
.= 2 * (tn * tau + tbn * tb) - (tn + tbn) - 1
.= (tn - tbn) * sqrt 5 - 1 by FIB_NUM:def 1,def 2
.= (((tn - tbn) / sqrt 5) * sqrt 5) * sqrt 5 - 1 by A2,XCMPLX_1:87
.= (Fib n * sqrt 5) * sqrt 5 - 1 by FIB_NUM:7
.= Fib n * (sqrt 5) ^2 - 1
.= 5 * Fib n - 1 by SQUARE_1:def 2; then
A6: (2 * Lucas (n+1) - Lucas n - 1)^2 = (5 * Fib n)^2 - 2 * (5*Fib n)*1 + 1^2
by SQUARE_1:5
.= 25 * (Fib n) ^2 - 10 * Fib n + 1;
5 * (Lucas n) ^2 - 2 * Lucas n >= 25 * (Fib n) ^2 - 10 * Fib n
proof
per cases by A1,XXREAL_0:1;
suppose n = 4;
hence thesis by FIB_NUM2:23,FIB_NUM3:16;
end;
suppose n > 4; then
A7: n >= 4+1 by NAT_1:13;
set s5 = sqrt 5;
A8: 5 *(Lucas n)^2 - 2*Lucas n =5*(Lucas n)^2 - 2*(tn+tbn) by FIB_NUM3:21
.= 5 * (tn + tbn) ^2 - 2 * (tn + tbn) by FIB_NUM3:21
.= 5 * tn ^2 + 5 * 2 * tn * tbn + 5 * tbn ^2 - 2 * tn - 2 * tbn;
A9: 25 * (Fib n)^2 - 10 * Fib n = 25 * (Fib n)^2 - 10 * ((tn-tbn)/s5)
by FIB_NUM:7
.= 25 * ((tn-tbn) / s5)^2 - 10 * ((tn-tbn) / s5) by FIB_NUM:7
.= 25 * ((tn-tbn)^2/s5^2)- 10 *((tn-tbn)/s5) by XCMPLX_1:76
.= 25 * ((tn-tbn)^2 / 5) - 10 * ((tn-tbn)/s5) by SQUARE_1:def 2
.= 5 *tn^2 - 5*2*tn*tbn + 5*tbn^2 - 10*(((tn-tbn)*s5)/s5^2)
by A2,XCMPLX_1:91
.= 5 * tn^2 - 10*tn*tbn + 5 * tbn^2 - 10 * (((tn-tbn)*s5)/5)
by SQUARE_1:def 2
.= 5 * tn^2 - 10*tn*tbn + 5 * tbn^2 - 2*tn*s5 + 2 * tbn * s5;
A10: n -' 1 + 1 = n + 1 -' 1 by A1,NAT_D:38,XXREAL_0:2
.= n by NAT_D:34;
A11: -10 <= 10 * (-1) to_power n by Lm1;
n -' 1 >= 5 -' 1 by A7,NAT_D:42; then
n -' 1 >= 5 - 1 by NAT_D:39; then
Lucas (n-'1) >= 7 by Th12,FIB_NUM3:16; then
Lucas (n-'1) >= 5 by XXREAL_0:2; then
Lucas (n-'1) * (-2) <= 5 * (-2) by XREAL_1:65; then
Lucas (n-'1+1) - (2 * Lucas (n-'1) + Lucas (n-'1+1)) <= -10; then
Lucas n - 5 * Fib n <= -10 by A10,FIB_NUM3:22; then
tn + tbn - 5 * Fib n <= -10 by FIB_NUM3:21; then
tn + tbn - 5 * ((tn-tbn) / s5) <= -10 by FIB_NUM:7; then
tn + tbn - 5 * ((tn-tbn) * (1/s5)) <= -10 by XCMPLX_1:99; then
tn + tbn - 5 * (1/s5) * (tn-tbn) <= -10; then
tn +tbn-(s5)^2*(1/s5)*(tn-tbn) <= -10 by SQUARE_1:def 2; then
tn + tbn - s5 * (s5 * (1/s5)) * (tn-tbn) <= -10; then
tn+tbn-s5*(s5/s5)*(tn-tbn) <= -10 by XCMPLX_1:99; then
tn + tbn - s5*1*(tn-tbn) <= -10 by A2,XCMPLX_1:60; then
tn + tbn - s5 * tn + s5 * tbn <= 10 * (tau * tb) to_power n
by Lm3,A11,XXREAL_0:2; then
tn + tbn - s5 * tn + sqrt 5 * tbn - 10 * (tau*tb) to_power n <=
10*(tau*tb) to_power n - 10*(tau*tb) to_power n by XREAL_1:9; then
tn + tbn - s5 * tn + s5 * tbn - 10 * (tau*tb) to_power n +
sqrt 5 * tn <= 0 + s5 * tn by XREAL_1:6; then
tn + tbn + s5 * tbn - 10*(tau*tb) to_power n <= s5 * tn; then
tn +tbn+s5*tbn - 10*(tn*tbn) <= s5*tn by NEWTON:7; then
(-10 * tn * tbn + tn + tbn + tbn * s5) * 2 <= (tn * s5) * 2
by XREAL_1:64; then
-(- 20 * tn * tbn + 2 * tn + 2 * tbn + 2*tbn*s5) >= - 2*tn*s5
by XREAL_1:24; then
10*tn*tbn - 2*tn - 2*tbn - 2*tbn*s5 + 10*tn*tbn - 10*tn*tbn >=
- 2 * tn * s5 - 10 * tn * tbn by XREAL_1:9; then
10*tn*tbn - 2*tn-2*tbn - 2*tbn*s5 + 2*tbn*s5 >=
- 10*tn*tbn - 2*tn*s5 + 2*tbn*s5 by XREAL_1:6; then
10 * tn * tbn - 2 * tn - 2 * tbn + 5 * tbn ^2 >=
- 10*tn*tbn - 2*tn*s5 + 2*tbn*s5 + 5*tbn^2 by XREAL_1:6; then
10 * tn * tbn + 5 * tbn ^2 - 2 * tn - 2 * tbn + 5 * tn ^2 >=
- 10*tn*tbn + 5*tbn^2 - 2*tn*s5 + 2 * tbn * s5 + 5 * tn ^2
by XREAL_1:6;
hence thesis by A8,A9;
end;
end; then
5 * (Lucas n) ^2 - 2 * Lucas n + 1 >= (2 * Lucas (n+1) - Lucas n - 1) ^2
by A6,XREAL_1:6; then
sqrt (5*(Lucas n)^2 - 2*Lucas n + 1) >=
sqrt ((2 * Lucas (n+1) - Lucas n - 1) ^2) by SQUARE_1:26; then
sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1) >= 2 *Lucas (n+1) - Lucas n - 1
by A5,SQUARE_1:def 2; then
sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1)+(Lucas n + 1) >=
2 * Lucas (n+1) - Lucas n - 1 + (Lucas n + 1) by XREAL_1:6; then
(Lucas n + 1 + sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1)) / 2 >=
(2 * Lucas (n+1)) / 2 by XREAL_1:72;
hence thesis;
end;
(Lucas n + 1 + sqrt (5*(Lucas n) ^2 - 2 * Lucas n + 1))/2 - 1 < Lucas (n+1)
proof
Lucas n >= n by FIB_NUM3:17; then
A12: Lucas n >= 4 by A1,XXREAL_0:2; then
A13: Lucas n / 5 >= 4 / 5 by XREAL_1:72;
Fib n >= 3 by A1,FIB_NUM2:23,45; then
Fib n + Lucas n / 5 >= 3 + 4/5 by A13,XREAL_1:7; then
A14: 2 < Fib n + Lucas n / 5 by XXREAL_0:2;
n is even or n is odd; then
(-1) to_power n <= 1 by FIB_NUM2:2,3; then
2 * (-1) to_power n <= 2 * 1 by XREAL_1:64; then
2 * (-1) to_power n < Fib n + Lucas n / 5 by A14,XXREAL_0:2; then
2 * (-1) to_power n < ((tn-tbn)/sqrt 5) + Lucas n/5 by FIB_NUM:7; then
2 * (-1) to_power n < ((tn-tbn)/sqrt 5) + (tn+tbn)/5 by FIB_NUM3:21; then
(2 * (-1) to_power n) * 10 < (((tn-tbn) / sqrt 5) + (tn+tbn) / 5) * 10
by XREAL_1:68; then
20 * (-1) to_power n < ((tn-tbn) / sqrt 5) * (2*5) + (tn+tbn) * 2; then
20 * (-1) to_power n < ((tn-tbn) / sqrt 5) * (2*(sqrt 5)^2) + (tn+tbn)*2
by SQUARE_1:def 2; then
20*(-1) to_power n<((tn-tbn)/sqrt 5)*sqrt 5*(sqrt 5*2)+(tn+tbn)*2; then
20*(-1) to_power n<(tn-tbn)*(2*sqrt 5)+(tn+tbn)*2 by A2,XCMPLX_1:87; then
20 * (-1) to_power n + (5*(tn)^2 + 5*(tbn)^2 + 1) <
(tn-tbn)*(2*sqrt 5)+(tn+tbn)*2+(5*(tn)^2+5*(tbn)^2+1) by XREAL_1:6; then
20 * (-1) to_power n + (5*(tn)^2 + 5*(tbn)^2 + 1) -(tn+tbn)*2 <
(tn-tbn)*(2*sqrt 5) + (tn+tbn)*2 + (5*(tn)^2 + 5*(tbn)^2 + 1)-(tn+tbn)*2
by XREAL_1:9; then
10*(-1) to_power n + 10 * (-1) to_power n + 5*(tn)^2 + 5*(tbn)^2 + 1 -
(tn+tbn)*2 -10*(-1) to_power n <
(tn-tbn)*(2*sqrt 5) + (5*(tn)^2 + 5*(tbn)^2 + 1)-10*(-1) to_power n
by XREAL_1:9; then
5*(2 * (tau*tau_bar) to_power n + (tn)^2 + (tbn)^2) + 1 -2*tn-2*tbn <
(2*sqrt 5)*tn-(2*sqrt 5)*tbn + 5*(tn)^2 + 5*(tbn)^2 -
10*(-1) to_power n + 1 by Lm3; then
5*(2 * (tn *tbn) + (tn)^2 + (tbn)^2) + 1 -2*tn-2*tbn <
(2*sqrt 5)*tn-(2*sqrt 5)*tbn + 5*(tn)^2 + 5*(tbn)^2 -
5*2*(-1) to_power n + 1 by NEWTON:7; then
5*(tn+tbn)^2 + 1 -2*tn-2*tbn <(2*sqrt 5)*tn-(2*sqrt 5)*tbn +
5*((tn)^2 +(tbn)^2 -2*(tau*tau_bar) to_power n) + 1
by Lm3; then
5 * (tn + tbn)^2 +1 - 2 * tn - 2 * tbn < (2*sqrt 5)*tn - (2*sqrt 5)*tbn +
5 * ((tn)^2 + (tbn)^2 - 2 * (tn * tbn)) + 1 by NEWTON:7; then
A15: 5 * (tn + tbn)^2 + 1 - 2 * (tn + tbn) < (2 * sqrt 5) * tn -
(2 * sqrt 5) * tbn + 5 * (tn - tbn)^2 + 1;
A16: 5 * (Lucas n) ^2 + 1 - 2 * Lucas n >= 0
proof
5 * Lucas n >= 5 * 4 by A12,XREAL_1:66; then
5 * Lucas n - 2 >= 20 - 2 by XREAL_1:9; then
Lucas n * (5 * Lucas n - 2) >= 4 * 18 by A12,XREAL_1:66; then
Lucas n * (5 * Lucas n - 2) + 1 >= 4 * 18 + 1 by XREAL_1:6;
hence thesis;
end;
A17: 2 * tau to_power (n+1) - tn + 2 * tau_bar to_power (n+1) - tbn + 1 > 0
proof
2 * tau to_power (n+1) - tn + 2 * tau_bar to_power (n+1) - tbn + 1 =
2*(tn*tau to_power 1)-tn+2*tau_bar to_power (n+1)-tbn + 1 by Th2
.= 2*(tn*tau to_power 1)-tn+2*(tbn*tb to_power 1)-tbn + 1 by Th2
.= 2*(tn*tau) - tn + 2*(tbn*tb to_power 1) - tbn + 1
.= tn * sqrt 5 + 2 * (tbn * tb) - tbn + 1 by FIB_NUM:def 1
.= sqrt 5 * (tn - tbn) * 1 + 1 by FIB_NUM:def 2
.= sqrt 5 * (tn - tbn) * (sqrt 5 / sqrt 5) + 1 by A2,XCMPLX_1:60
.= sqrt 5 * (tn - tbn) * (sqrt 5 * (1 / sqrt 5)) + 1 by XCMPLX_1:99
.= sqrt 5 * ((tn - tbn) * (1 / sqrt 5)) * sqrt 5 + 1
.= sqrt 5 * ((tn - tbn) / sqrt 5) * sqrt 5 + 1 by XCMPLX_1:99
.= sqrt 5 * Fib n * sqrt 5 + 1 by FIB_NUM:7
.= (sqrt 5) ^2 * Fib n + 1
.= 5 * Fib n + 1 by SQUARE_1:def 2;
hence thesis;
end;
(2*sqrt 5) *tn - (2*sqrt 5) *tbn + 5 * (tn-tbn) ^2 + 1 = 2*sqrt 5*tn -
2 * sqrt 5 * tbn + (sqrt 5) ^2 * (tn - tbn) ^2 + 1 by SQUARE_1:def 2
.= (2 * tau * tn - 1 * tn + 2 * tb * tbn - 1 * tbn + 1) ^2
by FIB_NUM:def 1,def 2
.= (2*tau to_power 1 * tn - 1*tn + 2*tb*tbn - 1*tbn + 1) ^2
.= (2 * (tau to_power 1*tn)-1*tn + 2*tb to_power 1*tbn - 1*tbn + 1) ^2
.= (2*tau to_power (n+1)-tn+2*(tb to_power 1*tbn)-tbn+1)^2 by Th2
.= (2*tau to_power (n+1) - tn + 2*tau_bar to_power (n+1) - tbn + 1) ^2
by Th2; then
5 * (Lucas n) ^2 + 1 - 2 * (tn+tbn) < (2 * tau to_power (n+1) - tn +
2 * tau_bar to_power (n+1) - tbn + 1) ^2 by A15,FIB_NUM3:21; then
5 * (Lucas n) ^2 + 1 - 2 * Lucas n < (2 * tau to_power (n+1) - tn +
2 * tau_bar to_power (n+1) - tbn + 1) ^2 by FIB_NUM3:21; then
sqrt (5*(Lucas n)^2 + 1 - 2*Lucas n) < sqrt ((2*tau to_power (n+1) - tn +
2 * tau_bar to_power (n+1) - tbn + 1) ^2) by A16,SQUARE_1:27; then
sqrt (5 * (Lucas n) ^2 + 1 - 2 * Lucas n) <
2 * (tau to_power (n+1) + tau_bar to_power (n+1)) - tn
- tbn + 1 by A17,SQUARE_1:22; then
sqrt (5 *(Lucas n) ^2 - 2 * Lucas n + 1) < 2 *Lucas (n+1) - tn - tbn + 1
by FIB_NUM3:21; then
1 + sqrt (5*(Lucas n)^2 - 2*Lucas n + 1) < 2*Lucas (n+1) + 1 -tn - tbn +1
by XREAL_1:6; then
tn + tbn + 1 + sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1) - tn - tbn <
2 * Lucas (n+1) + 2 - tn - tbn; then
Lucas n + 1 + sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1) - tn - tbn <
2 * Lucas (n+1) + 2 - tn - tbn by FIB_NUM3:21; then
Lucas n + 1 + sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1) - tn <
2 * Lucas (n+1) + 2 - tn by XREAL_1:9; then
Lucas n + 1 + sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1) - 2 + 2 <
2 * Lucas (n+1) + 2 by XREAL_1:9; then
Lucas n + 1 + sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1) - 2 <
2 * Lucas (n+1) by XREAL_1:6; then
((Lucas n + 1 + sqrt (5 * (Lucas n) ^2 - 2 * Lucas n + 1)) - 2) / 2 <
(2 * Lucas (n+1)) / 2 by XREAL_1:74;
hence thesis;
end;
hence thesis by A3,INT_1:def 6;
end;
theorem
for n being Nat st n > 2 holds
Lucas n = [\ (1/tau) * (Lucas (n+1) + 1/2) /]
proof
let n be Nat;
assume A1: n > 2; then
A2: n > 1 by XXREAL_0:2;
A3: sqrt 5 > 0 by SQUARE_1:25;
set tbn = tau_bar to_power n;
A4: (1/tau) * (Lucas (n+1) + 1/2) >= Lucas (n)
proof
tbn <= 1 / (2 * sqrt 5)
proof
per cases;
suppose A5: n is even;
n >= 2 + 1 by A1,NAT_1:13; then
n = 3 or n > 3 by XXREAL_0:1; then
n = 3 or n >= 3+1 by NAT_1:8; then
A6: tbn <= tau_bar to_power 4 by Th11,A5,POLYFORM:6;
A7: tau_bar to_power (3+1) = tau_bar to_power 3 * tau_bar to_power 1
by Th2
.= (2 - sqrt 5) * tau_bar by Lm8
.= (2 - 2*sqrt 5 - sqrt 5 + (sqrt 5) ^2) / 2 by FIB_NUM:def 2
.= (2 - 3 * sqrt 5 + 5) / 2 by SQUARE_1:def 2
.= (7 - 3 * sqrt 5) / 2;
sqrt 5 <= sqrt ((16/7) ^2) by SQUARE_1:26; then
sqrt 5 <= 16/7 by SQUARE_1:def 2; then
7 * sqrt 5 <= (16/7) * 7 by XREAL_1:64; then
7 * sqrt 5 - 3 * 5 <= 16 - 3*5 by XREAL_1:9; then
7 * sqrt 5 - 3 * (sqrt 5) ^2 <= 1 by SQUARE_1:def 2; then
((7-3*sqrt 5)*sqrt 5) / sqrt 5 <= 1 / sqrt 5 by A3,XREAL_1:72; then
7 - 3 * sqrt 5 <= 1 / sqrt 5 by A3,XCMPLX_1:89; then
(7 - 3 * sqrt 5) / 2 <= (1 / sqrt 5) / 2 by XREAL_1:72; then
tau_bar to_power 4 <= 1 / (2 * sqrt 5) by A7,XCMPLX_1:78;
hence thesis by A6,XXREAL_0:2;
end;
suppose n is odd; then
tbn < 0 by Th7;
hence thesis by A3;
end;
end; then
tbn * sqrt 5 <= (1 / (2 * sqrt 5)) * sqrt 5 by A3,XREAL_1:64; then
tbn * sqrt 5 <= 1/2 by A3,XCMPLX_1:92; then
- tbn * sqrt 5 >= - 1/2 by XREAL_1:24; then
tau_bar * tbn - tau * tbn + (1/2 + tau*tbn) >= - 1/2 + (1/2 + tau * tbn)
by FIB_NUM:def 1,def 2,XREAL_1:6; then
(tau_bar * tbn + 1/2) / tau >= (tbn * tau)/tau by XREAL_1:72; then
(tau_bar * tbn + 1/2) / tau >= tbn by XCMPLX_1:89; then
(tau_bar * tbn + 1/2) / tau + tau to_power (n+1) / tau >=
tbn + tau to_power (n+1) / tau by XREAL_1:6; then
(tau_bar * tbn + 1/2 + tau to_power (n+1))/tau >=
tbn + tau to_power (n+1) / tau by XCMPLX_1:62; then
(tau_bar to_power 1 * tbn + 1/2 + tau to_power (n+1)) / tau >=
tbn + tau to_power (n + 1) / tau; then
(tau_bar to_power 1 * tbn + tau to_power (n+1) + 1/2) / tau >=
tbn + (tau to_power n * tau to_power 1) / tau by Th2; then
(tau_bar to_power (1+n) + tau to_power (n+1) + 1/2)/tau >=
tbn + (tau to_power n * tau to_power 1) / tau by Th2; then
(Lucas (n+1) + 1/2)/tau >=
tbn + (tau to_power n * tau to_power 1) / tau by FIB_NUM3:21; then
(Lucas (n+1)+1/2)/tau >= tbn+(tau to_power n*tau)/tau; then
(Lucas (n+1) + 1/2)/tau >= tbn + tau to_power n by XCMPLX_1:89; then
(Lucas (n+1) + 1/2)/tau >= Lucas n by FIB_NUM3:21;
hence thesis by XCMPLX_1:99;
end;
(1/tau) * (Lucas (n+1) + 1/2) - 1 < Lucas n
proof
tbn > -1/2 by Th14,A2; then
- tbn < - (-1/2) by XREAL_1:24; then
(- tbn) * sqrt 5 < (1/2)*sqrt 5 by A3,XREAL_1:68; then
tbn * tau_bar - tbn * tau + (tbn * tau + 1/2) <
tau - 1/2 + (tbn * tau + 1/2) by FIB_NUM:def 1,def 2,XREAL_1:6; then
tbn * tau_bar + 1/2 - tau < tau - 1/2 + tbn * tau + 1/2 - tau
by XREAL_1:9; then
(tbn * tau_bar + 1/2 - tau)/tau < (tbn * tau)/tau by XREAL_1:74; then
(tbn * tau_bar) / tau + (1/2) / tau - tau / tau <
(tbn * tau) / tau by XCMPLX_1:124; then
(tbn * tau_bar) / tau + (1/2) /tau - tau/tau < tbn by XCMPLX_1:89; then
(tbn * tau_bar) / tau + (1 / 2) / tau - 1 < tbn by XCMPLX_1:60; then
(tbn * tau_bar) / tau + (1 / 2) / tau - 1 + tau to_power n <
tbn + tau to_power n by XREAL_1:6; then
(tbn * tau_bar) / tau + (1 / 2) / tau + tau to_power n * 1-1 < Lucas n
by FIB_NUM3:21; then
(tbn * tau_bar)/tau + (1 / 2) / tau + tau to_power n * (tau /tau) - 1 <
Lucas n by XCMPLX_1:60; then
(tbn * tau_bar)/tau + (1/2)/tau + (tau to_power n * tau)/tau - 1 <
Lucas n by XCMPLX_1:74; then
(tbn * tau_bar + 1/2 + tau to_power n * tau) / tau - 1 < Lucas n
by XCMPLX_1:63; then
(tbn * tau_bar to_power 1 + 1/2 + tau to_power n * tau) / tau - 1 <
Lucas n; then
(tbn * tau_bar to_power 1 + 1/2 + tau to_power n * tau to_power 1) /
tau - 1 < Lucas n; then
(tau_bar to_power (n+1) + 1/2 + tau to_power n * tau to_power 1) /
tau - 1 < Lucas n by Th2; then
(tau_bar to_power (n+1) + 1/2 + tau to_power (n+1)) / tau - 1 <
Lucas n by Th2; then
(tau_bar to_power (n+1) + tau to_power (n+1) + 1/2) / tau - 1 <
Lucas n; then
(Lucas (n+1) + 1/2) / tau - 1 < Lucas n by FIB_NUM3:21;
hence thesis by XCMPLX_1:99;
end;
hence thesis by A4,INT_1:def 6;
end;
theorem
for n,k being Nat st n >= 4 & k >= 1 & n > k & n is odd holds
Lucas (n+k) = [\ tau to_power k * Lucas n + 1 /]
proof
let n,k be Nat;
assume A1: n >= 4 & k >= 1 & n > k & n is odd;
set tb = tau_bar;
set tk = tau to_power k;
set tn = tau to_power n;
set tbn = tau_bar to_power n;
A2: sqrt 5 > 1 by SQUARE_1:18,27;
A3: tau to_power k * Lucas n + 1 >= Lucas (n+k)
proof
tk * tbn + 1 >= tb to_power (n+k)
proof
consider m being Nat such that A4: n = k + m by A1,NAT_1:10;
A5: m is non zero Nat by A1,A4; then
A6: m >= 1 by NAT_1:14;
A7: ((1-sqrt 5) to_power m * (-1) to_power k) / 2 to_power m + 1 >=
(1-sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m)
proof
per cases;
suppose A8: k is even; then
A9: m is odd by A1,A4;
A10: 2 to_power m > 0 by POWER:34;
A11: ((1-sqrt 5) to_power m * (-1) to_power k) / 2 to_power m + 1 =
((1-sqrt 5) to_power m *1) / 2 to_power m + 1 by A8,FIB_NUM2:3
.= (( - ( - 1 + sqrt 5)) to_power m) / 2 to_power m +
2 to_power m / 2 to_power m by A10,XCMPLX_1:60
.= (((-1) * (sqrt 5 - 1)) to_power m + 2 to_power m) / 2 to_power m
by XCMPLX_1:62
.= ((-1) to_power m * (sqrt 5-1) to_power m +
2 to_power m) / 2 to_power m by NEWTON:7
.= (2 to_power m + (-1) * (sqrt 5-1) to_power m) / 2 to_power m
by A9,FIB_NUM2:2
.= (2 to_power m - (sqrt 5 - 1) to_power m) / 2 to_power m;
A12: sqrt (3 ^2) > sqrt 5 & sqrt 5 > sqrt 1 by SQUARE_1:27; then
3 > sqrt 5 & sqrt 5 > 1 by SQUARE_1:def 2; then
3 - 1 > sqrt 5 - 1 & sqrt 5 - 1 > 1 - 1 by XREAL_1:9; then
2 to_power m > (sqrt 5 - 1) to_power m by A5,POWER:37; then
A13: 2 to_power m - (sqrt 5-1) to_power m > (sqrt 5-1) to_power m -
(sqrt 5-1) to_power m by XREAL_1:9;
A14: (1-sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m)
= ((-1) * (-1+sqrt 5)) to_power (2*k+m) / 2 to_power (2*k+m)
.= ((-1) to_power (2*k+m) * (-1+sqrt 5) to_power (2*k+m)) /
2 to_power (2*k+m) by NEWTON:7
.= ((-1) * (-1+sqrt 5) to_power (2*k+m)) / 2 to_power (2*k+m)
by A9,FIB_NUM2:2
.= (-1) * ((-1+sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m))
by XCMPLX_1:74;
sqrt 5 - 1 > 1 - 1 by A12,XREAL_1:9; then
(- 1 + sqrt 5) to_power (2*k+m) > 0 by POWER:34; then
(1 - sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m) <= 0 by A14;
hence thesis by A13,A11;
end;
suppose A15: k is odd; then
A16: m is even by A1,A4;
A17: 2 to_power m > 0 by POWER:34;
A18: 2 to_power (2*k) > 0 by POWER:34;
m > 1 by A16,A6,POLYFORM:4,XXREAL_0:1; then
A19: m - 1 is non zero Nat by NAT_1:20;
A20: ((1-sqrt 5) to_power m * (-1) to_power k) / 2 to_power m + 1 =
((1-sqrt 5) to_power m * (-1)) / 2 to_power m + 1
by A15,FIB_NUM2:2
.= ((1-sqrt 5) to_power m *(-1)) / 2 to_power m +
2 to_power m / 2 to_power m by A17,XCMPLX_1:60
.= (((-1) * (-1+sqrt 5)) to_power m * (-1) +
2 to_power m) / 2 to_power m by XCMPLX_1:62
.= (((-1) to_power m) * ((-1+sqrt 5) to_power m) * (-1) +
2 to_power m) / 2 to_power m by NEWTON:7
.= (1 * ((-1 + sqrt 5) to_power m) * (-1) +
2 to_power m) / 2 to_power m by A16,FIB_NUM2:3
.= ((-((-1+sqrt 5) to_power m) + 2 to_power m) * 2 to_power (2*k))/
(2 to_power m * 2 to_power (2*k)) by A18,XCMPLX_1:91
.= (-((-1+sqrt 5) to_power m) * 2 to_power (2*k) +
2 to_power m * 2 to_power (2*k)) / 2 to_power (m+2*k) by Th2
.= (-((-1+sqrt 5) to_power m) * 2 to_power (2*k) +
2 to_power (m+2*k)) / 2 to_power (m+2*k) by Th2
.= (2 to_power (m+2*k) - (-1+sqrt 5) to_power m *
2 to_power (2*k)) / 2 to_power (m+2*k);
A21: (1-sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m) =
((-1) * (-1+sqrt 5)) to_power (2*k+m) / 2 to_power (2*k+m)
.= ((-1) to_power (2*k+m) * (-1+sqrt 5) to_power (2*k+m)) /
2 to_power (2*k+m) by NEWTON:7
.= (1 * (- 1 + sqrt 5) to_power (2*k+m)) / 2 to_power (2*k+m)
by A16,FIB_NUM2:3
.= ((sqrt 5 - 1) to_power (2*k+m)) / 2 to_power (2*k+m);
2 to_power m - (sqrt 5 - 1) to_power m >= (sqrt 5 - 1) to_power m
proof
defpred P[Nat] means
2 to_power ($1+1) - (sqrt 5 - 1) to_power ($1+1) >=
(sqrt 5 - 1) to_power ($1+1);
A22: 2 to_power (1+1) - (sqrt 5 - 1) to_power (1+1) =
2 ^2 - (sqrt 5-1) to_power 2 by POWER:46
.= 4 - (sqrt 5-1) ^2 by POWER:46
.= 4 - ((sqrt 5) ^2 - 2 * sqrt 5 * 1 + 1 ^2)
.= 4 - (5 - 2 * sqrt 5 + 1) by SQUARE_1:def 2
.= 2 * sqrt 5 - 2;
A23: (sqrt 5 - 1) to_power (1+1) = (sqrt 5 - 1) ^2 by POWER:46
.= (sqrt 5) ^2 - 2 * sqrt 5 * 1 + 1 ^2
.= 5 - 2 * sqrt 5 + 1 by SQUARE_1:def 2
.= 6 - 2 * sqrt 5;
sqrt 5 >= sqrt (2 ^2) by SQUARE_1:27; then
sqrt 5 >= 2 by SQUARE_1:def 2; then
sqrt 5 * 4 >= 2 * 4 by XREAL_1:64; then
sqrt 5 * 2 + sqrt 5 * 2 - 2 >= 6 + 2 - 2 by XREAL_1:9; then
sqrt 5*2 + sqrt 5*2 -2-2*sqrt 5 >= 6 - 2*sqrt 5 by XREAL_1:9;
then
A24: P[1] by A22,A23;
A25: for k being non zero Nat st P[k] holds P[k+1]
proof
let k be non zero Nat;
A26: sqrt 5 - 1 > 1 - 1 by A2,XREAL_1:9;
assume P[k]; then
2 to_power (k+1) - (sqrt 5 - 1) to_power (k+1) + (sqrt 5 - 1)
to_power (k+1) >= (sqrt 5 - 1) to_power (k+1) +
(sqrt 5 - 1) to_power (k+1) by XREAL_1:6; then
2 to_power (k+1) * (sqrt 5-1) >=
2*(sqrt 5-1) to_power (k+1) * (sqrt 5-1) by A26,XREAL_1:64;
then
2 to_power (k+1) * (sqrt 5-1) >=
2*((sqrt 5 - 1) to_power (k+1) * (sqrt 5-1)); then
2 to_power (k+1) * (sqrt 5-1) >= 2*((sqrt 5 - 1) to_power (k+1)
* (sqrt 5-1) to_power 1); then
A27: 2 to_power (k+1) * (sqrt 5-1) >=
2 * (sqrt 5 - 1) to_power (k+1+1) by Th2,A26;
sqrt (3 ^2) >= sqrt 5 by SQUARE_1:27; then
3 >= sqrt 5 by SQUARE_1:def 2; then
3 - 1 >= sqrt 5 - 1 by XREAL_1:9; then
2 * 2 to_power (k+1) >= (sqrt 5-1) * 2 to_power (k+1)
by XREAL_1:64; then
2 to_power 1 * 2 to_power (k+1) >=
(sqrt 5-1) * 2 to_power (k+1); then
2 to_power (1+k+1) >= (sqrt 5-1) * 2 to_power (k+1)
by Th2; then
2 to_power (1+k+1) >= 2 * (sqrt 5 - 1) to_power (k+1+1)
by A27,XXREAL_0:2; then
2 to_power (1+k+1) - (sqrt 5 - 1) to_power (k+1+1) >=
2 * (sqrt 5 - 1) to_power (k+1+1)-(sqrt 5 - 1) to_power (k+1+1)
by XREAL_1:9;
hence thesis;
end;
for k being non zero Nat holds P[k] from NAT_1:sch 10(A24,A25);
then 2 to_power (m-1+1) - (sqrt 5 - 1) to_power (m-1+1) >=
(sqrt 5 - 1) to_power (m-1+1) by A19;
hence thesis;
end; then
(2 to_power m - (sqrt 5 - 1) to_power m)* 2 to_power (2*k) >=
(sqrt 5 - 1) to_power m * 2 to_power (2*k) by XREAL_1:64; then
2 to_power m * 2 to_power (2*k)-
(sqrt 5-1) to_power m * 2 to_power (2*k) >=
(sqrt 5 - 1) to_power m * 2 to_power (2*k); then
2 to_power (m+2*k) - (sqrt 5 - 1) to_power m * 2 to_power (2*k) >=
(sqrt 5 - 1) to_power m * 2 to_power (2*k) by Th2; then
(2 to_power (m + 2 * k) -
(sqrt 5 - 1) to_power m * 2 to_power (2*k)) / 2 to_power (m+2*k) >=
((sqrt 5 - 1) to_power m * 2 to_power (2*k)) / 2 to_power (m+2*k)
by XREAL_1:72; then
A28: (2 to_power m * 2 to_power (2*k) -
(sqrt 5 - 1) to_power m * 2 to_power (2*k)) / 2 to_power (m+2*k) >=
((sqrt 5 - 1) to_power m * 2 to_power (2*k)) / 2 to_power (m+2*k)
by Th2;
A29: sqrt 5 - 1 > 1 - 1 by A2,XREAL_1:9;
sqrt (3 ^2) > sqrt 5 & sqrt 5 > sqrt 1 by SQUARE_1:27; then
3 > sqrt 5 & sqrt 5 > 1 by SQUARE_1:def 2; then
A30: 3 - 1 > sqrt 5 - 1 & sqrt 5 - 1 > 1 - 1 by XREAL_1:9; then
A31: (sqrt 5 - 1) to_power m > 0 by POWER:34;
2 to_power (2*k) >= (sqrt 5-1) to_power (2*k)
by A30,A1,POWER:37; then
2 to_power (2*k) * (sqrt 5-1) to_power m >=
(sqrt 5-1) to_power (2*k)*(sqrt 5-1) to_power m
by A31,XREAL_1:64; then
(2 to_power (2*k) * (sqrt 5-1) to_power m) / 2 to_power (2*k+m) >=
((sqrt 5-1) to_power (2*k) * (sqrt 5-1) to_power m) /
2 to_power (2*k+m) by XREAL_1:72; then
((2 to_power m - (sqrt 5-1) to_power m) * 2 to_power (2*k)) /
2 to_power (m+2*k) >=
((sqrt 5-1) to_power (2*k)*(sqrt 5-1) to_power m) /
2 to_power (2*k+m) by A28,XXREAL_0:2; then
(2 to_power m *2 to_power (2*k) -
(sqrt 5-1) to_power m * 2 to_power (2*k)) / 2 to_power (m+2*k) >=
((sqrt 5-1) to_power (2*k+m)) /2 to_power (2*k+m) by Th2,A29;
hence thesis by A20,A21,Th2;
end;
end;
sqrt 5 - 1 > 1 - 1 by A2,XREAL_1:9; then
A32: - (sqrt 5 - 1) < 0;
((1+sqrt 5)*(1-sqrt 5)) / 2 to_power 2 = ((1+sqrt 5)*(1-sqrt 5)) / 2^2
by POWER:46
.= (1 ^2 - (sqrt 5) ^2) / 4
.= (1 - 5) / 4 by SQUARE_1:def 2
.= - 1; then
(-1) to_power k =
((1+sqrt 5) * (1-sqrt 5)) to_power k / (2 to_power 2) to_power k
by Th1
.= ((1+sqrt 5)*(1-sqrt 5)) to_power k / 2 to_power (2*k)
by NEWTON:9; then
((1-sqrt 5) to_power m * (((1+sqrt 5) * (1-sqrt 5)) to_power k) /
2 to_power (2*k)) / 2 to_power m + 1 >=
(1-sqrt 5) to_power (2*k+m) /2 to_power (2*k+m) by A7,XCMPLX_1:74; then
((1-sqrt 5) to_power m * (((1+sqrt 5)*(1-sqrt 5)) to_power k)) /
(2 to_power (2*k)*2 to_power m) + 1 >=
(1-sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m) by XCMPLX_1:78; then
((1-sqrt 5) to_power m * (((1+sqrt 5)*(1-sqrt 5)) to_power k)) /
2 to_power (2*k+m) + 1 >=
(1-sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m) by Th2; then
((1-sqrt 5) to_power m * ((1+sqrt 5) to_power k *
(1-sqrt 5) to_power k)) / 2 to_power (2*k+m) + 1 >=
(1-sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m) by NEWTON:7; then
((1-sqrt 5) to_power m *(1-sqrt 5) to_power k*(1+sqrt 5) to_power k) /
2 to_power (2*k+m) + 1 >=
(1-sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m); then
((1-sqrt 5) to_power (m+k) *(1+sqrt 5) to_power k) /
2 to_power (k+k+m) + 1 >=
(1-sqrt 5) to_power (2*k+m) / 2 to_power (2*k+m) by Th2,A32; then
((1-sqrt 5) to_power n *(1+sqrt 5) to_power k) /2 to_power (k+n) + 1 >=
((1-sqrt 5)/2) to_power (k+k+m) by A4,Th1; then
((1-sqrt 5) to_power n *(1+sqrt 5) to_power k) /
(2 to_power n * 2 to_power k) + 1 >=
tb to_power (k+n) by Th2,A4,FIB_NUM:def 2; then
((1-sqrt 5) to_power n/2 to_power n) * ((1+sqrt 5) to_power k /
(2 to_power k)) + 1 >= tb to_power (k+n) by XCMPLX_1:76; then
(((1-sqrt 5)/2) to_power n) *((1+sqrt 5) to_power k / (2 to_power k))+1
>= tb to_power (k+n) by Th1;
hence thesis by Th1,FIB_NUM:def 1,def 2;
end; then
tk * tbn + 1 + tau to_power (n+k) >=
tb to_power (n+k) + tau to_power (n+k) by XREAL_1:6; then
tau to_power (n+k)+tk*tbn+1 >= tau to_power (n+k)+tb to_power (n+k); then
tk*tn+tk*tbn+1 >= tau to_power (n+k)+tb to_power (n+k) by Th2;then
tk * (tn + tbn) + 1 >= Lucas (n+k) by FIB_NUM3:21;
hence thesis by FIB_NUM3:21;
end;
tau to_power k * Lucas n + 1 - 1 < Lucas (n+k)
proof
defpred P[Nat] means tau to_power $1 * Lucas n < Lucas (n+ $1);
tbn < 0 by Th7,A1; then
tbn * tau - tbn * tb < 0; then
tbn * tau - tbn * tb to_power 1 < 0; then
tbn * tau - tb to_power (n+1) < 0 by Th2; then
tbn*tau - tb to_power (n+1) + (tau to_power (n+1) +tb to_power (n+1)) <
0 + (tau to_power (n+1) + tb to_power (n+1)) by XREAL_1:6; then
tbn * tau + tau to_power (n+1) < Lucas (n+1) by FIB_NUM3:21; then
tbn * tau + tn * tau to_power 1 < Lucas (n+1) by Th2; then
tbn * tau + tn * tau < Lucas (n+1); then
(tbn + tn) * tau < Lucas (n+1); then
Lucas n * tau < Lucas (n+1) by FIB_NUM3:21; then
A33: P[1];
A34: for m being non zero Nat st P[m] holds P[m + 1]
proof
let m be non zero Nat;
assume P[m];
A35: (1-sqrt 5) to_power (m+1) < (1+sqrt 5) to_power (m+1)
proof
reconsider s = m + 1 as Element of NAT by ORDINAL1:def 12;
(1 - sqrt 5) to_power s <=
|.(1 - sqrt 5) to_power s.| by ABSVALUE:4; then
A36: (1-sqrt 5) to_power s <= (|.1-sqrt 5.|) to_power s by SERIES_1:2;
sqrt 5 > sqrt 1 by SQUARE_1:27; then
- sqrt 5 < - 1 by XREAL_1:24; then
A37: - sqrt 5 + 1 < - 1 + 1 by XREAL_1:6; then
A38: |.1 - sqrt 5.| = - (1 - sqrt 5) by ABSVALUE:def 1;
- (1 - sqrt 5) = -1 + sqrt 5; then
- (1 - sqrt 5) < 1 + sqrt 5 by XREAL_1:6; then
(|.1 - sqrt 5.|) to_power s < (1 + sqrt 5) to_power s
by A38,A37,POWER:37;
hence thesis by A36,XXREAL_0:2;
end;
2 to_power (m + 1) > 0 by POWER:34; then
((1 - sqrt 5) to_power (m+1)) / (2 to_power (m+1)) <
((1 + sqrt 5) to_power (m+1))/(2 to_power (m+1)) by A35,XREAL_1:74;
then
((1 - sqrt 5)/2) to_power (m+1) <
((1 + sqrt 5) to_power (m+1)) / (2 to_power (m+1)) by Th1; then
tb to_power (m+1) < tau to_power (m+1) & tbn < 0
by A1,Th7,Th1,FIB_NUM:def 1,def 2; then
tb to_power (m+1) * tbn > tau to_power (m+1) * tbn by XREAL_1:69; then
tb to_power (m+1) * tbn + tau to_power (n+m+1) >
tau to_power (m+1) * tbn + tau to_power (n+m+1) by XREAL_1:6; then
tb to_power (m+1+n) + tau to_power (n+m+1) >
tau to_power (m+1) * tbn + tau to_power (n+m+1) by Th2; then
tb to_power (m+1+n) + tau to_power (n+m+1) >
tau to_power (m+1) * tbn + tn * tau to_power (m+1) by Th2; then
Lucas (n+m+1) > tau to_power (m+1) * (tbn + tn) by FIB_NUM3:21;
hence thesis by FIB_NUM3:21;
end;
for m being non zero Nat holds P[m] from NAT_1:sch 10(A33,A34);
hence thesis by A1;
end;
hence thesis by A3,INT_1:def 6;
end;