let x, y be Complex; :: thesis: ( Re (x .|. y) = 0 iff ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) )

hereby :: thesis: ( ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) implies Re (x .|. y) = 0 )

assume A1: Re (x .|. y) = 0 ; :: thesis: ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) )
(|.x.| * |.y.|) ^2 = |.(x .|. y).| ^2 by Th30
.= (0 ^2) + ((Im (x .|. y)) ^2) by A1, Lm2
.= (Im (x .|. y)) ^2 ;
hence ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) by SQUARE_1:40; :: thesis: verum

end;

hereby :: thesis: verum

assume ( Im (x .|. y) = |.x.| * |.y.| or Im (x .|. y) = - (|.x.| * |.y.|) ) ; :: thesis: Re (x .|. y) = 0
then (Im (x .|. y)) ^2 = (|.x.| * |.y.|) ^2
.= |.(x .|. y).| ^2 by Th30
.= ((Re (x .|. y)) ^2) + ((Im (x .|. y)) ^2) by Lm2 ;
hence Re (x .|. y) = 0 ; :: thesis: verum

end;