:: Inverse Trigonometric Functions Arcsin and Arccos :: by Artur Korni{\l}owicz and Yasunari Shidama :: :: Received September 25, 2004 :: Copyright (c) 2004-2012 Association of Mizar Users begin theorem Th1: :: SIN_COS6:1 for r, s being real number st 0 <= r & r < s holds [\(r / s)/] = 0 proofend; theorem Th2: :: SIN_COS6:2 for f being Function for X, Y being set st f | X is one-to-one & Y c= X holds f | Y is one-to-one proofend; begin theorem Th3: :: SIN_COS6:3 for r being real number holds - 1 <= sin r proofend; theorem Th4: :: SIN_COS6:4 for r being real number holds sin r <= 1 proofend; theorem Th5: :: SIN_COS6:5 for r being real number holds - 1 <= cos r proofend; theorem Th6: :: SIN_COS6:6 for r being real number holds cos r <= 1 proofend; deffunc H1( Integer) -> Element of REAL = (2 * PI) * $1; Lm1: [.((- (PI / 2)) + H1( 0 )),((PI / 2) + H1( 0 )).] = [.(- (PI / 2)),(PI / 2).] ; Lm2: [.((PI / 2) + H1( 0 )),(((3 / 2) * PI) + H1( 0 )).] = [.(PI / 2),((3 / 2) * PI).] ; Lm3: [.H1( 0 ),(PI + H1( 0 )).] = [.0,PI.] ; Lm4: [.(PI + H1( 0 )),((2 * PI) + H1( 0 )).] = [.PI,(2 * PI).] ; Lm5: for r, s being real number st (r ^2) + (s ^2) = 1 holds ( - 1 <= r & r <= 1 ) proofend; registration cluster PI -> positive ; coherence PI is positive proofend; end; Lm6: PI / 2 < PI / 1 by XREAL_1:76; Lm7: 1 * PI < (3 / 2) * PI by XREAL_1:68; Lm8: 0 + H1(1) < (PI / 2) + H1(1) by XREAL_1:6; Lm9: (3 / 2) * PI < 2 * PI by XREAL_1:68; Lm10: 1 * PI < 2 * PI by XREAL_1:68; theorem Th7: :: SIN_COS6:7 ( sin (- (PI / 2)) = - 1 & sin . (- (PI / 2)) = - 1 ) proofend; theorem Th8: :: SIN_COS6:8 for r being real number for i being integer number holds sin . r = sin . (r + ((2 * PI) * i)) proofend; theorem Th9: :: SIN_COS6:9 ( cos (- (PI / 2)) = 0 & cos . (- (PI / 2)) = 0 ) proofend; theorem Th10: :: SIN_COS6:10 for r being real number for i being integer number holds cos . r = cos . (r + ((2 * PI) * i)) proofend; theorem Th11: :: SIN_COS6:11 for r being real number for i being integer number st (2 * PI) * i < r & r < PI + ((2 * PI) * i) holds sin r > 0 proofend; theorem Th12: :: SIN_COS6:12 for r being real number for i being integer number st PI + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds sin r < 0 proofend; theorem Th13: :: SIN_COS6:13 for r being real number for i being integer number st (- (PI / 2)) + ((2 * PI) * i) < r & r < (PI / 2) + ((2 * PI) * i) holds cos r > 0 proofend; theorem Th14: :: SIN_COS6:14 for r being real number for i being integer number st (PI / 2) + ((2 * PI) * i) < r & r < ((3 / 2) * PI) + ((2 * PI) * i) holds cos r < 0 proofend; theorem Th15: :: SIN_COS6:15 for r being real number for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) < r & r < (2 * PI) + ((2 * PI) * i) holds cos r > 0 proofend; theorem :: SIN_COS6:16 for r being real number for i being integer number st (2 * PI) * i <= r & r <= PI + ((2 * PI) * i) holds sin r >= 0 proofend; theorem :: SIN_COS6:17 for r being real number for i being integer number st PI + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds sin r <= 0 proofend; theorem :: SIN_COS6:18 for r being real number for i being integer number st (- (PI / 2)) + ((2 * PI) * i) <= r & r <= (PI / 2) + ((2 * PI) * i) holds cos r >= 0 proofend; theorem :: SIN_COS6:19 for r being real number for i being integer number st (PI / 2) + ((2 * PI) * i) <= r & r <= ((3 / 2) * PI) + ((2 * PI) * i) holds cos r <= 0 proofend; theorem :: SIN_COS6:20 for r being real number for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) <= r & r <= (2 * PI) + ((2 * PI) * i) holds cos r >= 0 proofend; theorem Th21: :: SIN_COS6:21 for r being real number for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & sin r = 0 & not r = (2 * PI) * i holds r = PI + ((2 * PI) * i) proofend; theorem Th22: :: SIN_COS6:22 for r being real number for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & cos r = 0 & not r = (PI / 2) + ((2 * PI) * i) holds r = ((3 / 2) * PI) + ((2 * PI) * i) proofend; theorem Th23: :: SIN_COS6:23 for r being real number st sin r = - 1 holds r = ((3 / 2) * PI) + ((2 * PI) * [\(r / (2 * PI))/]) proofend; theorem Th24: :: SIN_COS6:24 for r being real number st sin r = 1 holds r = (PI / 2) + ((2 * PI) * [\(r / (2 * PI))/]) proofend; theorem Th25: :: SIN_COS6:25 for r being real number st cos r = - 1 holds r = PI + ((2 * PI) * [\(r / (2 * PI))/]) proofend; theorem Th26: :: SIN_COS6:26 for r being real number st cos r = 1 holds r = (2 * PI) * [\(r / (2 * PI))/] proofend; theorem Th27: :: SIN_COS6:27 for r being real number st 0 <= r & r <= 2 * PI & sin r = - 1 holds r = (3 / 2) * PI proofend; theorem Th28: :: SIN_COS6:28 for r being real number st 0 <= r & r <= 2 * PI & sin r = 1 holds r = PI / 2 proofend; :: case cos(r) = 1 has been proved as UNIROOTS:17, COMPTRIG:79 theorem Th29: :: SIN_COS6:29 for r being real number st 0 <= r & r <= 2 * PI & cos r = - 1 holds r = PI proofend; theorem Th30: :: SIN_COS6:30 for r being real number st 0 <= r & r < PI / 2 holds sin r < 1 proofend; theorem Th31: :: SIN_COS6:31 for r being real number st 0 <= r & r < (3 / 2) * PI holds sin r > - 1 proofend; theorem Th32: :: SIN_COS6:32 for r being real number st (3 / 2) * PI < r & r <= 2 * PI holds sin r > - 1 proofend; theorem Th33: :: SIN_COS6:33 for r being real number st PI / 2 < r & r <= 2 * PI holds sin r < 1 proofend; theorem Th34: :: SIN_COS6:34 for r being real number st 0 < r & r < 2 * PI holds cos r < 1 proofend; theorem Th35: :: SIN_COS6:35 for r being real number st 0 <= r & r < PI holds cos r > - 1 proofend; theorem Th36: :: SIN_COS6:36 for r being real number st PI < r & r <= 2 * PI holds cos r > - 1 proofend; theorem :: SIN_COS6:37 for r being real number for i being integer number st (2 * PI) * i <= r & r < (PI / 2) + ((2 * PI) * i) holds sin r < 1 proofend; theorem :: SIN_COS6:38 for r being real number for i being integer number st (2 * PI) * i <= r & r < ((3 / 2) * PI) + ((2 * PI) * i) holds sin r > - 1 proofend; theorem :: SIN_COS6:39 for r being real number for i being integer number st ((3 / 2) * PI) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds sin r > - 1 proofend; theorem :: SIN_COS6:40 for r being real number for i being integer number st (PI / 2) + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds sin r < 1 proofend; theorem :: SIN_COS6:41 for r being real number for i being integer number st (2 * PI) * i < r & r < (2 * PI) + ((2 * PI) * i) holds cos r < 1 proofend; theorem :: SIN_COS6:42 for r being real number for i being integer number st (2 * PI) * i <= r & r < PI + ((2 * PI) * i) holds cos r > - 1 proofend; theorem :: SIN_COS6:43 for r being real number for i being integer number st PI + ((2 * PI) * i) < r & r <= (2 * PI) + ((2 * PI) * i) holds cos r > - 1 proofend; theorem :: SIN_COS6:44 for r being real number st cos ((2 * PI) * r) = 1 holds r in INT proofend; theorem Th45: :: SIN_COS6:45 sin .: [.(- (PI / 2)),(PI / 2).] = [.(- 1),1.] by COMPTRIG:30, RELAT_1:115; theorem Th46: :: SIN_COS6:46 sin .: ].(- (PI / 2)),(PI / 2).[ = ].(- 1),1.[ proofend; theorem :: SIN_COS6:47 sin .: [.(PI / 2),((3 / 2) * PI).] = [.(- 1),1.] by COMPTRIG:31, RELAT_1:115; theorem :: SIN_COS6:48 sin .: ].(PI / 2),((3 / 2) * PI).[ = ].(- 1),1.[ proofend; theorem Th49: :: SIN_COS6:49 cos .: [.0,PI.] = [.(- 1),1.] by COMPTRIG:32, RELAT_1:115; theorem Th50: :: SIN_COS6:50 cos .: ].0,PI.[ = ].(- 1),1.[ proofend; theorem :: SIN_COS6:51 cos .: [.PI,(2 * PI).] = [.(- 1),1.] by COMPTRIG:33, RELAT_1:115; theorem :: SIN_COS6:52 cos .: ].PI,(2 * PI).[ = ].(- 1),1.[ proofend; Lm11: now__::_thesis:_for_i_being_integer_number_ for_r,_p1,_p2_being_real_number_st_r_in_[.(p1_+_H1(i)),(p2_+_H1(i)).]_holds_ r_+_(2_*_PI)_in_[.(p1_+_H1(i_+_1)),(p2_+_H1(i_+_1)).] let i be integer number ; ::_thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] let r be real number ; ::_thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] let p1, p2 be real number ; ::_thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] implies r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] ) assume A1: r in [.(p1 + H1(i)),(p2 + H1(i)).] ; ::_thesis: r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] then r <= p2 + H1(i) by XXREAL_1:1; then A2: r + (2 * PI) <= (p2 + H1(i)) + (2 * PI) by XREAL_1:6; p1 + H1(i) <= r by A1, XXREAL_1:1; then (p1 + H1(i)) + (2 * PI) <= r + (2 * PI) by XREAL_1:6; hence r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] by A2, XXREAL_1:1; ::_thesis: verum end; Lm12: now__::_thesis:_for_i_being_integer_number_ for_r,_p1,_p2_being_real_number_st_r_in_[.(p1_+_H1(i)),(p2_+_H1(i)).]_/\_REAL_holds_ r_+_(2_*_PI)_in_[.(p1_+_H1(i_+_1)),(p2_+_H1(i_+_1)).]_/\_REAL let i be integer number ; ::_thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL let r be real number ; ::_thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL let p1, p2 be real number ; ::_thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL implies r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL ) assume r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL ; ::_thesis: r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL then r in [.(p1 + H1(i)),(p2 + H1(i)).] by XBOOLE_0:def_4; then r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] by Lm11; hence r + (2 * PI) in [.(p1 + H1(i + 1)),(p2 + H1(i + 1)).] /\ REAL by XBOOLE_0:def_4; ::_thesis: verum end; Lm13: now__::_thesis:_for_i_being_integer_number_ for_r,_p1,_p2_being_real_number_st_r_in_[.(p1_+_H1(i)),(p2_+_H1(i)).]_holds_ r_-_(2_*_PI)_in_[.(p1_+_H1(i_-_1)),(p2_+_H1(i_-_1)).] let i be integer number ; ::_thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] let r be real number ; ::_thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] holds r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] let p1, p2 be real number ; ::_thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] implies r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] ) assume A1: r in [.(p1 + H1(i)),(p2 + H1(i)).] ; ::_thesis: r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] then r <= p2 + H1(i) by XXREAL_1:1; then A2: r - (2 * PI) <= (p2 + H1(i)) - (2 * PI) by XREAL_1:9; p1 + H1(i) <= r by A1, XXREAL_1:1; then (p1 + H1(i)) - (2 * PI) <= r - (2 * PI) by XREAL_1:9; hence r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] by A2, XXREAL_1:1; ::_thesis: verum end; Lm14: now__::_thesis:_for_i_being_integer_number_ for_r,_p1,_p2_being_real_number_st_r_in_[.(p1_+_H1(i)),(p2_+_H1(i)).]_/\_REAL_holds_ r_-_(2_*_PI)_in_[.(p1_+_H1(i_-_1)),(p2_+_H1(i_-_1)).]_/\_REAL let i be integer number ; ::_thesis: for r, p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL let r be real number ; ::_thesis: for p1, p2 being real number st r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL holds r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL let p1, p2 be real number ; ::_thesis: ( r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL implies r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL ) assume r in [.(p1 + H1(i)),(p2 + H1(i)).] /\ REAL ; ::_thesis: r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL then r in [.(p1 + H1(i)),(p2 + H1(i)).] by XBOOLE_0:def_4; then r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] by Lm13; hence r - (2 * PI) in [.(p1 + H1(i - 1)),(p2 + H1(i - 1)).] /\ REAL by XBOOLE_0:def_4; ::_thesis: verum end; theorem Th53: :: SIN_COS6:53 for i being integer number holds sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is increasing proofend; theorem Th54: :: SIN_COS6:54 for i being integer number holds sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is decreasing proofend; theorem Th55: :: SIN_COS6:55 for i being integer number holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is decreasing proofend; theorem Th56: :: SIN_COS6:56 for i being integer number holds cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is increasing proofend; theorem Th57: :: SIN_COS6:57 for i being integer number holds sin | [.((- (PI / 2)) + ((2 * PI) * i)),((PI / 2) + ((2 * PI) * i)).] is one-to-one proofend; theorem Th58: :: SIN_COS6:58 for i being integer number holds sin | [.((PI / 2) + ((2 * PI) * i)),(((3 / 2) * PI) + ((2 * PI) * i)).] is one-to-one proofend; registration clustersin | [.(- (PI / 2)),(PI / 2).] -> one-to-one ; coherence sin | [.(- (PI / 2)),(PI / 2).] is one-to-one by Lm1, Th57; clustersin | [.(PI / 2),((3 / 2) * PI).] -> one-to-one ; coherence sin | [.(PI / 2),((3 / 2) * PI).] is one-to-one by Lm2, Th58; end; registration clustersin | [.(- (PI / 2)),0.] -> one-to-one ; coherence sin | [.(- (PI / 2)),0.] is one-to-one proofend; clustersin | [.0,(PI / 2).] -> one-to-one ; coherence sin | [.0,(PI / 2).] is one-to-one proofend; clustersin | [.(PI / 2),PI.] -> one-to-one ; coherence sin | [.(PI / 2),PI.] is one-to-one proofend; clustersin | [.PI,((3 / 2) * PI).] -> one-to-one ; coherence sin | [.PI,((3 / 2) * PI).] is one-to-one proofend; clustersin | [.((3 / 2) * PI),(2 * PI).] -> one-to-one ; coherence sin | [.((3 / 2) * PI),(2 * PI).] is one-to-one proofend; end; registration clustersin | ].(- (PI / 2)),(PI / 2).[ -> one-to-one ; coherence sin | ].(- (PI / 2)),(PI / 2).[ is one-to-one proofend; clustersin | ].(PI / 2),((3 / 2) * PI).[ -> one-to-one ; coherence sin | ].(PI / 2),((3 / 2) * PI).[ is one-to-one proofend; clustersin | ].(- (PI / 2)),0.[ -> one-to-one ; coherence sin | ].(- (PI / 2)),0.[ is one-to-one proofend; clustersin | ].0,(PI / 2).[ -> one-to-one ; coherence sin | ].0,(PI / 2).[ is one-to-one proofend; clustersin | ].(PI / 2),PI.[ -> one-to-one ; coherence sin | ].(PI / 2),PI.[ is one-to-one proofend; clustersin | ].PI,((3 / 2) * PI).[ -> one-to-one ; coherence sin | ].PI,((3 / 2) * PI).[ is one-to-one proofend; clustersin | ].((3 / 2) * PI),(2 * PI).[ -> one-to-one ; coherence sin | ].((3 / 2) * PI),(2 * PI).[ is one-to-one proofend; end; theorem Th59: :: SIN_COS6:59 for i being integer number holds cos | [.((2 * PI) * i),(PI + ((2 * PI) * i)).] is one-to-one proofend; theorem Th60: :: SIN_COS6:60 for i being integer number holds cos | [.(PI + ((2 * PI) * i)),((2 * PI) + ((2 * PI) * i)).] is one-to-one proofend; registration clustercos | [.0,PI.] -> one-to-one ; coherence cos | [.0,PI.] is one-to-one by Lm3, Th59; clustercos | [.PI,(2 * PI).] -> one-to-one ; coherence cos | [.PI,(2 * PI).] is one-to-one by Lm4, Th60; end; registration clustercos | [.0,(PI / 2).] -> one-to-one ; coherence cos | [.0,(PI / 2).] is one-to-one proofend; clustercos | [.(PI / 2),PI.] -> one-to-one ; coherence cos | [.(PI / 2),PI.] is one-to-one proofend; clustercos | [.PI,((3 / 2) * PI).] -> one-to-one ; coherence cos | [.PI,((3 / 2) * PI).] is one-to-one proofend; clustercos | [.((3 / 2) * PI),(2 * PI).] -> one-to-one ; coherence cos | [.((3 / 2) * PI),(2 * PI).] is one-to-one proofend; end; registration clustercos | ].0,PI.[ -> one-to-one ; coherence cos | ].0,PI.[ is one-to-one proofend; clustercos | ].PI,(2 * PI).[ -> one-to-one ; coherence cos | ].PI,(2 * PI).[ is one-to-one proofend; clustercos | ].0,(PI / 2).[ -> one-to-one ; coherence cos | ].0,(PI / 2).[ is one-to-one proofend; clustercos | ].(PI / 2),PI.[ -> one-to-one ; coherence cos | ].(PI / 2),PI.[ is one-to-one proofend; clustercos | ].PI,((3 / 2) * PI).[ -> one-to-one ; coherence cos | ].PI,((3 / 2) * PI).[ is one-to-one proofend; clustercos | ].((3 / 2) * PI),(2 * PI).[ -> one-to-one ; coherence cos | ].((3 / 2) * PI),(2 * PI).[ is one-to-one proofend; end; theorem :: SIN_COS6:61 for r, s being real number for i being integer number st (2 * PI) * i <= r & r < (2 * PI) + ((2 * PI) * i) & (2 * PI) * i <= s & s < (2 * PI) + ((2 * PI) * i) & sin r = sin s & cos r = cos s holds r = s proofend; begin definition func arcsin -> PartFunc of REAL,REAL equals :: SIN_COS6:def 1 (sin | [.(- (PI / 2)),(PI / 2).]) " ; coherence (sin | [.(- (PI / 2)),(PI / 2).]) " is PartFunc of REAL,REAL ; end; :: deftheorem defines arcsin SIN_COS6:def_1_:_ arcsin = (sin | [.(- (PI / 2)),(PI / 2).]) " ; definition let r be set ; func arcsin r -> set equals :: SIN_COS6:def 2 arcsin . r; coherence arcsin . r is set ; end; :: deftheorem defines arcsin SIN_COS6:def_2_:_ for r being set holds arcsin r = arcsin . r; definition let r be set ; :: original:arcsin redefine func arcsin r -> Real; coherence arcsin r is Real ; end; Lm15: arcsin " = sin | [.(- (PI / 2)),(PI / 2).] by FUNCT_1:43; theorem Th62: :: SIN_COS6:62 rng arcsin = [.(- (PI / 2)),(PI / 2).] proofend; registration cluster arcsin -> one-to-one ; coherence arcsin is one-to-one ; end; theorem Th63: :: SIN_COS6:63 dom arcsin = [.(- 1),1.] by COMPTRIG:30, FUNCT_1:33; theorem Th64: :: SIN_COS6:64 (sin | [.(- (PI / 2)),(PI / 2).]) * arcsin = id [.(- 1),1.] by COMPTRIG:30, FUNCT_1:39; theorem :: SIN_COS6:65 arcsin * (sin | [.(- (PI / 2)),(PI / 2).]) = id [.(- 1),1.] by COMPTRIG:30, FUNCT_1:39; theorem Th66: :: SIN_COS6:66 (sin | [.(- (PI / 2)),(PI / 2).]) * arcsin = id [.(- (PI / 2)),(PI / 2).] by Lm15, Th62, FUNCT_1:39; theorem :: SIN_COS6:67 arcsin * (sin | [.(- (PI / 2)),(PI / 2).]) = id [.(- (PI / 2)),(PI / 2).] by Lm15, Th62, FUNCT_1:39; theorem Th68: :: SIN_COS6:68 for r being real number st - 1 <= r & r <= 1 holds sin (arcsin r) = r proofend; theorem Th69: :: SIN_COS6:69 for r being real number st - (PI / 2) <= r & r <= PI / 2 holds arcsin (sin r) = r proofend; theorem :: SIN_COS6:70 arcsin (- 1) = - (PI / 2) by Th7, Th69; theorem :: SIN_COS6:71 arcsin 0 = 0 by Th69, SIN_COS:31; theorem :: SIN_COS6:72 arcsin 1 = PI / 2 by Th69, SIN_COS:77; theorem :: SIN_COS6:73 for r being real number st - 1 <= r & r <= 1 & arcsin r = - (PI / 2) holds r = - 1 by Th7, Th68; theorem :: SIN_COS6:74 for r being real number st - 1 <= r & r <= 1 & arcsin r = 0 holds r = 0 by Th68, SIN_COS:31; theorem :: SIN_COS6:75 for r being real number st - 1 <= r & r <= 1 & arcsin r = PI / 2 holds r = 1 by Th68, SIN_COS:77; theorem Th76: :: SIN_COS6:76 for r being real number st - 1 <= r & r <= 1 holds ( - (PI / 2) <= arcsin r & arcsin r <= PI / 2 ) proofend; theorem Th77: :: SIN_COS6:77 for r being real number st - 1 < r & r < 1 holds ( - (PI / 2) < arcsin r & arcsin r < PI / 2 ) proofend; theorem Th78: :: SIN_COS6:78 for r being real number st - 1 <= r & r <= 1 holds arcsin r = - (arcsin (- r)) proofend; theorem Th79: :: SIN_COS6:79 for s, r being real number st 0 <= s & (r ^2) + (s ^2) = 1 holds cos (arcsin r) = s proofend; theorem :: SIN_COS6:80 for s, r being real number st s <= 0 & (r ^2) + (s ^2) = 1 holds cos (arcsin r) = - s proofend; theorem Th81: :: SIN_COS6:81 for r being real number st - 1 <= r & r <= 1 holds cos (arcsin r) = sqrt (1 - (r ^2)) proofend; theorem :: SIN_COS6:82 arcsin | [.(- 1),1.] is increasing proofend; theorem :: SIN_COS6:83 for r being real number holds ( arcsin is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arcsin,r) = 1 / (sqrt (1 - (r ^2))) ) ) proofend; theorem :: SIN_COS6:84 arcsin | [.(- 1),1.] is continuous proofend; begin definition func arccos -> PartFunc of REAL,REAL equals :: SIN_COS6:def 3 (cos | [.0,PI.]) " ; coherence (cos | [.0,PI.]) " is PartFunc of REAL,REAL ; end; :: deftheorem defines arccos SIN_COS6:def_3_:_ arccos = (cos | [.0,PI.]) " ; definition let r be set ; func arccos r -> set equals :: SIN_COS6:def 4 arccos . r; coherence arccos . r is set ; end; :: deftheorem defines arccos SIN_COS6:def_4_:_ for r being set holds arccos r = arccos . r; definition let r be set ; :: original:arccos redefine func arccos r -> Real; coherence arccos r is Real ; end; Lm16: arccos " = cos | [.0,PI.] by FUNCT_1:43; theorem Th85: :: SIN_COS6:85 rng arccos = [.0,PI.] proofend; registration cluster arccos -> one-to-one ; coherence arccos is one-to-one ; end; theorem Th86: :: SIN_COS6:86 dom arccos = [.(- 1),1.] by COMPTRIG:32, FUNCT_1:33; theorem Th87: :: SIN_COS6:87 (cos | [.0,PI.]) * arccos = id [.(- 1),1.] by COMPTRIG:32, FUNCT_1:39; theorem :: SIN_COS6:88 arccos * (cos | [.0,PI.]) = id [.(- 1),1.] by COMPTRIG:32, FUNCT_1:39; theorem Th89: :: SIN_COS6:89 (cos | [.0,PI.]) * arccos = id [.0,PI.] by Lm16, Th85, FUNCT_1:39; theorem :: SIN_COS6:90 arccos * (cos | [.0,PI.]) = id [.0,PI.] by Lm16, Th85, FUNCT_1:39; theorem Th91: :: SIN_COS6:91 for r being real number st - 1 <= r & r <= 1 holds cos (arccos r) = r proofend; theorem Th92: :: SIN_COS6:92 for r being real number st 0 <= r & r <= PI holds arccos (cos r) = r proofend; theorem :: SIN_COS6:93 arccos (- 1) = PI by Th92, SIN_COS:77; theorem :: SIN_COS6:94 arccos 0 = PI / 2 by Lm6, Th92, SIN_COS:77; theorem :: SIN_COS6:95 arccos 1 = 0 by Th92, SIN_COS:31; theorem :: SIN_COS6:96 for r being real number st - 1 <= r & r <= 1 & arccos r = 0 holds r = 1 by Th91, SIN_COS:31; theorem :: SIN_COS6:97 for r being real number st - 1 <= r & r <= 1 & arccos r = PI / 2 holds r = 0 by Th91, SIN_COS:77; theorem :: SIN_COS6:98 for r being real number st - 1 <= r & r <= 1 & arccos r = PI holds r = - 1 by Th91, SIN_COS:77; theorem Th99: :: SIN_COS6:99 for r being real number st - 1 <= r & r <= 1 holds ( 0 <= arccos r & arccos r <= PI ) proofend; theorem Th100: :: SIN_COS6:100 for r being real number st - 1 < r & r < 1 holds ( 0 < arccos r & arccos r < PI ) proofend; theorem Th101: :: SIN_COS6:101 for r being real number st - 1 <= r & r <= 1 holds arccos r = PI - (arccos (- r)) proofend; theorem Th102: :: SIN_COS6:102 for s, r being real number st 0 <= s & (r ^2) + (s ^2) = 1 holds sin (arccos r) = s proofend; theorem :: SIN_COS6:103 for s, r being real number st s <= 0 & (r ^2) + (s ^2) = 1 holds sin (arccos r) = - s proofend; theorem Th104: :: SIN_COS6:104 for r being real number st - 1 <= r & r <= 1 holds sin (arccos r) = sqrt (1 - (r ^2)) proofend; theorem :: SIN_COS6:105 arccos | [.(- 1),1.] is decreasing proofend; theorem :: SIN_COS6:106 for r being real number holds ( arccos is_differentiable_on ].(- 1),1.[ & ( - 1 < r & r < 1 implies diff (arccos,r) = - (1 / (sqrt (1 - (r ^2)))) ) ) proofend; theorem :: SIN_COS6:107 arccos | [.(- 1),1.] is continuous proofend; :: Correspondence between arcsin and arccos theorem Th108: :: SIN_COS6:108 for r being real number st - 1 <= r & r <= 1 holds (arcsin r) + (arccos r) = PI / 2 proofend; theorem :: SIN_COS6:109 for r being real number st - 1 <= r & r <= 1 holds (arccos (- r)) - (arcsin r) = PI / 2 proofend; theorem :: SIN_COS6:110 for r being real number st - 1 <= r & r <= 1 holds (arccos r) - (arcsin (- r)) = PI / 2 proofend;