:: Lucas Numbers and Generalized {F}ibonacci Numbers
:: by Piotr Wojtecki and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004-2019 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, BOOLE, ARITHM;
begin :: Preliminaries
reserve a,b,n for Element of NAT;
theorem :: FIB_NUM3:1
for a being Real, n being Element of NAT st a to_power n = 0
holds a = 0;
theorem :: FIB_NUM3:2
for a being non negative Real holds (sqrt a) * (sqrt a) = a;
theorem :: FIB_NUM3:3
for a being Real holds a to_power 2 = (-a) to_power 2;
theorem :: FIB_NUM3:4
for k being non zero Nat holds k-'1+2 = k+2-'1;
theorem :: FIB_NUM3:5
(a+b) |^ 2 = a*a + a*b + a*b + b*b;
theorem :: FIB_NUM3:6
for a being non zero Real holds (a to_power n) to_power 2
= a to_power (2*n);
theorem :: FIB_NUM3:7
for a, b being Real holds
(a + b)*(a - b) = a to_power 2 - b to_power 2;
theorem :: FIB_NUM3:8
for a, b be non zero Real holds
(a*b) to_power n = a to_power n * b to_power n;
registration
cluster tau -> positive;
cluster tau_bar -> negative;
end;
theorem :: FIB_NUM3:9
for n being Nat holds tau to_power n + tau to_power(n+1) = tau to_power(n+2);
theorem :: FIB_NUM3:10
for n being Nat holds tau_bar to_power n + tau_bar to_power(n+1)
= tau_bar to_power(n+2);
begin :: Lucas Numbers
definition
let n be Nat;
::$N Lucas numbers
func Lucas (n) -> Element of NAT means
:: FIB_NUM3:def 1
ex L being sequence of [:NAT, NAT:]
st it = (L.n)`1 & L.0 = [2,1] & for n being Nat holds L.(n+1) = [ (L
.n)`2, (L.n)`1 + (L.n)`2 ];
end;
theorem :: FIB_NUM3:11
Lucas(0) = 2 & Lucas(1) = 1 & for n being Nat holds Lucas((n+1)+
1) = Lucas(n) + Lucas(n+1);
theorem :: FIB_NUM3:12
for n being Nat holds Lucas(n + 2) = Lucas (n) + Lucas (n+1);
theorem :: FIB_NUM3:13
for n being Nat holds Lucas(n+1) + Lucas(n+2) = Lucas(n+3);
theorem :: FIB_NUM3:14
Lucas(2) = 3;
theorem :: FIB_NUM3:15
Lucas(3) = 4;
theorem :: FIB_NUM3:16
Lucas(4) = 7;
theorem :: FIB_NUM3:17
for k being Nat holds Lucas(k) >= k;
theorem :: FIB_NUM3:18
for m being non zero Element of NAT holds Lucas(m+1) >= Lucas(m);
registration
let n be Element of NAT;
cluster Lucas n -> positive;
end;
theorem :: FIB_NUM3:19
for n being Element of NAT holds 2 * Lucas(n+2) = Lucas(n) + Lucas(n+3 );
theorem :: FIB_NUM3:20
for n being Nat holds Lucas(n+1) = Fib(n) + Fib(n+2);
theorem :: FIB_NUM3:21 :: Binet Formula for Lucas Numbers
for n being Nat holds Lucas(n) = tau to_power n + tau_bar to_power n;
theorem :: FIB_NUM3:22
for n being Nat holds 2 * Lucas(n) + Lucas(n + 1) = 5 * Fib(n + 1);
theorem :: FIB_NUM3:23
for n being Nat holds Lucas(n + 3) - 2 * Lucas(n) = 5 * Fib(n);
theorem :: FIB_NUM3:24
for n being Nat holds Lucas(n) + Fib(n) = 2 * Fib(n+1);
theorem :: FIB_NUM3:25
for n being Nat holds 3 * Fib(n) + Lucas(n) = 2 * Fib(n+2);
theorem :: FIB_NUM3:26
for n,m being Element of NAT holds 2 * Lucas(n + m) = Lucas(n) * Lucas
(m) + 5 * Fib(n) * Fib(m);
theorem :: FIB_NUM3:27
for n being Element of NAT holds Lucas(n + 3) * Lucas(n) = (Lucas(n +
2))|^2 - (Lucas(n+1))|^2;
theorem :: FIB_NUM3:28
for n being Nat holds Fib(2*n) = Fib(n) * Lucas(n);
theorem :: FIB_NUM3:29
for n being Element of NAT holds 2 * Fib(2*n+1) = Lucas(n+1) * Fib(n)
+ Lucas(n) * Fib(n+1);
theorem :: FIB_NUM3:30
for n being Element of NAT holds 5 * (Fib(n)) |^ 2 - (Lucas(n)) |^ 2 =
4 * (-1) to_power (n+1);
theorem :: FIB_NUM3:31
for n being Element of NAT holds Fib(2*n+1) = Fib(n+1) * Lucas(n+1) -
Fib(n) * Lucas(n);
begin :: Generalized Fibonacci Numbers
definition
let a,b be Nat;
redefine func [a,b] -> Element of [:NAT,NAT:];
end;
definition
let a,b,n be Nat;
func GenFib (a,b,n) -> Element of NAT means
:: FIB_NUM3:def 2
ex L being sequence of [:NAT, NAT:] st
it = (L.n)`1 & L.0 = [a,b] & for n being Nat holds L.(n+1)
= [ (L.n)`2, (L.n)`1 + (L.n)`2 ];
end;
theorem :: FIB_NUM3:32
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);
theorem :: FIB_NUM3:33
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);
theorem :: FIB_NUM3:34
for a,b,n being Nat holds GenFib(a,b,n) + GenFib(a,b,n+1) = GenFib(a,b,n+2);
theorem :: FIB_NUM3:35
for a,b,n being Nat holds GenFib(a,b,n+1) + GenFib(a,b,n+2) =
GenFib(a,b,n + 3);
theorem :: FIB_NUM3:36
for a,b,n being Element of NAT holds GenFib(a,b,n+2) + GenFib(a,
b,n+3) = GenFib(a,b,n + 4);
theorem :: FIB_NUM3:37
for n being Element of NAT holds GenFib(0,1,n) = Fib(n);
theorem :: FIB_NUM3:38
for n being Element of NAT holds GenFib(2,1,n) = Lucas(n);
theorem :: FIB_NUM3:39
for a,b,n being Element of NAT holds GenFib(a,b,n) + GenFib(a,b,
n + 3) = 2*GenFib(a,b,n + 2);
theorem :: FIB_NUM3:40
for a,b,n being Element of NAT holds GenFib(a,b,n) + GenFib(a,b,n + 4)
= 3*GenFib(a,b,n + 2);
theorem :: FIB_NUM3:41
for a,b,n being Element of NAT holds GenFib(a,b,n + 3) - GenFib(a,b,n)
= 2*GenFib(a,b,n +1);
theorem :: FIB_NUM3:42
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);
theorem :: FIB_NUM3:43
for n,m being Nat holds Fib(m) * Lucas(n) + Lucas(m) * Fib(n) = GenFib
(Fib(0),Lucas(0),n+m);
theorem :: FIB_NUM3:44
for n being Element of NAT holds Lucas(n) + Lucas(n + 3) = 2*Lucas(n + 2);
theorem :: FIB_NUM3:45
for a,n being Element of NAT holds GenFib(a,a,n) = ((GenFib(a,a,0)) /
2) * (Fib(n) + Lucas(n));
theorem :: FIB_NUM3:46
for a,b,n being Element of NAT holds GenFib(b,a+b,n) = GenFib(a,b,n+1);
theorem :: FIB_NUM3:47
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));
theorem :: FIB_NUM3:48
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);
theorem :: FIB_NUM3:49
for a,b,n being Element of NAT holds GenFib(a,b,n+1) = a*Fib(n) + b*Fib(n+1);
theorem :: FIB_NUM3:50
for b,n being Element of NAT holds GenFib(0,b,n) = b * Fib(n);
theorem :: FIB_NUM3:51
for a,n being Element of NAT holds GenFib(a,0,n+1) = a * Fib(n);
theorem :: FIB_NUM3:52
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);
theorem :: FIB_NUM3:53
for a,b,k,n being Element of NAT holds GenFib(k*a,k*b,n) = k * GenFib(
a,b,n );
theorem :: FIB_NUM3:54 :: 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);
theorem :: FIB_NUM3:55
for a,n being Element of NAT holds GenFib(2*a+1,2*a+1,n+1) = (2*a+1) *
Fib(n+2);