begin
theorem
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
begin
definition
let n be
Nat;
func Lucas n -> Element of
NAT means :
Def1:
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:
theorem Th12:
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem
theorem
theorem
theorem Th21:
theorem
theorem Th23:
theorem
theorem
theorem
theorem
theorem Th28:
theorem
theorem
theorem
begin
definition
let a,
b,
n be
Nat;
func GenFib a,
b,
n -> Element of
NAT means :
Def2:
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:
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:
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:
theorem Th35:
theorem Th36:
theorem
theorem Th38:
theorem Th39:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
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)))
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)
theorem Th49:
theorem
theorem
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
theorem
theorem
theorem