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