:: INTEGR14 semantic presentation

REAL is non empty V51() V52() V53() V57() V62() set
NAT is V51() V52() V53() V54() V55() V56() V57() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V51() V57() V62() set
K20(NAT,REAL) is V1() V34() V35() V36() set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is V1() V34() set
K19(K20(NAT,COMPLEX)) is set
K20(COMPLEX,COMPLEX) is V1() V34() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(REAL,REAL) is V1() V34() V35() V36() set
K19(K20(REAL,REAL)) is set
PFuncs (REAL,REAL) is set
K20(NAT,(PFuncs (REAL,REAL))) is V1() set
K19(K20(NAT,(PFuncs (REAL,REAL)))) is set
ExtREAL is non empty V52() set
RAT is non empty V51() V52() V53() V54() V57() V62() set
INT is non empty V51() V52() V53() V54() V55() V57() V62() set
NAT is V51() V52() V53() V54() V55() V56() V57() set
K19(NAT) is set
K19(NAT) is set
K20(COMPLEX,REAL) is V1() V34() V35() V36() set
K19(K20(COMPLEX,REAL)) is set
{} is set
the V1() V2() V3() V5( RAT ) empty V34() V35() V36() V37() V51() V52() V53() V54() V55() V56() V57() set is V1() V2() V3() V5( RAT ) empty V34() V35() V36() V37() V51() V52() V53() V54() V55() V56() V57() set
1 is V27() V28() V29() V30() ext-real V50() V51() V52() V53() V54() V55() V56() Element of NAT
{{},1} is set
0 is V27() V28() V29() V30() ext-real V50() V51() V52() V53() V54() V55() V56() Element of NAT
{0} is V51() V52() V53() V54() V55() V56() set
sin is V1() V4( REAL ) V5( REAL ) V6() V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
dom sin is V51() V52() V53() Element of K19(REAL)
cos is V1() V4( REAL ) V5( REAL ) V6() V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
dom cos is V51() V52() V53() Element of K19(REAL)
sin / cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
tan is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom tan is V51() V52() V53() Element of K19(REAL)
cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sin ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
exp_R is V1() V4( REAL ) V5( REAL ) V6() V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
sec * exp_R is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec * exp_R) is V51() V52() V53() Element of K19(REAL)
cosec * exp_R is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cosec * exp_R) is V51() V52() V53() Element of K19(REAL)
ln is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sec * ln is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec * ln) is V51() V52() V53() Element of K19(REAL)
cosec * ln is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cosec * ln) is V51() V52() V53() Element of K19(REAL)
exp_R * sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (exp_R * sec) is V51() V52() V53() Element of K19(REAL)
exp_R * cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (exp_R * cosec) is V51() V52() V53() Element of K19(REAL)
ln * sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln * sec) is V51() V52() V53() Element of K19(REAL)
ln * cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln * cosec) is V51() V52() V53() Element of K19(REAL)
exp_R (#) sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (exp_R (#) sec) is V51() V52() V53() Element of K19(REAL)
exp_R (#) cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (exp_R (#) cosec) is V51() V52() V53() Element of K19(REAL)
ln (#) sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln (#) sec) is V51() V52() V53() Element of K19(REAL)
ln (#) cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln (#) cosec) is V51() V52() V53() Element of K19(REAL)
sec * sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec * sin) is V51() V52() V53() Element of K19(REAL)
sec * cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec * cos) is V51() V52() V53() Element of K19(REAL)
cosec * sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cosec * sin) is V51() V52() V53() Element of K19(REAL)
cosec * cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cosec * cos) is V51() V52() V53() Element of K19(REAL)
sec * tan is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec * tan) is V51() V52() V53() Element of K19(REAL)
cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos / sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sec * cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec * cot) is V51() V52() V53() Element of K19(REAL)
cosec * tan is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cosec * tan) is V51() V52() V53() Element of K19(REAL)
cosec * cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cosec * cot) is V51() V52() V53() Element of K19(REAL)
tan (#) sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (tan (#) sec) is V51() V52() V53() Element of K19(REAL)
cot (#) sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cot (#) sec) is V51() V52() V53() Element of K19(REAL)
tan (#) cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (tan (#) cosec) is V51() V52() V53() Element of K19(REAL)
cot (#) cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cot (#) cosec) is V51() V52() V53() Element of K19(REAL)
tan * cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (tan * cot) is V51() V52() V53() Element of K19(REAL)
tan * tan is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (tan * tan) is V51() V52() V53() Element of K19(REAL)
cot * cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cot * cot) is V51() V52() V53() Element of K19(REAL)
cot * tan is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cot * tan) is V51() V52() V53() Element of K19(REAL)
tan - cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- cot is V1() V6() V34() set
K98(1) is V28() V29() V30() set
K98(1) (#) cot is V1() V6() set
tan + (- cot) is V1() V6() set
dom (tan - cot) is V51() V52() V53() Element of K19(REAL)
tan + cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (tan + cot) is V51() V52() V53() Element of K19(REAL)
sin * sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sin * cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos * sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos * cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos (#) cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cos (#) cot) is V51() V52() V53() Element of K19(REAL)
sin (#) tan is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sin (#) tan) is V51() V52() V53() Element of K19(REAL)
{0} is V51() V52() V53() V54() V55() V56() Element of K19(REAL)
A is V51() V52() V53() open Element of K19(REAL)
id A is V1() V4( REAL ) V4(A) V5( REAL ) V5(A) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(id A) " {0} is V51() V52() V53() Element of K19(REAL)
f is set
dom (id A) is V51() V52() V53() Element of K19(A)
K19(A) is set
(id A) . f is V28() V29() ext-real Element of REAL
f is set
(id A) . f is V28() V29() ext-real Element of REAL
dom (id A) is V51() V52() V53() Element of K19(A)
K19(A) is set
A is V51() V52() V53() open Element of K19(REAL)
id A is V1() V4( REAL ) V4(A) V5( REAL ) V5(A) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(id A) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sec * ((id A) ^) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec * ((id A) ^)) is V51() V52() V53() Element of K19(REAL)
- (sec * ((id A) ^)) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (sec * ((id A) ^)) is V1() V6() set
(- (sec * ((id A) ^))) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (sec * ((id A) ^))) is V51() V52() V53() Element of K19(REAL)
dom ((id A) ^) is V51() V52() V53() Element of K19(REAL)
dom (id A) is V51() V52() V53() Element of K19(A)
K19(A) is set
(id A) " {0} is V51() V52() V53() Element of K19(REAL)
(dom (id A)) \ ((id A) " {0}) is V51() V52() V53() Element of K19(A)
(dom (id A)) \ {0} is V51() V52() V53() Element of K19(A)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (sec * ((id A) ^)) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (sec * ((id A) ^))) `| A) . f is V28() V29() ext-real Element of REAL
1 / f is V28() V29() ext-real Element of REAL
K99(f) is V28() set
K97(1,K99(f)) is set
sin . (1 / f) is V28() V29() ext-real Element of REAL
f ^2 is V28() V29() ext-real Element of REAL
cos . (1 / f) is V28() V29() ext-real Element of REAL
(cos . (1 / f)) ^2 is V28() V29() ext-real Element of REAL
(f ^2) * ((cos . (1 / f)) ^2) is V28() V29() ext-real Element of REAL
(sin . (1 / f)) / ((f ^2) * ((cos . (1 / f)) ^2)) is V28() V29() ext-real Element of REAL
K99(((f ^2) * ((cos . (1 / f)) ^2))) is V28() set
K97((sin . (1 / f)),K99(((f ^2) * ((cos . (1 / f)) ^2)))) is set
(sec * ((id A) ^)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((sec * ((id A) ^)) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((sec * ((id A) ^)) `| A)) . f is V28() V29() ext-real Element of REAL
((sec * ((id A) ^)) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((sec * ((id A) ^)) `| A) . f) is V28() V29() ext-real Element of REAL
- ((sin . (1 / f)) / ((f ^2) * ((cos . (1 / f)) ^2))) is V28() V29() ext-real Element of REAL
(- 1) * (- ((sin . (1 / f)) / ((f ^2) * ((cos . (1 / f)) ^2)))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (sec * ((id A) ^))) `| A) . f is V28() V29() ext-real Element of REAL
1 / f is V28() V29() ext-real Element of REAL
K99(f) is V28() set
K97(1,K99(f)) is set
sin . (1 / f) is V28() V29() ext-real Element of REAL
f ^2 is V28() V29() ext-real Element of REAL
cos . (1 / f) is V28() V29() ext-real Element of REAL
(cos . (1 / f)) ^2 is V28() V29() ext-real Element of REAL
(f ^2) * ((cos . (1 / f)) ^2) is V28() V29() ext-real Element of REAL
(sin . (1 / f)) / ((f ^2) * ((cos . (1 / f)) ^2)) is V28() V29() ext-real Element of REAL
K99(((f ^2) * ((cos . (1 / f)) ^2))) is V28() set
K97((sin . (1 / f)),K99(((f ^2) * ((cos . (1 / f)) ^2)))) is set
- (cosec * exp_R) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cosec * exp_R) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (cosec * exp_R)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (cosec * exp_R)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cosec * exp_R) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (cosec * exp_R)) `| A) . f is V28() V29() ext-real Element of REAL
exp_R . f is V28() V29() ext-real Element of REAL
cos . (exp_R . f) is V28() V29() ext-real Element of REAL
(exp_R . f) * (cos . (exp_R . f)) is V28() V29() ext-real Element of REAL
sin . (exp_R . f) is V28() V29() ext-real Element of REAL
(sin . (exp_R . f)) ^2 is V28() V29() ext-real Element of REAL
((exp_R . f) * (cos . (exp_R . f))) / ((sin . (exp_R . f)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (exp_R . f)) ^2)) is V28() set
K97(((exp_R . f) * (cos . (exp_R . f))),K99(((sin . (exp_R . f)) ^2))) is set
(cosec * exp_R) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((cosec * exp_R) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((cosec * exp_R) `| A)) . f is V28() V29() ext-real Element of REAL
((cosec * exp_R) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((cosec * exp_R) `| A) . f) is V28() V29() ext-real Element of REAL
- (((exp_R . f) * (cos . (exp_R . f))) / ((sin . (exp_R . f)) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * (- (((exp_R . f) * (cos . (exp_R . f))) / ((sin . (exp_R . f)) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (cosec * exp_R)) `| A) . f is V28() V29() ext-real Element of REAL
exp_R . f is V28() V29() ext-real Element of REAL
cos . (exp_R . f) is V28() V29() ext-real Element of REAL
(exp_R . f) * (cos . (exp_R . f)) is V28() V29() ext-real Element of REAL
sin . (exp_R . f) is V28() V29() ext-real Element of REAL
(sin . (exp_R . f)) ^2 is V28() V29() ext-real Element of REAL
((exp_R . f) * (cos . (exp_R . f))) / ((sin . (exp_R . f)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (exp_R . f)) ^2)) is V28() set
K97(((exp_R . f) * (cos . (exp_R . f))),K99(((sin . (exp_R . f)) ^2))) is set
- (cosec * ln) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cosec * ln) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (cosec * ln)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (cosec * ln)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cosec * ln) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (cosec * ln)) `| A) . f is V28() V29() ext-real Element of REAL
ln . f is V28() V29() ext-real Element of REAL
cos . (ln . f) is V28() V29() ext-real Element of REAL
sin . (ln . f) is V28() V29() ext-real Element of REAL
(sin . (ln . f)) ^2 is V28() V29() ext-real Element of REAL
f * ((sin . (ln . f)) ^2) is V28() V29() ext-real Element of REAL
(cos . (ln . f)) / (f * ((sin . (ln . f)) ^2)) is V28() V29() ext-real Element of REAL
K99((f * ((sin . (ln . f)) ^2))) is V28() set
K97((cos . (ln . f)),K99((f * ((sin . (ln . f)) ^2)))) is set
(cosec * ln) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((cosec * ln) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((cosec * ln) `| A)) . f is V28() V29() ext-real Element of REAL
((cosec * ln) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((cosec * ln) `| A) . f) is V28() V29() ext-real Element of REAL
- ((cos . (ln . f)) / (f * ((sin . (ln . f)) ^2))) is V28() V29() ext-real Element of REAL
(- 1) * (- ((cos . (ln . f)) / (f * ((sin . (ln . f)) ^2)))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (cosec * ln)) `| A) . f is V28() V29() ext-real Element of REAL
ln . f is V28() V29() ext-real Element of REAL
cos . (ln . f) is V28() V29() ext-real Element of REAL
sin . (ln . f) is V28() V29() ext-real Element of REAL
(sin . (ln . f)) ^2 is V28() V29() ext-real Element of REAL
f * ((sin . (ln . f)) ^2) is V28() V29() ext-real Element of REAL
(cos . (ln . f)) / (f * ((sin . (ln . f)) ^2)) is V28() V29() ext-real Element of REAL
K99((f * ((sin . (ln . f)) ^2))) is V28() set
K97((cos . (ln . f)),K99((f * ((sin . (ln . f)) ^2)))) is set
- (exp_R * cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (exp_R * cosec) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (exp_R * cosec)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (exp_R * cosec)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (exp_R * cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (exp_R * cosec)) `| A) . f is V28() V29() ext-real Element of REAL
cosec . f is V28() V29() ext-real Element of REAL
exp_R . (cosec . f) is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
(exp_R . (cosec . f)) * (cos . f) is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
((exp_R . (cosec . f)) * (cos . f)) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97(((exp_R . (cosec . f)) * (cos . f)),K99(((sin . f) ^2))) is set
(exp_R * cosec) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((exp_R * cosec) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((exp_R * cosec) `| A)) . f is V28() V29() ext-real Element of REAL
((exp_R * cosec) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((exp_R * cosec) `| A) . f) is V28() V29() ext-real Element of REAL
- (((exp_R . (cosec . f)) * (cos . f)) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * (- (((exp_R . (cosec . f)) * (cos . f)) / ((sin . f) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (exp_R * cosec)) `| A) . f is V28() V29() ext-real Element of REAL
cosec . f is V28() V29() ext-real Element of REAL
exp_R . (cosec . f) is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
(exp_R . (cosec . f)) * (cos . f) is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
((exp_R . (cosec . f)) * (cos . f)) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97(((exp_R . (cosec . f)) * (cos . f)),K99(((sin . f) ^2))) is set
- (ln * cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (ln * cosec) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (ln * cosec)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (ln * cosec)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (ln * cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
dom cosec is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
((- (ln * cosec)) `| A) . f is V28() V29() ext-real Element of REAL
cot . f is V28() V29() ext-real Element of REAL
(ln * cosec) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((ln * cosec) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((ln * cosec) `| A)) . f is V28() V29() ext-real Element of REAL
((ln * cosec) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((ln * cosec) `| A) . f) is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(cos . f) / (sin . f) is V28() V29() ext-real Element of REAL
K99((sin . f)) is V28() set
K97((cos . f),K99((sin . f))) is set
- ((cos . f) / (sin . f)) is V28() V29() ext-real Element of REAL
(- 1) * (- ((cos . f) / (sin . f))) is V28() V29() ext-real Element of REAL
cot f is V28() V29() ext-real Element of REAL
cos f is set
sin f is set
K101((cos f),(sin f)) is set
f is V28() V29() ext-real Element of REAL
((- (ln * cosec)) `| A) . f is V28() V29() ext-real Element of REAL
cot . f is V28() V29() ext-real Element of REAL
A is V27() V29() V30() ext-real set
#Z A is V1() V4( REAL ) V5( REAL ) V6() V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
(#Z A) * cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((#Z A) * cosec) is V51() V52() V53() Element of K19(REAL)
- ((#Z A) * cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) ((#Z A) * cosec) is V1() V6() set
A + 1 is V28() V29() V30() ext-real Element of REAL
f is V51() V52() V53() open Element of K19(REAL)
(- ((#Z A) * cosec)) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- ((#Z A) * cosec)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) ((#Z A) * cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V28() V29() ext-real Element of REAL
((- ((#Z A) * cosec)) `| f) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
A * (cos . Z) is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
(sin . Z) #Z (A + 1) is V28() V29() ext-real Element of REAL
(A * (cos . Z)) / ((sin . Z) #Z (A + 1)) is V28() V29() ext-real Element of REAL
K99(((sin . Z) #Z (A + 1))) is V28() set
K97((A * (cos . Z)),K99(((sin . Z) #Z (A + 1)))) is set
((#Z A) * cosec) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) (((#Z A) * cosec) `| f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) (((#Z A) * cosec) `| f)) . Z is V28() V29() ext-real Element of REAL
(((#Z A) * cosec) `| f) . Z is V28() V29() ext-real Element of REAL
(- 1) * ((((#Z A) * cosec) `| f) . Z) is V28() V29() ext-real Element of REAL
- ((A * (cos . Z)) / ((sin . Z) #Z (A + 1))) is V28() V29() ext-real Element of REAL
(- 1) * (- ((A * (cos . Z)) / ((sin . Z) #Z (A + 1)))) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
((- ((#Z A) * cosec)) `| f) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
A * (cos . Z) is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
(sin . Z) #Z (A + 1) is V28() V29() ext-real Element of REAL
(A * (cos . Z)) / ((sin . Z) #Z (A + 1)) is V28() V29() ext-real Element of REAL
K99(((sin . Z) #Z (A + 1))) is V28() set
K97((A * (cos . Z)),K99(((sin . Z) #Z (A + 1)))) is set
A is V51() V52() V53() open Element of K19(REAL)
id A is V1() V4( REAL ) V4(A) V5( REAL ) V5(A) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(id A) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id A) ^) (#) sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id A) ^) (#) sec) is V51() V52() V53() Element of K19(REAL)
- (((id A) ^) (#) sec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (((id A) ^) (#) sec) is V1() V6() set
(- (((id A) ^) (#) sec)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (((id A) ^) (#) sec)) is V51() V52() V53() Element of K19(REAL)
dom ((id A) ^) is V51() V52() V53() Element of K19(REAL)
dom sec is V51() V52() V53() Element of K19(REAL)
(dom ((id A) ^)) /\ (dom sec) is V51() V52() V53() Element of K19(REAL)
dom (id A) is V51() V52() V53() Element of K19(A)
K19(A) is set
(id A) " {0} is V51() V52() V53() Element of K19(REAL)
(dom (id A)) \ ((id A) " {0}) is V51() V52() V53() Element of K19(A)
(dom (id A)) \ {0} is V51() V52() V53() Element of K19(A)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (((id A) ^) (#) sec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (((id A) ^) (#) sec)) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
1 / (cos . f) is V28() V29() ext-real Element of REAL
K99((cos . f)) is V28() set
K97(1,K99((cos . f))) is set
f ^2 is V28() V29() ext-real Element of REAL
(1 / (cos . f)) / (f ^2) is V28() V29() ext-real Element of REAL
K99((f ^2)) is V28() set
K97((1 / (cos . f)),K99((f ^2))) is set
sin . f is V28() V29() ext-real Element of REAL
(sin . f) / f is V28() V29() ext-real Element of REAL
K99(f) is V28() set
K97((sin . f),K99(f)) is set
(cos . f) ^2 is V28() V29() ext-real Element of REAL
((sin . f) / f) / ((cos . f) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . f) ^2)) is V28() set
K97(((sin . f) / f),K99(((cos . f) ^2))) is set
((1 / (cos . f)) / (f ^2)) - (((sin . f) / f) / ((cos . f) ^2)) is V28() V29() ext-real Element of REAL
K98((((sin . f) / f) / ((cos . f) ^2))) is V28() set
K96(((1 / (cos . f)) / (f ^2)),K98((((sin . f) / f) / ((cos . f) ^2)))) is set
(((id A) ^) (#) sec) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((((id A) ^) (#) sec) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((((id A) ^) (#) sec) `| A)) . f is V28() V29() ext-real Element of REAL
((((id A) ^) (#) sec) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((((id A) ^) (#) sec) `| A) . f) is V28() V29() ext-real Element of REAL
- ((1 / (cos . f)) / (f ^2)) is V28() V29() ext-real Element of REAL
(- ((1 / (cos . f)) / (f ^2))) + (((sin . f) / f) / ((cos . f) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * ((- ((1 / (cos . f)) / (f ^2))) + (((sin . f) / f) / ((cos . f) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (((id A) ^) (#) sec)) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
1 / (cos . f) is V28() V29() ext-real Element of REAL
K99((cos . f)) is V28() set
K97(1,K99((cos . f))) is set
f ^2 is V28() V29() ext-real Element of REAL
(1 / (cos . f)) / (f ^2) is V28() V29() ext-real Element of REAL
K99((f ^2)) is V28() set
K97((1 / (cos . f)),K99((f ^2))) is set
sin . f is V28() V29() ext-real Element of REAL
(sin . f) / f is V28() V29() ext-real Element of REAL
K99(f) is V28() set
K97((sin . f),K99(f)) is set
(cos . f) ^2 is V28() V29() ext-real Element of REAL
((sin . f) / f) / ((cos . f) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . f) ^2)) is V28() set
K97(((sin . f) / f),K99(((cos . f) ^2))) is set
((1 / (cos . f)) / (f ^2)) - (((sin . f) / f) / ((cos . f) ^2)) is V28() V29() ext-real Element of REAL
K98((((sin . f) / f) / ((cos . f) ^2))) is V28() set
K96(((1 / (cos . f)) / (f ^2)),K98((((sin . f) / f) / ((cos . f) ^2)))) is set
A is V51() V52() V53() open Element of K19(REAL)
id A is V1() V4( REAL ) V4(A) V5( REAL ) V5(A) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(id A) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id A) ^) (#) cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id A) ^) (#) cosec) is V51() V52() V53() Element of K19(REAL)
- (((id A) ^) (#) cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (((id A) ^) (#) cosec) is V1() V6() set
(- (((id A) ^) (#) cosec)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (((id A) ^) (#) cosec)) is V51() V52() V53() Element of K19(REAL)
dom ((id A) ^) is V51() V52() V53() Element of K19(REAL)
dom cosec is V51() V52() V53() Element of K19(REAL)
(dom ((id A) ^)) /\ (dom cosec) is V51() V52() V53() Element of K19(REAL)
dom (id A) is V51() V52() V53() Element of K19(A)
K19(A) is set
(id A) " {0} is V51() V52() V53() Element of K19(REAL)
(dom (id A)) \ ((id A) " {0}) is V51() V52() V53() Element of K19(A)
(dom (id A)) \ {0} is V51() V52() V53() Element of K19(A)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (((id A) ^) (#) cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (((id A) ^) (#) cosec)) `| A) . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
1 / (sin . f) is V28() V29() ext-real Element of REAL
K99((sin . f)) is V28() set
K97(1,K99((sin . f))) is set
f ^2 is V28() V29() ext-real Element of REAL
(1 / (sin . f)) / (f ^2) is V28() V29() ext-real Element of REAL
K99((f ^2)) is V28() set
K97((1 / (sin . f)),K99((f ^2))) is set
cos . f is V28() V29() ext-real Element of REAL
(cos . f) / f is V28() V29() ext-real Element of REAL
K99(f) is V28() set
K97((cos . f),K99(f)) is set
(sin . f) ^2 is V28() V29() ext-real Element of REAL
((cos . f) / f) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97(((cos . f) / f),K99(((sin . f) ^2))) is set
((1 / (sin . f)) / (f ^2)) + (((cos . f) / f) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
(((id A) ^) (#) cosec) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((((id A) ^) (#) cosec) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((((id A) ^) (#) cosec) `| A)) . f is V28() V29() ext-real Element of REAL
((((id A) ^) (#) cosec) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((((id A) ^) (#) cosec) `| A) . f) is V28() V29() ext-real Element of REAL
- ((1 / (sin . f)) / (f ^2)) is V28() V29() ext-real Element of REAL
(- ((1 / (sin . f)) / (f ^2))) - (((cos . f) / f) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
K98((((cos . f) / f) / ((sin . f) ^2))) is V28() set
K96((- ((1 / (sin . f)) / (f ^2))),K98((((cos . f) / f) / ((sin . f) ^2)))) is set
(- 1) * ((- ((1 / (sin . f)) / (f ^2))) - (((cos . f) / f) / ((sin . f) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (((id A) ^) (#) cosec)) `| A) . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
1 / (sin . f) is V28() V29() ext-real Element of REAL
K99((sin . f)) is V28() set
K97(1,K99((sin . f))) is set
f ^2 is V28() V29() ext-real Element of REAL
(1 / (sin . f)) / (f ^2) is V28() V29() ext-real Element of REAL
K99((f ^2)) is V28() set
K97((1 / (sin . f)),K99((f ^2))) is set
cos . f is V28() V29() ext-real Element of REAL
(cos . f) / f is V28() V29() ext-real Element of REAL
K99(f) is V28() set
K97((cos . f),K99(f)) is set
(sin . f) ^2 is V28() V29() ext-real Element of REAL
((cos . f) / f) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97(((cos . f) / f),K99(((sin . f) ^2))) is set
((1 / (sin . f)) / (f ^2)) + (((cos . f) / f) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
- (cosec * sin) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cosec * sin) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (cosec * sin)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (cosec * sin)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cosec * sin) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (cosec * sin)) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
cos . (sin . f) is V28() V29() ext-real Element of REAL
(cos . f) * (cos . (sin . f)) is V28() V29() ext-real Element of REAL
sin . (sin . f) is V28() V29() ext-real Element of REAL
(sin . (sin . f)) ^2 is V28() V29() ext-real Element of REAL
((cos . f) * (cos . (sin . f))) / ((sin . (sin . f)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (sin . f)) ^2)) is V28() set
K97(((cos . f) * (cos . (sin . f))),K99(((sin . (sin . f)) ^2))) is set
(cosec * sin) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((cosec * sin) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((cosec * sin) `| A)) . f is V28() V29() ext-real Element of REAL
((cosec * sin) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((cosec * sin) `| A) . f) is V28() V29() ext-real Element of REAL
- (((cos . f) * (cos . (sin . f))) / ((sin . (sin . f)) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * (- (((cos . f) * (cos . (sin . f))) / ((sin . (sin . f)) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (cosec * sin)) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
cos . (sin . f) is V28() V29() ext-real Element of REAL
(cos . f) * (cos . (sin . f)) is V28() V29() ext-real Element of REAL
sin . (sin . f) is V28() V29() ext-real Element of REAL
(sin . (sin . f)) ^2 is V28() V29() ext-real Element of REAL
((cos . f) * (cos . (sin . f))) / ((sin . (sin . f)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (sin . f)) ^2)) is V28() set
K97(((cos . f) * (cos . (sin . f))),K99(((sin . (sin . f)) ^2))) is set
- (sec * cot) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (sec * cot) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (sec * cot)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (sec * cot)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (sec * cot) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (sec * cot)) `| A) . f is V28() V29() ext-real Element of REAL
cot . f is V28() V29() ext-real Element of REAL
sin . (cot . f) is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
(sin . (cot . f)) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97((sin . (cot . f)),K99(((sin . f) ^2))) is set
cos . (cot . f) is V28() V29() ext-real Element of REAL
(cos . (cot . f)) ^2 is V28() V29() ext-real Element of REAL
((sin . (cot . f)) / ((sin . f) ^2)) / ((cos . (cot . f)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (cot . f)) ^2)) is V28() set
K97(((sin . (cot . f)) / ((sin . f) ^2)),K99(((cos . (cot . f)) ^2))) is set
(sec * cot) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((sec * cot) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((sec * cot) `| A)) . f is V28() V29() ext-real Element of REAL
((sec * cot) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((sec * cot) `| A) . f) is V28() V29() ext-real Element of REAL
- (((sin . (cot . f)) / ((sin . f) ^2)) / ((cos . (cot . f)) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * (- (((sin . (cot . f)) / ((sin . f) ^2)) / ((cos . (cot . f)) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (sec * cot)) `| A) . f is V28() V29() ext-real Element of REAL
cot . f is V28() V29() ext-real Element of REAL
sin . (cot . f) is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
(sin . (cot . f)) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97((sin . (cot . f)),K99(((sin . f) ^2))) is set
cos . (cot . f) is V28() V29() ext-real Element of REAL
(cos . (cot . f)) ^2 is V28() V29() ext-real Element of REAL
((sin . (cot . f)) / ((sin . f) ^2)) / ((cos . (cot . f)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (cot . f)) ^2)) is V28() set
K97(((sin . (cot . f)) / ((sin . f) ^2)),K99(((cos . (cot . f)) ^2))) is set
- (cosec * tan) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cosec * tan) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (cosec * tan)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (cosec * tan)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cosec * tan) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
tan . f is V28() V29() ext-real Element of REAL
sin . (tan . f) is V28() V29() ext-real Element of REAL
dom cosec is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
((- (cosec * tan)) `| A) . f is V28() V29() ext-real Element of REAL
tan . f is V28() V29() ext-real Element of REAL
cos . (tan . f) is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
(cos . f) ^2 is V28() V29() ext-real Element of REAL
(cos . (tan . f)) / ((cos . f) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . f) ^2)) is V28() set
K97((cos . (tan . f)),K99(((cos . f) ^2))) is set
sin . (tan . f) is V28() V29() ext-real Element of REAL
(sin . (tan . f)) ^2 is V28() V29() ext-real Element of REAL
((cos . (tan . f)) / ((cos . f) ^2)) / ((sin . (tan . f)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (tan . f)) ^2)) is V28() set
K97(((cos . (tan . f)) / ((cos . f) ^2)),K99(((sin . (tan . f)) ^2))) is set
diff ((- (cosec * tan)),f) is V28() V29() ext-real Element of REAL
diff ((cosec * tan),f) is V28() V29() ext-real Element of REAL
(- 1) * (diff ((cosec * tan),f)) is V28() V29() ext-real Element of REAL
diff (cosec,(tan . f)) is V28() V29() ext-real Element of REAL
diff (tan,f) is V28() V29() ext-real Element of REAL
(diff (cosec,(tan . f))) * (diff (tan,f)) is V28() V29() ext-real Element of REAL
(- 1) * ((diff (cosec,(tan . f))) * (diff (tan,f))) is V28() V29() ext-real Element of REAL
(cos . (tan . f)) / ((sin . (tan . f)) ^2) is V28() V29() ext-real Element of REAL
K97((cos . (tan . f)),K99(((sin . (tan . f)) ^2))) is set
- ((cos . (tan . f)) / ((sin . (tan . f)) ^2)) is V28() V29() ext-real Element of REAL
(- ((cos . (tan . f)) / ((sin . (tan . f)) ^2))) * (diff (tan,f)) is V28() V29() ext-real Element of REAL
(- 1) * ((- ((cos . (tan . f)) / ((sin . (tan . f)) ^2))) * (diff (tan,f))) is V28() V29() ext-real Element of REAL
1 / ((cos . f) ^2) is V28() V29() ext-real Element of REAL
K97(1,K99(((cos . f) ^2))) is set
(1 / ((cos . f) ^2)) * (- ((cos . (tan . f)) / ((sin . (tan . f)) ^2))) is V28() V29() ext-real Element of REAL
(- 1) * ((1 / ((cos . f) ^2)) * (- ((cos . (tan . f)) / ((sin . (tan . f)) ^2)))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (cosec * tan)) `| A) . f is V28() V29() ext-real Element of REAL
tan . f is V28() V29() ext-real Element of REAL
cos . (tan . f) is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
(cos . f) ^2 is V28() V29() ext-real Element of REAL
(cos . (tan . f)) / ((cos . f) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . f) ^2)) is V28() set
K97((cos . (tan . f)),K99(((cos . f) ^2))) is set
sin . (tan . f) is V28() V29() ext-real Element of REAL
(sin . (tan . f)) ^2 is V28() V29() ext-real Element of REAL
((cos . (tan . f)) / ((cos . f) ^2)) / ((sin . (tan . f)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (tan . f)) ^2)) is V28() set
K97(((cos . (tan . f)) / ((cos . f) ^2)),K99(((sin . (tan . f)) ^2))) is set
- (cot (#) sec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cot (#) sec) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (cot (#) sec)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (cot (#) sec)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cot (#) sec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (cot (#) sec)) `| A) . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97(1,K99(((sin . f) ^2))) is set
cos . f is V28() V29() ext-real Element of REAL
(1 / ((sin . f) ^2)) / (cos . f) is V28() V29() ext-real Element of REAL
K99((cos . f)) is V28() set
K97((1 / ((sin . f) ^2)),K99((cos . f))) is set
cot . f is V28() V29() ext-real Element of REAL
(cot . f) * (sin . f) is V28() V29() ext-real Element of REAL
(cos . f) ^2 is V28() V29() ext-real Element of REAL
((cot . f) * (sin . f)) / ((cos . f) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . f) ^2)) is V28() set
K97(((cot . f) * (sin . f)),K99(((cos . f) ^2))) is set
((1 / ((sin . f) ^2)) / (cos . f)) - (((cot . f) * (sin . f)) / ((cos . f) ^2)) is V28() V29() ext-real Element of REAL
K98((((cot . f) * (sin . f)) / ((cos . f) ^2))) is V28() set
K96(((1 / ((sin . f) ^2)) / (cos . f)),K98((((cot . f) * (sin . f)) / ((cos . f) ^2)))) is set
(cot (#) sec) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((cot (#) sec) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((cot (#) sec) `| A)) . f is V28() V29() ext-real Element of REAL
((cot (#) sec) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((cot (#) sec) `| A) . f) is V28() V29() ext-real Element of REAL
- ((1 / ((sin . f) ^2)) / (cos . f)) is V28() V29() ext-real Element of REAL
(- ((1 / ((sin . f) ^2)) / (cos . f))) + (((cot . f) * (sin . f)) / ((cos . f) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * ((- ((1 / ((sin . f) ^2)) / (cos . f))) + (((cot . f) * (sin . f)) / ((cos . f) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (cot (#) sec)) `| A) . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97(1,K99(((sin . f) ^2))) is set
cos . f is V28() V29() ext-real Element of REAL
(1 / ((sin . f) ^2)) / (cos . f) is V28() V29() ext-real Element of REAL
K99((cos . f)) is V28() set
K97((1 / ((sin . f) ^2)),K99((cos . f))) is set
cot . f is V28() V29() ext-real Element of REAL
(cot . f) * (sin . f) is V28() V29() ext-real Element of REAL
(cos . f) ^2 is V28() V29() ext-real Element of REAL
((cot . f) * (sin . f)) / ((cos . f) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . f) ^2)) is V28() set
K97(((cot . f) * (sin . f)),K99(((cos . f) ^2))) is set
((1 / ((sin . f) ^2)) / (cos . f)) - (((cot . f) * (sin . f)) / ((cos . f) ^2)) is V28() V29() ext-real Element of REAL
K98((((cot . f) * (sin . f)) / ((cos . f) ^2))) is V28() set
K96(((1 / ((sin . f) ^2)) / (cos . f)),K98((((cot . f) * (sin . f)) / ((cos . f) ^2)))) is set
- (cot (#) cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cot (#) cosec) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (cot (#) cosec)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (cot (#) cosec)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cot (#) cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (cot (#) cosec)) `| A) . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97(1,K99(((sin . f) ^2))) is set
(1 / ((sin . f) ^2)) / (sin . f) is V28() V29() ext-real Element of REAL
K99((sin . f)) is V28() set
K97((1 / ((sin . f) ^2)),K99((sin . f))) is set
cot . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
(cot . f) * (cos . f) is V28() V29() ext-real Element of REAL
((cot . f) * (cos . f)) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K97(((cot . f) * (cos . f)),K99(((sin . f) ^2))) is set
((1 / ((sin . f) ^2)) / (sin . f)) + (((cot . f) * (cos . f)) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
(cot (#) cosec) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((cot (#) cosec) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((cot (#) cosec) `| A)) . f is V28() V29() ext-real Element of REAL
((cot (#) cosec) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((cot (#) cosec) `| A) . f) is V28() V29() ext-real Element of REAL
- ((1 / ((sin . f) ^2)) / (sin . f)) is V28() V29() ext-real Element of REAL
(- ((1 / ((sin . f) ^2)) / (sin . f))) - (((cot . f) * (cos . f)) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
K98((((cot . f) * (cos . f)) / ((sin . f) ^2))) is V28() set
K96((- ((1 / ((sin . f) ^2)) / (sin . f))),K98((((cot . f) * (cos . f)) / ((sin . f) ^2)))) is set
(- 1) * ((- ((1 / ((sin . f) ^2)) / (sin . f))) - (((cot . f) * (cos . f)) / ((sin . f) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (cot (#) cosec)) `| A) . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97(1,K99(((sin . f) ^2))) is set
(1 / ((sin . f) ^2)) / (sin . f) is V28() V29() ext-real Element of REAL
K99((sin . f)) is V28() set
K97((1 / ((sin . f) ^2)),K99((sin . f))) is set
cot . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
(cot . f) * (cos . f) is V28() V29() ext-real Element of REAL
((cot . f) * (cos . f)) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K97(((cot . f) * (cos . f)),K99(((sin . f) ^2))) is set
((1 / ((sin . f) ^2)) / (sin . f)) + (((cot . f) * (cos . f)) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
- (cos (#) cot) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cos (#) cot) is V1() V6() set
A is V51() V52() V53() open Element of K19(REAL)
(- (cos (#) cot)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (- (cos (#) cot)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cos (#) cot) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- (cos (#) cot)) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
(cos . f) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97((cos . f),K99(((sin . f) ^2))) is set
(cos . f) + ((cos . f) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
(cos (#) cot) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((cos (#) cot) `| A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((cos (#) cot) `| A)) . f is V28() V29() ext-real Element of REAL
((cos (#) cot) `| A) . f is V28() V29() ext-real Element of REAL
(- 1) * (((cos (#) cot) `| A) . f) is V28() V29() ext-real Element of REAL
- (cos . f) is V28() V29() ext-real Element of REAL
(- (cos . f)) - ((cos . f) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
K98(((cos . f) / ((sin . f) ^2))) is V28() set
K96((- (cos . f)),K98(((cos . f) / ((sin . f) ^2)))) is set
(- 1) * ((- (cos . f)) - ((cos . f) / ((sin . f) ^2))) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- (cos (#) cot)) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
(cos . f) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . f) ^2)) is V28() set
K97((cos . f),K99(((sin . f) ^2))) is set
(cos . f) + ((cos . f) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V4(Z) V5( REAL ) V5(Z) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(id Z) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sec * ((id Z) ^) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec * ((id Z) ^)) is V51() V52() V53() Element of K19(REAL)
- (sec * ((id Z) ^)) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (sec * ((id Z) ^)) is V1() V6() set
(- (sec * ((id Z) ^))) . (upper_bound A) is V28() V29() ext-real Element of REAL
(- (sec * ((id Z) ^))) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (sec * ((id Z) ^))) . (upper_bound A)) - ((- (sec * ((id Z) ^))) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (sec * ((id Z) ^))) . (lower_bound A))) is V28() set
K96(((- (sec * ((id Z) ^))) . (upper_bound A)),K98(((- (sec * ((id Z) ^))) . (lower_bound A)))) is set
(- (sec * ((id Z) ^))) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (sec * ((id Z) ^))) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (sec * ((id Z) ^))) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
1 / x is V28() V29() ext-real Element of REAL
K99(x) is V28() set
K97(1,K99(x)) is set
sin . (1 / x) is V28() V29() ext-real Element of REAL
x ^2 is V28() V29() ext-real Element of REAL
cos . (1 / x) is V28() V29() ext-real Element of REAL
(cos . (1 / x)) ^2 is V28() V29() ext-real Element of REAL
(x ^2) * ((cos . (1 / x)) ^2) is V28() V29() ext-real Element of REAL
(sin . (1 / x)) / ((x ^2) * ((cos . (1 / x)) ^2)) is V28() V29() ext-real Element of REAL
K99(((x ^2) * ((cos . (1 / x)) ^2))) is V28() set
K97((sin . (1 / x)),K99(((x ^2) * ((cos . (1 / x)) ^2)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V4(Z) V5( REAL ) V5(Z) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(id Z) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cosec * ((id Z) ^) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (cosec * ((id Z) ^)) is V51() V52() V53() Element of K19(REAL)
(cosec * ((id Z) ^)) . (upper_bound A) is V28() V29() ext-real Element of REAL
(cosec * ((id Z) ^)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((cosec * ((id Z) ^)) . (upper_bound A)) - ((cosec * ((id Z) ^)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((cosec * ((id Z) ^)) . (lower_bound A))) is V28() set
K96(((cosec * ((id Z) ^)) . (upper_bound A)),K98(((cosec * ((id Z) ^)) . (lower_bound A)))) is set
dom ((id Z) ^) is V51() V52() V53() Element of K19(REAL)
dom (id Z) is V51() V52() V53() Element of K19(Z)
K19(Z) is set
(id Z) " {0} is V51() V52() V53() Element of K19(REAL)
(dom (id Z)) \ ((id Z) " {0}) is V51() V52() V53() Element of K19(Z)
(dom (id Z)) \ {0} is V51() V52() V53() Element of K19(Z)
(cosec * ((id Z) ^)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((cosec * ((id Z) ^)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((cosec * ((id Z) ^)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
1 / x is V28() V29() ext-real Element of REAL
K99(x) is V28() set
K97(1,K99(x)) is set
cos . (1 / x) is V28() V29() ext-real Element of REAL
x ^2 is V28() V29() ext-real Element of REAL
sin . (1 / x) is V28() V29() ext-real Element of REAL
(sin . (1 / x)) ^2 is V28() V29() ext-real Element of REAL
(x ^2) * ((sin . (1 / x)) ^2) is V28() V29() ext-real Element of REAL
(cos . (1 / x)) / ((x ^2) * ((sin . (1 / x)) ^2)) is V28() V29() ext-real Element of REAL
K99(((x ^2) * ((sin . (1 / x)) ^2))) is V28() set
K97((cos . (1 / x)),K99(((x ^2) * ((sin . (1 / x)) ^2)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(sec * exp_R) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(sec * exp_R) . (lower_bound A) is V28() V29() ext-real Element of REAL
((sec * exp_R) . (upper_bound A)) - ((sec * exp_R) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((sec * exp_R) . (lower_bound A))) is V28() set
K96(((sec * exp_R) . (upper_bound A)),K98(((sec * exp_R) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(sec * exp_R) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((sec * exp_R) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((sec * exp_R) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
exp_R . x is V28() V29() ext-real Element of REAL
sin . (exp_R . x) is V28() V29() ext-real Element of REAL
(exp_R . x) * (sin . (exp_R . x)) is V28() V29() ext-real Element of REAL
cos . (exp_R . x) is V28() V29() ext-real Element of REAL
(cos . (exp_R . x)) ^2 is V28() V29() ext-real Element of REAL
((exp_R . x) * (sin . (exp_R . x))) / ((cos . (exp_R . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (exp_R . x)) ^2)) is V28() set
K97(((exp_R . x) * (sin . (exp_R . x))),K99(((cos . (exp_R . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cosec * exp_R)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cosec * exp_R)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cosec * exp_R)) . (upper_bound A)) - ((- (cosec * exp_R)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cosec * exp_R)) . (lower_bound A))) is V28() set
K96(((- (cosec * exp_R)) . (upper_bound A)),K98(((- (cosec * exp_R)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (cosec * exp_R)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (cosec * exp_R)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cosec * exp_R)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
exp_R . x is V28() V29() ext-real Element of REAL
cos . (exp_R . x) is V28() V29() ext-real Element of REAL
(exp_R . x) * (cos . (exp_R . x)) is V28() V29() ext-real Element of REAL
sin . (exp_R . x) is V28() V29() ext-real Element of REAL
(sin . (exp_R . x)) ^2 is V28() V29() ext-real Element of REAL
((exp_R . x) * (cos . (exp_R . x))) / ((sin . (exp_R . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (exp_R . x)) ^2)) is V28() set
K97(((exp_R . x) * (cos . (exp_R . x))),K99(((sin . (exp_R . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(sec * ln) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(sec * ln) . (lower_bound A) is V28() V29() ext-real Element of REAL
((sec * ln) . (upper_bound A)) - ((sec * ln) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((sec * ln) . (lower_bound A))) is V28() set
K96(((sec * ln) . (upper_bound A)),K98(((sec * ln) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(sec * ln) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((sec * ln) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((sec * ln) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
ln . x is V28() V29() ext-real Element of REAL
sin . (ln . x) is V28() V29() ext-real Element of REAL
cos . (ln . x) is V28() V29() ext-real Element of REAL
(cos . (ln . x)) ^2 is V28() V29() ext-real Element of REAL
x * ((cos . (ln . x)) ^2) is V28() V29() ext-real Element of REAL
(sin . (ln . x)) / (x * ((cos . (ln . x)) ^2)) is V28() V29() ext-real Element of REAL
K99((x * ((cos . (ln . x)) ^2))) is V28() set
K97((sin . (ln . x)),K99((x * ((cos . (ln . x)) ^2)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cosec * ln)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cosec * ln)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cosec * ln)) . (upper_bound A)) - ((- (cosec * ln)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cosec * ln)) . (lower_bound A))) is V28() set
K96(((- (cosec * ln)) . (upper_bound A)),K98(((- (cosec * ln)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (cosec * ln)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (cosec * ln)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cosec * ln)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
ln . x is V28() V29() ext-real Element of REAL
cos . (ln . x) is V28() V29() ext-real Element of REAL
sin . (ln . x) is V28() V29() ext-real Element of REAL
(sin . (ln . x)) ^2 is V28() V29() ext-real Element of REAL
x * ((sin . (ln . x)) ^2) is V28() V29() ext-real Element of REAL
(cos . (ln . x)) / (x * ((sin . (ln . x)) ^2)) is V28() V29() ext-real Element of REAL
K99((x * ((sin . (ln . x)) ^2))) is V28() set
K97((cos . (ln . x)),K99((x * ((sin . (ln . x)) ^2)))) is set
cos ^2 is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos (#) cos is V1() V6() set
sin / (cos ^2) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(exp_R * sec) (#) (sin / (cos ^2)) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(exp_R * sec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(exp_R * sec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((exp_R * sec) . (upper_bound A)) - ((exp_R * sec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((exp_R * sec) . (lower_bound A))) is V28() set
K96(((exp_R * sec) . (upper_bound A)),K98(((exp_R * sec) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
dom (sin / (cos ^2)) is V51() V52() V53() Element of K19(REAL)
(dom (exp_R * sec)) /\ (dom (sin / (cos ^2))) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sec . x is V28() V29() ext-real Element of REAL
exp_R . (sec . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(exp_R . (sec . x)) * (sin . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(((exp_R . (sec . x)) * (sin . x)),K99(((cos . x) ^2))) is set
((exp_R * sec) (#) (sin / (cos ^2))) . x is V28() V29() ext-real Element of REAL
(exp_R * sec) . x is V28() V29() ext-real Element of REAL
(sin / (cos ^2)) . x is V28() V29() ext-real Element of REAL
((exp_R * sec) . x) * ((sin / (cos ^2)) . x) is V28() V29() ext-real Element of REAL
(exp_R . (sec . x)) * ((sin / (cos ^2)) . x) is V28() V29() ext-real Element of REAL
(cos ^2) . x is V28() V29() ext-real Element of REAL
(sin . x) / ((cos ^2) . x) is V28() V29() ext-real Element of REAL
K99(((cos ^2) . x)) is V28() set
K97((sin . x),K99(((cos ^2) . x))) is set
(exp_R . (sec . x)) * ((sin . x) / ((cos ^2) . x)) is V28() V29() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K97((sin . x),K99(((cos . x) ^2))) is set
(exp_R . (sec . x)) * ((sin . x) / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
(exp_R * sec) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((exp_R * sec) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((exp_R * sec) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sec . x is V28() V29() ext-real Element of REAL
exp_R . (sec . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(exp_R . (sec . x)) * (sin . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
((exp_R . (sec . x)) * (sin . x)) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(((exp_R . (sec . x)) * (sin . x)),K99(((cos . x) ^2))) is set
sin ^2 is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sin (#) sin is V1() V6() set
cos / (sin ^2) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(exp_R * cosec) (#) (cos / (sin ^2)) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (exp_R * cosec)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (exp_R * cosec)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (exp_R * cosec)) . (upper_bound A)) - ((- (exp_R * cosec)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (exp_R * cosec)) . (lower_bound A))) is V28() set
K96(((- (exp_R * cosec)) . (upper_bound A)),K98(((- (exp_R * cosec)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
dom (cos / (sin ^2)) is V51() V52() V53() Element of K19(REAL)
(dom (exp_R * cosec)) /\ (dom (cos / (sin ^2))) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cosec . x is V28() V29() ext-real Element of REAL
exp_R . (cosec . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(exp_R . (cosec . x)) * (cos . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(((exp_R . (cosec . x)) * (cos . x)),K99(((sin . x) ^2))) is set
((exp_R * cosec) (#) (cos / (sin ^2))) . x is V28() V29() ext-real Element of REAL
(exp_R * cosec) . x is V28() V29() ext-real Element of REAL
(cos / (sin ^2)) . x is V28() V29() ext-real Element of REAL
((exp_R * cosec) . x) * ((cos / (sin ^2)) . x) is V28() V29() ext-real Element of REAL
(exp_R . (cosec . x)) * ((cos / (sin ^2)) . x) is V28() V29() ext-real Element of REAL
(sin ^2) . x is V28() V29() ext-real Element of REAL
(cos . x) / ((sin ^2) . x) is V28() V29() ext-real Element of REAL
K99(((sin ^2) . x)) is V28() set
K97((cos . x),K99(((sin ^2) . x))) is set
(exp_R . (cosec . x)) * ((cos . x) / ((sin ^2) . x)) is V28() V29() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K97((cos . x),K99(((sin . x) ^2))) is set
(exp_R . (cosec . x)) * ((cos . x) / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
(- (exp_R * cosec)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (exp_R * cosec)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (exp_R * cosec)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cosec . x is V28() V29() ext-real Element of REAL
exp_R . (cosec . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(exp_R . (cosec . x)) * (cos . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
((exp_R . (cosec . x)) * (cos . x)) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(((exp_R . (cosec . x)) * (cos . x)),K99(((sin . x) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
tan | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (tan,A) is V28() V29() ext-real Element of REAL
upper_bound A is V28() V29() ext-real Element of REAL
(ln * sec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(ln * sec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((ln * sec) . (upper_bound A)) - ((ln * sec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((ln * sec) . (lower_bound A))) is V28() set
K96(((ln * sec) . (upper_bound A)),K98(((ln * sec) . (lower_bound A)))) is set
f is V51() V52() V53() open Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
dom sec is V51() V52() V53() Element of K19(REAL)
(ln * sec) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((ln * sec) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((ln * sec) `| f) . Z is V28() V29() ext-real Element of REAL
tan . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
tan Z is V28() V29() ext-real Element of REAL
sin Z is set
sin . Z is V28() V29() ext-real Element of REAL
cos Z is set
K101((sin Z),(cos Z)) is set
dom cot is V51() V52() V53() Element of K19(REAL)
- cot is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
(- cot) | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((- cot),A) is V28() V29() ext-real Element of REAL
upper_bound A is V28() V29() ext-real Element of REAL
(ln * cosec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(ln * cosec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((ln * cosec) . (upper_bound A)) - ((ln * cosec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((ln * cosec) . (lower_bound A))) is V28() set
K96(((ln * cosec) . (upper_bound A)),K98(((ln * cosec) . (lower_bound A)))) is set
f is V51() V52() V53() open Element of K19(REAL)
dom (- cot) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
dom cosec is V51() V52() V53() Element of K19(REAL)
(ln * cosec) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((ln * cosec) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((ln * cosec) `| f) . Z is V28() V29() ext-real Element of REAL
(- cot) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
cot Z is V28() V29() ext-real Element of REAL
cos Z is set
cos . Z is V28() V29() ext-real Element of REAL
sin Z is set
K101((cos Z),(sin Z)) is set
- (cot Z) is V28() V29() ext-real Element of REAL
cot . Z is V28() V29() ext-real Element of REAL
- (cot . Z) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
cot | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (cot,A) is V28() V29() ext-real Element of REAL
upper_bound A is V28() V29() ext-real Element of REAL
(- (ln * cosec)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (ln * cosec)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (ln * cosec)) . (upper_bound A)) - ((- (ln * cosec)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (ln * cosec)) . (lower_bound A))) is V28() set
K96(((- (ln * cosec)) . (upper_bound A)),K98(((- (ln * cosec)) . (lower_bound A)))) is set
f is V51() V52() V53() open Element of K19(REAL)
(- (ln * cosec)) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (ln * cosec)) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((- (ln * cosec)) `| f) . Z is V28() V29() ext-real Element of REAL
cot . Z is V28() V29() ext-real Element of REAL
A is V27() V29() V30() ext-real set
A + 1 is V28() V29() V30() ext-real Element of REAL
#Z A is V1() V4( REAL ) V5( REAL ) V6() V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
(#Z A) * sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((#Z A) * sec) is V51() V52() V53() Element of K19(REAL)
f is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
((#Z A) * sec) . (upper_bound f) is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
((#Z A) * sec) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((#Z A) * sec) . (upper_bound f)) - (((#Z A) * sec) . (lower_bound f)) is V28() V29() ext-real Element of REAL
K98((((#Z A) * sec) . (lower_bound f))) is V28() set
K96((((#Z A) * sec) . (upper_bound f)),K98((((#Z A) * sec) . (lower_bound f)))) is set
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
x is V51() V52() V53() open Element of K19(REAL)
((#Z A) * sec) `| x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((#Z A) * sec) `| x) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((#Z A) * sec) `| x) . Z is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
A * (sin . Z) is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
(cos . Z) #Z (A + 1) is V28() V29() ext-real Element of REAL
(A * (sin . Z)) / ((cos . Z) #Z (A + 1)) is V28() V29() ext-real Element of REAL
K99(((cos . Z) #Z (A + 1))) is V28() set
K97((A * (sin . Z)),K99(((cos . Z) #Z (A + 1)))) is set
A is V27() V29() V30() ext-real set
A + 1 is V28() V29() V30() ext-real Element of REAL
#Z A is V1() V4( REAL ) V5( REAL ) V6() V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
(#Z A) * cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((#Z A) * cosec) is V51() V52() V53() Element of K19(REAL)
- ((#Z A) * cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) ((#Z A) * cosec) is V1() V6() set
f is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
(- ((#Z A) * cosec)) . (upper_bound f) is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
(- ((#Z A) * cosec)) . (lower_bound f) is V28() V29() ext-real Element of REAL
((- ((#Z A) * cosec)) . (upper_bound f)) - ((- ((#Z A) * cosec)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
K98(((- ((#Z A) * cosec)) . (lower_bound f))) is V28() set
K96(((- ((#Z A) * cosec)) . (upper_bound f)),K98(((- ((#Z A) * cosec)) . (lower_bound f)))) is set
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
x is V51() V52() V53() open Element of K19(REAL)
(- ((#Z A) * cosec)) `| x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- ((#Z A) * cosec)) `| x) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((- ((#Z A) * cosec)) `| x) . Z is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
A * (cos . Z) is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
(sin . Z) #Z (A + 1) is V28() V29() ext-real Element of REAL
(A * (cos . Z)) / ((sin . Z) #Z (A + 1)) is V28() V29() ext-real Element of REAL
K99(((sin . Z) #Z (A + 1))) is V28() set
K97((A * (cos . Z)),K99(((sin . Z) #Z (A + 1)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(exp_R (#) sec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(exp_R (#) sec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((exp_R (#) sec) . (upper_bound A)) - ((exp_R (#) sec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((exp_R (#) sec) . (lower_bound A))) is V28() set
K96(((exp_R (#) sec) . (upper_bound A)),K98(((exp_R (#) sec) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(exp_R (#) sec) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((exp_R (#) sec) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((exp_R (#) sec) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
exp_R . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(exp_R . x) / (cos . x) is V28() V29() ext-real Element of REAL
K99((cos . x)) is V28() set
K97((exp_R . x),K99((cos . x))) is set
sin . x is V28() V29() ext-real Element of REAL
(exp_R . x) * (sin . x) is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
((exp_R . x) * (sin . x)) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(((exp_R . x) * (sin . x)),K99(((cos . x) ^2))) is set
((exp_R . x) / (cos . x)) + (((exp_R . x) * (sin . x)) / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(exp_R (#) cosec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(exp_R (#) cosec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((exp_R (#) cosec) . (upper_bound A)) - ((exp_R (#) cosec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((exp_R (#) cosec) . (lower_bound A))) is V28() set
K96(((exp_R (#) cosec) . (upper_bound A)),K98(((exp_R (#) cosec) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(exp_R (#) cosec) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((exp_R (#) cosec) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((exp_R (#) cosec) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
exp_R . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(exp_R . x) / (sin . x) is V28() V29() ext-real Element of REAL
K99((sin . x)) is V28() set
K97((exp_R . x),K99((sin . x))) is set
cos . x is V28() V29() ext-real Element of REAL
(exp_R . x) * (cos . x) is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
((exp_R . x) * (cos . x)) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(((exp_R . x) * (cos . x)),K99(((sin . x) ^2))) is set
((exp_R . x) / (sin . x)) - (((exp_R . x) * (cos . x)) / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
K98((((exp_R . x) * (cos . x)) / ((sin . x) ^2))) is V28() set
K96(((exp_R . x) / (sin . x)),K98((((exp_R . x) * (cos . x)) / ((sin . x) ^2)))) is set
A is V28() V29() ext-real Element of REAL
1 / A is V28() V29() ext-real Element of REAL
K99(A) is V28() set
K97(1,K99(A)) is set
f is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sec * x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(1 / A) (#) (sec * x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V4(Z) V5( REAL ) V5(Z) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((1 / A) (#) (sec * x)) - (id Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (id Z) is V1() V6() V34() set
K98(1) (#) (id Z) is V1() V6() set
((1 / A) (#) (sec * x)) + (- (id Z)) is V1() V6() set
dom (((1 / A) (#) (sec * x)) - (id Z)) is V51() V52() V53() Element of K19(REAL)
(((1 / A) (#) (sec * x)) - (id Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
(((1 / A) (#) (sec * x)) - (id Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
((((1 / A) (#) (sec * x)) - (id Z)) . (upper_bound f)) - ((((1 / A) (#) (sec * x)) - (id Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
K98(((((1 / A) (#) (sec * x)) - (id Z)) . (lower_bound f))) is V28() set
K96(((((1 / A) (#) (sec * x)) - (id Z)) . (upper_bound f)),K98(((((1 / A) (#) (sec * x)) - (id Z)) . (lower_bound f)))) is set
(((1 / A) (#) (sec * x)) - (id Z)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((((1 / A) (#) (sec * x)) - (id Z)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((((1 / A) (#) (sec * x)) - (id Z)) `| Z) . x is V28() V29() ext-real Element of REAL
Z . x is V28() V29() ext-real Element of REAL
A * x is V28() V29() ext-real Element of REAL
sin . (A * x) is V28() V29() ext-real Element of REAL
cos . (A * x) is V28() V29() ext-real Element of REAL
(cos . (A * x)) ^2 is V28() V29() ext-real Element of REAL
(sin . (A * x)) - ((cos . (A * x)) ^2) is V28() V29() ext-real Element of REAL
K98(((cos . (A * x)) ^2)) is V28() set
K96((sin . (A * x)),K98(((cos . (A * x)) ^2))) is set
((sin . (A * x)) - ((cos . (A * x)) ^2)) / ((cos . (A * x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (A * x)) ^2)) is V28() set
K97(((sin . (A * x)) - ((cos . (A * x)) ^2)),K99(((cos . (A * x)) ^2))) is set
A is V28() V29() ext-real Element of REAL
1 / A is V28() V29() ext-real Element of REAL
K99(A) is V28() set
K97(1,K99(A)) is set
- (1 / A) is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V4(f) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cosec * x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- (1 / A)) (#) (cosec * x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V4(Z) V5( REAL ) V5(Z) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- (1 / A)) (#) (cosec * x)) - (id Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (id Z) is V1() V6() V34() set
K98(1) (#) (id Z) is V1() V6() set
((- (1 / A)) (#) (cosec * x)) + (- (id Z)) is V1() V6() set
dom (((- (1 / A)) (#) (cosec * x)) - (id Z)) is V51() V52() V53() Element of K19(REAL)
(((- (1 / A)) (#) (cosec * x)) - (id Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
(((- (1 / A)) (#) (cosec * x)) - (id Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
((((- (1 / A)) (#) (cosec * x)) - (id Z)) . (upper_bound f)) - ((((- (1 / A)) (#) (cosec * x)) - (id Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
K98(((((- (1 / A)) (#) (cosec * x)) - (id Z)) . (lower_bound f))) is V28() set
K96(((((- (1 / A)) (#) (cosec * x)) - (id Z)) . (upper_bound f)),K98(((((- (1 / A)) (#) (cosec * x)) - (id Z)) . (lower_bound f)))) is set
(((- (1 / A)) (#) (cosec * x)) - (id Z)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((((- (1 / A)) (#) (cosec * x)) - (id Z)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((((- (1 / A)) (#) (cosec * x)) - (id Z)) `| Z) . x is V28() V29() ext-real Element of REAL
Z . x is V28() V29() ext-real Element of REAL
A * x is V28() V29() ext-real Element of REAL
cos . (A * x) is V28() V29() ext-real Element of REAL
sin . (A * x) is V28() V29() ext-real Element of REAL
(sin . (A * x)) ^2 is V28() V29() ext-real Element of REAL
(cos . (A * x)) - ((sin . (A * x)) ^2) is V28() V29() ext-real Element of REAL
K98(((sin . (A * x)) ^2)) is V28() set
K96((cos . (A * x)),K98(((sin . (A * x)) ^2))) is set
((cos . (A * x)) - ((sin . (A * x)) ^2)) / ((sin . (A * x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (A * x)) ^2)) is V28() set
K97(((cos . (A * x)) - ((sin . (A * x)) ^2)),K99(((sin . (A * x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(ln (#) sec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(ln (#) sec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((ln (#) sec) . (upper_bound A)) - ((ln (#) sec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((ln (#) sec) . (lower_bound A))) is V28() set
K96(((ln (#) sec) . (upper_bound A)),K98(((ln (#) sec) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(ln (#) sec) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((ln (#) sec) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((ln (#) sec) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
1 / (cos . x) is V28() V29() ext-real Element of REAL
K99((cos . x)) is V28() set
K97(1,K99((cos . x))) is set
(1 / (cos . x)) / x is V28() V29() ext-real Element of REAL
K99(x) is V28() set
K97((1 / (cos . x)),K99(x)) is set
ln . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(ln . x) * (sin . x) is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
((ln . x) * (sin . x)) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(((ln . x) * (sin . x)),K99(((cos . x) ^2))) is set
((1 / (cos . x)) / x) + (((ln . x) * (sin . x)) / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(ln (#) cosec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(ln (#) cosec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((ln (#) cosec) . (upper_bound A)) - ((ln (#) cosec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((ln (#) cosec) . (lower_bound A))) is V28() set
K96(((ln (#) cosec) . (upper_bound A)),K98(((ln (#) cosec) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(ln (#) cosec) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((ln (#) cosec) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((ln (#) cosec) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
1 / (sin . x) is V28() V29() ext-real Element of REAL
K99((sin . x)) is V28() set
K97(1,K99((sin . x))) is set
(1 / (sin . x)) / x is V28() V29() ext-real Element of REAL
K99(x) is V28() set
K97((1 / (sin . x)),K99(x)) is set
ln . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(ln . x) * (cos . x) is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
((ln . x) * (cos . x)) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(((ln . x) * (cos . x)),K99(((sin . x) ^2))) is set
((1 / (sin . x)) / x) - (((ln . x) * (cos . x)) / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
K98((((ln . x) * (cos . x)) / ((sin . x) ^2))) is V28() set
K96(((1 / (sin . x)) / x),K98((((ln . x) * (cos . x)) / ((sin . x) ^2)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V4(Z) V5( REAL ) V5(Z) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(id Z) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id Z) ^) (#) sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id Z) ^) (#) sec) is V51() V52() V53() Element of K19(REAL)
- (((id Z) ^) (#) sec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (((id Z) ^) (#) sec) is V1() V6() set
(- (((id Z) ^) (#) sec)) . (upper_bound A) is V28() V29() ext-real Element of REAL
(- (((id Z) ^) (#) sec)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (((id Z) ^) (#) sec)) . (upper_bound A)) - ((- (((id Z) ^) (#) sec)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (((id Z) ^) (#) sec)) . (lower_bound A))) is V28() set
K96(((- (((id Z) ^) (#) sec)) . (upper_bound A)),K98(((- (((id Z) ^) (#) sec)) . (lower_bound A)))) is set
(- (((id Z) ^) (#) sec)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (((id Z) ^) (#) sec)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (((id Z) ^) (#) sec)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
1 / (cos . x) is V28() V29() ext-real Element of REAL
K99((cos . x)) is V28() set
K97(1,K99((cos . x))) is set
x ^2 is V28() V29() ext-real Element of REAL
(1 / (cos . x)) / (x ^2) is V28() V29() ext-real Element of REAL
K99((x ^2)) is V28() set
K97((1 / (cos . x)),K99((x ^2))) is set
sin . x is V28() V29() ext-real Element of REAL
(sin . x) / x is V28() V29() ext-real Element of REAL
K99(x) is V28() set
K97((sin . x),K99(x)) is set
(cos . x) ^2 is V28() V29() ext-real Element of REAL
((sin . x) / x) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(((sin . x) / x),K99(((cos . x) ^2))) is set
((1 / (cos . x)) / (x ^2)) - (((sin . x) / x) / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
K98((((sin . x) / x) / ((cos . x) ^2))) is V28() set
K96(((1 / (cos . x)) / (x ^2)),K98((((sin . x) / x) / ((cos . x) ^2)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V4(Z) V5( REAL ) V5(Z) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(id Z) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id Z) ^) (#) cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id Z) ^) (#) cosec) is V51() V52() V53() Element of K19(REAL)
- (((id Z) ^) (#) cosec) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (((id Z) ^) (#) cosec) is V1() V6() set
(- (((id Z) ^) (#) cosec)) . (upper_bound A) is V28() V29() ext-real Element of REAL
(- (((id Z) ^) (#) cosec)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (((id Z) ^) (#) cosec)) . (upper_bound A)) - ((- (((id Z) ^) (#) cosec)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (((id Z) ^) (#) cosec)) . (lower_bound A))) is V28() set
K96(((- (((id Z) ^) (#) cosec)) . (upper_bound A)),K98(((- (((id Z) ^) (#) cosec)) . (lower_bound A)))) is set
(- (((id Z) ^) (#) cosec)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (((id Z) ^) (#) cosec)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (((id Z) ^) (#) cosec)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
1 / (sin . x) is V28() V29() ext-real Element of REAL
K99((sin . x)) is V28() set
K97(1,K99((sin . x))) is set
x ^2 is V28() V29() ext-real Element of REAL
(1 / (sin . x)) / (x ^2) is V28() V29() ext-real Element of REAL
K99((x ^2)) is V28() set
K97((1 / (sin . x)),K99((x ^2))) is set
cos . x is V28() V29() ext-real Element of REAL
(cos . x) / x is V28() V29() ext-real Element of REAL
K99(x) is V28() set
K97((cos . x),K99(x)) is set
(sin . x) ^2 is V28() V29() ext-real Element of REAL
((cos . x) / x) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(((cos . x) / x),K99(((sin . x) ^2))) is set
((1 / (sin . x)) / (x ^2)) + (((cos . x) / x) / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(sec * sin) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(sec * sin) . (lower_bound A) is V28() V29() ext-real Element of REAL
((sec * sin) . (upper_bound A)) - ((sec * sin) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((sec * sin) . (lower_bound A))) is V28() set
K96(((sec * sin) . (upper_bound A)),K98(((sec * sin) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(sec * sin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((sec * sin) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((sec * sin) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
sin . (sin . x) is V28() V29() ext-real Element of REAL
(cos . x) * (sin . (sin . x)) is V28() V29() ext-real Element of REAL
cos . (sin . x) is V28() V29() ext-real Element of REAL
(cos . (sin . x)) ^2 is V28() V29() ext-real Element of REAL
((cos . x) * (sin . (sin . x))) / ((cos . (sin . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (sin . x)) ^2)) is V28() set
K97(((cos . x) * (sin . (sin . x))),K99(((cos . (sin . x)) ^2))) is set
- (sec * cos) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (sec * cos) is V1() V6() set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (sec * cos)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (sec * cos)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (sec * cos)) . (upper_bound A)) - ((- (sec * cos)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (sec * cos)) . (lower_bound A))) is V28() set
K96(((- (sec * cos)) . (upper_bound A)),K98(((- (sec * cos)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
dom (- (sec * cos)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (sec * cos) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- (sec * cos)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V28() V29() ext-real Element of REAL
((- (sec * cos)) `| Z) . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
sin . (cos . x) is V28() V29() ext-real Element of REAL
(sin . x) * (sin . (cos . x)) is V28() V29() ext-real Element of REAL
cos . (cos . x) is V28() V29() ext-real Element of REAL
(cos . (cos . x)) ^2 is V28() V29() ext-real Element of REAL
((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (cos . x)) ^2)) is V28() set
K97(((sin . x) * (sin . (cos . x))),K99(((cos . (cos . x)) ^2))) is set
(sec * cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((sec * cos) `| Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((sec * cos) `| Z)) . x is V28() V29() ext-real Element of REAL
((sec * cos) `| Z) . x is V28() V29() ext-real Element of REAL
(- 1) * (((sec * cos) `| Z) . x) is V28() V29() ext-real Element of REAL
- (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * (- (((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2))) is V28() V29() ext-real Element of REAL
dom ((- (sec * cos)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (sec * cos)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
sin . (cos . x) is V28() V29() ext-real Element of REAL
(sin . x) * (sin . (cos . x)) is V28() V29() ext-real Element of REAL
cos . (cos . x) is V28() V29() ext-real Element of REAL
(cos . (cos . x)) ^2 is V28() V29() ext-real Element of REAL
((sin . x) * (sin . (cos . x))) / ((cos . (cos . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (cos . x)) ^2)) is V28() set
K97(((sin . x) * (sin . (cos . x))),K99(((cos . (cos . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cosec * sin)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cosec * sin)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cosec * sin)) . (upper_bound A)) - ((- (cosec * sin)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cosec * sin)) . (lower_bound A))) is V28() set
K96(((- (cosec * sin)) . (upper_bound A)),K98(((- (cosec * sin)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (cosec * sin)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (cosec * sin)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cosec * sin)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
cos . (sin . x) is V28() V29() ext-real Element of REAL
(cos . x) * (cos . (sin . x)) is V28() V29() ext-real Element of REAL
sin . (sin . x) is V28() V29() ext-real Element of REAL
(sin . (sin . x)) ^2 is V28() V29() ext-real Element of REAL
((cos . x) * (cos . (sin . x))) / ((sin . (sin . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (sin . x)) ^2)) is V28() set
K97(((cos . x) * (cos . (sin . x))),K99(((sin . (sin . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(cosec * cos) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(cosec * cos) . (lower_bound A) is V28() V29() ext-real Element of REAL
((cosec * cos) . (upper_bound A)) - ((cosec * cos) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((cosec * cos) . (lower_bound A))) is V28() set
K96(((cosec * cos) . (upper_bound A)),K98(((cosec * cos) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(cosec * cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((cosec * cos) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((cosec * cos) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
cos . (cos . x) is V28() V29() ext-real Element of REAL
(sin . x) * (cos . (cos . x)) is V28() V29() ext-real Element of REAL
sin . (cos . x) is V28() V29() ext-real Element of REAL
(sin . (cos . x)) ^2 is V28() V29() ext-real Element of REAL
((sin . x) * (cos . (cos . x))) / ((sin . (cos . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (cos . x)) ^2)) is V28() set
K97(((sin . x) * (cos . (cos . x))),K99(((sin . (cos . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(sec * tan) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(sec * tan) . (lower_bound A) is V28() V29() ext-real Element of REAL
((sec * tan) . (upper_bound A)) - ((sec * tan) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((sec * tan) . (lower_bound A))) is V28() set
K96(((sec * tan) . (upper_bound A)),K98(((sec * tan) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(sec * tan) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((sec * tan) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((sec * tan) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
tan . x is V28() V29() ext-real Element of REAL
sin . (tan . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
(sin . (tan . x)) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97((sin . (tan . x)),K99(((cos . x) ^2))) is set
cos . (tan . x) is V28() V29() ext-real Element of REAL
(cos . (tan . x)) ^2 is V28() V29() ext-real Element of REAL
((sin . (tan . x)) / ((cos . x) ^2)) / ((cos . (tan . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (tan . x)) ^2)) is V28() set
K97(((sin . (tan . x)) / ((cos . x) ^2)),K99(((cos . (tan . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (sec * cot)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (sec * cot)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (sec * cot)) . (upper_bound A)) - ((- (sec * cot)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (sec * cot)) . (lower_bound A))) is V28() set
K96(((- (sec * cot)) . (upper_bound A)),K98(((- (sec * cot)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (sec * cot)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (sec * cot)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (sec * cot)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cot . x is V28() V29() ext-real Element of REAL
sin . (cot . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
(sin . (cot . x)) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97((sin . (cot . x)),K99(((sin . x) ^2))) is set
cos . (cot . x) is V28() V29() ext-real Element of REAL
(cos . (cot . x)) ^2 is V28() V29() ext-real Element of REAL
((sin . (cot . x)) / ((sin . x) ^2)) / ((cos . (cot . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (cot . x)) ^2)) is V28() set
K97(((sin . (cot . x)) / ((sin . x) ^2)),K99(((cos . (cot . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cosec * tan)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cosec * tan)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cosec * tan)) . (upper_bound A)) - ((- (cosec * tan)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cosec * tan)) . (lower_bound A))) is V28() set
K96(((- (cosec * tan)) . (upper_bound A)),K98(((- (cosec * tan)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (cosec * tan)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (cosec * tan)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cosec * tan)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
tan . x is V28() V29() ext-real Element of REAL
cos . (tan . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
(cos . (tan . x)) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97((cos . (tan . x)),K99(((cos . x) ^2))) is set
sin . (tan . x) is V28() V29() ext-real Element of REAL
(sin . (tan . x)) ^2 is V28() V29() ext-real Element of REAL
((cos . (tan . x)) / ((cos . x) ^2)) / ((sin . (tan . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (tan . x)) ^2)) is V28() set
K97(((cos . (tan . x)) / ((cos . x) ^2)),K99(((sin . (tan . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(cosec * cot) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(cosec * cot) . (lower_bound A) is V28() V29() ext-real Element of REAL
((cosec * cot) . (upper_bound A)) - ((cosec * cot) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((cosec * cot) . (lower_bound A))) is V28() set
K96(((cosec * cot) . (upper_bound A)),K98(((cosec * cot) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(cosec * cot) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((cosec * cot) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((cosec * cot) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cot . x is V28() V29() ext-real Element of REAL
cos . (cot . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
(cos . (cot . x)) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97((cos . (cot . x)),K99(((sin . x) ^2))) is set
sin . (cot . x) is V28() V29() ext-real Element of REAL
(sin . (cot . x)) ^2 is V28() V29() ext-real Element of REAL
((cos . (cot . x)) / ((sin . x) ^2)) / ((sin . (cot . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (cot . x)) ^2)) is V28() set
K97(((cos . (cot . x)) / ((sin . x) ^2)),K99(((sin . (cot . x)) ^2))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(tan (#) sec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(tan (#) sec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((tan (#) sec) . (upper_bound A)) - ((tan (#) sec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((tan (#) sec) . (lower_bound A))) is V28() set
K96(((tan (#) sec) . (upper_bound A)),K98(((tan (#) sec) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(tan (#) sec) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((tan (#) sec) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((tan (#) sec) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(1,K99(((cos . x) ^2))) is set
(1 / ((cos . x) ^2)) / (cos . x) is V28() V29() ext-real Element of REAL
K99((cos . x)) is V28() set
K97((1 / ((cos . x) ^2)),K99((cos . x))) is set
tan . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(tan . x) * (sin . x) is V28() V29() ext-real Element of REAL
((tan . x) * (sin . x)) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K97(((tan . x) * (sin . x)),K99(((cos . x) ^2))) is set
((1 / ((cos . x) ^2)) / (cos . x)) + (((tan . x) * (sin . x)) / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cot (#) sec)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cot (#) sec)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cot (#) sec)) . (upper_bound A)) - ((- (cot (#) sec)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cot (#) sec)) . (lower_bound A))) is V28() set
K96(((- (cot (#) sec)) . (upper_bound A)),K98(((- (cot (#) sec)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (cot (#) sec)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (cot (#) sec)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cot (#) sec)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(1,K99(((sin . x) ^2))) is set
cos . x is V28() V29() ext-real Element of REAL
(1 / ((sin . x) ^2)) / (cos . x) is V28() V29() ext-real Element of REAL
K99((cos . x)) is V28() set
K97((1 / ((sin . x) ^2)),K99((cos . x))) is set
cot . x is V28() V29() ext-real Element of REAL
(cot . x) * (sin . x) is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
((cot . x) * (sin . x)) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(((cot . x) * (sin . x)),K99(((cos . x) ^2))) is set
((1 / ((sin . x) ^2)) / (cos . x)) - (((cot . x) * (sin . x)) / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
K98((((cot . x) * (sin . x)) / ((cos . x) ^2))) is V28() set
K96(((1 / ((sin . x) ^2)) / (cos . x)),K98((((cot . x) * (sin . x)) / ((cos . x) ^2)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(tan (#) cosec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(tan (#) cosec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((tan (#) cosec) . (upper_bound A)) - ((tan (#) cosec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((tan (#) cosec) . (lower_bound A))) is V28() set
K96(((tan (#) cosec) . (upper_bound A)),K98(((tan (#) cosec) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(tan (#) cosec) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((tan (#) cosec) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((tan (#) cosec) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(1,K99(((cos . x) ^2))) is set
sin . x is V28() V29() ext-real Element of REAL
(1 / ((cos . x) ^2)) / (sin . x) is V28() V29() ext-real Element of REAL
K99((sin . x)) is V28() set
K97((1 / ((cos . x) ^2)),K99((sin . x))) is set
tan . x is V28() V29() ext-real Element of REAL
(tan . x) * (cos . x) is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
((tan . x) * (cos . x)) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(((tan . x) * (cos . x)),K99(((sin . x) ^2))) is set
((1 / ((cos . x) ^2)) / (sin . x)) - (((tan . x) * (cos . x)) / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
K98((((tan . x) * (cos . x)) / ((sin . x) ^2))) is V28() set
K96(((1 / ((cos . x) ^2)) / (sin . x)),K98((((tan . x) * (cos . x)) / ((sin . x) ^2)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cot (#) cosec)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cot (#) cosec)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cot (#) cosec)) . (upper_bound A)) - ((- (cot (#) cosec)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cot (#) cosec)) . (lower_bound A))) is V28() set
K96(((- (cot (#) cosec)) . (upper_bound A)),K98(((- (cot (#) cosec)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (cot (#) cosec)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (cot (#) cosec)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cot (#) cosec)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(1,K99(((sin . x) ^2))) is set
(1 / ((sin . x) ^2)) / (sin . x) is V28() V29() ext-real Element of REAL
K99((sin . x)) is V28() set
K97((1 / ((sin . x) ^2)),K99((sin . x))) is set
cot . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cot . x) * (cos . x) is V28() V29() ext-real Element of REAL
((cot . x) * (cos . x)) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K97(((cot . x) * (cos . x)),K99(((sin . x) ^2))) is set
((1 / ((sin . x) ^2)) / (sin . x)) + (((cot . x) * (cos . x)) / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
- (tan * cot) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (tan * cot) is V1() V6() set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (tan * cot)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (tan * cot)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (tan * cot)) . (upper_bound A)) - ((- (tan * cot)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (tan * cot)) . (lower_bound A))) is V28() set
K96(((- (tan * cot)) . (upper_bound A)),K98(((- (tan * cot)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
dom (- (tan * cot)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (tan * cot) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- (tan * cot)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V28() V29() ext-real Element of REAL
((- (tan * cot)) `| Z) . x is V28() V29() ext-real Element of REAL
cot . x is V28() V29() ext-real Element of REAL
cos . (cot . x) is V28() V29() ext-real Element of REAL
(cos . (cot . x)) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . (cot . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (cot . x)) ^2)) is V28() set
K97(1,K99(((cos . (cot . x)) ^2))) is set
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(1,K99(((sin . x) ^2))) is set
(1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
(tan * cot) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((tan * cot) `| Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((tan * cot) `| Z)) . x is V28() V29() ext-real Element of REAL
((tan * cot) `| Z) . x is V28() V29() ext-real Element of REAL
(- 1) * (((tan * cot) `| Z) . x) is V28() V29() ext-real Element of REAL
- (1 / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
(1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) is V28() V29() ext-real Element of REAL
(- 1) * ((1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2)))) is V28() V29() ext-real Element of REAL
dom ((- (tan * cot)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (tan * cot)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cot . x is V28() V29() ext-real Element of REAL
cos . (cot . x) is V28() V29() ext-real Element of REAL
(cos . (cot . x)) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . (cot . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (cot . x)) ^2)) is V28() set
K97(1,K99(((cos . (cot . x)) ^2))) is set
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(1,K99(((sin . x) ^2))) is set
(1 / ((cos . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(tan * tan) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(tan * tan) . (lower_bound A) is V28() V29() ext-real Element of REAL
((tan * tan) . (upper_bound A)) - ((tan * tan) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((tan * tan) . (lower_bound A))) is V28() set
K96(((tan * tan) . (upper_bound A)),K98(((tan * tan) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(tan * tan) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((tan * tan) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((tan * tan) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
tan . x is V28() V29() ext-real Element of REAL
cos . (tan . x) is V28() V29() ext-real Element of REAL
(cos . (tan . x)) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . (tan . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . (tan . x)) ^2)) is V28() set
K97(1,K99(((cos . (tan . x)) ^2))) is set
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(1,K99(((cos . x) ^2))) is set
(1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(cot * cot) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(cot * cot) . (lower_bound A) is V28() V29() ext-real Element of REAL
((cot * cot) . (upper_bound A)) - ((cot * cot) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((cot * cot) . (lower_bound A))) is V28() set
K96(((cot * cot) . (upper_bound A)),K98(((cot * cot) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(cot * cot) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((cot * cot) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((cot * cot) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cot . x is V28() V29() ext-real Element of REAL
sin . (cot . x) is V28() V29() ext-real Element of REAL
(sin . (cot . x)) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . (cot . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (cot . x)) ^2)) is V28() set
K97(1,K99(((sin . (cot . x)) ^2))) is set
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(1,K99(((sin . x) ^2))) is set
(1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
- (cot * tan) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cot * tan) is V1() V6() set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cot * tan)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cot * tan)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cot * tan)) . (upper_bound A)) - ((- (cot * tan)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cot * tan)) . (lower_bound A))) is V28() set
K96(((- (cot * tan)) . (upper_bound A)),K98(((- (cot * tan)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
dom (- (cot * tan)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cot * tan) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- (cot * tan)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V28() V29() ext-real Element of REAL
((- (cot * tan)) `| Z) . x is V28() V29() ext-real Element of REAL
tan . x is V28() V29() ext-real Element of REAL
sin . (tan . x) is V28() V29() ext-real Element of REAL
(sin . (tan . x)) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . (tan . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (tan . x)) ^2)) is V28() set
K97(1,K99(((sin . (tan . x)) ^2))) is set
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(1,K99(((cos . x) ^2))) is set
(1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
(cot * tan) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((cot * tan) `| Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((cot * tan) `| Z)) . x is V28() V29() ext-real Element of REAL
((cot * tan) `| Z) . x is V28() V29() ext-real Element of REAL
(- 1) * (((cot * tan) `| Z) . x) is V28() V29() ext-real Element of REAL
- (1 / ((sin . (tan . x)) ^2)) is V28() V29() ext-real Element of REAL
(- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * ((- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2))) is V28() V29() ext-real Element of REAL
dom ((- (cot * tan)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cot * tan)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
tan . x is V28() V29() ext-real Element of REAL
sin . (tan . x) is V28() V29() ext-real Element of REAL
(sin . (tan . x)) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . (tan . x)) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . (tan . x)) ^2)) is V28() set
K97(1,K99(((sin . (tan . x)) ^2))) is set
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(1,K99(((cos . x) ^2))) is set
(1 / ((sin . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(tan - cot) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(tan - cot) . (lower_bound A) is V28() V29() ext-real Element of REAL
((tan - cot) . (upper_bound A)) - ((tan - cot) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((tan - cot) . (lower_bound A))) is V28() set
K96(((tan - cot) . (upper_bound A)),K98(((tan - cot) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(tan - cot) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((tan - cot) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((tan - cot) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(1,K99(((cos . x) ^2))) is set
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(1,K99(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(tan + cot) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(tan + cot) . (lower_bound A) is V28() V29() ext-real Element of REAL
((tan + cot) . (upper_bound A)) - ((tan + cot) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((tan + cot) . (lower_bound A))) is V28() set
K96(((tan + cot) . (upper_bound A)),K98(((tan + cot) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(tan + cot) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((tan + cot) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((tan + cot) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97(1,K99(((cos . x) ^2))) is set
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
1 / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97(1,K99(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
K98((1 / ((sin . x) ^2))) is V28() set
K96((1 / ((cos . x) ^2)),K98((1 / ((sin . x) ^2)))) is set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(sin * sin) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(sin * sin) . (lower_bound A) is V28() V29() ext-real Element of REAL
((sin * sin) . (upper_bound A)) - ((sin * sin) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((sin * sin) . (lower_bound A))) is V28() set
K96(((sin * sin) . (upper_bound A)),K98(((sin * sin) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(sin * sin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((sin * sin) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((sin * sin) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
cos . (sin . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . (sin . x)) * (cos . x) is V28() V29() ext-real Element of REAL
- (sin * cos) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (sin * cos) is V1() V6() set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (sin * cos)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (sin * cos)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (sin * cos)) . (upper_bound A)) - ((- (sin * cos)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (sin * cos)) . (lower_bound A))) is V28() set
K96(((- (sin * cos)) . (upper_bound A)),K98(((- (sin * cos)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
rng cos is V51() V52() V53() Element of K19(REAL)
dom (sin * cos) is V51() V52() V53() Element of K19(REAL)
dom (- (sin * cos)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (sin * cos) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- (sin * cos)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V28() V29() ext-real Element of REAL
((- (sin * cos)) `| Z) . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
cos . (cos . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(cos . (cos . x)) * (sin . x) is V28() V29() ext-real Element of REAL
(sin * cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((sin * cos) `| Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((sin * cos) `| Z)) . x is V28() V29() ext-real Element of REAL
((sin * cos) `| Z) . x is V28() V29() ext-real Element of REAL
(- 1) * (((sin * cos) `| Z) . x) is V28() V29() ext-real Element of REAL
- ((cos . (cos . x)) * (sin . x)) is V28() V29() ext-real Element of REAL
(- 1) * (- ((cos . (cos . x)) * (sin . x))) is V28() V29() ext-real Element of REAL
dom ((- (sin * cos)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (sin * cos)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
cos . (cos . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(cos . (cos . x)) * (sin . x) is V28() V29() ext-real Element of REAL
- (cos * sin) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (cos * sin) is V1() V6() set
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cos * sin)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cos * sin)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cos * sin)) . (upper_bound A)) - ((- (cos * sin)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cos * sin)) . (lower_bound A))) is V28() set
K96(((- (cos * sin)) . (upper_bound A)),K98(((- (cos * sin)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
rng sin is V51() V52() V53() Element of K19(REAL)
dom (cos * sin) is V51() V52() V53() Element of K19(REAL)
dom (- (cos * sin)) is V51() V52() V53() Element of K19(REAL)
- 1 is V28() V29() V30() ext-real Element of REAL
(- 1) (#) (cos * sin) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- (cos * sin)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V28() V29() ext-real Element of REAL
((- (cos * sin)) `| Z) . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
sin . (sin . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(sin . (sin . x)) * (cos . x) is V28() V29() ext-real Element of REAL
(cos * sin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) ((cos * sin) `| Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- 1) (#) ((cos * sin) `| Z)) . x is V28() V29() ext-real Element of REAL
((cos * sin) `| Z) . x is V28() V29() ext-real Element of REAL
(- 1) * (((cos * sin) `| Z) . x) is V28() V29() ext-real Element of REAL
- ((sin . (sin . x)) * (cos . x)) is V28() V29() ext-real Element of REAL
(- 1) * (- ((sin . (sin . x)) * (cos . x))) is V28() V29() ext-real Element of REAL
dom ((- (cos * sin)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cos * sin)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
sin . (sin . x) is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(sin . (sin . x)) * (cos . x) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(cos * cos) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(cos * cos) . (lower_bound A) is V28() V29() ext-real Element of REAL
((cos * cos) . (upper_bound A)) - ((cos * cos) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((cos * cos) . (lower_bound A))) is V28() set
K96(((cos * cos) . (upper_bound A)),K98(((cos * cos) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(cos * cos) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((cos * cos) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((cos * cos) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
sin . (cos . x) is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . (cos . x)) * (sin . x) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- (cos (#) cot)) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- (cos (#) cot)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- (cos (#) cot)) . (upper_bound A)) - ((- (cos (#) cot)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((- (cos (#) cot)) . (lower_bound A))) is V28() set
K96(((- (cos (#) cot)) . (upper_bound A)),K98(((- (cos (#) cot)) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (cos (#) cot)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (cos (#) cot)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (cos (#) cot)) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL
K99(((sin . x) ^2)) is V28() set
K97((cos . x),K99(((sin . x) ^2))) is set
(cos . x) + ((cos . x) / ((sin . x) ^2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V76() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(sin (#) tan) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(sin (#) tan) . (lower_bound A) is V28() V29() ext-real Element of REAL
((sin (#) tan) . (upper_bound A)) - ((sin (#) tan) . (lower_bound A)) is V28() V29() ext-real Element of REAL
K98(((sin (#) tan) . (lower_bound A))) is V28() set
K96(((sin (#) tan) . (upper_bound A)),K98(((sin (#) tan) . (lower_bound A)))) is set
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V4(A) V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(sin (#) tan) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((sin (#) tan) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((sin (#) tan) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
K99(((cos . x) ^2)) is V28() set
K97((sin . x),K99(((cos . x) ^2))) is set
(sin . x) + ((sin . x) / ((cos . x) ^2)) is V28() V29() ext-real Element of REAL