defpred S1[ Nat] means for n being Element of NAT holds 2 * (Lucas (n + \$1)) = (() * (Lucas \$1)) + ((5 * (Fib n)) * (Fib \$1));
A1: now :: thesis: for k being Nat st S1[k] & S1[k + 1] holds
S1[k + 2]
let k be Nat; :: thesis: ( S1[k] & S1[k + 1] implies S1[k + 2] )
assume that
A2: S1[k] and
A3: S1[k + 1] ; :: thesis: S1[k + 2]
thus S1[k + 2] :: thesis: verum
proof
let n be Element of NAT ; :: thesis: 2 * (Lucas (n + (k + 2))) = (() * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2)))
A4: 2 * (Lucas (n + (k + 1))) = (() * (Lucas (k + 1))) + ((5 * (Fib n)) * (Fib (k + 1))) by A3;
2 * (Lucas (n + (k + 2))) = 2 * (Lucas ((n + k) + 2))
.= 2 * ((Lucas (n + k)) + (Lucas ((n + k) + 1))) by Th12
.= (2 * (Lucas (n + k))) + (2 * (Lucas ((n + k) + 1)))
.= ((() * ()) + ((5 * (Fib n)) * (Fib k))) + (2 * (Lucas (n + (k + 1)))) by A2
.= (() * (() + (Lucas (k + 1)))) + ((5 * (Fib n)) * ((Fib k) + (Fib (k + 1)))) by A4
.= (() * (Lucas (k + 2))) + ((5 * (Fib n)) * ((Fib k) + (Fib (k + 1)))) by Th12
.= (() * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2))) by FIB_NUM2:24 ;
hence 2 * (Lucas (n + (k + 2))) = (() * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2))) ; :: thesis: verum
end;
end;
A5: S1
proof
let n be Element of NAT ; :: thesis: 2 * (Lucas (n + 1)) = (() * ()) + ((5 * (Fib n)) * (Fib 1))
2 * (Lucas (n + 1)) = (((Lucas (n + 1)) + ()) + (Lucas (n + 1))) - ()
.= ((Lucas (n + 1)) + (Lucas (n + 2))) - () by Th12
.= (Lucas (n + 3)) - () by Th13
.= () + ((Lucas (n + 3)) - (2 * ()))
.= (() * ()) + ((5 * (Fib n)) * (Fib 1)) by ;
hence 2 * (Lucas (n + 1)) = (() * ()) + ((5 * (Fib n)) * (Fib 1)) ; :: thesis: verum
end;
A6: S1[ 0 ] by ;
for k being Nat holds S1[k] from FIB_NUM:sch 1(A6, A5, A1);
hence for n, m being Element of NAT holds 2 * (Lucas (n + m)) = (() * ()) + ((5 * (Fib n)) * (Fib m)) ; :: thesis: verum