environ
vocabularies HIDDEN, NUMBERS, PARTFUN1, INTEGRA1, SUBSET_1, REAL_1, RCOMP_1, SIN_COS, ARYTM_3, XXREAL_0, CARD_1, XXREAL_1, RELAT_1, ARYTM_1, FUNCT_1, SQUARE_1, COMPLEX1, TARSKI, SIN_COS6, SIN_COS2, POWER, VALUED_1, FDIFF_1, SEQ_1, FUNCT_2, SEQ_2, ORDINAL2, FUNCOP_1, FUNCT_3, XBOOLE_0, SEQ_4, INTEGRA5, MEASURE7, REALSET1, XXREAL_2, INTEGRA8, MEASURE5, VALUED_0, NAT_1;
notations HIDDEN, TARSKI, XBOOLE_0, ORDINAL1, FUNCT_1, FUNCOP_1, INTEGRA1, RFUNCT_1, RELAT_1, INTEGRA5, VALUED_0, SIN_COS, SUBSET_1, PARTFUN1, RCOMP_1, NUMBERS, FDIFF_1, XXREAL_0, XCMPLX_0, XREAL_0, COMPLEX1, REAL_1, FCONT_1, COMSEQ_2, SEQ_2, SEQ_4, SIN_COS2, NAT_1, POWER, SQUARE_1, VALUED_1, SEQ_1, SIN_COS6, FUNCT_2, MEASURE5;
definitions ;
theorems PARTFUN1, INTEGRA1, FUNCT_1, SEQ_1, FDIFF_1, INTEGRA4, XBOOLE_0, XBOOLE_1, FUNCOP_1, INTEGRA5, FUNCT_3, SIN_COS, SIN_COS2, FCONT_1, RFUNCT_1, SEQ_2, RFUNCT_2, IRRAT_1, TAYLOR_1, XCMPLX_1, XREAL_1, SQUARE_1, FDIFF_7, SIN_COS6, FDIFF_2, SIN_COS5, COMPLEX1, ABSVALUE, INTEGRA2, FUNCT_2, VALUED_0, VALUED_1, XXREAL_1, XXREAL_2, RELAT_1, FDIFF_8, XREAL_0;
schemes NAT_1;
registrations RELSET_1, MEMBERED, RCOMP_1, FDIFF_1, INT_1, XXREAL_0, XREAL_0, NUMBERS, XBOOLE_0, VALUED_0, VALUED_1, FUNCT_2, XXREAL_2, FCONT_1, SIN_COS, FCONT_3, MEASURE5, ORDINAL1, SQUARE_1, SIN_COS6;
constructors HIDDEN, BINOP_2, FINSEQOP, INTEGRA5, SIN_COS, COMSEQ_3, PARTFUN1, REAL_1, SQUARE_1, RFUNCT_1, FDIFF_1, RFUNCT_2, FCONT_1, SIN_COS2, NAT_1, SIN_COS6, POWER, XXREAL_2, SEQ_4, RELSET_1, SEQ_2, INTEGRA1, COMSEQ_2, NUMBERS;
requirements HIDDEN, ARITHM, SUBSET, NUMERALS, BOOLE, REAL;
equalities SIN_COS, INTEGRA5, VALUED_1, SQUARE_1, SUBSET_1, ORDINAL1;
expansions INTEGRA5;
Lm1:
sin (PI / 4) > 0
Lm2:
sin (- (PI / 4)) < 0
Lm3:
cos (PI / 4) > 0
Lm4:
for f1, f2 being PartFunc of REAL,REAL holds (- f1) (#) (- f2) = f1 (#) f2
reconsider jj = 1 as Element of REAL by XREAL_0:def 1;
Lm5:
dom sin = REAL
by FUNCT_2:def 1;
Lm6:
dom cos = REAL
by FUNCT_2:def 1;
Lm7:
dom (- sin) = REAL
by FUNCT_2:def 1;
Lm8:
dom exp_R = REAL
by FUNCT_2:def 1;
Lm9:
dom sinh = REAL
by FUNCT_2:def 1;
Lm10:
dom cosh = REAL
by FUNCT_2:def 1;
Lm11:
for A being non empty closed_interval Subset of REAL holds
( cos is_integrable_on A & cos | A is bounded )
Lm12:
for A being non empty closed_interval Subset of REAL holds
( - sin is_integrable_on A & (- sin) | A is bounded )
Lm13:
for A being non empty closed_interval Subset of REAL holds
( exp_R is_integrable_on A & exp_R | A is bounded )
reconsider jj = 1 as Real ;
Lm14:
for A being non empty closed_interval Subset of REAL holds sinh | A is continuous
Lm15:
for A being non empty closed_interval Subset of REAL holds
( sinh is_integrable_on A & sinh | A is bounded )
by Lm14, Lm9, INTEGRA5:10, INTEGRA5:11;
Lm16:
for A being non empty closed_interval Subset of REAL holds cosh | A is continuous
Lm17:
for A being non empty closed_interval Subset of REAL holds
( cosh is_integrable_on A & cosh | A is bounded )
by Lm16, Lm10, INTEGRA5:10, INTEGRA5:11;
Lm18:
dom (arcsin `| ].(- 1),1.[) = ].(- 1),1.[
by FDIFF_1:def 7, SIN_COS6:83;
Lm19:
for A being non empty closed_interval Subset of REAL holds
( sin is_integrable_on A & sin | A is bounded )
Lm20:
for A being non empty closed_interval Subset of REAL holds
( cos (#) cos is_integrable_on A & (cos (#) cos) | A is bounded )
Lm21:
for A being non empty closed_interval Subset of REAL holds
( exp_R (#) (sin + cos) is_integrable_on A & (exp_R (#) (sin + cos)) | A is bounded )
Lm22:
for A being non empty closed_interval Subset of REAL holds
( exp_R (#) (cos - sin) is_integrable_on A & (exp_R (#) (cos - sin)) | A is bounded )