:: FDIFF_10 semantic presentation

REAL is V1() V62() V63() V64() V68() V70() set
NAT is V62() V63() V64() V65() V66() V67() V68() Element of K6(REAL)
K6(REAL) is set
K7(REAL,REAL) is V52() V53() V54() set
K6(K7(REAL,REAL)) is set
K69(REAL,REAL) is set
K7(NAT,K69(REAL,REAL)) is set
K6(K7(NAT,K69(REAL,REAL))) is set
K7(NAT,REAL) is V52() V53() V54() set
K6(K7(NAT,REAL)) is set
COMPLEX is V1() V62() V68() V70() set
K7(NAT,COMPLEX) is V52() set
K6(K7(NAT,COMPLEX)) is set
K7(COMPLEX,COMPLEX) is V52() set
K6(K7(COMPLEX,COMPLEX)) is set
0 is set
1 is V6() V10() V11() V12() ext-real non negative V47() V62() V63() V64() V65() V66() V67() V81() Element of NAT
{0,1} is set
NAT is V62() V63() V64() V65() V66() V67() V68() set
K6(NAT) is set
K6(NAT) is set
RAT is V1() V62() V63() V64() V65() V68() V70() set
INT is V1() V62() V63() V64() V65() V66() V68() V70() set
0 is V6() V10() V11() V12() ext-real non negative V47() V62() V63() V64() V65() V66() V67() V81() Element of NAT
exp_R is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
[#] REAL is V62() V63() V64() Element of K6(REAL)
dom exp_R is V62() V63() V64() Element of K6(REAL)
rng exp_R is V62() V63() V64() Element of K6(REAL)
right_open_halfline 0 is V62() V63() V64() Element of K6(REAL)
+infty is V1() ext-real positive non negative set
K148(0,+infty) is set
ln is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
K132(REAL,REAL,exp_R) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ln is V62() V63() V64() Element of K6(REAL)
rng ln is V62() V63() V64() Element of K6(REAL)
sin is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
cos is V13() V16( REAL ) V17( REAL ) V18() V27( REAL , REAL ) V52() V53() V54() Element of K6(K7(REAL,REAL))
sin + cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin + cos) is V62() V63() V64() Element of K6(REAL)
sin - cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin - cos) is V62() V63() V64() Element of K6(REAL)
sin / cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
cos / sin is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
{0} is V62() V63() V64() V65() V66() V67() set
dom sin is V62() V63() V64() Element of K6(REAL)
dom cos is V62() V63() V64() Element of K6(REAL)
tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom tan is V62() V63() V64() Element of K6(REAL)
cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom cot is V62() V63() V64() Element of K6(REAL)
sec is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
K232(REAL,REAL,cos) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
cosec is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
K232(REAL,REAL,sin) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
tan * cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (tan * cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(tan * cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
dom (cos / sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
(cos . (cot . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (cot . x)),(cos . (cot . x))) is set
1 / ((cos . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (cot . x)) ^2)) is V11() set
K37(1,K39(((cos . (cot . x)) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
diff ((tan * cot),x) is V11() V12() ext-real Element of REAL
diff (tan,(cot . x)) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(diff (tan,(cot . x))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
(1 / ((cos . (cot . x)) ^2)) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
(cos . (cot . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (cot . x)),(cos . (cot . x))) is set
1 / ((cos . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (cot . x)) ^2)) is V11() set
K37(1,K39(((cos . (cot . x)) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(1 / ((cos . (cot . x)) ^2)) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
tan * tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (tan * tan) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(tan * tan) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
dom (sin / cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
(cos . (tan . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (tan . x)),(cos . (tan . x))) is set
1 / ((cos . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (tan . x)) ^2)) is V11() set
K37(1,K39(((cos . (tan . x)) ^2))) is set
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
diff ((tan * tan),x) is V11() V12() ext-real Element of REAL
diff (tan,(tan . x)) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(diff (tan,(tan . x))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
(1 / ((cos . (tan . x)) ^2)) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
(cos . (tan . x)) ^2 is V11() V12() ext-real Element of REAL
K37((cos . (tan . x)),(cos . (tan . x))) is set
1 / ((cos . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . (tan . x)) ^2)) is V11() set
K37(1,K39(((cos . (tan . x)) ^2))) is set
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(1 / ((cos . (tan . x)) ^2)) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
cot * cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cot * cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cot * cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
dom (cos / sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cot * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
(sin . (cot . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (cot . x)),(sin . (cot . x))) is set
1 / ((sin . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (cot . x)) ^2)) is V11() set
K37(1,K39(((sin . (cot . x)) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
diff ((cot * cot),x) is V11() V12() ext-real Element of REAL
diff (cot,(cot . x)) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(diff (cot,(cot . x))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
- (1 / ((sin . (cot . x)) ^2)) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . (cot . x)) ^2))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . (cot . x)) ^2))) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cot * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
(sin . (cot . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (cot . x)),(sin . (cot . x))) is set
1 / ((sin . (cot . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (cot . x)) ^2)) is V11() set
K37(1,K39(((sin . (cot . x)) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((sin . (cot . x)) ^2)) * (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
cot * tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cot * tan) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cot * tan) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
dom (sin / cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cot * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
(sin . (tan . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (tan . x)),(sin . (tan . x))) is set
1 / ((sin . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (tan . x)) ^2)) is V11() set
K37(1,K39(((sin . (tan . x)) ^2))) is set
- (1 / ((sin . (tan . x)) ^2)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
diff ((cot * tan),x) is V11() V12() ext-real Element of REAL
diff (cot,(tan . x)) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(diff (cot,(tan . x))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
(- (1 / ((sin . (tan . x)) ^2))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cot * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
(sin . (tan . x)) ^2 is V11() V12() ext-real Element of REAL
K37((sin . (tan . x)),(sin . (tan . x))) is set
1 / ((sin . (tan . x)) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . (tan . x)) ^2)) is V11() set
K37(1,K39(((sin . (tan . x)) ^2))) is set
- (1 / ((sin . (tan . x)) ^2)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(- (1 / ((sin . (tan . x)) ^2))) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
tan - cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (tan - cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(tan - cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom tan) /\ (dom cot) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(diff (tan,x)) - (diff (cot,x)) is V11() V12() ext-real Element of REAL
K38((diff (cot,x))) is V11() set
K36((diff (tan,x)),K38((diff (cot,x)))) is set
(1 / ((cos . x) ^2)) - (diff (cot,x)) is V11() V12() ext-real Element of REAL
K36((1 / ((cos . x) ^2)),K38((diff (cot,x)))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(1 / ((cos . x) ^2)) - (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
K38((- (1 / ((sin . x) ^2)))) is V11() set
K36((1 / ((cos . x) ^2)),K38((- (1 / ((sin . x) ^2))))) is set
x is V11() V12() ext-real Element of REAL
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
tan + cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (tan + cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(tan + cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom tan) /\ (dom cot) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
diff (tan,x) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(diff (tan,x)) + (diff (cot,x)) is V11() V12() ext-real Element of REAL
(1 / ((cos . x) ^2)) + (diff (cot,x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
sin * sin is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
Z is open V62() V63() V64() Element of K6(REAL)
(sin * sin) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
rng sin is V62() V63() V64() Element of K6(REAL)
dom (sin * sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((sin * sin) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
diff ((sin * sin),x) is V11() V12() ext-real Element of REAL
diff (sin,(sin . x)) is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
(diff (sin,(sin . x))) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(cos . (sin . x)) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * sin) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
sin * cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
Z is open V62() V63() V64() Element of K6(REAL)
(sin * cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
rng cos is V62() V63() V64() Element of K6(REAL)
dom (sin * cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((sin * cos) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
cos . (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . (cos . x)) * (sin . x) is V11() V12() ext-real Element of REAL
- ((cos . (cos . x)) * (sin . x)) is V11() V12() ext-real Element of REAL
diff ((sin * cos),x) is V11() V12() ext-real Element of REAL
diff (sin,(cos . x)) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
(diff (sin,(cos . x))) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
(cos . (cos . x)) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(cos . (cos . x)) * (- (sin . x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * cos) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
cos . (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . (cos . x)) * (sin . x) is V11() V12() ext-real Element of REAL
- ((cos . (cos . x)) * (sin . x)) is V11() V12() ext-real Element of REAL
cos * sin is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
Z is open V62() V63() V64() Element of K6(REAL)
(cos * sin) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
rng sin is V62() V63() V64() Element of K6(REAL)
dom (cos * sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((cos * sin) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
sin . (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(sin . (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
- ((sin . (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
diff ((cos * sin),x) is V11() V12() ext-real Element of REAL
diff (cos,(sin . x)) is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
(diff (cos,(sin . x))) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
- (sin . (sin . x)) is V11() V12() ext-real Element of REAL
(- (sin . (sin . x))) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(- (sin . (sin . x))) * (cos . x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * sin) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
sin . (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(sin . (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
- ((sin . (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
cos * cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
Z is open V62() V63() V64() Element of K6(REAL)
(cos * cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
rng cos is V62() V63() V64() Element of K6(REAL)
dom (cos * cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((cos * cos) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . (cos . x)) * (sin . x) is V11() V12() ext-real Element of REAL
diff ((cos * cos),x) is V11() V12() ext-real Element of REAL
diff (cos,(cos . x)) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
(diff (cos,(cos . x))) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
- (sin . (cos . x)) is V11() V12() ext-real Element of REAL
(- (sin . (cos . x))) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(- (sin . (cos . x))) * (- (sin . x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * cos) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sin . (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . (cos . x)) * (sin . x) is V11() V12() ext-real Element of REAL
cos (#) cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos (#) cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos (#) cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom cos) /\ (dom cot) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos (#) cot) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
- (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37((cos . x),K39(((sin . x) ^2))) is set
(- (cos . x)) - ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38(((cos . x) / ((sin . x) ^2))) is V11() set
K36((- (cos . x)),K38(((cos . x) / ((sin . x) ^2)))) is set
diff (cos,x) is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(diff (cos,x)) * (cot . x) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(cos . x) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
((diff (cos,x)) * (cot . x)) + ((cos . x) * (diff (cot,x))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(cot . x) * (- (sin . x)) is V11() V12() ext-real Element of REAL
((cot . x) * (- (sin . x))) + ((cos . x) * (diff (cot,x))) is V11() V12() ext-real Element of REAL
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((sin . x) ^2))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(cos . x) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((cot . x) * (- (sin . x))) + ((cos . x) * (- (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(cos . x) / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() set
K37((cos . x),K39((sin . x))) is set
(sin . x) / 1 is V11() V12() ext-real Element of REAL
K39(1) is V11() set
K37((sin . x),K39(1)) is set
- ((sin . x) / 1) is V11() V12() ext-real Element of REAL
((cos . x) / (sin . x)) * (- ((sin . x) / 1)) is V11() V12() ext-real Element of REAL
(((cos . x) / (sin . x)) * (- ((sin . x) / 1))) - ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K36((((cos . x) / (sin . x)) * (- ((sin . x) / 1))),K38(((cos . x) / ((sin . x) ^2)))) is set
(sin . x) / (sin . x) is V11() V12() ext-real Element of REAL
K37((sin . x),K39((sin . x))) is set
(cos . x) * ((sin . x) / (sin . x)) is V11() V12() ext-real Element of REAL
- ((cos . x) * ((sin . x) / (sin . x))) is V11() V12() ext-real Element of REAL
(- ((cos . x) * ((sin . x) / (sin . x)))) - ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K36((- ((cos . x) * ((sin . x) / (sin . x)))),K38(((cos . x) / ((sin . x) ^2)))) is set
(cos . x) * 1 is V11() V12() ext-real Element of REAL
- ((cos . x) * 1) is V11() V12() ext-real Element of REAL
(- ((cos . x) * 1)) - ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K36((- ((cos . x) * 1)),K38(((cos . x) / ((sin . x) ^2)))) is set
x is V11() V12() ext-real Element of REAL
((cos (#) cot) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
- (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37((cos . x),K39(((sin . x) ^2))) is set
(- (cos . x)) - ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38(((cos . x) / ((sin . x) ^2))) is V11() set
K36((- (cos . x)),K38(((cos . x) / ((sin . x) ^2)))) is set
sin (#) tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin (#) tan) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin (#) tan) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom sin) /\ (dom tan) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
x is V11() V12() ext-real Element of REAL
((sin (#) tan) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37((sin . x),K39(((cos . x) ^2))) is set
(sin . x) + ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
(diff (sin,x)) * (tan . x) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(sin . x) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
((diff (sin,x)) * (tan . x)) + ((sin . x) * (diff (tan,x))) is V11() V12() ext-real Element of REAL
(cos . x) * (tan . x) is V11() V12() ext-real Element of REAL
((cos . x) * (tan . x)) + ((sin . x) * (diff (tan,x))) is V11() V12() ext-real Element of REAL
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((cos . x) ^2))) is set
(sin . x) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((cos . x) * (tan . x)) + ((sin . x) * (1 / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
(sin . x) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() set
K37((sin . x),K39((cos . x))) is set
(cos . x) / 1 is V11() V12() ext-real Element of REAL
K39(1) is V11() set
K37((cos . x),K39(1)) is set
((sin . x) / (cos . x)) * ((cos . x) / 1) is V11() V12() ext-real Element of REAL
(((sin . x) / (cos . x)) * ((cos . x) / 1)) + ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
(cos . x) / (cos . x) is V11() V12() ext-real Element of REAL
K37((cos . x),K39((cos . x))) is set
(sin . x) * ((cos . x) / (cos . x)) is V11() V12() ext-real Element of REAL
((sin . x) * ((cos . x) / (cos . x))) + ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
(sin . x) * 1 is V11() V12() ext-real Element of REAL
((sin . x) * 1) + ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin (#) tan) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37((sin . x),K39(((cos . x) ^2))) is set
(sin . x) + ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
sin (#) cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin (#) cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin (#) cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom sin) /\ (dom cot) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin (#) cot) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(cos . x) * (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
1 / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() set
K37(1,K39((sin . x))) is set
((cos . x) * (cot . x)) - (1 / (sin . x)) is V11() V12() ext-real Element of REAL
K38((1 / (sin . x))) is V11() set
K36(((cos . x) * (cot . x)),K38((1 / (sin . x)))) is set
diff (sin,x) is V11() V12() ext-real Element of REAL
(diff (sin,x)) * (cot . x) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(sin . x) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
((diff (sin,x)) * (cot . x)) + ((sin . x) * (diff (cot,x))) is V11() V12() ext-real Element of REAL
((cos . x) * (cot . x)) + ((sin . x) * (diff (cot,x))) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(sin . x) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((cos . x) * (cot . x)) + ((sin . x) * (- (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(sin . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((sin . x) ^2))) is set
((cos . x) * (cot . x)) - ((sin . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38(((sin . x) / ((sin . x) ^2))) is V11() set
K36(((cos . x) * (cot . x)),K38(((sin . x) / ((sin . x) ^2)))) is set
(sin . x) / (sin . x) is V11() V12() ext-real Element of REAL
K37((sin . x),K39((sin . x))) is set
((sin . x) / (sin . x)) / (sin . x) is V11() V12() ext-real Element of REAL
K37(((sin . x) / (sin . x)),K39((sin . x))) is set
((cos . x) * (cot . x)) - (((sin . x) / (sin . x)) / (sin . x)) is V11() V12() ext-real Element of REAL
K38((((sin . x) / (sin . x)) / (sin . x))) is V11() set
K36(((cos . x) * (cot . x)),K38((((sin . x) / (sin . x)) / (sin . x)))) is set
x is V11() V12() ext-real Element of REAL
((sin (#) cot) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(cos . x) * (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
1 / (sin . x) is V11() V12() ext-real Element of REAL
K39((sin . x)) is V11() set
K37(1,K39((sin . x))) is set
((cos . x) * (cot . x)) - (1 / (sin . x)) is V11() V12() ext-real Element of REAL
K38((1 / (sin . x))) is V11() set
K36(((cos . x) * (cot . x)),K38((1 / (sin . x)))) is set
cos (#) tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos (#) tan) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos (#) tan) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom cos) /\ (dom tan) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
x is V11() V12() ext-real Element of REAL
((cos (#) tan) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
cos . x is V11() V12() ext-real Element of REAL
((sin . x) ^2) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() set
K37(((sin . x) ^2),K39((cos . x))) is set
- (((sin . x) ^2) / (cos . x)) is V11() V12() ext-real Element of REAL
1 / (cos . x) is V11() V12() ext-real Element of REAL
K37(1,K39((cos . x))) is set
(- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
(diff (cos,x)) * (tan . x) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(cos . x) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
((diff (cos,x)) * (tan . x)) + ((cos . x) * (diff (tan,x))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(tan . x) * (- (sin . x)) is V11() V12() ext-real Element of REAL
((tan . x) * (- (sin . x))) + ((cos . x) * (diff (tan,x))) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(cos . x) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
((tan . x) * (- (sin . x))) + ((cos . x) * (1 / ((cos . x) ^2))) is V11() V12() ext-real Element of REAL
(sin . x) / (cos . x) is V11() V12() ext-real Element of REAL
K37((sin . x),K39((cos . x))) is set
(sin . x) / 1 is V11() V12() ext-real Element of REAL
K39(1) is V11() set
K37((sin . x),K39(1)) is set
- ((sin . x) / 1) is V11() V12() ext-real Element of REAL
((sin . x) / (cos . x)) * (- ((sin . x) / 1)) is V11() V12() ext-real Element of REAL
(cos . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((cos . x) ^2))) is set
(((sin . x) / (cos . x)) * (- ((sin . x) / 1))) + ((cos . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
(cos . x) / (cos . x) is V11() V12() ext-real Element of REAL
K37((cos . x),K39((cos . x))) is set
((cos . x) / (cos . x)) / (cos . x) is V11() V12() ext-real Element of REAL
K37(((cos . x) / (cos . x)),K39((cos . x))) is set
(- (((sin . x) ^2) / (cos . x))) + (((cos . x) / (cos . x)) / (cos . x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos (#) tan) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
cos . x is V11() V12() ext-real Element of REAL
((sin . x) ^2) / (cos . x) is V11() V12() ext-real Element of REAL
K39((cos . x)) is V11() set
K37(((sin . x) ^2),K39((cos . x))) is set
- (((sin . x) ^2) / (cos . x)) is V11() V12() ext-real Element of REAL
1 / (cos . x) is V11() V12() ext-real Element of REAL
K37(1,K39((cos . x))) is set
(- (((sin . x) ^2) / (cos . x))) + (1 / (cos . x)) is V11() V12() ext-real Element of REAL
sin (#) cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin (#) cos) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin (#) cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
(dom sin) /\ (dom cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((sin (#) cos) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
((cos . x) ^2) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() set
K36(((cos . x) ^2),K38(((sin . x) ^2))) is set
diff (sin,x) is V11() V12() ext-real Element of REAL
(diff (sin,x)) * (cos . x) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
(sin . x) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
((diff (sin,x)) * (cos . x)) + ((sin . x) * (diff (cos,x))) is V11() V12() ext-real Element of REAL
(cos . x) * (cos . x) is V11() V12() ext-real Element of REAL
((cos . x) * (cos . x)) + ((sin . x) * (diff (cos,x))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(sin . x) * (- (sin . x)) is V11() V12() ext-real Element of REAL
((cos . x) * (cos . x)) + ((sin . x) * (- (sin . x))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin (#) cos) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
((cos . x) ^2) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() set
K36(((cos . x) ^2),K38(((sin . x) ^2))) is set
ln (#) sin is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (ln (#) sin) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(ln (#) sin) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom ln) /\ (dom sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : not b₁ <= 0 } is set
c₃ is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37(1,K39(x)) is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : not b₁ <= 0 } is set
x is V11() V12() ext-real Element of REAL
((ln (#) sin) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37((sin . x),K39(x)) is set
ln . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(ln . x) * (cos . x) is V11() V12() ext-real Element of REAL
((sin . x) / x) + ((ln . x) * (cos . x)) is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
(sin . x) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
(ln . x) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
((sin . x) * (diff (ln,x))) + ((ln . x) * (diff (sin,x))) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K37(1,K39(x)) is set
(sin . x) * (1 / x) is V11() V12() ext-real Element of REAL
((sin . x) * (1 / x)) + ((ln . x) * (diff (sin,x))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln (#) sin) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37((sin . x),K39(x)) is set
ln . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(ln . x) * (cos . x) is V11() V12() ext-real Element of REAL
((sin . x) / x) + ((ln . x) * (cos . x)) is V11() V12() ext-real Element of REAL
ln (#) cos is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (ln (#) cos) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(ln (#) cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom ln) /\ (dom cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
{ b<sub>1</sub> where b<sub>1</sub> is V11() V12() ext-real Element of REAL : not b<sub>1</sub> <= 0 } is set
c<sub>3</sub> is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37(1,K39(x)) is set
{ b<sub>1</sub> where b<sub>1</sub> is V11() V12() ext-real Element of REAL : not b<sub>1</sub> <= 0 } is set
x is V11() V12() ext-real Element of REAL
((ln (#) cos) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37((cos . x),K39(x)) is set
ln . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(ln . x) * (sin . x) is V11() V12() ext-real Element of REAL
((cos . x) / x) - ((ln . x) * (sin . x)) is V11() V12() ext-real Element of REAL
K38(((ln . x) * (sin . x))) is V11() set
K36(((cos . x) / x),K38(((ln . x) * (sin . x)))) is set
diff (ln,x) is V11() V12() ext-real Element of REAL
(cos . x) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
(ln . x) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
((cos . x) * (diff (ln,x))) + ((ln . x) * (diff (cos,x))) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K37(1,K39(x)) is set
(cos . x) * (1 / x) is V11() V12() ext-real Element of REAL
((cos . x) * (1 / x)) + ((ln . x) * (diff (cos,x))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
(ln . x) * (- (sin . x)) is V11() V12() ext-real Element of REAL
((cos . x) / x) + ((ln . x) * (- (sin . x))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln (#) cos) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37((cos . x),K39(x)) is set
ln . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(ln . x) * (sin . x) is V11() V12() ext-real Element of REAL
((cos . x) / x) - ((ln . x) * (sin . x)) is V11() V12() ext-real Element of REAL
K38(((ln . x) * (sin . x))) is V11() set
K36(((cos . x) / x),K38(((ln . x) * (sin . x)))) is set
ln (#) exp_R is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (ln (#) exp_R) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(ln (#) exp_R) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom ln) /\ (dom exp_R) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : not b₁ <= 0 } is set
c₃ is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37(1,K39(x)) is set
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : not b₁ <= 0 } is set
x is V11() V12() ext-real Element of REAL
((ln (#) exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
(exp_R . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37((exp_R . x),K39(x)) is set
ln . x is V11() V12() ext-real Element of REAL
(ln . x) * (exp_R . x) is V11() V12() ext-real Element of REAL
((exp_R . x) / x) + ((ln . x) * (exp_R . x)) is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (diff (ln,x)) is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
(ln . x) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
((exp_R . x) * (diff (ln,x))) + ((ln . x) * (diff (exp_R,x))) is V11() V12() ext-real Element of REAL
1 / x is V11() V12() ext-real Element of REAL
K37(1,K39(x)) is set
(exp_R . x) * (1 / x) is V11() V12() ext-real Element of REAL
((exp_R . x) * (1 / x)) + ((ln . x) * (diff (exp_R,x))) is V11() V12() ext-real Element of REAL
((exp_R . x) * (1 / x)) + ((ln . x) * (exp_R . x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln (#) exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
(exp_R . x) / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37((exp_R . x),K39(x)) is set
ln . x is V11() V12() ext-real Element of REAL
(ln . x) * (exp_R . x) is V11() V12() ext-real Element of REAL
((exp_R . x) / x) + ((ln . x) * (exp_R . x)) is V11() V12() ext-real Element of REAL
ln * ln is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (ln * ln) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(ln * ln) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
].0,+infty.[ is V62() V63() V64() Element of K6(REAL)
{ b<sub>1</sub> where b<sub>1</sub> is V11() V12() ext-real Element of REAL : not b<sub>1</sub> <= 0 } is set
c<sub>3</sub> is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln * ln) `| Z) . x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
(ln . x) * x is V11() V12() ext-real Element of REAL
1 / ((ln . x) * x) is V11() V12() ext-real Element of REAL
K39(((ln . x) * x)) is V11() set
K37(1,K39(((ln . x) * x))) is set
].0,+infty.[ is V62() V63() V64() Element of K6(REAL)
{ b₁ where b₁ is V11() V12() ext-real Element of REAL : not b₁ <= 0 } is set
diff ((ln * ln),x) is V11() V12() ext-real Element of REAL
diff (ln,x) is V11() V12() ext-real Element of REAL
(diff (ln,x)) / (ln . x) is V11() V12() ext-real Element of REAL
K39((ln . x)) is V11() set
K37((diff (ln,x)),K39((ln . x))) is set
1 / (ln . x) is V11() V12() ext-real Element of REAL
K37(1,K39((ln . x))) is set
1 / x is V11() V12() ext-real Element of REAL
K39(x) is V11() set
K37(1,K39(x)) is set
(1 / (ln . x)) * (1 / x) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((ln * ln) `| Z) . x is V11() V12() ext-real Element of REAL
ln . x is V11() V12() ext-real Element of REAL
(ln . x) * x is V11() V12() ext-real Element of REAL
1 / ((ln . x) * x) is V11() V12() ext-real Element of REAL
K39(((ln . x) * x)) is V11() set
K37(1,K39(((ln . x) * x))) is set
exp_R * exp_R is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R * exp_R) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R * exp_R) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
exp_R . (exp_R . x) is V11() V12() ext-real Element of REAL
(exp_R . (exp_R . x)) * (exp_R . x) is V11() V12() ext-real Element of REAL
diff ((exp_R * exp_R),x) is V11() V12() ext-real Element of REAL
diff (exp_R,(exp_R . x)) is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
(diff (exp_R,(exp_R . x))) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
(exp_R . (exp_R . x)) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
exp_R . (exp_R . x) is V11() V12() ext-real Element of REAL
(exp_R . (exp_R . x)) * (exp_R . x) is V11() V12() ext-real Element of REAL
sin * tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin * tan) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin * tan) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
dom (sin / cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos (tan . x) is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
(cos (tan . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37((cos (tan . x)),K39(((cos . x) ^2))) is set
diff ((sin * tan),x) is V11() V12() ext-real Element of REAL
diff (sin,(tan . x)) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(diff (sin,(tan . x))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
(cos (tan . x)) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((cos . x) ^2))) is set
(cos (tan . x)) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cos (tan . x) is V11() V12() ext-real Element of REAL
cos . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
(cos (tan . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37((cos (tan . x)),K39(((cos . x) ^2))) is set
sin * cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin * cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin * cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
dom (cos / sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos (cot . x) is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(cos (cot . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37((cos (cot . x)),K39(((sin . x) ^2))) is set
- ((cos (cot . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
diff ((sin * cot),x) is V11() V12() ext-real Element of REAL
diff (sin,(cot . x)) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(diff (sin,(cot . x))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
(cos (cot . x)) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((sin . x) ^2))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(cos (cot . x)) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
cos (cot . x) is V11() V12() ext-real Element of REAL
cos . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(cos (cot . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37((cos (cot . x)),K39(((sin . x) ^2))) is set
- ((cos (cot . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
cos * tan is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos * tan) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos * tan) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
dom (sin / cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin (tan . x) is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
(sin (tan . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37((sin (tan . x)),K39(((cos . x) ^2))) is set
- ((sin (tan . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
diff ((cos * tan),x) is V11() V12() ext-real Element of REAL
diff (cos,(tan . x)) is V11() V12() ext-real Element of REAL
diff (tan,x) is V11() V12() ext-real Element of REAL
(diff (cos,(tan . x))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
- (sin (tan . x)) is V11() V12() ext-real Element of REAL
(- (sin (tan . x))) * (diff (tan,x)) is V11() V12() ext-real Element of REAL
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((cos . x) ^2))) is set
(- (sin (tan . x))) * (1 / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * tan) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
sin (tan . x) is V11() V12() ext-real Element of REAL
sin . (tan . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
(sin (tan . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37((sin (tan . x)),K39(((cos . x) ^2))) is set
- ((sin (tan . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
cos * cot is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos * cot) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos * cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
dom (cos / sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin (cot . x) is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(sin (cot . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37((sin (cot . x)),K39(((sin . x) ^2))) is set
diff ((cos * cot),x) is V11() V12() ext-real Element of REAL
diff (cos,(cot . x)) is V11() V12() ext-real Element of REAL
diff (cot,x) is V11() V12() ext-real Element of REAL
(diff (cos,(cot . x))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
- (sin (cot . x)) is V11() V12() ext-real Element of REAL
(- (sin (cot . x))) * (diff (cot,x)) is V11() V12() ext-real Element of REAL
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37(1,K39(((sin . x) ^2))) is set
- (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- (sin (cot . x))) * (- (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * cot) `| Z) . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
sin (cot . x) is V11() V12() ext-real Element of REAL
sin . (cot . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(sin (cot . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37((sin (cot . x)),K39(((sin . x) ^2))) is set
sin (#) (tan + cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin (#) (tan + cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin (#) (tan + cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom (tan + cot)) /\ (dom sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((sin (#) (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
(cos . x) * ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
((tan + cot) . x) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
diff ((tan + cot),x) is V11() V12() ext-real Element of REAL
(sin . x) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
(((tan + cot) . x) * (diff (sin,x))) + ((sin . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
((tan . x) + (cot . x)) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (diff (sin,x))) + ((sin . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
((tan . x) + (cot . x)) * (cos . x) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
(tan + cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
(sin . x) * (((tan + cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * (((tan + cot) `| Z) . x)) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (cos . x)) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin (#) (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
(cos . x) * ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((cos . x) * ((tan . x) + (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
cos (#) (tan + cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos (#) (tan + cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos (#) (tan + cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom (tan + cot)) /\ (dom cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((cos (#) (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
(sin . x) * ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
- ((sin . x) * ((tan . x) + (cot . x))) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
((tan + cot) . x) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
diff ((tan + cot),x) is V11() V12() ext-real Element of REAL
(cos . x) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
(((tan + cot) . x) * (diff (cos,x))) + ((cos . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
((tan . x) + (cot . x)) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (diff (cos,x))) + ((cos . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
((tan . x) + (cot . x)) * (- (sin . x)) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
(tan + cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
(cos . x) * (((tan + cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * (((tan + cot) `| Z) . x)) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (- (sin . x))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos (#) (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
(sin . x) * ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
- ((sin . x) * ((tan . x) + (cot . x))) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(- ((sin . x) * ((tan . x) + (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
sin (#) (tan - cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin (#) (tan - cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin (#) (tan - cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom (tan - cot)) /\ (dom sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((sin (#) (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
(cos . x) * ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
((tan - cot) . x) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
diff ((tan - cot),x) is V11() V12() ext-real Element of REAL
(sin . x) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
(((tan - cot) . x) * (diff (sin,x))) + ((sin . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
((tan . x) - (cot . x)) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (diff (sin,x))) + ((sin . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
((tan . x) - (cot . x)) * (cos . x) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
(tan - cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
(sin . x) * (((tan - cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * (((tan - cot) `| Z) . x)) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (cos . x)) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin (#) (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
(cos . x) * ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((cos . x) * ((tan . x) - (cot . x))) + ((sin . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
cos (#) (tan - cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos (#) (tan - cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos (#) (tan - cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom (tan - cot)) /\ (dom cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((cos (#) (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
(sin . x) * ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
- ((sin . x) * ((tan . x) - (cot . x))) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
((tan - cot) . x) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
diff ((tan - cot),x) is V11() V12() ext-real Element of REAL
(cos . x) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
(((tan - cot) . x) * (diff (cos,x))) + ((cos . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
((tan . x) - (cot . x)) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (diff (cos,x))) + ((cos . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
((tan . x) - (cot . x)) * (- (sin . x)) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
(tan - cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
(cos . x) * (((tan - cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * (((tan - cot) `| Z) . x)) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (- (sin . x))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos (#) (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
(sin . x) * ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
- ((sin . x) * ((tan . x) - (cot . x))) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(- ((sin . x) * ((tan . x) - (cot . x)))) + ((cos . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
exp_R (#) (tan + cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R (#) (tan + cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R (#) (tan + cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom (tan + cot)) /\ (dom exp_R) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((exp_R (#) (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
(exp_R . x) * ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
((tan + cot) . x) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
diff ((tan + cot),x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
(((tan + cot) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
((tan . x) + (cot . x)) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
(((tan . x) + (cot . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * (diff ((tan + cot),x))) is V11() V12() ext-real Element of REAL
(tan + cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
(exp_R . x) * (((tan + cot) `| Z) . x) is V11() V12() ext-real Element of REAL
((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * (((tan + cot) `| Z) . x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R (#) (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
(exp_R . x) * ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((exp_R . x) * ((tan . x) + (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
exp_R (#) (tan - cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R (#) (tan - cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R (#) (tan - cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
(dom (tan - cot)) /\ (dom exp_R) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((exp_R (#) (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
(exp_R . x) * ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
((tan - cot) . x) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
diff ((tan - cot),x) is V11() V12() ext-real Element of REAL
(exp_R . x) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
(((tan - cot) . x) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
((tan . x) - (cot . x)) * (diff (exp_R,x)) is V11() V12() ext-real Element of REAL
(((tan . x) - (cot . x)) * (diff (exp_R,x))) + ((exp_R . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * (diff ((tan - cot),x))) is V11() V12() ext-real Element of REAL
(tan - cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
(exp_R . x) * (((tan - cot) `| Z) . x) is V11() V12() ext-real Element of REAL
((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * (((tan - cot) `| Z) . x)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R (#) (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
(exp_R . x) * ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
((exp_R . x) * ((tan . x) - (cot . x))) + ((exp_R . x) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
sin (#) (sin + cos) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin (#) (sin + cos)) is V62() V63() V64() Element of K6(REAL)
2 is V6() V10() V11() V12() ext-real non negative V47() V62() V63() V64() V65() V66() V67() V81() Element of NAT
Z is open V62() V63() V64() Element of K6(REAL)
(sin (#) (sin + cos)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom (sin + cos)) /\ (dom sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((sin (#) (sin + cos)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
sin . x is V11() V12() ext-real Element of REAL
2 * (sin . x) is V11() V12() ext-real Element of REAL
(2 * (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
((cos . x) ^2) + ((2 * (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() set
K36((((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))),K38(((sin . x) ^2))) is set
(sin + cos) . x is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
((sin + cos) . x) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
diff ((sin + cos),x) is V11() V12() ext-real Element of REAL
(sin . x) * (diff ((sin + cos),x)) is V11() V12() ext-real Element of REAL
(((sin + cos) . x) * (diff (sin,x))) + ((sin . x) * (diff ((sin + cos),x))) is V11() V12() ext-real Element of REAL
(sin . x) + (cos . x) is V11() V12() ext-real Element of REAL
((sin . x) + (cos . x)) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(((sin . x) + (cos . x)) * (diff (sin,x))) + ((sin . x) * (diff ((sin + cos),x))) is V11() V12() ext-real Element of REAL
((sin . x) + (cos . x)) * (cos . x) is V11() V12() ext-real Element of REAL
(((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * (diff ((sin + cos),x))) is V11() V12() ext-real Element of REAL
(sin + cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((sin + cos) `| Z) . x is V11() V12() ext-real Element of REAL
(sin . x) * (((sin + cos) `| Z) . x) is V11() V12() ext-real Element of REAL
(((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * (((sin + cos) `| Z) . x)) is V11() V12() ext-real Element of REAL
(cos . x) - (sin . x) is V11() V12() ext-real Element of REAL
K38((sin . x)) is V11() set
K36((cos . x),K38((sin . x))) is set
(sin . x) * ((cos . x) - (sin . x)) is V11() V12() ext-real Element of REAL
(((sin . x) + (cos . x)) * (cos . x)) + ((sin . x) * ((cos . x) - (sin . x))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin (#) (sin + cos)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
sin . x is V11() V12() ext-real Element of REAL
2 * (sin . x) is V11() V12() ext-real Element of REAL
(2 * (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
((cos . x) ^2) + ((2 * (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() set
K36((((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))),K38(((sin . x) ^2))) is set
sin (#) (sin - cos) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin (#) (sin - cos)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin (#) (sin - cos)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom (sin - cos)) /\ (dom sin) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((sin (#) (sin - cos)) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
2 * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(2 * (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
((sin . x) ^2) + ((2 * (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
(((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K38(((cos . x) ^2)) is V11() set
K36((((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))),K38(((cos . x) ^2))) is set
(sin - cos) . x is V11() V12() ext-real Element of REAL
diff (sin,x) is V11() V12() ext-real Element of REAL
((sin - cos) . x) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
diff ((sin - cos),x) is V11() V12() ext-real Element of REAL
(sin . x) * (diff ((sin - cos),x)) is V11() V12() ext-real Element of REAL
(((sin - cos) . x) * (diff (sin,x))) + ((sin . x) * (diff ((sin - cos),x))) is V11() V12() ext-real Element of REAL
(sin . x) - (cos . x) is V11() V12() ext-real Element of REAL
K38((cos . x)) is V11() set
K36((sin . x),K38((cos . x))) is set
((sin . x) - (cos . x)) * (diff (sin,x)) is V11() V12() ext-real Element of REAL
(((sin . x) - (cos . x)) * (diff (sin,x))) + ((sin . x) * (diff ((sin - cos),x))) is V11() V12() ext-real Element of REAL
((sin . x) - (cos . x)) * (cos . x) is V11() V12() ext-real Element of REAL
(((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * (diff ((sin - cos),x))) is V11() V12() ext-real Element of REAL
(sin - cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((sin - cos) `| Z) . x is V11() V12() ext-real Element of REAL
(sin . x) * (((sin - cos) `| Z) . x) is V11() V12() ext-real Element of REAL
(((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * (((sin - cos) `| Z) . x)) is V11() V12() ext-real Element of REAL
(cos . x) + (sin . x) is V11() V12() ext-real Element of REAL
(sin . x) * ((cos . x) + (sin . x)) is V11() V12() ext-real Element of REAL
(((sin . x) - (cos . x)) * (cos . x)) + ((sin . x) * ((cos . x) + (sin . x))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin (#) (sin - cos)) `| Z) . x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
2 * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(2 * (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
((sin . x) ^2) + ((2 * (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
(((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K38(((cos . x) ^2)) is V11() set
K36((((sin . x) ^2) + ((2 * (sin . x)) * (cos . x))),K38(((cos . x) ^2))) is set
cos (#) (sin - cos) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos (#) (sin - cos)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos (#) (sin - cos)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom (sin - cos)) /\ (dom cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((cos (#) (sin - cos)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
sin . x is V11() V12() ext-real Element of REAL
2 * (sin . x) is V11() V12() ext-real Element of REAL
(2 * (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
((cos . x) ^2) + ((2 * (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() set
K36((((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))),K38(((sin . x) ^2))) is set
(sin - cos) . x is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
((sin - cos) . x) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
diff ((sin - cos),x) is V11() V12() ext-real Element of REAL
(cos . x) * (diff ((sin - cos),x)) is V11() V12() ext-real Element of REAL
(((sin - cos) . x) * (diff (cos,x))) + ((cos . x) * (diff ((sin - cos),x))) is V11() V12() ext-real Element of REAL
(sin . x) - (cos . x) is V11() V12() ext-real Element of REAL
K38((cos . x)) is V11() set
K36((sin . x),K38((cos . x))) is set
((sin . x) - (cos . x)) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
(((sin . x) - (cos . x)) * (diff (cos,x))) + ((cos . x) * (diff ((sin - cos),x))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
((sin . x) - (cos . x)) * (- (sin . x)) is V11() V12() ext-real Element of REAL
(((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * (diff ((sin - cos),x))) is V11() V12() ext-real Element of REAL
(sin - cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((sin - cos) `| Z) . x is V11() V12() ext-real Element of REAL
(cos . x) * (((sin - cos) `| Z) . x) is V11() V12() ext-real Element of REAL
(((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * (((sin - cos) `| Z) . x)) is V11() V12() ext-real Element of REAL
(cos . x) + (sin . x) is V11() V12() ext-real Element of REAL
(cos . x) * ((cos . x) + (sin . x)) is V11() V12() ext-real Element of REAL
(((sin . x) - (cos . x)) * (- (sin . x))) + ((cos . x) * ((cos . x) + (sin . x))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos (#) (sin - cos)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
sin . x is V11() V12() ext-real Element of REAL
2 * (sin . x) is V11() V12() ext-real Element of REAL
(2 * (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
((cos . x) ^2) + ((2 * (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() set
K36((((cos . x) ^2) + ((2 * (sin . x)) * (cos . x))),K38(((sin . x) ^2))) is set
cos (#) (sin + cos) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos (#) (sin + cos)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos (#) (sin + cos)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(dom (sin + cos)) /\ (dom cos) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
((cos (#) (sin + cos)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
sin . x is V11() V12() ext-real Element of REAL
2 * (sin . x) is V11() V12() ext-real Element of REAL
(2 * (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
((cos . x) ^2) - ((2 * (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
K38(((2 * (sin . x)) * (cos . x))) is V11() set
K36(((cos . x) ^2),K38(((2 * (sin . x)) * (cos . x)))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() set
K36((((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))),K38(((sin . x) ^2))) is set
(sin + cos) . x is V11() V12() ext-real Element of REAL
diff (cos,x) is V11() V12() ext-real Element of REAL
((sin + cos) . x) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
diff ((sin + cos),x) is V11() V12() ext-real Element of REAL
(cos . x) * (diff ((sin + cos),x)) is V11() V12() ext-real Element of REAL
(((sin + cos) . x) * (diff (cos,x))) + ((cos . x) * (diff ((sin + cos),x))) is V11() V12() ext-real Element of REAL
(sin . x) + (cos . x) is V11() V12() ext-real Element of REAL
((sin . x) + (cos . x)) * (diff (cos,x)) is V11() V12() ext-real Element of REAL
(((sin . x) + (cos . x)) * (diff (cos,x))) + ((cos . x) * (diff ((sin + cos),x))) is V11() V12() ext-real Element of REAL
- (sin . x) is V11() V12() ext-real Element of REAL
((sin . x) + (cos . x)) * (- (sin . x)) is V11() V12() ext-real Element of REAL
(((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * (diff ((sin + cos),x))) is V11() V12() ext-real Element of REAL
(sin + cos) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((sin + cos) `| Z) . x is V11() V12() ext-real Element of REAL
(cos . x) * (((sin + cos) `| Z) . x) is V11() V12() ext-real Element of REAL
(((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * (((sin + cos) `| Z) . x)) is V11() V12() ext-real Element of REAL
(cos . x) - (sin . x) is V11() V12() ext-real Element of REAL
K38((sin . x)) is V11() set
K36((cos . x),K38((sin . x))) is set
(cos . x) * ((cos . x) - (sin . x)) is V11() V12() ext-real Element of REAL
(((sin . x) + (cos . x)) * (- (sin . x))) + ((cos . x) * ((cos . x) - (sin . x))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos (#) (sin + cos)) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
sin . x is V11() V12() ext-real Element of REAL
2 * (sin . x) is V11() V12() ext-real Element of REAL
(2 * (sin . x)) * (cos . x) is V11() V12() ext-real Element of REAL
((cos . x) ^2) - ((2 * (sin . x)) * (cos . x)) is V11() V12() ext-real Element of REAL
K38(((2 * (sin . x)) * (cos . x))) is V11() set
K36(((cos . x) ^2),K38(((2 * (sin . x)) * (cos . x)))) is set
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
(((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))) - ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K38(((sin . x) ^2)) is V11() set
K36((((cos . x) ^2) - ((2 * (sin . x)) * (cos . x))),K38(((sin . x) ^2))) is set
sin * (tan + cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin * (tan + cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin * (tan + cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
cos . ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
diff ((sin * (tan + cot)),x) is V11() V12() ext-real Element of REAL
diff (sin,((tan + cot) . x)) is V11() V12() ext-real Element of REAL
diff ((tan + cot),x) is V11() V12() ext-real Element of REAL
(diff (sin,((tan + cot) . x))) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
cos . ((tan + cot) . x) is V11() V12() ext-real Element of REAL
(cos . ((tan + cot) . x)) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
(tan + cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
(cos . ((tan + cot) . x)) * (((tan + cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(cos . ((tan + cot) . x)) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
cos . ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(cos . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
sin * (tan - cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin * (tan - cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin * (tan - cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
cos . ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
diff ((sin * (tan - cot)),x) is V11() V12() ext-real Element of REAL
diff (sin,((tan - cot) . x)) is V11() V12() ext-real Element of REAL
diff ((tan - cot),x) is V11() V12() ext-real Element of REAL
(diff (sin,((tan - cot) . x))) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
cos . ((tan - cot) . x) is V11() V12() ext-real Element of REAL
(cos . ((tan - cot) . x)) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
(tan - cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
(cos . ((tan - cot) . x)) * (((tan - cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(cos . ((tan - cot) . x)) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
cos . ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(cos . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
cos * (tan - cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos * (tan - cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos * (tan - cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
sin . ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
- ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
diff ((cos * (tan - cot)),x) is V11() V12() ext-real Element of REAL
diff (cos,((tan - cot) . x)) is V11() V12() ext-real Element of REAL
diff ((tan - cot),x) is V11() V12() ext-real Element of REAL
(diff (cos,((tan - cot) . x))) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
sin . ((tan - cot) . x) is V11() V12() ext-real Element of REAL
- (sin . ((tan - cot) . x)) is V11() V12() ext-real Element of REAL
(- (sin . ((tan - cot) . x))) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
(tan - cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
(- (sin . ((tan - cot) . x))) * (((tan - cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(- (sin . ((tan - cot) . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
- (sin . ((tan . x) - (cot . x))) is V11() V12() ext-real Element of REAL
(- (sin . ((tan . x) - (cot . x)))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
sin . ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
- ((sin . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
cos * (tan + cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos * (tan + cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos * (tan + cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
sin . ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
- ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
diff ((cos * (tan + cot)),x) is V11() V12() ext-real Element of REAL
diff (cos,((tan + cot) . x)) is V11() V12() ext-real Element of REAL
diff ((tan + cot),x) is V11() V12() ext-real Element of REAL
(diff (cos,((tan + cot) . x))) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
sin . ((tan + cot) . x) is V11() V12() ext-real Element of REAL
- (sin . ((tan + cot) . x)) is V11() V12() ext-real Element of REAL
(- (sin . ((tan + cot) . x))) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
(tan + cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
(- (sin . ((tan + cot) . x))) * (((tan + cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(- (sin . ((tan + cot) . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
- (sin . ((tan . x) + (cot . x))) is V11() V12() ext-real Element of REAL
(- (sin . ((tan . x) + (cot . x)))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
sin . ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
- ((sin . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)))) is V11() V12() ext-real Element of REAL
exp_R * (tan + cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R * (tan + cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R * (tan + cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
exp_R . ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(tan + cot) . x is V11() V12() ext-real Element of REAL
diff ((exp_R * (tan + cot)),x) is V11() V12() ext-real Element of REAL
diff (exp_R,((tan + cot) . x)) is V11() V12() ext-real Element of REAL
diff ((tan + cot),x) is V11() V12() ext-real Element of REAL
(diff (exp_R,((tan + cot) . x))) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
exp_R . ((tan + cot) . x) is V11() V12() ext-real Element of REAL
(exp_R . ((tan + cot) . x)) * (diff ((tan + cot),x)) is V11() V12() ext-real Element of REAL
(tan + cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
(exp_R . ((tan + cot) . x)) * (((tan + cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(exp_R . ((tan + cot) . x)) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * (tan + cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
exp_R . ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
(exp_R . ((tan . x) + (cot . x))) * ((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
exp_R * (tan - cot) is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (exp_R * (tan - cot)) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(exp_R * (tan - cot)) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
exp_R . ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(tan - cot) . x is V11() V12() ext-real Element of REAL
diff ((exp_R * (tan - cot)),x) is V11() V12() ext-real Element of REAL
diff (exp_R,((tan - cot) . x)) is V11() V12() ext-real Element of REAL
diff ((tan - cot),x) is V11() V12() ext-real Element of REAL
(diff (exp_R,((tan - cot) . x))) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
exp_R . ((tan - cot) . x) is V11() V12() ext-real Element of REAL
(exp_R . ((tan - cot) . x)) * (diff ((tan - cot),x)) is V11() V12() ext-real Element of REAL
(tan - cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
(exp_R . ((tan - cot) . x)) * (((tan - cot) `| Z) . x) is V11() V12() ext-real Element of REAL
(exp_R . ((tan - cot) . x)) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((exp_R * (tan - cot)) `| Z) . x is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
cot . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
exp_R . ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(exp_R . ((tan . x) - (cot . x))) * ((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
(tan - cot) / exp_R is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((tan - cot) / exp_R) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
((tan - cot) / exp_R) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
exp_R " {0} is V62() V63() V64() Element of K6(REAL)
(dom exp_R) \ (exp_R " {0}) is V62() V63() V64() Element of K6(REAL)
(dom (tan - cot)) /\ ((dom exp_R) \ (exp_R " {0})) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
(((tan - cot) / exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x) is V11() V12() ext-real Element of REAL
K38((tan . x)) is V11() set
K36(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))),K38((tan . x))) is set
cot . x is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x) is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) is V11() V12() ext-real Element of REAL
K39((exp_R . x)) is V11() set
K37(((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)),K39((exp_R . x))) is set
(tan - cot) . x is V11() V12() ext-real Element of REAL
(tan . x) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((tan . x),K38((cot . x))) is set
diff (((tan - cot) / exp_R),x) is V11() V12() ext-real Element of REAL
diff ((tan - cot),x) is V11() V12() ext-real Element of REAL
(diff ((tan - cot),x)) * (exp_R . x) is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
(diff (exp_R,x)) * ((tan - cot) . x) is V11() V12() ext-real Element of REAL
((diff ((tan - cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x)) is V11() V12() ext-real Element of REAL
K38(((diff (exp_R,x)) * ((tan - cot) . x))) is V11() set
K36(((diff ((tan - cot),x)) * (exp_R . x)),K38(((diff (exp_R,x)) * ((tan - cot) . x)))) is set
(exp_R . x) ^2 is V11() V12() ext-real Element of REAL
K37((exp_R . x),(exp_R . x)) is set
(((diff ((tan - cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) is V11() V12() ext-real Element of REAL
K39(((exp_R . x) ^2)) is V11() set
K37((((diff ((tan - cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))),K39(((exp_R . x) ^2))) is set
(tan - cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan - cot) `| Z) . x is V11() V12() ext-real Element of REAL
(((tan - cot) `| Z) . x) * (exp_R . x) is V11() V12() ext-real Element of REAL
((((tan - cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x)) is V11() V12() ext-real Element of REAL
K36(((((tan - cot) `| Z) . x) * (exp_R . x)),K38(((diff (exp_R,x)) * ((tan - cot) . x)))) is set
(((((tan - cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) is V11() V12() ext-real Element of REAL
K37((((((tan - cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))),K39(((exp_R . x) ^2))) is set
((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x) is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x)) is V11() V12() ext-real Element of REAL
K36((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)),K38(((diff (exp_R,x)) * ((tan - cot) . x)))) is set
((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))) / ((exp_R . x) ^2) is V11() V12() ext-real Element of REAL
K37(((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan - cot) . x))),K39(((exp_R . x) ^2))) is set
(exp_R . x) * ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) - (cot . x))) is V11() V12() ext-real Element of REAL
K38(((exp_R . x) * ((tan . x) - (cot . x)))) is V11() set
K36((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)),K38(((exp_R . x) * ((tan . x) - (cot . x))))) is set
(exp_R . x) * (exp_R . x) is V11() V12() ext-real Element of REAL
((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) - (cot . x)))) / ((exp_R . x) * (exp_R . x)) is V11() V12() ext-real Element of REAL
K39(((exp_R . x) * (exp_R . x))) is V11() set
K37(((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) - (cot . x)))),K39(((exp_R . x) * (exp_R . x)))) is set
((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x)) is V11() V12() ext-real Element of REAL
K38(((tan . x) - (cot . x))) is V11() set
K36(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))),K38(((tan . x) - (cot . x)))) is set
(exp_R . x) / ((exp_R . x) * (exp_R . x)) is V11() V12() ext-real Element of REAL
K37((exp_R . x),K39(((exp_R . x) * (exp_R . x)))) is set
(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))) is V11() V12() ext-real Element of REAL
(exp_R . x) / (exp_R . x) is V11() V12() ext-real Element of REAL
K37((exp_R . x),K39((exp_R . x))) is set
((exp_R . x) / (exp_R . x)) / (exp_R . x) is V11() V12() ext-real Element of REAL
K37(((exp_R . x) / (exp_R . x)),K39((exp_R . x))) is set
(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x)) is V11() V12() ext-real Element of REAL
1 / (exp_R . x) is V11() V12() ext-real Element of REAL
K37(1,K39((exp_R . x))) is set
(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) * (1 / (exp_R . x)) is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))) / (exp_R . x) is V11() V12() ext-real Element of REAL
K37((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - ((tan . x) - (cot . x))),K39((exp_R . x))) is set
x is V11() V12() ext-real Element of REAL
(((tan - cot) / exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
tan . x is V11() V12() ext-real Element of REAL
((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x) is V11() V12() ext-real Element of REAL
K38((tan . x)) is V11() set
K36(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))),K38((tan . x))) is set
cot . x is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x) is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)) / (exp_R . x) is V11() V12() ext-real Element of REAL
K39((exp_R . x)) is V11() set
K37(((((1 / ((cos . x) ^2)) + (1 / ((sin . x) ^2))) - (tan . x)) + (cot . x)),K39((exp_R . x))) is set
(tan + cot) / exp_R is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom ((tan + cot) / exp_R) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
((tan + cot) / exp_R) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
x is V11() V12() ext-real Element of REAL
exp_R . x is V11() V12() ext-real Element of REAL
exp_R " {0} is V62() V63() V64() Element of K6(REAL)
(dom exp_R) \ (exp_R " {0}) is V62() V63() V64() Element of K6(REAL)
(dom (tan + cot)) /\ ((dom exp_R) \ (exp_R " {0})) is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
(((tan + cot) / exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
tan . x is V11() V12() ext-real Element of REAL
((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x) is V11() V12() ext-real Element of REAL
K38((tan . x)) is V11() set
K36(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))),K38((tan . x))) is set
cot . x is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)),K38((cot . x))) is set
exp_R . x is V11() V12() ext-real Element of REAL
((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) is V11() V12() ext-real Element of REAL
K39((exp_R . x)) is V11() set
K37(((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)),K39((exp_R . x))) is set
(tan + cot) . x is V11() V12() ext-real Element of REAL
(tan . x) + (cot . x) is V11() V12() ext-real Element of REAL
diff (((tan + cot) / exp_R),x) is V11() V12() ext-real Element of REAL
diff ((tan + cot),x) is V11() V12() ext-real Element of REAL
(diff ((tan + cot),x)) * (exp_R . x) is V11() V12() ext-real Element of REAL
diff (exp_R,x) is V11() V12() ext-real Element of REAL
(diff (exp_R,x)) * ((tan + cot) . x) is V11() V12() ext-real Element of REAL
((diff ((tan + cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x)) is V11() V12() ext-real Element of REAL
K38(((diff (exp_R,x)) * ((tan + cot) . x))) is V11() set
K36(((diff ((tan + cot),x)) * (exp_R . x)),K38(((diff (exp_R,x)) * ((tan + cot) . x)))) is set
(exp_R . x) ^2 is V11() V12() ext-real Element of REAL
K37((exp_R . x),(exp_R . x)) is set
(((diff ((tan + cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) is V11() V12() ext-real Element of REAL
K39(((exp_R . x) ^2)) is V11() set
K37((((diff ((tan + cot),x)) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))),K39(((exp_R . x) ^2))) is set
(tan + cot) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
((tan + cot) `| Z) . x is V11() V12() ext-real Element of REAL
(((tan + cot) `| Z) . x) * (exp_R . x) is V11() V12() ext-real Element of REAL
((((tan + cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x)) is V11() V12() ext-real Element of REAL
K36(((((tan + cot) `| Z) . x) * (exp_R . x)),K38(((diff (exp_R,x)) * ((tan + cot) . x)))) is set
(((((tan + cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) is V11() V12() ext-real Element of REAL
K37((((((tan + cot) `| Z) . x) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))),K39(((exp_R . x) ^2))) is set
((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x) is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x)) is V11() V12() ext-real Element of REAL
K36((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)),K38(((diff (exp_R,x)) * ((tan + cot) . x)))) is set
((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))) / ((exp_R . x) ^2) is V11() V12() ext-real Element of REAL
K37(((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((diff (exp_R,x)) * ((tan + cot) . x))),K39(((exp_R . x) ^2))) is set
(exp_R . x) * ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) + (cot . x))) is V11() V12() ext-real Element of REAL
K38(((exp_R . x) * ((tan . x) + (cot . x)))) is V11() set
K36((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)),K38(((exp_R . x) * ((tan . x) + (cot . x))))) is set
(exp_R . x) * (exp_R . x) is V11() V12() ext-real Element of REAL
((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) + (cot . x)))) / ((exp_R . x) * (exp_R . x)) is V11() V12() ext-real Element of REAL
K39(((exp_R . x) * (exp_R . x))) is V11() set
K37(((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) * (exp_R . x)) - ((exp_R . x) * ((tan . x) + (cot . x)))),K39(((exp_R . x) * (exp_R . x)))) is set
((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x)) is V11() V12() ext-real Element of REAL
K38(((tan . x) + (cot . x))) is V11() set
K36(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))),K38(((tan . x) + (cot . x)))) is set
(exp_R . x) / ((exp_R . x) * (exp_R . x)) is V11() V12() ext-real Element of REAL
K37((exp_R . x),K39(((exp_R . x) * (exp_R . x)))) is set
(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * ((exp_R . x) / ((exp_R . x) * (exp_R . x))) is V11() V12() ext-real Element of REAL
(exp_R . x) / (exp_R . x) is V11() V12() ext-real Element of REAL
K37((exp_R . x),K39((exp_R . x))) is set
((exp_R . x) / (exp_R . x)) / (exp_R . x) is V11() V12() ext-real Element of REAL
K37(((exp_R . x) / (exp_R . x)),K39((exp_R . x))) is set
(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * (((exp_R . x) / (exp_R . x)) / (exp_R . x)) is V11() V12() ext-real Element of REAL
1 / (exp_R . x) is V11() V12() ext-real Element of REAL
K37(1,K39((exp_R . x))) is set
(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) * (1 / (exp_R . x)) is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))) / (exp_R . x) is V11() V12() ext-real Element of REAL
K37((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - ((tan . x) + (cot . x))),K39((exp_R . x))) is set
x is V11() V12() ext-real Element of REAL
(((tan + cot) / exp_R) `| Z) . x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
1 / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(1,K39(((cos . x) ^2))) is set
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
1 / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(1,K39(((sin . x) ^2))) is set
(1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
K38((1 / ((sin . x) ^2))) is V11() set
K36((1 / ((cos . x) ^2)),K38((1 / ((sin . x) ^2)))) is set
tan . x is V11() V12() ext-real Element of REAL
((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x) is V11() V12() ext-real Element of REAL
K38((tan . x)) is V11() set
K36(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))),K38((tan . x))) is set
cot . x is V11() V12() ext-real Element of REAL
(((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x) is V11() V12() ext-real Element of REAL
K38((cot . x)) is V11() set
K36((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)),K38((cot . x))) is set
exp_R . x is V11() V12() ext-real Element of REAL
((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)) / (exp_R . x) is V11() V12() ext-real Element of REAL
K39((exp_R . x)) is V11() set
K37(((((1 / ((cos . x) ^2)) - (1 / ((sin . x) ^2))) - (tan . x)) - (cot . x)),K39((exp_R . x))) is set
sin * sec is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin * sec) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin * sec) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom sec is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sec . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * sec) `| Z) . x is V11() V12() ext-real Element of REAL
sec . x is V11() V12() ext-real Element of REAL
cos . (sec . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . (sec . x)) * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(((cos . (sec . x)) * (sin . x)),K39(((cos . x) ^2))) is set
diff ((sin * sec),x) is V11() V12() ext-real Element of REAL
diff (sin,(sec . x)) is V11() V12() ext-real Element of REAL
diff (sec,x) is V11() V12() ext-real Element of REAL
(diff (sin,(sec . x))) * (diff (sec,x)) is V11() V12() ext-real Element of REAL
cos (sec . x) is V11() V12() ext-real Element of REAL
(cos (sec . x)) * (diff (sec,x)) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is set
(cos (sec . x)) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * sec) `| Z) . x is V11() V12() ext-real Element of REAL
sec . x is V11() V12() ext-real Element of REAL
cos . (sec . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(cos . (sec . x)) * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
((cos . (sec . x)) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(((cos . (sec . x)) * (sin . x)),K39(((cos . x) ^2))) is set
cos * sec is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos * sec) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos * sec) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom sec is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
sec . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * sec) `| Z) . x is V11() V12() ext-real Element of REAL
sec . x is V11() V12() ext-real Element of REAL
sin . (sec . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . (sec . x)) * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(((sin . (sec . x)) * (sin . x)),K39(((cos . x) ^2))) is set
- (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
diff ((cos * sec),x) is V11() V12() ext-real Element of REAL
diff (cos,(sec . x)) is V11() V12() ext-real Element of REAL
diff (sec,x) is V11() V12() ext-real Element of REAL
(diff (cos,(sec . x))) * (diff (sec,x)) is V11() V12() ext-real Element of REAL
sin (sec . x) is V11() V12() ext-real Element of REAL
- (sin (sec . x)) is V11() V12() ext-real Element of REAL
(- (sin (sec . x))) * (diff (sec,x)) is V11() V12() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K37((sin . x),K39(((cos . x) ^2))) is set
(- (sin (sec . x))) * ((sin . x) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * sec) `| Z) . x is V11() V12() ext-real Element of REAL
sec . x is V11() V12() ext-real Element of REAL
sin . (sec . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . (sec . x)) * (sin . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . x) ^2 is V11() V12() ext-real Element of REAL
K37((cos . x),(cos . x)) is set
((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2) is V11() V12() ext-real Element of REAL
K39(((cos . x) ^2)) is V11() set
K37(((sin . (sec . x)) * (sin . x)),K39(((cos . x) ^2))) is set
- (((sin . (sec . x)) * (sin . x)) / ((cos . x) ^2)) is V11() V12() ext-real Element of REAL
sin * cosec is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (sin * cosec) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(sin * cosec) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom cosec is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cosec . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * cosec) `| Z) . x is V11() V12() ext-real Element of REAL
cosec . x is V11() V12() ext-real Element of REAL
cos . (cosec . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . (cosec . x)) * (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(((cos . (cosec . x)) * (cos . x)),K39(((sin . x) ^2))) is set
- (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
diff ((sin * cosec),x) is V11() V12() ext-real Element of REAL
diff (sin,(cosec . x)) is V11() V12() ext-real Element of REAL
diff (cosec,x) is V11() V12() ext-real Element of REAL
(diff (sin,(cosec . x))) * (diff (cosec,x)) is V11() V12() ext-real Element of REAL
cos (cosec . x) is V11() V12() ext-real Element of REAL
(cos (cosec . x)) * (diff (cosec,x)) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(cos (cosec . x)) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((sin * cosec) `| Z) . x is V11() V12() ext-real Element of REAL
cosec . x is V11() V12() ext-real Element of REAL
cos . (cosec . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(cos . (cosec . x)) * (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(((cos . (cosec . x)) * (cos . x)),K39(((sin . x) ^2))) is set
- (((cos . (cosec . x)) * (cos . x)) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
cos * cosec is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom (cos * cosec) is V62() V63() V64() Element of K6(REAL)
Z is open V62() V63() V64() Element of K6(REAL)
(cos * cosec) `| Z is V13() V16( REAL ) V17( REAL ) V18() V52() V53() V54() Element of K6(K7(REAL,REAL))
dom cosec is V62() V63() V64() Element of K6(REAL)
x is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
cosec . x is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * cosec) `| Z) . x is V11() V12() ext-real Element of REAL
cosec . x is V11() V12() ext-real Element of REAL
sin . (cosec . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(sin . (cosec . x)) * (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(((sin . (cosec . x)) * (cos . x)),K39(((sin . x) ^2))) is set
diff ((cos * cosec),x) is V11() V12() ext-real Element of REAL
diff (cos,(cosec . x)) is V11() V12() ext-real Element of REAL
diff (cosec,x) is V11() V12() ext-real Element of REAL
(diff (cos,(cosec . x))) * (diff (cosec,x)) is V11() V12() ext-real Element of REAL
sin (cosec . x) is V11() V12() ext-real Element of REAL
- (sin (cosec . x)) is V11() V12() ext-real Element of REAL
(- (sin (cosec . x))) * (diff (cosec,x)) is V11() V12() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K37((cos . x),K39(((sin . x) ^2))) is set
- ((cos . x) / ((sin . x) ^2)) is V11() V12() ext-real Element of REAL
(- (sin (cosec . x))) * (- ((cos . x) / ((sin . x) ^2))) is V11() V12() ext-real Element of REAL
x is V11() V12() ext-real Element of REAL
((cos * cosec) `| Z) . x is V11() V12() ext-real Element of REAL
cosec . x is V11() V12() ext-real Element of REAL
sin . (cosec . x) is V11() V12() ext-real Element of REAL
cos . x is V11() V12() ext-real Element of REAL
(sin . (cosec . x)) * (cos . x) is V11() V12() ext-real Element of REAL
sin . x is V11() V12() ext-real Element of REAL
(sin . x) ^2 is V11() V12() ext-real Element of REAL
K37((sin . x),(sin . x)) is set
((sin . (cosec . x)) * (cos . x)) / ((sin . x) ^2) is V11() V12() ext-real Element of REAL
K39(((sin . x) ^2)) is V11() set
K37(((sin . (cosec . x)) * (cos . x)),K39(((sin . x) ^2))) is set