:: Inverse Trigonometric Functions Arcsin and Arccos :: by Artur Korni{\l}owicz and Yasunari Shidama :: :: Received September 25, 2004 :: Copyright (c) 2004-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies NUMBERS, XREAL_0, INT_1, CARD_1, XXREAL_0, ARYTM_3, ARYTM_1, FUNCT_1, RELAT_1, TARSKI, XBOOLE_0, SIN_COS, XXREAL_1, SQUARE_1, REAL_1, ORDINAL2, VALUED_0, PARTFUN1, FDIFF_1, SIN_COS6, ORDINAL1; notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, INT_1, SQUARE_1, RCOMP_1, RELAT_1, FUNCT_1, PARTFUN1, RELSET_1, PARTFUN2, RFUNCT_2, FCONT_1, FDIFF_1, SIN_COS; constructors PARTFUN1, ARYTM_0, REAL_1, SQUARE_1, RCOMP_1, PARTFUN2, RFUNCT_2, FCONT_1, FDIFF_1, COMSEQ_3, SIN_COS, RVSUM_1, RELSET_1; registrations FUNCT_1, RELSET_1, XCMPLX_0, XXREAL_0, XREAL_0, SQUARE_1, INT_1, RCOMP_1, RFUNCT_2, SIN_COS, VALUED_0, ORDINAL1; requirements SUBSET, NUMERALS, ARITHM, REAL; begin :: Preliminaries reserve r,r1,r2, s,x for Real, i for Integer; theorem :: SIN_COS6:1 0 <= r & r < s implies [\ r/s /] = 0; theorem :: SIN_COS6:2 for f being Function, X, Y being set st f|X is one-to-one & Y c= X holds f|Y is one-to-one; begin :: sine and cosine theorem :: SIN_COS6:3 -1 <= sin r; theorem :: SIN_COS6:4 sin r <= 1; theorem :: SIN_COS6:5 -1 <= cos r; theorem :: SIN_COS6:6 cos r <= 1; registration cluster PI -> positive; end; theorem :: SIN_COS6:7 sin(-PI/2) = -1 & sin.-PI/2 = -1; theorem :: SIN_COS6:8 sin.r = sin.(r+2*PI*i); theorem :: SIN_COS6:9 cos(-PI/2) = 0 & cos.-PI/2 = 0; theorem :: SIN_COS6:10 cos.r = cos.(r+2*PI*i); theorem :: SIN_COS6:11 2*PI*i < r & r < PI+2*PI*i implies sin r > 0; theorem :: SIN_COS6:12 PI+2*PI*i < r & r < 2*PI+2*PI*i implies sin r < 0; theorem :: SIN_COS6:13 -PI/2+2*PI*i < r & r < PI/2+2*PI*i implies cos r > 0; theorem :: SIN_COS6:14 PI/2+2*PI*i < r & r < 3/2*PI+2*PI*i implies cos r < 0; theorem :: SIN_COS6:15 3/2*PI+2*PI*i < r & r < 2*PI+2*PI*i implies cos r > 0; theorem :: SIN_COS6:16 2*PI*i <= r & r <= PI+2*PI*i implies sin r >= 0; theorem :: SIN_COS6:17 PI+2*PI*i <= r & r <= 2*PI+2*PI*i implies sin r <= 0; theorem :: SIN_COS6:18 -PI/2+2*PI*i <= r & r <= PI/2+2*PI*i implies cos r >= 0; theorem :: SIN_COS6:19 PI/2+2*PI*i <= r & r <= 3/2*PI+2*PI*i implies cos r <= 0; theorem :: SIN_COS6:20 3/2*PI+2*PI*i <= r & r <= 2*PI+2*PI*i implies cos r >= 0; theorem :: SIN_COS6:21 2*PI*i <= r & r < 2*PI+2*PI*i & sin r = 0 implies r = 2*PI*i or r = PI+2*PI*i ; theorem :: SIN_COS6:22 2*PI*i <= r & r < 2*PI+2*PI*i & cos r = 0 implies r = PI/2+2*PI* i or r = 3/2*PI+2*PI*i; theorem :: SIN_COS6:23 sin r = -1 implies r = 3/2*PI + 2*PI*[\r/(2*PI)/]; theorem :: SIN_COS6:24 sin r = 1 implies r = PI/2 + 2*PI*[\r/(2*PI)/]; theorem :: SIN_COS6:25 cos r = -1 implies r = PI + 2*PI*[\r/(2*PI)/]; theorem :: SIN_COS6:26 cos r = 1 implies r = 2*PI*[\r/(2*PI)/]; theorem :: SIN_COS6:27 0 <= r & r <= 2*PI & sin r = -1 implies r = 3/2*PI; theorem :: SIN_COS6:28 0 <= r & r <= 2*PI & sin r = 1 implies r = PI/2; :: case cos(r) = 1 has been proved as UNIROOTS:17, COMPTRIG:79 theorem :: SIN_COS6:29 0 <= r & r <= 2*PI & cos r = -1 implies r = PI; theorem :: SIN_COS6:30 0 <= r & r < PI/2 implies sin r < 1; theorem :: SIN_COS6:31 0 <= r & r < 3/2*PI implies sin r > -1; theorem :: SIN_COS6:32 3/2*PI < r & r <= 2*PI implies sin r > -1; theorem :: SIN_COS6:33 PI/2 < r & r <= 2*PI implies sin r < 1; theorem :: SIN_COS6:34 0 < r & r < 2*PI implies cos r < 1; theorem :: SIN_COS6:35 0 <= r & r < PI implies cos r > -1; theorem :: SIN_COS6:36 PI < r & r <= 2*PI implies cos r > -1; theorem :: SIN_COS6:37 2*PI*i <= r & r < PI/2+2*PI*i implies sin r < 1; theorem :: SIN_COS6:38 2*PI*i <= r & r < 3/2*PI+2*PI*i implies sin r > -1; theorem :: SIN_COS6:39 3/2*PI+2*PI*i < r & r <= 2*PI+2*PI*i implies sin r > -1; theorem :: SIN_COS6:40 PI/2+2*PI*i < r & r <= 2*PI+2*PI*i implies sin r < 1; theorem :: SIN_COS6:41 2*PI*i < r & r < 2*PI+2*PI*i implies cos r < 1; theorem :: SIN_COS6:42 2*PI*i <= r & r < PI+2*PI*i implies cos r > -1; theorem :: SIN_COS6:43 PI+2*PI*i < r & r <= 2*PI+2*PI*i implies cos r > -1; theorem :: SIN_COS6:44 cos(2*PI*r) = 1 implies r in INT; theorem :: SIN_COS6:45 sin.:[.-PI/2,PI/2.] = [.-1,1.]; theorem :: SIN_COS6:46 sin.:].-PI/2,PI/2.[ = ].-1,1.[; theorem :: SIN_COS6:47 sin.:[.PI/2,3/2*PI.] = [.-1,1.]; theorem :: SIN_COS6:48 sin.:].PI/2,3/2*PI.[ = ].-1,1.[; theorem :: SIN_COS6:49 cos.:[.0,PI.] = [.-1,1.]; theorem :: SIN_COS6:50 cos.:].0,PI.[ = ].-1,1.[; theorem :: SIN_COS6:51 cos.:[.PI,2*PI.] = [.-1,1.]; theorem :: SIN_COS6:52 cos.:].PI,2*PI.[ = ].-1,1.[; theorem :: SIN_COS6:53 sin|[.-PI/2+2*PI*i,PI/2+2*PI*i.] is increasing; theorem :: SIN_COS6:54 sin|[.PI/2+2*PI*i,3/2*PI+2*PI*i.] is decreasing; theorem :: SIN_COS6:55 cos|[.2*PI*i,PI+2*PI*i.] is decreasing; theorem :: SIN_COS6:56 cos|[.PI+2*PI*i,2*PI+2*PI*i.] is increasing; theorem :: SIN_COS6:57 sin | [.-PI/2+2*PI*i,PI/2+2*PI*i.] is one-to-one; theorem :: SIN_COS6:58 sin | [.PI/2+2*PI*i,3/2*PI+2*PI*i.] is one-to-one; registration cluster sin | [.-PI/2,PI/2.] -> one-to-one; cluster sin | [.PI/2,3/2*PI.] -> one-to-one; end; registration cluster sin | [.-PI/2,0 .] -> one-to-one; cluster sin | [.0,PI/2.] -> one-to-one; cluster sin | [.PI/2,PI.] -> one-to-one; cluster sin | [.PI,3/2*PI.] -> one-to-one; cluster sin | [.3/2*PI,2*PI.] -> one-to-one; end; registration cluster sin | ].-PI/2,PI/2.[ -> one-to-one; cluster sin | ].PI/2,3/2*PI.[ -> one-to-one; cluster sin | ].-PI/2,0 .[ -> one-to-one; cluster sin | ].0,PI/2.[ -> one-to-one; cluster sin | ].PI/2,PI.[ -> one-to-one; cluster sin | ].PI,3/2*PI.[ -> one-to-one; cluster sin | ].3/2*PI,2*PI.[ -> one-to-one; end; theorem :: SIN_COS6:59 cos | [.2*PI*i,PI+2*PI*i.] is one-to-one; theorem :: SIN_COS6:60 cos | [.PI+2*PI*i,2*PI+2*PI*i.] is one-to-one; registration cluster cos | [.0,PI.] -> one-to-one; cluster cos | [.PI,2*PI.] -> one-to-one; end; registration cluster cos | [.0,PI/2.] -> one-to-one; cluster cos | [.PI/2,PI.] -> one-to-one; cluster cos | [.PI,3/2*PI.] -> one-to-one; cluster cos | [.3/2*PI,2*PI.] -> one-to-one; end; registration cluster cos | ].0,PI.[ -> one-to-one; cluster cos | ].PI,2*PI.[ -> one-to-one; cluster cos | ].0,PI/2.[ -> one-to-one; cluster cos | ].PI/2,PI.[ -> one-to-one; cluster cos | ].PI,3/2*PI.[ -> one-to-one; cluster cos | ].3/2*PI,2*PI.[ -> one-to-one; end; theorem :: SIN_COS6:61 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 implies r = s; begin :: arcsin definition func arcsin -> PartFunc of REAL, REAL equals :: SIN_COS6:def 1 (sin | [.-PI/2,PI/2.])"; end; definition let r be object; func arcsin r -> number equals :: SIN_COS6:def 2 arcsin.r; end; registration let r be object; cluster arcsin r -> real; end; theorem :: SIN_COS6:62 rng arcsin = [.-PI/2,PI/2.]; registration cluster arcsin -> one-to-one; end; theorem :: SIN_COS6:63 dom arcsin = [.-1,1.]; theorem :: SIN_COS6:64 (sin | [.-PI/2,PI/2.]) qua Function * arcsin = id [.-1,1.]; theorem :: SIN_COS6:65 arcsin * (sin | [.-PI/2,PI/2.]) = id [.-1,1.]; theorem :: SIN_COS6:66 (sin | [.-PI/2,PI/2.]) * arcsin = id [.-PI/2,PI/2.]; theorem :: SIN_COS6:67 arcsin qua Function * (sin | [.-PI/2,PI/2.]) = id [.-PI/2,PI/2.]; theorem :: SIN_COS6:68 -1 <= r & r <= 1 implies sin arcsin r = r; theorem :: SIN_COS6:69 -PI/2 <= r & r <= PI/2 implies arcsin sin r = r; theorem :: SIN_COS6:70 arcsin (-1) = -PI/2; theorem :: SIN_COS6:71 arcsin 0 = 0; theorem :: SIN_COS6:72 arcsin 1 = PI/2; theorem :: SIN_COS6:73 -1 <= r & r <= 1 & arcsin r = -PI/2 implies r = -1; theorem :: SIN_COS6:74 -1 <= r & r <= 1 & arcsin r = 0 implies r = 0; theorem :: SIN_COS6:75 -1 <= r & r <= 1 & arcsin r = PI/2 implies r = 1; theorem :: SIN_COS6:76 -1 <= r & r <= 1 implies -PI/2 <= arcsin r & arcsin r <= PI/2; theorem :: SIN_COS6:77 -1 < r & r < 1 implies -PI/2 < arcsin r & arcsin r < PI/2; theorem :: SIN_COS6:78 -1 <= r & r <= 1 implies arcsin r = -arcsin(-r); theorem :: SIN_COS6:79 0 <= s & r^2 + s^2 = 1 implies cos arcsin r = s; theorem :: SIN_COS6:80 s <= 0 & r^2 + s^2 = 1 implies cos arcsin r = -s; theorem :: SIN_COS6:81 -1 <= r & r <= 1 implies cos arcsin r = sqrt(1-r^2); theorem :: SIN_COS6:82 arcsin|[.-1,1.] is increasing; theorem :: SIN_COS6:83 arcsin is_differentiable_on ].-1,1.[ & (-1 < r & r < 1 implies diff( arcsin,r) = 1 / sqrt(1-r^2)); theorem :: SIN_COS6:84 arcsin|[.-1,1.] is continuous; begin :: arccos definition func arccos -> PartFunc of REAL, REAL equals :: SIN_COS6:def 3 (cos | [.0,PI.])"; end; definition let r be object; func arccos r -> number equals :: SIN_COS6:def 4 arccos.r; end; registration let r be object; cluster arccos r -> real; end; theorem :: SIN_COS6:85 rng arccos = [.0,PI.]; registration cluster arccos -> one-to-one; end; theorem :: SIN_COS6:86 dom arccos = [.-1,1.]; theorem :: SIN_COS6:87 (cos | [.0,PI.]) qua Function * arccos = id [.-1,1.]; theorem :: SIN_COS6:88 arccos * (cos | [.0,PI.]) = id [.-1,1.]; theorem :: SIN_COS6:89 (cos | [.0,PI.]) * arccos = id [.0,PI.]; theorem :: SIN_COS6:90 arccos qua Function * (cos | [.0,PI.]) = id [.0,PI.]; theorem :: SIN_COS6:91 -1 <= r & r <= 1 implies cos arccos r = r; theorem :: SIN_COS6:92 0 <= r & r <= PI implies arccos cos r = r; theorem :: SIN_COS6:93 arccos (-1) = PI; theorem :: SIN_COS6:94 arccos 0 = PI/2; theorem :: SIN_COS6:95 arccos 1 = 0; theorem :: SIN_COS6:96 -1 <= r & r <= 1 & arccos r = 0 implies r = 1; theorem :: SIN_COS6:97 -1 <= r & r <= 1 & arccos r = PI/2 implies r = 0; theorem :: SIN_COS6:98 -1 <= r & r <= 1 & arccos r = PI implies r = -1; theorem :: SIN_COS6:99 -1 <= r & r <= 1 implies 0 <= arccos r & arccos r <= PI; theorem :: SIN_COS6:100 -1 < r & r < 1 implies 0 < arccos r & arccos r < PI; theorem :: SIN_COS6:101 -1 <= r & r <= 1 implies arccos r = PI - arccos(-r); theorem :: SIN_COS6:102 0 <= s & r^2 + s^2 = 1 implies sin arccos r = s; theorem :: SIN_COS6:103 s <= 0 & r^2 + s^2 = 1 implies sin arccos r = -s; theorem :: SIN_COS6:104 -1 <= r & r <= 1 implies sin arccos r = sqrt(1-r^2); theorem :: SIN_COS6:105 arccos|[.-1,1.] is decreasing; theorem :: SIN_COS6:106 arccos is_differentiable_on ].-1,1.[ & (-1 < r & r < 1 implies diff( arccos,r) = -1 / sqrt(1-r^2)); theorem :: SIN_COS6:107 arccos|[.-1,1.] is continuous; :: Correspondence between arcsin and arccos theorem :: SIN_COS6:108 -1 <= r & r <= 1 implies arcsin r + arccos r = PI/2; theorem :: SIN_COS6:109 -1 <= r & r <= 1 implies arccos(-r) - arcsin r = PI/2; theorem :: SIN_COS6:110 -1 <= r & r <= 1 implies arccos r - arcsin(-r) = PI/2;