let a, b be 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 ) ) )
A1: - ((Im (a .|. b)) / (|.a.| * |.b.|)) = (- (Im (a .|. b))) / (|.a.| * |.b.|) ;
assume A2: ( a <> 0 & b <> 0 ) ; :: thesis: ( Re (a .|. b) = 0 iff ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) )
then A3: ( |.a.| <> 0 & |.b.| <> 0 ) by COMPLEX1:45;
A4: ( angle (a,b) = angle (a,0c,b) & 0 <= angle (a,0c,b) ) by Th68, Th71;
A5: ( angle (a,0c,b) < 2 * PI & PI / 2 < 2 * PI ) by Th68, COMPTRIG:5, XXREAL_0:2;
A6: cos (angle (a,b)) = (Re (a .|. b)) / (|.a.| * |.b.|) by A2, Th67;
A7: sin (angle (a,b)) = - ((Im (a .|. b)) / (|.a.| * |.b.|)) by A2, Th67;
hereby :: thesis: ( ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) implies Re (a .|. b) = 0 )
assume A8: 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 Th48;
then ( sin (angle (a,b)) = 1 or sin (angle (a,b)) = - 1 ) by A7, A3, A1, XCMPLX_1:60;
hence ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) by A6, A4, A5, A8, Th11, COMPTRIG:5, SIN_COS:77; :: 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 A6, A3, Th71, SIN_COS:77; :: thesis: verum