let g, r be Element of 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 7, XCMPLX_1:217
.= |.((1r / g) - (1r / r)).| by COMPLEX1:def 7, XCMPLX_1:217
.= |.((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:117
.= |.(r - g).| / |.(g * r).| by COMPLEX1:153, COMPLEX1:def 7
.= |.(- (g - r)).| / (|.g.| * |.r.|) by COMPLEX1:151
.= |.(g - r).| / (|.g.| * |.r.|) by COMPLEX1:138 ; :: thesis: verum