let z be Element of F_Complex; :: thesis: ex b being Element of F_Complex st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 )
set r = |.z.|;
A1: ( |.z.| = 0 implies ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )
proof
assume A2: |.z.| = 0 ; :: thesis: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take a = 1. F_Complex; :: thesis: ( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
thus |.a.| = 1 by COMPLFLD:60; :: thesis: ( Re (a * z) = |.z.| & Im (a * z) = 0 )
z = 0. F_Complex by A2, COMPLFLD:58
.= 0 by COMPLFLD:def 1 ;
hence ( Re (a * z) = |.z.| & Im (a * z) = 0 ) by A2, Lm1, COMPLEX1:12; :: thesis: verum
end;
( 0 < |.z.| implies ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 ) )
proof
assume A3: 0 < |.z.| ; :: thesis: ex a being Element of F_Complex st
( |.a.| = 1 & Re (a * z) = |.z.| & Im (a * z) = 0 )
take [**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] ; :: thesis: ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 )
thus ( |.[**((Re z) / |.z.|),((- (Im z)) / |.z.|)**].| = 1 & Re ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = |.z.| & Im ([**((Re z) / |.z.|),((- (Im z)) / |.z.|)**] * z) = 0 ) by A3, Th7, COMPLFLD:57; :: thesis: verum
end;
hence ex b being Element of F_Complex st
( |.b.| = 1 & Re (b * z) = |.z.| & Im (b * z) = 0 ) by A1, COMPLEX1:46; :: thesis: verum