let a, b be Complex; ( 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 )
; ( 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 ( ( 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
;
( 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;
verum
end;
assume
( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI )
; Re (a .|. b) = 0
hence
Re (a .|. b) = 0
by A6, A3, Th71, SIN_COS:77; verum