let z be Complex; :: thesis: ( z <> 0c implies ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = 0 ) )
set r = |.z.|;
set a = ((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>);
assume z <> 0c ; :: thesis: ( |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)).| = 1 & Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = 0 )
then A1: 0 < |.z.| by COMPLEX1:47;
|.(z * z).| = ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:68;
then 0 <= ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:46;
then A2: |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2) by SQUARE_1:def 2;
A3: ( Re (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) = (Re z) / |.z.| & Im (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) = (- (Im z)) / |.z.| ) by COMPLEX1:12;
then ((Re (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>))) ^2) + ((Im (((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>))) ^2) = (((Re z) ^2) / (|.z.| ^2)) + (((- (Im z)) / |.z.|) ^2) by XCMPLX_1:76
.= (((Re z) ^2) / (|.z.| ^2)) + (((- (Im z)) ^2) / (|.z.| ^2)) by XCMPLX_1:76
.= (((Re z) ^2) + ((Im z) ^2)) / (|.z.| ^2) by XCMPLX_1:62
.= 1 ^2 by A1, A2, XCMPLX_1:60 ;
hence |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)).| = 1 by SQUARE_1:18; :: thesis: ( Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = |.z.| & Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = 0 )
thus Re ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = (((Re z) / |.z.|) * (Re z)) - (((- (Im z)) / |.z.|) * (Im z)) by A3, COMPLEX1:9
.= (((Re z) * (Re z)) / |.z.|) - (((- (Im z)) / |.z.|) * (Im z)) by XCMPLX_1:74
.= (((Re z) ^2) / |.z.|) - (((- (Im z)) * (Im z)) / |.z.|) by XCMPLX_1:74
.= (((Re z) ^2) - (- ((Im z) * (Im z)))) / |.z.| by XCMPLX_1:120
.= |.z.| by A1, A2, XCMPLX_1:89 ; :: thesis: Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = 0
thus Im ((((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)) * z) = (((Re z) / |.z.|) * (Im z)) + ((Re z) * ((- (Im z)) / |.z.|)) by A3, COMPLEX1:9
.= (((Re z) * (Im z)) / |.z.|) + ((Re z) * ((- (Im z)) / |.z.|)) by XCMPLX_1:74
.= (((Re z) * (Im z)) / |.z.|) + (((- (Im z)) * (Re z)) / |.z.|) by XCMPLX_1:74
.= (((Re z) * (Im z)) + (- ((Im z) * (Re z)))) / |.z.| by XCMPLX_1:62
.= 0 ; :: thesis: verum