let a, b be Complex; :: thesis: ( a <> 0 & b <> 0 implies ( ( ( not Im (a .|. b) = |.a.| * |.b.| & not Im (a .|. b) = - (|.a.| * |.b.|) ) or angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) & ( ( not angle (a,0,b) = PI / 2 & not angle (a,0,b) = (3 / 2) * PI ) or Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) ) )
assume A1: ( a <> 0 & b <> 0 ) ; :: thesis: ( ( ( not Im (a .|. b) = |.a.| * |.b.| & not Im (a .|. b) = - (|.a.| * |.b.|) ) or angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) & ( ( not angle (a,0,b) = PI / 2 & not angle (a,0,b) = (3 / 2) * PI ) or Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) )
hereby :: thesis: ( ( not angle (a,0,b) = PI / 2 & not angle (a,0,b) = (3 / 2) * PI ) or Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) )
assume ( Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) ; :: thesis: ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI )
then Re (a .|. b) = 0 by Th48;
hence ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) by A1, Th73; :: thesis: verum
end;
hereby :: thesis: verum
assume ( angle (a,0,b) = PI / 2 or angle (a,0,b) = (3 / 2) * PI ) ; :: thesis: ( Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) )
then Re (a .|. b) = 0 by A1, Th73;
hence ( Im (a .|. b) = |.a.| * |.b.| or Im (a .|. b) = - (|.a.| * |.b.|) ) by Th48; :: thesis: verum
end;