:: Lucas Numbers and Generalized {F}ibonacci Numbers
:: by Piotr Wojtecki and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004-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 NUMBERS, SUBSET_1, POWER, CARD_1, NEWTON, XXREAL_0, SQUARE_1,
RELAT_1, ARYTM_1, ABIAN, NAT_1, ARYTM_3, PREPOWER, FIB_NUM, FUNCT_1,
ZFMISC_1, MCART_1, PRE_FF, FIB_NUM3, REAL_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ZFMISC_1, SQUARE_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, NEWTON, NAT_1, MCART_1, DOMAIN_1, PREPOWER,
POWER, FUNCT_2, NAT_D, PRE_FF, FIB_NUM, ABIAN;
constructors DOMAIN_1, SQUARE_1, MEMBERED, NEWTON, PREPOWER, POWER, PRE_FF,
NAT_1, NAT_D, ABIAN, FIB_NUM, REAL_1, MCART_1;
registrations SUBSET_1, ORDINAL1, XXREAL_0, XREAL_0, SQUARE_1, NAT_1,
MEMBERED, XCMPLX_0, CARD_1, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, ARITHM;
equalities SQUARE_1;
theorems NAT_1, POWER, PREPOWER, XCMPLX_1, PRE_FF, FIB_NUM, SQUARE_1,
WSIERP_1, NAT_2, ABIAN, FIB_NUM2, XREAL_1, XXREAL_0, ORDINAL1, NAT_D;
schemes FIB_NUM, FIB_NUM2, NAT_1;
begin :: Preliminaries
reserve a,b,n for Element of NAT;
theorem
for a being Real, n being Element of NAT st a to_power n = 0
holds a = 0
proof
let a be Real, n be Element of NAT;
assume a to_power n = 0;
then
A1: a |^ n = 0 by POWER:41;
assume a <> 0;
hence thesis by A1,PREPOWER:5;
end;
theorem Th2:
for a being non negative Real holds (sqrt a) * (sqrt a) = a
proof
let a be non negative Real;
a = sqrt(a^2) by SQUARE_1:22
.= (sqrt a)*(sqrt a) by SQUARE_1:29;
hence thesis;
end;
theorem Th3:
for a being Real holds a to_power 2 = (-a) to_power 2
proof
let a be Real;
2 = 1*2;
then 2 is even by ABIAN:def 2;
hence thesis by POWER:47;
end;
theorem Th4:
for k being non zero Nat holds k-'1+2 = k+2-'1
proof
let k be non zero Nat;
k >= 1 by NAT_2:19;
hence thesis by NAT_D:38;
end;
theorem Th5:
(a+b) |^ 2 = a*a + a*b + a*b + b*b
proof
(a+b)|^2=(a+b)*(a+b) by WSIERP_1:1
.=a*a+a*b+b*a+b*b;
hence thesis;
end;
theorem Th6:
for a being non zero Real holds (a to_power n) to_power 2
= a to_power (2*n)
proof
let a be non zero Real;
((a to_power n)to_power 2)=((a to_power n)to_power(1+1))
.=((a to_power n)to_power 1)*((a to_power n)to_power 1) by FIB_NUM2:5
.=(a to_power n)*((a to_power n)to_power 1) by POWER:25
.=(a to_power n)*(a to_power n) by POWER:25
.=a to_power (n+n) by FIB_NUM2:5
.=a to_power (2*n);
hence thesis;
end;
theorem Th7:
for a, b being Real holds
(a + b)*(a - b) = a to_power 2 - b to_power 2
proof
let a, b be Real;
(a + b)*(a - b) = a^2 - b^2 .= a to_power 2 - b^2 by POWER:46
.= a to_power 2 - b to_power 2 by POWER:46;
hence thesis;
end;
theorem Th8:
for a, b be non zero Real holds
(a*b) to_power n = a to_power n * b to_power n
proof
let a, b be non zero Real;
A1: b #Z n = b to_power n by POWER:43;
(a * b) #Z n = (a * b) to_power n & a #Z n = a to_power n by POWER:43;
hence thesis by A1,PREPOWER:40;
end;
registration
cluster tau -> positive;
coherence by FIB_NUM2:33;
cluster tau_bar -> negative;
coherence by FIB_NUM2:36;
end;
theorem Th9:
for n being Nat holds tau to_power n + tau to_power(n+1) = tau to_power(n+2)
proof
defpred P[Nat] means tau to_power $1 + tau to_power($1+1)= tau to_power($1+2
);
let n be Nat;
A1: tau to_power 0 + tau to_power(0+1) =1+tau to_power(1) by POWER:24
.=1+(1+sqrt 5)/2 by FIB_NUM:def 1,POWER:25
.=(1+sqrt 5+ sqrt 5 + 5)/4
.=(1+sqrt 5+ sqrt 5 + sqrt(5^2))/4 by SQUARE_1:22
.=(1+1*sqrt 5+(sqrt 5)*1+(sqrt 5)*(sqrt 5))/4 by SQUARE_1:29
.=tau*tau by FIB_NUM:def 1
.=(tau to_power 1)*(tau) by POWER:25
.=(tau to_power 1)*(tau to_power 1) by POWER:25
.=(tau)to_power(1+1) by POWER:27
.=tau to_power(0+2);
A2: 1 + tau = 1 + tau to_power 1 by POWER:25
.= tau to_power(0+2) by A1,POWER:24;
A3: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
P[k] and
P[k+1];
tau to_power(k+2) + tau to_power((k+2)+1) =tau to_power(k+2)+(tau
to_power(k+2)*tau to_power(1)) by POWER:27
.=tau to_power(k+2)*(1+tau to_power(1))
.= tau to_power(k+2)* tau to_power(2) by A2,POWER:25
.= tau to_power((k+2)+2) by POWER:27;
hence thesis;
end;
tau to_power 1 + tau to_power(1+1) =tau + (tau)to_power(1+1) by POWER:25
.=tau + (tau to_power 1)*(tau to_power 1) by POWER:27
.=tau + (tau to_power 1)*(tau) by POWER:25
.=tau + (tau)*(tau) by POWER:25
.=tau*(1+tau)
.=(tau to_power(1))*(tau to_power(2)) by A2,POWER:25
.= tau to_power(1+2) by POWER:27;
then
A4: P[1];
A5: P[0] by A1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A4, A3);
hence thesis;
end;
theorem Th10:
for n being Nat holds tau_bar to_power n + tau_bar to_power(n+1)
= tau_bar to_power(n+2)
proof
defpred P[Nat] means tau_bar to_power $1 + tau_bar to_power($1+1)= tau_bar
to_power($1+2);
let n be Nat;
A1: tau_bar to_power 0 + tau_bar to_power(0+1) =1+tau_bar to_power(1) by
POWER:24
.=1+(1-sqrt 5)/2 by FIB_NUM:def 2,POWER:25
.=(1-sqrt 5- sqrt 5 + 5)/4
.=(1-sqrt 5- sqrt 5 + sqrt (5^2))/4 by SQUARE_1:22
.=(1-1*sqrt 5-(sqrt 5)*1+(sqrt 5)*(sqrt 5))/4 by SQUARE_1:29
.=tau_bar*tau_bar by FIB_NUM:def 2
.=(tau_bar to_power 1)*tau_bar by POWER:25
.=(tau_bar to_power 1)*(tau_bar to_power 1) by POWER:25
.=(tau_bar)to_power(1+1) by FIB_NUM2:5
.=tau_bar to_power(0+2);
A2: tau_bar+1= tau_bar + tau_bar to_power 0 by POWER:24
.=tau_bar to_power(2) by A1,POWER:25;
A3: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
P[k] and
P[k+1];
tau_bar to_power(k+2) + tau_bar to_power((k+2)+1) =tau_bar to_power(k+
2)+(tau_bar to_power(k+2)*tau_bar to_power(1)) by FIB_NUM2:5
.=tau_bar to_power(k+2)*(1+tau_bar to_power(1))
.= tau_bar to_power(k+2)* tau_bar to_power(2) by A2,POWER:25
.= tau_bar to_power((k+2)+2) by FIB_NUM2:5;
hence thesis;
end;
tau_bar to_power 1 + tau_bar to_power(1+1) = tau_bar+tau_bar to_power (1
+1) by POWER:25
.=tau_bar+(tau_bar to_power 1)*(tau_bar to_power 1) by FIB_NUM2:5
.=tau_bar+(tau_bar to_power 1)*(tau_bar) by POWER:25
.=tau_bar+tau_bar*tau_bar by POWER:25
.=tau_bar*(1+tau_bar)
.=(tau_bar to_power(1))*(tau_bar to_power(2)) by A2,POWER:25
.= tau_bar to_power(1+2) by FIB_NUM2:5;
then
A4: P[1];
A5: P[0] by A1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A4, A3);
hence thesis;
end;
begin :: Lucas Numbers
deffunc F(set,Element of [: NAT, NAT :]) = [ $2`2, $2`1 + $2`2 ];
definition
func Lucas -> sequence of [:NAT, NAT:] means :Def1:
it.0 = [2,1] &
for n being Nat holds it.(n+1) = [ (it.n)`2, (it.n)`1 + (it.n)`2 ];
existence
proof
consider L being sequence of [: NAT, NAT :] such that
A1: L.0 = [2,1] & for n being Nat holds L.(n+1) = F(n,L.n) from NAT_1:sch 12;
take L;
thus thesis by A1;
end;
uniqueness
proof
let L1,L2 be sequence of [:NAT, NAT:] such that
A3: L1.0 = [2,1] and
A4: for n being Nat holds L1.(n+1) = F(n,(L1.n)) and
A6: L2.0 = [2,1] and
A7: for n being Nat holds L2.(n+1) = F(n,(L2.n));
thus L1 = L2 from NAT_1:sch 16(A3,A4,A6,A7);
end;
end;
definition
let n be Nat;
::$N Lucas numbers
func Lucas(n) -> Element of NAT equals
(Lucas.n)`1;
coherence;
end;
theorem Th11:
Lucas(0) = 2 & Lucas(1) = 1 &
for n being Nat holds Lucas((n+1)+1) = Lucas(n) + Lucas(n+1)
proof
set L = Lucas;
A1: L.0 = [2,1] by Def1;
thus Lucas (0) = [2, 1]`1 by Def1
.= 2;
thus Lucas (1) = (L.(0+1))`1
.= ([ (L.0)`2, (L.0)`1 + (L.0)`2 ])`1 by Def1
.= 1 by A1;
let n be Nat;
A3: (L.(n+1))`1 = [ (L.n)`2, (L.n)`1 + (L.n)`2 ]`1 by Def1
.= (L.n)`2;
thus Lucas((n+1)+1) = [ (L.(n+1))`2, (L.(n+1))`1 + (L.(n+1))`2 ]`1 by Def1
.= [ (L.n)`2, (L.n)`1 + (L.n)`2 ]`2 by Def1
.= Lucas(n) + Lucas(n+1) by A3;
end;
theorem Th12:
for n being Nat holds Lucas(n + 2) = Lucas (n) + Lucas (n+1)
proof
let n be Nat;
thus Lucas(n+2) = Lucas((n+1)+1) .= Lucas(n) + Lucas(n+1) by Th11;
end;
theorem Th13:
for n being Nat holds Lucas(n+1) + Lucas(n+2) = Lucas(n+3)
proof
let n be Nat;
Lucas(n+1) + Lucas(n+2) = Lucas((n+1+1)+1) by Th11
.= Lucas(n+3);
hence thesis;
end;
theorem Th14:
Lucas(2) = 3
proof
Lucas(2) = Lucas(0+1+1) .= 2 + 1 by Th11
.= 3;
hence thesis;
end;
theorem Th15:
Lucas(3) = 4
proof
Lucas(3) = Lucas(1+1+1) .= 3+1 by Th11,Th14
.= 4;
hence thesis;
end;
theorem Th16:
Lucas(4) = 7
proof
Lucas(4) = Lucas(1+1+1+1) .=4+3 by Th11,Th14,Th15
.=7;
hence thesis;
end;
theorem Th17:
for k being Nat holds Lucas(k) >= k
proof
defpred P[Nat] means Lucas($1) >= $1;
A1: P[0];
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A3: P[k] and
A4: P[k+1];
per cases;
suppose
k = 0;
hence thesis by Th14;
end;
suppose
k <> 0;
then
A5: 1 + (k+1) <= k + (k+1) by XREAL_1:6,NAT_1:14;
A6: k + (k+1) <= Lucas(k) + (k+1) by A3,XREAL_1:6;
Lucas((k + 1) + 1) = Lucas(k + 1) + Lucas(k) & Lucas(k) + (k+1) <=
Lucas(k+1 ) + Lucas(k) by A4,Th11,XREAL_1:6;
then k + (k+1) <= Lucas((k+1)+1) by A6,XXREAL_0:2;
hence thesis by A5,XXREAL_0:2;
end;
end;
A7: P[1] by Th11;
thus for k being Nat holds P[k] from FIB_NUM:sch 1 (A1, A7, A2);
end;
theorem
for m being non zero Element of NAT holds Lucas(m+1) >= Lucas(m)
proof
let m be non zero Element of NAT;
thus Lucas(m+1)>=Lucas(m)
proof
defpred P[Nat] means Lucas($1+1) >= Lucas($1);
A1: for k being non zero Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be non zero Nat;
assume that
P[k] and
P[k+1];
Lucas(k+2)+Lucas(k+1)=Lucas(k+3) by Th13;
hence P[k+2] by NAT_1:12;
end;
A2: P[2] by Th14,Th15;
A3: P[1] by Th11,Th14;
for k being non zero Nat holds P[k] from FIB_NUM2:sch 1(A3,A2, A1);
hence thesis;
end;
end;
registration
let n be Element of NAT;
cluster Lucas n -> positive;
coherence
proof
per cases;
suppose
n = 0;
hence thesis by Th11;
end;
suppose
n <> 0;
hence thesis by Th17;
end;
end;
end;
theorem
for n being Element of NAT holds 2 * Lucas(n+2) = Lucas(n) + Lucas(n+3 )
proof
let n be Element of NAT;
A1: Lucas(n+1) + Lucas(n+2) = Lucas(n+3) by Th13;
thus 2 * Lucas(n+2) = Lucas(n+2) + Lucas(n+2)
.= Lucas(n+1) + Lucas(n) + Lucas(n+2) by Th12
.= Lucas(n) + Lucas(n+3) by A1;
end;
theorem
for n being Nat holds Lucas(n+1) = Fib(n) + Fib(n+2)
proof
defpred P[Nat] means Lucas($1 +1)=Fib($1) + Fib($1+2);
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume
A2: ( P[k])& P[k+1];
Fib((k + 2) + 2) = Fib((k+2) + 1 + 1);
then
A3: Fib((k + 2) + 2) = Fib(k+2) + Fib((k+2) + 1) by PRE_FF:1;
Lucas((k+2)+1) = Lucas(k+1) + Lucas((k+1)+1) by Th11
.= Fib(k) + Fib(k+1) + Fib(k+2) + Fib((k+1)+2) by A2
.= Fib((k+1)+1) + Fib(k+2) + Fib((k+1)+2) by PRE_FF:1
.= Fib(k+2) + Fib((k+2)+ 2) by A3;
hence thesis;
end;
0+1+1=2;
then Fib(2) = 1 by PRE_FF:1;
then
A4: P[1] by Th14,PRE_FF:1;
0+1+1=2;
then
A5: P[0] by Th11,PRE_FF:1;
thus for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A4, A1);
end;
theorem Th21: :: Binet Formula for Lucas Numbers
for n being Nat holds Lucas(n) = tau to_power n + tau_bar to_power n
proof
defpred P[Nat] means Lucas($1) = tau to_power $1 + tau_bar to_power $1;
tau_bar to_power 0 = 1 by POWER:24;
then (tau to_power 0) + (tau_bar to_power 0) = (1 + 1) by POWER:24
.= 2;
then
A1: P[0] by Th11;
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A3: P[k] and
A4: P[k+1];
Lucas(k+2)=(tau to_power k + tau_bar to_power k)+Lucas(k+1) by A3,Th12
.=tau to_power k + tau to_power (k+1) + tau_bar to_power k + tau_bar
to_power (k+1) by A4
.=tau to_power (k+2) + tau_bar to_power k + tau_bar to_power (k+1) by Th9
.=tau to_power (k+2) + (tau_bar to_power k + tau_bar to_power (k+1))
.=tau to_power (k+2) + tau_bar to_power (k+2) by Th10;
hence thesis;
end;
tau_bar to_power 1 = tau_bar & tau to_power 1 = tau by POWER:25;
then
A5: P[1] by Th11,FIB_NUM:def 1,def 2;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A1, A5, A2);
hence thesis;
end;
theorem
for n being Nat holds 2 * Lucas(n) + Lucas(n + 1) = 5 * Fib(n + 1)
proof
defpred P[Nat] means 2*Lucas($1)+Lucas($1+1)=5*Fib($1+1);
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A2: P[k] and
A3: P[k+1];
2* Lucas(k+2) + Lucas((k+2)+1) = 2* Lucas(k+2) + Lucas(k+(2+1))
.= 2* Lucas(k+2) + (Lucas(k+1) + Lucas(k+2)) by Th13
.= 2* Lucas(k+2) + Lucas(k+1) + Lucas(k+2)
.= 2* Lucas(k+2) + Lucas(k+1) + (Lucas(k) + Lucas(k+1)) by Th12
.= Lucas(k+2) + (2*Lucas(k+1) + Lucas(k+2)) + Lucas(k)
.= Lucas(k) + Lucas(k+1) + 5*Fib(k+2) + Lucas(k) by A3,Th12
.= 5*Fib(k+1) + 5*Fib(k+2) by A2
.= 5*(Fib(k+1)+Fib(k+(1+1)))
.= 5*Fib(((k+1)+1)+1) by PRE_FF:1
.= 5*Fib((k+2)+1);
hence thesis;
end;
0+1+1=2;
then Fib(2) = 1 by PRE_FF:1;
then
A4: P[1] by Th11,Th14;
A5: P[0] by Th11,PRE_FF:1;
thus for k being Nat holds P[k] from FIB_NUM:sch 1 (A5,A4,A1);
end;
theorem Th23:
for n being Nat holds Lucas(n + 3) - 2 * Lucas(n) = 5 * Fib(n)
proof
defpred P[Nat] means Lucas($1+3)-2*Lucas($1)=5*Fib($1);
A1: P[1] by Th11,Th16,PRE_FF:1;
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A3: P[k] and
A4: P[k+1];
Lucas(k+2+3) - 2*Lucas(k+2)= Lucas(((k+1+1+1)+1)+1) - 2* Lucas(k+2)
.= Lucas(k+3)+Lucas(k+4) - 2* Lucas(k+2) by Th11;
then Lucas(k+2+3) - 2*Lucas(k+2)= Lucas(k+3) + Lucas(k+4) - 2*(Lucas(k) +
Lucas(k+1)) by Th12
.= Lucas(k+4) - 2*Lucas(k+1)+ 5*Fib(k) by A3
.= 5*Fib(k) + 5*Fib(k+1) by A4
.= 5*(Fib(k) + Fib(k+1))
.= 5*Fib(k+1+1) by PRE_FF:1
.= 5*Fib(k+2);
hence thesis;
end;
A5: P[0] by Th11,Th15,PRE_FF:1;
thus for k being Nat holds P[k] from FIB_NUM:sch 1 (A5,A1,A2);
end;
theorem
for n being Nat holds Lucas(n) + Fib(n) = 2 * Fib(n+1)
proof
defpred P[Nat] means Lucas($1)+Fib($1)=2*Fib($1+1);
let n be Nat;
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A2: P[k] and
A3: P[k+1];
Lucas(k+2)+Fib(k+2)= Lucas(k)+Lucas(k+1)+Fib(k+2) by Th12
.= Lucas(k)+Lucas(k+1)+(Fib(k)+Fib(k+1)) by FIB_NUM2:24
.= 2*Fib(k+1)+2*Fib(k+1+1) by A2,A3
.=2*(Fib(k+1)+Fib(k+2))
.=2*Fib(k+3) by FIB_NUM2:25
.=2*Fib((k+2)+1);
hence thesis;
end;
0+1+1=2;
then Fib(2) = 1 by PRE_FF:1;
then
A4: P[1] by Th11,PRE_FF:1;
A5: P[0] by Th11,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A4, A1);
hence thesis;
end;
theorem
for n being Nat holds 3 * Fib(n) + Lucas(n) = 2 * Fib(n+2)
proof
defpred P[Nat] means 3*Fib($1)+Lucas($1)=2*Fib($1+2);
let n be Nat;
0+1+1=2;
then
A1: Fib(2) = 1 by PRE_FF:1;
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume
A3: ( P[k])& P[k+1];
3*Fib(k+2)+Lucas(k+2)= 3*(Fib(k)+Fib(k+1))+Lucas(k+2) by FIB_NUM2:24
.= 3*Fib(k)+3*Fib(k+1)+(Lucas(k)+Lucas(k+1)) by Th12
.= 2*Fib(k+2)+2*Fib((k+1)+2) by A3
.= 2*(Fib(k+2)+Fib((k+2)+1))
.= 2*Fib((k+2)+2) by FIB_NUM2:24;
hence thesis;
end;
0+1+1+1=3;
then Fib(3)=2 by A1,PRE_FF:1;
then
A4: P[1] by Th11,PRE_FF:1;
A5: P[0] by A1,Th11,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A4, A2);
hence thesis;
end;
theorem
for n,m being Element of NAT holds 2 * Lucas(n + m) = Lucas(n) * Lucas
(m) + 5 * Fib(n) * Fib(m)
proof
defpred P[Nat] means for n holds 2* Lucas(n + $1) = Lucas(n)*Lucas($1) + 5*
Fib(n)* Fib($1);
A1: now
let k be Nat;
assume that
A2: P[k] and
A3: P[k+1];
thus P[k+2]
proof
let n;
A4: 2* Lucas(n + (k+1)) = Lucas(n)*Lucas(k+1) + 5*Fib(n)* Fib(k+1) by A3;
2* Lucas(n+(k+2))=2*Lucas(n+k+2) .= 2*(Lucas(n+k)+Lucas((n+k)+1)) by Th12
.= 2*Lucas(n+k)+2*Lucas(n+k+1)
.= (Lucas(n)*Lucas(k) + 5*Fib(n)* Fib(k)) + 2*Lucas(n+(k+1)) by A2
.= Lucas(n)*(Lucas(k) + Lucas(k+1))+5*Fib(n)* (Fib(k) + Fib(k+1)) by A4
.= Lucas(n)*Lucas(k+2) + 5*Fib(n)*(Fib(k) + Fib(k+1)) by Th12
.= Lucas(n)*Lucas(k+2) + 5*Fib(n)* Fib(k+2) by FIB_NUM2:24;
hence thesis;
end;
end;
A5: P[1]
proof
let n be Element of NAT;
2*Lucas(n + 1) = Lucas(n+1)+Lucas(n)+Lucas(n+1)-Lucas(n)
.= Lucas(n+1)+Lucas(n+2)-Lucas(n) by Th12
.= Lucas(n+3)-Lucas(n) by Th13
.= Lucas(n) + (Lucas(n + 3) - 2* Lucas(n))
.= Lucas(n)*Lucas(1) + 5*Fib(n)* Fib(1) by Th11,Th23,PRE_FF:1;
hence thesis;
end;
A6: P[0] by Th11,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A6, A5, A1);
hence thesis;
end;
theorem
for n being Element of NAT holds Lucas(n + 3) * Lucas(n) = (Lucas(n +
2))|^2 - (Lucas(n+1))|^2
proof
defpred P[Nat] means Lucas($1 + 3) * Lucas($1) = (Lucas($1 + 2))|^2 - (Lucas
($1+1))|^2;
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
P[k] and
P[k+1];
Lucas((k+2)+3)* Lucas(k+2)=Lucas((k+3)+2)*Lucas(k+2)
.=(Lucas(k+3)+Lucas((k+3)+1))*Lucas(k+2) by Th12
.=(Lucas(k+3)+Lucas((k+2)+2))*Lucas(k+2)
.=(Lucas(k+3)+(Lucas(k+2)+Lucas((k+2)+1)))*Lucas(k+2) by Th12
.=(Lucas(k+2)+Lucas(k+3))*(Lucas(k+2)+Lucas((k+2)+1))- Lucas(k+3)*
Lucas(k+3)
.=(Lucas(k+2)+Lucas(k+3))*Lucas((k+2)+2)-Lucas(k+3)*Lucas(k+3) by Th12
.=(Lucas(k+2)+Lucas((k+2)+1))*Lucas(k+4)-Lucas(k+3)*Lucas(k+3)
.=Lucas((k+2)+2)*Lucas(k+4)-Lucas(k+3)*Lucas(k+3) by Th12
.=Lucas(k+4)*Lucas(k+4)-(Lucas(k+3))|^2 by WSIERP_1:1
.=(Lucas((k+2)+2))|^2-(Lucas((k+2)+1))|^2 by WSIERP_1:1;
hence thesis;
end;
Lucas(1 + 3) * Lucas(1) = 4*4 - 3*3 by Th11,Th16
.= 4*4 - 3|^2 by WSIERP_1:1
.= (Lucas(1 + 2))|^2 - (Lucas(1+1))|^2 by Th14,Th15,WSIERP_1:1;
then
A2: P[1];
(Lucas(0 + 2))|^2 - (Lucas(0+1))|^2 = 3*3 - (Lucas(1))|^2 by Th14,WSIERP_1:1
.= 9-1*1 by Th11,WSIERP_1:1
.= Lucas(0+3) * Lucas(0) by Th11,Th15;
then
A3: P[0];
for k being Nat holds P[k] from FIB_NUM:sch 1 (A3, A2, A1);
hence thesis;
end;
theorem Th28:
for n being Nat holds Fib(2*n) = Fib(n) * Lucas(n)
proof
let n be Nat;
A1: n in NAT by ORDINAL1:def 12;
Fib(n)*Lucas(n)= (((tau to_power n) - (tau_bar to_power n))/(sqrt 5))*
Lucas(n) by FIB_NUM:7
.=(((tau to_power n) - (tau_bar to_power n))/(sqrt 5)) * (tau to_power n
+ tau_bar to_power n) by Th21
.=( tau to_power n + tau_bar to_power n)* ( tau to_power n - tau_bar
to_power n)/(sqrt 5) by XCMPLX_1:74
.=((tau to_power n)to_power 2 - (tau_bar to_power n)to_power 2)/(sqrt 5)
by Th7
.=((tau to_power n)to_power 2 - tau_bar to_power (2*n))/(sqrt 5) by A1,Th6
.= (tau to_power (2*n) - tau_bar to_power (2*n))/(sqrt 5) by POWER:33
.=Fib(2*n) by FIB_NUM:7;
hence thesis;
end;
theorem
for n being Element of NAT holds 2 * Fib(2*n+1) = Lucas(n+1) * Fib(n)
+ Lucas(n) * Fib(n+1)
proof
defpred P[Nat] means 2*Fib(2*$1+1)= Lucas($1+1)*Fib($1)+Lucas($1)*Fib($1+1);
0+1+1=2;
then
A1: Fib(2) = 1 by PRE_FF:1;
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A3: P[k] and
A4: P[k+1];
set f2 = Fib(k+2);
set f1 = Fib(k+1);
set f = Fib(k);
set l2 = Lucas(k+2);
set l1 = Lucas(k+1);
set l = Lucas(k);
A5: 2*Fib(2*k)=2*(Fib(2*k+2)-Fib(2*k+1)) by FIB_NUM2:30
.=2*(Fib((2*k+1)+1)-Fib(2*k+1))
.=2*((Fib((2*k+1)+2)-Fib(2*k+1))-Fib(2*k+1)) by FIB_NUM2:29
.=2*Fib(2*k+3)-2*(2*Fib(2*k+1))
.=l2*f1 + l1*f2 - 2*(Lucas(k+1)*Fib(k)+Lucas(k)*Fib(k+1)) by A3,A4
.=l2*f1 + l1*f2 - 2*l1*f - 2*l*f1
.=(l+l1)*f1 + l1*f2 - 2*l1*f - 2*l*f1 by Th12
.=l*f1 + l1*f1 + l1*(f+f1) - 2*l1*f - 2*l*f1 by FIB_NUM2:24
.=2*l1*f1 - l*f1 - l1*f;
2*Fib(2*(k+2)+1)=2*(Fib((2*k+3)+2))
.=2*(Fib(2*k+3)+Fib((2*k+3)+1)) by FIB_NUM2:24
.=2*(Fib(2*k+3)+Fib((2*k+2)+2))
.=2*(Fib(2*k+3)+(Fib(2*k+2)+Fib((2*k+2)+1) ) ) by FIB_NUM2:24
.=2*(Fib(2*k+3)+Fib((2*k+1)+1)+Fib(2*k+3))
.=2*(Fib(2*k+3)+(Fib((2*k+1)+2)-Fib(2*k+1))+Fib(2*k+3)) by FIB_NUM2:29
.=3*(2*Fib(2*k+3))-2*Fib(2*k+1)
.=3*(Lucas(k+2)*Fib(k+1)+Lucas(k+1)*Fib(k+2))-2*Fib(2*k+1) by A4
.=3*l2*f1+3*l1*f2-l1*f-l*f1 by A3
.=3*(l+l1)*f1+3*l1*f2-l1*f-l*f1 by Th12
.=(3*l+3*l1)*f1+3*l1*(f+f1)-l1*f-l*f1 by FIB_NUM2:24
.=3*l*f1 + 4*l1*f1 + 3*l1*f + (2*l1*f1 - l*f1 - l1*f)
.=3*l*f1 + 4*l1*f1 + 3*l1*f + 2*(l*f) by A5,Th28
.=l*f1+l1*f1+l1*(f+f1)+2*l*f+2*l*f1+2*l1*f+2*l1*f1
.=(l+l1)*f1+l1*f2+2*l*f+2*l*f1+2*l1*f+2*l1*f1 by FIB_NUM2:24
.=l2*f1+l1*f2+2*l*f+2*l*f1+2*l1*f+2*l1*f1 by Th12
.=Lucas(k+2)*Fib(k+1)+Lucas(k+1)*Fib(k+2)+2*(l*f+l*f1+l1*f+l1*f1)
.=2*Fib(2*k+3)+2*(l*f+l*f1+l1*f+l1*f1) by A4
.=2*(Fib(2*k+3)+(Lucas(k)+Lucas(k+1))*(Fib(k)+Fib(k+1)))
.=2*(Fib(2*k+3)+(Lucas(k)+Lucas(k+1))*Fib(k+2)) by FIB_NUM2:24
.=2*(Fib(2*k+3)+Lucas(k+2)*Fib(k+2)) by Th12
.=2*Fib(2*k+3)+Lucas(k+2)*Fib(k+2)+Lucas(k+2)*Fib(k+2)
.=(Lucas(k+1)*Fib(k+2)+Lucas(k+2)*Fib(k+1))+ Lucas(k+2)*Fib(k+2)+Lucas
(k+2)*Fib(k+2) by A4
.=(Lucas(k+1)+Lucas(k+2))*Fib(k+2)+Lucas(k+2)*(Fib(k+1)+Fib(k+2))
.=(Lucas(k+1)+Lucas((k+1)+1))*Fib(k+2)+Lucas(k+2)*Fib((k+1)+2) by
FIB_NUM2:24
.=Lucas((k+2)+1)*Fib(k+2)+Lucas(k+2)*Fib((k+2)+1) by Th12;
hence thesis;
end;
1+1+1=3;
then 2*Fib(2*1+1)=2*2 by A1,PRE_FF:1
.=Lucas(1+1)*Fib(1)+Lucas(1)*Fib(1+1) by A1,Th11,Th14,PRE_FF:1;
then
A6: P[1];
A7: P[0] by Th11,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A7, A6, A2);
hence thesis;
end;
theorem
for n being Element of NAT holds 5 * (Fib(n)) |^ 2 - (Lucas(n)) |^ 2 =
4 * (-1) to_power (n+1)
proof
let n be Element of NAT;
set a = (tau to_power n);
set b = (tau_bar to_power n);
A1: (Fib(n))|^2=(Fib(n)*Fib(n)) by WSIERP_1:1
.=(((tau to_power n)-(tau_bar to_power n))/(sqrt 5))*Fib(n) by FIB_NUM:7
.=(((tau to_power n)-(tau_bar to_power n))/(sqrt 5)) *(((tau to_power n)
-(tau_bar to_power n))/(sqrt 5)) by FIB_NUM:7
.=((a - b)*(a - b))/(sqrt 5 * sqrt 5) by XCMPLX_1:76
.=(a*a -2*a*b + b*b)/5 by Th2;
A2: a*b=(tau*tau_bar)to_power n by Th8
.=((1*1-(sqrt 5 * sqrt 5))/4) to_power n by FIB_NUM:def 1,def 2
.=((1-5)/4) to_power n by Th2
.=(-1)to_power n;
(Lucas(n))|^2=(Lucas(n)*Lucas(n)) by WSIERP_1:1
.=(tau to_power n + tau_bar to_power n)*(Lucas(n)) by Th21
.=(tau to_power n + tau_bar to_power n)* (tau to_power n + tau_bar
to_power n) by Th21
.=a*a+2*a*b+b*b;
then 5*(Fib(n))|^2-(Lucas(n))|^2=4*(-1)*(-1)to_power n by A1,A2
.=4*((-1)to_power 1)*(-1)to_power n by POWER:25
.=4*(((-1)to_power 1)*(-1)to_power n)
.=4*(-1)to_power(n+1) by FIB_NUM2:5;
hence thesis;
end;
theorem
for n being Element of NAT holds Fib(2*n+1) = Fib(n+1) * Lucas(n+1) -
Fib(n) * Lucas(n)
proof
let n be Element of NAT;
Fib(n+1) * Lucas(n+1) - Fib(n) * Lucas(n) = Fib(2*(n+1)) - Fib(n)* Lucas
(n) by Th28
.= Fib((2*n)+2) - Fib(2*n) by Th28
.= Fib((2*n)+1) by FIB_NUM2:29;
hence thesis;
end;
begin :: Generalized Fibonacci Numbers
definition
let a,b be Nat;
redefine func [a,b] -> Element of [:NAT,NAT:]; :: redefines [ (TARSKI, definition)
coherence
proof
reconsider a,b as Element of NAT by ORDINAL1:def 12;
[a,b] is Element of [:NAT,NAT:];
hence thesis;
end;
end;
definition
let a,b be Nat;
deffunc F(set,Element of [: NAT, NAT :]) = [ $2`2, $2`1 + $2`2 ];
func GenFib (a,b) -> sequence of [:NAT, NAT:] means :Def2:
it.0 = [a,b] &
for n being Nat holds it.(n+1) = [ (it.n)`2, (it.n)`1 + (it.n)`2 ];
existence
proof
consider L being sequence of [: NAT, NAT :] such that
A1: L.0 = [a,b] & for n being Nat holds L.(n+1) = F(n,L.n) from NAT_1:sch 12;
take L;
thus thesis by A1;
end;
uniqueness
proof
let L1,L2 be sequence of [:NAT, NAT:] such that
A3: L1.0 = [a,b] and
A4: for n being Nat holds L1.(n+1) = F(n,L1.n) and
A6: L2.0 = [a,b] and
A7: for n being Nat holds L2.(n+1) = F(n,L2.n);
thus L1 = L2 from NAT_1:sch 16(A3,A4,A6,A7);
end;
end;
definition
let a,b,n be Nat;
func GenFib (a,b,n) -> Element of NAT equals
(GenFib(a,b).n)`1;
coherence;
end;
theorem Th32:
for a,b being Nat holds GenFib(a,b,0) = a & GenFib(a,b,1) = b &
for n being Nat holds GenFib(a,b,(n+1)+1) = GenFib(a,b,n) + GenFib(a,b,n+1)
proof
deffunc F(set,Element of [: NAT, NAT :]) = [ $2`2, $2`1 + $2`2 ];
let a, b be Nat;
consider L being sequence of [: NAT, NAT :] such that
A1: L.0 = [a,b] and
A2: for n being Nat holds L.(n+1) = F(n,L.n) from NAT_1:sch 12;
thus GenFib(a,b,0) = [a, b]`1 by Def2
.= a;
thus GenFib(a,b,1) = (L.(0+1))`1 by A1,A2,Def2
.= ([ (L.0)`2, (L.0)`1 + (L.0)`2 ])`1 by A2
.= b by A1;
let n be Nat;
A3: (L.(n+1))`1 = [ (L.n)`2, (L.n)`1 + (L.n)`2 ]`1 by A2
.= (L.n)`2;
GenFib(a,b,(n+1)+1) = (L.((n+1)+1))`1 by A1,A2,Def2
.= [ (L.(n+1))`2, (L.(n+1))`1 + (L.(n+1))`2 ]`1 by A2
.= [ (L.n)`2, (L.n)`1 + (L.n)`2 ]`2 by A2
.= GenFib(a,b,n) + (L.(n+1))`1 by A1,A2,A3,Def2
.= GenFib(a,b,n) + GenFib(a,b,n+1) by A1,A2,Def2;
hence thesis;
end;
theorem Th33:
for k being Nat holds (GenFib(a,b,k+1)+GenFib(a,b,(k+1)+1)) |^ 2
= (GenFib(a,b,k+1)|^2+2*GenFib(a,b,k+1) * GenFib(a,b,(k+1)+1)+GenFib(a,b,(k+1)+
1)|^2)
proof
let k be Nat;
set a1 = GenFib(a,b,k+1);
set b1 = GenFib(a,b,(k+1)+1);
(GenFib(a,b,k+1)+GenFib(a,b,(k+1)+1))|^2 =a1*a1+a1*b1+b1*a1+b1*b1 by Th5
.=a1*a1+2*(a1*b1)+b1*b1
.=a1|^2+2*a1*b1+b1*b1 by WSIERP_1:1
.=a1|^2+2*a1*b1+b1|^2 by WSIERP_1:1;
hence thesis;
end;
theorem Th34:
for a,b,n being Nat holds GenFib(a,b,n) + GenFib(a,b,n+1) = GenFib(a,b,n+2)
proof
let a,b,n be Nat;
GenFib(a,b,n) + GenFib(a,b,n+1) = GenFib(a,b,n+1+1) by Th32
.= GenFib(a,b,n+2);
hence thesis;
end;
theorem Th35:
for a,b,n being Nat holds GenFib(a,b,n+1) + GenFib(a,b,n+2) =
GenFib(a,b,n + 3)
proof
let a,b,n be Nat;
GenFib(a,b,n+1) + GenFib(a,b,n+2)= GenFib(a,b,((n+1)+1)+1) by Th32
.= GenFib(a,b,n + 3);
hence thesis;
end;
theorem Th36:
for a,b,n being Element of NAT holds GenFib(a,b,n+2) + GenFib(a,
b,n+3) = GenFib(a,b,n + 4)
proof
let a,b,n be Element of NAT;
GenFib(a,b,n+2) + GenFib(a,b,n+3) = GenFib(a,b,(((n+1)+1)+1)+1) by Th32
.= GenFib(a,b,n + 4);
hence thesis;
end;
theorem
for n being Element of NAT holds GenFib(0,1,n) = Fib(n)
proof
defpred P[Nat] means GenFib(0,1,$1) = Fib($1);
A1: P[1] by Th32,PRE_FF:1;
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume ( P[k])& P[k+1];
then GenFib(0,1,k+2)=Fib(k)+Fib(k+1) by Th34
.=Fib(k+2) by FIB_NUM2:24;
hence thesis;
end;
A3: P[0] by Th32,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A3, A1, A2);
hence thesis;
end;
theorem Th38:
for n being Element of NAT holds GenFib(2,1,n) = Lucas(n)
proof
defpred P[Nat] means GenFib(2,1,$1)=Lucas($1);
A1: P[1] by Th11,Th32;
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume ( P[k])& P[k+1];
then GenFib(2,1,k+2)= Lucas(k)+Lucas(k+1) by Th34
.= Lucas(k+2) by Th12;
hence thesis;
end;
A3: P[0] by Th11,Th32;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A3, A1, A2);
hence thesis;
end;
theorem Th39:
for a,b,n being Element of NAT holds GenFib(a,b,n) + GenFib(a,b,
n + 3) = 2*GenFib(a,b,n + 2)
proof
let a,b,n be Element of NAT;
GenFib(a,b,n)+GenFib(a,b,n+3)= GenFib(a,b,n)+(GenFib(a,b,n+1)+GenFib(a,b
,n+2)) by Th35
.= GenFib(a,b,n) + GenFib(a,b,n+1) + GenFib(a,b,n+2)
.= GenFib(a,b,n+2)+ GenFib(a,b,n+2) by Th34
.= 2*GenFib(a,b,n + 2);
hence thesis;
end;
theorem
for a,b,n being Element of NAT holds GenFib(a,b,n) + GenFib(a,b,n + 4)
= 3*GenFib(a,b,n + 2)
proof
let a,b,n be Element of NAT;
GenFib(a,b,n) + GenFib(a,b,n + 4) = GenFib(a,b,n)+(GenFib(a,b,n+2) +
GenFib(a,b,n+3)) by Th36
.=GenFib(a,b,n) + GenFib(a,b,n+2) + GenFib(a,b,n+3)
.=GenFib(a,b,n) + GenFib(a,b,n+2) + (GenFib(a,b,n+1)+ GenFib(a,b,n+2))
by Th35
.=GenFib(a,b,n) + GenFib(a,b,n+1)+ GenFib(a,b,n+2)+ GenFib(a,b,n+2)
.=GenFib(a,b,n+2) + GenFib(a,b,n+2) + GenFib(a,b,n+2) by Th34
.= 3*GenFib(a,b,n + 2);
hence thesis;
end;
theorem
for a,b,n being Element of NAT holds GenFib(a,b,n + 3) - GenFib(a,b,n)
= 2*GenFib(a,b,n +1)
proof
let a,b,n be Element of NAT;
GenFib(a,b,n + 3) - GenFib(a,b,n) = GenFib(a,b,n+1)+ GenFib(a,b,n+2)-
GenFib(a,b,n) by Th35
.=GenFib(a,b,n+1)+ (GenFib(a,b,n)+GenFib(a,b,n+1))- GenFib(a,b,n) by Th34
.= 2*GenFib(a,b,n +1);
hence thesis;
end;
theorem
for a,b,n being non zero Element of NAT holds GenFib(a,b,n) = GenFib(
a,b,0)*Fib(n-'1) + GenFib(a,b,1)*Fib(n)
proof
let a,b,n be non zero Element of NAT;
thus GenFib(a,b,n)=GenFib(a,b,0)*Fib(n-'1)+GenFib(a,b,1)*Fib(n)
proof
defpred P[Nat] means GenFib(a,b,$1) = GenFib(a,b,0)* Fib($1-'1)+GenFib(a,b
,1)* Fib($1);
GenFib(a,b,1) = GenFib(a,b,0)* Fib(0)+GenFib(a,b,1)* Fib(1) by PRE_FF:1
.= GenFib(a,b,0)* Fib(1-'1)+GenFib(a,b,1)* Fib(1) by XREAL_1:232;
then
A1: P[1];
A2: for k being non zero Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be non zero Nat;
assume that
A3: P[k] and
A4: P[k+1];
1 <= k by NAT_2:19;
then
A5: Fib(k-'1)+Fib((k+1)-'1) = Fib(k-'1)+Fib(k-'1+1) by NAT_D:38
.= Fib(k-'1+1+1) by PRE_FF:1
.= Fib(k-'1+2)
.= Fib(k+2-'1) by Th4;
GenFib(a,b,k+2) =GenFib(a,b,0)* Fib(k-'1)+GenFib(a,b,1)* Fib(k) +
GenFib(a,b,k+1) by A3,Th34
.=a*Fib(k-'1)+GenFib(a,b,1)* Fib(k) + GenFib(a,b,k+1) by Th32
.=a*Fib(k-'1)+b* Fib(k) + GenFib(a,b,k+1) by Th32
.=a*Fib(k-'1)+b* Fib(k) + GenFib(a,b,0)* Fib((k+1)-'1)+ GenFib(a,b,1
)* Fib(k+1) by A4
.=a*Fib(k-'1)+b* Fib(k) + a* Fib((k+1)-'1)+ GenFib(a,b,1)* Fib(k+1)
by Th32
.=a*Fib(k-'1)+b* Fib(k) + a* Fib((k+1)-'1)+b* Fib(k+1) by Th32
.=a*(Fib(k-'1)+Fib((k+1)-'1))+b*(Fib(k)+ Fib(k+1))
.=a*Fib((k+2)-'1)+b*Fib(k+2) by A5,FIB_NUM2:24
.=a*Fib((k+2)-'1)+GenFib(a,b,1)* Fib(k+2) by Th32
.=GenFib(a,b,0)* Fib((k+2)-'1)+GenFib(a,b,1)* Fib(k+2) by Th32;
hence thesis;
end;
0+1+1=2;
then
A6: Fib(2)=1 by PRE_FF:1;
GenFib(a,b,2)=GenFib(a,b,0+2)
.= GenFib(a,b,0)* Fib(1+0)+GenFib(a,b,1)* Fib(2) by A6,Th34,PRE_FF:1
.= GenFib(a,b,0)* Fib(1+(1-'1))+GenFib(a,b,1)* Fib(2) by XREAL_1:232
.= GenFib(a,b,0)* Fib(1+1-'1)+GenFib(a,b,1)* Fib(2) by NAT_D:38
.= GenFib(a,b,0)* Fib(2-'1)+GenFib(a,b,1)* Fib(2);
then
A7: P[2];
for k being non zero Nat holds P[k] from FIB_NUM2:sch 1(A1,A7, A2);
hence thesis;
end;
end;
theorem
for n,m being Nat holds Fib(m) * Lucas(n) + Lucas(m) * Fib(n) = GenFib
(Fib(0),Lucas(0),n+m)
proof
let n,m be Nat;
defpred P[Nat] means Fib($1)* Lucas(n) + Lucas($1)* Fib(n) = GenFib(Fib(0),
Lucas(0),n+$1);
2*Fib(n)= GenFib(0,2,n)
proof
defpred R[Nat] means 2* Fib($1)= GenFib(0,2,$1);
A1: R[1] by Th32,PRE_FF:1;
A2: for i being Nat st R[i] & R[i+1] holds R[i+2]
proof
let i be Nat;
assume
A3: ( R[i])& R[i+1];
2* Fib(i+2)=2*(Fib(i)+Fib(i+1)) by FIB_NUM2:24
.=2* Fib(i)+2* Fib(i+1)
.= GenFib(0,2,i+2) by A3,Th34;
hence thesis;
end;
A4: R[0] by Th32,PRE_FF:1;
for i being Nat holds R[i] from FIB_NUM:sch 1 (A4, A1, A2);
hence thesis;
end;
then
A5: P[0] by Th11,PRE_FF:1;
Lucas(n) + Fib(n) = GenFib(0,2,n+1)
proof
defpred Q[Nat] means Lucas($1) + Fib($1) = GenFib(0,2,$1+1);
A6: for j being Nat st Q[j] & Q[j+1] holds Q[j+2]
proof
let j be Nat;
assume
A7: ( Q[j])& Q[j+1];
Lucas(j+2) + Fib(j+2)=Lucas(j)+Lucas(j+1)+Fib(j+2) by Th12
.=Lucas(j)+Lucas(j+1)+(Fib(j) +Fib(j+1)) by FIB_NUM2:24
.=GenFib(0,2,j+1)+ GenFib(0,2,j+2) by A7
.=GenFib(0,2,j+3) by Th35
.=GenFib(0,2,(j+2)+1);
hence thesis;
end;
Lucas(1) + Fib(1)= 0+ GenFib(0,2,1) by Th11,Th32,PRE_FF:1
.= GenFib(0,2,0+0)+ GenFib(0,2,0+1) by Th32
.= GenFib(0,2,0+2) by Th34
.= GenFib(0,2,1+1);
then
A8: Q[1];
A9: Q[0] by Th11,Th32,PRE_FF:1;
for j being Nat holds Q[j] from FIB_NUM:sch 1 (A9, A8, A6);
hence thesis;
end;
then
A10: P[1] by Th11,PRE_FF:1;
A11: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume
A12: ( P[k])& P[k+1];
Fib(k+2)* Lucas(n) + Lucas(k+2)* Fib(n) = (Fib(k)+Fib(k+1))* Lucas(n)
+ Lucas(k+2)* Fib(n) by FIB_NUM2:24
.=Fib(k)*Lucas(n)+Fib(k+1)* Lucas(n) + (Lucas(k)+Lucas(k+1))* Fib(n)
by Th12
.= GenFib(0,2,(n+k))+GenFib(0,2,(n+k)+1) by A12,Th11,PRE_FF:1
.= GenFib(0,2,(n+k)+2) by Th34
.= GenFib(Fib(0),Lucas(0),n+(k+2)) by Th11,PRE_FF:1;
hence thesis;
end;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A10, A11);
hence thesis;
end;
theorem
for n being Element of NAT holds Lucas(n) + Lucas(n + 3) = 2*Lucas(n + 2)
proof
let n be Element of NAT;
A1: 2*GenFib(2,1,n + 2)=2*Lucas(n+2) by Th38;
GenFib(2,1,n)= Lucas(n) & GenFib(2,1,n + 3) =Lucas(n+3) by Th38;
hence thesis by A1,Th39;
end;
theorem
for a,n being Element of NAT holds GenFib(a,a,n) = ((GenFib(a,a,0)) /
2) * (Fib(n) + Lucas(n))
proof
let a,b be Element of NAT;
defpred P[Nat] means GenFib(a,a,$1)=((GenFib(a,a,0))/2)*(Fib($1)+Lucas($1));
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A2: P[k] and
A3: P[k+1];
GenFib(a,a,k+2)=((GenFib(a,a,0))/2)*(Fib(k)+Lucas(k))+GenFib(a,a,k+1)
by A2,Th34
.=((GenFib(a,a,0))/2)*(Fib(k)+Fib(k+1)+(Lucas(k)+Lucas(k+1))) by A3
.=((GenFib(a,a,0))/2)*(Fib(k+2)+(Lucas(k)+Lucas(k+1))) by FIB_NUM2:24
.=((GenFib(a,a,0))/2)*(Fib(k+2)+Lucas(k+2)) by Th12;
hence thesis;
end;
GenFib(a,a,1)=a by Th32;
then
A4: P[1] by Th11,Th32,PRE_FF:1;
A5: P[0] by Th11,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A4, A1);
hence thesis;
end;
theorem
for a,b,n being Element of NAT holds GenFib(b,a+b,n) = GenFib(a,b,n+1)
proof
let a,b,n be Element of NAT;
defpred P[Nat] means GenFib(b,a+b,$1) = GenFib(a,b,$1+1);
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume ( P[k])& P[k+1];
then GenFib(b,a+b,k+2) = GenFib(a,b,k+1) + GenFib(a,b,k+2) by Th34
.= GenFib(a,b,k+3) by Th35
.= GenFib(a,b,((k+2)+1));
hence thesis;
end;
GenFib(b,a+b,0)=b by Th32
.=GenFib(a,b,0+1) by Th32;
then
A2: P[0];
GenFib(b,a+b,1)=a+b by Th32
.=a+GenFib(a,b,1) by Th32
.=GenFib(a,b,0)+GenFib(a,b,0+1) by Th32
.=GenFib(a,b,0+2) by Th34
.=GenFib(a,b,1+1);
then
A3: P[1];
for k being Nat holds P[k] from FIB_NUM:sch 1 (A2, A3, A1);
hence thesis;
end;
theorem
for a,b,n being Element of NAT holds GenFib(a,b,n+2) * GenFib(a,b,n) -
GenFib(a,b,n+1)|^2 = ((-1)to_power n) * (GenFib(a,b,2)|^2 - GenFib(a,b,1) *
GenFib(a,b,3))
proof
let a,b,n be Element of NAT;
defpred P[Nat] means GenFib(a,b,$1+2)* GenFib(a,b,$1)-GenFib(a,b,$1+1)|^2 =(
(-1)to_power $1)*(GenFib(a,b,2)|^2-GenFib(a,b,1)*GenFib(a,b,3));
A1: GenFib(a,b,2)=GenFib(a,b,0+2) .=GenFib(a,b,0)+GenFib(a,b,0+1) by Th34
.=a+GenFib(a,b,1) by Th32
.=a+b by Th32;
A2: GenFib(a,b,3)=GenFib(a,b,(1+2)) .=GenFib(a,b,1)+GenFib(a,b,1+1) by Th32
.=b+(a+b) by A1,Th32
.=2*b+a;
then
GenFib(a,b,1+2)* GenFib(a,b,1)-GenFib(a,b,1+1)|^2 =(2*b+a)*b-(a+b)|^2 by A1
,Th32
.=2*b*b+a*b-((a+b)*(a+b)) by WSIERP_1:1
.=(-1)*(((a+b)*(a+b))-b*(2*b+a))
.=((-1)to_power 1)*(((a+b)*(a+b))-b*(2*b+a)) by POWER:25
.=((-1)to_power 1)*((a+b)|^2-b*GenFib(a,b,3)) by A2,WSIERP_1:1
.=((-1)to_power 1)*(GenFib(a,b,2)|^2-GenFib(a,b,1)*GenFib(a,b,3)) by A1
,Th32;
then
A3: P[1];
A4: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A5: P[k] and
A6: P[k+1];
set d = GenFib(a,b,k+2)*GenFib(a,b,k);
A7: (-1)to_power(k+1)+((-1)to_power k)= ((-1)to_power(k)*(-1)to_power (1)
)+(-1)to_power k by FIB_NUM2:5
.=(-1)to_power(k)*(-1)+(-1)to_power k by POWER:25
.=0;
GenFib(a,b,2)|^2= GenFib(a,b,0+2)|^2
.=(GenFib(a,b,0)+GenFib(a,b,0+1))|^2 by Th34
.=(a+GenFib(a,b,1))|^2 by Th32
.=(a+b)|^2 by Th32;
then
A8: GenFib(a,b,2)|^2-GenFib(a,b,1)*GenFib(a,b,3)=(a+b)|^2-b*GenFib(a,b, 1
+2 ) by Th32
.=(a+b)|^2-b*(GenFib(a,b,1)+GenFib(a,b,1+1)) by Th34
.=(a+b)|^2-b*(b+GenFib(a,b,0+2)) by Th32
.=(a+b)|^2-b*(b+(GenFib(a,b,0)+GenFib(a,b,0+1))) by Th34
.=(a+b)|^2-b*(b+(a+GenFib(a,b,1))) by Th32
.=(a+b)|^2-b*(b+(a+b)) by Th32
.=(a+b)|^2-b*b-b*a-b*b
.=(a*a+a*b+b*a+b*b)-b*b-b*a-b*b by Th5
.=a*a+a*b-b*b;
then d-GenFib(a,b,k+1)|^2 = ((-1)to_power k)*(a*a+a*b-b*b) by A5;
then
A9: (((-1) to_power (k+1))*(a*a+a*b-b*b))+(d-GenFib(a,b,k+1)|^2) = (((-1)
to_power (k+1))+((-1)to_power k))*(a*a+a*b-b*b)
.= (a*a+a*b-b*b)*0 by A7;
set c = GenFib(a,b,(k+2)+1)*GenFib(a,b,k+1);
A10: c-GenFib(a,b,(k+1)+1)|^2=((-1)to_power (k+1))*(GenFib(a,b,2)|^2 -
GenFib(a,b,1)*GenFib(a,b,3)) by A6;
A11: c+d-(GenFib(a,b,k+1)+GenFib(a,b,(k+1)+1))|^2 =c+d-(GenFib(a,b,k+1)|^2
+2*GenFib(a,b,k+1)*GenFib(a,b,(k+1)+1)+ GenFib(a,b,(k+1)+1)|^2) by Th33
.=((-1)to_power (k+1))*(GenFib(a,b,2)|^2 -GenFib(a,b,1)*GenFib(a,b,3))
+d-GenFib(a,b,k+1)|^2-2*GenFib(a,b,k+1)* GenFib(a,b,(k+1)+1) by A10
.=(((-1)to_power (k+1))*(a*a+a*b-b*b)) +d-GenFib(a,b,k+1)|^2-2*GenFib(
a,b,k+1)*GenFib(a,b,(k+1)+1) by A8
.=-2*GenFib(a,b,k+1)*GenFib(a,b,(k+1)+1) by A9;
GenFib(a,b,(k+2)+2)*GenFib(a,b,k+2)-GenFib(a,b,(k+2)+1)|^2 =(GenFib(a
,b,k+2)+GenFib(a,b,(k+2)+1))*GenFib(a,b,k+2)- GenFib(a,b,(k+2)+1)|^2 by Th34
.=(GenFib(a,b,(k+2)+1)+GenFib(a,b,k+2))*(GenFib(a,b,k)+ GenFib(a,b,k+1
)) -GenFib(a,b,(k+1)+2)|^2 by Th34
.=(GenFib(a,b,(k+2)+1)*GenFib(a,b,k)+c+d+GenFib(a,b,k+2)* GenFib(a,b,k
+1)) -(GenFib(a,b,k+1)+GenFib(a,b,(k+1)+1))|^2 by Th32
.=GenFib(a,b,(k+2)+1)*GenFib(a,b,k)+GenFib(a,b,k+2)* GenFib(a,b,k+1)+(
c+d -(GenFib(a,b,k+1)+GenFib(a,b,(k+1)+1))|^2)
.=GenFib(a,b,(k+2)+1)*GenFib(a,b,k)+GenFib(a,b,k+2)*GenFib(a,b,k+1)+ -
2*GenFib(a,b,k+1)*GenFib(a,b,k+2) by A11
.=GenFib(a,b,(k+1)+2)*GenFib(a,b,k)-GenFib(a,b,k+2)*GenFib(a,b,k+1)
.=(GenFib(a,b,k+1)+GenFib(a,b,(k+1)+1))*GenFib(a,b,k) -GenFib(a,b,k+2)
*GenFib(a,b,k+1) by Th34
.=GenFib(a,b,k+1)*GenFib(a,b,k)+d -(GenFib(a,b,k)+GenFib(a,b,k+1))*
GenFib(a,b,k+1) by Th34
.=d-(GenFib(a,b,k+1)*GenFib(a,b,k+1))
.=((-1)to_power k)*1*(GenFib(a,b,2)|^2-GenFib(a,b,1)*GenFib(a,b,3)) by A5
,WSIERP_1:1
.=((-1)to_power (k)*(1)to_power (2))*(GenFib(a,b,2)|^2 -GenFib(a,b,1)*
GenFib(a,b,3)) by POWER:26
.=((-1)to_power (k)*(-1)to_power (2))*(GenFib(a,b,2)|^2 -GenFib(a,b,1)
*GenFib(a,b,3)) by Th3
.=((-1)to_power (k+2))*(GenFib(a,b,2)|^2- GenFib(a,b,1)*GenFib(a,b,3))
by FIB_NUM2:5;
hence thesis;
end;
GenFib(a,b,0+2)* GenFib(a,b,0)-GenFib(a,b,0+1)|^2= GenFib(a,b,2)*a-
GenFib(a,b,1)|^2 by Th32
.=(a+b)*a-b|^2 by A1,Th32
.=a*a+b*a-b*b by WSIERP_1:1
.=(a+b)*(a+b)-b*(2*b+a)
.=1*(GenFib(a,b,2)|^2-b*GenFib(a,b,3)) by A1,A2,WSIERP_1:1
.=((-1)to_power 0)*(GenFib(a,b,2)|^2-b*GenFib(a,b,3)) by POWER:24
.=((-1)to_power 0)*(GenFib(a,b,2)|^2-GenFib(a,b,1)*GenFib(a,b,3)) by Th32;
then
A12: P[0];
for k being Nat holds P[k] from FIB_NUM:sch 1 (A12, A3, A4);
hence thesis;
end;
theorem
for a,b,k,n being Element of NAT holds GenFib(GenFib(a,b,k),GenFib(a,b
,k+1),n) = GenFib(a,b,n+k)
proof
let a,b,k,n be Element of NAT;
defpred P[Nat] means GenFib(GenFib(a,b,k),GenFib(a,b,k+1),$1)=GenFib(a,b,$1+
k);
A1: P[1] by Th32;
A2: for i being Nat st P[i] & P[i+1] holds P[i+2]
proof
let i be Nat;
assume ( P[i])& P[i+1];
then
GenFib(GenFib(a,b,k),GenFib(a,b,k+1),i+2) =GenFib(a,b,i+k)+GenFib(a,b,
(i+k)+1) by Th34
.=GenFib(a,b,(i+k)+2) by Th34
.=GenFib(a,b,(i+2)+k);
hence thesis;
end;
A3: P[0] by Th32;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A3, A1, A2);
hence thesis;
end;
theorem Th49:
for a,b,n being Element of NAT holds GenFib(a,b,n+1) = a*Fib(n) + b*Fib(n+1)
proof
let a,b,n be Element of NAT;
defpred P[Nat] means GenFib(a,b,$1+1)=a*Fib($1)+b*Fib($1+1);
A1: Fib(2)=Fib(0+2) .=0+1 by FIB_NUM2:24,PRE_FF:1;
GenFib(a,b,2)=GenFib(a,b,0+2) .=GenFib(a,b,0)+GenFib(a,b,0+1) by Th34
.=a+GenFib(a,b,1) by Th32
.=a+b by Th32;
then
A2: P[1] by A1,PRE_FF:1;
A3: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A4: P[k] and
A5: P[k+1];
GenFib(a,b,(k+2)+1)=GenFib(a,b,(k+1)+2)
.=a*Fib(k)+b*Fib(k+1)+GenFib(a,b,(k+1)+1) by A4,Th34
.=a*(Fib(k)+Fib(k+1))+b*(Fib(k+1)+Fib((k+1)+1)) by A5
.=a*Fib(k+2)+b*(Fib(k+1)+Fib((k+1)+1)) by FIB_NUM2:24
.=a*Fib(k+2)+b*Fib((k+1)+2) by FIB_NUM2:24
.=a*Fib(k+2)+b*Fib((k+2)+1);
hence thesis;
end;
A6: P[0] by Th32,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A6, A2, A3);
hence thesis;
end;
theorem
for b,n being Element of NAT holds GenFib(0,b,n) = b * Fib(n)
proof
let b,n be Element of NAT;
defpred P[Nat] means GenFib(0,b,$1)=b*Fib($1);
A1: P[1] by Th32,PRE_FF:1;
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A3: P[k] and
A4: P[k+1];
GenFib(0,b,k+2)=b*Fib(k)+GenFib(0,b,k+1) by A3,Th34
.=b*(Fib(k)+Fib(k+1)) by A4
.=b*Fib(k+2) by FIB_NUM2:24;
hence thesis;
end;
A5: P[0] by Th32,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A1, A2);
hence thesis;
end;
theorem
for a,n being Element of NAT holds GenFib(a,0,n+1) = a * Fib(n)
proof
let a,n be Element of NAT;
defpred P[Nat] means GenFib(a,0,$1+1)=a*Fib($1);
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A2: P[k] and
A3: P[k+1];
GenFib(a,0,(k+2)+1)=GenFib(a,0,(k+1)+2)
.=a*Fib(k)+GenFib(a,0,(k+1)+1) by A2,Th34
.=a*(Fib(k)+Fib(k+1)) by A3
.=a*Fib(k+2) by FIB_NUM2:24;
hence thesis;
end;
GenFib(a,0,2)=GenFib(a,0,0+2) .=GenFib(a,0,0)+GenFib(a,0,0+1) by Th34
.=a+GenFib(a,0,1) by Th32
.=a+0 by Th32;
then
A4: P[1] by PRE_FF:1;
A5: P[0] by Th32,PRE_FF:1;
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A4, A1);
hence thesis;
end;
theorem
for a,b,c,d,n being Element of NAT holds GenFib(a,b,n) + GenFib(c,d,n)
= GenFib(a+c,b+d,n)
proof
let a,b,c,d,n be Element of NAT;
defpred P[Nat] means GenFib(a,b,$1)+GenFib(c,d,$1)=GenFib(a+c,b+d,$1);
A1: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
assume that
A2: P[k] and
A3: P[k+1];
GenFib(a,b,k+2)+GenFib(c,d,k+2) =GenFib(a,b,k)+GenFib(a,b,k+1)+GenFib(
c,d,k+2) by Th34
.=GenFib(a,b,k)+GenFib(a,b,k+1)+(GenFib(c,d,k)+GenFib(c,d,k+1)) by Th34
.=GenFib(a+c,b+d,k)+(GenFib(a,b,k+1)+GenFib(c,d,k+1)) by A2
.=GenFib(a+c,b+d,k+2) by A3,Th34;
hence thesis;
end;
GenFib(a,b,1)+GenFib(c,d,1)=b+GenFib(c,d,1) by Th32
.=b+d by Th32
.=GenFib(a+c,b+d,1) by Th32;
then
A4: P[1];
GenFib(a,b,0)+GenFib(c,d,0)=a+GenFib(c,d,0) by Th32
.=a+c by Th32
.=GenFib(a+c,b+d,0) by Th32;
then
A5: P[0];
for k being Nat holds P[k] from FIB_NUM:sch 1 (A5, A4, A1);
hence thesis;
end;
theorem
for a,b,k,n being Element of NAT holds GenFib(k*a,k*b,n) = k * GenFib(
a,b,n )
proof
let a,b,k,n be Element of NAT;
defpred P[Nat] means GenFib(k*a,k*b,$1)=k*GenFib(a,b,$1);
A1: for i being Nat st P[i] & P[i+1] holds P[i+2]
proof
let i be Nat;
assume that
A2: P[i] and
A3: P[i+1];
GenFib(k*a,k*b,i+2)=k*GenFib(a,b,i)+GenFib(k*a,k*b,i+1) by A2,Th34
.=k*(GenFib(a,b,i)+GenFib(a,b,i+1)) by A3
.=k*GenFib(a,b,i+2) by Th34;
hence thesis;
end;
GenFib(k*a,k*b,1)=k*b by Th32
.=k*GenFib(a,b,1) by Th32;
then
A4: P[1];
GenFib(k*a,k*b,0)=k*a by Th32
.=k*GenFib(a,b,0) by Th32;
then
A5: P[0];
for i being Nat holds P[i] from FIB_NUM:sch 1 (A5, A4, A1);
hence thesis;
end;
theorem :: Binet Formula for Generalized Fibonacci Numbers
for a,b,n being Element of NAT holds GenFib(a,b,n) = ((a*(-tau_bar)+b)
* tau to_power n + (a*tau-b) * tau_bar to_power n) / sqrt(5)
proof
let a,b,n be Element of NAT;
defpred P[Nat] means GenFib(a,b,$1)=((a*(-tau_bar)+b)*(tau)to_power($1)+ (a*
tau-b)*(tau_bar)to_power($1)) / sqrt(5);
((a*(-tau_bar)+b)*(tau)to_power(1)+(a*tau-b)*(tau_bar)to_power(1)) /
sqrt(5) =((a*(-tau_bar)+b)*(tau)+(a*tau-b)*(tau_bar)to_power(1)) / sqrt(5)
by POWER:25
.=((a*(-tau_bar)+b)*(tau)+(a*tau-b)*(tau_bar)) / sqrt(5) by POWER:25
.=(b*(tau-tau_bar)) / sqrt (5)
.=b by FIB_NUM:def 1,def 2,XCMPLX_1:89
.=GenFib(a,b,1) by Th32;
then
A1: P[1];
A2: for k being Nat st P[k] & P[k+1] holds P[k+2]
proof
let k be Nat;
set c = tau to_power k;
set d = tau_bar to_power k;
A3: (tau)to_power(k+1)=(tau)to_power(k)*(tau)to_power(1) by POWER:27
.=c*tau by POWER:25;
set g = ((a*(-tau_bar)+b)*c+(a*tau-b)*d);
A4: (tau_bar)to_power(k+1)=(tau_bar)to_power(k)*(tau_bar)to_power(1) by
FIB_NUM2:5
.=d*tau_bar by POWER:25;
(sqrt 5)*(sqrt 5) = 5 by Th2;
then
A5: 1+tau=((1+sqrt 5)*(1+sqrt 5))/(2*2) by FIB_NUM:def 1
.=tau*tau by FIB_NUM:def 1
.=(tau to_power 1)*tau by POWER:25
.=(tau to_power 1)*(tau to_power 1) by POWER:25
.=(tau)to_power(1+1) by POWER:27;
A6: 1+tau_bar=(1-sqrt 5- sqrt 5 + 5)/4 by FIB_NUM:def 2
.=(1-1*sqrt 5-(sqrt 5)*1+((sqrt 5)*(sqrt 5)))/4 by Th2
.=tau_bar*tau_bar by FIB_NUM:def 2
.=(tau_bar to_power 1)*tau_bar by POWER:25
.=(tau_bar to_power 1)*(tau_bar to_power 1) by POWER:25
.=(tau_bar)to_power(1+1) by FIB_NUM2:5
.=(tau_bar)to_power(2);
set h = ((a*(-tau_bar)+b)*c*(tau)+(a*tau-b)*d*(tau_bar));
A7: (tau)to_power(k+2)=c*(tau)to_power(2) & (tau_bar)to_power(k+2)=d*(
tau_bar) to_power(2) by FIB_NUM2:5;
assume ( P[k])& P[k+1];
then GenFib(a,b,k+2)=g/(sqrt 5)+h/(sqrt 5) by A3,A4,Th34
.=(g+h)/(sqrt 5) by XCMPLX_1:62
.=((a*(-tau_bar)+b)*(tau)to_power(k+2)+(a*tau-b)* (tau_bar)to_power(k+
2)) / sqrt(5) by A7,A5,A6;
hence thesis;
end;
((a*(-tau_bar)+b)*(tau) to_power(0)+(a*tau-b)* (tau_bar)to_power(0)) /
sqrt 5 =((a*(-tau_bar)+b)*1+(a*tau-b)*(tau_bar)to_power(0)) / sqrt 5 by
POWER:24
.=((a*(-tau_bar)+b)+(a*tau-b)*1) / sqrt 5 by POWER:24
.=(a*(tau-tau_bar)) / sqrt 5
.=a by FIB_NUM:def 1,def 2,XCMPLX_1:89
.=GenFib(a,b,0) by Th32;
then
A8: P[0];
for k being Nat holds P[k] from FIB_NUM:sch 1 (A8, A1, A2);
hence thesis;
end;
theorem
for a,n being Element of NAT holds GenFib(2*a+1,2*a+1,n+1) = (2*a+1) *
Fib(n+2)
proof
let a,n be Element of NAT;
GenFib(2*a+1,2*a+1,n+1)=(2*a+1)*Fib(n)+(2*a+1)*Fib(n+1) by Th49
.= (2*a+1)*(Fib(n)+Fib(n+1))
.= (2*a+1)*Fib(n+2) by FIB_NUM2:24;
hence thesis;
end;