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 :
for n being Nat
for b2 being Element of NAT holds
( b2 = Lucas n iff 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))] ) ) );
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 :
for a, b, n being Nat
for b4 being Element of NAT holds
( b4 = GenFib (a,b,n) iff ex L being Function of NAT,[:NAT,NAT:] st
( b4 = (L . n) `1 & L . 0 = [a,b] & ( for n being Nat holds L . (n + 1) = [((L . n) `2),(((L . n) `1) + ((L . n) `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