let g, r be real number ; :: thesis: ( g <> 0 & r <> 0 implies abs ((g ") - (r ")) = (abs (g - r)) / ((abs g) * (abs r)) )
assume that
A1: g <> 0 and
A2: r <> 0 ; :: thesis: abs ((g ") - (r ")) = (abs (g - r)) / ((abs g) * (abs r))
thus abs ((g ") - (r ")) = abs ((1 / g) - (r ")) by XCMPLX_1:215
.= abs ((1 / g) - (1 / r)) by XCMPLX_1:215
.= abs (((1 * r) - (1 * g)) / (g * r)) by A1, A2, XCMPLX_1:130
.= (abs (r - g)) / (abs (g * r)) by COMPLEX1:67
.= (abs (- (g - r))) / ((abs g) * (abs r)) by COMPLEX1:65
.= (abs (g - r)) / ((abs g) * (abs r)) by COMPLEX1:52 ; :: thesis: verum