let a, b be 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:19
.= - (Im b) by A1 ;
A5: (Re b) + 0 < Re a by A2, A3, Th20;
then (Re a) - (Re b) > 0 by XREAL_1:20;
then A6: Re (a - b) > 0 by COMPLEX1:19;
a = (Re a) + (0 * <i>) by A1, COMPLEX1:13;
then A7: Arg a = 0 by A2, COMPTRIG:35;
then A8: (Arg (b - 0c)) - (Arg (a - 0c)) > 0 by A3, COMPTRIG:5;
- (- ((Re a) - (Re b))) > 0 by A5, XREAL_1:20;
then (Re b) - (Re a) < 0 ;
then A9: Re (b - a) < 0 by COMPLEX1:19;
A10: Im (b - a) = (Im b) - (Im a) by COMPLEX1:19
.= 0 by A1, A3, Th20 ;
then A11: - (Arg (b - a)) = - PI by A9, Th20;
A12: Arg (b - a) = PI by A9, A10, Th20;
A13: Arg (- b) = (Arg b) - PI by A3, Lm1, Th12, COMPTRIG:5;
A14: Im b = 0 by A3, Th20;
then A15: Arg (a - b) = 0 by A4, A6, Th19;
Arg (- a) = (Arg a) + PI by A2, A7, Th12, COMPLEX1:4, COMPTRIG:5
.= PI by A7 ;
then A16: angle (b,a,0c) = (Arg (0c - a)) - (Arg (b - a)) by A11, Def4;
A17: (Arg a) - (Arg (- a)) = (Arg a) - ((Arg a) + PI) by A2, A7, Th12, COMPLEX1:4, COMPTRIG:5
.= - PI ;
A18: Arg (- b) = (Arg b) - PI by A3, Lm1, Th12, COMPTRIG:5;
then A19: (Arg (a - b)) - (Arg (0c - b)) = 0 by A3, A14, A4, A6, Th19;
then angle (0c,b,a) = (Arg (a - b)) - (Arg (- b)) by Def4;
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, Def4
.= ((((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, Th19;
then A21: angle (0c,b,a) = (Arg (a - b)) - (Arg (0c - b)) by A18, Def4;
thus 0 = angle (0,b,a) by A19, Def4; :: thesis: 0 = angle (b,a,0)
angle (a,0c,b) = (Arg b) - (Arg a) by A8, Def4;
hence 0 = angle (b,a,0) by A3, A7, A19, A21, A20, XCMPLX_1:3; :: thesis: verum