let a, b be Complex; :: thesis: ( Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI implies ( ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = PI & 0 < angle (0c,b,a) & 0 < angle (b,a,0c) ) )
assume that
A1: Im a = 0 and
A2: Re a > 0 and
A3: 0 < Arg b and
A4: Arg b < PI ; :: thesis: ( ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = PI & 0 < angle (0c,b,a) & 0 < angle (b,a,0c) )
a = (Re a) + (0 * <i>) by A1, COMPLEX1:13;
then A5: Arg a = 0 by A2, COMPTRIG:35;
then A6: (Arg a) - (Arg (- a)) = (Arg a) - ((Arg a) + PI) by A2, Th12, COMPLEX1:4, COMPTRIG:5
.= - PI ;
(Arg (b - 0c)) - (Arg (a - 0c)) >= 0 by A3, A5;
then A7: angle (a,0c,b) = (Arg b) - (Arg a) by Def4;
Arg b in ].0,PI.[ by A3, A4, XXREAL_1:4;
then A8: Im b > 0 by Th16;
then A9: (Arg b) - (Arg (- b)) = (Arg b) - ((Arg b) + PI) by A4, Th12, COMPLEX1:4
.= - PI ;
A10: Im (a - b) = (Im a) - (Im b) by COMPLEX1:19
.= - (Im b) by A1 ;
then A11: Arg (a - b) > PI by A8, Th22;
then Arg (b - a) <= PI by A8, A10, Th15, COMPLEX1:4;
then A12: - (Arg (b - a)) >= - PI by XREAL_1:24;
A13: (Arg (a - b)) - (Arg (b - a)) = (Arg (a - b)) - (Arg (- (a - b)))
.= (Arg (a - b)) - ((Arg (a - b)) - PI) by A8, A10, A11, Th12, COMPLEX1:4
.= PI ;
Arg (- a) = (Arg a) + PI by A2, A5, Th12, COMPLEX1:4, COMPTRIG:5
.= PI by A5 ;
then (Arg (- a)) + (- (Arg (b - a))) >= (0 - PI) + PI by A12, XREAL_1:7;
then A14: angle (b,a,0c) = (Arg (0c - a)) - (Arg (b - a)) by Def4;
now :: thesis: for a, b being Complex st Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI holds
(Arg (b - a)) - (Arg b) > 0
let a, b be Complex; :: thesis: ( Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI implies (Arg (b2 - b1)) - (Arg b2) > 0 )
assume that
A15: Im a = 0 and
A16: Re a > 0 and
A17: ( 0 < Arg b & Arg b < PI ) ; :: thesis: (Arg (b2 - b1)) - (Arg b2) > 0
A18: (Re b) + (- (Re a)) < (Re b) + 0 by A16, XREAL_1:8;
set ba = b - a;
set B = Arg b;
set BA = Arg (b - a);
set mb = |.b.|;
set mba = |.(b - a).|;
A19: Re (b - a) = (Re b) - (Re a) by COMPLEX1:19;
( b - a = (|.(b - a).| * (cos (Arg (b - a)))) + ((|.(b - a).| * (sin (Arg (b - a)))) * <i>) & b - a = (Re (b - a)) + ((Im (b - a)) * <i>) ) by COMPTRIG:62, COMPLEX1:13;
then A20: Im (b - a) = |.(b - a).| * (sin (Arg (b - a))) by COMPLEX1:77;
set Rb = Re b;
set Rba = Re (b - a);
set Ib = Im b;
set Iba = Im (b - a);
A21: Im (b - a) = (Im b) - (Im a) by COMPLEX1:19
.= Im b by A15 ;
then A22: ( |.b.| = sqrt (((Re b) ^2) + ((Im b) ^2)) & |.(b - a).| = sqrt (((Re (b - a)) ^2) + ((Im b) ^2)) ) by COMPLEX1:def 12;
A23: ( (Re b) ^2 >= 0 & (Im b) ^2 >= 0 ) by XREAL_1:63;
A24: ( (Re (b - a)) ^2 >= 0 & (Im b) ^2 >= 0 ) by XREAL_1:63;
Arg b in ].0,PI.[ by A17, XXREAL_1:4;
then A25: Im b > 0 by Th16;
then A26: |.b.| >= 0 by COMPLEX1:4, COMPLEX1:47;
A27: |.(b - a).| >= 0 by A25, A21, COMPLEX1:4, COMPLEX1:47;
A28: sin (Arg (b - a)) > 0 by A25, A21, COMPTRIG:45;
A29: |.b.| <> 0 by A25, COMPLEX1:4, COMPLEX1:47;
( b = (|.b.| * (cos (Arg b))) + ((|.b.| * (sin (Arg b))) * <i>) & b = (Re b) + ((Im b) * <i>) ) by COMPTRIG:62, COMPLEX1:13;
then Im b = |.b.| * (sin (Arg b)) by COMPLEX1:77;
then A30: |.(b - a).| / |.b.| = (sin (Arg b)) / (sin (Arg (b - a))) by A21, A20, A29, A28, XCMPLX_1:94;
per cases ( 0 < Re (b - a) or 0 = Re (b - a) or 0 > Re (b - a) ) ;
suppose A31: 0 < Re (b - a) ; :: thesis: (Arg (b2 - b1)) - (Arg b2) > 0
then (Re b) ^2 > (Re (b - a)) ^2 by A19, A18, SQUARE_1:16;
then ((Re b) ^2) + ((Im b) ^2) > ((Re (b - a)) ^2) + ((Im b) ^2) by XREAL_1:8;
then |.b.| > |.(b - a).| by A22, A24, SQUARE_1:27;
then |.(b - a).| / |.b.| < 1 by A27, XREAL_1:189;
then ((sin (Arg b)) / (sin (Arg (b - a)))) * (sin (Arg (b - a))) < 1 * (sin (Arg (b - a))) by A28, A30, XREAL_1:68;
then A32: sin (Arg b) < 1 * (sin (Arg (b - a))) by A28, XCMPLX_1:87;
( Arg b in ].0,(PI / 2).[ & Arg (b - a) in ].0,(PI / 2).[ ) by A25, A21, A19, A18, A31, COMPTRIG:41;
then Arg (b - a) > Arg b by A32, Th6;
then (Arg (b - a)) + (- (Arg b)) > (Arg b) + (- (Arg b)) by XREAL_1:8;
hence (Arg (b - a)) - (Arg b) > 0 ; :: thesis: verum
end;
suppose A33: 0 = Re (b - a) ; :: thesis: (Arg (b2 - b1)) - (Arg b2) > 0
then b - a = 0 + ((Im (b - a)) * <i>) by COMPLEX1:13;
then A34: Arg (b - a) = PI / 2 by A25, A21, COMPTRIG:37;
Arg b in ].0,(PI / 2).[ by A16, A25, A19, A33, COMPTRIG:41;
then Arg b < Arg (b - a) by A34, XXREAL_1:4;
then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:8;
hence (Arg (b - a)) - (Arg b) > 0 ; :: thesis: verum
end;
suppose A35: 0 > Re (b - a) ; :: thesis: (Arg (b2 - b1)) - (Arg b2) > 0
thus (Arg (b - a)) - (Arg b) > 0 :: thesis: verum
proof
per cases ( 0 < Re b or 0 = Re b or 0 > Re b ) ;
suppose 0 < Re b ; :: thesis: (Arg (b - a)) - (Arg b) > 0
then Arg b in ].0,(PI / 2).[ by A25, COMPTRIG:41;
then A36: Arg b < PI / 2 by XXREAL_1:4;
Arg (b - a) in ].(PI / 2),PI.[ by A25, A21, A35, COMPTRIG:42;
then Arg (b - a) > PI / 2 by XXREAL_1:4;
then Arg (b - a) > Arg b by A36, XXREAL_0:2;
then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:8;
hence (Arg (b - a)) - (Arg b) > 0 ; :: thesis: verum
end;
suppose 0 = Re b ; :: thesis: (Arg (b - a)) - (Arg b) > 0
then b = 0 + ((Im b) * <i>) by COMPLEX1:13;
then A37: Arg b = PI / 2 by A25, COMPTRIG:37;
Arg (b - a) in ].(PI / 2),PI.[ by A25, A21, A35, COMPTRIG:42;
then Arg b < Arg (b - a) by A37, XXREAL_1:4;
then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:8;
hence (Arg (b - a)) - (Arg b) > 0 ; :: thesis: verum
end;
suppose A38: 0 > Re b ; :: thesis: (Arg (b - a)) - (Arg b) > 0
then (Re b) ^2 < (Re (b - a)) ^2 by A19, A18, SQUARE_1:44;
then ((Re b) ^2) + ((Im b) ^2) < ((Re (b - a)) ^2) + ((Im b) ^2) by XREAL_1:8;
then |.b.| < |.(b - a).| by A22, A23, SQUARE_1:27;
then |.(b - a).| / |.b.| > 1 by A26, A29, XREAL_1:187;
then ((sin (Arg b)) / (sin (Arg (b - a)))) * (sin (Arg (b - a))) > 1 * (sin (Arg (b - a))) by A28, A30, XREAL_1:68;
then A39: sin (Arg b) > 1 * (sin (Arg (b - a))) by A28, XCMPLX_1:87;
A40: Arg b in ].(PI / 2),PI.[ by A25, A38, COMPTRIG:42;
Arg (b - a) in ].(PI / 2),PI.[ by A25, A21, A35, COMPTRIG:42;
then Arg (b - a) > Arg b by A40, A39, Th7;
then (Arg (b - a)) + (- (Arg b)) > (Arg b) + (- (Arg b)) by XREAL_1:8;
hence (Arg (b - a)) - (Arg b) > 0 ; :: thesis: verum
end;
end;
end;
end;
end;
end;
then (Arg (b - a)) - (Arg b) > 0 by A1, A2, A3, A4;
then (Arg (- (a - b))) - (Arg b) > 0 ;
then ((Arg (a - b)) - PI) - (Arg b) > 0 by A8, A10, A11, Th12, COMPLEX1:4;
then A41: (Arg (a - b)) - ((Arg b) + PI) > 0 ;
then (Arg (a - b)) - (Arg (- b)) > 0 by A4, A8, Th12, COMPLEX1:4;
then angle (0c,b,a) = (Arg (a - b)) - (Arg (0c - b)) by Def4;
hence ((angle (a,0c,b)) + (angle (0c,b,a))) + (angle (b,a,0c)) = ((((Arg b) - (Arg (- b))) - (Arg a)) + (Arg (a - b))) + ((Arg (- a)) - (Arg (b - a))) by A7, A14
.= PI by A9, A6, A13 ;
:: thesis: ( 0 < angle (0c,b,a) & 0 < angle (b,a,0c) )
(Arg (a - b)) - (Arg (0c - b)) > 0 by A4, A8, A41, Th12, COMPLEX1:4;
hence 0 < angle (0c,b,a) by Def4; :: thesis: 0 < angle (b,a,0c)
A42: Arg a >= 0 by COMPTRIG:34;
2 * PI > 0 + (Arg (a - b)) by COMPTRIG:34;
then A43: (2 * PI) - (Arg (a - b)) > 0 by XREAL_1:20;
(Arg (- a)) - ((Arg (a - b)) - PI) = (Arg a) + ((2 * PI) - (Arg (a - b))) by A6;
hence 0 < angle (b,a,0c) by A14, A13, A43, A42; :: thesis: verum