let z1, z2 be Complex; z1 / z2 = ((((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>)
reconsider z1 = z1, z2 = z2 as Element of COMPLEX by XCMPLX_0:def 2;
reconsider k = ((Re z2) ^2) + ((Im z2) ^2) as Element of REAL by XREAL_0:def 1;
reconsider r = (Re z2) / k, i = (- (Im z2)) / k as Element of REAL ;
A1: Re [*r,i*] =
Re (((Re z2) / k) + (((- (Im z2)) / k) * <i>))
by Lm21
.=
(Re z2) / k
by Th12
;
A2: Im [*r,i*] =
Im (((Re z2) / k) + (((- (Im z2)) / k) * <i>))
by Lm21
.=
(- (Im z2)) / k
by Th12
;
reconsider r1 = (((Re z1) / 1) * ((Re z2) / k)) - ((Im z1) * ((- (Im z2)) / k)), i1 = ((Re z1) * ((- (Im z2)) / k)) + (((Re z2) / k) * (Im z1)) as Element of REAL by XREAL_0:def 1;
z1 / z2 =
z1 * (z2 ")
by XCMPLX_0:def 9
.=
z1 * (r + (i * <i>))
by Lm24
.=
z1 * [*r,i*]
by Lm21
.=
[*r1,i1*]
by A1, A2, Lm16
.=
((((Re z1) / 1) * ((Re z2) / k)) - ((Im z1) * ((- (Im z2)) / k))) + ((((Re z1) * ((- (Im z2)) / k)) + (((Re z2) / k) * (Im z1))) * <i>)
by Lm21
.=
((((Re z1) * (Re z2)) / (1 * k)) - (((Im z1) / 1) * ((- (Im z2)) / k))) + ((((Re z1) * ((- (Im z2)) / k)) + (((Re z2) / k) * (Im z1))) * <i>)
by XCMPLX_1:76
.=
((((Re z1) * (Re z2)) / k) - (((Im z1) * (- (Im z2))) / (1 * k))) + (((((Re z1) / 1) * ((- (Im z2)) / k)) + (((Re z2) / k) * (Im z1))) * <i>)
by XCMPLX_1:76
.=
((((Re z1) * (Re z2)) / k) - (((Im z1) * (- (Im z2))) / k)) + (((((Re z1) * (- (Im z2))) / (1 * k)) + (((Re z2) / k) * ((Im z1) / 1))) * <i>)
by XCMPLX_1:76
.=
((((Re z1) * (Re z2)) / k) - (((Im z1) * (- (Im z2))) / k)) + (((((Re z1) * (- (Im z2))) / k) + (((Im z1) * (Re z2)) / (1 * k))) * <i>)
by XCMPLX_1:76
.=
((((Re z1) * (Re z2)) - ((Im z1) * (- (Im z2)))) / k) + (((((Re z1) * (- (Im z2))) / k) + (((Im z1) * (Re z2)) / (1 * k))) * <i>)
by XCMPLX_1:120
.=
((((Re z1) * (Re z2)) + ((Im z1) * (Im z2))) / k) + ((((- ((Re z1) * (Im z2))) + ((Im z1) * (Re z2))) / k) * <i>)
by XCMPLX_1:62
.=
((((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
z1 / z2 = ((((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