let a, b, n be non zero Element of NAT ; GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n))
thus
GenFib (a,b,n) = ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n))
verumproof
defpred S1[
Nat]
means GenFib (
a,
b,$1)
= ((GenFib (a,b,0)) * (Fib ($1 -' 1))) + ((GenFib (a,b,1)) * (Fib $1));
GenFib (
a,
b,1) =
((GenFib (a,b,0)) * (Fib 0)) + ((GenFib (a,b,1)) * (Fib 1))
by PRE_FF:1
.=
((GenFib (a,b,0)) * (Fib (1 -' 1))) + ((GenFib (a,b,1)) * (Fib 1))
by XREAL_1:232
;
then A1:
S1[1]
;
A2:
for
k being non
zero Nat st
S1[
k] &
S1[
k + 1] holds
S1[
k + 2]
proof
let k be non
zero Nat;
( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that A3:
S1[
k]
and A4:
S1[
k + 1]
;
S1[k + 2]
1
<= k
by NAT_2:19;
then A5:
(Fib (k -' 1)) + (Fib ((k + 1) -' 1)) =
(Fib (k -' 1)) + (Fib ((k -' 1) + 1))
by NAT_D:38
.=
Fib (((k -' 1) + 1) + 1)
by PRE_FF:1
.=
Fib ((k -' 1) + 2)
.=
Fib ((k + 2) -' 1)
by Th4
;
GenFib (
a,
b,
(k + 2)) =
(((GenFib (a,b,0)) * (Fib (k -' 1))) + ((GenFib (a,b,1)) * (Fib k))) + (GenFib (a,b,(k + 1)))
by A3, Th34
.=
((a * (Fib (k -' 1))) + ((GenFib (a,b,1)) * (Fib k))) + (GenFib (a,b,(k + 1)))
by Th32
.=
((a * (Fib (k -' 1))) + (b * (Fib k))) + (GenFib (a,b,(k + 1)))
by Th32
.=
(((a * (Fib (k -' 1))) + (b * (Fib k))) + ((GenFib (a,b,0)) * (Fib ((k + 1) -' 1)))) + ((GenFib (a,b,1)) * (Fib (k + 1)))
by A4
.=
(((a * (Fib (k -' 1))) + (b * (Fib k))) + (a * (Fib ((k + 1) -' 1)))) + ((GenFib (a,b,1)) * (Fib (k + 1)))
by Th32
.=
(((a * (Fib (k -' 1))) + (b * (Fib k))) + (a * (Fib ((k + 1) -' 1)))) + (b * (Fib (k + 1)))
by Th32
.=
(a * ((Fib (k -' 1)) + (Fib ((k + 1) -' 1)))) + (b * ((Fib k) + (Fib (k + 1))))
.=
(a * (Fib ((k + 2) -' 1))) + (b * (Fib (k + 2)))
by A5, FIB_NUM2:24
.=
(a * (Fib ((k + 2) -' 1))) + ((GenFib (a,b,1)) * (Fib (k + 2)))
by Th32
.=
((GenFib (a,b,0)) * (Fib ((k + 2) -' 1))) + ((GenFib (a,b,1)) * (Fib (k + 2)))
by Th32
;
hence
S1[
k + 2]
;
verum
end;
(0 + 1) + 1
= 2
;
then A6:
Fib 2
= 1
by PRE_FF:1;
GenFib (
a,
b,2) =
GenFib (
a,
b,
(0 + 2))
.=
((GenFib (a,b,0)) * (Fib (1 + 0))) + ((GenFib (a,b,1)) * (Fib 2))
by A6, Th34, PRE_FF:1
.=
((GenFib (a,b,0)) * (Fib (1 + (1 -' 1)))) + ((GenFib (a,b,1)) * (Fib 2))
by XREAL_1:232
.=
((GenFib (a,b,0)) * (Fib ((1 + 1) -' 1))) + ((GenFib (a,b,1)) * (Fib 2))
by NAT_D:38
.=
((GenFib (a,b,0)) * (Fib (2 -' 1))) + ((GenFib (a,b,1)) * (Fib 2))
;
then A7:
S1[2]
;
for
k being non
zero Nat holds
S1[
k]
from FIB_NUM2:sch 1(A1, A7, A2);
hence
GenFib (
a,
b,
n)
= ((GenFib (a,b,0)) * (Fib (n -' 1))) + ((GenFib (a,b,1)) * (Fib n))
;
verum
end;