let z be Complex; :: thesis: ex b being Complex st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 )
set r = |.z.|;
A1: ( |.z.| = 0 implies ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )
proof
assume A2: |.z.| = 0 ; :: thesis: ex a being Element of COMPLEX st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take 1r ; :: thesis: ( |.1r.| = 1 & Re (1r * z) = |.z.| & Im (1r * z) = 0 )
thus ( |.1r.| = 1 & Re (1r * z) = |.z.| & Im (1r * z) = 0 ) by A2, COMPLEX1:4, COMPLEX1:45, COMPLEX1:48; :: thesis: verum
end;
( 0 < |.z.| implies ex a being Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )
proof
assume A3: 0 < |.z.| ; :: thesis: ex a being Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take ((Re z) / |.z.|) + (((- (Im z)) / |.z.|) * <i>) ; :: 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 )
thus ( |.(((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 ) by A3, Th2, COMPLEX1:44; :: thesis: verum
end;
hence ex b being Complex st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 ) by A1, COMPLEX1:46; :: thesis: verum