let a, b be Element of COMPLEX ; :: thesis: ( Im a = 0 & Re a > 0 & Arg b = PI implies ( ((angle a,0 ,b) + (angle 0 ,b,a)) + (angle b,a,0 ) = PI & 0 = angle 0 ,b,a & 0 = angle b,a,0 ) )
assume that
A1: Im a = 0 and
A2: Re a > 0 and
A3: Arg b = PI ; :: thesis: ( ((angle a,0 ,b) + (angle 0 ,b,a)) + (angle b,a,0 ) = PI & 0 = angle 0 ,b,a & 0 = angle b,a,0 )
a = (Re a) + (0 * <i> ) by A1, COMPLEX1:29;
then A4: Arg a = 0 by A2, COMPTRIG:53;
then A5: Arg (- a) = (Arg a) + PI by A2, Th22, COMPLEX1:12, COMPTRIG:21
.= PI by A4 ;
A6: ( Re b < 0 & Im b = 0 ) by A3, Th35;
A7: Im (a - b) = (Im a) - (Im b) by COMPLEX1:48
.= - (Im b) by A1 ;
A8: (Re b) + 0 < Re a by A2, A3, Th35;
then (Re a) - (Re b) > 0 by XREAL_1:22;
then A9: Re (a - b) > 0 by COMPLEX1:48;
then A10: Arg (a - b) = 0 by A6, A7, Th34;
- (- ((Re a) - (Re b))) > 0 by A8, XREAL_1:22;
then (Re b) - (Re a) < 0 ;
then A11: Re (b - a) < 0 by COMPLEX1:48;
A12: Im (b - a) = (Im b) - (Im a) by COMPLEX1:48
.= 0 by A1, A3, Th35 ;
then A13: Arg (b - a) = PI by A11, Th35;
A14: (Arg (b - 0c )) - (Arg (a - 0c )) > 0 by A3, A4, COMPTRIG:21;
then A15: angle a,0c ,b = (Arg b) - (Arg a) by Def6;
A16: Arg (- b) = (Arg b) - PI by A3, Lm2, Th22, COMPTRIG:21;
A17: ((Arg (a - b)) + PI ) - (Arg b) = 0 by A3, A6, A7, A9, Th34;
A18: (Arg (a - b)) - (Arg (0c - b)) = 0 by A3, A6, A7, A9, A16, Th34;
A19: angle 0c ,b,a = (Arg (a - b)) - (Arg (0c - b)) by A16, A17, Def6;
A20: angle 0c ,b,a = (Arg (a - b)) - (Arg (- b)) by A18, Def6;
- (Arg (b - a)) = - PI by A11, A12, Th35;
then A21: angle b,a,0c = (Arg (0c - a)) - (Arg (b - a)) by A5, Def6;
A22: Arg (- b) = (Arg b) - PI by A3, Lm2, Th22, COMPTRIG:21;
A23: (Arg a) - (Arg (- a)) = (Arg a) - ((Arg a) + PI ) by A2, A4, Th22, COMPLEX1:12, COMPTRIG:21
.= - PI ;
thus A24: ((angle a,0 ,b) + (angle 0 ,b,a)) + (angle b,a,0 ) = (((Arg b) - (Arg a)) + ((Arg (a - b)) - (Arg (- b)))) + ((Arg (0 - a)) - (Arg (b - a))) by A14, A20, A21, Def6
.= ((((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b))) + ((Arg (- a)) - (Arg (b - a)))
.= PI by A10, A13, A22, A23 ; :: thesis: ( 0 = angle 0 ,b,a & 0 = angle b,a,0 )
thus 0 = angle 0 ,b,a by A18, Def6; :: thesis: 0 = angle b,a,0
thus 0 = angle b,a,0 by A3, A4, A15, A18, A19, A24, XCMPLX_1:3; :: thesis: verum