:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2 :: by Bing Xie , Xiquan Liang and Fuguo Ge :: :: Received March 18, 2008 :: Copyright (c) 2008-2012 Association of Mizar Users begin Lm1: [.0,(PI / 2).[ c= ].(- (PI / 2)),(PI / 2).[ proofend; theorem Th1: :: SINCOS10:1 [.0,(PI / 2).[ c= dom sec proofend; Lm2: ].(PI / 2),PI.] c= ].(PI / 2),((3 / 2) * PI).[ proofend; theorem Th2: :: SINCOS10:2 ].(PI / 2),PI.] c= dom sec proofend; Lm3: [.(- (PI / 2)),0.[ c= ].(- PI),0.[ proofend; theorem Th3: :: SINCOS10:3 [.(- (PI / 2)),0.[ c= dom cosec proofend; Lm4: ].0,(PI / 2).] c= ].0,PI.[ proofend; theorem Th4: :: SINCOS10:4 ].0,(PI / 2).] c= dom cosec proofend; theorem Th5: :: SINCOS10:5 ( sec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds diff (sec,x) = (sin . x) / ((cos . x) ^2) ) ) proofend; theorem Th6: :: SINCOS10:6 ( sec is_differentiable_on ].(PI / 2),PI.[ & ( for x being Real st x in ].(PI / 2),PI.[ holds diff (sec,x) = (sin . x) / ((cos . x) ^2) ) ) proofend; theorem Th7: :: SINCOS10:7 ( cosec is_differentiable_on ].(- (PI / 2)),0.[ & ( for x being Real st x in ].(- (PI / 2)),0.[ holds diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) ) proofend; theorem Th8: :: SINCOS10:8 ( cosec is_differentiable_on ].0,(PI / 2).[ & ( for x being Real st x in ].0,(PI / 2).[ holds diff (cosec,x) = - ((cos . x) / ((sin . x) ^2)) ) ) proofend; theorem :: SINCOS10:9 sec | ].0,(PI / 2).[ is continuous by Th5, FDIFF_1:25; theorem :: SINCOS10:10 sec | ].(PI / 2),PI.[ is continuous by Th6, FDIFF_1:25; theorem :: SINCOS10:11 cosec | ].(- (PI / 2)),0.[ is continuous by Th7, FDIFF_1:25; theorem :: SINCOS10:12 cosec | ].0,(PI / 2).[ is continuous by Th8, FDIFF_1:25; Lm5: ( 0 in [.0,(PI / 2).[ & PI / 4 in [.0,(PI / 2).[ ) proofend; Lm6: ( (3 / 4) * PI in ].(PI / 2),PI.] & PI in ].(PI / 2),PI.] ) proofend; Lm7: ( - (PI / 2) in [.(- (PI / 2)),0.[ & - (PI / 4) in [.(- (PI / 2)),0.[ ) proofend; Lm8: ( PI / 4 in ].0,(PI / 2).] & PI / 2 in ].0,(PI / 2).] ) proofend; Lm9: ].0,(PI / 2).[ c= [.0,(PI / 2).[ by XXREAL_1:22; then Lm10: ].0,(PI / 2).[ c= dom sec by Th1, XBOOLE_1:1; Lm11: ].(PI / 2),PI.[ c= ].(PI / 2),PI.] by XXREAL_1:21; then Lm12: ].(PI / 2),PI.[ c= dom sec by Th2, XBOOLE_1:1; Lm13: [.0,(PI / 4).] c= [.0,(PI / 2).[ by Lm5, XXREAL_2:def_12; Lm14: [.((3 / 4) * PI),PI.] c= ].(PI / 2),PI.] by Lm6, XXREAL_2:def_12; Lm15: ].(- (PI / 2)),0.[ c= [.(- (PI / 2)),0.[ by XXREAL_1:22; then Lm16: ].(- (PI / 2)),0.[ c= dom cosec by Th3, XBOOLE_1:1; Lm17: ].0,(PI / 2).[ c= ].0,(PI / 2).] by XXREAL_1:21; then Lm18: ].0,(PI / 2).[ c= dom cosec by Th4, XBOOLE_1:1; Lm19: [.(- (PI / 2)),(- (PI / 4)).] c= [.(- (PI / 2)),0.[ by Lm7, XXREAL_2:def_12; Lm20: [.(PI / 4),(PI / 2).] c= ].0,(PI / 2).] by Lm8, XXREAL_2:def_12; ].0,(PI / 2).[ = dom (sec | ].0,(PI / 2).[) by Lm9, Th1, RELAT_1:62, XBOOLE_1:1; then Lm21: ].0,(PI / 2).[ c= dom ((sec | [.0,(PI / 2).[) | ].0,(PI / 2).[) by RELAT_1:74, XXREAL_1:22; ].(PI / 2),PI.[ = dom (sec | ].(PI / 2),PI.[) by Lm11, Th2, RELAT_1:62, XBOOLE_1:1; then Lm22: ].(PI / 2),PI.[ c= dom ((sec | ].(PI / 2),PI.]) | ].(PI / 2),PI.[) by RELAT_1:74, XXREAL_1:21; ].(- (PI / 2)),0.[ = dom (cosec | ].(- (PI / 2)),0.[) by Lm15, Th3, RELAT_1:62, XBOOLE_1:1; then Lm23: ].(- (PI / 2)),0.[ c= dom ((cosec | [.(- (PI / 2)),0.[) | ].(- (PI / 2)),0.[) by RELAT_1:74, XXREAL_1:22; ].0,(PI / 2).[ = dom (cosec | ].0,(PI / 2).[) by Lm17, Th4, RELAT_1:62, XBOOLE_1:1; then Lm24: ].0,(PI / 2).[ c= dom ((cosec | ].0,(PI / 2).]) | ].0,(PI / 2).[) by RELAT_1:74, XXREAL_1:21; theorem Th13: :: SINCOS10:13 sec | ].0,(PI / 2).[ is increasing proofend; theorem Th14: :: SINCOS10:14 sec | ].(PI / 2),PI.[ is increasing proofend; theorem Th15: :: SINCOS10:15 cosec | ].(- (PI / 2)),0.[ is decreasing proofend; theorem Th16: :: SINCOS10:16 cosec | ].0,(PI / 2).[ is decreasing proofend; theorem Th17: :: SINCOS10:17 sec | [.0,(PI / 2).[ is increasing proofend; theorem Th18: :: SINCOS10:18 sec | ].(PI / 2),PI.] is increasing proofend; theorem Th19: :: SINCOS10:19 cosec | [.(- (PI / 2)),0.[ is decreasing proofend; theorem Th20: :: SINCOS10:20 cosec | ].0,(PI / 2).] is decreasing proofend; theorem :: SINCOS10:21 sec | [.0,(PI / 2).[ is one-to-one by Th17, FCONT_3:8; theorem :: SINCOS10:22 sec | ].(PI / 2),PI.] is one-to-one by Th18, FCONT_3:8; theorem :: SINCOS10:23 cosec | [.(- (PI / 2)),0.[ is one-to-one by Th19, FCONT_3:8; theorem :: SINCOS10:24 cosec | ].0,(PI / 2).] is one-to-one by Th20, FCONT_3:8; registration clusterK77(sec,[.0,(PI / 2).[) -> one-to-one ; coherence sec | [.0,(PI / 2).[ is one-to-one by Th17, FCONT_3:8; clusterK77(sec,].(PI / 2),PI.]) -> one-to-one ; coherence sec | ].(PI / 2),PI.] is one-to-one by Th18, FCONT_3:8; clusterK77(cosec,[.(- (PI / 2)),0.[) -> one-to-one ; coherence cosec | [.(- (PI / 2)),0.[ is one-to-one by Th19, FCONT_3:8; clusterK77(cosec,].0,(PI / 2).]) -> one-to-one ; coherence cosec | ].0,(PI / 2).] is one-to-one by Th20, FCONT_3:8; end; definition func arcsec1 -> PartFunc of REAL,REAL equals :: SINCOS10:def 1 (sec | [.0,(PI / 2).[) " ; coherence (sec | [.0,(PI / 2).[) " is PartFunc of REAL,REAL ; func arcsec2 -> PartFunc of REAL,REAL equals :: SINCOS10:def 2 (sec | ].(PI / 2),PI.]) " ; coherence (sec | ].(PI / 2),PI.]) " is PartFunc of REAL,REAL ; func arccosec1 -> PartFunc of REAL,REAL equals :: SINCOS10:def 3 (cosec | [.(- (PI / 2)),0.[) " ; coherence (cosec | [.(- (PI / 2)),0.[) " is PartFunc of REAL,REAL ; func arccosec2 -> PartFunc of REAL,REAL equals :: SINCOS10:def 4 (cosec | ].0,(PI / 2).]) " ; coherence (cosec | ].0,(PI / 2).]) " is PartFunc of REAL,REAL ; end; :: deftheorem defines arcsec1 SINCOS10:def_1_:_ arcsec1 = (sec | [.0,(PI / 2).[) " ; :: deftheorem defines arcsec2 SINCOS10:def_2_:_ arcsec2 = (sec | ].(PI / 2),PI.]) " ; :: deftheorem defines arccosec1 SINCOS10:def_3_:_ arccosec1 = (cosec | [.(- (PI / 2)),0.[) " ; :: deftheorem defines arccosec2 SINCOS10:def_4_:_ arccosec2 = (cosec | ].0,(PI / 2).]) " ; definition let r be Real; func arcsec1 r -> set equals :: SINCOS10:def 5 arcsec1 . r; coherence arcsec1 . r is set ; func arcsec2 r -> set equals :: SINCOS10:def 6 arcsec2 . r; coherence arcsec2 . r is set ; func arccosec1 r -> set equals :: SINCOS10:def 7 arccosec1 . r; coherence arccosec1 . r is set ; func arccosec2 r -> set equals :: SINCOS10:def 8 arccosec2 . r; coherence arccosec2 . r is set ; end; :: deftheorem defines arcsec1 SINCOS10:def_5_:_ for r being Real holds arcsec1 r = arcsec1 . r; :: deftheorem defines arcsec2 SINCOS10:def_6_:_ for r being Real holds arcsec2 r = arcsec2 . r; :: deftheorem defines arccosec1 SINCOS10:def_7_:_ for r being Real holds arccosec1 r = arccosec1 . r; :: deftheorem defines arccosec2 SINCOS10:def_8_:_ for r being Real holds arccosec2 r = arccosec2 . r; definition let r be Real; :: original:arcsec1 redefine func arcsec1 r -> Real; coherence arcsec1 r is Real ; :: original:arcsec2 redefine func arcsec2 r -> Real; coherence arcsec2 r is Real ; :: original:arccosec1 redefine func arccosec1 r -> Real; coherence arccosec1 r is Real ; :: original:arccosec2 redefine func arccosec2 r -> Real; coherence arccosec2 r is Real ; end; Lm25: arcsec1 " = sec | [.0,(PI / 2).[ by FUNCT_1:43; Lm26: arcsec2 " = sec | ].(PI / 2),PI.] by FUNCT_1:43; Lm27: arccosec1 " = cosec | [.(- (PI / 2)),0.[ by FUNCT_1:43; Lm28: arccosec2 " = cosec | ].0,(PI / 2).] by FUNCT_1:43; theorem Th25: :: SINCOS10:25 rng arcsec1 = [.0,(PI / 2).[ proofend; theorem Th26: :: SINCOS10:26 rng arcsec2 = ].(PI / 2),PI.] proofend; theorem Th27: :: SINCOS10:27 rng arccosec1 = [.(- (PI / 2)),0.[ proofend; theorem Th28: :: SINCOS10:28 rng arccosec2 = ].0,(PI / 2).] proofend; registration cluster arcsec1 -> one-to-one ; coherence arcsec1 is one-to-one ; cluster arcsec2 -> one-to-one ; coherence arcsec2 is one-to-one ; cluster arccosec1 -> one-to-one ; coherence arccosec1 is one-to-one ; cluster arccosec2 -> one-to-one ; coherence arccosec2 is one-to-one ; end; theorem Th29: :: SINCOS10:29 ( sin . (PI / 4) = 1 / (sqrt 2) & cos . (PI / 4) = 1 / (sqrt 2) ) proofend; theorem Th30: :: SINCOS10:30 ( sin . (- (PI / 4)) = - (1 / (sqrt 2)) & cos . (- (PI / 4)) = 1 / (sqrt 2) & sin . ((3 / 4) * PI) = 1 / (sqrt 2) & cos . ((3 / 4) * PI) = - (1 / (sqrt 2)) ) proofend; theorem Th31: :: SINCOS10:31 ( sec . 0 = 1 & sec . (PI / 4) = sqrt 2 & sec . ((3 / 4) * PI) = - (sqrt 2) & sec . PI = - 1 ) proofend; theorem Th32: :: SINCOS10:32 ( cosec . (- (PI / 2)) = - 1 & cosec . (- (PI / 4)) = - (sqrt 2) & cosec . (PI / 4) = sqrt 2 & cosec . (PI / 2) = 1 ) proofend; theorem Th33: :: SINCOS10:33 for x being set st x in [.0,(PI / 4).] holds sec . x in [.1,(sqrt 2).] proofend; theorem Th34: :: SINCOS10:34 for x being set st x in [.((3 / 4) * PI),PI.] holds sec . x in [.(- (sqrt 2)),(- 1).] proofend; theorem Th35: :: SINCOS10:35 for x being set st x in [.(- (PI / 2)),(- (PI / 4)).] holds cosec . x in [.(- (sqrt 2)),(- 1).] proofend; theorem Th36: :: SINCOS10:36 for x being set st x in [.(PI / 4),(PI / 2).] holds cosec . x in [.1,(sqrt 2).] proofend; Lm29: dom (sec | [.0,(PI / 4).]) = [.0,(PI / 4).] proofend; Lm30: dom (sec | [.((3 / 4) * PI),PI.]) = [.((3 / 4) * PI),PI.] proofend; Lm31: dom (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (PI / 2)),(- (PI / 4)).] proofend; Lm32: dom (cosec | [.(PI / 4),(PI / 2).]) = [.(PI / 4),(PI / 2).] proofend; Lm33: ( dom (sec | [.0,(PI / 2).[) = [.0,(PI / 2).[ & ( for th being real number st th in [.0,(PI / 2).[ holds (sec | [.0,(PI / 2).[) . th = sec . th ) ) proofend; Lm34: ( dom (sec | ].(PI / 2),PI.]) = ].(PI / 2),PI.] & ( for th being real number st th in ].(PI / 2),PI.] holds (sec | ].(PI / 2),PI.]) . th = sec . th ) ) proofend; Lm35: ( dom (cosec | [.(- (PI / 2)),0.[) = [.(- (PI / 2)),0.[ & ( for th being real number st th in [.(- (PI / 2)),0.[ holds (cosec | [.(- (PI / 2)),0.[) . th = cosec . th ) ) proofend; Lm36: ( dom (cosec | ].0,(PI / 2).]) = ].0,(PI / 2).] & ( for th being real number st th in ].0,(PI / 2).] holds (cosec | ].0,(PI / 2).]) . th = cosec . th ) ) proofend; theorem Th37: :: SINCOS10:37 sec | [.0,(PI / 2).[ is continuous proofend; theorem Th38: :: SINCOS10:38 sec | ].(PI / 2),PI.] is continuous proofend; theorem Th39: :: SINCOS10:39 cosec | [.(- (PI / 2)),0.[ is continuous proofend; theorem Th40: :: SINCOS10:40 cosec | ].0,(PI / 2).] is continuous proofend; theorem Th41: :: SINCOS10:41 rng (sec | [.0,(PI / 4).]) = [.1,(sqrt 2).] proofend; theorem Th42: :: SINCOS10:42 rng (sec | [.((3 / 4) * PI),PI.]) = [.(- (sqrt 2)),(- 1).] proofend; theorem Th43: :: SINCOS10:43 rng (cosec | [.(- (PI / 2)),(- (PI / 4)).]) = [.(- (sqrt 2)),(- 1).] proofend; theorem Th44: :: SINCOS10:44 rng (cosec | [.(PI / 4),(PI / 2).]) = [.1,(sqrt 2).] proofend; theorem Th45: :: SINCOS10:45 [.1,(sqrt 2).] c= dom arcsec1 proofend; theorem Th46: :: SINCOS10:46 [.(- (sqrt 2)),(- 1).] c= dom arcsec2 proofend; theorem Th47: :: SINCOS10:47 [.(- (sqrt 2)),(- 1).] c= dom arccosec1 proofend; theorem Th48: :: SINCOS10:48 [.1,(sqrt 2).] c= dom arccosec2 proofend; Lm37: (sec | [.0,(PI / 4).]) | [.0,(PI / 4).] is increasing proofend; Lm38: (sec | [.((3 / 4) * PI),PI.]) | [.((3 / 4) * PI),PI.] is increasing proofend; Lm39: (cosec | [.(- (PI / 2)),(- (PI / 4)).]) | [.(- (PI / 2)),(- (PI / 4)).] is decreasing proofend; Lm40: (cosec | [.(PI / 4),(PI / 2).]) | [.(PI / 4),(PI / 2).] is decreasing proofend; Lm41: sec | [.0,(PI / 4).] is one-to-one proofend; Lm42: sec | [.((3 / 4) * PI),PI.] is one-to-one proofend; Lm43: cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one proofend; Lm44: cosec | [.(PI / 4),(PI / 2).] is one-to-one proofend; registration clusterK77(sec,[.0,(PI / 4).]) -> one-to-one ; coherence sec | [.0,(PI / 4).] is one-to-one by Lm41; clusterK77(sec,[.((3 / 4) * PI),PI.]) -> one-to-one ; coherence sec | [.((3 / 4) * PI),PI.] is one-to-one by Lm42; clusterK77(cosec,[.(- (PI / 2)),(- (PI / 4)).]) -> one-to-one ; coherence cosec | [.(- (PI / 2)),(- (PI / 4)).] is one-to-one by Lm43; clusterK77(cosec,[.(PI / 4),(PI / 2).]) -> one-to-one ; coherence cosec | [.(PI / 4),(PI / 2).] is one-to-one by Lm44; end; theorem Th49: :: SINCOS10:49 arcsec1 | [.1,(sqrt 2).] = (sec | [.0,(PI / 4).]) " proofend; theorem Th50: :: SINCOS10:50 arcsec2 | [.(- (sqrt 2)),(- 1).] = (sec | [.((3 / 4) * PI),PI.]) " proofend; theorem Th51: :: SINCOS10:51 arccosec1 | [.(- (sqrt 2)),(- 1).] = (cosec | [.(- (PI / 2)),(- (PI / 4)).]) " proofend; theorem Th52: :: SINCOS10:52 arccosec2 | [.1,(sqrt 2).] = (cosec | [.(PI / 4),(PI / 2).]) " proofend; theorem :: SINCOS10:53 (sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th41, Th49, FUNCT_1:39; theorem :: SINCOS10:54 (sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th42, Th50, FUNCT_1:39; theorem :: SINCOS10:55 (cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th43, Th51, FUNCT_1:39; theorem :: SINCOS10:56 (cosec | [.(PI / 4),(PI / 2).]) * (arccosec2 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th44, Th52, FUNCT_1:39; theorem :: SINCOS10:57 (sec | [.0,(PI / 4).]) * (arcsec1 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th41, Th49, FUNCT_1:39; theorem :: SINCOS10:58 (sec | [.((3 / 4) * PI),PI.]) * (arcsec2 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th42, Th50, FUNCT_1:39; theorem :: SINCOS10:59 (cosec | [.(- (PI / 2)),(- (PI / 4)).]) * (arccosec1 | [.(- (sqrt 2)),(- 1).]) = id [.(- (sqrt 2)),(- 1).] by Th43, Th51, FUNCT_1:39; theorem :: SINCOS10:60 (cosec | [.(PI / 4),(PI / 2).]) * (arccosec2 | [.1,(sqrt 2).]) = id [.1,(sqrt 2).] by Th44, Th52, FUNCT_1:39; theorem :: SINCOS10:61 arcsec1 * (sec | [.0,(PI / 2).[) = id [.0,(PI / 2).[ by Lm25, Th25, FUNCT_1:39; theorem :: SINCOS10:62 arcsec2 * (sec | ].(PI / 2),PI.]) = id ].(PI / 2),PI.] by Lm26, Th26, FUNCT_1:39; theorem :: SINCOS10:63 arccosec1 * (cosec | [.(- (PI / 2)),0.[) = id [.(- (PI / 2)),0.[ by Lm27, Th27, FUNCT_1:39; theorem :: SINCOS10:64 arccosec2 * (cosec | ].0,(PI / 2).]) = id ].0,(PI / 2).] by Lm28, Th28, FUNCT_1:39; theorem Th65: :: SINCOS10:65 arcsec1 * (sec | [.0,(PI / 2).[) = id [.0,(PI / 2).[ by Lm25, Th25, FUNCT_1:39; theorem Th66: :: SINCOS10:66 arcsec2 * (sec | ].(PI / 2),PI.]) = id ].(PI / 2),PI.] by Lm26, Th26, FUNCT_1:39; theorem Th67: :: SINCOS10:67 arccosec1 * (cosec | [.(- (PI / 2)),0.[) = id [.(- (PI / 2)),0.[ by Lm27, Th27, FUNCT_1:39; theorem Th68: :: SINCOS10:68 arccosec2 * (cosec | ].0,(PI / 2).]) = id ].0,(PI / 2).] by Lm28, Th28, FUNCT_1:39; theorem Th69: :: SINCOS10:69 for r being Real st 0 <= r & r < PI / 2 holds arcsec1 (sec . r) = r proofend; theorem Th70: :: SINCOS10:70 for r being Real st PI / 2 < r & r <= PI holds arcsec2 (sec . r) = r proofend; theorem Th71: :: SINCOS10:71 for r being Real st - (PI / 2) <= r & r < 0 holds arccosec1 (cosec . r) = r proofend; theorem Th72: :: SINCOS10:72 for r being Real st 0 < r & r <= PI / 2 holds arccosec2 (cosec . r) = r proofend; theorem Th73: :: SINCOS10:73 ( arcsec1 . 1 = 0 & arcsec1 . (sqrt 2) = PI / 4 ) proofend; theorem Th74: :: SINCOS10:74 ( arcsec2 . (- (sqrt 2)) = (3 / 4) * PI & arcsec2 . (- 1) = PI ) proofend; theorem Th75: :: SINCOS10:75 ( arccosec1 . (- 1) = - (PI / 2) & arccosec1 . (- (sqrt 2)) = - (PI / 4) ) proofend; theorem Th76: :: SINCOS10:76 ( arccosec2 . (sqrt 2) = PI / 4 & arccosec2 . 1 = PI / 2 ) proofend; theorem Th77: :: SINCOS10:77 arcsec1 | (sec .: [.0,(PI / 2).[) is increasing proofend; theorem Th78: :: SINCOS10:78 arcsec2 | (sec .: ].(PI / 2),PI.]) is increasing proofend; theorem Th79: :: SINCOS10:79 arccosec1 | (cosec .: [.(- (PI / 2)),0.[) is decreasing proofend; theorem Th80: :: SINCOS10:80 arccosec2 | (cosec .: ].0,(PI / 2).]) is decreasing proofend; theorem Th81: :: SINCOS10:81 arcsec1 | [.1,(sqrt 2).] is increasing proofend; theorem Th82: :: SINCOS10:82 arcsec2 | [.(- (sqrt 2)),(- 1).] is increasing proofend; theorem Th83: :: SINCOS10:83 arccosec1 | [.(- (sqrt 2)),(- 1).] is decreasing proofend; theorem Th84: :: SINCOS10:84 arccosec2 | [.1,(sqrt 2).] is decreasing proofend; theorem Th85: :: SINCOS10:85 for x being set st x in [.1,(sqrt 2).] holds arcsec1 . x in [.0,(PI / 4).] proofend; theorem Th86: :: SINCOS10:86 for x being set st x in [.(- (sqrt 2)),(- 1).] holds arcsec2 . x in [.((3 / 4) * PI),PI.] proofend; theorem Th87: :: SINCOS10:87 for x being set st x in [.(- (sqrt 2)),(- 1).] holds arccosec1 . x in [.(- (PI / 2)),(- (PI / 4)).] proofend; theorem Th88: :: SINCOS10:88 for x being set st x in [.1,(sqrt 2).] holds arccosec2 . x in [.(PI / 4),(PI / 2).] proofend; theorem Th89: :: SINCOS10:89 for r being Real st 1 <= r & r <= sqrt 2 holds sec . (arcsec1 r) = r proofend; theorem Th90: :: SINCOS10:90 for r being Real st - (sqrt 2) <= r & r <= - 1 holds sec . (arcsec2 r) = r proofend; theorem Th91: :: SINCOS10:91 for r being Real st - (sqrt 2) <= r & r <= - 1 holds cosec . (arccosec1 r) = r proofend; theorem Th92: :: SINCOS10:92 for r being Real st 1 <= r & r <= sqrt 2 holds cosec . (arccosec2 r) = r proofend; theorem Th93: :: SINCOS10:93 arcsec1 | [.1,(sqrt 2).] is continuous proofend; theorem Th94: :: SINCOS10:94 arcsec2 | [.(- (sqrt 2)),(- 1).] is continuous proofend; theorem Th95: :: SINCOS10:95 arccosec1 | [.(- (sqrt 2)),(- 1).] is continuous proofend; theorem Th96: :: SINCOS10:96 arccosec2 | [.1,(sqrt 2).] is continuous proofend; theorem Th97: :: SINCOS10:97 rng (arcsec1 | [.1,(sqrt 2).]) = [.0,(PI / 4).] proofend; theorem Th98: :: SINCOS10:98 rng (arcsec2 | [.(- (sqrt 2)),(- 1).]) = [.((3 / 4) * PI),PI.] proofend; theorem Th99: :: SINCOS10:99 rng (arccosec1 | [.(- (sqrt 2)),(- 1).]) = [.(- (PI / 2)),(- (PI / 4)).] proofend; theorem Th100: :: SINCOS10:100 rng (arccosec2 | [.1,(sqrt 2).]) = [.(PI / 4),(PI / 2).] proofend; theorem :: SINCOS10:101 for r being Real holds ( ( 1 <= r & r <= sqrt 2 & arcsec1 r = 0 implies r = 1 ) & ( 1 <= r & r <= sqrt 2 & arcsec1 r = PI / 4 implies r = sqrt 2 ) ) by Th31, Th89; theorem :: SINCOS10:102 for r being Real holds ( ( - (sqrt 2) <= r & r <= - 1 & arcsec2 r = (3 / 4) * PI implies r = - (sqrt 2) ) & ( - (sqrt 2) <= r & r <= - 1 & arcsec2 r = PI implies r = - 1 ) ) by Th31, Th90; theorem :: SINCOS10:103 for r being Real holds ( ( - (sqrt 2) <= r & r <= - 1 & arccosec1 r = - (PI / 2) implies r = - 1 ) & ( - (sqrt 2) <= r & r <= - 1 & arccosec1 r = - (PI / 4) implies r = - (sqrt 2) ) ) by Th32, Th91; theorem :: SINCOS10:104 for r being Real holds ( ( 1 <= r & r <= sqrt 2 & arccosec2 r = PI / 4 implies r = sqrt 2 ) & ( 1 <= r & r <= sqrt 2 & arccosec2 r = PI / 2 implies r = 1 ) ) by Th32, Th92; theorem Th105: :: SINCOS10:105 for r being Real st 1 <= r & r <= sqrt 2 holds ( 0 <= arcsec1 r & arcsec1 r <= PI / 4 ) proofend; theorem Th106: :: SINCOS10:106 for r being Real st - (sqrt 2) <= r & r <= - 1 holds ( (3 / 4) * PI <= arcsec2 r & arcsec2 r <= PI ) proofend; theorem Th107: :: SINCOS10:107 for r being Real st - (sqrt 2) <= r & r <= - 1 holds ( - (PI / 2) <= arccosec1 r & arccosec1 r <= - (PI / 4) ) proofend; theorem Th108: :: SINCOS10:108 for r being Real st 1 <= r & r <= sqrt 2 holds ( PI / 4 <= arccosec2 r & arccosec2 r <= PI / 2 ) proofend; theorem Th109: :: SINCOS10:109 for r being Real st 1 < r & r < sqrt 2 holds ( 0 < arcsec1 r & arcsec1 r < PI / 4 ) proofend; theorem Th110: :: SINCOS10:110 for r being Real st - (sqrt 2) < r & r < - 1 holds ( (3 / 4) * PI < arcsec2 r & arcsec2 r < PI ) proofend; theorem Th111: :: SINCOS10:111 for r being Real st - (sqrt 2) < r & r < - 1 holds ( - (PI / 2) < arccosec1 r & arccosec1 r < - (PI / 4) ) proofend; theorem Th112: :: SINCOS10:112 for r being Real st 1 < r & r < sqrt 2 holds ( PI / 4 < arccosec2 r & arccosec2 r < PI / 2 ) proofend; theorem Th113: :: SINCOS10:113 for r being Real st 1 <= r & r <= sqrt 2 holds ( sin . (arcsec1 r) = (sqrt ((r ^2) - 1)) / r & cos . (arcsec1 r) = 1 / r ) proofend; theorem Th114: :: SINCOS10:114 for r being Real st - (sqrt 2) <= r & r <= - 1 holds ( sin . (arcsec2 r) = - ((sqrt ((r ^2) - 1)) / r) & cos . (arcsec2 r) = 1 / r ) proofend; theorem Th115: :: SINCOS10:115 for r being Real st - (sqrt 2) <= r & r <= - 1 holds ( sin . (arccosec1 r) = 1 / r & cos . (arccosec1 r) = - ((sqrt ((r ^2) - 1)) / r) ) proofend; theorem Th116: :: SINCOS10:116 for r being Real st 1 <= r & r <= sqrt 2 holds ( sin . (arccosec2 r) = 1 / r & cos . (arccosec2 r) = (sqrt ((r ^2) - 1)) / r ) proofend; theorem :: SINCOS10:117 for r being Real st 1 < r & r < sqrt 2 holds cosec . (arcsec1 r) = r / (sqrt ((r ^2) - 1)) proofend; theorem :: SINCOS10:118 for r being Real st - (sqrt 2) < r & r < - 1 holds cosec . (arcsec2 r) = - (r / (sqrt ((r ^2) - 1))) proofend; theorem :: SINCOS10:119 for r being Real st - (sqrt 2) < r & r < - 1 holds sec . (arccosec1 r) = - (r / (sqrt ((r ^2) - 1))) proofend; theorem :: SINCOS10:120 for r being Real st 1 < r & r < sqrt 2 holds sec . (arccosec2 r) = r / (sqrt ((r ^2) - 1)) proofend; theorem Th121: :: SINCOS10:121 arcsec1 is_differentiable_on sec .: ].0,(PI / 2).[ proofend; theorem Th122: :: SINCOS10:122 arcsec2 is_differentiable_on sec .: ].(PI / 2),PI.[ proofend; theorem Th123: :: SINCOS10:123 arccosec1 is_differentiable_on cosec .: ].(- (PI / 2)),0.[ proofend; theorem Th124: :: SINCOS10:124 arccosec2 is_differentiable_on cosec .: ].0,(PI / 2).[ proofend; theorem :: SINCOS10:125 sec .: ].0,(PI / 2).[ is open proofend; theorem :: SINCOS10:126 sec .: ].(PI / 2),PI.[ is open proofend; theorem :: SINCOS10:127 cosec .: ].(- (PI / 2)),0.[ is open proofend; theorem :: SINCOS10:128 cosec .: ].0,(PI / 2).[ is open proofend; theorem :: SINCOS10:129 arcsec1 | (sec .: ].0,(PI / 2).[) is continuous by Th121, FDIFF_1:25; theorem :: SINCOS10:130 arcsec2 | (sec .: ].(PI / 2),PI.[) is continuous by Th122, FDIFF_1:25; theorem :: SINCOS10:131 arccosec1 | (cosec .: ].(- (PI / 2)),0.[) is continuous by Th123, FDIFF_1:25; theorem :: SINCOS10:132 arccosec2 | (cosec .: ].0,(PI / 2).[) is continuous by Th124, FDIFF_1:25;