defpred S1[ Nat] means for n being Element of NAT holds 2 * (Lucas (n + $1)) = ((Lucas n) * (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 n) * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2)))
A4: 2 * (Lucas (n + (k + 1))) = ((Lucas n) * (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)))
.= (((Lucas n) * (Lucas k)) + ((5 * (Fib n)) * (Fib k))) + (2 * (Lucas (n + (k + 1)))) by A2
.= ((Lucas n) * ((Lucas k) + (Lucas (k + 1)))) + ((5 * (Fib n)) * ((Fib k) + (Fib (k + 1)))) by A4
.= ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * ((Fib k) + (Fib (k + 1)))) by Th12
.= ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2))) by FIB_NUM2:24 ;
hence 2 * (Lucas (n + (k + 2))) = ((Lucas n) * (Lucas (k + 2))) + ((5 * (Fib n)) * (Fib (k + 2))) ; :: thesis: verum
end;
end;
A5: S1[1]
proof
let n be Element of NAT ; :: thesis: 2 * (Lucas (n + 1)) = ((Lucas n) * (Lucas 1)) + ((5 * (Fib n)) * (Fib 1))
2 * (Lucas (n + 1)) = (((Lucas (n + 1)) + (Lucas n)) + (Lucas (n + 1))) - (Lucas n)
.= ((Lucas (n + 1)) + (Lucas (n + 2))) - (Lucas n) by Th12
.= (Lucas (n + 3)) - (Lucas n) by Th13
.= (Lucas n) + ((Lucas (n + 3)) - (2 * (Lucas n)))
.= ((Lucas n) * (Lucas 1)) + ((5 * (Fib n)) * (Fib 1)) by Th11, Th23, PRE_FF:1 ;
hence 2 * (Lucas (n + 1)) = ((Lucas n) * (Lucas 1)) + ((5 * (Fib n)) * (Fib 1)) ; :: thesis: verum
end;
A6: S1[ 0 ] by Th11, PRE_FF:1;
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)) = ((Lucas n) * (Lucas m)) + ((5 * (Fib n)) * (Fib m)) ; :: thesis: verum