let r be Real; :: thesis: ( ( for n being Nat holds (c_d r) . n <> 0 ) implies for n being Nat holds |.((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))).| = 1 / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).| )
set s1 = c_n r;
set s2 = c_d r;
assume A1: for n being Nat holds (c_d r) . n <> 0 ; :: thesis: for n being Nat holds |.((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))).| = 1 / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).|
let n be Nat; :: thesis: |.((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))).| = 1 / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).|
reconsider n = n as Element of NAT by ORDINAL1:def 12;
|.((((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))).| by A1, Th65
.= |.((- 1) |^ n).| / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).| by COMPLEX1:67
.= |.((- 1) to_power n).| / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).| by POWER:41
.= (|.(- 1).| to_power n) / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).| by SERIES_1:2
.= ((- (- 1)) to_power n) / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).| by ABSVALUE:def 1
.= 1 / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).| by POWER:26 ;
hence |.((((c_n r) . (n + 1)) / ((c_d r) . (n + 1))) - (((c_n r) . n) / ((c_d r) . n))).| = 1 / |.(((c_d r) . (n + 1)) * ((c_d r) . n)).| ; :: thesis: verum