let c1, c2 be Element of COMPLEX ; :: thesis: ( c2 <> 0 & (Arg c2) - (Arg c1) < 0 implies angle (c1,c2) = ((2 * PI) - (Arg c1)) + (Arg c2) )
assume that
A1: c2 <> 0 and
A2: (Arg c2) - (Arg c1) < 0 ; :: thesis: angle (c1,c2) = ((2 * PI) - (Arg c1)) + (Arg c2)
thus angle (c1,c2) = Arg (Rotate (c2,(- (Arg c1)))) by A1, COMPLEX2:def 3
.= ((2 * PI) - (Arg c1)) + (Arg c2) by A1, A2, Lm12 ; :: thesis: verum