definition
let n be
Nat;
existence
ex b1 being Element of NAT ex L being sequence of [: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 sequence of [: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 sequence of [: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;
definition
let a,
b,
n be
Nat;
existence
ex b1 being Element of NAT ex L being sequence of [: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 sequence of [: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 sequence of [: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;
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
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
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)