let a, b be Element of COMPLEX ; :: thesis: ( a <> 0 & b <> 0 implies ( Re (a .|. b) = 0 iff ( angle a,0 ,b = PI / 2 or angle a,0 ,b = (3 / 2) * PI ) ) )
assume that
A1: a <> 0 and
A2: b <> 0 ; :: thesis: ( Re (a .|. b) = 0 iff ( angle a,0 ,b = PI / 2 or angle a,0 ,b = (3 / 2) * PI ) )
A3: ( cos (angle a,b) = (Re (a .|. b)) / (|.a.| * |.b.|) & sin (angle a,b) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) ) by A1, A2, Th83;
A4: angle a,b = angle a,0c ,b by Th87;
A5: ( |.a.| <> 0 & |.b.| <> 0 ) by A1, A2, COMPLEX1:131;
A6: ( 0 <= angle a,0c ,b & angle a,0c ,b < 2 * PI ) by Th84;
A7: PI / 2 < 2 * PI by COMPTRIG:21, XXREAL_0:2;
A8: - ((Im (a .|. b)) / (|.a.| * |.b.|)) = (- (Im (a .|. b))) / (|.a.| * |.b.|) ;

hereby :: thesis: ( ( angle a,0 ,b = PI / 2 or angle a,0 ,b = (3 / 2) * PI ) implies Re (a .|. b) = 0 )

assume A9: Re (a .|. b) = 0 ; :: thesis: ( angle a,0 ,b = PI / 2 or angle a,0 ,b = (3 / 2) * PI )
then ( Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) by Th64;
then ( sin (angle a,b) = 1 or sin (angle a,b) = - 1 ) by A3, A5, A8, XCMPLX_1:60;
hence ( angle a,0 ,b = PI / 2 or angle a,0 ,b = (3 / 2) * PI ) by A3, A4, A6, A7, A9, Th12, COMPTRIG:21, SIN_COS:82; :: thesis: verum

end;

assume ( angle a,0 ,b = PI / 2 or angle a,0 ,b = (3 / 2) * PI ) ; :: thesis: Re (a .|. b) = 0
hence Re (a .|. b) = 0 by A3, Th87, A5, SIN_COS:82; :: thesis: verum