defpred S1[ Nat] means Fib $1 = ((tau to_power $1) - (tau_bar to_power $1)) / (sqrt 5);
A1: tau_bar to_power 1 = tau_bar by POWER:25;
tau_bar to_power 0 = 1 by POWER:24;
then ((tau to_power 0) - (tau_bar to_power 0)) / (sqrt 5) = (1 - 1) / (sqrt 5) by POWER:24
.= 0 ;
then A2: S1[ 0 ] by PRE_FF:1;
A3: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
proof
let k be Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A4: S1[k] and
A5: S1[k + 1] ; :: thesis: S1[k + 2]
set a = tau to_power k;
set a1 = tau_bar to_power k;
set b = tau to_power (k + 1);
set b1 = tau_bar to_power (k + 1);
set c = tau to_power (k + 2);
set c1 = tau_bar to_power (k + 2);
A6: tau_bar to_power (k + 2) = tau_bar |^ (k + 2) by POWER:41
.= (tau_bar |^ k) * (tau_bar |^ (1 + 1)) by NEWTON:8
.= (tau_bar |^ k) * (tau_bar * (tau_bar |^ 1)) by NEWTON:6
.= (tau_bar |^ k) * (tau_bar + 1) by Lm8
.= ((tau_bar |^ k) * tau_bar) + ((tau_bar |^ k) * 1)
.= (tau_bar |^ (k + 1)) + ((tau_bar |^ k) * 1) by NEWTON:6
.= (tau_bar to_power (k + 1)) + (tau_bar |^ k) by POWER:41
.= (tau_bar to_power k) + (tau_bar to_power (k + 1)) by POWER:41 ;
A7: tau to_power (k + 2) = (tau to_power 2) * (tau to_power k) by Lm12, POWER:27
.= (tau to_power k) * (tau + 1) by Lm8, POWER:46
.= ((tau to_power k) * tau) + ((tau to_power k) * 1)
.= ((tau to_power k) * (tau to_power 1)) + (tau to_power k) by POWER:25
.= (tau to_power k) + (tau to_power (k + 1)) by Lm12, POWER:27 ;
Fib (k + 2) = Fib ((k + 1) + 1)
.= (((tau to_power k) - (tau_bar to_power k)) / (sqrt 5)) + (((tau to_power (k + 1)) - (tau_bar to_power (k + 1))) / (sqrt 5)) by A4, A5, PRE_FF:1
.= ((tau to_power (k + 2)) - (tau_bar to_power (k + 2))) / (sqrt 5) by A7, A6 ;
hence S1[k + 2] ; :: thesis: verum
end;
tau - tau_bar = sqrt 5 ;
then ((tau to_power 1) - (tau_bar to_power 1)) / (sqrt 5) = (sqrt 5) / (sqrt 5) by A1, POWER:25
.= Fib 1 by Lm10, PRE_FF:1, XCMPLX_1:60 ;
then A8: S1[1] ;
thus for n being Nat holds S1[n] from FIB_NUM:sch 1(A2, A8, A3); :: thesis: verum