let n be Nat; :: thesis: for r being Real holds (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n
let r be Real; :: thesis: (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n
set s = scf r;
set s1 = c_n r;
set s2 = c_d r;
defpred S2[ Nat] means (((c_n r) . ($1 + 1)) * ((c_d r) . $1)) - (((c_n r) . $1) * ((c_d r) . ($1 + 1))) = (- 1) |^ $1;
A1: ( (c_d r) . 0 = 1 & (c_d r) . 1 = (scf r) . 1 ) by Def6;
A2: for n being Nat st S2[n] holds
S2[n + 1]
proof
let l be Nat; :: thesis: ( S2[l] implies S2[l + 1] )
assume A3: (((c_n r) . (l + 1)) * ((c_d r) . l)) - (((c_n r) . l) * ((c_d r) . (l + 1))) = (- 1) |^ l ; :: thesis: S2[l + 1]
(((c_n r) . (l + 2)) * ((c_d r) . (l + 1))) - (((c_n r) . (l + 1)) * ((c_d r) . (l + 2))) = (((((scf r) . (l + 2)) * ((c_n r) . (l + 1))) + ((c_n r) . l)) * ((c_d r) . (l + 1))) - (((c_n r) . (l + 1)) * ((c_d r) . (l + 2))) by Def5
.= (((((scf r) . (l + 2)) * ((c_n r) . (l + 1))) * ((c_d r) . (l + 1))) + (((c_n r) . l) * ((c_d r) . (l + 1)))) - (((c_n r) . (l + 1)) * ((((scf r) . (l + 2)) * ((c_d r) . (l + 1))) + ((c_d r) . l))) by Def6
.= (- 1) * ((((c_n r) . (l + 1)) * ((c_d r) . l)) - (((c_n r) . l) * ((c_d r) . (l + 1))))
.= (- 1) |^ (l + 1) by A3, NEWTON:6 ;
hence S2[l + 1] ; :: thesis: verum
end;
( (c_n r) . 0 = (scf r) . 0 & (c_n r) . 1 = (((scf r) . 1) * ((scf r) . 0)) + 1 ) by Def5;
then A4: S2[ 0 ] by A1, NEWTON:4;
for n being Nat holds S2[n] from NAT_1:sch 2(A4, A2);
 hence (((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1))) = (- 1) |^ n ; :: thesis: verum