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 )
A4: Im (a - b) = (Im a) - (Im b) by COMPLEX1:48
.= - (Im b) by A1 ;
A5: (Re b) + 0 < Re a by A2, A3, Th35;
then (Re a) - (Re b) > 0 by XREAL_1:22;
then A6: Re (a - b) > 0 by COMPLEX1:48;
a = (Re a) + (0 * <i> ) by A1, COMPLEX1:29;
then A7: Arg a = 0 by A2, COMPTRIG:53;
then A8: (Arg (b - 0c )) - (Arg (a - 0c )) > 0 by A3, COMPTRIG:21;
- (- ((Re a) - (Re b))) > 0 by A5, XREAL_1:22;
then (Re b) - (Re a) < 0 ;
then A9: Re (b - a) < 0 by COMPLEX1:48;
A10: Im (b - a) = (Im b) - (Im a) by COMPLEX1:48
.= 0 by A1, A3, Th35 ;
then A11: - (Arg (b - a)) = - PI by A9, Th35;
A12: Arg (b - a) = PI by A9, A10, Th35;
A13: Arg (- b) = (Arg b) - PI by A3, Lm1, Th22, COMPTRIG:21;
A14: Im b = 0 by A3, Th35;
then A15: Arg (a - b) = 0 by A4, A6, Th34;
Arg (- a) = (Arg a) + PI by A2, A7, Th22, COMPLEX1:12, COMPTRIG:21
.= PI by A7 ;
then A16: angle b,a,0c = (Arg (0c - a)) - (Arg (b - a)) by A11, Def6;
A17: (Arg a) - (Arg (- a)) = (Arg a) - ((Arg a) + PI ) by A2, A7, Th22, COMPLEX1:12, COMPTRIG:21
.= - PI ;
A18: Arg (- b) = (Arg b) - PI by A3, Lm1, Th22, COMPTRIG:21;
then A19: (Arg (a - b)) - (Arg (0c - b)) = 0 by A3, A14, A4, A6, Th34;
then angle 0c ,b,a = (Arg (a - b)) - (Arg (- b)) by Def6;
hence A20: ((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 A8, A16, Def6
.= ((((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b))) + ((Arg (- a)) - (Arg (b - a)))
.= PI by A15, A12, A13, A17 ;
:: thesis: ( 0 = angle 0 ,b,a & 0 = angle b,a,0 )
((Arg (a - b)) + PI ) - (Arg b) = 0 by A3, A14, A4, A6, Th34;
then A21: angle 0c ,b,a = (Arg (a - b)) - (Arg (0c - b)) by A18, Def6;
thus 0 = angle 0 ,b,a by A19, Def6; :: thesis: 0 = angle b,a,0
angle a,0c ,b = (Arg b) - (Arg a) by A8, Def6;
hence 0 = angle b,a,0 by A3, A7, A19, A21, A20, XCMPLX_1:3; :: thesis: verum