reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def 2;
set k = ((Re z2) ^2 ) + ((Im z2) ^2 );
A1: Re [*((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))),((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 )))*] =
Re (((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * <i> ))
by Lm21
.=
(Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))
by Th28
;
A2: Im [*((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))),((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 )))*] =
Im (((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * <i> ))
by Lm21
.=
(- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))
by Th28
;
z1 / z2 =
z1 * (z2 " )
by XCMPLX_0:def 9
.=
z1 * [*((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))),((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 )))*]
by Lm21
.=
[*((((Re z1) / 1) * ((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 )))) - ((Im z1) * ((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))))),(((Re z1) * ((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 )))) + (((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * (Im z1)))*]
by A1, A2, Lm16
.=
((((Re z1) / 1) * ((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 )))) - ((Im z1) * ((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))))) + ((((Re z1) * ((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 )))) + (((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * (Im z1))) * <i> )
by Lm21
.=
((((Re z1) * (Re z2)) / (1 * (((Re z2) ^2 ) + ((Im z2) ^2 )))) - (((Im z1) / 1) * ((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))))) + ((((Re z1) * ((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 )))) + (((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * (Im z1))) * <i> )
by XCMPLX_1:77
.=
((((Re z1) * (Re z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) - (((Im z1) * (- (Im z2))) / (1 * (((Re z2) ^2 ) + ((Im z2) ^2 ))))) + (((((Re z1) / 1) * ((- (Im z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 )))) + (((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * (Im z1))) * <i> )
by XCMPLX_1:77
.=
((((Re z1) * (Re z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) - (((Im z1) * (- (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 )))) + (((((Re z1) * (- (Im z2))) / (1 * (((Re z2) ^2 ) + ((Im z2) ^2 )))) + (((Re z2) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * ((Im z1) / 1))) * <i> )
by XCMPLX_1:77
.=
((((Re z1) * (Re z2)) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) - (((Im z1) * (- (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 )))) + (((((Re z1) * (- (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((Im z1) * (Re z2)) / (1 * (((Re z2) ^2 ) + ((Im z2) ^2 ))))) * <i> )
by XCMPLX_1:77
.=
((((Re z1) * (Re z2)) - ((Im z1) * (- (Im z2)))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((((Re z1) * (- (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((Im z1) * (Re z2)) / (1 * (((Re z2) ^2 ) + ((Im z2) ^2 ))))) * <i> )
by XCMPLX_1:121
.=
((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + ((((- ((Re z1) * (Im z2))) + ((Im z1) * (Re z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * <i> )
by XCMPLX_1:63
.=
((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * <i> )
;
hence
for b1 being Element of COMPLEX holds
( b1 = z1 / z2 iff b1 = ((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) + (((((Re z2) * (Im z1)) - ((Re z1) * (Im z2))) / (((Re z2) ^2 ) + ((Im z2) ^2 ))) * <i> ) )
; verum