:: Inverse Trigonometric Functions Arcsec1, Arcsec2, Arccosec1 and Arccosec2
:: by Bing Xie , Xiquan Liang and Fuguo Ge
::
:: Received March 18, 2008
:: Copyright (c) 2008-2016 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;
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 -> set equals
:: SINCOS10:def 5
arcsec1.r;
func arcsec2 r -> set equals
:: SINCOS10:def 6
arcsec2.r;
func arccosec1 r -> set equals
:: SINCOS10:def 7
arccosec1.r;
func arccosec2 r -> set 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;