let z be Element of 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:133;
|.(z * z).| = ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:154;
then 0 <= ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:132;
then A2: |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2) by SQUARE_1:def 4;
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:28;
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:77
.= (((Re z) ^2) / (|.z.| ^2)) + (((- (Im z)) ^2) / (|.z.| ^2)) by XCMPLX_1:77
.= (((Re z) ^2) + ((Im z) ^2)) / (|.z.| ^2) by XCMPLX_1:63
.= (|.z.| / |.z.|) ^2 by A2, XCMPLX_1:77
.= 1 ^2 by A1, XCMPLX_1:60 ;
hence |.(((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>)).| = 1 by SQUARE_1:83; :: 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:24
.= (((Re z) * (Re z)) / |.z.|) - (((- (Im z)) / |.z.|) * (Im z)) by XCMPLX_1:75
.= (((Re z) ^2) / |.z.|) - (((- (Im z)) * (Im z)) / |.z.|) by XCMPLX_1:75
.= (((Re z) ^2) - (- ((Im z) * (Im z)))) / |.z.| by XCMPLX_1:121
.= |.z.| by A1, A2, XCMPLX_1:90 ; :: 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:24
.= (((Re z) * (Im z)) / |.z.|) + ((Re z) * ((- (Im z)) / |.z.|)) by XCMPLX_1:75
.= (((Re z) * (Im z)) / |.z.|) + (((- (Im z)) * (Re z)) / |.z.|) by XCMPLX_1:75
.= (((Re z) * (Im z)) + (- ((Im z) * (Re z)))) / |.z.| by XCMPLX_1:63
.= 0 ; :: thesis: verum