let a, b be Element of 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:29;
then A5: Arg a = 0 by A2, COMPTRIG:53;
then A6: Arg (- a) = (Arg a) + PI by A2, Th22, COMPLEX1:12, COMPTRIG:21
.= PI by A5 ;
Arg b in ].0 ,PI .[ by A3, A4, XXREAL_1:4;
then A7: Im b > 0 by Th27;
A8: Im (a - b) = (Im a) - (Im b) by COMPLEX1:48
.= - (Im b) by A1 ;
A10: Arg (a - b) > PI by Th37, A7, A8;
(Arg (b - 0c )) - (Arg (a - 0c )) >= 0 by A3, A5;
then A11: angle a,0c ,b = (Arg b) - (Arg a) by Def6;
now
let a, b be Element of COMPLEX ; :: thesis: ( Im a = 0 & Re a > 0 & 0 < Arg b & Arg b < PI implies (Arg (b2 - b1)) - (Arg b2) > 0 )
assume that
A12: Im a = 0 and
A13: Re a > 0 and
A14: 0 < Arg b and
A15: Arg b < PI ; :: thesis: (Arg (b2 - b1)) - (Arg b2) > 0
Arg b in ].0 ,PI .[ by A14, A15, XXREAL_1:4;
then A16: Im b > 0 by Th27;
A17: Im (b - a) = (Im b) - (Im a) by COMPLEX1:48
.= Im b by A12 ;
A18: Re (b - a) = (Re b) - (Re a) by COMPLEX1:48;
A19: (Re b) + (- (Re a)) < (Re b) + 0 by XREAL_1:10, A13;
set ba = b - a;
set Rb = Re b;
set Rba = Re (b - a);
set Ib = Im b;
set Iba = Im (b - a);
set B = Arg b;
set BA = Arg (b - a);
set mb = |.b.|;
set mba = |.(b - a).|;
A20: b = (|.b.| * (cos (Arg b))) + ((|.b.| * (sin (Arg b))) * <i> ) by Th19;
b = (Re b) + ((Im b) * <i> ) by COMPLEX1:29;
then A21: ( Re b = |.b.| * (cos (Arg b)) & Im b = |.b.| * (sin (Arg b)) ) by A20, COMPLEX1:163;
A22: b - a = (|.(b - a).| * (cos (Arg (b - a)))) + ((|.(b - a).| * (sin (Arg (b - a)))) * <i> ) by Th19;
b - a = (Re (b - a)) + ((Im (b - a)) * <i> ) by COMPLEX1:29;
then A23: ( Re (b - a) = |.(b - a).| * (cos (Arg (b - a))) & Im (b - a) = |.(b - a).| * (sin (Arg (b - a))) ) by A22, COMPLEX1:163;
A24: |.b.| = sqrt (((Re b) ^2 ) + ((Im b) ^2 )) by COMPLEX1:def 16;
A25: |.(b - a).| = sqrt (((Re (b - a)) ^2 ) + ((Im b) ^2 )) by A17, COMPLEX1:def 16;
A26: ( |.b.| >= 0 & |.b.| <> 0 ) by A16, COMPLEX1:12, COMPLEX1:133;
A27: ( |.(b - a).| >= 0 & |.(b - a).| <> 0 ) by A16, A17, COMPLEX1:12, COMPLEX1:133;
B28: ( (Re (b - a)) ^2 >= 0 & (Im b) ^2 >= 0 ) by XREAL_1:65;
B29: ( (Re b) ^2 >= 0 & (Im b) ^2 >= 0 ) by XREAL_1:65;
A30: sin (Arg (b - a)) > 0 by A16, A17, COMPTRIG:63;
then A31: |.(b - a).| / |.b.| = (sin (Arg b)) / (sin (Arg (b - a))) by A17, A21, A23, A26, XCMPLX_1:95;
per cases ( 0 < Re (b - a) or 0 = Re (b - a) or 0 > Re (b - a) ) ;
suppose A32: 0 < Re (b - a) ; :: thesis: (Arg (b2 - b1)) - (Arg b2) > 0
then A33: Arg b in ].0 ,(PI / 2).[ by A16, A18, A19, COMPTRIG:59;
A34: Arg (b - a) in ].0 ,(PI / 2).[ by A16, A17, A32, COMPTRIG:59;
(Re b) ^2 > (Re (b - a)) ^2 by A18, A19, A32, SQUARE_1:78;
then ((Re b) ^2 ) + ((Im b) ^2 ) > ((Re (b - a)) ^2 ) + ((Im b) ^2 ) by XREAL_1:10;
then |.b.| > |.(b - a).| by A24, A25, B28, SQUARE_1:95;
then |.(b - a).| / |.b.| < 1 by A27, XREAL_1:191;
then ((sin (Arg b)) / (sin (Arg (b - a)))) * (sin (Arg (b - a))) < 1 * (sin (Arg (b - a))) by A30, A31, XREAL_1:70;
then sin (Arg b) < 1 * (sin (Arg (b - a))) by A30, XCMPLX_1:88;
then Arg (b - a) > Arg b by A33, A34, Th7;
then (Arg (b - a)) + (- (Arg b)) > (Arg b) + (- (Arg b)) by XREAL_1:10;
hence (Arg (b - a)) - (Arg b) > 0 ; :: thesis: verum
end;
suppose A35: 0 = Re (b - a) ; :: thesis: (Arg (b2 - b1)) - (Arg b2) > 0
then b - a = 0 + ((Im (b - a)) * <i> ) by COMPLEX1:29;
then A36: Arg (b - a) = PI / 2 by A16, A17, COMPTRIG:55;
Arg b in ].0 ,(PI / 2).[ by A16, A18, A13, A35, COMPTRIG:59;
then Arg b < Arg (b - a) by A36, XXREAL_1:4;
then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:10;
hence (Arg (b - a)) - (Arg b) > 0 ; :: thesis: verum
end;
suppose A37: 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 A16, COMPTRIG:59;
then A38: Arg b < PI / 2 by XXREAL_1:4;
Arg (b - a) in ].(PI / 2),PI .[ by A16, A17, A37, COMPTRIG:60;
then Arg (b - a) > PI / 2 by XXREAL_1:4;
then Arg (b - a) > Arg b by A38, XXREAL_0:2;
then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:10;
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:29;
then A39: Arg b = PI / 2 by A16, COMPTRIG:55;
Arg (b - a) in ].(PI / 2),PI .[ by A16, A17, A37, COMPTRIG:60;
then Arg b < Arg (b - a) by A39, XXREAL_1:4;
then (Arg b) + (- (Arg b)) < (Arg (b - a)) + (- (Arg b)) by XREAL_1:10;
hence (Arg (b - a)) - (Arg b) > 0 ; :: thesis: verum
end;
suppose A40: 0 > Re b ; :: thesis: (Arg (b - a)) - (Arg b) > 0
then A41: Arg b in ].(PI / 2),PI .[ by A16, COMPTRIG:60;
A42: Arg (b - a) in ].(PI / 2),PI .[ by A16, A17, A37, COMPTRIG:60;
(Re b) ^2 < (Re (b - a)) ^2 by A18, A19, A40, SQUARE_1:114;
then ((Re b) ^2 ) + ((Im b) ^2 ) < ((Re (b - a)) ^2 ) + ((Im b) ^2 ) by XREAL_1:10;
then |.b.| < |.(b - a).| by A24, A25, B29, SQUARE_1:95;
then |.(b - a).| / |.b.| > 1 by A26, XREAL_1:189;
then ((sin (Arg b)) / (sin (Arg (b - a)))) * (sin (Arg (b - a))) > 1 * (sin (Arg (b - a))) by A30, A31, XREAL_1:70;
then sin (Arg b) > 1 * (sin (Arg (b - a))) by A30, XCMPLX_1:88;
then Arg (b - a) > Arg b by A41, A42, Th8;
then (Arg (b - a)) + (- (Arg b)) > (Arg b) + (- (Arg b)) by XREAL_1:10;
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 A7, A8, A10, Th22, COMPLEX1:12;
then B43: (Arg (a - b)) - ((Arg b) + PI ) > 0 ;
then A43: (Arg (a - b)) - (Arg (- b)) > 0 by A4, A7, Th22, COMPLEX1:12;
A44: (Arg (a - b)) - (Arg (0c - b)) > 0 by A4, A7, Th22, COMPLEX1:12, B43;
A45: angle 0c ,b,a = (Arg (a - b)) - (Arg (0c - b)) by A43, Def6;
Arg (b - a) <= PI by A7, A8, A10, Th26, COMPLEX1:12;
then - (Arg (b - a)) >= - PI by XREAL_1:26;
then (Arg (- a)) + (- (Arg (b - a))) >= (0 - PI ) + PI by A6, XREAL_1:9;
then A46: angle b,a,0c = (Arg (0c - a)) - (Arg (b - a)) by Def6;
A47: (Arg b) - (Arg (- b)) = (Arg b) - ((Arg b) + PI ) by A4, A7, Th22, COMPLEX1:12
.= - PI ;
A48: (Arg a) - (Arg (- a)) = (Arg a) - ((Arg a) + PI ) by A2, A5, Th22, COMPLEX1:12, COMPTRIG:21
.= - PI ;
A49: (Arg (a - b)) - (Arg (b - a)) = (Arg (a - b)) - (Arg (- (a - b)))
.= (Arg (a - b)) - ((Arg (a - b)) - PI ) by A7, A8, A10, Th22, COMPLEX1:12
.= PI ;
thus ((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 A11, A45, A46
.= PI by A47, A48, A49 ; :: thesis: ( 0 < angle 0c ,b,a & 0 < angle b,a,0c )
thus 0 < angle 0c ,b,a by A44, Def6; :: thesis: 0 < angle b,a,0c
A50: (Arg (- a)) - ((Arg (a - b)) - PI ) = (Arg a) + ((2 * PI ) - (Arg (a - b))) by A48;
2 * PI > 0 + (Arg (a - b)) by COMPTRIG:52;
then ( (2 * PI ) - (Arg (a - b)) > 0 & Arg a >= 0 ) by COMPTRIG:52, XREAL_1:22;
hence 0 < angle b,a,0c by A46, A49, A50; :: thesis: verum