comptrig.miz

begin

 reserve x for Real;

 scheme :: COMPTRIG:sch1

 Regrwithout0 { P[ Nat] } :

P[1]

 provided

 A1: ex k be non zero Nat st P[k]

 and

 A2: for k be non zero Nat st k <> 1 & P[k] holds ex n be non zero Nat st n < k & P[n];

 consider t be non zero Nat such that

 A3: P[t] by A1;

 defpred R[ Nat] means P[($1 + 1)];

 A4:

 now

 let k be Nat;

 assume that

 A5: k <> 0 and

 A6: R[k];

 reconsider k1 = (k + 1) as non zero Element of NAT ;

 (k + 1) > ( 0 + 1) by A5, XREAL_1: 6;

 then

 consider n be non zero Nat such that

 A7: n < k1 and

 A8: P[n] by A2, A6;

 consider l be Nat such that

 A9: n = (l + 1) by NAT_1: 6;

 take l;

 thus l < k by A7, A9, XREAL_1: 6;

 thus R[l] by A8, A9;

 end;

 ex s be Nat st t = (s + 1) by NAT_1: 6;

 then

 A10: ex k be Nat st R[k] by A3;

 R[ 0 ] from NAT_1:sch 7( A10, A4);

 hence thesis;

 end;

 theorem :: COMPTRIG:1



 Th1: for z be Complex holds ( Re z) >= ( - |.z.|)

 proof

 let z be Complex;

 0 <= (( Im z) ^2 ) by XREAL_1: 63;

 then

 A1: ((( Re z) ^2 ) + 0 ) <= ((( Re z) ^2 ) + (( Im z) ^2 )) by XREAL_1: 7;

 0 <= (( Re z) ^2 ) by XREAL_1: 63;

 then ( sqrt (( Re z) ^2 )) <= |.z.| by A1, SQUARE_1: 26;

 then ( - ( sqrt (( Re z) ^2 ))) >= ( - |.z.|) by XREAL_1: 24;

 then ( Re z) >= ( - |.( Re z).|) & ( - |.( Re z).|) >= ( - |.z.|) by ABSVALUE: 4, COMPLEX1: 72;

 hence thesis by XXREAL_0: 2;

 end;

 theorem :: COMPTRIG:2

 for z be Complex holds ( Im z) >= ( - |.z.|)

 proof

 let z be Complex;

 0 <= (( Re z) ^2 ) by XREAL_1: 63;

 then

 A1: ((( Im z) ^2 ) + 0 ) <= ((( Re z) ^2 ) + (( Im z) ^2 )) by XREAL_1: 7;

 0 <= (( Im z) ^2 ) by XREAL_1: 63;

 then ( sqrt (( Im z) ^2 )) <= |.z.| by A1, SQUARE_1: 26;

 then ( - ( sqrt (( Im z) ^2 ))) >= ( - |.z.|) by XREAL_1: 24;

 then ( Im z) >= ( - |.( Im z).|) & ( - |.( Im z).|) >= ( - |.z.|) by ABSVALUE: 4, COMPLEX1: 72;

 hence thesis by XXREAL_0: 2;

 end;

 theorem :: COMPTRIG:3



 Th3: for z be Complex holds ( |.z.| ^2 ) = ((( Re z) ^2 ) + (( Im z) ^2 ))

 proof

 let z be Complex;



 thus ( |.z.| ^2 ) = |.(z * z).| by COMPLEX1: 65

 .= ((( Re z) ^2 ) + (( Im z) ^2 )) by COMPLEX1: 68;

 end;

 theorem :: COMPTRIG:4



 Th4: for n be Nat st x >= 0 & n <> 0 holds ((n -root x) |^ n) = x

 proof

 let n be Nat;

 assume that

 A1: x >= 0 and

 A2: n <> 0 ;

 n >= ( 0 + 1) by A2, NAT_1: 13;

 hence thesis by A1, POWER: 4;

 end;

 registration

 cluster PI -> non negative;

 coherence

 proof

 PI in ]. 0 , 4.[ by SIN_COS:def 28;

 hence thesis by XXREAL_1: 4;

 end;

 end

 begin

 PI in ]. 0 , 4.[ by SIN_COS:def 28;

 then

 Lm1: 0 < PI by XXREAL_1: 4;

 then

 Lm2: ( 0 + ( PI / 2)) < (( PI / 2) + ( PI / 2)) by XREAL_1: 6;



 Lm3: ( 0 + PI ) < ( PI + PI ) by Lm1, XREAL_1: 6;



 Lm4: ( 0 + ( PI / 2)) < ( PI + ( PI / 2)) by Lm1, XREAL_1: 6;



 Lm5: (( PI / 2) + ( PI / 2)) < ( PI + ( PI / 2)) by Lm2, XREAL_1: 6;

 (((3 / 2) * PI ) + ( PI / 2)) = (2 * PI );

 then

 Lm6: ((3 / 2) * PI ) < (2 * PI ) by Lm5, XREAL_1: 6;



 Lm7: 0 < ((3 / 2) * PI ) by Lm1;

 theorem :: COMPTRIG:5

 0 < ( PI / 2) & ( PI / 2) < PI & 0 < PI & ( - ( PI / 2)) < ( PI / 2) & PI < (2 * PI ) & ( PI / 2) < ((3 / 2) * PI ) & ( - ( PI / 2)) < 0 & 0 < (2 * PI ) & PI < ((3 / 2) * PI ) & ((3 / 2) * PI ) < (2 * PI ) & 0 < ((3 / 2) * PI ) by Lm2, Lm3, Lm4, XREAL_1: 6;

 theorem :: COMPTRIG:6



 Th6: for a,b,c,x be Real st x in ].a, c.[ holds x in ].a, b.[ or x = b or x in ].b, c.[

 proof

 let a,b,c,x be Real;

 assume that

 A1: x in ].a, c.[ and

 A2: not x in ].a, b.[ and

 A3: not x = b;

 x <= a or x >= b by A2, XXREAL_1: 4;

 then

 A4: x > b by A1, A3, XXREAL_0: 1, XXREAL_1: 4;

 x < c by A1, XXREAL_1: 4;

 hence thesis by A4, XXREAL_1: 4;

 end;

 theorem :: COMPTRIG:7



 Th7: x in ]. 0 , PI .[ implies ( sin . x) > 0

 proof

 assume

 A1: x in ]. 0 , PI .[;

 per cases by A1, Th6;

 suppose

 A2: x in ]. 0 , ( PI / 2).[;

 then x < ( PI / 2) by XXREAL_1: 4;

 then ( - x) > ( - ( PI / 2)) by XREAL_1: 24;

 then

 A3: (( - x) + ( PI / 2)) > (( - ( PI / 2)) + ( PI / 2)) by XREAL_1: 6;

 0 < x by A2, XXREAL_1: 4;

 then (( - x) + ( PI / 2)) < ( 0 + ( PI / 2)) by XREAL_1: 6;

 then (( PI / 2) - x) in ]. 0 , ( PI / 2).[ by A3, XXREAL_1: 4;

 then ( cos . (( PI / 2) - x)) > 0 by SIN_COS: 80;

 hence thesis by SIN_COS: 78;

 end;

 suppose x = ( PI / 2);

 hence thesis by SIN_COS: 76;

 end;

 suppose

 A4: x in ].( PI / 2), PI .[;

 then x < PI by XXREAL_1: 4;

 then

 A5: (x - ( PI / 2)) < ( PI - ( PI / 2)) by XREAL_1: 9;

 ( PI / 2) < x by A4, XXREAL_1: 4;

 then (( PI / 2) - ( PI / 2)) < (x - ( PI / 2)) by XREAL_1: 9;

 then (x - ( PI / 2)) in ]. 0 , ( PI / 2).[ by A5, XXREAL_1: 4;

 then ( cos . ( - (( PI / 2) - x))) > 0 by SIN_COS: 80;

 then ( cos . (( PI / 2) - x)) > 0 by SIN_COS: 30;

 hence thesis by SIN_COS: 78;

 end;

 end;

 theorem :: COMPTRIG:8



 Th8: x in [. 0 , PI .] implies ( sin . x) >= 0

 proof

 assume

 A1: x in [. 0 , PI .];

 then x <= PI by XXREAL_1: 1;

 then x = 0 or x = PI or 0 < x & x < PI by A1, XXREAL_0: 1, XXREAL_1: 1;

 then x = 0 or x = PI or x in ]. 0 , PI .[ by XXREAL_1: 4;

 hence thesis by Th7, SIN_COS: 30, SIN_COS: 76;

 end;

 theorem :: COMPTRIG:9



 Th9: x in ]. PI , (2 * PI ).[ implies ( sin . x) < 0

 proof



 A1: ( sin . (x - PI )) = ( sin . ( - ( PI - x)))

 .= ( - ( sin . ( PI + ( - x)))) by SIN_COS: 30

 .= ( - ( - ( sin . ( - x)))) by SIN_COS: 78

 .= ( - ( sin . x)) by SIN_COS: 30;

 assume

 A2: x in ]. PI , (2 * PI ).[;

 then x < (2 * PI ) by XXREAL_1: 4;

 then

 A3: (x - PI ) < ((2 * PI ) - PI ) by XREAL_1: 9;

 PI < x by A2, XXREAL_1: 4;

 then ( PI - PI ) < (x - PI ) by XREAL_1: 9;

 then (x - PI ) in ]. 0 , PI .[ by A3, XXREAL_1: 4;

 hence thesis by A1, Th7;

 end;

 theorem :: COMPTRIG:10



 Th10: x in [. PI , (2 * PI ).] implies ( sin . x) <= 0

 proof

 assume x in [. PI , (2 * PI ).];

 then PI <= x & x <= (2 * PI ) by XXREAL_1: 1;

 then x = PI or x = (2 * PI ) or PI < x & x < (2 * PI ) by XXREAL_0: 1;

 then x = PI or x = (2 * PI ) or x in ]. PI , (2 * PI ).[ by XXREAL_1: 4;

 hence thesis by Th9, SIN_COS: 76;

 end;

 theorem :: COMPTRIG:11



 Th11: x in ].( - ( PI / 2)), ( PI / 2).[ implies ( cos . x) > 0

 proof



 A1: ( sin . (x + ( PI / 2))) = ( cos . x) by SIN_COS: 78;

 assume

 A2: x in ].( - ( PI / 2)), ( PI / 2).[;

 then x < ( PI / 2) by XXREAL_1: 4;

 then

 A3: (x + ( PI / 2)) < (( PI / 2) + ( PI / 2)) by XREAL_1: 6;

 ( - ( PI / 2)) < x by A2, XXREAL_1: 4;

 then (( - ( PI / 2)) + ( PI / 2)) < (x + ( PI / 2)) by XREAL_1: 6;

 then (x + ( PI / 2)) in ]. 0 , PI .[ by A3, XXREAL_1: 4;

 hence thesis by A1, Th7;

 end;

 theorem :: COMPTRIG:12



 Th12: x in [.( - ( PI / 2)), ( PI / 2).] implies ( cos . x) >= 0

 proof

 assume x in [.( - ( PI / 2)), ( PI / 2).];

 then ( - ( PI / 2)) <= x & x <= ( PI / 2) by XXREAL_1: 1;

 then x = ( - ( PI / 2)) or x = ( PI / 2) or ( - ( PI / 2)) < x & x < ( PI / 2) by XXREAL_0: 1;

 then x = ( - ( PI / 2)) or x = ( PI / 2) or x in ].( - ( PI / 2)), ( PI / 2).[ by XXREAL_1: 4;

 hence thesis by Th11, SIN_COS: 30, SIN_COS: 76;

 end;

 theorem :: COMPTRIG:13



 Th13: x in ].( PI / 2), ((3 / 2) * PI ).[ implies ( cos . x) < 0

 proof



 A1: ( sin . (x + ( PI / 2))) = ( cos . x) by SIN_COS: 78;

 assume

 A2: x in ].( PI / 2), ((3 / 2) * PI ).[;

 then x < ((3 / 2) * PI ) by XXREAL_1: 4;

 then

 A3: (x + ( PI / 2)) < (((3 / 2) * PI ) + ( PI / 2)) by XREAL_1: 6;

 ( PI / 2) < x by A2, XXREAL_1: 4;

 then (( PI / 2) + ( PI / 2)) < (x + ( PI / 2)) by XREAL_1: 6;

 then (x + ( PI / 2)) in ]. PI , (2 * PI ).[ by A3, XXREAL_1: 4;

 hence thesis by A1, Th9;

 end;

 theorem :: COMPTRIG:14



 Th14: x in [.( PI / 2), ((3 / 2) * PI ).] implies ( cos . x) <= 0

 proof

 assume x in [.( PI / 2), ((3 / 2) * PI ).];

 then ( PI / 2) <= x & x <= ((3 / 2) * PI ) by XXREAL_1: 1;

 then x = ( PI / 2) or x = ((3 / 2) * PI ) or ( PI / 2) < x & x < ((3 / 2) * PI ) by XXREAL_0: 1;

 then x = ( PI / 2) or x = ((3 / 2) * PI ) or x in ].( PI / 2), ((3 / 2) * PI ).[ by XXREAL_1: 4;

 hence thesis by Th13, SIN_COS: 76;

 end;

 theorem :: COMPTRIG:15



 Th15: x in ].((3 / 2) * PI ), (2 * PI ).[ implies ( cos . x) > 0

 proof



 A1: ( cos . (x - PI )) = ( cos . ( - ( PI - x)))

 .= ( cos . ( PI + ( - x))) by SIN_COS: 30

 .= ( - ( cos . ( - x))) by SIN_COS: 78

 .= ( - ( cos . x)) by SIN_COS: 30;

 assume

 A2: x in ].((3 / 2) * PI ), (2 * PI ).[;

 then x < (2 * PI ) by XXREAL_1: 4;

 then (x - PI ) < ((2 * PI ) - PI ) by XREAL_1: 9;

 then

 A3: (x - PI ) < ((3 / 2) * PI ) by Lm5, XXREAL_0: 2;

 ((3 / 2) * PI ) < x by A2, XXREAL_1: 4;

 then (((3 / 2) * PI ) - PI ) < (x - PI ) by XREAL_1: 9;

 then (x - PI ) in ].( PI / 2), ((3 / 2) * PI ).[ by A3, XXREAL_1: 4;

 hence thesis by A1, Th13;

 end;

 theorem :: COMPTRIG:16



 Th16: x in [.((3 / 2) * PI ), (2 * PI ).] implies ( cos . x) >= 0

 proof

 assume x in [.((3 / 2) * PI ), (2 * PI ).];

 then ((3 / 2) * PI ) <= x & x <= (2 * PI ) by XXREAL_1: 1;

 then x = ((3 / 2) * PI ) or x = (2 * PI ) or ((3 / 2) * PI ) < x & x < (2 * PI ) by XXREAL_0: 1;

 then x = ((3 / 2) * PI ) or x = (2 * PI ) or x in ].((3 / 2) * PI ), (2 * PI ).[ by XXREAL_1: 4;

 hence thesis by Th15, SIN_COS: 76;

 end;

 theorem :: COMPTRIG:17



 Th17: 0 <= x & x < (2 * PI ) & ( sin x) = 0 implies x = 0 or x = PI

 proof

 assume that

 A1: 0 <= x & x < (2 * PI ) and

 A2: ( sin x) = 0 ;

 ( sin . x) = 0 by A2, SIN_COS:def 17;

 then ( not x in ]. 0 , PI .[) & not x in ]. PI , (2 * PI ).[ by Th7, Th9;

 then x = 0 or x >= PI & PI >= x by A1, XXREAL_1: 4;

 hence thesis by XXREAL_0: 1;

 end;

 theorem :: COMPTRIG:18



 Th18: 0 <= x & x < (2 * PI ) & ( cos x) = 0 implies x = ( PI / 2) or x = ((3 / 2) * PI )

 proof

 assume that

 A1: 0 <= x and

 A2: x < (2 * PI ) and

 A3: ( cos x) = 0 ;



 A4: ( cos . x) = 0 by A3, SIN_COS:def 19;

 then not x in ].( PI / 2), ((3 / 2) * PI ).[ by Th13;

 then

 A5: ( PI / 2) >= x or x >= ((3 / 2) * PI ) by XXREAL_1: 4;

 not x in ].( - ( PI / 2)), ( PI / 2).[ by A4, Th11;

 then ( - ( PI / 2)) >= x or x >= ( PI / 2) by XXREAL_1: 4;

 then x = ( PI / 2) or x = ((3 / 2) * PI ) or x > ((3 / 2) * PI ) by A1, A5, Lm1, XXREAL_0: 1;

 then x = ( PI / 2) or x = ((3 / 2) * PI ) or x in ].((3 / 2) * PI ), (2 * PI ).[ by A2, XXREAL_1: 4;

 hence thesis by A4, Th15;

 end;

 theorem :: COMPTRIG:19



 Th19: ( sin | ].( - ( PI / 2)), ( PI / 2).[) is increasing

 proof



 A1: for x st x in ].( - ( PI / 2)), ( PI / 2).[ holds ( diff ( sin ,x)) > 0

 proof

 let x;

 assume x in ].( - ( PI / 2)), ( PI / 2).[;

 then 0 < ( cos . x) by Th11;

 hence thesis by SIN_COS: 68;

 end;

 ].( - ( PI / 2)), ( PI / 2).[ is open by RCOMP_1: 7;

 hence thesis by A1, FDIFF_1: 26, ROLLE: 9, SIN_COS: 24, SIN_COS: 68;

 end;

 theorem :: COMPTRIG:20



 Th20: ( sin | ].( PI / 2), ((3 / 2) * PI ).[) is decreasing

 proof



 A1: for x st x in ].( PI / 2), ((3 / 2) * PI ).[ holds ( diff ( sin ,x)) < 0

 proof

 let x;

 assume x in ].( PI / 2), ((3 / 2) * PI ).[;

 then 0 > ( cos . x) by Th13;

 hence thesis by SIN_COS: 68;

 end;

 ].( PI / 2), ((3 / 2) * PI ).[ is open by RCOMP_1: 7;

 hence thesis by A1, FDIFF_1: 26, ROLLE: 10, SIN_COS: 24, SIN_COS: 68;

 end;

 theorem :: COMPTRIG:21



 Th21: ( cos | ]. 0 , PI .[) is decreasing

 proof



 A1: for x st x in ]. 0 , PI .[ holds ( diff ( cos ,x)) < 0

 proof

 let x;

 assume x in ]. 0 , PI .[;

 then 0 < ( sin . x) by Th7;

 then ( 0 - ( sin . x)) < 0 ;

 hence thesis by SIN_COS: 67;

 end;

 ]. 0 , PI .[ is open by RCOMP_1: 7;

 hence thesis by A1, FDIFF_1: 26, ROLLE: 10, SIN_COS: 24, SIN_COS: 67;

 end;

 theorem :: COMPTRIG:22



 Th22: ( cos | ]. PI , (2 * PI ).[) is increasing

 proof



 A1: for x st x in ]. PI , (2 * PI ).[ holds ( diff ( cos ,x)) > 0

 proof

 let x;

 assume x in ]. PI , (2 * PI ).[;

 then ( 0 - ( sin . x)) > 0 by Th9, XREAL_1: 50;

 hence thesis by SIN_COS: 67;

 end;

 ]. PI , (2 * PI ).[ is open by RCOMP_1: 7;

 hence thesis by A1, FDIFF_1: 26, ROLLE: 9, SIN_COS: 24, SIN_COS: 67;

 end;

 theorem :: COMPTRIG:23

 ( sin | [.( - ( PI / 2)), ( PI / 2).]) is increasing

 proof

 now

 let r1,r2 be Real;

 assume that

 A1: r1 in ( [.( - ( PI / 2)), ( PI / 2).] /\ ( dom sin )) and

 A2: r2 in ( [.( - ( PI / 2)), ( PI / 2).] /\ ( dom sin )) and

 A3: r1 < r2;



 A4: r1 in ( dom sin ) by A1, XBOOLE_0:def 4;

 set r3 = ((r1 + r2) / 2);

 r1 in [.( - ( PI / 2)), ( PI / 2).] by A1, XBOOLE_0:def 4;

 then

 A5: ( - ( PI / 2)) <= r1 by XXREAL_1: 1;

 |.( sin r3).| <= 1 by SIN_COS: 27;

 then

 A6: |.( sin . r3).| <= 1 by SIN_COS:def 17;

 then

 A7: ( sin . r3) <= 1 by ABSVALUE: 5;

 r2 in [.( - ( PI / 2)), ( PI / 2).] by A2, XBOOLE_0:def 4;

 then

 A8: r2 <= ( PI / 2) by XXREAL_1: 1;



 A9: r1 < r3 by A3, XREAL_1: 226;

 then

 A10: ( - ( PI / 2)) < r3 by A5, XXREAL_0: 2;



 A11: r3 < r2 by A3, XREAL_1: 226;

 then r3 < ( PI / 2) by A8, XXREAL_0: 2;

 then r3 in ].( - ( PI / 2)), ( PI / 2).[ by A10, XXREAL_1: 4;

 then

 A12: r3 in ( ].( - ( PI / 2)), ( PI / 2).[ /\ ( dom sin )) by SIN_COS: 24, XBOOLE_0:def 4;

 |.( sin r2).| <= 1 by SIN_COS: 27;

 then |.( sin . r2).| <= 1 by SIN_COS:def 17;

 then

 A13: ( sin . r2) >= ( - 1) by ABSVALUE: 5;



 A14: r2 in ( dom sin ) by A2, XBOOLE_0:def 4;



 A15: ( sin . r3) >= ( - 1) by A6, ABSVALUE: 5;

 now

 per cases by A5, XXREAL_0: 1;

 suppose

 A16: ( - ( PI / 2)) < r1;

 then

 A17: ( - ( PI / 2)) < r2 by A3, XXREAL_0: 2;

 now

 per cases by A8, XXREAL_0: 1;

 suppose

 A18: r2 < ( PI / 2);

 then r1 < ( PI / 2) by A3, XXREAL_0: 2;

 then r1 in ].( - ( PI / 2)), ( PI / 2).[ by A16, XXREAL_1: 4;

 then

 A19: r1 in ( ].( - ( PI / 2)), ( PI / 2).[ /\ ( dom sin )) by A4, XBOOLE_0:def 4;

 r2 in ].( - ( PI / 2)), ( PI / 2).[ by A17, A18, XXREAL_1: 4;

 then r2 in ( ].( - ( PI / 2)), ( PI / 2).[ /\ ( dom sin )) by A14, XBOOLE_0:def 4;

 hence ( sin . r2) > ( sin . r1) by A3, A19, Th19, RFUNCT_2: 20;

 end;

 suppose

 A20: r2 = ( PI / 2);

 then r1 in ].( - ( PI / 2)), ( PI / 2).[ by A3, A16, XXREAL_1: 4;

 then r1 in ( ].( - ( PI / 2)), ( PI / 2).[ /\ ( dom sin )) by A4, XBOOLE_0:def 4;

 then

 A21: ( sin . r3) > ( sin . r1) by A9, A12, Th19, RFUNCT_2: 20;

 assume ( sin . r2) <= ( sin . r1);

 hence contradiction by A7, A20, A21, SIN_COS: 76, XXREAL_0: 2;

 end;

 end;

 hence ( sin . r2) > ( sin . r1);

 end;

 suppose

 A22: ( - ( PI / 2)) = r1;

 now

 per cases by A8, XXREAL_0: 1;

 suppose r2 < ( PI / 2);

 then r2 in ].( - ( PI / 2)), ( PI / 2).[ by A3, A22, XXREAL_1: 4;

 then r2 in ( ].( - ( PI / 2)), ( PI / 2).[ /\ ( dom sin )) by A14, XBOOLE_0:def 4;

 then

 A23: ( sin . r2) > ( sin . r3) by A11, A12, Th19, RFUNCT_2: 20;

 assume ( sin . r2) <= ( sin . r1);

 then ( sin . r2) <= ( - 1) by A22, SIN_COS: 30, SIN_COS: 76;

 hence contradiction by A15, A13, A23, XXREAL_0: 1;

 end;

 suppose r2 = ( PI / 2);

 hence ( sin . r2) > ( sin . r1) by A22, SIN_COS: 30, SIN_COS: 76;

 end;

 end;

 hence ( sin . r2) > ( sin . r1);

 end;

 end;

 hence ( sin . r2) > ( sin . r1);

 end;

 hence thesis by RFUNCT_2: 20;

 end;

 theorem :: COMPTRIG:24

 ( sin | [.( PI / 2), ((3 / 2) * PI ).]) is decreasing

 proof

 now

 let r1,r2 be Real;

 assume that

 A1: r1 in ( [.( PI / 2), ((3 / 2) * PI ).] /\ ( dom sin )) and

 A2: r2 in ( [.( PI / 2), ((3 / 2) * PI ).] /\ ( dom sin )) and

 A3: r1 < r2;



 A4: r1 in ( dom sin ) by A1, XBOOLE_0:def 4;

 |.( sin r2).| <= 1 by SIN_COS: 27;

 then |.( sin . r2).| <= 1 by SIN_COS:def 17;

 then

 A5: ( sin . r2) <= 1 by ABSVALUE: 5;

 |.( sin r1).| <= 1 by SIN_COS: 27;

 then |.( sin . r1).| <= 1 by SIN_COS:def 17;

 then

 A6: ( sin . r1) >= ( - 1) by ABSVALUE: 5;

 r2 in [.( PI / 2), ((3 / 2) * PI ).] by A2, XBOOLE_0:def 4;

 then

 A7: r2 <= ((3 / 2) * PI ) by XXREAL_1: 1;

 set r3 = ((r1 + r2) / 2);

 r1 in [.( PI / 2), ((3 / 2) * PI ).] by A1, XBOOLE_0:def 4;

 then

 A8: ( PI / 2) <= r1 by XXREAL_1: 1;

 |.( sin r3).| <= 1 by SIN_COS: 27;

 then

 A9: |.( sin . r3).| <= 1 by SIN_COS:def 17;

 then

 A10: ( sin . r3) <= 1 by ABSVALUE: 5;



 A11: r2 in ( dom sin ) by A2, XBOOLE_0:def 4;



 A12: r1 < r3 by A3, XREAL_1: 226;

 then

 A13: ( PI / 2) < r3 by A8, XXREAL_0: 2;



 A14: r3 < r2 by A3, XREAL_1: 226;

 then r3 < ((3 / 2) * PI ) by A7, XXREAL_0: 2;

 then r3 in ].( PI / 2), ((3 / 2) * PI ).[ by A13, XXREAL_1: 4;

 then

 A15: r3 in ( ].( PI / 2), ((3 / 2) * PI ).[ /\ ( dom sin )) by SIN_COS: 24, XBOOLE_0:def 4;



 A16: ( sin . r3) >= ( - 1) by A9, ABSVALUE: 5;

 now

 per cases by A8, XXREAL_0: 1;

 suppose

 A17: ( PI / 2) < r1;

 then

 A18: ( PI / 2) < r2 by A3, XXREAL_0: 2;

 now

 per cases by A7, XXREAL_0: 1;

 suppose

 A19: r2 < ((3 / 2) * PI );

 then r1 < ((3 / 2) * PI ) by A3, XXREAL_0: 2;

 then r1 in ].( PI / 2), ((3 / 2) * PI ).[ by A17, XXREAL_1: 4;

 then

 A20: r1 in ( ].( PI / 2), ((3 / 2) * PI ).[ /\ ( dom sin )) by A4, XBOOLE_0:def 4;

 r2 in ].( PI / 2), ((3 / 2) * PI ).[ by A18, A19, XXREAL_1: 4;

 then r2 in ( ].( PI / 2), ((3 / 2) * PI ).[ /\ ( dom sin )) by A11, XBOOLE_0:def 4;

 hence ( sin . r2) < ( sin . r1) by A3, A20, Th20, RFUNCT_2: 21;

 end;

 suppose

 A21: r2 = ((3 / 2) * PI );

 then r1 in ].( PI / 2), ((3 / 2) * PI ).[ by A3, A17, XXREAL_1: 4;

 then r1 in ( ].( PI / 2), ((3 / 2) * PI ).[ /\ ( dom sin )) by A4, XBOOLE_0:def 4;

 then

 A22: ( sin . r3) < ( sin . r1) by A12, A15, Th20, RFUNCT_2: 21;

 assume ( sin . r2) >= ( sin . r1);

 hence contradiction by A6, A16, A21, A22, SIN_COS: 76, XXREAL_0: 1;

 end;

 end;

 hence ( sin . r2) < ( sin . r1);

 end;

 suppose

 A23: ( PI / 2) = r1;

 now

 per cases by A7, XXREAL_0: 1;

 suppose r2 < ((3 / 2) * PI );

 then r2 in ].( PI / 2), ((3 / 2) * PI ).[ by A3, A23, XXREAL_1: 4;

 then r2 in ( ].( PI / 2), ((3 / 2) * PI ).[ /\ ( dom sin )) by A11, XBOOLE_0:def 4;

 then

 A24: ( sin . r2) < ( sin . r3) by A14, A15, Th20, RFUNCT_2: 21;

 assume ( sin . r2) >= ( sin . r1);

 hence contradiction by A10, A5, A23, A24, SIN_COS: 76, XXREAL_0: 1;

 end;

 suppose r2 = ((3 / 2) * PI );

 hence ( sin . r2) < ( sin . r1) by A23, SIN_COS: 76;

 end;

 end;

 hence ( sin . r2) < ( sin . r1);

 end;

 end;

 hence ( sin . r2) < ( sin . r1);

 end;

 hence thesis by RFUNCT_2: 21;

 end;

 theorem :: COMPTRIG:25



 Th25: ( cos | [. 0 , PI .]) is decreasing

 proof

 now

 let r1,r2 be Real;

 assume that

 A1: r1 in ( [. 0 , PI .] /\ ( dom cos )) and

 A2: r2 in ( [. 0 , PI .] /\ ( dom cos )) and

 A3: r1 < r2;



 A4: r1 in ( dom cos ) by A1, XBOOLE_0:def 4;

 |.( cos r2).| <= 1 by SIN_COS: 27;

 then |.( cos . r2).| <= 1 by SIN_COS:def 19;

 then

 A5: ( cos . r2) <= 1 by ABSVALUE: 5;

 |.( cos r1).| <= 1 by SIN_COS: 27;

 then |.( cos . r1).| <= 1 by SIN_COS:def 19;

 then

 A6: ( cos . r1) >= ( - 1) by ABSVALUE: 5;

 r2 in [. 0 , PI .] by A2, XBOOLE_0:def 4;

 then

 A7: r2 <= PI by XXREAL_1: 1;

 set r3 = ((r1 + r2) / 2);



 A8: r1 < r3 by A3, XREAL_1: 226;

 |.( cos r3).| <= 1 by SIN_COS: 27;

 then

 A9: |.( cos . r3).| <= 1 by SIN_COS:def 19;

 then

 A10: ( cos . r3) <= 1 by ABSVALUE: 5;



 A11: r2 in ( dom cos ) by A2, XBOOLE_0:def 4;



 A12: r1 in [. 0 , PI .] by A1, XBOOLE_0:def 4;

 then

 A13: 0 < r3 by A8, XXREAL_1: 1;



 A14: r3 < r2 by A3, XREAL_1: 226;

 then r3 < PI by A7, XXREAL_0: 2;

 then r3 in ]. 0 , PI .[ by A13, XXREAL_1: 4;

 then

 A15: r3 in ( ]. 0 , PI .[ /\ ( dom cos )) by SIN_COS: 24, XBOOLE_0:def 4;



 A16: ( cos . r3) >= ( - 1) by A9, ABSVALUE: 5;

 now

 per cases by A12, XXREAL_1: 1;

 suppose

 A17: 0 < r1;

 now

 per cases by A7, XXREAL_0: 1;

 suppose

 A18: r2 < PI ;

 then r1 < PI by A3, XXREAL_0: 2;

 then r1 in ]. 0 , PI .[ by A17, XXREAL_1: 4;

 then

 A19: r1 in ( ]. 0 , PI .[ /\ ( dom cos )) by A4, XBOOLE_0:def 4;

 r2 in ]. 0 , PI .[ by A3, A17, A18, XXREAL_1: 4;

 then r2 in ( ]. 0 , PI .[ /\ ( dom cos )) by A11, XBOOLE_0:def 4;

 hence ( cos . r2) < ( cos . r1) by A3, A19, Th21, RFUNCT_2: 21;

 end;

 suppose

 A20: r2 = PI ;

 then r1 in ]. 0 , PI .[ by A3, A17, XXREAL_1: 4;

 then r1 in ( ]. 0 , PI .[ /\ ( dom cos )) by A4, XBOOLE_0:def 4;

 then

 A21: ( cos . r3) < ( cos . r1) by A8, A15, Th21, RFUNCT_2: 21;

 assume ( cos . r2) >= ( cos . r1);

 hence contradiction by A6, A16, A20, A21, SIN_COS: 76, XXREAL_0: 1;

 end;

 end;

 hence ( cos . r2) < ( cos . r1);

 end;

 suppose

 A22: 0 = r1;

 now

 per cases by A7, XXREAL_0: 1;

 suppose r2 < PI ;

 then r2 in ]. 0 , PI .[ by A3, A22, XXREAL_1: 4;

 then r2 in ( ]. 0 , PI .[ /\ ( dom cos )) by A11, XBOOLE_0:def 4;

 then

 A23: ( cos . r2) < ( cos . r3) by A14, A15, Th21, RFUNCT_2: 21;

 assume ( cos . r2) >= ( cos . r1);

 hence contradiction by A10, A5, A22, A23, SIN_COS: 30, XXREAL_0: 1;

 end;

 suppose r2 = PI ;

 hence ( cos . r2) < ( cos . r1) by A22, SIN_COS: 30, SIN_COS: 76;

 end;

 end;

 hence ( cos . r2) < ( cos . r1);

 end;

 end;

 hence ( cos . r2) < ( cos . r1);

 end;

 hence thesis by RFUNCT_2: 21;

 end;

 theorem :: COMPTRIG:26



 Th26: ( cos | [. PI , (2 * PI ).]) is increasing

 proof

 now

 let r1,r2 be Real;

 assume that

 A1: r1 in ( [. PI , (2 * PI ).] /\ ( dom cos )) and

 A2: r2 in ( [. PI , (2 * PI ).] /\ ( dom cos )) and

 A3: r1 < r2;



 A4: r1 in ( dom cos ) by A1, XBOOLE_0:def 4;

 set r3 = ((r1 + r2) / 2);

 r1 in [. PI , (2 * PI ).] by A1, XBOOLE_0:def 4;

 then

 A5: PI <= r1 by XXREAL_1: 1;

 |.( cos r3).| <= 1 by SIN_COS: 27;

 then

 A6: |.( cos . r3).| <= 1 by SIN_COS:def 19;

 then

 A7: ( cos . r3) <= 1 by ABSVALUE: 5;

 r2 in [. PI , (2 * PI ).] by A2, XBOOLE_0:def 4;

 then

 A8: r2 <= (2 * PI ) by XXREAL_1: 1;



 A9: r1 < r3 by A3, XREAL_1: 226;

 then

 A10: PI < r3 by A5, XXREAL_0: 2;



 A11: r3 < r2 by A3, XREAL_1: 226;

 then r3 < (2 * PI ) by A8, XXREAL_0: 2;

 then r3 in ]. PI , (2 * PI ).[ by A10, XXREAL_1: 4;

 then

 A12: r3 in ( ]. PI , (2 * PI ).[ /\ ( dom cos )) by SIN_COS: 24, XBOOLE_0:def 4;

 |.( cos r2).| <= 1 by SIN_COS: 27;

 then |.( cos . r2).| <= 1 by SIN_COS:def 19;

 then

 A13: ( cos . r2) >= ( - 1) by ABSVALUE: 5;



 A14: r2 in ( dom cos ) by A2, XBOOLE_0:def 4;



 A15: ( cos . r3) >= ( - 1) by A6, ABSVALUE: 5;

 now

 per cases by A5, XXREAL_0: 1;

 suppose

 A16: PI < r1;

 then

 A17: PI < r2 by A3, XXREAL_0: 2;

 now

 per cases by A8, XXREAL_0: 1;

 suppose

 A18: r2 < (2 * PI );

 then r1 < (2 * PI ) by A3, XXREAL_0: 2;

 then r1 in ]. PI , (2 * PI ).[ by A16, XXREAL_1: 4;

 then

 A19: r1 in ( ]. PI , (2 * PI ).[ /\ ( dom cos )) by A4, XBOOLE_0:def 4;

 r2 in ]. PI , (2 * PI ).[ by A17, A18, XXREAL_1: 4;

 then r2 in ( ]. PI , (2 * PI ).[ /\ ( dom cos )) by A14, XBOOLE_0:def 4;

 hence ( cos . r2) > ( cos . r1) by A3, A19, Th22, RFUNCT_2: 20;

 end;

 suppose

 A20: r2 = (2 * PI );

 then r1 in ]. PI , (2 * PI ).[ by A3, A16, XXREAL_1: 4;

 then r1 in ( ]. PI , (2 * PI ).[ /\ ( dom cos )) by A4, XBOOLE_0:def 4;

 then

 A21: ( cos . r3) > ( cos . r1) by A9, A12, Th22, RFUNCT_2: 20;

 assume ( cos . r2) <= ( cos . r1);

 hence contradiction by A7, A20, A21, SIN_COS: 76, XXREAL_0: 2;

 end;

 end;

 hence ( cos . r2) > ( cos . r1);

 end;

 suppose

 A22: PI = r1;

 now

 per cases by A8, XXREAL_0: 1;

 suppose r2 < (2 * PI );

 then r2 in ]. PI , (2 * PI ).[ by A3, A22, XXREAL_1: 4;

 then r2 in ( ]. PI , (2 * PI ).[ /\ ( dom cos )) by A14, XBOOLE_0:def 4;

 then

 A23: ( cos . r2) > ( cos . r3) by A11, A12, Th22, RFUNCT_2: 20;

 assume ( cos . r2) <= ( cos . r1);

 hence contradiction by A15, A13, A22, A23, SIN_COS: 76, XXREAL_0: 1;

 end;

 suppose r2 = (2 * PI );

 hence ( cos . r2) > ( cos . r1) by A22, SIN_COS: 76;

 end;

 end;

 hence ( cos . r2) > ( cos . r1);

 end;

 end;

 hence ( cos . r2) > ( cos . r1);

 end;

 hence thesis by RFUNCT_2: 20;

 end;

 theorem :: COMPTRIG:27



 Th27: ( sin . x) in [.( - 1), 1.] & ( cos . x) in [.( - 1), 1.]

 proof

 |.( cos x).| <= 1 by SIN_COS: 27;

 then |.( cos . x).| <= 1 by SIN_COS:def 19;

 then

 A1: ( - 1) <= ( cos . x) & ( cos . x) <= 1 by ABSVALUE: 5;

 |.( sin x).| <= 1 by SIN_COS: 27;

 then |.( sin . x).| <= 1 by SIN_COS:def 17;

 then ( - 1) <= ( sin . x) & ( sin . x) <= 1 by ABSVALUE: 5;

 hence thesis by A1, XXREAL_1: 1;

 end;

 theorem :: COMPTRIG:28

 ( rng sin ) = [.( - 1), 1.]

 proof

 now

 let y be object;

 thus y in [.( - 1), 1.] implies ex x be object st x in ( dom sin ) & y = ( sin . x)

 proof

 assume

 A1: y in [.( - 1), 1.];

 then

 reconsider y1 = y as Real;

 y1 in ( [.( - 1), 1.] \/ [.1, ( sin . ( - ( PI / 2))).]) by A1, XBOOLE_0:def 3;

 then ( sin | [.( - ( PI / 2)), ( PI / 2).]) is continuous & y1 in ( [.( sin . ( - ( PI / 2))), ( sin . ( PI / 2)).] \/ [.( sin . ( PI / 2)), ( sin . ( - ( PI / 2))).]) by SIN_COS: 30, SIN_COS: 76;

 then

 consider x be Real such that x in [.( - ( PI / 2)), ( PI / 2).] and

 A2: y1 = ( sin . x) by FCONT_2: 15, SIN_COS: 24;

 take x;

 x in REAL by XREAL_0:def 1;

 hence thesis by A2, SIN_COS: 24;

 end;

 thus (ex x be object st x in ( dom sin ) & y = ( sin . x)) implies y in [.( - 1), 1.] by Th27, SIN_COS: 24;

 end;

 hence thesis by FUNCT_1:def 3;

 end;

 theorem :: COMPTRIG:29

 ( rng cos ) = [.( - 1), 1.]

 proof

 now

 let y be object;

 thus y in [.( - 1), 1.] implies ex x be object st x in ( dom cos ) & y = ( cos . x)

 proof

 assume

 A1: y in [.( - 1), 1.];

 then

 reconsider y1 = y as Real;

 ( cos | [. 0 , PI .]) is continuous & y1 in ( [.( cos . 0 ), ( cos . PI ).] \/ [.( cos . PI ), ( cos . 0 ).]) by A1, SIN_COS: 30, SIN_COS: 76, XBOOLE_0:def 3;

 then

 consider x be Real such that x in [. 0 , PI .] and

 A2: y1 = ( cos . x) by FCONT_2: 15, SIN_COS: 24;

 take x;

 x in REAL by XREAL_0:def 1;

 hence thesis by A2, SIN_COS: 24;

 end;

 thus (ex x be object st x in ( dom cos ) & y = ( cos . x)) implies y in [.( - 1), 1.] by Th27, SIN_COS: 24;

 end;

 hence thesis by FUNCT_1:def 3;

 end;

 theorem :: COMPTRIG:30

 ( rng ( sin | [.( - ( PI / 2)), ( PI / 2).])) = [.( - 1), 1.]

 proof

 set sin1 = ( sin | [.( - ( PI / 2)), ( PI / 2).]);

 now

 let y be object;

 thus y in [.( - 1), 1.] implies ex x be object st x in ( dom sin1) & y = (sin1 . x)

 proof

 assume

 A1: y in [.( - 1), 1.];

 then

 reconsider y1 = y as Real;

 ( PI / 2) in [.( - ( PI / 2)), ( PI / 2).] by XXREAL_1: 1;

 then

 A2: (sin1 . ( PI / 2)) = ( sin . ( PI / 2)) by FUNCT_1: 49;

 ( - ( PI / 2)) in [.( - ( PI / 2)), ( PI / 2).] by XXREAL_1: 1;

 then (sin1 . ( - ( PI / 2))) = ( sin . ( - ( PI / 2))) by FUNCT_1: 49;

 then y1 in [.(sin1 . ( - ( PI / 2))), (sin1 . ( PI / 2)).] by A1, A2, SIN_COS: 30, SIN_COS: 76;

 then

 A3: (sin1 | [.( - ( PI / 2)), ( PI / 2).]) is continuous & y1 in ( [.(sin1 . ( - ( PI / 2))), (sin1 . ( PI / 2)).] \/ [.(sin1 . ( PI / 2)), (sin1 . ( - ( PI / 2))).]) by XBOOLE_0:def 3;

 ( dom sin1) = ( [.( - ( PI / 2)), ( PI / 2).] /\ REAL ) by RELAT_1: 61, SIN_COS: 24

 .= [.( - ( PI / 2)), ( PI / 2).] by XBOOLE_1: 28;

 then

 consider x be Real such that

 A4: x in [.( - ( PI / 2)), ( PI / 2).] and

 A5: y1 = (sin1 . x) by A3, FCONT_2: 15;

 take x;

 x in ( REAL /\ [.( - ( PI / 2)), ( PI / 2).]) by A4, XBOOLE_0:def 4;

 hence thesis by A5, RELAT_1: 61, SIN_COS: 24;

 end;

 thus (ex x be object st x in ( dom sin1) & y = (sin1 . x)) implies y in [.( - 1), 1.]

 proof

 given x be object such that

 A6: x in ( dom sin1) and

 A7: y = (sin1 . x);

 ( dom sin1) c= ( dom sin ) by RELAT_1: 60;

 then

 reconsider x1 = x as Real by A6, SIN_COS: 24;

 y = ( sin . x1) by A6, A7, FUNCT_1: 47;

 hence thesis by Th27;

 end;

 end;

 hence thesis by FUNCT_1:def 3;

 end;

 theorem :: COMPTRIG:31

 ( rng ( sin | [.( PI / 2), ((3 / 2) * PI ).])) = [.( - 1), 1.]

 proof

 set sin1 = ( sin | [.( PI / 2), ((3 / 2) * PI ).]);

 now

 let y be object;

 thus y in [.( - 1), 1.] implies ex x be object st x in ( dom sin1) & y = (sin1 . x)

 proof

 ((3 / 2) * PI ) in [.( PI / 2), ((3 / 2) * PI ).] by Lm4, XXREAL_1: 1;

 then

 A1: (sin1 . ((3 / 2) * PI )) = ( sin . ((3 / 2) * PI )) by FUNCT_1: 49;

 assume

 A2: y in [.( - 1), 1.];

 then

 reconsider y1 = y as Real;



 A3: ( dom sin1) = ( [.( PI / 2), ((3 / 2) * PI ).] /\ REAL ) by RELAT_1: 61, SIN_COS: 24

 .= [.( PI / 2), ((3 / 2) * PI ).] by XBOOLE_1: 28;

 ( PI / 2) in [.( PI / 2), ((3 / 2) * PI ).] by Lm4, XXREAL_1: 1;

 then (sin1 . ( PI / 2)) = ( sin . ( PI / 2)) by FUNCT_1: 49;

 then (sin1 | [.( PI / 2), ((3 / 2) * PI ).]) is continuous & y1 in ( [.(sin1 . ( PI / 2)), (sin1 . ((3 / 2) * PI )).] \/ [.(sin1 . ((3 / 2) * PI )), (sin1 . ( PI / 2)).]) by A2, A1, SIN_COS: 76, XBOOLE_0:def 3;

 then

 consider x be Real such that

 A4: x in [.( PI / 2), ((3 / 2) * PI ).] and

 A5: y1 = (sin1 . x) by A3, Lm4, FCONT_2: 15;

 take x;

 x in ( REAL /\ [.( PI / 2), ((3 / 2) * PI ).]) by A4, XBOOLE_0:def 4;

 hence thesis by A5, RELAT_1: 61, SIN_COS: 24;

 end;

 thus (ex x be object st x in ( dom sin1) & y = (sin1 . x)) implies y in [.( - 1), 1.]

 proof

 given x be object such that

 A6: x in ( dom sin1) and

 A7: y = (sin1 . x);

 ( dom sin1) c= ( dom sin ) by RELAT_1: 60;

 then

 reconsider x1 = x as Real by A6, SIN_COS: 24;

 y = ( sin . x1) by A6, A7, FUNCT_1: 47;

 hence thesis by Th27;

 end;

 end;

 hence thesis by FUNCT_1:def 3;

 end;

 theorem :: COMPTRIG:32



 Th32: ( rng ( cos | [. 0 , PI .])) = [.( - 1), 1.]

 proof

 set cos1 = ( cos | [. 0 , PI .]);

 now

 let y be object;

 thus y in [.( - 1), 1.] implies ex x be object st x in ( dom cos1) & y = (cos1 . x)

 proof

 PI in [. 0 , PI .] by XXREAL_1: 1;

 then

 A1: (cos1 . PI ) = ( cos . PI ) by FUNCT_1: 49;

 assume

 A2: y in [.( - 1), 1.];

 then

 reconsider y1 = y as Real;



 A3: ( dom cos1) = ( [. 0 , PI .] /\ REAL ) by RELAT_1: 61, SIN_COS: 24

 .= [. 0 , PI .] by XBOOLE_1: 28;

 0 in [. 0 , PI .] by XXREAL_1: 1;

 then (cos1 . 0 ) = ( cos . 0 ) by FUNCT_1: 49;

 then (cos1 | [. 0 , PI .]) is continuous & y1 in ( [.(cos1 . 0 ), (cos1 . PI ).] \/ [.(cos1 . PI ), (cos1 . 0 ).]) by A2, A1, SIN_COS: 30, SIN_COS: 76, XBOOLE_0:def 3;

 then

 consider x be Real such that

 A4: x in [. 0 , PI .] and

 A5: y1 = (cos1 . x) by A3, FCONT_2: 15;

 take x;

 x in ( REAL /\ [. 0 , PI .]) by A4, XBOOLE_0:def 4;

 hence thesis by A5, RELAT_1: 61, SIN_COS: 24;

 end;

 thus (ex x be object st x in ( dom cos1) & y = (cos1 . x)) implies y in [.( - 1), 1.]

 proof

 given x be object such that

 A6: x in ( dom cos1) and

 A7: y = (cos1 . x);

 ( dom cos1) c= ( dom cos ) by RELAT_1: 60;

 then

 reconsider x1 = x as Real by A6, SIN_COS: 24;

 y = ( cos . x1) by A6, A7, FUNCT_1: 47;

 hence thesis by Th27;

 end;

 end;

 hence thesis by FUNCT_1:def 3;

 end;

 theorem :: COMPTRIG:33



 Th33: ( rng ( cos | [. PI , (2 * PI ).])) = [.( - 1), 1.]

 proof

 set cos1 = ( cos | [. PI , (2 * PI ).]);

 now

 let y be object;

 thus y in [.( - 1), 1.] implies ex x be object st x in ( dom cos1) & y = (cos1 . x)

 proof

 (2 * PI ) in [. PI , (2 * PI ).] by Lm3, XXREAL_1: 1;

 then

 A1: (cos1 . (2 * PI )) = ( cos . (2 * PI )) by FUNCT_1: 49;

 assume

 A2: y in [.( - 1), 1.];

 then

 reconsider y1 = y as Real;



 A3: ( dom cos1) = ( [. PI , (2 * PI ).] /\ REAL ) by RELAT_1: 61, SIN_COS: 24

 .= [. PI , (2 * PI ).] by XBOOLE_1: 28;

 PI in [. PI , (2 * PI ).] by Lm3, XXREAL_1: 1;

 then (cos1 . PI ) = ( cos . PI ) by FUNCT_1: 49;

 then (cos1 | [. PI , (2 * PI ).]) is continuous & y1 in ( [.(cos1 . PI ), (cos1 . (2 * PI )).] \/ [.(cos1 . (2 * PI )), (cos1 . PI ).]) by A2, A1, SIN_COS: 76, XBOOLE_0:def 3;

 then

 consider x be Real such that

 A4: x in [. PI , (2 * PI ).] and

 A5: y1 = (cos1 . x) by A3, Lm3, FCONT_2: 15;

 take x;

 x in ( REAL /\ [. PI , (2 * PI ).]) by A4, XBOOLE_0:def 4;

 hence thesis by A5, RELAT_1: 61, SIN_COS: 24;

 end;

 thus (ex x be object st x in ( dom cos1) & y = (cos1 . x)) implies y in [.( - 1), 1.]

 proof

 given x be object such that

 A6: x in ( dom cos1) and

 A7: y = (cos1 . x);

 ( dom cos1) c= ( dom cos ) by RELAT_1: 60;

 then

 reconsider x1 = x as Real by A6, SIN_COS: 24;

 y = ( cos . x1) by A6, A7, FUNCT_1: 47;

 hence thesis by Th27;

 end;

 end;

 hence thesis by FUNCT_1:def 3;

 end;

 begin

 definition

 let z be Complex;

 :: COMPTRIG:def1

 func Arg z -> Real means

 : Def1: z = (( |.z.| * ( cos it )) + (( |.z.| * ( sin it )) * )) & 0 <= it & it < (2 * PI ) if z <> 0

 otherwise it = 0 ;

 existence

 proof

 thus z <> 0 implies ex r be Real st z = (( |.z.| * ( cos r)) + (( |.z.| * ( sin r)) * )) & 0 <= r & r < (2 * PI )

 proof

 |.z.| >= 0 by COMPLEX1: 46;

 then

 A1: (( Re z) / |.z.|) <= 1 by COMPLEX1: 54, XREAL_1: 185;

 assume

 A2: z <> 0 ;

 then

 A3: |.z.| <> 0 by COMPLEX1: 45;

 now

 per cases ;

 suppose

 A4: ( Im z) >= 0 ;

 set 0PI = [. 0 , PI .];

 reconsider cos1 = ( cos | 0PI) as PartFunc of 0PI, REAL by PARTFUN1: 10;

 reconsider cos1 as one-to-one PartFunc of 0PI, REAL by Th25, RFUNCT_2: 50;

 reconsider r = ((cos1 " ) . (( Re z) / |.z.|)) as Real;



 A5: ( |.z.| ^2 ) = ((( Re z) ^2 ) + (( Im z) ^2 )) by Th3;

 take r;

 ( Re z) >= ( - |.z.|) by Th1;

 then ( - 1) <= (( Re z) / |.z.|) by COMPLEX1: 46, XREAL_1: 193;

 then

 A6: (( Re z) / |.z.|) in ( rng cos1) by A1, Th32, XXREAL_1: 1;

 then (( Re z) / |.z.|) in ( dom (cos1 " )) by FUNCT_1: 33;

 then r in ( rng (cos1 " )) by FUNCT_1:def 3;

 then r in ( dom cos1) by FUNCT_1: 33;

 then

 A7: r in [. 0 , PI .] by RELAT_1: 57;

 then r <= PI by XXREAL_1: 1;

 then

 A8: r = PI or r < PI by XXREAL_0: 1;



 A9: ( cos r) = ( cos . r) by SIN_COS:def 19

 .= (cos1 . r) by A7, FUNCT_1: 49

 .= (( Re z) / |.z.|) by A6, FUNCT_1: 35;

 0 = r or 0 < r by A7, XXREAL_1: 1;

 then r = 0 or r = PI or r in ]. 0 , PI .[ by A8, XXREAL_1: 4;

 then

 A10: ( sin . r) >= 0 by Th7, SIN_COS: 30, SIN_COS: 76;

 ((( cos . r) ^2 ) + (( sin . r) ^2 )) = 1 by SIN_COS: 28;



 then (( sin . r) ^2 ) = (1 - (( cos . r) ^2 ))

 .= (1 - ((( Re z) / |.z.|) ^2 )) by A9, SIN_COS:def 19

 .= (1 - ((( Re z) ^2 ) / ( |.z.| ^2 ))) by XCMPLX_1: 76

 .= ((( |.z.| ^2 ) / ( |.z.| ^2 )) - ((( Re z) ^2 ) / ( |.z.| ^2 ))) by A3, XCMPLX_1: 60

 .= ((( |.z.| ^2 ) - (( Re z) ^2 )) / ( |.z.| ^2 ))

 .= ((( Im z) / |.z.|) ^2 ) by A5, XCMPLX_1: 76;



 then ( sin . r) = ( sqrt ((( Im z) / |.z.|) ^2 )) by A10, SQUARE_1: 22

 .= |.(( Im z) / |.z.|).| by COMPLEX1: 72

 .= ( |.( Im z).| / |. |.z.|.|) by COMPLEX1: 67

 .= ( |.( Im z).| / |.z.|);

 then |.( Im z).| = ( |.z.| * ( sin . r)) by A2, COMPLEX1: 45, XCMPLX_1: 87;



 then

 A11: ( Im z) = ( |.z.| * ( sin . r)) by A4, ABSVALUE:def 1

 .= ( |.z.| * ( sin r)) by SIN_COS:def 17;

 ( Re z) = ( |.z.| * ( cos r)) by A2, A9, COMPLEX1: 45, XCMPLX_1: 87;

 hence z = (( |.z.| * ( cos r)) + (( |.z.| * ( sin r)) * )) by A11, COMPLEX1: 13;

 thus 0 <= r by A7, XXREAL_1: 1;

 r <= PI by A7, XXREAL_1: 1;

 hence r < (2 * PI ) by Lm3, XXREAL_0: 2;

 end;

 suppose

 A12: ( Im z) < 0 ;

 per cases ;

 suppose

 A13: ( Re z) <> |.z.|;

 set 0PI = [. PI , (2 * PI ).];

 reconsider cos1 = ( cos | 0PI) as PartFunc of 0PI, REAL by PARTFUN1: 10;

 reconsider cos1 as one-to-one PartFunc of 0PI, REAL by Th26, RFUNCT_2: 50;

 reconsider r = ((cos1 " ) . (( Re z) / |.z.|)) as Real;

 ( Re z) >= ( - |.z.|) by Th1;

 then ( - 1) <= (( Re z) / |.z.|) by COMPLEX1: 46, XREAL_1: 193;

 then

 A14: (( Re z) / |.z.|) in ( rng cos1) by A1, Th33, XXREAL_1: 1;

 then

 A15: (( Re z) / |.z.|) in ( dom (cos1 " )) by FUNCT_1: 33;

 then r in ( rng (cos1 " )) by FUNCT_1:def 3;

 then r in ( dom cos1) by FUNCT_1: 33;

 then

 A16: r in [. PI , (2 * PI ).] by RELAT_1: 57;

 then r <= (2 * PI ) by XXREAL_1: 1;

 then

 A17: r = (2 * PI ) or r < (2 * PI ) by XXREAL_0: 1;



 A18: (( Re z) / |.z.|) <> 1 by A13, XCMPLX_1: 58;



 A19: r <> (2 * PI )

 proof

 (2 * PI ) in [. PI , (2 * PI ).] by Lm3, XXREAL_1: 1;

 then (2 * PI ) in ( dom cos1) & (cos1 . (2 * PI )) = 1 by FUNCT_1: 49, RELAT_1: 57, SIN_COS: 24, SIN_COS: 76;

 then

 A20: ((cos1 " ) . 1) = (2 * PI ) by FUNCT_1: 32;

 1 in ( rng cos1) by Th33, XXREAL_1: 1;

 then

 A21: 1 in ( dom (cos1 " )) by FUNCT_1: 33;

 assume r = (2 * PI );

 hence contradiction by A18, A15, A21, A20, FUNCT_1:def 4;

 end;



 A22: ( cos r) = ( cos . r) by SIN_COS:def 19

 .= (cos1 . r) by A16, FUNCT_1: 49

 .= (( Re z) / |.z.|) by A14, FUNCT_1: 35;

 PI <= r by A16, XXREAL_1: 1;

 then PI = r or PI < r by XXREAL_0: 1;

 then r = PI or r = (2 * PI ) or r in ]. PI , (2 * PI ).[ by A17, XXREAL_1: 4;

 then

 A23: ( sin . r) <= 0 by Th9, SIN_COS: 76;

 take r;



 A24: ( |.z.| ^2 ) = ((( Re z) ^2 ) + (( Im z) ^2 )) by Th3;

 ((( cos . r) ^2 ) + (( sin . r) ^2 )) = 1 by SIN_COS: 28;



 then (( sin . r) ^2 ) = (1 - (( cos . r) ^2 ))

 .= (1 - ((( Re z) / |.z.|) ^2 )) by A22, SIN_COS:def 19

 .= (1 - ((( Re z) ^2 ) / ( |.z.| ^2 ))) by XCMPLX_1: 76

 .= ((( |.z.| ^2 ) / ( |.z.| ^2 )) - ((( Re z) ^2 ) / ( |.z.| ^2 ))) by A3, XCMPLX_1: 60

 .= ((( |.z.| ^2 ) - (( Re z) ^2 )) / ( |.z.| ^2 ))

 .= ((( Im z) / |.z.|) ^2 ) by A24, XCMPLX_1: 76;



 then ( - ( sin . r)) = ( sqrt ((( Im z) / |.z.|) ^2 )) by A23, SQUARE_1: 23

 .= |.(( Im z) / |.z.|).| by COMPLEX1: 72

 .= ( |.( Im z).| / |. |.z.|.|) by COMPLEX1: 67

 .= ( |.( Im z).| / |.z.|);

 then ( sin . r) = (( - |.( Im z).|) / |.z.|);

 then ( - |.( Im z).|) = ( |.z.| * ( sin . r)) by A2, COMPLEX1: 45, XCMPLX_1: 87;



 then

 A25: ( - ( - ( Im z))) = ( |.z.| * ( sin . r)) by A12, ABSVALUE:def 1

 .= ( |.z.| * ( sin r)) by SIN_COS:def 17;

 ( Re z) = ( |.z.| * ( cos r)) by A2, A22, COMPLEX1: 45, XCMPLX_1: 87;

 hence z = (( |.z.| * ( cos r)) + (( |.z.| * ( sin r)) * )) by A25, COMPLEX1: 13;

 thus 0 <= r by A16, XXREAL_1: 1;

 r <= (2 * PI ) by A16, XXREAL_1: 1;

 hence r < (2 * PI ) by A19, XXREAL_0: 1;

 end;

 suppose

 A26: ( Re z) = |.z.|;

 reconsider r = 0 as Real;

 take r;

 (( Re z) ^2 ) = ((( Re z) ^2 ) + (( Im z) ^2 )) by A26, Th3;

 then ( Im z) = 0 ;

 hence z = (( |.z.| * ( cos r)) + (( |.z.| * ( sin r)) * )) by A26, COMPLEX1: 13, SIN_COS: 31;

 thus 0 <= r;

 thus r < (2 * PI ) by Lm1;

 end;

 end;

 end;

 hence thesis;

 end;

 thus thesis;

 end;

 uniqueness

 proof

 z <> 0 implies for x,y be Real st z = (( |.z.| * ( cos x)) + (( |.z.| * ( sin x)) * )) & 0 <= x & x < (2 * PI ) & z = (( |.z.| * ( cos y)) + (( |.z.| * ( sin y)) * )) & 0 <= y & y < (2 * PI ) holds x = y

 proof

 assume z <> 0 ;

 then

 A27: |.z.| <> 0 by COMPLEX1: 45;

 let x,y be Real;

 assume that

 A28: z = (( |.z.| * ( cos x)) + (( |.z.| * ( sin x)) * )) and

 A29: 0 <= x and

 A30: x < (2 * PI ) and

 A31: z = (( |.z.| * ( cos y)) + (( |.z.| * ( sin y)) * )) and

 A32: 0 <= y and

 A33: y < (2 * PI );

 ( |.z.| * ( cos x)) = ( |.z.| * ( cos y)) by A28, A31, COMPLEX1: 77;

 then ( cos x) = ( cos y) by A27, XCMPLX_1: 5;

 then ( cos x) = ( cos . y) by SIN_COS:def 19;

 then

 A34: ( cos . x) = ( cos . y) by SIN_COS:def 19;

 ( |.z.| * ( sin x)) = ( |.z.| * ( sin y)) by A28, A31, COMPLEX1: 77;

 then ( sin x) = ( sin y) by A27, XCMPLX_1: 5;

 then

 A35: ( sin x) = ( sin . y) by SIN_COS:def 17;

 now

 per cases ;

 suppose

 A36: x <= PI & y <= PI ;

 then y in [. 0 , PI .] by A32, XXREAL_1: 1;

 then

 A37: y in ( [. 0 , PI .] /\ ( dom cos )) by SIN_COS: 24, XBOOLE_0:def 4;

 assume x <> y;

 then

 A38: x < y or y < x by XXREAL_0: 1;

 x in [. 0 , PI .] by A29, A36, XXREAL_1: 1;

 then x in ( [. 0 , PI .] /\ ( dom cos )) by SIN_COS: 24, XBOOLE_0:def 4;

 hence contradiction by A34, A37, A38, Th25, RFUNCT_2: 21;

 end;

 suppose

 A39: x > PI & y > PI ;

 then y in [. PI , (2 * PI ).] by A33, XXREAL_1: 1;

 then

 A40: y in ( [. PI , (2 * PI ).] /\ ( dom cos )) by SIN_COS: 24, XBOOLE_0:def 4;

 assume x <> y;

 then

 A41: x < y or y < x by XXREAL_0: 1;

 x in [. PI , (2 * PI ).] by A30, A39, XXREAL_1: 1;

 then x in ( [. PI , (2 * PI ).] /\ ( dom cos )) by SIN_COS: 24, XBOOLE_0:def 4;

 hence contradiction by A34, A40, A41, Th26, RFUNCT_2: 20;

 end;

 suppose

 A42: x <= PI & y > PI ;

 then y in ]. PI , (2 * PI ).[ by A33, XXREAL_1: 4;

 then

 A43: ( sin . y) < 0 by Th9;

 x in [. 0 , PI .] by A29, A42, XXREAL_1: 1;

 then ( sin . x) >= 0 by Th8;

 hence thesis by A35, A43, SIN_COS:def 17;

 end;

 suppose

 A44: y <= PI & x > PI ;

 then x in ]. PI , (2 * PI ).[ by A30, XXREAL_1: 4;

 then

 A45: ( sin . x) < 0 by Th9;

 y in [. 0 , PI .] by A32, A44, XXREAL_1: 1;

 then ( sin . y) >= 0 by Th8;

 hence thesis by A35, A45, SIN_COS:def 17;

 end;

 end;

 hence thesis;

 end;

 hence thesis;

 end;

 consistency ;

 end

 theorem :: COMPTRIG:34



 Th34: for z be Complex holds 0 <= ( Arg z) & ( Arg z) < (2 * PI )

 proof

 let z be Complex;

 0 <= ( Arg z) & ( Arg z) < (2 * PI ) or z = 0 by Def1;

 hence thesis by Def1, Lm6, Lm7;

 end;

 theorem :: COMPTRIG:35



 Th35: for x be Real st x >= 0 holds ( Arg x) = 0

 proof

 let x be Real;



 A1: 0 <= ( Arg (x + ( 0 * ))) & ( Arg (x + ( 0 * ))) < (2 * PI ) by Th34;

 assume

 A2: x >= 0 ;

 per cases by A2;

 suppose

 A3: x > ( - 0 );

 then

 A4: (x + ( 0 * )) = (( |.(x + ( 0 * )).| * ( cos ( Arg (x + ( 0 * ))))) + (( |.(x + ( 0 * )).| * ( sin ( Arg (x + ( 0 * ))))) * )) by Def1;

 |.(x + ( 0 * )).| <> 0 by A3, COMPLEX1: 45;

 then ( sin ( Arg (x + ( 0 * )))) = 0 by A4, COMPLEX1: 77;

 then ( Arg (x + ( 0 * ))) = 0 or ( |.(x + ( 0 * )).| * ( - 1)) = x by A1, A4, Th17, SIN_COS: 77;

 then ( Arg (x + ( 0 * ))) = 0 or |.(x + ( 0 * )).| < 0 by A3;

 hence thesis by COMPLEX1: 46;

 end;

 suppose (x + ( 0 * )) = 0 ;

 hence thesis by Def1;

 end;

 end;

 theorem :: COMPTRIG:36



 Th36: for x be Real st x < 0 holds ( Arg x) = PI

 proof

 let x be Real;



 A1: 0 <= ( Arg (x + ( 0 * ))) & ( Arg (x + ( 0 * ))) < (2 * PI ) by Th34;

 assume

 A2: x < 0 ;

 then

 A3: (x + ( 0 * )) = (( |.(x + ( 0 * )).| * ( cos ( Arg (x + ( 0 * ))))) + (( |.(x + ( 0 * )).| * ( sin ( Arg (x + ( 0 * ))))) * )) by Def1;

 |.(x + ( 0 * )).| <> 0 by A2, COMPLEX1: 45;

 then ( sin ( Arg (x + ( 0 * )))) = 0 by A3, COMPLEX1: 77;

 then ( Arg (x + ( 0 * ))) = PI or ( |.(x + ( 0 * )).| * 1) = x by A1, A3, Th17, SIN_COS: 31;

 hence thesis by A2, COMPLEX1: 46;

 end;

 theorem :: COMPTRIG:37



 Th37: for x be Real st x > 0 holds ( Arg (x * )) = ( PI / 2)

 proof

 let x be Real;



 A1: 0 <= ( Arg ( 0 + (x * ))) & ( Arg ( 0 + (x * ))) < (2 * PI ) by Th34;

 assume

 A2: x > 0 ;

 then

 A3: ( 0 + (x * )) <> 0 ;

 then

 A4: ( 0 + (x * )) = (( |.( 0 + (x * )).| * ( cos ( Arg ( 0 + (x * ))))) + (( |.( 0 + (x * )).| * ( sin ( Arg ( 0 + (x * ))))) * )) by Def1;

 |.( 0 + (x * )).| <> 0 by A3, COMPLEX1: 45;

 then ( cos ( Arg ( 0 + (x * )))) = 0 by A4, COMPLEX1: 77;

 then ( Arg ( 0 + (x * ))) = ( PI / 2) or ( |.( 0 + (x * )).| * ( - 1)) = x by A1, A4, Th18, SIN_COS: 77;

 then ( Arg ( 0 + (x * ))) = ( PI / 2) or |.( 0 + (x * )).| < 0 by A2;

 hence thesis by COMPLEX1: 46;

 end;

 theorem :: COMPTRIG:38



 Th38: for x be Real st x < 0 holds ( Arg (x * )) = ((3 / 2) * PI )

 proof

 let x be Real;



 A1: 0 <= ( Arg ( 0 + (x * ))) & ( Arg ( 0 + (x * ))) < (2 * PI ) by Th34;

 assume

 A2: x < 0 ;

 then

 A3: ( 0 + (x * )) <> 0 ;

 then

 A4: ( 0 + (x * )) = (( |.( 0 + (x * )).| * ( cos ( Arg ( 0 + (x * ))))) + (( |.( 0 + (x * )).| * ( sin ( Arg ( 0 + (x * ))))) * )) by Def1;

 |.( 0 + (x * )).| <> 0 by A3, COMPLEX1: 45;

 then ( cos ( Arg ( 0 + (x * )))) = 0 by A4, COMPLEX1: 77;

 then ( Arg ( 0 + (x * ))) = ((3 / 2) * PI ) or ( |.( 0 + (x * )).| * 1) = x by A1, A4, Th18, SIN_COS: 77;

 hence thesis by A2, COMPLEX1: 46;

 end;

 theorem :: COMPTRIG:39

 ( Arg 1) = 0 by Th35;

 theorem :: COMPTRIG:40

 ( Arg ) = ( PI / 2)

 proof

 = ( 0 + (1 * ));

 hence thesis by Th37;

 end;

 theorem :: COMPTRIG:41



 Th41: for z be Complex holds ( Arg z) in ]. 0 , ( PI / 2).[ iff ( Re z) > 0 & ( Im z) > 0

 proof

 let z be Complex;



 A1: ( Arg z) < (2 * PI ) by Th34;

 thus ( Arg z) in ]. 0 , ( PI / 2).[ implies ( Re z) > 0 & ( Im z) > 0

 proof

 assume

 A2: ( Arg z) in ]. 0 , ( PI / 2).[;

 then

 A3: ( Arg z) > 0 by XXREAL_1: 4;

 then z <> 0 by Def1;

 then

 A4: z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) & |.z.| > 0 by Def1, COMPLEX1: 47;

 ( cos ( Arg z)) > 0 by A2, SIN_COS: 81;

 hence ( Re z) > 0 by A4, COMPLEX1: 12;

 ( Arg z) < ( PI / 2) by A2, XXREAL_1: 4;

 then ( Arg z) < PI by Lm2, XXREAL_0: 2;

 then ( Arg z) in ]. 0 , PI .[ by A3, XXREAL_1: 4;

 then ( sin . ( Arg z)) > 0 by Th7;

 then ( sin ( Arg z)) > 0 by SIN_COS:def 17;

 hence thesis by A4, COMPLEX1: 12;

 end;

 assume that

 A5: ( Re z) > 0 and

 A6: ( Im z) > 0 ;

 z = (( Re z) + (( Im z) * )) by COMPLEX1: 13;

 then z <> ( 0 + ( 0 * )) by A5, COMPLEX1: 77;

 then

 A7: |.z.| > 0 & z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) by Def1, COMPLEX1: 47;

 then ( sin ( Arg z)) > 0 by A6, COMPLEX1: 12;

 then

 A8: ( sin . ( Arg z)) > 0 by SIN_COS:def 17;

 ( cos ( Arg z)) > 0 by A5, A7, COMPLEX1: 12;

 then ( cos . ( Arg z)) > 0 by SIN_COS:def 19;

 then

 A9: not ( Arg z) in [.( PI / 2), ((3 / 2) * PI ).] by Th14;

 0 <= ( Arg z) by Th34;

 then

 A10: ( Arg z) > 0 by A8, SIN_COS: 30;

 not ( Arg z) in [. PI , (2 * PI ).] by A8, Th10;

 then ( PI / 2) > ( Arg z) or PI > ( Arg z) & ((3 / 2) * PI ) < ( Arg z) by A1, A9, XXREAL_1: 1;

 hence thesis by A10, Lm5, XXREAL_0: 2, XXREAL_1: 4;

 end;

 theorem :: COMPTRIG:42



 Th42: for z be Complex holds ( Arg z) in ].( PI / 2), PI .[ iff ( Re z) < 0 & ( Im z) > 0

 proof

 let z be Complex;

 thus ( Arg z) in ].( PI / 2), PI .[ implies ( Re z) < 0 & ( Im z) > 0

 proof

 assume

 A1: ( Arg z) in ].( PI / 2), PI .[;

 then ( Arg z) < PI by XXREAL_1: 4;

 then

 A2: ( Arg z) < ((3 / 2) * PI ) by Lm5, XXREAL_0: 2;



 A3: ( Arg z) > ( PI / 2) by A1, XXREAL_1: 4;

 then z <> 0 by Def1;

 then

 A4: z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) & |.z.| > 0 by Def1, COMPLEX1: 47;

 ( PI / 2) < ( Arg z) by A1, XXREAL_1: 4;

 then ( Arg z) in ].( PI / 2), ((3 / 2) * PI ).[ by A2, XXREAL_1: 4;

 then ( cos . ( Arg z)) < 0 by Th13;

 then ( cos ( Arg z)) < 0 by SIN_COS:def 19;

 hence ( Re z) < 0 by A4, COMPLEX1: 12;

 ( Arg z) < PI by A1, XXREAL_1: 4;

 then ( Arg z) in ]. 0 , PI .[ by A3, XXREAL_1: 4;

 then ( sin . ( Arg z)) > 0 by Th7;

 then ( sin ( Arg z)) > 0 by SIN_COS:def 17;

 hence thesis by A4, COMPLEX1: 12;

 end;

 assume that

 A5: ( Re z) < 0 and

 A6: ( Im z) > 0 ;

 z = (( Re z) + (( Im z) * )) by COMPLEX1: 13;

 then z <> ( 0 + ( 0 * )) by A5, COMPLEX1: 77;

 then

 A7: |.z.| > 0 & z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) by Def1, COMPLEX1: 47;

 then ( sin ( Arg z)) > 0 by A6, COMPLEX1: 12;

 then ( sin . ( Arg z)) > 0 by SIN_COS:def 17;

 then

 A8: not ( Arg z) in [. PI , (2 * PI ).] by Th10;

 ( cos ( Arg z)) < 0 by A5, A7, COMPLEX1: 12;

 then ( cos . ( Arg z)) < 0 by SIN_COS:def 19;

 then not ( Arg z) in [.( - ( PI / 2)), ( PI / 2).] by Th12;

 then

 A9: ( Arg z) < ( - ( PI / 2)) or ( Arg z) > ( PI / 2) by XXREAL_1: 1;

 ( Arg z) < (2 * PI ) by Th34;

 then ( Arg z) < PI by A8, XXREAL_1: 1;

 hence thesis by A9, Th34, XXREAL_1: 4;

 end;

 theorem :: COMPTRIG:43



 Th43: for z be Complex holds ( Arg z) in ]. PI , ((3 / 2) * PI ).[ iff ( Re z) < 0 & ( Im z) < 0

 proof

 let z be Complex;

 thus ( Arg z) in ]. PI , ((3 / 2) * PI ).[ implies ( Re z) < 0 & ( Im z) < 0

 proof

 assume

 A1: ( Arg z) in ]. PI , ((3 / 2) * PI ).[;

 then PI < ( Arg z) by XXREAL_1: 4;

 then

 A2: ( PI / 2) < ( Arg z) by Lm2, XXREAL_0: 2;



 A3: ( Arg z) > PI by A1, XXREAL_1: 4;

 then z <> 0 by Def1;

 then

 A4: z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) & |.z.| > 0 by Def1, COMPLEX1: 47;

 ( Arg z) < ((3 / 2) * PI ) by A1, XXREAL_1: 4;

 then ( Arg z) in ].( PI / 2), ((3 / 2) * PI ).[ by A2, XXREAL_1: 4;

 then ( cos . ( Arg z)) < 0 by Th13;

 then ( cos ( Arg z)) < 0 by SIN_COS:def 19;

 hence ( Re z) < 0 by A4, COMPLEX1: 12;

 ( Arg z) < ((3 / 2) * PI ) by A1, XXREAL_1: 4;

 then ( Arg z) < (2 * PI ) by Lm6, XXREAL_0: 2;

 then ( Arg z) in ]. PI , (2 * PI ).[ by A3, XXREAL_1: 4;

 then ( sin . ( Arg z)) < 0 by Th9;

 then ( sin ( Arg z)) < 0 by SIN_COS:def 17;

 hence thesis by A4, COMPLEX1: 12;

 end;

 assume that

 A5: ( Re z) < 0 and

 A6: ( Im z) < 0 ;

 z = (( Re z) + (( Im z) * )) by COMPLEX1: 13;

 then z <> ( 0 + ( 0 * )) by A5, COMPLEX1: 77;

 then

 A7: |.z.| > 0 & z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) by Def1, COMPLEX1: 47;

 then ( cos ( Arg z)) < 0 by A5, COMPLEX1: 12;

 then ( cos . ( Arg z)) < 0 by SIN_COS:def 19;

 then

 A8: not ( Arg z) in [.((3 / 2) * PI ), (2 * PI ).] by Th16;

 ( sin ( Arg z)) < 0 by A6, A7, COMPLEX1: 12;

 then ( sin . ( Arg z)) < 0 by SIN_COS:def 17;

 then

 A9: not ( Arg z) in [. 0 , PI .] by Th8;

 ( Arg z) < (2 * PI ) by Th34;

 then

 A10: ( Arg z) < ((3 / 2) * PI ) by A8, XXREAL_1: 1;

 0 <= ( Arg z) by Th34;

 then ( Arg z) > PI by A9, XXREAL_1: 1;

 hence thesis by A10, XXREAL_1: 4;

 end;

 theorem :: COMPTRIG:44



 Th44: for z be Complex holds ( Arg z) in ].((3 / 2) * PI ), (2 * PI ).[ iff ( Re z) > 0 & ( Im z) < 0

 proof

 let z be Complex;

 thus ( Arg z) in ].((3 / 2) * PI ), (2 * PI ).[ implies ( Re z) > 0 & ( Im z) < 0

 proof

 assume

 A1: ( Arg z) in ].((3 / 2) * PI ), (2 * PI ).[;

 then

 A2: ( Arg z) < (2 * PI ) by XXREAL_1: 4;



 A3: ( Arg z) > ((3 / 2) * PI ) by A1, XXREAL_1: 4;

 then z <> 0 by Def1;

 then

 A4: z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) & |.z.| > 0 by Def1, COMPLEX1: 47;

 ( cos . ( Arg z)) > 0 by A1, Th15;

 then ( cos ( Arg z)) > 0 by SIN_COS:def 19;

 hence ( Re z) > 0 by A4, COMPLEX1: 12;

 ( Arg z) > PI by A3, Lm5, XXREAL_0: 2;

 then ( Arg z) in ]. PI , (2 * PI ).[ by A2, XXREAL_1: 4;

 then ( sin . ( Arg z)) < 0 by Th9;

 then ( sin ( Arg z)) < 0 by SIN_COS:def 17;

 hence thesis by A4, COMPLEX1: 12;

 end;

 assume that

 A5: ( Re z) > 0 and

 A6: ( Im z) < 0 ;

 z = (( Re z) + (( Im z) * )) by COMPLEX1: 13;

 then z <> ( 0 + ( 0 * )) by A5, COMPLEX1: 77;

 then

 A7: |.z.| > 0 & z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) by Def1, COMPLEX1: 47;

 then ( sin ( Arg z)) < 0 by A6, COMPLEX1: 12;

 then ( sin . ( Arg z)) < 0 by SIN_COS:def 17;

 then

 A8: not ( Arg z) in [. 0 , PI .] by Th8;

 ( cos ( Arg z)) > 0 by A5, A7, COMPLEX1: 12;

 then ( cos . ( Arg z)) > 0 by SIN_COS:def 19;

 then not ( Arg z) in [.( PI / 2), ((3 / 2) * PI ).] by Th14;

 then

 A9: ( Arg z) < ( PI / 2) or ( Arg z) > ((3 / 2) * PI ) by XXREAL_1: 1;

 0 <= ( Arg z) by Th34;

 then

 A10: ( Arg z) > PI by A8, XXREAL_1: 1;

 ( Arg z) < (2 * PI ) by Th34;

 hence thesis by A10, A9, Lm2, XXREAL_0: 2, XXREAL_1: 4;

 end;

 theorem :: COMPTRIG:45



 Th45: for z be Complex st ( Im z) > 0 holds ( sin ( Arg z)) > 0

 proof

 let z be Complex;

 ( Re z) < 0 or ( Re z) = 0 or ( Re z) > 0 ;

 then

 A1: ( Re z) < 0 or ( Re z) > 0 or z = ( 0 + (( Im z) * )) by COMPLEX1: 13;

 assume ( Im z) > 0 ;

 then ( Arg z) in ].( PI / 2), PI .[ or ( Arg z) in ]. 0 , ( PI / 2).[ or ( Arg z) = ( PI / 2) by A1, Th37, Th41, Th42;

 then

 A2: ( PI / 2) < ( Arg z) & ( Arg z) < PI or 0 < ( Arg z) & ( Arg z) < ( PI / 2) or ( Arg z) = ( PI / 2) by XXREAL_1: 4;

 then ( Arg z) < PI by Lm2, XXREAL_0: 2;

 then ( Arg z) in ]. 0 , PI .[ by A2, XXREAL_1: 4;

 then ( sin . ( Arg z)) > 0 by Th7;

 hence thesis by SIN_COS:def 17;

 end;

 theorem :: COMPTRIG:46



 Th46: for z be Complex st ( Im z) < 0 holds ( sin ( Arg z)) < 0

 proof

 let z be Complex;

 ( Re z) < 0 or ( Re z) = 0 or ( Re z) > 0 ;

 then

 A1: ( Re z) < 0 or ( Re z) > 0 or z = ( 0 + (( Im z) * )) by COMPLEX1: 13;

 assume ( Im z) < 0 ;

 then ( Arg z) in ]. PI , ((3 / 2) * PI ).[ or ( Arg z) in ].((3 / 2) * PI ), (2 * PI ).[ or ( Arg z) = ((3 / 2) * PI ) by A1, Th38, Th43, Th44;

 then PI < ( Arg z) & ( Arg z) < ((3 / 2) * PI ) or ((3 / 2) * PI ) < ( Arg z) & ( Arg z) < (2 * PI ) or ( Arg z) = ((3 / 2) * PI ) by XXREAL_1: 4;

 then PI < ( Arg z) & ( Arg z) < (2 * PI ) by Lm5, Lm6, XXREAL_0: 2;

 then ( Arg z) in ]. PI , (2 * PI ).[ by XXREAL_1: 4;

 then ( sin . ( Arg z)) < 0 by Th9;

 hence thesis by SIN_COS:def 17;

 end;

 theorem :: COMPTRIG:47

 for z be Complex st ( Im z) >= 0 holds ( sin ( Arg z)) >= 0

 proof

 let z be Complex;

 assume ( Im z) >= 0 ;

 then ( Im z) > 0 or ( Im z) = 0 ;

 then ( sin ( Arg z)) > 0 or z = (( Re z) + ( 0 * )) & (( Re z) >= 0 or ( Re z) < 0 ) by Th45, COMPLEX1: 13;

 hence thesis by Th35, Th36, SIN_COS: 31, SIN_COS: 77;

 end;

 theorem :: COMPTRIG:48

 for z be Complex st ( Im z) <= 0 holds ( sin ( Arg z)) <= 0

 proof

 let z be Complex;

 assume ( Im z) <= 0 ;

 then ( Im z) < 0 or ( Im z) = 0 ;

 then ( sin ( Arg z)) < 0 or z = (( Re z) + ( 0 * )) & (( Re z) >= 0 or ( Re z) < 0 ) by Th46, COMPLEX1: 13;

 hence thesis by Th35, Th36, SIN_COS: 31, SIN_COS: 77;

 end;

 theorem :: COMPTRIG:49



 Th49: for z be Complex st ( Re z) > 0 holds ( cos ( Arg z)) > 0

 proof

 let z be Complex;

 ( Im z) < 0 or ( Im z) = 0 or ( Im z) > 0 ;

 then

 A1: ( Im z) < 0 or ( Im z) > 0 or z = (( Re z) + ( 0 * )) by COMPLEX1: 13;

 assume ( Re z) > 0 ;

 then ( Arg z) in ]. 0 , ( PI / 2).[ or ( Arg z) in ].((3 / 2) * PI ), (2 * PI ).[ or ( Arg z) = 0 by A1, Th35, Th41, Th44;

 then ( cos . ( Arg z)) > 0 by Th15, SIN_COS: 30, SIN_COS: 80;

 hence thesis by SIN_COS:def 19;

 end;

 theorem :: COMPTRIG:50



 Th50: for z be Complex st ( Re z) < 0 holds ( cos ( Arg z)) < 0

 proof

 let z be Complex;

 ( Im z) < 0 or ( Im z) = 0 or ( Im z) > 0 ;

 then

 A1: ( Im z) < 0 or ( Im z) > 0 or z = (( Re z) + ( 0 * )) by COMPLEX1: 13;

 assume ( Re z) < 0 ;

 then ( Arg z) in ].( PI / 2), PI .[ or ( Arg z) in ]. PI , ((3 / 2) * PI ).[ or ( Arg z) = PI by A1, Th36, Th42, Th43;

 then ( PI / 2) < ( Arg z) & ( Arg z) < PI or PI < ( Arg z) & ( Arg z) < ((3 / 2) * PI ) or ( Arg z) = PI by XXREAL_1: 4;

 then ( PI / 2) < ( Arg z) & ( Arg z) < ((3 / 2) * PI ) by Lm2, Lm5, XXREAL_0: 2;

 then ( Arg z) in ].( PI / 2), ((3 / 2) * PI ).[ by XXREAL_1: 4;

 then ( cos . ( Arg z)) < 0 by Th13;

 hence thesis by SIN_COS:def 19;

 end;

 theorem :: COMPTRIG:51

 for z be Complex st ( Re z) >= 0 holds ( cos ( Arg z)) >= 0

 proof

 let z be Complex;

 assume ( Re z) >= 0 ;

 then ( Re z) > 0 or ( Re z) = 0 ;

 then ( cos ( Arg z)) > 0 or z = ( 0 + (( Im z) * )) & (( Im z) > 0 or ( Im z) < 0 or ( Im z) = 0 ) by Th49, COMPLEX1: 13;

 hence thesis by Def1, Th37, Th38, SIN_COS: 31, SIN_COS: 77;

 end;

 theorem :: COMPTRIG:52

 for z be Complex st ( Re z) <= 0 & z <> 0 holds ( cos ( Arg z)) <= 0

 proof

 let z be Complex;

 assume that

 A1: ( Re z) <= 0 and

 A2: z <> 0 ;



 A3: 0 = ( 0 + ( 0 * ));

 ( Re z) < 0 or ( Re z) = 0 by A1;

 then ( cos ( Arg z)) < 0 or z = ( 0 + (( Im z) * )) & (( Im z) >= 0 or ( Im z) < 0 ) by Th50, COMPLEX1: 13;

 then ( cos ( Arg z)) < 0 or z = ( 0 + (( Im z) * )) & (( Im z) > 0 or ( Im z) < 0 ) by A2, A3;

 hence thesis by Th37, Th38, SIN_COS: 77;

 end;

 theorem :: COMPTRIG:53



 Th53: for x be Real, n be Nat holds ((( cos x) + (( sin x) * )) |^ n) = (( cos (n * x)) + (( sin (n * x)) * ))

 proof

 let x be Real;

 defpred P[ Nat] means ((( cos x) + (( sin x) * )) |^ $1) = (( cos ($1 * x)) + (( sin ($1 * x)) * ));

 A1:

 now

 let n be Nat;

 assume P[n];



 then ((( cos x) + (( sin x) * )) |^ (n + 1)) = ((( cos (n * x)) + (( sin (n * x)) * )) * (( cos x) + (( sin x) * ))) by NEWTON: 6

 .= ((((( cos (n * x)) * ( cos x)) - (( sin (n * x)) * ( sin x))) + ((( cos (n * x)) * ( sin x)) * )) + ((( cos x) * ( sin (n * x))) * ))

 .= ((( cos ((n * x) + x)) + ((( cos (n * x)) * ( sin x)) * )) + ((( cos x) * ( sin (n * x))) * )) by SIN_COS: 75

 .= (( cos ((n * x) + x)) + (((( cos (n * x)) * ( sin x)) + (( cos x) * ( sin (n * x)))) * ))

 .= (( cos ((n + 1) * x)) + (( sin ((n + 1) * x)) * )) by SIN_COS: 75;

 hence P[(n + 1)];

 end;



 A2: P[ 0 ] by NEWTON: 4, SIN_COS: 31;

 thus for n be Nat holds P[n] from NAT_1:sch 2( A2, A1);

 end;

 theorem :: COMPTRIG:54

 for z be Element of COMPLEX holds for n be Nat st z <> 0 or n <> 0 holds (z |^ n) = ((( |.z.| |^ n) * ( cos (n * ( Arg z)))) + ((( |.z.| |^ n) * ( sin (n * ( Arg z)))) * ))

 proof

 let z be Element of COMPLEX ;

 let n be Nat;

 assume

 A1: z <> 0 or n <> 0 ;

 per cases by A1;

 suppose z <> 0 ;



 hence (z |^ n) = ((( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * )) |^ n) by Def1

 .= ((( |.z.| + ( 0 * )) * (( cos ( Arg z)) + (( sin ( Arg z)) * ))) |^ n)

 .= ((( |.z.| + ( 0 * )) |^ n) * ((( cos ( Arg z)) + (( sin ( Arg z)) * )) |^ n)) by NEWTON: 7

 .= ((( |.z.| |^ n) + ( 0 * )) * (( cos (n * ( Arg z))) + (( sin (n * ( Arg z))) * ))) by Th53

 .= ((( |.z.| |^ n) * ( cos (n * ( Arg z)))) + ((( |.z.| |^ n) * ( sin (n * ( Arg z)))) * ));

 end;

 suppose

 A2: z = 0 & n > 0 ;

 then

 A3: n >= (1 + 0 ) by NAT_1: 13;



 hence (z |^ n) = (( 0 * ( cos (n * ( Arg z)))) + (( 0 * ( sin (n * ( Arg z)))) * )) by A2, NEWTON: 11

 .= (( 0 * ( cos (n * ( Arg z)))) + ((( |.z.| |^ n) * ( sin (n * ( Arg z)))) * )) by A2, A3, COMPLEX1: 44, NEWTON: 11

 .= ((( |.z.| |^ n) * ( cos (n * ( Arg z)))) + ((( |.z.| |^ n) * ( sin (n * ( Arg z)))) * )) by A2, A3, COMPLEX1: 44, NEWTON: 11;

 end;

 end;

 theorem :: COMPTRIG:55



 Th55: for x be Real, n,k be Nat st n <> 0 holds ((( cos ((x + ((2 * PI ) * k)) / n)) + (( sin ((x + ((2 * PI ) * k)) / n)) * )) |^ n) = (( cos x) + (( sin x) * ))

 proof

 let x be Real;

 let n,k be Nat;

 assume

 A1: n <> 0 ;



 thus ((( cos ((x + ((2 * PI ) * k)) / n)) + (( sin ((x + ((2 * PI ) * k)) / n)) * )) |^ n) = (( cos (n * ((x + ((2 * PI ) * k)) / n))) + (( sin (n * ((x + ((2 * PI ) * k)) / n))) * )) by Th53

 .= (( cos (x + ((2 * PI ) * k))) + (( sin (n * ((x + ((2 * PI ) * k)) / n))) * )) by A1, XCMPLX_1: 87

 .= (( cos (x + ((2 * PI ) * k))) + (( sin (x + ((2 * PI ) * k))) * )) by A1, XCMPLX_1: 87

 .= (( cos . (x + ((2 * PI ) * k))) + (( sin (x + ((2 * PI ) * k))) * )) by SIN_COS:def 19

 .= (( cos . (x + ((2 * PI ) * k))) + (( sin . (x + ((2 * PI ) * k))) * )) by SIN_COS:def 17

 .= (( cos . (x + ((2 * PI ) * k))) + (( sin . x) * )) by SIN_COS2: 10

 .= (( cos . x) + (( sin . x) * )) by SIN_COS2: 11

 .= (( cos . x) + (( sin x) * )) by SIN_COS:def 17

 .= (( cos x) + (( sin x) * )) by SIN_COS:def 19;

 end;

 theorem :: COMPTRIG:56



 Th56: for z be Complex holds for n,k be Nat st n <> 0 holds z = ((((n -root |.z.|) * ( cos ((( Arg z) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * ( sin ((( Arg z) + ((2 * PI ) * k)) / n))) * )) |^ n)

 proof

 let z be Complex;

 let n,k be Nat;

 assume

 A1: n <> 0 ;

 then

 A2: n >= ( 0 + 1) by NAT_1: 13;

 per cases ;

 suppose

 A3: z <> 0 ;



 thus ((((n -root |.z.|) * ( cos ((( Arg z) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * ( sin ((( Arg z) + ((2 * PI ) * k)) / n))) * )) |^ n) = ((((n -root |.z.|) + ( 0 * )) * (( cos ((( Arg z) + ((2 * PI ) * k)) / n)) + (( sin ((( Arg z) + ((2 * PI ) * k)) / n)) * ))) |^ n)

 .= ((((n -root |.z.|) + ( 0 * )) |^ n) * ((( cos ((( Arg z) + ((2 * PI ) * k)) / n)) + (( sin ((( Arg z) + ((2 * PI ) * k)) / n)) * )) |^ n)) by NEWTON: 7

 .= ((((n -root |.z.|) + ( 0 * )) |^ n) * (( cos ( Arg z)) + (( sin ( Arg z)) * ))) by A1, Th55

 .= (( |.z.| + ( 0 * )) * (( cos ( Arg z)) + (( sin ( Arg z)) * ))) by A1, Th4, COMPLEX1: 46

 .= ((( |.z.| * ( cos ( Arg z))) - ( 0 * ( sin ( Arg z)))) + ((( |.z.| * ( sin ( Arg z))) + ( 0 * ( cos ( Arg z)))) * ))

 .= z by A3, Def1;

 end;

 suppose

 A4: z = 0 ;



 hence ((((n -root |.z.|) * ( cos ((( Arg z) + ((2 * PI ) * k)) / n))) + (((n -root |.z.|) * ( sin ((( Arg z) + ((2 * PI ) * k)) / n))) * )) |^ n) = ((( 0 * ( cos ((( Arg z) + ((2 * PI ) * k)) / n))) + (((n -root 0 ) * ( sin ((( Arg z) + ((2 * PI ) * k)) / n))) * )) |^ n) by A2, COMPLEX1: 44, POWER: 5

 .= (( 0 + (( 0 * ( sin ((( Arg z) + ((2 * PI ) * k)) / n))) * )) |^ n) by A2, POWER: 5

 .= z by A2, A4, NEWTON: 11;

 end;

 end;

 definition

 let x be Complex;

 let n be non zero Nat;

 :: COMPTRIG:def2

 mode CRoot of n,x -> Complex means

 : Def2: (it |^ n) = x;

 existence

 proof

 reconsider z = (((n -root |.x.|) * ( cos ((( Arg x) + ((2 * PI ) * 0 )) / n))) + (((n -root |.x.|) * ( sin ((( Arg x) + ((2 * PI ) * 0 )) / n))) * )) as Element of COMPLEX by XCMPLX_0:def 2;

 take z;

 thus thesis by Th56;

 end;

 end

 theorem :: COMPTRIG:57

 for x be Element of COMPLEX holds for n be non zero Nat holds for k be Nat holds (((n -root |.x.|) * ( cos ((( Arg x) + ((2 * PI ) * k)) / n))) + (((n -root |.x.|) * ( sin ((( Arg x) + ((2 * PI ) * k)) / n))) * )) is CRoot of n, x

 proof

 let x be Element of COMPLEX ;

 let n be non zero Nat;

 let k be Nat;

 reconsider z = (((n -root |.x.|) * ( cos ((( Arg x) + ((2 * PI ) * k)) / n))) + (((n -root |.x.|) * ( sin ((( Arg x) + ((2 * PI ) * k)) / n))) * )) as Element of COMPLEX by XCMPLX_0:def 2;

 (z |^ n) = x by Th56;

 hence thesis by Def2;

 end;

 theorem :: COMPTRIG:58

 for x be Element of COMPLEX holds for v be CRoot of 1, x holds v = x

 proof

 let x be Element of COMPLEX ;

 let v be CRoot of 1, x;

 (v |^ 1) = x by Def2;

 hence thesis;

 end;

 theorem :: COMPTRIG:59

 for n be non zero Nat holds for v be CRoot of n, 0 holds v = 0

 proof

 let n be non zero Nat;

 let v be CRoot of n, 0 ;

 defpred P[ Nat] means (v |^ $1) = 0 ;

 assume

 A1: v <> 0 ;

 A2:

 now

 let k be non zero Nat;

 assume that

 A3: k <> 1 and

 A4: P[k];

 consider t be Nat such that

 A5: k = (t + 1) by NAT_1: 6;

 reconsider t as non zero Nat by A3, A5;

 take t;

 thus t < k by A5, NAT_1: 13;

 (v |^ k) = ((v |^ t) * v) by A5, NEWTON: 6;

 hence P[t] by A1, A4;

 end;



 A6: ex n be non zero Nat st P[n]

 proof

 take n;

 thus thesis by Def2;

 end;

 P[1] from Regrwithout0( A6, A2);

 hence thesis by A1;

 end;

 theorem :: COMPTRIG:60

 for n be non zero Nat holds for x be Element of COMPLEX holds for v be CRoot of n, x st v = 0 holds x = 0

 proof

 let n be non zero Nat;

 let x be Element of COMPLEX ;

 let v be CRoot of n, x;

 assume v = 0 ;

 then n >= ( 0 + 1) & ( 0 |^ n) = x by Def2, NAT_1: 13;

 hence thesis by NEWTON: 11;

 end;

 theorem :: COMPTRIG:61

 for a be Real st 0 <= a & a < (2 * PI ) & ( cos a) = 1 holds a = 0

 proof

 let a be Real such that

 A1: 0 <= a & a < (2 * PI ) and

 A2: ( cos a) = 1;

 ((1 * 1) + (( sin a) * ( sin a))) = 1 by A2, SIN_COS: 29;

 then ( sin a) = 0 ;

 hence thesis by A1, A2, Th17, SIN_COS: 77;

 end;

 theorem :: COMPTRIG:62

 for z be Complex holds z = (( |.z.| * ( cos ( Arg z))) + (( |.z.| * ( sin ( Arg z))) * ))

 proof

 let z be Complex;

 per cases ;

 suppose z = 0 ;

 hence thesis by COMPLEX1: 44;

 end;

 suppose z <> 0 ;

 hence thesis by Def1;

 end;

 end;