let r, g be Complex; :: thesis: ( g <> 0c & r <> 0c implies |.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|) )
assume A1: ( g <> 0c & r <> 0c ) ; :: thesis: |.((g ") - (r ")).| = |.(g - r).| / (|.g.| * |.r.|)
thus |.((g ") - (r ")).| = |.((1r / g) - (r ")).| by COMPLEX1:def 4, XCMPLX_1:215
.= |.((1r / g) - (1r / r)).| by COMPLEX1:def 4, XCMPLX_1:215
.= |.((1r / g) + (- (1r / r))).|
.= |.((1r / g) + (- (1r * (r ")))).| by XCMPLX_0:def 9
.= |.((1r / g) + ((- 1r) * (r "))).|
.= |.((1r / g) + ((- 1r) / r)).| by XCMPLX_0:def 9
.= |.(((1r * r) + ((- 1r) * g)) / (r * g)).| by A1, XCMPLX_1:116
.= |.(r - g).| / |.(g * r).| by COMPLEX1:67, COMPLEX1:def 4
.= |.(- (g - r)).| / (|.g.| * |.r.|) by COMPLEX1:65
.= |.(g - r).| / (|.g.| * |.r.|) by COMPLEX1:52 ; :: thesis: verum