environ
vocabularies HIDDEN, NUMBERS, REAL_1, XREAL_0, SUBSET_1, RCOMP_1, PARTFUN1, XXREAL_1, ARYTM_1, SIN_COS, ARYTM_3, TARSKI, RELAT_1, XBOOLE_0, CARD_1, FUNCT_1, FDIFF_1, SQUARE_1, ORDINAL2, XXREAL_0, VALUED_0, VALUED_1, TAYLOR_1, PREPOWER, ORDINAL4, LIMFUNC1, SIN_COS9;
notations HIDDEN, TARSKI, SUBSET_1, ORDINAL1, XXREAL_0, XCMPLX_0, FUNCT_1, RELSET_1, PARTFUN1, RCOMP_1, SIN_COS, RFUNCT_1, SQUARE_1, VALUED_1, NUMBERS, REAL_1, FDIFF_1, XREAL_0, INT_1, SIN_COS4, PARTFUN2, FCONT_1, XBOOLE_0, TAYLOR_1, PREPOWER, LIMFUNC1, RFUNCT_2;
definitions TARSKI;
theorems FDIFF_2, XCMPLX_1, FDIFF_1, RELAT_1, SIN_COS, COMPTRIG, RFUNCT_2, FCONT_1, SIN_COS4, FUNCT_1, RCOMP_1, XBOOLE_0, FCONT_3, XREAL_1, TARSKI, XBOOLE_1, FDIFF_7, ROLLE, RFUNCT_1, FCONT_2, TAYLOR_1, PREPOWER, VALUED_1, FDIFF_4, FDIFF_5, XXREAL_1, XXREAL_0, XXREAL_2, XREAL_0;
schemes ;
registrations XCMPLX_0, XXREAL_0, XREAL_0, MEMBERED, RCOMP_1, RELSET_1, SIN_COS, FUNCT_1, SIN_COS6, RFUNCT_2, NUMBERS, INT_1, VALUED_0, XXREAL_2, ORDINAL1, SQUARE_1, PREPOWER;
constructors HIDDEN, REAL_1, SQUARE_1, RCOMP_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1, SIN_COS, PARTFUN2, SIN_COS4, TAYLOR_1, PREPOWER, LIMFUNC1, VALUED_1, XXREAL_2, PARTFUN1, SIN_COS6, RELSET_1, COMPLEX1;
requirements HIDDEN, SUBSET, BOOLE, NUMERALS, ARITHM, REAL;
equalities XCMPLX_0, LIMFUNC1, SIN_COS, VALUED_1, SQUARE_1;
expansions TARSKI;
Lm1:
tan is_differentiable_on ].(- (PI / 2)),(PI / 2).[
Lm2:
cot is_differentiable_on ].0,PI.[
Lm3:
for x being Real st x in ].(- (PI / 2)),(PI / 2).[ holds
diff (tan,x) = 1 / ((cos . x) ^2)
Lm4:
for x being Real st x in ].0,PI.[ holds
diff (cot,x) = - (1 / ((sin . x) ^2))
Lm5:
arctan " = tan | ].(- (PI / 2)),(PI / 2).[
by FUNCT_1:43;
Lm6:
arccot " = cot | ].0,PI.[
by FUNCT_1:43;
Lm7:
- (PI / 4) in ].(- (PI / 2)),(PI / 2).[
Lm8:
PI / 4 in ].(- (PI / 2)),(PI / 2).[
Lm9:
PI / 4 in ].0,PI.[
Lm10:
(3 / 4) * PI in ].0,PI.[
Lm11:
dom (tan | [.(- (PI / 4)),(PI / 4).]) = [.(- (PI / 4)),(PI / 4).]
Lm12:
dom (cot | [.(PI / 4),((3 / 4) * PI).]) = [.(PI / 4),((3 / 4) * PI).]
Lm13:
(tan | [.(- (PI / 4)),(PI / 4).]) | [.(- (PI / 4)),(PI / 4).] is increasing
Lm14:
(cot | [.(PI / 4),((3 / 4) * PI).]) | [.(PI / 4),((3 / 4) * PI).] is decreasing
Lm15:
tan | [.(- (PI / 4)),(PI / 4).] is one-to-one
Lm16:
cot | [.(PI / 4),((3 / 4) * PI).] is one-to-one