:: COMPTRIG semantic presentation begin scheme :: COMPTRIG:sch 1 Regrwithout0{ P1[ Nat] } : P1[1] provided A1: ex k being non empty Nat st P1[k] and A2: for k being non empty Nat st k <> 1 & P1[k] holds ex n being non empty Nat st ( n < k & P1[n] ) proof consider t being non empty Nat such that A3: P1[t] by A1; defpred S1[ Nat] means P1[$1 + 1]; A4: now__::_thesis:_for_k_being_Nat_st_k_<>_0_&_S1[k]_holds_ ex_l_being_Nat_st_ (_l_<_k_&_S1[l]_) let k be Nat; ::_thesis: ( k <> 0 & S1[k] implies ex l being Nat st ( l < k & S1[l] ) ) assume that A5: k <> 0 and A6: S1[k] ; ::_thesis: ex l being Nat st ( l < k & S1[l] ) reconsider k1 = k + 1 as non empty Element of NAT ; k + 1 > 0 + 1 by A5, XREAL_1:6; then consider n being non empty Nat such that A7: n < k1 and A8: P1[n] by A2, A6; consider l being Nat such that A9: n = l + 1 by NAT_1:6; take l = l; ::_thesis: ( l < k & S1[l] ) thus l < k by A7, A9, XREAL_1:6; ::_thesis: S1[l] thus S1[l] by A8, A9; ::_thesis: verum end; ex s being Nat st t = s + 1 by NAT_1:6; then A10: ex k being Nat st S1[k] by A3; S1[ 0 ] from NAT_1:sch_7(A10, A4); hence P1[1] ; ::_thesis: verum end; theorem Th1: :: COMPTRIG:1 for z being complex number holds Re z >= - |.z.| proof let z be complex number ; ::_thesis: Re z >= - |.z.| 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 >= - (abs (Re z)) & - (abs (Re z)) >= - |.z.| ) by ABSVALUE:4, COMPLEX1:72; hence Re z >= - |.z.| by XXREAL_0:2; ::_thesis: verum end; theorem :: COMPTRIG:2 for z being complex number holds Im z >= - |.z.| proof let z be complex number ; ::_thesis: Im z >= - |.z.| 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 >= - (abs (Im z)) & - (abs (Im z)) >= - |.z.| ) by ABSVALUE:4, COMPLEX1:72; hence Im z >= - |.z.| by XXREAL_0:2; ::_thesis: verum end; theorem Th3: :: COMPTRIG:3 for z being complex number holds |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2) proof let z be complex number ; ::_thesis: |.z.| ^2 = ((Re z) ^2) + ((Im z) ^2) thus |.z.| ^2 = |.(z * z).| by COMPLEX1:65 .= ((Re z) ^2) + ((Im z) ^2) by COMPLEX1:68 ; ::_thesis: verum end; theorem Th4: :: COMPTRIG:4 for x being real number for n being Nat st x >= 0 & n <> 0 holds (n -root x) |^ n = x proof let x be real number ; ::_thesis: for n being Nat st x >= 0 & n <> 0 holds (n -root x) |^ n = x let n be Nat; ::_thesis: ( x >= 0 & n <> 0 implies (n -root x) |^ n = x ) assume that A1: x >= 0 and A2: n <> 0 ; ::_thesis: (n -root x) |^ n = x n >= 0 + 1 by A2, NAT_1:13; hence (n -root x) |^ n = x by A1, POWER:4; ::_thesis: verum end; registration cluster PI -> non negative ; coherence not PI is negative proof PI in ].0,4.[ by SIN_COS:def_28; hence not PI is negative by XXREAL_1:4; ::_thesis: verum 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 Th6: :: COMPTRIG:6 for a, b, c, x being real number holds ( not x in ].a,c.[ or x in ].a,b.[ or x = b or x in ].b,c.[ ) proof let a, b, c, x be real number ; ::_thesis: ( not x in ].a,c.[ or x in ].a,b.[ or x = b or x in ].b,c.[ ) assume that A1: x in ].a,c.[ and A2: not x in ].a,b.[ and A3: not x = b ; ::_thesis: x in ].b,c.[ ( 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 x in ].b,c.[ by A4, XXREAL_1:4; ::_thesis: verum end; theorem Th7: :: COMPTRIG:7 for x being real number st x in ].0,PI.[ holds sin . x > 0 proof let x be real number ; ::_thesis: ( x in ].0,PI.[ implies sin . x > 0 ) assume A1: x in ].0,PI.[ ; ::_thesis: sin . x > 0 percases ( x in ].0,(PI / 2).[ or x = PI / 2 or x in ].(PI / 2),PI.[ ) by A1, Th6; supposeA2: x in ].0,(PI / 2).[ ; ::_thesis: sin . x > 0 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 sin . x > 0 by SIN_COS:78; ::_thesis: verum end; suppose x = PI / 2 ; ::_thesis: sin . x > 0 hence sin . x > 0 by SIN_COS:76; ::_thesis: verum end; supposeA4: x in ].(PI / 2),PI.[ ; ::_thesis: sin . x > 0 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 sin . x > 0 by SIN_COS:78; ::_thesis: verum end; end; end; theorem Th8: :: COMPTRIG:8 for x being real number st x in [.0,PI.] holds sin . x >= 0 proof let x be real number ; ::_thesis: ( x in [.0,PI.] implies sin . x >= 0 ) assume A1: x in [.0,PI.] ; ::_thesis: sin . x >= 0 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 sin . x >= 0 by Th7, SIN_COS:30, SIN_COS:76; ::_thesis: verum end; theorem Th9: :: COMPTRIG:9 for x being real number st x in ].PI,(2 * PI).[ holds sin . x < 0 proof let x be real number ; ::_thesis: ( x in ].PI,(2 * PI).[ implies sin . x < 0 ) 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).[ ; ::_thesis: sin . x < 0 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 sin . x < 0 by A1, Th7; ::_thesis: verum end; theorem Th10: :: COMPTRIG:10 for x being real number st x in [.PI,(2 * PI).] holds sin . x <= 0 proof let x be real number ; ::_thesis: ( x in [.PI,(2 * PI).] implies sin . x <= 0 ) assume x in [.PI,(2 * PI).] ; ::_thesis: sin . x <= 0 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 sin . x <= 0 by Th9, SIN_COS:76; ::_thesis: verum end; theorem Th11: :: COMPTRIG:11 for x being real number st x in ].(- (PI / 2)),(PI / 2).[ holds cos . x > 0 proof let x be real number ; ::_thesis: ( x in ].(- (PI / 2)),(PI / 2).[ implies cos . x > 0 ) A1: sin . (x + (PI / 2)) = cos . x by SIN_COS:78; assume A2: x in ].(- (PI / 2)),(PI / 2).[ ; ::_thesis: cos . x > 0 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 cos . x > 0 by A1, Th7; ::_thesis: verum end; theorem Th12: :: COMPTRIG:12 for x being real number st x in [.(- (PI / 2)),(PI / 2).] holds cos . x >= 0 proof let x be real number ; ::_thesis: ( x in [.(- (PI / 2)),(PI / 2).] implies cos . x >= 0 ) assume x in [.(- (PI / 2)),(PI / 2).] ; ::_thesis: cos . x >= 0 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 cos . x >= 0 by Th11, SIN_COS:30, SIN_COS:76; ::_thesis: verum end; theorem Th13: :: COMPTRIG:13 for x being real number st x in ].(PI / 2),((3 / 2) * PI).[ holds cos . x < 0 proof let x be real number ; ::_thesis: ( x in ].(PI / 2),((3 / 2) * PI).[ implies cos . x < 0 ) A1: sin . (x + (PI / 2)) = cos . x by SIN_COS:78; assume A2: x in ].(PI / 2),((3 / 2) * PI).[ ; ::_thesis: cos . x < 0 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 cos . x < 0 by A1, Th9; ::_thesis: verum end; theorem Th14: :: COMPTRIG:14 for x being real number st x in [.(PI / 2),((3 / 2) * PI).] holds cos . x <= 0 proof let x be real number ; ::_thesis: ( x in [.(PI / 2),((3 / 2) * PI).] implies cos . x <= 0 ) assume x in [.(PI / 2),((3 / 2) * PI).] ; ::_thesis: cos . x <= 0 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 cos . x <= 0 by Th13, SIN_COS:76; ::_thesis: verum end; theorem Th15: :: COMPTRIG:15 for x being real number st x in ].((3 / 2) * PI),(2 * PI).[ holds cos . x > 0 proof let x be real number ; ::_thesis: ( x in ].((3 / 2) * PI),(2 * PI).[ implies cos . x > 0 ) 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).[ ; ::_thesis: cos . x > 0 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 cos . x > 0 by A1, Th13; ::_thesis: verum end; theorem Th16: :: COMPTRIG:16 for x being real number st x in [.((3 / 2) * PI),(2 * PI).] holds cos . x >= 0 proof let x be real number ; ::_thesis: ( x in [.((3 / 2) * PI),(2 * PI).] implies cos . x >= 0 ) assume x in [.((3 / 2) * PI),(2 * PI).] ; ::_thesis: cos . x >= 0 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 cos . x >= 0 by Th15, SIN_COS:76; ::_thesis: verum end; theorem Th17: :: COMPTRIG:17 for x being real number st 0 <= x & x < 2 * PI & sin x = 0 & not x = 0 holds x = PI proof let x be real number ; ::_thesis: ( 0 <= x & x < 2 * PI & sin x = 0 & not x = 0 implies x = PI ) assume that A1: ( 0 <= x & x < 2 * PI ) and A2: sin x = 0 ; ::_thesis: ( x = 0 or x = PI ) 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 ( x = 0 or x = PI ) by XXREAL_0:1; ::_thesis: verum end; theorem Th18: :: COMPTRIG:18 for x being real number st 0 <= x & x < 2 * PI & cos x = 0 & not x = PI / 2 holds x = (3 / 2) * PI proof let x be real number ; ::_thesis: ( 0 <= x & x < 2 * PI & cos x = 0 & not x = PI / 2 implies x = (3 / 2) * PI ) assume that A1: 0 <= x and A2: x < 2 * PI and A3: cos x = 0 ; ::_thesis: ( x = PI / 2 or x = (3 / 2) * PI ) 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 ( x = PI / 2 or x = (3 / 2) * PI ) by A4, Th15; ::_thesis: verum end; theorem Th19: :: COMPTRIG:19 sin | ].(- (PI / 2)),(PI / 2).[ is increasing proof A1: for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds diff (sin,x) > 0 proof let x be Real; ::_thesis: ( x in ].(- (PI / 2)),(PI / 2).[ implies diff (sin,x) > 0 ) assume x in ].(- (PI / 2)),(PI / 2).[ ; ::_thesis: diff (sin,x) > 0 then 0 < cos . x by Th11; hence diff (sin,x) > 0 by SIN_COS:68; ::_thesis: verum end; ].(- (PI / 2)),(PI / 2).[ is open by RCOMP_1:7; hence sin | ].(- (PI / 2)),(PI / 2).[ is increasing by A1, FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:68; ::_thesis: verum end; theorem Th20: :: COMPTRIG:20 sin | ].(PI / 2),((3 / 2) * PI).[ is decreasing proof A1: for x being Real st x in ].(PI / 2),((3 / 2) * PI).[ holds diff (sin,x) < 0 proof let x be Real; ::_thesis: ( x in ].(PI / 2),((3 / 2) * PI).[ implies diff (sin,x) < 0 ) assume x in ].(PI / 2),((3 / 2) * PI).[ ; ::_thesis: diff (sin,x) < 0 then 0 > cos . x by Th13; hence diff (sin,x) < 0 by SIN_COS:68; ::_thesis: verum end; ].(PI / 2),((3 / 2) * PI).[ is open by RCOMP_1:7; hence sin | ].(PI / 2),((3 / 2) * PI).[ is decreasing by A1, FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:68; ::_thesis: verum end; theorem Th21: :: COMPTRIG:21 cos | ].0,PI.[ is decreasing proof A1: for x being Real st x in ].0,PI.[ holds diff (cos,x) < 0 proof let x be Real; ::_thesis: ( x in ].0,PI.[ implies diff (cos,x) < 0 ) assume x in ].0,PI.[ ; ::_thesis: diff (cos,x) < 0 then 0 < sin . x by Th7; then 0 - (sin . x) < 0 ; hence diff (cos,x) < 0 by SIN_COS:67; ::_thesis: verum end; ].0,PI.[ is open by RCOMP_1:7; hence cos | ].0,PI.[ is decreasing by A1, FDIFF_1:26, ROLLE:10, SIN_COS:24, SIN_COS:67; ::_thesis: verum end; theorem Th22: :: COMPTRIG:22 cos | ].PI,(2 * PI).[ is increasing proof A1: for x being Real st x in ].PI,(2 * PI).[ holds diff (cos,x) > 0 proof let x be Real; ::_thesis: ( x in ].PI,(2 * PI).[ implies diff (cos,x) > 0 ) assume x in ].PI,(2 * PI).[ ; ::_thesis: diff (cos,x) > 0 then 0 - (sin . x) > 0 by Th9, XREAL_1:50; hence diff (cos,x) > 0 by SIN_COS:67; ::_thesis: verum end; ].PI,(2 * PI).[ is open by RCOMP_1:7; hence cos | ].PI,(2 * PI).[ is increasing by A1, FDIFF_1:26, ROLLE:9, SIN_COS:24, SIN_COS:67; ::_thesis: verum end; theorem :: COMPTRIG:23 sin | [.(- (PI / 2)),(PI / 2).] is increasing proof now__::_thesis:_for_r1,_r2_being_Real_st_r1_in_[.(-_(PI_/_2)),(PI_/_2).]_/\_(dom_sin)_&_r2_in_[.(-_(PI_/_2)),(PI_/_2).]_/\_(dom_sin)_&_r1_<_r2_holds_ sin_._r2_>_sin_._r1 let r1, r2 be Real; ::_thesis: ( r1 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r2 in [.(- (PI / 2)),(PI / 2).] /\ (dom sin) & r1 < r2 implies sin . r2 > sin . r1 ) 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 ; ::_thesis: sin . r2 > sin . r1 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; abs (sin ((r1 + r2) / 2)) <= 1 by SIN_COS:27; then A6: abs (sin . ((r1 + r2) / 2)) <= 1 by SIN_COS:def_17; then A7: sin . ((r1 + r2) / 2) <= 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 < (r1 + r2) / 2 by A3, XREAL_1:226; then A10: - (PI / 2) < (r1 + r2) / 2 by A5, XXREAL_0:2; A11: (r1 + r2) / 2 < r2 by A3, XREAL_1:226; then (r1 + r2) / 2 < PI / 2 by A8, XXREAL_0:2; then (r1 + r2) / 2 in ].(- (PI / 2)),(PI / 2).[ by A10, XXREAL_1:4; then A12: (r1 + r2) / 2 in ].(- (PI / 2)),(PI / 2).[ /\ (dom sin) by SIN_COS:24, XBOOLE_0:def_4; abs (sin r2) <= 1 by SIN_COS:27; then abs (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 . ((r1 + r2) / 2) >= - 1 by A6, ABSVALUE:5; now__::_thesis:_sin_._r2_>_sin_._r1 percases ( - (PI / 2) < r1 or - (PI / 2) = r1 ) by A5, XXREAL_0:1; supposeA16: - (PI / 2) < r1 ; ::_thesis: sin . r2 > sin . r1 then A17: - (PI / 2) < r2 by A3, XXREAL_0:2; now__::_thesis:_sin_._r2_>_sin_._r1 percases ( r2 < PI / 2 or r2 = PI / 2 ) by A8, XXREAL_0:1; supposeA18: r2 < PI / 2 ; ::_thesis: sin . r2 > sin . r1 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; ::_thesis: verum end; supposeA20: r2 = PI / 2 ; ::_thesis: not sin . r2 <= sin . r1 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 . ((r1 + r2) / 2) > sin . r1 by A9, A12, Th19, RFUNCT_2:20; assume sin . r2 <= sin . r1 ; ::_thesis: contradiction hence contradiction by A7, A20, A21, SIN_COS:76, XXREAL_0:2; ::_thesis: verum end; end; end; hence sin . r2 > sin . r1 ; ::_thesis: verum end; supposeA22: - (PI / 2) = r1 ; ::_thesis: sin . r2 > sin . r1 now__::_thesis:_not_sin_._r2_<=_sin_._r1 percases ( r2 < PI / 2 or r2 = PI / 2 ) by A8, XXREAL_0:1; suppose r2 < PI / 2 ; ::_thesis: not sin . r2 <= sin . r1 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 . ((r1 + r2) / 2) by A11, A12, Th19, RFUNCT_2:20; assume sin . r2 <= sin . r1 ; ::_thesis: contradiction then sin . r2 <= - 1 by A22, SIN_COS:30, SIN_COS:76; hence contradiction by A15, A13, A23, XXREAL_0:1; ::_thesis: verum end; suppose r2 = PI / 2 ; ::_thesis: sin . r2 > sin . r1 hence sin . r2 > sin . r1 by A22, SIN_COS:30, SIN_COS:76; ::_thesis: verum end; end; end; hence sin . r2 > sin . r1 ; ::_thesis: verum end; end; end; hence sin . r2 > sin . r1 ; ::_thesis: verum end; hence sin | [.(- (PI / 2)),(PI / 2).] is increasing by RFUNCT_2:20; ::_thesis: verum end; theorem :: COMPTRIG:24 sin | [.(PI / 2),((3 / 2) * PI).] is decreasing proof now__::_thesis:_for_r1,_r2_being_Real_st_r1_in_[.(PI_/_2),((3_/_2)_*_PI).]_/\_(dom_sin)_&_r2_in_[.(PI_/_2),((3_/_2)_*_PI).]_/\_(dom_sin)_&_r1_<_r2_holds_ sin_._r2_<_sin_._r1 let r1, r2 be Real; ::_thesis: ( r1 in [.(PI / 2),((3 / 2) * PI).] /\ (dom sin) & r2 in [.(PI / 2),((3 / 2) * PI).] /\ (dom sin) & r1 < r2 implies sin . r2 < sin . r1 ) 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 ; ::_thesis: sin . r2 < sin . r1 A4: r1 in dom sin by A1, XBOOLE_0:def_4; abs (sin r2) <= 1 by SIN_COS:27; then abs (sin . r2) <= 1 by SIN_COS:def_17; then A5: sin . r2 <= 1 by ABSVALUE:5; abs (sin r1) <= 1 by SIN_COS:27; then abs (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; abs (sin ((r1 + r2) / 2)) <= 1 by SIN_COS:27; then A9: abs (sin . ((r1 + r2) / 2)) <= 1 by SIN_COS:def_17; then A10: sin . ((r1 + r2) / 2) <= 1 by ABSVALUE:5; A11: r2 in dom sin by A2, XBOOLE_0:def_4; A12: r1 < (r1 + r2) / 2 by A3, XREAL_1:226; then A13: PI / 2 < (r1 + r2) / 2 by A8, XXREAL_0:2; A14: (r1 + r2) / 2 < r2 by A3, XREAL_1:226; then (r1 + r2) / 2 < (3 / 2) * PI by A7, XXREAL_0:2; then (r1 + r2) / 2 in ].(PI / 2),((3 / 2) * PI).[ by A13, XXREAL_1:4; then A15: (r1 + r2) / 2 in ].(PI / 2),((3 / 2) * PI).[ /\ (dom sin) by SIN_COS:24, XBOOLE_0:def_4; A16: sin . ((r1 + r2) / 2) >= - 1 by A9, ABSVALUE:5; now__::_thesis:_sin_._r2_<_sin_._r1 percases ( PI / 2 < r1 or PI / 2 = r1 ) by A8, XXREAL_0:1; supposeA17: PI / 2 < r1 ; ::_thesis: sin . r2 < sin . r1 then A18: PI / 2 < r2 by A3, XXREAL_0:2; now__::_thesis:_sin_._r2_<_sin_._r1 percases ( r2 < (3 / 2) * PI or r2 = (3 / 2) * PI ) by A7, XXREAL_0:1; supposeA19: r2 < (3 / 2) * PI ; ::_thesis: sin . r2 < sin . r1 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; ::_thesis: verum end; supposeA21: r2 = (3 / 2) * PI ; ::_thesis: not sin . r2 >= sin . r1 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 . ((r1 + r2) / 2) < sin . r1 by A12, A15, Th20, RFUNCT_2:21; assume sin . r2 >= sin . r1 ; ::_thesis: contradiction hence contradiction by A6, A16, A21, A22, SIN_COS:76, XXREAL_0:1; ::_thesis: verum end; end; end; hence sin . r2 < sin . r1 ; ::_thesis: verum end; supposeA23: PI / 2 = r1 ; ::_thesis: sin . r2 < sin . r1 now__::_thesis:_not_sin_._r2_>=_sin_._r1 percases ( r2 < (3 / 2) * PI or r2 = (3 / 2) * PI ) by A7, XXREAL_0:1; suppose r2 < (3 / 2) * PI ; ::_thesis: not sin . r2 >= sin . r1 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 . ((r1 + r2) / 2) by A14, A15, Th20, RFUNCT_2:21; assume sin . r2 >= sin . r1 ; ::_thesis: contradiction hence contradiction by A10, A5, A23, A24, SIN_COS:76, XXREAL_0:1; ::_thesis: verum end; suppose r2 = (3 / 2) * PI ; ::_thesis: sin . r2 < sin . r1 hence sin . r2 < sin . r1 by A23, SIN_COS:76; ::_thesis: verum end; end; end; hence sin . r2 < sin . r1 ; ::_thesis: verum end; end; end; hence sin . r2 < sin . r1 ; ::_thesis: verum end; hence sin | [.(PI / 2),((3 / 2) * PI).] is decreasing by RFUNCT_2:21; ::_thesis: verum end; theorem Th25: :: COMPTRIG:25 cos | [.0,PI.] is decreasing proof now__::_thesis:_for_r1,_r2_being_Real_st_r1_in_[.0,PI.]_/\_(dom_cos)_&_r2_in_[.0,PI.]_/\_(dom_cos)_&_r1_<_r2_holds_ cos_._r2_<_cos_._r1 let r1, r2 be Real; ::_thesis: ( r1 in [.0,PI.] /\ (dom cos) & r2 in [.0,PI.] /\ (dom cos) & r1 < r2 implies cos . r2 < cos . r1 ) assume that A1: r1 in [.0,PI.] /\ (dom cos) and A2: r2 in [.0,PI.] /\ (dom cos) and A3: r1 < r2 ; ::_thesis: cos . r2 < cos . r1 A4: r1 in dom cos by A1, XBOOLE_0:def_4; abs (cos r2) <= 1 by SIN_COS:27; then abs (cos . r2) <= 1 by SIN_COS:def_19; then A5: cos . r2 <= 1 by ABSVALUE:5; abs (cos r1) <= 1 by SIN_COS:27; then abs (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 < (r1 + r2) / 2 by A3, XREAL_1:226; abs (cos ((r1 + r2) / 2)) <= 1 by SIN_COS:27; then A9: abs (cos . ((r1 + r2) / 2)) <= 1 by SIN_COS:def_19; then A10: cos . ((r1 + r2) / 2) <= 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 < (r1 + r2) / 2 by A8, XXREAL_1:1; A14: (r1 + r2) / 2 < r2 by A3, XREAL_1:226; then (r1 + r2) / 2 < PI by A7, XXREAL_0:2; then (r1 + r2) / 2 in ].0,PI.[ by A13, XXREAL_1:4; then A15: (r1 + r2) / 2 in ].0,PI.[ /\ (dom cos) by SIN_COS:24, XBOOLE_0:def_4; A16: cos . ((r1 + r2) / 2) >= - 1 by A9, ABSVALUE:5; now__::_thesis:_cos_._r2_<_cos_._r1 percases ( 0 < r1 or 0 = r1 ) by A12, XXREAL_1:1; supposeA17: 0 < r1 ; ::_thesis: cos . r2 < cos . r1 now__::_thesis:_cos_._r2_<_cos_._r1 percases ( r2 < PI or r2 = PI ) by A7, XXREAL_0:1; supposeA18: r2 < PI ; ::_thesis: cos . r2 < cos . r1 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; ::_thesis: verum end; supposeA20: r2 = PI ; ::_thesis: not cos . r2 >= cos . r1 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 . ((r1 + r2) / 2) < cos . r1 by A8, A15, Th21, RFUNCT_2:21; assume cos . r2 >= cos . r1 ; ::_thesis: contradiction hence contradiction by A6, A16, A20, A21, SIN_COS:76, XXREAL_0:1; ::_thesis: verum end; end; end; hence cos . r2 < cos . r1 ; ::_thesis: verum end; supposeA22: 0 = r1 ; ::_thesis: cos . r2 < cos . r1 now__::_thesis:_not_cos_._r2_>=_cos_._r1 percases ( r2 < PI or r2 = PI ) by A7, XXREAL_0:1; suppose r2 < PI ; ::_thesis: not cos . r2 >= cos . r1 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 . ((r1 + r2) / 2) by A14, A15, Th21, RFUNCT_2:21; assume cos . r2 >= cos . r1 ; ::_thesis: contradiction hence contradiction by A10, A5, A22, A23, SIN_COS:30, XXREAL_0:1; ::_thesis: verum end; suppose r2 = PI ; ::_thesis: cos . r2 < cos . r1 hence cos . r2 < cos . r1 by A22, SIN_COS:30, SIN_COS:76; ::_thesis: verum end; end; end; hence cos . r2 < cos . r1 ; ::_thesis: verum end; end; end; hence cos . r2 < cos . r1 ; ::_thesis: verum end; hence cos | [.0,PI.] is decreasing by RFUNCT_2:21; ::_thesis: verum end; theorem Th26: :: COMPTRIG:26 cos | [.PI,(2 * PI).] is increasing proof now__::_thesis:_for_r1,_r2_being_Real_st_r1_in_[.PI,(2_*_PI).]_/\_(dom_cos)_&_r2_in_[.PI,(2_*_PI).]_/\_(dom_cos)_&_r1_<_r2_holds_ cos_._r2_>_cos_._r1 let r1, r2 be Real; ::_thesis: ( r1 in [.PI,(2 * PI).] /\ (dom cos) & r2 in [.PI,(2 * PI).] /\ (dom cos) & r1 < r2 implies cos . r2 > cos . r1 ) assume that A1: r1 in [.PI,(2 * PI).] /\ (dom cos) and A2: r2 in [.PI,(2 * PI).] /\ (dom cos) and A3: r1 < r2 ; ::_thesis: cos . r2 > cos . r1 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; abs (cos ((r1 + r2) / 2)) <= 1 by SIN_COS:27; then A6: abs (cos . ((r1 + r2) / 2)) <= 1 by SIN_COS:def_19; then A7: cos . ((r1 + r2) / 2) <= 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 < (r1 + r2) / 2 by A3, XREAL_1:226; then A10: PI < (r1 + r2) / 2 by A5, XXREAL_0:2; A11: (r1 + r2) / 2 < r2 by A3, XREAL_1:226; then (r1 + r2) / 2 < 2 * PI by A8, XXREAL_0:2; then (r1 + r2) / 2 in ].PI,(2 * PI).[ by A10, XXREAL_1:4; then A12: (r1 + r2) / 2 in ].PI,(2 * PI).[ /\ (dom cos) by SIN_COS:24, XBOOLE_0:def_4; abs (cos r2) <= 1 by SIN_COS:27; then abs (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 . ((r1 + r2) / 2) >= - 1 by A6, ABSVALUE:5; now__::_thesis:_cos_._r2_>_cos_._r1 percases ( PI < r1 or PI = r1 ) by A5, XXREAL_0:1; supposeA16: PI < r1 ; ::_thesis: cos . r2 > cos . r1 then A17: PI < r2 by A3, XXREAL_0:2; now__::_thesis:_cos_._r2_>_cos_._r1 percases ( r2 < 2 * PI or r2 = 2 * PI ) by A8, XXREAL_0:1; supposeA18: r2 < 2 * PI ; ::_thesis: cos . r2 > cos . r1 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; ::_thesis: verum end; supposeA20: r2 = 2 * PI ; ::_thesis: not cos . r2 <= cos . r1 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 . ((r1 + r2) / 2) > cos . r1 by A9, A12, Th22, RFUNCT_2:20; assume cos . r2 <= cos . r1 ; ::_thesis: contradiction hence contradiction by A7, A20, A21, SIN_COS:76, XXREAL_0:2; ::_thesis: verum end; end; end; hence cos . r2 > cos . r1 ; ::_thesis: verum end; supposeA22: PI = r1 ; ::_thesis: cos . r2 > cos . r1 now__::_thesis:_not_cos_._r2_<=_cos_._r1 percases ( r2 < 2 * PI or r2 = 2 * PI ) by A8, XXREAL_0:1; suppose r2 < 2 * PI ; ::_thesis: not cos . r2 <= cos . r1 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 . ((r1 + r2) / 2) by A11, A12, Th22, RFUNCT_2:20; assume cos . r2 <= cos . r1 ; ::_thesis: contradiction hence contradiction by A15, A13, A22, A23, SIN_COS:76, XXREAL_0:1; ::_thesis: verum end; suppose r2 = 2 * PI ; ::_thesis: cos . r2 > cos . r1 hence cos . r2 > cos . r1 by A22, SIN_COS:76; ::_thesis: verum end; end; end; hence cos . r2 > cos . r1 ; ::_thesis: verum end; end; end; hence cos . r2 > cos . r1 ; ::_thesis: verum end; hence cos | [.PI,(2 * PI).] is increasing by RFUNCT_2:20; ::_thesis: verum end; theorem Th27: :: COMPTRIG:27 for x being real number holds ( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] ) proof let x be real number ; ::_thesis: ( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] ) abs (cos x) <= 1 by SIN_COS:27; then abs (cos . x) <= 1 by SIN_COS:def_19; then A1: ( - 1 <= cos . x & cos . x <= 1 ) by ABSVALUE:5; abs (sin x) <= 1 by SIN_COS:27; then abs (sin . x) <= 1 by SIN_COS:def_17; then ( - 1 <= sin . x & sin . x <= 1 ) by ABSVALUE:5; hence ( sin . x in [.(- 1),1.] & cos . x in [.(- 1),1.] ) by A1, XXREAL_1:1; ::_thesis: verum end; theorem :: COMPTRIG:28 rng sin = [.(- 1),1.] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_1),1.]_implies_ex_x_being_set_st_ (_x_in_dom_sin_&_y_=_sin_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_sin_&_y_=_sin_._x_)_implies_y_in_[.(-_1),1.]_)_) let y be set ; ::_thesis: ( ( y in [.(- 1),1.] implies ex x being set st ( x in dom sin & y = sin . x ) ) & ( ex x being set st ( x in dom sin & y = sin . x ) implies y in [.(- 1),1.] ) ) thus ( y in [.(- 1),1.] implies ex x being set st ( x in dom sin & y = sin . x ) ) ::_thesis: ( ex x being set st ( x in dom sin & y = sin . x ) implies y in [.(- 1),1.] ) proof assume A1: y in [.(- 1),1.] ; ::_thesis: ex x being set st ( x in dom sin & y = sin . x ) 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 being Real such that x in [.(- (PI / 2)),(PI / 2).] and A2: y1 = sin . x by FCONT_2:15, SIN_COS:24; take x ; ::_thesis: ( x in dom sin & y = sin . x ) thus ( x in dom sin & y = sin . x ) by A2, SIN_COS:24; ::_thesis: verum end; thus ( ex x being set st ( x in dom sin & y = sin . x ) implies y in [.(- 1),1.] ) by Th27, SIN_COS:24; ::_thesis: verum end; hence rng sin = [.(- 1),1.] by FUNCT_1:def_3; ::_thesis: verum end; theorem :: COMPTRIG:29 rng cos = [.(- 1),1.] proof now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_1),1.]_implies_ex_x_being_set_st_ (_x_in_dom_cos_&_y_=_cos_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_cos_&_y_=_cos_._x_)_implies_y_in_[.(-_1),1.]_)_) let y be set ; ::_thesis: ( ( y in [.(- 1),1.] implies ex x being set st ( x in dom cos & y = cos . x ) ) & ( ex x being set st ( x in dom cos & y = cos . x ) implies y in [.(- 1),1.] ) ) thus ( y in [.(- 1),1.] implies ex x being set st ( x in dom cos & y = cos . x ) ) ::_thesis: ( ex x being set st ( x in dom cos & y = cos . x ) implies y in [.(- 1),1.] ) proof assume A1: y in [.(- 1),1.] ; ::_thesis: ex x being set st ( x in dom cos & y = cos . x ) 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 being Real such that x in [.0,PI.] and A2: y1 = cos . x by FCONT_2:15, SIN_COS:24; take x ; ::_thesis: ( x in dom cos & y = cos . x ) thus ( x in dom cos & y = cos . x ) by A2, SIN_COS:24; ::_thesis: verum end; thus ( ex x being set st ( x in dom cos & y = cos . x ) implies y in [.(- 1),1.] ) by Th27, SIN_COS:24; ::_thesis: verum end; hence rng cos = [.(- 1),1.] by FUNCT_1:def_3; ::_thesis: verum end; theorem :: COMPTRIG:30 rng (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- 1),1.] proof set sin1 = sin | [.(- (PI / 2)),(PI / 2).]; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_1),1.]_implies_ex_x_being_set_st_ (_x_in_dom_(sin_|_[.(-_(PI_/_2)),(PI_/_2).])_&_y_=_(sin_|_[.(-_(PI_/_2)),(PI_/_2).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(sin_|_[.(-_(PI_/_2)),(PI_/_2).])_&_y_=_(sin_|_[.(-_(PI_/_2)),(PI_/_2).])_._x_)_implies_y_in_[.(-_1),1.]_)_) let y be set ; ::_thesis: ( ( y in [.(- 1),1.] implies ex x being set st ( x in dom (sin | [.(- (PI / 2)),(PI / 2).]) & y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ) ) & ( ex x being set st ( x in dom (sin | [.(- (PI / 2)),(PI / 2).]) & y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ) implies y in [.(- 1),1.] ) ) thus ( y in [.(- 1),1.] implies ex x being set st ( x in dom (sin | [.(- (PI / 2)),(PI / 2).]) & y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (sin | [.(- (PI / 2)),(PI / 2).]) & y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ) implies y in [.(- 1),1.] ) proof assume A1: y in [.(- 1),1.] ; ::_thesis: ex x being set st ( x in dom (sin | [.(- (PI / 2)),(PI / 2).]) & y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ) then reconsider y1 = y as Real ; PI / 2 in [.(- (PI / 2)),(PI / 2).] by XXREAL_1:1; then A2: (sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2) = sin . (PI / 2) by FUNCT_1:49; - (PI / 2) in [.(- (PI / 2)),(PI / 2).] by XXREAL_1:1; then (sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2)) = sin . (- (PI / 2)) by FUNCT_1:49; then y1 in [.((sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2))),((sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2)).] by A1, A2, SIN_COS:30, SIN_COS:76; then A3: ( (sin | [.(- (PI / 2)),(PI / 2).]) | [.(- (PI / 2)),(PI / 2).] is continuous & y1 in [.((sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2))),((sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2)).] \/ [.((sin | [.(- (PI / 2)),(PI / 2).]) . (PI / 2)),((sin | [.(- (PI / 2)),(PI / 2).]) . (- (PI / 2))).] ) by XBOOLE_0:def_3; dom (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- (PI / 2)),(PI / 2).] /\ REAL by RELAT_1:61, SIN_COS:24 .= [.(- (PI / 2)),(PI / 2).] by XBOOLE_1:28 ; then consider x being Real such that A4: x in [.(- (PI / 2)),(PI / 2).] and A5: y1 = (sin | [.(- (PI / 2)),(PI / 2).]) . x by A3, FCONT_2:15; take x ; ::_thesis: ( x in dom (sin | [.(- (PI / 2)),(PI / 2).]) & y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ) x in REAL /\ [.(- (PI / 2)),(PI / 2).] by A4, XBOOLE_0:def_4; hence ( x in dom (sin | [.(- (PI / 2)),(PI / 2).]) & y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ) by A5, RELAT_1:61, SIN_COS:24; ::_thesis: verum end; thus ( ex x being set st ( x in dom (sin | [.(- (PI / 2)),(PI / 2).]) & y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ) implies y in [.(- 1),1.] ) ::_thesis: verum proof given x being set such that A6: x in dom (sin | [.(- (PI / 2)),(PI / 2).]) and A7: y = (sin | [.(- (PI / 2)),(PI / 2).]) . x ; ::_thesis: y in [.(- 1),1.] dom (sin | [.(- (PI / 2)),(PI / 2).]) 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 y in [.(- 1),1.] by Th27; ::_thesis: verum end; end; hence rng (sin | [.(- (PI / 2)),(PI / 2).]) = [.(- 1),1.] by FUNCT_1:def_3; ::_thesis: verum end; theorem :: COMPTRIG:31 rng (sin | [.(PI / 2),((3 / 2) * PI).]) = [.(- 1),1.] proof set sin1 = sin | [.(PI / 2),((3 / 2) * PI).]; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_1),1.]_implies_ex_x_being_set_st_ (_x_in_dom_(sin_|_[.(PI_/_2),((3_/_2)_*_PI).])_&_y_=_(sin_|_[.(PI_/_2),((3_/_2)_*_PI).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(sin_|_[.(PI_/_2),((3_/_2)_*_PI).])_&_y_=_(sin_|_[.(PI_/_2),((3_/_2)_*_PI).])_._x_)_implies_y_in_[.(-_1),1.]_)_) let y be set ; ::_thesis: ( ( y in [.(- 1),1.] implies ex x being set st ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) ) & ( ex x being set st ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) implies y in [.(- 1),1.] ) ) thus ( y in [.(- 1),1.] implies ex x being set st ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) implies y in [.(- 1),1.] ) proof (3 / 2) * PI in [.(PI / 2),((3 / 2) * PI).] by Lm4, XXREAL_1:1; then A1: (sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI) = sin . ((3 / 2) * PI) by FUNCT_1:49; assume A2: y in [.(- 1),1.] ; ::_thesis: ex x being set st ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) then reconsider y1 = y as Real ; A3: dom (sin | [.(PI / 2),((3 / 2) * PI).]) = [.(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 (sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2) = sin . (PI / 2) by FUNCT_1:49; then ( (sin | [.(PI / 2),((3 / 2) * PI).]) | [.(PI / 2),((3 / 2) * PI).] is continuous & y1 in [.((sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2)),((sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI)).] \/ [.((sin | [.(PI / 2),((3 / 2) * PI).]) . ((3 / 2) * PI)),((sin | [.(PI / 2),((3 / 2) * PI).]) . (PI / 2)).] ) by A2, A1, SIN_COS:76, XBOOLE_0:def_3; then consider x being Real such that A4: x in [.(PI / 2),((3 / 2) * PI).] and A5: y1 = (sin | [.(PI / 2),((3 / 2) * PI).]) . x by A3, Lm4, FCONT_2:15; take x ; ::_thesis: ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) x in REAL /\ [.(PI / 2),((3 / 2) * PI).] by A4, XBOOLE_0:def_4; hence ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) by A5, RELAT_1:61, SIN_COS:24; ::_thesis: verum end; thus ( ex x being set st ( x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) & y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ) implies y in [.(- 1),1.] ) ::_thesis: verum proof given x being set such that A6: x in dom (sin | [.(PI / 2),((3 / 2) * PI).]) and A7: y = (sin | [.(PI / 2),((3 / 2) * PI).]) . x ; ::_thesis: y in [.(- 1),1.] dom (sin | [.(PI / 2),((3 / 2) * PI).]) 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 y in [.(- 1),1.] by Th27; ::_thesis: verum end; end; hence rng (sin | [.(PI / 2),((3 / 2) * PI).]) = [.(- 1),1.] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th32: :: COMPTRIG:32 rng (cos | [.0,PI.]) = [.(- 1),1.] proof set cos1 = cos | [.0,PI.]; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_1),1.]_implies_ex_x_being_set_st_ (_x_in_dom_(cos_|_[.0,PI.])_&_y_=_(cos_|_[.0,PI.])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(cos_|_[.0,PI.])_&_y_=_(cos_|_[.0,PI.])_._x_)_implies_y_in_[.(-_1),1.]_)_) let y be set ; ::_thesis: ( ( y in [.(- 1),1.] implies ex x being set st ( x in dom (cos | [.0,PI.]) & y = (cos | [.0,PI.]) . x ) ) & ( ex x being set st ( x in dom (cos | [.0,PI.]) & y = (cos | [.0,PI.]) . x ) implies y in [.(- 1),1.] ) ) thus ( y in [.(- 1),1.] implies ex x being set st ( x in dom (cos | [.0,PI.]) & y = (cos | [.0,PI.]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (cos | [.0,PI.]) & y = (cos | [.0,PI.]) . x ) implies y in [.(- 1),1.] ) proof PI in [.0,PI.] by XXREAL_1:1; then A1: (cos | [.0,PI.]) . PI = cos . PI by FUNCT_1:49; assume A2: y in [.(- 1),1.] ; ::_thesis: ex x being set st ( x in dom (cos | [.0,PI.]) & y = (cos | [.0,PI.]) . x ) then reconsider y1 = y as Real ; A3: dom (cos | [.0,PI.]) = [.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 (cos | [.0,PI.]) . 0 = cos . 0 by FUNCT_1:49; then ( (cos | [.0,PI.]) | [.0,PI.] is continuous & y1 in [.((cos | [.0,PI.]) . 0),((cos | [.0,PI.]) . PI).] \/ [.((cos | [.0,PI.]) . PI),((cos | [.0,PI.]) . 0).] ) by A2, A1, SIN_COS:30, SIN_COS:76, XBOOLE_0:def_3; then consider x being Real such that A4: x in [.0,PI.] and A5: y1 = (cos | [.0,PI.]) . x by A3, FCONT_2:15; take x ; ::_thesis: ( x in dom (cos | [.0,PI.]) & y = (cos | [.0,PI.]) . x ) x in REAL /\ [.0,PI.] by A4, XBOOLE_0:def_4; hence ( x in dom (cos | [.0,PI.]) & y = (cos | [.0,PI.]) . x ) by A5, RELAT_1:61, SIN_COS:24; ::_thesis: verum end; thus ( ex x being set st ( x in dom (cos | [.0,PI.]) & y = (cos | [.0,PI.]) . x ) implies y in [.(- 1),1.] ) ::_thesis: verum proof given x being set such that A6: x in dom (cos | [.0,PI.]) and A7: y = (cos | [.0,PI.]) . x ; ::_thesis: y in [.(- 1),1.] dom (cos | [.0,PI.]) 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 y in [.(- 1),1.] by Th27; ::_thesis: verum end; end; hence rng (cos | [.0,PI.]) = [.(- 1),1.] by FUNCT_1:def_3; ::_thesis: verum end; theorem Th33: :: COMPTRIG:33 rng (cos | [.PI,(2 * PI).]) = [.(- 1),1.] proof set cos1 = cos | [.PI,(2 * PI).]; now__::_thesis:_for_y_being_set_holds_ (_(_y_in_[.(-_1),1.]_implies_ex_x_being_set_st_ (_x_in_dom_(cos_|_[.PI,(2_*_PI).])_&_y_=_(cos_|_[.PI,(2_*_PI).])_._x_)_)_&_(_ex_x_being_set_st_ (_x_in_dom_(cos_|_[.PI,(2_*_PI).])_&_y_=_(cos_|_[.PI,(2_*_PI).])_._x_)_implies_y_in_[.(-_1),1.]_)_) let y be set ; ::_thesis: ( ( y in [.(- 1),1.] implies ex x being set st ( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) ) & ( ex x being set st ( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) implies y in [.(- 1),1.] ) ) thus ( y in [.(- 1),1.] implies ex x being set st ( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) ) ::_thesis: ( ex x being set st ( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) implies y in [.(- 1),1.] ) proof 2 * PI in [.PI,(2 * PI).] by Lm3, XXREAL_1:1; then A1: (cos | [.PI,(2 * PI).]) . (2 * PI) = cos . (2 * PI) by FUNCT_1:49; assume A2: y in [.(- 1),1.] ; ::_thesis: ex x being set st ( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) then reconsider y1 = y as Real ; A3: dom (cos | [.PI,(2 * PI).]) = [.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 (cos | [.PI,(2 * PI).]) . PI = cos . PI by FUNCT_1:49; then ( (cos | [.PI,(2 * PI).]) | [.PI,(2 * PI).] is continuous & y1 in [.((cos | [.PI,(2 * PI).]) . PI),((cos | [.PI,(2 * PI).]) . (2 * PI)).] \/ [.((cos | [.PI,(2 * PI).]) . (2 * PI)),((cos | [.PI,(2 * PI).]) . PI).] ) by A2, A1, SIN_COS:76, XBOOLE_0:def_3; then consider x being Real such that A4: x in [.PI,(2 * PI).] and A5: y1 = (cos | [.PI,(2 * PI).]) . x by A3, Lm3, FCONT_2:15; take x ; ::_thesis: ( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) x in REAL /\ [.PI,(2 * PI).] by A4, XBOOLE_0:def_4; hence ( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) by A5, RELAT_1:61, SIN_COS:24; ::_thesis: verum end; thus ( ex x being set st ( x in dom (cos | [.PI,(2 * PI).]) & y = (cos | [.PI,(2 * PI).]) . x ) implies y in [.(- 1),1.] ) ::_thesis: verum proof given x being set such that A6: x in dom (cos | [.PI,(2 * PI).]) and A7: y = (cos | [.PI,(2 * PI).]) . x ; ::_thesis: y in [.(- 1),1.] dom (cos | [.PI,(2 * PI).]) 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 y in [.(- 1),1.] by Th27; ::_thesis: verum end; end; hence rng (cos | [.PI,(2 * PI).]) = [.(- 1),1.] by FUNCT_1:def_3; ::_thesis: verum end; begin definition let z be complex number ; func Arg z -> Real means :Def1: :: COMPTRIG:def 1 ( z = (|.z.| * (cos it)) + ((|.z.| * (sin it)) * ) & 0 <= it & it < 2 * PI ) if z <> 0 otherwise it = 0 ; existence ( ( z <> 0 implies ex b1 being Real st ( z = (|.z.| * (cos b1)) + ((|.z.| * (sin b1)) * ) & 0 <= b1 & b1 < 2 * PI ) ) & ( not z <> 0 implies ex b1 being Real st b1 = 0 ) ) proof thus ( z <> 0 implies ex r being Real st ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) ) ::_thesis: ( not z <> 0 implies ex b1 being Real st b1 = 0 ) proof |.z.| >= 0 by COMPLEX1:46; then A1: (Re z) / |.z.| <= 1 by COMPLEX1:54, XREAL_1:185; assume A2: z <> 0 ; ::_thesis: ex r being Real st ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) then A3: |.z.| <> 0 by COMPLEX1:45; now__::_thesis:_ex_r_being_Real_st_ (_z_=_(|.z.|_*_(cos_r))_+_((|.z.|_*_(sin_r))_*_)_&_0_<=_r_&_r_<_2_*_PI_) percases ( Im z >= 0 or Im z < 0 ) ; supposeA4: Im z >= 0 ; ::_thesis: ex r being Real st ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) set 0PI = [.0,PI.]; reconsider cos1 = cos | [.0,PI.] as PartFunc of [.0,PI.],REAL by PARTFUN1:10; reconsider cos1 = cos1 as one-to-one PartFunc of [.0,PI.],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 = r; ::_thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) 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 .= abs ((Im z) / |.z.|) by COMPLEX1:72 .= (abs (Im z)) / (abs |.z.|) by COMPLEX1:67 .= (abs (Im z)) / |.z.| ; then abs (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; ::_thesis: ( 0 <= r & r < 2 * PI ) thus 0 <= r by A7, XXREAL_1:1; ::_thesis: r < 2 * PI r <= PI by A7, XXREAL_1:1; hence r < 2 * PI by Lm3, XXREAL_0:2; ::_thesis: verum end; supposeA12: Im z < 0 ; ::_thesis: ex r being Real st ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) now__::_thesis:_ex_r_being_Real_st_ (_z_=_(|.z.|_*_(cos_r))_+_((|.z.|_*_(sin_r))_*_)_&_0_<=_r_&_r_<_2_*_PI_) percases ( Re z <> |.z.| or Re z = |.z.| ) ; supposeA13: Re z <> |.z.| ; ::_thesis: ex r being Real st ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) set 0PI = [.PI,(2 * PI).]; reconsider cos1 = cos | [.PI,(2 * PI).] as PartFunc of [.PI,(2 * PI).],REAL by PARTFUN1:10; reconsider cos1 = cos1 as one-to-one PartFunc of [.PI,(2 * PI).],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 ; ::_thesis: contradiction hence contradiction by A18, A15, A21, A20, FUNCT_1:def_4; ::_thesis: verum 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 = r; ::_thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) 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 .= abs ((Im z) / |.z.|) by COMPLEX1:72 .= (abs (Im z)) / (abs |.z.|) by COMPLEX1:67 .= (abs (Im z)) / |.z.| ; then sin . r = (- (abs (Im z))) / |.z.| ; then - (abs (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; ::_thesis: ( 0 <= r & r < 2 * PI ) thus 0 <= r by A16, XXREAL_1:1; ::_thesis: r < 2 * PI r <= 2 * PI by A16, XXREAL_1:1; hence r < 2 * PI by A19, XXREAL_0:1; ::_thesis: verum end; supposeA26: Re z = |.z.| ; ::_thesis: ex r being Real st ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) reconsider r = 0 as Real ; take r = r; ::_thesis: ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) (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; ::_thesis: ( 0 <= r & r < 2 * PI ) thus 0 <= r ; ::_thesis: r < 2 * PI thus r < 2 * PI by Lm1; ::_thesis: verum end; end; end; hence ex r being Real st ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) ; ::_thesis: verum end; end; end; hence ex r being Real st ( z = (|.z.| * (cos r)) + ((|.z.| * (sin r)) * ) & 0 <= r & r < 2 * PI ) ; ::_thesis: verum end; thus ( not z <> 0 implies ex b1 being Real st b1 = 0 ) ; ::_thesis: verum end; uniqueness for b1, b2 being Real holds ( ( z <> 0 & z = (|.z.| * (cos b1)) + ((|.z.| * (sin b1)) * ) & 0 <= b1 & b1 < 2 * PI & z = (|.z.| * (cos b2)) + ((|.z.| * (sin b2)) * ) & 0 <= b2 & b2 < 2 * PI implies b1 = b2 ) & ( not z <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) proof ( z <> 0 implies for x, y being 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 ; ::_thesis: for x, y being 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 then A27: |.z.| <> 0 by COMPLEX1:45; let x, y be Real; ::_thesis: ( z = (|.z.| * (cos x)) + ((|.z.| * (sin x)) * ) & 0 <= x & x < 2 * PI & z = (|.z.| * (cos y)) + ((|.z.| * (sin y)) * ) & 0 <= y & y < 2 * PI implies x = y ) 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 ; ::_thesis: x = y |.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__::_thesis:_not_x_<>_y percases ( ( x <= PI & y <= PI ) or ( x > PI & y > PI ) or ( x <= PI & y > PI ) or ( y <= PI & x > PI ) ) ; supposeA36: ( x <= PI & y <= PI ) ; ::_thesis: not x <> y 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; supposeA39: ( x > PI & y > PI ) ; ::_thesis: not x <> y 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 ; ::_thesis: contradiction 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; ::_thesis: verum end; supposeA42: ( x <= PI & y > PI ) ; ::_thesis: x = y 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 x = y by A35, A43, SIN_COS:def_17; ::_thesis: verum end; supposeA44: ( y <= PI & x > PI ) ; ::_thesis: x = y 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 x = y by A35, A45, SIN_COS:def_17; ::_thesis: verum end; end; end; hence x = y ; ::_thesis: verum end; hence for b1, b2 being Real holds ( ( z <> 0 & z = (|.z.| * (cos b1)) + ((|.z.| * (sin b1)) * ) & 0 <= b1 & b1 < 2 * PI & z = (|.z.| * (cos b2)) + ((|.z.| * (sin b2)) * ) & 0 <= b2 & b2 < 2 * PI implies b1 = b2 ) & ( not z <> 0 & b1 = 0 & b2 = 0 implies b1 = b2 ) ) ; ::_thesis: verum end; consistency for b1 being Real holds verum ; end; :: deftheorem Def1 defines Arg COMPTRIG:def_1_:_ for z being complex number for b2 being Real holds ( ( z <> 0 implies ( b2 = Arg z iff ( z = (|.z.| * (cos b2)) + ((|.z.| * (sin b2)) * ) & 0 <= b2 & b2 < 2 * PI ) ) ) & ( not z <> 0 implies ( b2 = Arg z iff b2 = 0 ) ) ); theorem Th34: :: COMPTRIG:34 for z being complex number holds ( 0 <= Arg z & Arg z < 2 * PI ) proof let z be complex number ; ::_thesis: ( 0 <= Arg z & Arg z < 2 * PI ) ( ( 0 <= Arg z & Arg z < 2 * PI ) or z = 0 ) by Def1; hence ( 0 <= Arg z & Arg z < 2 * PI ) by Def1, Lm6, Lm7; ::_thesis: verum end; theorem Th35: :: COMPTRIG:35 for x being Real st x >= 0 holds Arg x = 0 proof let x be Real; ::_thesis: ( x >= 0 implies Arg x = 0 ) A1: ( 0 <= Arg (x + (0 * )) & Arg (x + (0 * )) < 2 * PI ) by Th34; assume A2: x >= 0 ; ::_thesis: Arg x = 0 percases ( x > - 0 or x + (0 * ) = 0 ) by A2; supposeA3: x > - 0 ; ::_thesis: Arg 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 Arg x = 0 by COMPLEX1:46; ::_thesis: verum end; suppose x + (0 * ) = 0 ; ::_thesis: Arg x = 0 hence Arg x = 0 by Def1; ::_thesis: verum end; end; end; theorem Th36: :: COMPTRIG:36 for x being Real st x < 0 holds Arg x = PI proof let x be Real; ::_thesis: ( x < 0 implies Arg x = PI ) A1: ( 0 <= Arg (x + (0 * )) & Arg (x + (0 * )) < 2 * PI ) by Th34; assume A2: x < 0 ; ::_thesis: Arg x = PI 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 Arg x = PI by A2, COMPLEX1:46; ::_thesis: verum end; theorem Th37: :: COMPTRIG:37 for x being Real st x > 0 holds Arg (x * ) = PI / 2 proof let x be Real; ::_thesis: ( x > 0 implies Arg (x * ) = PI / 2 ) A1: ( 0 <= Arg (0 + (x * )) & Arg (0 + (x * )) < 2 * PI ) by Th34; assume A2: x > 0 ; ::_thesis: Arg (x * ) = PI / 2 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 Arg (x * ) = PI / 2 by COMPLEX1:46; ::_thesis: verum end; theorem Th38: :: COMPTRIG:38 for x being Real st x < 0 holds Arg (x * ) = (3 / 2) * PI proof let x be Real; ::_thesis: ( x < 0 implies Arg (x * ) = (3 / 2) * PI ) A1: ( 0 <= Arg (0 + (x * )) & Arg (0 + (x * )) < 2 * PI ) by Th34; assume A2: x < 0 ; ::_thesis: Arg (x * ) = (3 / 2) * PI 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 Arg (x * ) = (3 / 2) * PI by A2, COMPLEX1:46; ::_thesis: verum end; theorem :: COMPTRIG:39 Arg 1 = 0 by Th35; theorem :: COMPTRIG:40 Arg = PI / 2 proof = 0 + (1 * ) ; hence Arg = PI / 2 by Th37; ::_thesis: verum end; theorem Th41: :: COMPTRIG:41 for z being complex number holds ( Arg z in ].0,(PI / 2).[ iff ( Re z > 0 & Im z > 0 ) ) proof let z be complex number ; ::_thesis: ( Arg z in ].0,(PI / 2).[ iff ( Re z > 0 & Im z > 0 ) ) A1: Arg z < 2 * PI by Th34; thus ( Arg z in ].0,(PI / 2).[ implies ( Re z > 0 & Im z > 0 ) ) ::_thesis: ( Re z > 0 & Im z > 0 implies Arg z in ].0,(PI / 2).[ ) proof assume A2: Arg z in ].0,(PI / 2).[ ; ::_thesis: ( Re z > 0 & Im z > 0 ) 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; ::_thesis: Im z > 0 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 Im z > 0 by A4, COMPLEX1:12; ::_thesis: verum end; assume that A5: Re z > 0 and A6: Im z > 0 ; ::_thesis: Arg z in ].0,(PI / 2).[ 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 Arg z in ].0,(PI / 2).[ by A10, Lm5, XXREAL_0:2, XXREAL_1:4; ::_thesis: verum end; theorem Th42: :: COMPTRIG:42 for z being complex number holds ( Arg z in ].(PI / 2),PI.[ iff ( Re z < 0 & Im z > 0 ) ) proof let z be complex number ; ::_thesis: ( Arg z in ].(PI / 2),PI.[ iff ( Re z < 0 & Im z > 0 ) ) thus ( Arg z in ].(PI / 2),PI.[ implies ( Re z < 0 & Im z > 0 ) ) ::_thesis: ( Re z < 0 & Im z > 0 implies Arg z in ].(PI / 2),PI.[ ) proof assume A1: Arg z in ].(PI / 2),PI.[ ; ::_thesis: ( Re z < 0 & Im z > 0 ) 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; ::_thesis: Im z > 0 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 Im z > 0 by A4, COMPLEX1:12; ::_thesis: verum end; assume that A5: Re z < 0 and A6: Im z > 0 ; ::_thesis: Arg z in ].(PI / 2),PI.[ 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 Arg z in ].(PI / 2),PI.[ by A9, Th34, XXREAL_1:4; ::_thesis: verum end; theorem Th43: :: COMPTRIG:43 for z being complex number holds ( Arg z in ].PI,((3 / 2) * PI).[ iff ( Re z < 0 & Im z < 0 ) ) proof let z be complex number ; ::_thesis: ( Arg z in ].PI,((3 / 2) * PI).[ iff ( Re z < 0 & Im z < 0 ) ) thus ( Arg z in ].PI,((3 / 2) * PI).[ implies ( Re z < 0 & Im z < 0 ) ) ::_thesis: ( Re z < 0 & Im z < 0 implies Arg z in ].PI,((3 / 2) * PI).[ ) proof assume A1: Arg z in ].PI,((3 / 2) * PI).[ ; ::_thesis: ( Re z < 0 & Im z < 0 ) 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; ::_thesis: Im z < 0 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 Im z < 0 by A4, COMPLEX1:12; ::_thesis: verum end; assume that A5: Re z < 0 and A6: Im z < 0 ; ::_thesis: Arg z in ].PI,((3 / 2) * PI).[ 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 Arg z in ].PI,((3 / 2) * PI).[ by A10, XXREAL_1:4; ::_thesis: verum end; theorem Th44: :: COMPTRIG:44 for z being complex number holds ( Arg z in ].((3 / 2) * PI),(2 * PI).[ iff ( Re z > 0 & Im z < 0 ) ) proof let z be complex number ; ::_thesis: ( Arg z in ].((3 / 2) * PI),(2 * PI).[ iff ( Re z > 0 & Im z < 0 ) ) thus ( Arg z in ].((3 / 2) * PI),(2 * PI).[ implies ( Re z > 0 & Im z < 0 ) ) ::_thesis: ( Re z > 0 & Im z < 0 implies Arg z in ].((3 / 2) * PI),(2 * PI).[ ) proof assume A1: Arg z in ].((3 / 2) * PI),(2 * PI).[ ; ::_thesis: ( Re z > 0 & Im z < 0 ) 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; ::_thesis: Im z < 0 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 Im z < 0 by A4, COMPLEX1:12; ::_thesis: verum end; assume that A5: Re z > 0 and A6: Im z < 0 ; ::_thesis: Arg z in ].((3 / 2) * PI),(2 * PI).[ 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 Arg z in ].((3 / 2) * PI),(2 * PI).[ by A10, A9, Lm2, XXREAL_0:2, XXREAL_1:4; ::_thesis: verum end; theorem Th45: :: COMPTRIG:45 for z being complex number st Im z > 0 holds sin (Arg z) > 0 proof let z be complex number ; ::_thesis: ( Im z > 0 implies sin (Arg z) > 0 ) ( 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 ; ::_thesis: sin (Arg 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 sin (Arg z) > 0 by SIN_COS:def_17; ::_thesis: verum end; theorem Th46: :: COMPTRIG:46 for z being complex number st Im z < 0 holds sin (Arg z) < 0 proof let z be complex number ; ::_thesis: ( Im z < 0 implies sin (Arg z) < 0 ) ( 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 ; ::_thesis: sin (Arg 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 sin (Arg z) < 0 by SIN_COS:def_17; ::_thesis: verum end; theorem :: COMPTRIG:47 for z being complex number st Im z >= 0 holds sin (Arg z) >= 0 proof let z be complex number ; ::_thesis: ( Im z >= 0 implies sin (Arg z) >= 0 ) assume Im z >= 0 ; ::_thesis: sin (Arg 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 sin (Arg z) >= 0 by Th35, Th36, SIN_COS:31, SIN_COS:77; ::_thesis: verum end; theorem :: COMPTRIG:48 for z being complex number st Im z <= 0 holds sin (Arg z) <= 0 proof let z be complex number ; ::_thesis: ( Im z <= 0 implies sin (Arg z) <= 0 ) assume Im z <= 0 ; ::_thesis: sin (Arg 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 sin (Arg z) <= 0 by Th35, Th36, SIN_COS:31, SIN_COS:77; ::_thesis: verum end; theorem Th49: :: COMPTRIG:49 for z being complex number st Re z > 0 holds cos (Arg z) > 0 proof let z be complex number ; ::_thesis: ( Re z > 0 implies cos (Arg z) > 0 ) ( 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 ; ::_thesis: cos (Arg 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 cos (Arg z) > 0 by SIN_COS:def_19; ::_thesis: verum end; theorem Th50: :: COMPTRIG:50 for z being complex number st Re z < 0 holds cos (Arg z) < 0 proof let z be complex number ; ::_thesis: ( Re z < 0 implies cos (Arg z) < 0 ) ( 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 ; ::_thesis: cos (Arg 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 cos (Arg z) < 0 by SIN_COS:def_19; ::_thesis: verum end; theorem :: COMPTRIG:51 for z being complex number st Re z >= 0 holds cos (Arg z) >= 0 proof let z be complex number ; ::_thesis: ( Re z >= 0 implies cos (Arg z) >= 0 ) assume Re z >= 0 ; ::_thesis: cos (Arg 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 cos (Arg z) >= 0 by Def1, Th37, Th38, SIN_COS:31, SIN_COS:77; ::_thesis: verum end; theorem :: COMPTRIG:52 for z being complex number st Re z <= 0 & z <> 0 holds cos (Arg z) <= 0 proof let z be complex number ; ::_thesis: ( Re z <= 0 & z <> 0 implies cos (Arg z) <= 0 ) assume that A1: Re z <= 0 and A2: z <> 0 ; ::_thesis: cos (Arg 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 cos (Arg z) <= 0 by Th37, Th38, SIN_COS:77; ::_thesis: verum end; theorem Th53: :: COMPTRIG:53 for x being real number for n being Nat holds ((cos x) + ((sin x) * )) |^ n = (cos (n * x)) + ((sin (n * x)) * ) proof let x be real number ; ::_thesis: for n being Nat holds ((cos x) + ((sin x) * )) |^ n = (cos (n * x)) + ((sin (n * x)) * ) defpred S1[ Nat] means ((cos x) + ((sin x) * )) |^ $1 = (cos ($1 * x)) + ((sin ($1 * x)) * ); A1: now__::_thesis:_for_n_being_Nat_st_S1[n]_holds_ S1[n_+_1] let n be Nat; ::_thesis: ( S1[n] implies S1[n + 1] ) assume S1[n] ; ::_thesis: S1[n + 1] 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 S1[n + 1] ; ::_thesis: verum end; A2: S1[ 0 ] by NEWTON:4, SIN_COS:31; thus for n being Nat holds S1[n] from NAT_1:sch_2(A2, A1); ::_thesis: verum end; theorem :: COMPTRIG:54 for z being Element of COMPLEX for n being 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 ; ::_thesis: for n being Nat st ( z <> 0 or n <> 0 ) holds z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * ) let n be Nat; ::_thesis: ( ( z <> 0 or n <> 0 ) implies z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * ) ) assume A1: ( z <> 0 or n <> 0 ) ; ::_thesis: z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * ) percases ( z <> 0 or ( z = 0 & n > 0 ) ) by A1; suppose z <> 0 ; ::_thesis: z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * ) 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)))) * ) ; ::_thesis: verum end; supposeA2: ( z = 0 & n > 0 ) ; ::_thesis: z |^ n = ((|.z.| |^ n) * (cos (n * (Arg z)))) + (((|.z.| |^ n) * (sin (n * (Arg z)))) * ) 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 ; ::_thesis: verum end; end; end; theorem Th55: :: COMPTRIG:55 for x being Real for n, k being 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; ::_thesis: for n, k being Nat st n <> 0 holds ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos x) + ((sin x) * ) let n, k be Nat; ::_thesis: ( n <> 0 implies ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos x) + ((sin x) * ) ) assume A1: n <> 0 ; ::_thesis: ((cos ((x + ((2 * PI) * k)) / n)) + ((sin ((x + ((2 * PI) * k)) / n)) * )) |^ n = (cos x) + ((sin x) * ) 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 ; ::_thesis: verum end; theorem Th56: :: COMPTRIG:56 for z being complex number for n, k being 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 number ; ::_thesis: for n, k being 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 let n, k be Nat; ::_thesis: ( n <> 0 implies z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n ) assume A1: n <> 0 ; ::_thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n then A2: n >= 0 + 1 by NAT_1:13; percases ( z <> 0 or z = 0 ) ; supposeA3: z <> 0 ; ::_thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n 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 ; ::_thesis: verum end; supposeA4: z = 0 ; ::_thesis: z = (((n -root |.z.|) * (cos (((Arg z) + ((2 * PI) * k)) / n))) + (((n -root |.z.|) * (sin (((Arg z) + ((2 * PI) * k)) / n))) * )) |^ n 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 ; ::_thesis: verum end; end; end; definition let x be complex number ; let n be non empty Nat; mode CRoot of n,x -> complex number means :Def2: :: COMPTRIG:def 2 it |^ n = x; existence ex b1 being complex number st b1 |^ n = x 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 ; ::_thesis: z |^ n = x thus z |^ n = x by Th56; ::_thesis: verum end; end; :: deftheorem Def2 defines CRoot COMPTRIG:def_2_:_ for x being complex number for n being non empty Nat for b3 being complex number holds ( b3 is CRoot of n,x iff b3 |^ n = x ); theorem :: COMPTRIG:57 for x being Element of COMPLEX for n being non empty Nat for k being 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 ; ::_thesis: for n being non empty Nat for k being 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 let n be non empty Nat; ::_thesis: for k being 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 let k be Nat; ::_thesis: ((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 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 ((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 by Def2; ::_thesis: verum end; theorem :: COMPTRIG:58 for x being Element of COMPLEX for v being CRoot of 1,x holds v = x proof let x be Element of COMPLEX ; ::_thesis: for v being CRoot of 1,x holds v = x let v be CRoot of 1,x; ::_thesis: v = x v |^ 1 = x by Def2; hence v = x by NEWTON:5; ::_thesis: verum end; theorem :: COMPTRIG:59 for n being non empty Nat for v being CRoot of n, 0 holds v = 0 proof let n be non empty Nat; ::_thesis: for v being CRoot of n, 0 holds v = 0 let v be CRoot of n, 0 ; ::_thesis: v = 0 defpred S1[ Nat] means v |^ $1 = 0 ; assume A1: v <> 0 ; ::_thesis: contradiction A2: now__::_thesis:_for_k_being_non_empty_Nat_st_k_<>_1_&_S1[k]_holds_ ex_t_being_non_empty_Nat_st_ (_t_<_k_&_S1[t]_) let k be non empty Nat; ::_thesis: ( k <> 1 & S1[k] implies ex t being non empty Nat st ( t < k & S1[t] ) ) assume that A3: k <> 1 and A4: S1[k] ; ::_thesis: ex t being non empty Nat st ( t < k & S1[t] ) consider t being Nat such that A5: k = t + 1 by NAT_1:6; reconsider t = t as non empty Nat by A3, A5; take t = t; ::_thesis: ( t < k & S1[t] ) thus t < k by A5, NAT_1:13; ::_thesis: S1[t] v |^ k = (v |^ t) * v by A5, NEWTON:6; hence S1[t] by A1, A4; ::_thesis: verum end; A6: ex n being non empty Nat st S1[n] proof take n ; ::_thesis: S1[n] thus S1[n] by Def2; ::_thesis: verum end; S1[1] from COMPTRIG:sch_1(A6, A2); hence contradiction by A1, NEWTON:5; ::_thesis: verum end; theorem :: COMPTRIG:60 for n being non empty Nat for x being Element of COMPLEX for v being CRoot of n,x st v = 0 holds x = 0 proof let n be non empty Nat; ::_thesis: for x being Element of COMPLEX for v being CRoot of n,x st v = 0 holds x = 0 let x be Element of COMPLEX ; ::_thesis: for v being CRoot of n,x st v = 0 holds x = 0 let v be CRoot of n,x; ::_thesis: ( v = 0 implies x = 0 ) assume v = 0 ; ::_thesis: x = 0 then ( n >= 0 + 1 & 0 |^ n = x ) by Def2, NAT_1:13; hence x = 0 by NEWTON:11; ::_thesis: verum end; theorem :: COMPTRIG:61 for a being real number st 0 <= a & a < 2 * PI & cos a = 1 holds a = 0 proof let a be real number ; ::_thesis: ( 0 <= a & a < 2 * PI & cos a = 1 implies a = 0 ) assume that A1: ( 0 <= a & a < 2 * PI ) and A2: cos a = 1 ; ::_thesis: a = 0 (1 * 1) + ((sin a) * (sin a)) = 1 by A2, SIN_COS:29; then sin a = 0 ; hence a = 0 by A1, A2, Th17, SIN_COS:77; ::_thesis: verum end; theorem :: COMPTRIG:62 for z being complex number holds z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * ) proof let z be complex number ; ::_thesis: z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * ) percases ( z = 0 or z <> 0 ) ; suppose z = 0 ; ::_thesis: z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * ) hence z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * ) by COMPLEX1:44; ::_thesis: verum end; suppose z <> 0 ; ::_thesis: z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * ) hence z = (|.z.| * (cos (Arg z))) + ((|.z.| * (sin (Arg z))) * ) by Def1; ::_thesis: verum end; end; end;