:: Lucas Numbers and Generalized {F}ibonacci Numbers
:: by Piotr Wojtecki and Adam Grabowski
::
:: Received May 24, 2004
:: Copyright (c) 2004 Association of Mizar Users
theorem :: FIB_NUM3:1
theorem Th2: :: FIB_NUM3:2
theorem Th3: :: FIB_NUM3:3
theorem Th4: :: FIB_NUM3:4
theorem Th5: :: FIB_NUM3:5
Lm2:
tau_bar < 0
by FIB_NUM2:35, FIB_NUM2:38;
theorem Th6: :: FIB_NUM3:6
theorem Th7: :: FIB_NUM3:7
theorem Th8: :: FIB_NUM3:8
theorem Th9: :: FIB_NUM3:9
theorem Th10: :: FIB_NUM3:10
definition
let n be
Nat;
func Lucas n -> Element of
NAT means :
Def1:
:: FIB_NUM3:def 1
ex
L being
Function of
NAT ,
[: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 ))] ) );
existence
ex b1 being Element of NAT ex L being Function of NAT ,[:NAT ,NAT :] st
( b1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2 ),(((L . n) `1 ) + ((L . n) `2 ))] ) )
uniqueness
for b1, b2 being Element of NAT st ex L being Function of NAT ,[:NAT ,NAT :] st
( b1 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2 ),(((L . n) `1 ) + ((L . n) `2 ))] ) ) & ex L being Function of NAT ,[:NAT ,NAT :] st
( b2 = (L . n) `1 & L . 0 = [2,1] & ( for n being Nat holds L . (n + 1) = [((L . n) `2 ),(((L . n) `1 ) + ((L . n) `2 ))] ) ) holds
b1 = b2
end;
:: deftheorem Def1 defines Lucas FIB_NUM3:def 1 :
theorem Th11: :: FIB_NUM3:11
theorem Th12: :: FIB_NUM3:12
theorem Th13: :: FIB_NUM3:13
theorem Th14: :: FIB_NUM3:14
theorem Th15: :: FIB_NUM3:15
theorem Th16: :: FIB_NUM3:16
theorem Th17: :: FIB_NUM3:17
theorem :: FIB_NUM3:18
theorem :: FIB_NUM3:19
theorem :: FIB_NUM3:20
theorem Th21: :: FIB_NUM3:21
theorem :: FIB_NUM3:22
theorem Th23: :: FIB_NUM3:23
theorem :: FIB_NUM3:24
theorem :: FIB_NUM3:25
theorem :: FIB_NUM3:26
theorem :: FIB_NUM3:27
theorem Th28: :: FIB_NUM3:28
theorem :: FIB_NUM3:29
theorem :: FIB_NUM3:30
theorem :: FIB_NUM3:31
definition
let a,
b,
n be
Nat;
func GenFib a,
b,
n -> Element of
NAT means :
Def2:
:: FIB_NUM3:def 2
ex
L being
Function of
NAT ,
[: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 ))] ) );
existence
ex b1 being Element of NAT ex L being Function of NAT ,[:NAT ,NAT :] st
( b1 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2 ),(((L . n) `1 ) + ((L . n) `2 ))] ) )
uniqueness
for b1, b2 being Element of NAT st ex L being Function of NAT ,[:NAT ,NAT :] st
( b1 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2 ),(((L . n) `1 ) + ((L . n) `2 ))] ) ) & ex L being Function of NAT ,[:NAT ,NAT :] st
( b2 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2 ),(((L . n) `1 ) + ((L . n) `2 ))] ) ) holds
b1 = b2
end;
:: deftheorem Def2 defines GenFib FIB_NUM3:def 2 :
theorem Th32: :: 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 Th33: :: FIB_NUM3:33
for
a,
b being
Element of
NAT 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 Th34: :: FIB_NUM3:34
theorem Th35: :: FIB_NUM3:35
theorem Th36: :: FIB_NUM3:36
theorem :: FIB_NUM3:37
theorem Th38: :: FIB_NUM3:38
theorem Th39: :: FIB_NUM3:39
theorem :: FIB_NUM3:40
theorem :: FIB_NUM3:41
theorem :: FIB_NUM3:42
theorem :: FIB_NUM3:43
theorem :: FIB_NUM3:44
theorem :: FIB_NUM3:45
theorem :: FIB_NUM3:46
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 Th49: :: FIB_NUM3:49
theorem :: FIB_NUM3:50
theorem :: FIB_NUM3:51
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
theorem :: FIB_NUM3:54
theorem :: FIB_NUM3:55