let n be Nat; :: thesis: for r being Real st ( for n being Nat holds (c_d r) . n <> 0 ) holds
(((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n))
let r be Real; :: thesis: ( ( for n being Nat holds (c_d r) . n <> 0 ) implies (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) )
set s1 = c_n r;
set s2 = c_d r;
assume for n being Nat holds (c_d r) . n <> 0 ; :: thesis: (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n))
then ( (c_d r) . n <> 0 & (c_d r) . (n + 1) <> 0 ) ;
then (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((((c_n r) . (n + 1)) * ((c_d r) . n)) - (((c_n r) . n) * ((c_d r) . (n + 1)))) / (((c_d r) . (n + 1)) * ((c_d r) . n)) by XCMPLX_1:130
.= ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) by Th64 ;
hence (((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n)) = ((- 1) |^ n) / (((c_d r) . (n + 1)) * ((c_d r) . n)) ; :: thesis: verum