:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
::  by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-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, REAL_1, XREAL_0, SUBSET_1, RCOMP_1, SEQ_1, PARTFUN1,
      XXREAL_1, CARD_1, SIN_COS, ARYTM_3, TARSKI, ARYTM_1, XBOOLE_0, RELAT_1,
      SIN_COS4, ORDINAL4, FUNCT_1, FDIFF_1, SQUARE_1, ORDINAL2, XXREAL_0,
      VALUED_0, FCONT_1, SEQ_2, FUNCT_2, SINCOS10, ORDINAL1;
 notations TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, FUNCT_1, RELSET_1,
      PARTFUN1, FUNCT_2, RCOMP_1, SIN_COS, RFUNCT_1, SQUARE_1, NUMBERS, REAL_1,
      SEQ_1, FDIFF_1, XREAL_0, INT_1, SIN_COS4, PARTFUN2, RFUNCT_2, FCONT_1,
      XBOOLE_0, FDIFF_9, SEQ_2;
 constructors REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1,
      SIN_COS, PARTFUN2, SIN_COS4, RELSET_1, FDIFF_9, SEQ_2, XXREAL_2, NEWTON,
      COMSEQ_2;
 registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1,
      FUNCT_1, SIN_COS6, RFUNCT_2, ORDINAL1, INT_1, VALUED_0, XXREAL_2,
      XBOOLE_0, NUMBERS, SIN_COS, SQUARE_1;
 requirements SUBSET, BOOLE, NUMERALS, ARITHM, REAL;


begin ::  arcsec, arccosec

reserve x,x0, r,r1,r2 for Real,
      th for Real,

  rr for set,

  rseq for Real_Sequence;

theorem :: SINCOS10:1
  [.0,PI/2.[ c= dom sec;

theorem :: SINCOS10:2
  ].PI/2,PI.] c= dom sec;

theorem :: SINCOS10:3
  [.-PI/2,0.[ c= dom cosec;

theorem :: SINCOS10:4
  ].0,PI/2.] c= dom cosec;

theorem :: SINCOS10:5
  sec is_differentiable_on ].0,PI/2.[ & for x st x in ].0,PI/2.[
  holds diff(sec,x) = sin.x/(cos.x)^2;

theorem :: SINCOS10:6
  sec is_differentiable_on ].PI/2,PI.[ & for x st x in ].PI/2,PI.[
  holds diff(sec,x) = sin.x/(cos.x)^2;

theorem :: SINCOS10:7
  cosec is_differentiable_on ].-PI/2,0.[ & for x st x in ].-PI/2,0
  .[ holds diff(cosec,x) = -cos.x/(sin.x)^2;

theorem :: SINCOS10:8
  cosec is_differentiable_on ].0,PI/2.[ & for x st x in ].0,PI/2.[
  holds diff(cosec,x) = -cos.x/(sin.x)^2;

theorem :: SINCOS10:9
  sec|].0,PI/2.[ is continuous;

theorem :: SINCOS10:10
  sec|].PI/2,PI.[ is continuous;

theorem :: SINCOS10:11
  cosec|].-PI/2,0.[ is continuous;

theorem :: SINCOS10:12
  cosec|].0,PI/2.[ is continuous;

theorem :: SINCOS10:13
  sec|].0,PI/2.[ is increasing;

theorem :: SINCOS10:14
  sec|].PI/2,PI.[ is increasing;

theorem :: SINCOS10:15
  cosec|].-PI/2,0.[ is decreasing;

theorem :: SINCOS10:16
  cosec|].0,PI/2.[ is decreasing;

theorem :: SINCOS10:17
  sec|[.0,PI/2.[ is increasing;

theorem :: SINCOS10:18
  sec|].PI/2,PI.] is increasing;

theorem :: SINCOS10:19
  cosec|[.-PI/2,0.[ is decreasing;

theorem :: SINCOS10:20
  cosec|].0,PI/2.] is decreasing;

theorem :: SINCOS10:21
  sec | [.0,PI/2.[ is one-to-one;

theorem :: SINCOS10:22
  sec | ].PI/2,PI.] is one-to-one;

theorem :: SINCOS10:23
  cosec | [.-PI/2,0.[ is one-to-one;

theorem :: SINCOS10:24
  cosec | ].0,PI/2.] is one-to-one;

registration
  cluster sec | [.0,PI/2.[ -> one-to-one;
  cluster sec | ].PI/2,PI.] -> one-to-one;
  cluster cosec | [.-PI/2,0.[ -> one-to-one;
  cluster cosec | ].0,PI/2.] -> one-to-one;
end;

definition
  func arcsec1 -> PartFunc of REAL, REAL equals
:: SINCOS10:def 1
  (sec | [.0,PI/2.[)";
  func arcsec2 -> PartFunc of REAL, REAL equals
:: SINCOS10:def 2
  (sec | ].PI/2, PI.])";
  func arccosec1 -> PartFunc of REAL, REAL equals
:: SINCOS10:def 3
  (cosec | [.-PI/2,0.[)";
  func arccosec2 -> PartFunc of REAL, REAL equals
:: SINCOS10:def 4
  (cosec | ].0,PI/2.])";
end;

definition
  let r be Real;
  func arcsec1 r -> number equals
:: SINCOS10:def 5
  arcsec1.r;
  func arcsec2 r -> number equals
:: SINCOS10:def 6
  arcsec2.r;
  func arccosec1 r -> number equals
:: SINCOS10:def 7
  arccosec1.r;
  func arccosec2 r -> number equals
:: SINCOS10:def 8
  arccosec2.r;
end;

registration
  let r be Real;
  cluster arcsec1 r -> real;
  cluster arcsec2 r -> real;
  cluster arccosec1 r -> real;
  cluster arccosec2 r -> real;
end;

theorem :: SINCOS10:25
  rng arcsec1 = [.0,PI/2.[;

theorem :: SINCOS10:26
  rng arcsec2 = ].PI/2,PI.];

theorem :: SINCOS10:27
  rng arccosec1 = [.-PI/2,0.[;

theorem :: SINCOS10:28
  rng arccosec2 = ].0,PI/2.];

registration
  cluster arcsec1 -> one-to-one;
  cluster arcsec2 -> one-to-one;
  cluster arccosec1 -> one-to-one;
  cluster arccosec2 -> one-to-one;
end;

theorem :: SINCOS10:29
  sin.(PI/4) = 1/sqrt 2 & cos.(PI/4) = 1/sqrt 2;

theorem :: 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;

theorem :: SINCOS10:31
  sec.0 = 1 & sec.(PI/4) = sqrt 2 & sec.(3/4*PI) = -sqrt 2 & sec. PI = -1;

theorem :: SINCOS10:32
  cosec.(-PI/2) = -1 & cosec.(-PI/4) = -sqrt 2 & cosec.(PI/4) =
  sqrt 2 & cosec.(PI/2) = 1;

theorem :: SINCOS10:33
  for x be set st x in [.0,PI/4.] holds sec.x in [.1,sqrt 2.];

theorem :: SINCOS10:34
  for x be set st x in [.3/4*PI,PI.] holds sec.x in [.-sqrt 2,-1.];

theorem :: SINCOS10:35
  for x be set st x in [.-PI/2,-PI/4.] holds cosec.x in [.-sqrt 2, -1.];

theorem :: SINCOS10:36
  for x be set st x in [.PI/4,PI/2.] holds cosec.x in [.1,sqrt 2.];

theorem :: SINCOS10:37
  sec|[.0,PI/2.[ is continuous;

theorem :: SINCOS10:38
  sec|].PI/2,PI.] is continuous;

theorem :: SINCOS10:39
  cosec|[.-PI/2,0.[ is continuous;

theorem :: SINCOS10:40
  cosec|].0,PI/2.] is continuous;

theorem :: SINCOS10:41
  rng(sec | [.0,PI/4.]) = [.1,sqrt 2.];

theorem :: SINCOS10:42
  rng(sec | [.3/4*PI,PI.]) = [.-sqrt 2,-1.];

theorem :: SINCOS10:43
  rng(cosec | [.-PI/2,-PI/4.]) = [.-sqrt 2,-1.];

theorem :: SINCOS10:44
  rng(cosec | [.PI/4,PI/2.]) = [.1,sqrt 2.];

theorem :: SINCOS10:45
  [.1,sqrt 2.] c= dom arcsec1;

theorem :: SINCOS10:46
  [.-sqrt 2,-1.] c= dom arcsec2;

theorem :: SINCOS10:47
  [.-sqrt 2,-1.] c= dom arccosec1;

theorem :: SINCOS10:48
  [.1,sqrt 2.] c= dom arccosec2;

registration
  cluster sec | [.0,PI/4.] -> one-to-one;
  cluster sec | [.3/4*PI,PI.] -> one-to-one;
  cluster cosec | [.-PI/2,-PI/4.] -> one-to-one;
  cluster cosec | [.PI/4,PI/2.] -> one-to-one;
end;

theorem :: SINCOS10:49
  arcsec1 | [.1,sqrt 2.] = (sec | [.0,PI/4.])";

theorem :: SINCOS10:50
  arcsec2 | [.-sqrt 2,-1.] = (sec | [.3/4*PI,PI.])";

theorem :: SINCOS10:51
  arccosec1 | [.-sqrt 2,-1.] = (cosec | [.-PI/2,-PI/4.])";

theorem :: SINCOS10:52
  arccosec2 | [.1,sqrt 2.] = (cosec | [.PI/4,PI/2.])";

theorem :: SINCOS10:53
  (sec | [.0,PI/4.]) qua Function * (arcsec1 | [.1,sqrt 2.]) = id [.1,
  sqrt 2.];

theorem :: SINCOS10:54
  (sec | [.3/4*PI,PI.]) qua Function * (arcsec2 | [.-sqrt 2,-1.]) = id
  [.-sqrt 2,-1.];

theorem :: SINCOS10:55
  (cosec | [.-PI/2,-PI/4.]) qua Function * (arccosec1 | [.-sqrt 2,-1.])
  = id [.-sqrt 2,-1.];

theorem :: SINCOS10:56
  (cosec | [.PI/4,PI/2.]) qua Function * (arccosec2 | [.1,sqrt 2.]) = id
  [.1,sqrt 2.];

theorem :: SINCOS10:57
  (sec | [.0,PI/4.]) * (arcsec1 | [.1,sqrt 2.]) = id [.1,sqrt 2.];

theorem :: SINCOS10:58
  (sec | [.3/4*PI,PI.]) * (arcsec2 | [.-sqrt 2,-1.]) = id [.-sqrt 2,-1.];

theorem :: SINCOS10:59
  (cosec | [.-PI/2,-PI/4.]) * (arccosec1 | [.-sqrt 2,-1.]) = id [.-sqrt
  2,-1.];

theorem :: SINCOS10:60
  (cosec | [.PI/4,PI/2.]) * (arccosec2 | [.1,sqrt 2.]) = id [.1,sqrt 2.];

theorem :: SINCOS10:61
  arcsec1 qua Function * (sec | [.0,PI/2.[) = id [.0,PI/2.[;

theorem :: SINCOS10:62
  arcsec2 qua Function * (sec | ].PI/2,PI.]) = id ].PI/2,PI.];

theorem :: SINCOS10:63
  arccosec1 qua Function * (cosec | [.-PI/2,0.[) = id [.-PI/2,0.[;

theorem :: SINCOS10:64
  arccosec2 qua Function * (cosec | ].0,PI/2.]) = id ].0,PI/2.];

theorem :: SINCOS10:65
  arcsec1 * (sec | [.0,PI/2.[) = id [.0,PI/2.[;

theorem :: SINCOS10:66
  arcsec2 * (sec | ].PI/2,PI.]) = id ].PI/2,PI.];

theorem :: SINCOS10:67
  arccosec1 * (cosec | [.-PI/2,0.[) = id [.-PI/2,0.[;

theorem :: SINCOS10:68
  arccosec2 * (cosec | ].0,PI/2.]) = id ].0,PI/2.];

theorem :: SINCOS10:69
  0 <= r & r < PI/2 implies arcsec1 sec.r = r;

theorem :: SINCOS10:70
  PI/2 < r & r <= PI implies arcsec2 sec.r = r;

theorem :: SINCOS10:71
  -PI/2 <= r & r < 0 implies arccosec1 cosec.r = r;

theorem :: SINCOS10:72
  0 < r & r <= PI/2 implies arccosec2 cosec.r = r;

theorem :: SINCOS10:73
  arcsec1.1 = 0 & arcsec1.(sqrt 2) = PI/4;

theorem :: SINCOS10:74
  arcsec2.(-sqrt 2) = 3/4*PI & arcsec2.(-1) = PI;

theorem :: SINCOS10:75
  arccosec1.(-1) = -PI/2 & arccosec1.(-sqrt 2) = -PI/4;

theorem :: SINCOS10:76
  arccosec2.(sqrt 2) = PI/4 & arccosec2.1 = PI/2;

theorem :: SINCOS10:77
  arcsec1|(sec.:[.0,PI/2.[) is increasing;

theorem :: SINCOS10:78
  arcsec2|(sec.:].PI/2,PI.]) is increasing;

theorem :: SINCOS10:79
  arccosec1|(cosec.:[.-PI/2,0.[) is decreasing;

theorem :: SINCOS10:80
  arccosec2|(cosec.:].0,PI/2.]) is decreasing;

theorem :: SINCOS10:81
  arcsec1|[.1,sqrt 2.] is increasing;

theorem :: SINCOS10:82
  arcsec2|[.-sqrt 2,-1.] is increasing;

theorem :: SINCOS10:83
  arccosec1|[.-sqrt 2,-1.] is decreasing;

theorem :: SINCOS10:84
  arccosec2|[.1,sqrt 2.] is decreasing;

theorem :: SINCOS10:85
  for x be set st x in [.1,sqrt 2.] holds arcsec1.x in [.0,PI/4.];

theorem :: SINCOS10:86
  for x be set st x in [.-sqrt 2,-1.] holds arcsec2.x in [.3/4*PI, PI.];

theorem :: SINCOS10:87
  for x be set st x in [.-sqrt 2,-1.] holds arccosec1.x in [.-PI/2 ,-PI/4.];

theorem :: SINCOS10:88
  for x be set st x in [.1,sqrt 2.] holds arccosec2.x in [.PI/4,PI /2.];

theorem :: SINCOS10:89
  1 <= r & r <= sqrt 2 implies sec.(arcsec1 r) = r;

theorem :: SINCOS10:90
  -sqrt 2 <= r & r <= -1 implies sec.(arcsec2 r ) = r;

theorem :: SINCOS10:91
  -sqrt 2 <= r & r <= -1 implies cosec.(arccosec1 r) = r;

theorem :: SINCOS10:92
  1 <= r & r <= sqrt 2 implies cosec.(arccosec2 r) = r;

theorem :: SINCOS10:93
  arcsec1|[.1,sqrt 2.] is continuous;

theorem :: SINCOS10:94
  arcsec2|[.-sqrt 2,-1.] is continuous;

theorem :: SINCOS10:95
  arccosec1|[.-sqrt 2,-1.] is continuous;

theorem :: SINCOS10:96
  arccosec2|[.1,sqrt 2.] is continuous;

theorem :: SINCOS10:97
  rng(arcsec1 | [.1,sqrt 2.]) = [.0,PI/4.];

theorem :: SINCOS10:98
  rng(arcsec2 | [.-sqrt 2,-1.]) = [.3/4*PI,PI.];

theorem :: SINCOS10:99
  rng(arccosec1 | [.-sqrt 2,-1.]) = [.-PI/2,-PI/4.];

theorem :: SINCOS10:100
  rng(arccosec2 | [.1,sqrt 2.]) = [.PI/4,PI/2.];

theorem :: SINCOS10:101
  (1 <= r & r <= sqrt 2 & arcsec1 r = 0 implies r = 1) & (1 <= r & r <=
  sqrt 2 & arcsec1 r = PI/4 implies r = sqrt 2);

theorem :: SINCOS10:102
  (-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);

theorem :: SINCOS10:103
  (-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);

theorem :: SINCOS10:104
  (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);

theorem :: SINCOS10:105
  1 <= r & r <= sqrt 2 implies 0 <= arcsec1 r & arcsec1 r <= PI/4;

theorem :: SINCOS10:106
  -sqrt 2 <= r & r <= -1 implies 3/4*PI <= arcsec2 r & arcsec2 r <= PI;

theorem :: SINCOS10:107
  -sqrt 2 <= r & r <= -1 implies -PI/2 <= arccosec1 r & arccosec1 r <= -PI/4;

theorem :: SINCOS10:108
  1 <= r & r <= sqrt 2 implies PI/4 <= arccosec2 r & arccosec2 r <= PI/2;

theorem :: SINCOS10:109
  1 < r & r < sqrt 2 implies 0 < arcsec1 r & arcsec1 r < PI/4;

theorem :: SINCOS10:110
  -sqrt 2 < r & r < -1 implies 3/4*PI < arcsec2 r & arcsec2 r < PI;

theorem :: SINCOS10:111
  -sqrt 2 < r & r < -1 implies -PI/2 < arccosec1 r & arccosec1 r < -PI/4;

theorem :: SINCOS10:112
  1 < r & r < sqrt 2 implies PI/4 < arccosec2 r & arccosec2 r < PI/2;

theorem :: SINCOS10:113
  1 <= r & r <= sqrt 2 implies sin.(arcsec1 r) = sqrt(r^2-1)/r &
  cos.(arcsec1 r) = 1/r;

theorem :: SINCOS10:114
  -sqrt 2 <= r & r <= -1 implies sin.(arcsec2 r) = -sqrt(r^2-1)/r
  & cos.(arcsec2 r) = 1/r;

theorem :: SINCOS10:115
  -sqrt 2 <= r & r <= -1 implies sin.(arccosec1 r) = 1/r & cos.(
  arccosec1 r) = -sqrt(r^2-1)/r;

theorem :: SINCOS10:116
  1 <= r & r <= sqrt 2 implies sin.(arccosec2 r) = 1/r & cos.(
  arccosec2 r) = sqrt(r^2-1)/r;

theorem :: SINCOS10:117
  1 < r & r < sqrt 2 implies cosec.(arcsec1 r) = r/sqrt(r^2-1);

theorem :: SINCOS10:118
  -sqrt 2 < r & r < -1 implies cosec.(arcsec2 r) = -r/sqrt(r^2-1);

theorem :: SINCOS10:119
  -sqrt 2 < r & r < -1 implies sec.(arccosec1 r) = -r/sqrt(r^2-1);

theorem :: SINCOS10:120
  1 < r & r < sqrt 2 implies sec.(arccosec2 r) = r/sqrt(r^2-1);

theorem :: SINCOS10:121
  arcsec1 is_differentiable_on sec.:].0,PI/2.[;

theorem :: SINCOS10:122
  arcsec2 is_differentiable_on sec.:].PI/2,PI.[;

theorem :: SINCOS10:123
  arccosec1 is_differentiable_on cosec.:].-PI/2,0.[;

theorem :: SINCOS10:124
  arccosec2 is_differentiable_on cosec.:].0,PI/2.[;

theorem :: SINCOS10:125
  sec.:].0,PI/2.[ is open;

theorem :: SINCOS10:126
  sec.:].PI/2,PI.[ is open;

theorem :: SINCOS10:127
  cosec.:].-PI/2,0.[ is open;

theorem :: SINCOS10:128
  cosec.:].0,PI/2.[ is open;

theorem :: SINCOS10:129
  arcsec1|(sec.:].0,PI/2.[) is continuous;

theorem :: SINCOS10:130
  arcsec2|(sec.:].PI/2,PI.[) is continuous;

theorem :: SINCOS10:131
  arccosec1|(cosec.:].-PI/2,0.[) is continuous;

theorem :: SINCOS10:132
  arccosec2|(cosec.:].0,PI/2.[) is continuous;