let a, b, n be Element of NAT ; GenFib (a,b,n) = ((((a * (- tau_bar)) + b) * (tau to_power n)) + (((a * tau) - b) * (tau_bar to_power n))) / (sqrt 5)
defpred S1[ Nat] means GenFib (a,b,$1) = ((((a * (- tau_bar)) + b) * (tau to_power $1)) + (((a * tau) - b) * (tau_bar to_power $1))) / (sqrt 5);
((((a * (- tau_bar)) + b) * (tau to_power 1)) + (((a * tau) - b) * (tau_bar to_power 1))) / (sqrt 5) =
((((a * (- tau_bar)) + b) * tau) + (((a * tau) - b) * (tau_bar to_power 1))) / (sqrt 5)
by POWER:25
.=
((((a * (- tau_bar)) + b) * tau) + (((a * tau) - b) * tau_bar)) / (sqrt 5)
by POWER:25
.=
(b * (tau - tau_bar)) / (sqrt 5)
.=
b
by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:89
.=
GenFib (a,b,1)
by Th32
;
then A1:
S1[1]
;
A2:
for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
((((a * (- tau_bar)) + b) * (tau to_power 0)) + (((a * tau) - b) * (tau_bar to_power 0))) / (sqrt 5) =
((((a * (- tau_bar)) + b) * 1) + (((a * tau) - b) * (tau_bar to_power 0))) / (sqrt 5)
by POWER:24
.=
(((a * (- tau_bar)) + b) + (((a * tau) - b) * 1)) / (sqrt 5)
by POWER:24
.=
(a * (tau - tau_bar)) / (sqrt 5)
.=
a
by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:89
.=
GenFib (a,b,0)
by Th32
;
then A8:
S1[ 0 ]
;
for k being Nat holds S1[k]
from FIB_NUM:sch 1(A8, A1, A2);
hence
GenFib (a,b,n) = ((((a * (- tau_bar)) + b) * (tau to_power n)) + (((a * tau) - b) * (tau_bar to_power n))) / (sqrt 5)
; verum