let a, b, n be Element of NAT ; :: thesis: GenFib a,b,n = ((((a * (- tau_bar )) + b) * (tau to_power n)) + (((a * tau ) - b) * (tau_bar to_power n))) / (sqrt 5)
defpred S₁[ Nat] means GenFib a,b,$1 = ((((a * (- tau_bar )) + b) * (tau to_power $1)) + (((a * tau ) - b) * (tau_bar to_power $1))) / (sqrt 5);
A1: S₁[ 0 ]

proof

((((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:29
.= (((a * (- tau_bar )) + b) + (((a * tau ) - b) * 1)) / (sqrt 5) by POWER:29
.= (a * (tau - tau_bar )) / (sqrt 5)
.= a by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:90
.= GenFib a,b,0 by Th32 ;
hence S₁[ 0 ] ; :: thesis: verum

end;

A2: S₁[1]

proof

((((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:30
.= ((((a * (- tau_bar )) + b) * tau ) + (((a * tau ) - b) * tau_bar )) / (sqrt 5) by POWER:30
.= (b * (tau - tau_bar )) / (sqrt 5)
.= b by FIB_NUM:def 1, FIB_NUM:def 2, XCMPLX_1:90
.= GenFib a,b,1 by Th32 ;
hence S₁[1] ; :: thesis: verum

end;

A3: for k being Nat st S₁[k] & S₁[k + 1] holds
S₁[k + 2]

proof

let k be Nat; :: thesis: ( S₁[k] & S₁[k + 1] implies S₁[k + 2] )
assume that
A4: S₁[k] and
A5: S₁[k + 1] ; :: thesis: S₁[k + 2]
set c = tau to_power k;
set d = tau_bar to_power k;
A6: tau to_power (k + 1) = (tau to_power k) * (tau to_power 1) by POWER:32
.= (tau to_power k) * tau by POWER:30 ;
A7: tau_bar to_power (k + 1) = (tau_bar to_power k) * (tau_bar to_power 1) by FIB_NUM2:7
.= (tau_bar to_power k) * tau_bar by POWER:30 ;
A8: tau to_power (k + 2) = (tau to_power k) * (tau to_power 2) by POWER:32;
A9: tau_bar to_power (k + 2) = (tau_bar to_power k) * (tau_bar to_power 2) by FIB_NUM2:7;
(sqrt 5) * (sqrt 5) = 5 by Th2;
then A10: 1 + tau = ((1 + (sqrt 5)) * (1 + (sqrt 5))) / (2 * 2) by FIB_NUM:def 1
.= tau * tau by FIB_NUM:def 1
.= (tau to_power 1) * tau by POWER:30
.= (tau to_power 1) * (tau to_power 1) by POWER:30
.= tau to_power (1 + 1) by POWER:32 ;
A11: 1 + tau_bar = (((1 - (sqrt 5)) - (sqrt 5)) + 5) / 4 by FIB_NUM:def 2
.= (((1 - (1 * (sqrt 5))) - ((sqrt 5) * 1)) + ((sqrt 5) * (sqrt 5))) / 4 by Th2
.= tau_bar * tau_bar by FIB_NUM:def 2
.= (tau_bar to_power 1) * tau_bar by POWER:30
.= (tau_bar to_power 1) * (tau_bar to_power 1) by POWER:30
.= tau_bar to_power (1 + 1) by FIB_NUM2:7
.= tau_bar to_power 2 ;
set g = (((a * (- tau_bar )) + b) * (tau to_power k)) + (((a * tau ) - b) * (tau_bar to_power k));
set h = ((((a * (- tau_bar )) + b) * (tau to_power k)) * tau ) + ((((a * tau ) - b) * (tau_bar to_power k)) * tau_bar );
GenFib a,b,(k + 2) = (((((a * (- tau_bar )) + b) * (tau to_power k)) + (((a * tau ) - b) * (tau_bar to_power k))) / (sqrt 5)) + ((((((a * (- tau_bar )) + b) * (tau to_power k)) * tau ) + ((((a * tau ) - b) * (tau_bar to_power k)) * tau_bar )) / (sqrt 5)) by A4, A5, A6, A7, Th34
.= (((((a * (- tau_bar )) + b) * (tau to_power k)) + (((a * tau ) - b) * (tau_bar to_power k))) + (((((a * (- tau_bar )) + b) * (tau to_power k)) * tau ) + ((((a * tau ) - b) * (tau_bar to_power k)) * tau_bar ))) / (sqrt 5) by XCMPLX_1:63
.= ((((a * (- tau_bar )) + b) * (tau to_power (k + 2))) + (((a * tau ) - b) * (tau_bar to_power (k + 2)))) / (sqrt 5) by A8, A9, A10, A11 ;
hence S₁[k + 2] ; :: thesis: verum

end;

for k being Nat holds S₁[k] from FIB_NUM:sch 1(A1, A2, A3);
hence GenFib a,b,n = ((((a * (- tau_bar )) + b) * (tau to_power n)) + (((a * tau ) - b) * (tau_bar to_power n))) / (sqrt 5) ; :: thesis: verum