:: INTEGRA8 semantic presentation

REAL is non empty V34() V49() V50() V51() V55() V88() V89() V91() set
NAT is V49() V50() V51() V52() V53() V54() V55() V88() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V34() V49() V55() set
RAT is non empty V34() V49() V50() V51() V52() V55() set
INT is non empty V34() V49() V50() V51() V52() V53() V55() set
K20(COMPLEX,COMPLEX) is complex-valued set
K19(K20(COMPLEX,COMPLEX)) is set
K20(K20(COMPLEX,COMPLEX),COMPLEX) is complex-valued set
K19(K20(K20(COMPLEX,COMPLEX),COMPLEX)) is set
K20(REAL,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(REAL,REAL)) is set
K20(K20(REAL,REAL),REAL) is complex-valued ext-real-valued real-valued set
K19(K20(K20(REAL,REAL),REAL)) is set
K20(RAT,RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(RAT,RAT)) is set
K20(K20(RAT,RAT),RAT) is RAT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(RAT,RAT),RAT)) is set
K20(INT,INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(INT,INT)) is set
K20(K20(INT,INT),INT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued set
K19(K20(K20(INT,INT),INT)) is set
K20(NAT,NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K20(K20(NAT,NAT),NAT) is RAT -valued INT -valued complex-valued ext-real-valued real-valued natural-valued set
K19(K20(K20(NAT,NAT),NAT)) is set
NAT is V49() V50() V51() V52() V53() V54() V55() V88() set
K19(NAT) is set
K19(NAT) is set
ExtREAL is non empty V50() V91() set
K20(NAT,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is complex-valued set
K19(K20(NAT,COMPLEX)) is set
{} is empty V49() V50() V51() V52() V53() V54() V55() V88() V91() set
1 is non empty V21() V28() V29() V30() V31() ext-real positive non negative V49() V50() V51() V52() V53() V54() V86() V88() Element of NAT
{{},1} is non empty set
K20(COMPLEX,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(COMPLEX,REAL)) is set
0 is empty V21() V28() V29() V30() V31() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of NAT
sin is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
K488(REAL,sin) is V49() V50() V51() Element of K19(REAL)
cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
K488(REAL,cos) is V49() V50() V51() Element of K19(REAL)
exp_R is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
K488(REAL,exp_R) is V49() V50() V51() Element of K19(REAL)
exp_R 0 is V21() V29() ext-real Element of REAL
exp_R . 0 is V21() V29() ext-real Element of REAL
PI is V21() V29() ext-real set
tan is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
sin / cos is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
4 is non empty V21() V28() V29() V30() V31() ext-real positive non negative V49() V50() V51() V52() V53() V54() V86() V88() Element of NAT
].0,4.[ is V49() V50() V51() V86() V87() V91() open Element of K19(REAL)
PI is V21() V29() ext-real Element of REAL
2 is non empty V21() V28() V29() V30() V31() ext-real positive non negative V49() V50() V51() V52() V53() V54() V86() V88() Element of NAT
PI / 2 is V21() V29() ext-real Element of REAL
cos . (PI / 2) is V21() V29() ext-real Element of REAL
sin . (PI / 2) is V21() V29() ext-real Element of REAL
cos . PI is V21() V29() ext-real Element of REAL
- 1 is V21() V29() V30() ext-real non positive Element of REAL
sin . PI is V21() V29() ext-real Element of REAL
PI + (PI / 2) is V21() V29() ext-real Element of REAL
cos . (PI + (PI / 2)) is V21() V29() ext-real Element of REAL
sin . (PI + (PI / 2)) is V21() V29() ext-real Element of REAL
2 * PI is V21() V29() ext-real Element of REAL
cos . (2 * PI) is V21() V29() ext-real Element of REAL
sin . (2 * PI) is V21() V29() ext-real Element of REAL
cos (PI / 2) is V21() V29() ext-real Element of REAL
sin (PI / 2) is V21() V29() ext-real Element of REAL
cos PI is V21() V29() ext-real Element of REAL
sin PI is V21() V29() ext-real Element of REAL
cos (PI + (PI / 2)) is V21() V29() ext-real Element of REAL
sin (PI + (PI / 2)) is V21() V29() ext-real Element of REAL
cos (2 * PI) is V21() V29() ext-real Element of REAL
sin (2 * PI) is V21() V29() ext-real Element of REAL
sinh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
cosh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
sinh . 0 is V21() V29() ext-real Element of REAL
K488(REAL,sinh) is V49() V50() V51() Element of K19(REAL)
K488(REAL,cosh) is V49() V50() V51() Element of K19(REAL)
tanh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K488(REAL,tanh) is V49() V50() V51() Element of K19(REAL)
number_e is V21() V29() ext-real set
exp_R 1 is V21() V29() ext-real Element of REAL
exp_R . 1 is V21() V29() ext-real Element of REAL
number_e is V21() V29() ext-real Element of REAL
sqrt 1 is V21() V29() ext-real Element of REAL
sqrt 4 is V21() V29() ext-real Element of REAL
exp_R (#) sin is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
K488(REAL,(exp_R (#) sin)) is V49() V50() V51() Element of K19(REAL)
exp_R (#) cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
K488(REAL,(exp_R (#) cos)) is V49() V50() V51() Element of K19(REAL)
- (PI / 2) is V21() V29() ext-real Element of REAL
arcsin is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
].(- 1),1.[ is V49() V50() V51() V86() V87() V91() open Element of K19(REAL)
arccos is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K488(REAL,tan) is V49() V50() V51() Element of K19(REAL)
cot is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
cos / sin is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K488(REAL,cot) is V49() V50() V51() Element of K19(REAL)
PI / 4 is V21() V29() ext-real Element of REAL
sin (PI / 4) is V21() V29() ext-real Element of REAL
sin . (PI / 4) is V21() V29() ext-real Element of REAL
PI / 1 is V21() V29() ext-real Element of REAL
(2 * PI) * 0 is V21() V29() ext-real Element of REAL
PI + ((2 * PI) * 0) is V21() V29() ext-real Element of REAL
0 / 4 is empty V21() V29() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
- (PI / 4) is V21() V29() ext-real Element of REAL
sin (- (PI / 4)) is V21() V29() ext-real Element of REAL
sin . (- (PI / 4)) is V21() V29() ext-real Element of REAL
0 / 4 is empty V21() V29() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
0 * (- 1) is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
(PI / 4) * (- 1) is V21() V29() ext-real Element of REAL
PI / 1 is V21() V29() ext-real Element of REAL
PI * (- 1) is V21() V29() ext-real Element of REAL
(2 * PI) * (- 1) is V21() V29() ext-real Element of REAL
PI + ((2 * PI) * (- 1)) is V21() V29() ext-real Element of REAL
(2 * PI) + ((2 * PI) * (- 1)) is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
sin A is V21() V29() ext-real Element of REAL
sin . A is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
sin A is V21() V29() ext-real Element of REAL
sin . A is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) * PI is V21() V29() ext-real Element of REAL
A + ((2 * x) * PI) is V21() V29() ext-real Element of REAL
sin (A + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
sin . (A + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
sin . A is V21() V29() ext-real Element of REAL
(2 * PI) * x is V21() V29() ext-real Element of REAL
((2 * PI) * x) + A is V21() V29() ext-real Element of REAL
sin . (((2 * PI) * x) + A) is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
sin A is V21() V29() ext-real Element of REAL
sin . A is V21() V29() ext-real Element of REAL
- (sin A) is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * x) + 1) * PI is V21() V29() ext-real Element of REAL
A + (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
sin (A + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (A + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * n) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * n) + 1) * PI is V21() V29() ext-real Element of REAL
A + (((2 * n) + 1) * PI) is V21() V29() ext-real Element of REAL
sin (A + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (A + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
n + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * (n + 1) is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * (n + 1)) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * (n + 1)) + 1) * PI is V21() V29() ext-real Element of REAL
A + (((2 * (n + 1)) + 1) * PI) is V21() V29() ext-real Element of REAL
sin (A + (((2 * (n + 1)) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (A + (((2 * (n + 1)) + 1) * PI)) is V21() V29() ext-real Element of REAL
(A + (((2 * n) + 1) * PI)) + (2 * PI) is V21() V29() ext-real Element of REAL
sin ((A + (((2 * n) + 1) * PI)) + (2 * PI)) is V21() V29() ext-real Element of REAL
sin . ((A + (((2 * n) + 1) * PI)) + (2 * PI)) is V21() V29() ext-real Element of REAL
(sin (A + (((2 * n) + 1) * PI))) * (cos (2 * PI)) is V21() V29() ext-real Element of REAL
cos (A + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (A + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
(cos (A + (((2 * n) + 1) * PI))) * (sin (2 * PI)) is V21() V29() ext-real Element of REAL
((sin (A + (((2 * n) + 1) * PI))) * (cos (2 * PI))) + ((cos (A + (((2 * n) + 1) * PI))) * (sin (2 * PI))) is V21() V29() ext-real Element of REAL
2 * 0 is empty V21() V28() V29() V30() V31() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of NAT
(2 * 0) + 1 is non empty V21() V28() V29() V30() V31() ext-real positive non negative V49() V50() V51() V52() V53() V54() V86() V88() Element of NAT
((2 * 0) + 1) * PI is V21() V29() ext-real Element of REAL
A + (((2 * 0) + 1) * PI) is V21() V29() ext-real Element of REAL
sin (A + (((2 * 0) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (A + (((2 * 0) + 1) * PI)) is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
cos A is V21() V29() ext-real Element of REAL
cos . A is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) * PI is V21() V29() ext-real Element of REAL
A + ((2 * x) * PI) is V21() V29() ext-real Element of REAL
cos (A + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
cos . (A + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
cos . A is V21() V29() ext-real Element of REAL
(2 * PI) * x is V21() V29() ext-real Element of REAL
A + ((2 * PI) * x) is V21() V29() ext-real Element of REAL
cos . (A + ((2 * PI) * x)) is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
cos A is V21() V29() ext-real Element of REAL
cos . A is V21() V29() ext-real Element of REAL
- (cos A) is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * x) + 1) * PI is V21() V29() ext-real Element of REAL
A + (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
cos (A + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (A + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * n) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * n) + 1) * PI is V21() V29() ext-real Element of REAL
A + (((2 * n) + 1) * PI) is V21() V29() ext-real Element of REAL
cos (A + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (A + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
n + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * (n + 1) is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * (n + 1)) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * (n + 1)) + 1) * PI is V21() V29() ext-real Element of REAL
A + (((2 * (n + 1)) + 1) * PI) is V21() V29() ext-real Element of REAL
cos (A + (((2 * (n + 1)) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (A + (((2 * (n + 1)) + 1) * PI)) is V21() V29() ext-real Element of REAL
(A + (((2 * n) + 1) * PI)) + (2 * PI) is V21() V29() ext-real Element of REAL
cos ((A + (((2 * n) + 1) * PI)) + (2 * PI)) is V21() V29() ext-real Element of REAL
cos . ((A + (((2 * n) + 1) * PI)) + (2 * PI)) is V21() V29() ext-real Element of REAL
(cos (A + (((2 * n) + 1) * PI))) * (cos (2 * PI)) is V21() V29() ext-real Element of REAL
sin (A + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (A + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
(sin (A + (((2 * n) + 1) * PI))) * (sin (2 * PI)) is V21() V29() ext-real Element of REAL
((cos (A + (((2 * n) + 1) * PI))) * (cos (2 * PI))) - ((sin (A + (((2 * n) + 1) * PI))) * (sin (2 * PI))) is V21() V29() ext-real Element of REAL
2 * 0 is empty V21() V28() V29() V30() V31() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of NAT
(2 * 0) + 1 is non empty V21() V28() V29() V30() V31() ext-real positive non negative V49() V50() V51() V52() V53() V54() V86() V88() Element of NAT
((2 * 0) + 1) * PI is V21() V29() ext-real Element of REAL
A + (((2 * 0) + 1) * PI) is V21() V29() ext-real Element of REAL
cos (A + (((2 * 0) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (A + (((2 * 0) + 1) * PI)) is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
A / 2 is V21() V29() ext-real Element of REAL
sin (A / 2) is V21() V29() ext-real Element of REAL
sin . (A / 2) is V21() V29() ext-real Element of REAL
cos A is V21() V29() ext-real Element of REAL
cos . A is V21() V29() ext-real Element of REAL
1 - (cos A) is V21() V29() ext-real Element of REAL
(1 - (cos A)) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 - (cos A)) / 2) is V21() V29() ext-real Element of REAL
2 * (A / 2) is V21() V29() ext-real Element of REAL
cos (2 * (A / 2)) is V21() V29() ext-real Element of REAL
cos . (2 * (A / 2)) is V21() V29() ext-real Element of REAL
1 - (cos (2 * (A / 2))) is V21() V29() ext-real Element of REAL
(1 - (cos (2 * (A / 2)))) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 - (cos (2 * (A / 2)))) / 2) is V21() V29() ext-real Element of REAL
(sin (A / 2)) ^2 is V21() V29() ext-real Element of REAL
K86((sin (A / 2)),(sin (A / 2))) is V21() V29() ext-real set
2 * ((sin (A / 2)) ^2) is V21() V29() ext-real Element of REAL
1 - (2 * ((sin (A / 2)) ^2)) is V21() V29() ext-real Element of REAL
1 - (1 - (2 * ((sin (A / 2)) ^2))) is V21() V29() ext-real Element of REAL
(1 - (1 - (2 * ((sin (A / 2)) ^2)))) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 - (1 - (2 * ((sin (A / 2)) ^2)))) / 2) is V21() V29() ext-real Element of REAL
abs (sin (A / 2)) is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
A / 2 is V21() V29() ext-real Element of REAL
sin (A / 2) is V21() V29() ext-real Element of REAL
sin . (A / 2) is V21() V29() ext-real Element of REAL
cos A is V21() V29() ext-real Element of REAL
cos . A is V21() V29() ext-real Element of REAL
1 - (cos A) is V21() V29() ext-real Element of REAL
(1 - (cos A)) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 - (cos A)) / 2) is V21() V29() ext-real Element of REAL
- (sqrt ((1 - (cos A)) / 2)) is V21() V29() ext-real Element of REAL
2 * (A / 2) is V21() V29() ext-real Element of REAL
cos (2 * (A / 2)) is V21() V29() ext-real Element of REAL
cos . (2 * (A / 2)) is V21() V29() ext-real Element of REAL
1 - (cos (2 * (A / 2))) is V21() V29() ext-real Element of REAL
(1 - (cos (2 * (A / 2)))) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 - (cos (2 * (A / 2)))) / 2) is V21() V29() ext-real Element of REAL
(sin (A / 2)) ^2 is V21() V29() ext-real Element of REAL
K86((sin (A / 2)),(sin (A / 2))) is V21() V29() ext-real set
2 * ((sin (A / 2)) ^2) is V21() V29() ext-real Element of REAL
1 - (2 * ((sin (A / 2)) ^2)) is V21() V29() ext-real Element of REAL
1 - (1 - (2 * ((sin (A / 2)) ^2))) is V21() V29() ext-real Element of REAL
(1 - (1 - (2 * ((sin (A / 2)) ^2)))) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 - (1 - (2 * ((sin (A / 2)) ^2)))) / 2) is V21() V29() ext-real Element of REAL
abs (sin (A / 2)) is V21() V29() ext-real Element of REAL
- (sin (A / 2)) is V21() V29() ext-real Element of REAL
sqrt 2 is V21() V29() ext-real Element of REAL
(sqrt 2) / 2 is V21() V29() ext-real Element of REAL
(PI / 2) / 2 is V21() V29() ext-real Element of REAL
sin ((PI / 2) / 2) is V21() V29() ext-real Element of REAL
sin . ((PI / 2) / 2) is V21() V29() ext-real Element of REAL
1 - (cos (PI / 2)) is V21() V29() ext-real Element of REAL
(1 - (cos (PI / 2))) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 - (cos (PI / 2))) / 2) is V21() V29() ext-real Element of REAL
1 / (sqrt 2) is V21() V29() ext-real Element of REAL
(sqrt 2) * 1 is V21() V29() ext-real Element of REAL
(sqrt 2) * (sqrt 2) is V21() V29() ext-real Element of REAL
((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2)) is V21() V29() ext-real Element of REAL
(sqrt 2) ^2 is V21() V29() ext-real Element of REAL
K86((sqrt 2),(sqrt 2)) is V21() V29() ext-real set
((sqrt 2) * 1) / ((sqrt 2) ^2) is V21() V29() ext-real Element of REAL
- ((sqrt 2) / 2) is V21() V29() ext-real Element of REAL
cos (- (PI / 2)) is V21() V29() ext-real Element of REAL
cos . (- (PI / 2)) is V21() V29() ext-real Element of REAL
(PI / 2) - (- (PI / 2)) is V21() V29() ext-real Element of REAL
sin ((PI / 2) - (- (PI / 2))) is V21() V29() ext-real Element of REAL
sin . ((PI / 2) - (- (PI / 2))) is V21() V29() ext-real Element of REAL
(- (PI / 2)) / 2 is V21() V29() ext-real Element of REAL
sin ((- (PI / 2)) / 2) is V21() V29() ext-real Element of REAL
sin . ((- (PI / 2)) / 2) is V21() V29() ext-real Element of REAL
1 - (cos (- (PI / 2))) is V21() V29() ext-real Element of REAL
(1 - (cos (- (PI / 2)))) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 - (cos (- (PI / 2)))) / 2) is V21() V29() ext-real Element of REAL
- (sqrt ((1 - (cos (- (PI / 2)))) / 2)) is V21() V29() ext-real Element of REAL
1 / (sqrt 2) is V21() V29() ext-real Element of REAL
- (1 / (sqrt 2)) is V21() V29() ext-real Element of REAL
(sqrt 2) * 1 is V21() V29() ext-real Element of REAL
(sqrt 2) * (sqrt 2) is V21() V29() ext-real Element of REAL
((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2)) is V21() V29() ext-real Element of REAL
- (((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2))) is V21() V29() ext-real Element of REAL
(sqrt 2) ^2 is V21() V29() ext-real Element of REAL
K86((sqrt 2),(sqrt 2)) is V21() V29() ext-real set
((sqrt 2) * 1) / ((sqrt 2) ^2) is V21() V29() ext-real Element of REAL
- (((sqrt 2) * 1) / ((sqrt 2) ^2)) is V21() V29() ext-real Element of REAL
[.(- ((sqrt 2) / 2)),((sqrt 2) / 2).] is V49() V50() V51() V91() closed Element of K19(REAL)
2 / 2 is V21() V29() ext-real non negative Element of REAL
((sqrt 2) / 2) * (- 1) is V21() V29() ext-real Element of REAL
1 * (- 1) is V21() V29() V30() ext-real non positive Element of REAL
arcsin ((sqrt 2) / 2) is V21() V29() ext-real Element of REAL
arcsin (- ((sqrt 2) / 2)) is V21() V29() ext-real Element of REAL
(PI / 4) * (- 1) is V21() V29() ext-real Element of REAL
(PI / 2) * (- 1) is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
A / 2 is V21() V29() ext-real Element of REAL
cos (A / 2) is V21() V29() ext-real Element of REAL
cos . (A / 2) is V21() V29() ext-real Element of REAL
cos A is V21() V29() ext-real Element of REAL
cos . A is V21() V29() ext-real Element of REAL
1 + (cos A) is V21() V29() ext-real Element of REAL
(1 + (cos A)) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 + (cos A)) / 2) is V21() V29() ext-real Element of REAL
2 * (A / 2) is V21() V29() ext-real Element of REAL
cos (2 * (A / 2)) is V21() V29() ext-real Element of REAL
cos . (2 * (A / 2)) is V21() V29() ext-real Element of REAL
1 + (cos (2 * (A / 2))) is V21() V29() ext-real Element of REAL
(1 + (cos (2 * (A / 2)))) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 + (cos (2 * (A / 2)))) / 2) is V21() V29() ext-real Element of REAL
(cos (A / 2)) ^2 is V21() V29() ext-real Element of REAL
K86((cos (A / 2)),(cos (A / 2))) is V21() V29() ext-real set
2 * ((cos (A / 2)) ^2) is V21() V29() ext-real Element of REAL
(2 * ((cos (A / 2)) ^2)) - 1 is V21() V29() ext-real Element of REAL
1 + ((2 * ((cos (A / 2)) ^2)) - 1) is V21() V29() ext-real Element of REAL
(1 + ((2 * ((cos (A / 2)) ^2)) - 1)) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 + ((2 * ((cos (A / 2)) ^2)) - 1)) / 2) is V21() V29() ext-real Element of REAL
abs (cos (A / 2)) is V21() V29() ext-real Element of REAL
cos (PI / 4) is V21() V29() ext-real Element of REAL
cos . (PI / 4) is V21() V29() ext-real Element of REAL
0 / 2 is empty V21() V29() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
0 * (- 1) is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
(PI / 2) * (- 1) is V21() V29() ext-real Element of REAL
(2 * PI) * 0 is V21() V29() ext-real Element of REAL
(- (PI / 2)) + ((2 * PI) * 0) is V21() V29() ext-real Element of REAL
(PI / 2) + ((2 * PI) * 0) is V21() V29() ext-real Element of REAL
(PI / 2) / 2 is V21() V29() ext-real Element of REAL
cos ((PI / 2) / 2) is V21() V29() ext-real Element of REAL
cos . ((PI / 2) / 2) is V21() V29() ext-real Element of REAL
1 + (cos (PI / 2)) is V21() V29() ext-real Element of REAL
(1 + (cos (PI / 2))) / 2 is V21() V29() ext-real Element of REAL
sqrt ((1 + (cos (PI / 2))) / 2) is V21() V29() ext-real Element of REAL
1 / (sqrt 2) is V21() V29() ext-real Element of REAL
(sqrt 2) * 1 is V21() V29() ext-real Element of REAL
(sqrt 2) * (sqrt 2) is V21() V29() ext-real Element of REAL
((sqrt 2) * 1) / ((sqrt 2) * (sqrt 2)) is V21() V29() ext-real Element of REAL
(sqrt 2) ^2 is V21() V29() ext-real Element of REAL
K86((sqrt 2),(sqrt 2)) is V21() V29() ext-real set
((sqrt 2) * 1) / ((sqrt 2) ^2) is V21() V29() ext-real Element of REAL
3 is non empty V21() V28() V29() V30() V31() ext-real positive non negative V49() V50() V51() V52() V53() V54() V86() V88() Element of NAT
3 * PI is V21() V29() ext-real Element of REAL
(3 * PI) / 4 is V21() V29() ext-real Element of REAL
cos ((3 * PI) / 4) is V21() V29() ext-real Element of REAL
cos . ((3 * PI) / 4) is V21() V29() ext-real Element of REAL
(PI / 2) + (PI / 4) is V21() V29() ext-real Element of REAL
cos ((PI / 2) + (PI / 4)) is V21() V29() ext-real Element of REAL
cos . ((PI / 2) + (PI / 4)) is V21() V29() ext-real Element of REAL
arccos ((sqrt 2) / 2) is V21() V29() ext-real Element of REAL
PI / 1 is V21() V29() ext-real Element of REAL
arccos (- ((sqrt 2) / 2)) is V21() V29() ext-real Element of REAL
1 * PI is V21() V29() ext-real Element of REAL
3 / 4 is V21() V29() ext-real non negative Element of REAL
(3 / 4) * PI is V21() V29() ext-real Element of REAL
sinh . 1 is V21() V29() ext-real Element of REAL
number_e ^2 is V21() V29() ext-real Element of REAL
K86(number_e,number_e) is V21() V29() ext-real set
(number_e ^2) - 1 is V21() V29() ext-real Element of REAL
2 * number_e is V21() V29() ext-real Element of REAL
((number_e ^2) - 1) / (2 * number_e) is V21() V29() ext-real Element of REAL
exp_R (- 1) is V21() V29() ext-real Element of REAL
exp_R . (- 1) is V21() V29() ext-real Element of REAL
number_e - (exp_R (- 1)) is V21() V29() ext-real Element of REAL
(number_e - (exp_R (- 1))) / 2 is V21() V29() ext-real Element of REAL
number_e / 1 is V21() V29() ext-real Element of REAL
1 / number_e is V21() V29() ext-real Element of REAL
(number_e / 1) - (1 / number_e) is V21() V29() ext-real Element of REAL
((number_e / 1) - (1 / number_e)) / 2 is V21() V29() ext-real Element of REAL
number_e * number_e is V21() V29() ext-real Element of REAL
1 * number_e is V21() V29() ext-real Element of REAL
(number_e * number_e) / (1 * number_e) is V21() V29() ext-real Element of REAL
((number_e * number_e) / (1 * number_e)) - (1 / number_e) is V21() V29() ext-real Element of REAL
(((number_e * number_e) / (1 * number_e)) - (1 / number_e)) / 2 is V21() V29() ext-real Element of REAL
(number_e ^2) / number_e is V21() V29() ext-real Element of REAL
((number_e ^2) / number_e) - (1 / number_e) is V21() V29() ext-real Element of REAL
(((number_e ^2) / number_e) - (1 / number_e)) / 2 is V21() V29() ext-real Element of REAL
((number_e ^2) - 1) / number_e is V21() V29() ext-real Element of REAL
(((number_e ^2) - 1) / number_e) / 2 is V21() V29() ext-real Element of REAL
cosh . 0 is V21() V29() ext-real Element of REAL
exp_R . 0 is V21() V29() ext-real Element of REAL
- 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
exp_R . (- 0) is V21() V29() ext-real Element of REAL
(exp_R . 0) + (exp_R . (- 0)) is V21() V29() ext-real Element of REAL
((exp_R . 0) + (exp_R . (- 0))) / 2 is V21() V29() ext-real Element of REAL
cosh . 1 is V21() V29() ext-real Element of REAL
(number_e ^2) + 1 is V21() V29() ext-real Element of REAL
((number_e ^2) + 1) / (2 * number_e) is V21() V29() ext-real Element of REAL
exp_R (- 1) is V21() V29() ext-real Element of REAL
exp_R . (- 1) is V21() V29() ext-real Element of REAL
number_e + (exp_R (- 1)) is V21() V29() ext-real Element of REAL
(number_e + (exp_R (- 1))) / 2 is V21() V29() ext-real Element of REAL
number_e / 1 is V21() V29() ext-real Element of REAL
1 / number_e is V21() V29() ext-real Element of REAL
(number_e / 1) + (1 / number_e) is V21() V29() ext-real Element of REAL
((number_e / 1) + (1 / number_e)) / 2 is V21() V29() ext-real Element of REAL
number_e * number_e is V21() V29() ext-real Element of REAL
1 * number_e is V21() V29() ext-real Element of REAL
(number_e * number_e) / (1 * number_e) is V21() V29() ext-real Element of REAL
((number_e * number_e) / (1 * number_e)) + (1 / number_e) is V21() V29() ext-real Element of REAL
(((number_e * number_e) / (1 * number_e)) + (1 / number_e)) / 2 is V21() V29() ext-real Element of REAL
(number_e ^2) / number_e is V21() V29() ext-real Element of REAL
((number_e ^2) / number_e) + (1 / number_e) is V21() V29() ext-real Element of REAL
(((number_e ^2) / number_e) + (1 / number_e)) / 2 is V21() V29() ext-real Element of REAL
((number_e ^2) + 1) / number_e is V21() V29() ext-real Element of REAL
(((number_e ^2) + 1) / number_e) / 2 is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) is V21() V29() V30() ext-real non positive set
K87(1) * A is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) * x is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
(- A) (#) (- x) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A (#) x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A (#) (- x) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(- 1) (#) (A (#) (- x)) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- (- x) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) * (- x) is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
A (#) (- (- x)) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued linear Element of K19(K20(REAL,REAL))
- A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) is V21() V29() V30() ext-real non positive set
K87(1) * A is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
x is V21() V29() ext-real Element of REAL
n is V21() V29() ext-real Element of REAL
(- A) . n is V21() V29() ext-real Element of REAL
A . n is V21() V29() ext-real Element of REAL
- (A . n) is V21() V29() ext-real Element of REAL
x * n is V21() V29() ext-real Element of REAL
- (x * n) is V21() V29() ext-real Element of REAL
- x is V21() V29() ext-real Element of REAL
(- x) * n is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued RestFunc-like Element of K19(K20(REAL,REAL))
- A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) is V21() V29() V30() ext-real non positive set
K87(1) * A is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
dom A is set
x is Relation-like non-empty NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
A /* x is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (A /* x) is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
K87(1) * (A /* x) is Relation-like NAT -defined V6() total complex-valued ext-real-valued real-valued set
(- A) /* x is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
rng x is V49() V50() V51() set
x is Relation-like non-empty NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued 0 -convergent convergent Element of K19(K20(NAT,REAL))
x " is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
A /* x is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(x ") (#) (A /* x) is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(- A) /* x is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
(x ") (#) ((- A) /* x) is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- (A /* x) is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
K87(1) * (A /* x) is Relation-like NAT -defined V6() total complex-valued ext-real-valued real-valued set
(x ") (#) (- (A /* x)) is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
- ((x ") (#) (A /* x)) is Relation-like NAT -defined REAL -valued V6() total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(NAT,REAL))
K87(1) * ((x ") (#) (A /* x)) is Relation-like NAT -defined V6() total complex-valued ext-real-valued real-valued set
lim ((x ") (#) (A /* x)) is V21() V29() ext-real Element of REAL
lim ((x ") (#) ((- A) /* x)) is V21() V29() ext-real Element of REAL
- (lim ((x ") (#) (A /* x))) is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) is V21() V29() V30() ext-real non positive set
K87(1) * A is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
x is V21() V29() ext-real Element of REAL
diff ((- A),x) is V21() V29() ext-real Element of REAL
diff (A,x) is V21() V29() ext-real Element of REAL
- (diff (A,x)) is V21() V29() ext-real Element of REAL
dom A is set
A . x is V21() V29() ext-real Element of REAL
n is V49() V50() V51() open Neighbourhood of x
Z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued linear Element of K19(K20(REAL,REAL))
R1 is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued RestFunc-like Element of K19(K20(REAL,REAL))
Z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued linear Element of K19(K20(REAL,REAL))
R1 is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued RestFunc-like Element of K19(K20(REAL,REAL))
- R1 is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) * R1 is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
- Z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) * Z is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
N is V49() V50() V51() open Neighbourhood of x
x is V21() V29() ext-real Element of REAL
(- A) . x is V21() V29() ext-real Element of REAL
(- A) . x is V21() V29() ext-real Element of REAL
((- A) . x) - ((- A) . x) is V21() V29() ext-real Element of REAL
A . x is V21() V29() ext-real Element of REAL
- (A . x) is V21() V29() ext-real Element of REAL
(- (A . x)) - ((- A) . x) is V21() V29() ext-real Element of REAL
- (A . x) is V21() V29() ext-real Element of REAL
(- (A . x)) - (- (A . x)) is V21() V29() ext-real Element of REAL
(A . x) - (A . x) is V21() V29() ext-real Element of REAL
- ((A . x) - (A . x)) is V21() V29() ext-real Element of REAL
x - x is V21() V29() ext-real Element of REAL
Z . (x - x) is V21() V29() ext-real Element of REAL
R1 . (x - x) is V21() V29() ext-real Element of REAL
(Z . (x - x)) + (R1 . (x - x)) is V21() V29() ext-real Element of REAL
- ((Z . (x - x)) + (R1 . (x - x))) is V21() V29() ext-real Element of REAL
- (Z . (x - x)) is V21() V29() ext-real Element of REAL
- (R1 . (x - x)) is V21() V29() ext-real Element of REAL
(- (Z . (x - x))) + (- (R1 . (x - x))) is V21() V29() ext-real Element of REAL
L is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued linear Element of K19(K20(REAL,REAL))
L . (x - x) is V21() V29() ext-real Element of REAL
(L . (x - x)) + (- (R1 . (x - x))) is V21() V29() ext-real Element of REAL
R is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued RestFunc-like Element of K19(K20(REAL,REAL))
R . (x - x) is V21() V29() ext-real Element of REAL
(L . (x - x)) + (R . (x - x)) is V21() V29() ext-real Element of REAL
dom (- A) is set
L . 1 is V21() V29() ext-real Element of REAL
Z . 1 is V21() V29() ext-real Element of REAL
- (Z . 1) is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) is V21() V29() V30() ext-real non positive set
K87(1) * A is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
dom (- A) is set
x is V49() V50() V51() open Element of K19(REAL)
(- A) `| x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
n is V21() V29() ext-real Element of REAL
n is V21() V29() ext-real Element of REAL
((- A) `| x) . n is V21() V29() ext-real Element of REAL
diff ((- A),n) is V21() V29() ext-real Element of REAL
diff (A,n) is V21() V29() ext-real Element of REAL
- (diff (A,n)) is V21() V29() ext-real Element of REAL
n is V21() V29() ext-real Element of REAL
((- A) `| x) . n is V21() V29() ext-real Element of REAL
diff (A,n) is V21() V29() ext-real Element of REAL
- (diff (A,n)) is V21() V29() ext-real Element of REAL
- sin is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) is V21() V29() V30() ext-real non positive set
K87(1) * sin is Relation-like REAL -defined V6() total complex-valued ext-real-valued real-valued set
dom (- sin) is set
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
- cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) * cos is Relation-like REAL -defined V6() total complex-valued ext-real-valued real-valued set
A is V21() V29() ext-real Element of REAL
diff ((- cos),A) is V21() V29() ext-real Element of REAL
sin . A is V21() V29() ext-real Element of REAL
diff (cos,A) is V21() V29() ext-real Element of REAL
- (diff (cos,A)) is V21() V29() ext-real Element of REAL
- (sin . A) is V21() V29() ext-real Element of REAL
- (- (sin . A)) is V21() V29() ext-real Element of REAL
dom (- cos) is set
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
A is V21() V29() ext-real Element of REAL
diff ((- cos),A) is V21() V29() ext-real Element of REAL
sin . A is V21() V29() ext-real Element of REAL
sin `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is V21() V29() ext-real Element of REAL
diff (sin,A) is V21() V29() ext-real Element of REAL
cos . A is V21() V29() ext-real Element of REAL
cos `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (cos `| REAL) is set
A is V21() V29() ext-real Element of REAL
(cos `| REAL) . A is V21() V29() ext-real Element of REAL
(- sin) . A is V21() V29() ext-real Element of REAL
diff (cos,A) is V21() V29() ext-real Element of REAL
sin . A is V21() V29() ext-real Element of REAL
- (sin . A) is V21() V29() ext-real Element of REAL
dom (- sin) is set
(- cos) `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
sinh `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is V21() V29() ext-real Element of REAL
diff (sinh,A) is V21() V29() ext-real Element of REAL
cosh . A is V21() V29() ext-real Element of REAL
cosh `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is V21() V29() ext-real Element of REAL
diff (cosh,A) is V21() V29() ext-real Element of REAL
sinh . A is V21() V29() ext-real Element of REAL
exp_R `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is V21() V29() ext-real Element of REAL
diff (exp_R,A) is V21() V29() ext-real Element of REAL
exp_R . A is V21() V29() ext-real Element of REAL
dom tan is set
A is V49() V50() V51() open Element of K19(REAL)
tan `| A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
(tan `| A) . x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
(cos . x) ^2 is V21() V29() ext-real Element of REAL
K86((cos . x),(cos . x)) is V21() V29() ext-real set
1 / ((cos . x) ^2) is V21() V29() ext-real Element of REAL
diff (tan,x) is V21() V29() ext-real Element of REAL
diff (sin,x) is V21() V29() ext-real Element of REAL
(diff (sin,x)) * (cos . x) is V21() V29() ext-real Element of REAL
diff (cos,x) is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
(diff (cos,x)) * (sin . x) is V21() V29() ext-real Element of REAL
((diff (sin,x)) * (cos . x)) - ((diff (cos,x)) * (sin . x)) is V21() V29() ext-real Element of REAL
(((diff (sin,x)) * (cos . x)) - ((diff (cos,x)) * (sin . x))) / ((cos . x) ^2) is V21() V29() ext-real Element of REAL
(cos . x) * (cos . x) is V21() V29() ext-real Element of REAL
((cos . x) * (cos . x)) - ((diff (cos,x)) * (sin . x)) is V21() V29() ext-real Element of REAL
(((cos . x) * (cos . x)) - ((diff (cos,x)) * (sin . x))) / ((cos . x) ^2) is V21() V29() ext-real Element of REAL
- (sin . x) is V21() V29() ext-real Element of REAL
(- (sin . x)) * (sin . x) is V21() V29() ext-real Element of REAL
((cos . x) * (cos . x)) - ((- (sin . x)) * (sin . x)) is V21() V29() ext-real Element of REAL
(((cos . x) * (cos . x)) - ((- (sin . x)) * (sin . x))) / ((cos . x) ^2) is V21() V29() ext-real Element of REAL
(sin . x) * (sin . x) is V21() V29() ext-real Element of REAL
((cos . x) * (cos . x)) + ((sin . x) * (sin . x)) is V21() V29() ext-real Element of REAL
(((cos . x) * (cos . x)) + ((sin . x) * (sin . x))) / ((cos . x) ^2) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
(tan `| A) . x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
(cos . x) ^2 is V21() V29() ext-real Element of REAL
K86((cos . x),(cos . x)) is V21() V29() ext-real set
1 / ((cos . x) ^2) is V21() V29() ext-real Element of REAL
dom cot is set
A is V49() V50() V51() open Element of K19(REAL)
cot `| A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
(cot `| A) . x is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
(sin . x) ^2 is V21() V29() ext-real Element of REAL
K86((sin . x),(sin . x)) is V21() V29() ext-real set
1 / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
- (1 / ((sin . x) ^2)) is V21() V29() ext-real Element of REAL
diff (cot,x) is V21() V29() ext-real Element of REAL
diff (cos,x) is V21() V29() ext-real Element of REAL
(diff (cos,x)) * (sin . x) is V21() V29() ext-real Element of REAL
diff (sin,x) is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
(diff (sin,x)) * (cos . x) is V21() V29() ext-real Element of REAL
((diff (cos,x)) * (sin . x)) - ((diff (sin,x)) * (cos . x)) is V21() V29() ext-real Element of REAL
(((diff (cos,x)) * (sin . x)) - ((diff (sin,x)) * (cos . x))) / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
- (sin . x) is V21() V29() ext-real Element of REAL
(- (sin . x)) * (sin . x) is V21() V29() ext-real Element of REAL
((- (sin . x)) * (sin . x)) - ((diff (sin,x)) * (cos . x)) is V21() V29() ext-real Element of REAL
(((- (sin . x)) * (sin . x)) - ((diff (sin,x)) * (cos . x))) / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
(sin . x) * (sin . x) is V21() V29() ext-real Element of REAL
- ((sin . x) * (sin . x)) is V21() V29() ext-real Element of REAL
(cos . x) * (cos . x) is V21() V29() ext-real Element of REAL
(- ((sin . x) * (sin . x))) - ((cos . x) * (cos . x)) is V21() V29() ext-real Element of REAL
((- ((sin . x) * (sin . x))) - ((cos . x) * (cos . x))) / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
((sin . x) * (sin . x)) + ((cos . x) * (cos . x)) is V21() V29() ext-real Element of REAL
- (((sin . x) * (sin . x)) + ((cos . x) * (cos . x))) is V21() V29() ext-real Element of REAL
(- (((sin . x) * (sin . x)) + ((cos . x) * (cos . x)))) / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
(cos . x) ^2 is V21() V29() ext-real Element of REAL
K86((cos . x),(cos . x)) is V21() V29() ext-real set
((sin . x) * (sin . x)) + ((cos . x) ^2) is V21() V29() ext-real Element of REAL
- (((sin . x) * (sin . x)) + ((cos . x) ^2)) is V21() V29() ext-real Element of REAL
(- (((sin . x) * (sin . x)) + ((cos . x) ^2))) / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
((sin . x) ^2) + ((cos . x) ^2) is V21() V29() ext-real Element of REAL
- (((sin . x) ^2) + ((cos . x) ^2)) is V21() V29() ext-real Element of REAL
(- (((sin . x) ^2) + ((cos . x) ^2))) / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
((cos . x) ^2) + ((sin . x) ^2) is V21() V29() ext-real Element of REAL
(((cos . x) ^2) + ((sin . x) ^2)) / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
- ((((cos . x) ^2) + ((sin . x) ^2)) / ((sin . x) ^2)) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
(cot `| A) . x is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
(sin . x) ^2 is V21() V29() ext-real Element of REAL
K86((sin . x),(sin . x)) is V21() V29() ext-real set
1 / ((sin . x) ^2) is V21() V29() ext-real Element of REAL
- (1 / ((sin . x) ^2)) is V21() V29() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
REAL --> A is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
rng (REAL --> A) is V49() V50() V51() set
{A} is non empty V49() V50() V51() Element of K19(REAL)
A is V21() V29() ext-real Element of REAL
REAL --> A is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(1) is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
REAL --> 1 is Relation-like REAL -defined REAL -valued RAT -valued INT -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued natural-valued Element of K19(K20(REAL,REAL))
n is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
chi (n,n) is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
K20(n,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(n,REAL)) is set
(1) | n is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ((1) | n) is set
dom (1) is set
(dom (1)) /\ n is V49() V50() V51() Element of K19(REAL)
Z is set
((1) | n) . Z is V21() V29() ext-real Element of REAL
(REAL --> 1) . Z is V21() V28() V29() V30() V31() ext-real Element of REAL
A is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
[.A,x.] is V49() V50() V51() V91() closed Element of K19(REAL)
n is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound n is V21() V29() ext-real Element of REAL
lower_bound n is V21() V29() ext-real Element of REAL
[.(lower_bound n),(upper_bound n).] is V49() V50() V51() V91() closed Element of K19(REAL)
A is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
integral ((1),A,x) is V21() V29() ext-real Element of REAL
x - A is V21() V29() ext-real Element of REAL
[.A,x.] is V49() V50() V51() V91() closed Element of K19(REAL)
['A,x'] is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
n is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound n is V21() V29() ext-real Element of REAL
lower_bound n is V21() V29() ext-real Element of REAL
vol n is V21() V29() ext-real Element of REAL
integral ((1),n) is V21() V29() ext-real Element of REAL
(1) || n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
K20(n,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(n,REAL)) is set
integral ((1) || n) is V21() V29() ext-real Element of REAL
chi (n,n) is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
dom sin is set
dom cos is set
dom (- sin) is set
dom exp_R is set
dom sinh is set
dom cosh is set
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
cos | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cos,A) is V21() V29() ext-real Element of REAL
cos || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cos || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
sin . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sin . (lower_bound A) is V21() V29() ext-real Element of REAL
(sin . (upper_bound A)) - (sin . (lower_bound A)) is V21() V29() ext-real Element of REAL
dom (sin `| REAL) is set
x is V21() V29() ext-real Element of REAL
(sin `| REAL) . x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
diff (sin,x) is V21() V29() ext-real Element of REAL
cos | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
[.0,(PI / 2).] is V49() V50() V51() V91() closed Element of K19(REAL)
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cos,A) is V21() V29() ext-real Element of REAL
cos || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cos || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
1 - (sin . 0) is V21() V29() ext-real Element of REAL
(PI / 2) - 0 is V21() V29() ext-real Element of REAL
cos . ((PI / 2) - 0) is V21() V29() ext-real Element of REAL
1 - (cos . ((PI / 2) - 0)) is V21() V29() ext-real Element of REAL
1 - 0 is non empty V21() V29() V30() ext-real positive non negative Element of REAL
[.0,PI.] is V49() V50() V51() V91() closed Element of K19(REAL)
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cos,A) is V21() V29() ext-real Element of REAL
cos || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cos || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
0 - (sin . 0) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
0 - (sin . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
0 - 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
PI * 3 is V21() V29() ext-real Element of REAL
(PI * 3) / 2 is V21() V29() ext-real Element of REAL
[.0,((PI * 3) / 2).] is V49() V50() V51() V91() closed Element of K19(REAL)
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cos,A) is V21() V29() ext-real Element of REAL
cos || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cos || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
(- 1) - (sin . 0) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(- 1) - (sin . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(- 1) - 0 is V21() V29() V30() ext-real non positive Element of REAL
PI * 2 is V21() V29() ext-real Element of REAL
[.0,(PI * 2).] is V49() V50() V51() V91() closed Element of K19(REAL)
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cos,A) is V21() V29() ext-real Element of REAL
cos || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cos || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
0 - (sin . 0) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
0 - (sin . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
0 - 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cos,A) is V21() V29() ext-real Element of REAL
cos || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cos || A) is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) * PI is V21() V29() ext-real Element of REAL
(2 * x) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * x) + 1) * PI is V21() V29() ext-real Element of REAL
[.((2 * x) * PI),(((2 * x) + 1) * PI).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
0 + (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
sin (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
0 + ((2 * x) * PI) is V21() V29() ext-real Element of REAL
sin (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
(sin (0 + (((2 * x) + 1) * PI))) - (sin (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
sin 0 is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
- (sin 0) is V21() V29() ext-real Element of REAL
(- (sin 0)) - (sin (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
(- (sin 0)) - (sin 0) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
sin (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (sin (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(- (sin (0 + (2 * PI)))) - (sin 0) is V21() V29() ext-real Element of REAL
0 - 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cos,A) is V21() V29() ext-real Element of REAL
cos || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cos || A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
sin x is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
2 * (sin x) is V21() V29() ext-real Element of REAL
- (2 * (sin x)) is V21() V29() ext-real Element of REAL
n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * n) * PI is V21() V29() ext-real Element of REAL
x + ((2 * n) * PI) is V21() V29() ext-real Element of REAL
(2 * n) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * n) + 1) * PI is V21() V29() ext-real Element of REAL
x + (((2 * n) + 1) * PI) is V21() V29() ext-real Element of REAL
[.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sin (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
sin . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
(sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
- (sin x) is V21() V29() ext-real Element of REAL
(- (sin x)) - (sin (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
(- (sin x)) - (sin x) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
(- sin) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((- sin),A) is V21() V29() ext-real Element of REAL
(- sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((- sin) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
cos . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . (lower_bound A) is V21() V29() ext-real Element of REAL
(cos . (upper_bound A)) - (cos . (lower_bound A)) is V21() V29() ext-real Element of REAL
dom (cos `| REAL) is set
x is V21() V29() ext-real Element of REAL
(cos `| REAL) . x is V21() V29() ext-real Element of REAL
(- sin) . x is V21() V29() ext-real Element of REAL
diff (cos,x) is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
- (sin . x) is V21() V29() ext-real Element of REAL
(- sin) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((- sin),A) is V21() V29() ext-real Element of REAL
(- sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((- sin) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
0 - (cos . 0) is V21() V29() ext-real Element of REAL
(PI / 2) - 0 is V21() V29() ext-real Element of REAL
sin . ((PI / 2) - 0) is V21() V29() ext-real Element of REAL
0 - (sin . ((PI / 2) - 0)) is V21() V29() ext-real Element of REAL
0 - 1 is non empty V21() V29() V30() ext-real non positive negative Element of REAL
- 2 is V21() V29() V30() ext-real non positive Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((- sin),A) is V21() V29() ext-real Element of REAL
(- sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((- sin) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
(- 1) - (cos . 0) is V21() V29() ext-real Element of REAL
(PI / 2) - 0 is V21() V29() ext-real Element of REAL
sin . ((PI / 2) - 0) is V21() V29() ext-real Element of REAL
(- 1) - (sin . ((PI / 2) - 0)) is V21() V29() ext-real Element of REAL
(- 1) - 1 is non empty V21() V29() V30() ext-real non positive negative Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((- sin),A) is V21() V29() ext-real Element of REAL
(- sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((- sin) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
0 - (cos . 0) is V21() V29() ext-real Element of REAL
(PI / 2) - 0 is V21() V29() ext-real Element of REAL
sin . ((PI / 2) - 0) is V21() V29() ext-real Element of REAL
0 - (sin . ((PI / 2) - 0)) is V21() V29() ext-real Element of REAL
0 - 1 is non empty V21() V29() V30() ext-real non positive negative Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((- sin),A) is V21() V29() ext-real Element of REAL
(- sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((- sin) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
1 - (cos . 0) is V21() V29() ext-real Element of REAL
(PI / 2) - 0 is V21() V29() ext-real Element of REAL
sin . ((PI / 2) - 0) is V21() V29() ext-real Element of REAL
1 - (sin . ((PI / 2) - 0)) is V21() V29() ext-real Element of REAL
1 - 1 is V21() V29() V30() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((- sin),A) is V21() V29() ext-real Element of REAL
(- sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((- sin) || A) is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) * PI is V21() V29() ext-real Element of REAL
(2 * x) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * x) + 1) * PI is V21() V29() ext-real Element of REAL
[.((2 * x) * PI),(((2 * x) + 1) * PI).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
0 + (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
cos (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
0 + ((2 * x) * PI) is V21() V29() ext-real Element of REAL
cos (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
(cos (0 + (((2 * x) + 1) * PI))) - (cos (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
cos 0 is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos 0) is V21() V29() ext-real Element of REAL
(- (cos 0)) - (cos (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
(- (cos 0)) - (cos 0) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(- (cos (0 + (2 * PI)))) - (cos 0) is V21() V29() ext-real Element of REAL
(- 1) - 1 is non empty V21() V29() V30() ext-real non positive negative Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((- sin),A) is V21() V29() ext-real Element of REAL
(- sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((- sin) || A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
cos x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
2 * (cos x) is V21() V29() ext-real Element of REAL
- (2 * (cos x)) is V21() V29() ext-real Element of REAL
n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * n) * PI is V21() V29() ext-real Element of REAL
x + ((2 * n) * PI) is V21() V29() ext-real Element of REAL
(2 * n) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * n) + 1) * PI is V21() V29() ext-real Element of REAL
x + (((2 * n) + 1) * PI) is V21() V29() ext-real Element of REAL
[.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
cos . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
(cos (x + (((2 * n) + 1) * PI))) - (cos (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
- (cos x) is V21() V29() ext-real Element of REAL
(- (cos x)) - (cos (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
(- (cos x)) - (cos x) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
exp_R | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (exp_R,A) is V21() V29() ext-real Element of REAL
exp_R || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (exp_R || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
exp_R . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
exp_R . (lower_bound A) is V21() V29() ext-real Element of REAL
(exp_R . (upper_bound A)) - (exp_R . (lower_bound A)) is V21() V29() ext-real Element of REAL
dom (exp_R `| REAL) is set
x is V21() V29() ext-real Element of REAL
(exp_R `| REAL) . x is V21() V29() ext-real Element of REAL
exp_R . x is V21() V29() ext-real Element of REAL
diff (exp_R,x) is V21() V29() ext-real Element of REAL
exp_R | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
[.0,1.] is V49() V50() V51() V91() closed Element of K19(REAL)
number_e - 1 is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (exp_R,A) is V21() V29() ext-real Element of REAL
exp_R || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (exp_R || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
sinh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
sinh | REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
sinh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (sinh,A) is V21() V29() ext-real Element of REAL
sinh || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (sinh || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
cosh . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cosh . (lower_bound A) is V21() V29() ext-real Element of REAL
(cosh . (upper_bound A)) - (cosh . (lower_bound A)) is V21() V29() ext-real Element of REAL
dom (cosh `| REAL) is set
x is V21() V29() ext-real Element of REAL
(cosh `| REAL) . x is V21() V29() ext-real Element of REAL
sinh . x is V21() V29() ext-real Element of REAL
diff (cosh,x) is V21() V29() ext-real Element of REAL
sinh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(number_e - 1) ^2 is V21() V29() ext-real Element of REAL
K86((number_e - 1),(number_e - 1)) is V21() V29() ext-real set
((number_e - 1) ^2) / (2 * number_e) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (sinh,A) is V21() V29() ext-real Element of REAL
sinh || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (sinh || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(((number_e ^2) + 1) / (2 * number_e)) - 1 is V21() V29() ext-real Element of REAL
(2 * number_e) / (2 * number_e) is V21() V29() ext-real Element of REAL
(((number_e ^2) + 1) / (2 * number_e)) - ((2 * number_e) / (2 * number_e)) is V21() V29() ext-real Element of REAL
((number_e ^2) + 1) - (2 * number_e) is V21() V29() ext-real Element of REAL
(((number_e ^2) + 1) - (2 * number_e)) / (2 * number_e) is V21() V29() ext-real Element of REAL
(2 * number_e) * 1 is V21() V29() ext-real Element of REAL
(number_e ^2) - ((2 * number_e) * 1) is V21() V29() ext-real Element of REAL
1 ^2 is V21() V29() ext-real Element of REAL
K86(1,1) is V21() V29() V30() ext-real non negative set
((number_e ^2) - ((2 * number_e) * 1)) + (1 ^2) is V21() V29() ext-real Element of REAL
(((number_e ^2) - ((2 * number_e) * 1)) + (1 ^2)) / (2 * number_e) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
cosh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
cosh | REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
cosh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cosh,A) is V21() V29() ext-real Element of REAL
cosh || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cosh || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
sinh . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sinh . (lower_bound A) is V21() V29() ext-real Element of REAL
(sinh . (upper_bound A)) - (sinh . (lower_bound A)) is V21() V29() ext-real Element of REAL
dom (sinh `| REAL) is set
x is V21() V29() ext-real Element of REAL
(sinh `| REAL) . x is V21() V29() ext-real Element of REAL
cosh . x is V21() V29() ext-real Element of REAL
diff (sinh,x) is V21() V29() ext-real Element of REAL
cosh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral (cosh,A) is V21() V29() ext-real Element of REAL
cosh || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral (cosh || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(sinh . 1) - 0 is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom A is set
x is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
A | x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (A,x) is V21() V29() ext-real Element of REAL
A || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
K20(x,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(x,REAL)) is set
integral (A || x) is V21() V29() ext-real Element of REAL
upper_bound x is V21() V29() ext-real Element of REAL
tan . (upper_bound x) is V21() V29() ext-real Element of REAL
lower_bound x is V21() V29() ext-real Element of REAL
tan . (lower_bound x) is V21() V29() ext-real Element of REAL
(tan . (upper_bound x)) - (tan . (lower_bound x)) is V21() V29() ext-real Element of REAL
n is V49() V50() V51() open Element of K19(REAL)
tan `| n is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (tan `| n) is set
Z is V21() V29() ext-real Element of REAL
(tan `| n) . Z is V21() V29() ext-real Element of REAL
A . Z is V21() V29() ext-real Element of REAL
cos . Z is V21() V29() ext-real Element of REAL
(cos . Z) ^2 is V21() V29() ext-real Element of REAL
K86((cos . Z),(cos . Z)) is V21() V29() ext-real set
1 / ((cos . Z) ^2) is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom A is set
x is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
A | x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (A,x) is V21() V29() ext-real Element of REAL
A || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
K20(x,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(x,REAL)) is set
integral (A || x) is V21() V29() ext-real Element of REAL
upper_bound x is V21() V29() ext-real Element of REAL
cot . (upper_bound x) is V21() V29() ext-real Element of REAL
lower_bound x is V21() V29() ext-real Element of REAL
cot . (lower_bound x) is V21() V29() ext-real Element of REAL
(cot . (upper_bound x)) - (cot . (lower_bound x)) is V21() V29() ext-real Element of REAL
n is V49() V50() V51() open Element of K19(REAL)
cot `| n is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (cot `| n) is set
Z is V21() V29() ext-real Element of REAL
(cot `| n) . Z is V21() V29() ext-real Element of REAL
A . Z is V21() V29() ext-real Element of REAL
sin . Z is V21() V29() ext-real Element of REAL
(sin . Z) ^2 is V21() V29() ext-real Element of REAL
K86((sin . Z),(sin . Z)) is V21() V29() ext-real set
1 / ((sin . Z) ^2) is V21() V29() ext-real Element of REAL
- (1 / ((sin . Z) ^2)) is V21() V29() ext-real Element of REAL
dom tanh is set
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom A is set
x is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
A | x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (A,x) is V21() V29() ext-real Element of REAL
A || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
K20(x,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(x,REAL)) is set
integral (A || x) is V21() V29() ext-real Element of REAL
upper_bound x is V21() V29() ext-real Element of REAL
tanh . (upper_bound x) is V21() V29() ext-real Element of REAL
lower_bound x is V21() V29() ext-real Element of REAL
tanh . (lower_bound x) is V21() V29() ext-real Element of REAL
(tanh . (upper_bound x)) - (tanh . (lower_bound x)) is V21() V29() ext-real Element of REAL
tanh `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (tanh `| REAL) is set
n is V21() V29() ext-real Element of REAL
(tanh `| REAL) . n is V21() V29() ext-real Element of REAL
A . n is V21() V29() ext-real Element of REAL
diff (tanh,n) is V21() V29() ext-real Element of REAL
cosh . n is V21() V29() ext-real Element of REAL
(cosh . n) ^2 is V21() V29() ext-real Element of REAL
K86((cosh . n),(cosh . n)) is V21() V29() ext-real set
1 / ((cosh . n) ^2) is V21() V29() ext-real Element of REAL
arcsin `| ].(- 1),1.[ is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (arcsin `| ].(- 1),1.[) is set
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom A is set
x is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
A | x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (A,x) is V21() V29() ext-real Element of REAL
A || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
K20(x,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(x,REAL)) is set
integral (A || x) is V21() V29() ext-real Element of REAL
upper_bound x is V21() V29() ext-real Element of REAL
arcsin . (upper_bound x) is V21() V29() ext-real Element of REAL
lower_bound x is V21() V29() ext-real Element of REAL
arcsin . (lower_bound x) is V21() V29() ext-real Element of REAL
(arcsin . (upper_bound x)) - (arcsin . (lower_bound x)) is V21() V29() ext-real Element of REAL
n is V21() V29() ext-real Element of REAL
(arcsin `| ].(- 1),1.[) . n is V21() V29() ext-real Element of REAL
A . n is V21() V29() ext-real Element of REAL
diff (arcsin,n) is V21() V29() ext-real Element of REAL
n ^2 is V21() V29() ext-real Element of REAL
K86(n,n) is V21() V29() ext-real set
1 - (n ^2) is V21() V29() ext-real Element of REAL
sqrt (1 - (n ^2)) is V21() V29() ext-real Element of REAL
1 / (sqrt (1 - (n ^2))) is V21() V29() ext-real Element of REAL
arccos `| ].(- 1),1.[ is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom (arccos `| ].(- 1),1.[) is set
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom A is set
x is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
A | x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (A,x) is V21() V29() ext-real Element of REAL
A || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
K20(x,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(x,REAL)) is set
integral (A || x) is V21() V29() ext-real Element of REAL
upper_bound x is V21() V29() ext-real Element of REAL
arccos . (upper_bound x) is V21() V29() ext-real Element of REAL
lower_bound x is V21() V29() ext-real Element of REAL
arccos . (lower_bound x) is V21() V29() ext-real Element of REAL
(arccos . (upper_bound x)) - (arccos . (lower_bound x)) is V21() V29() ext-real Element of REAL
n is V21() V29() ext-real Element of REAL
(arccos `| ].(- 1),1.[) . n is V21() V29() ext-real Element of REAL
A . n is V21() V29() ext-real Element of REAL
diff (arccos,n) is V21() V29() ext-real Element of REAL
n ^2 is V21() V29() ext-real Element of REAL
K86(n,n) is V21() V29() ext-real set
1 - (n ^2) is V21() V29() ext-real Element of REAL
sqrt (1 - (n ^2)) is V21() V29() ext-real Element of REAL
1 / (sqrt (1 - (n ^2))) is V21() V29() ext-real Element of REAL
- (1 / (sqrt (1 - (n ^2)))) is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom A is set
x is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
A | x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (A,x) is V21() V29() ext-real Element of REAL
A || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
K20(x,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(x,REAL)) is set
integral (A || x) is V21() V29() ext-real Element of REAL
upper_bound x is V21() V29() ext-real Element of REAL
lower_bound x is V21() V29() ext-real Element of REAL
arcsin . ((sqrt 2) / 2) is V21() V29() ext-real Element of REAL
arcsin . (- ((sqrt 2) / 2)) is V21() V29() ext-real Element of REAL
(arcsin . ((sqrt 2) / 2)) - (arcsin . (- ((sqrt 2) / 2))) is V21() V29() ext-real Element of REAL
(arcsin ((sqrt 2) / 2)) - (arcsin . (- ((sqrt 2) / 2))) is V21() V29() ext-real Element of REAL
(arcsin ((sqrt 2) / 2)) - (arcsin (- ((sqrt 2) / 2))) is V21() V29() ext-real Element of REAL
(2 * PI) / 4 is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom A is set
x is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
A | x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (A,x) is V21() V29() ext-real Element of REAL
A || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
K20(x,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(x,REAL)) is set
integral (A || x) is V21() V29() ext-real Element of REAL
upper_bound x is V21() V29() ext-real Element of REAL
lower_bound x is V21() V29() ext-real Element of REAL
arccos . ((sqrt 2) / 2) is V21() V29() ext-real Element of REAL
arccos . (- ((sqrt 2) / 2)) is V21() V29() ext-real Element of REAL
(arccos . ((sqrt 2) / 2)) - (arccos . (- ((sqrt 2) / 2))) is V21() V29() ext-real Element of REAL
(arccos ((sqrt 2) / 2)) - (arccos . (- ((sqrt 2) / 2))) is V21() V29() ext-real Element of REAL
(arccos ((sqrt 2) / 2)) - (arccos (- ((sqrt 2) / 2))) is V21() V29() ext-real Element of REAL
- (2 * PI) is V21() V29() ext-real Element of REAL
(- (2 * PI)) / 4 is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
n is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound n is V21() V29() ext-real Element of REAL
A . (upper_bound n) is V21() V29() ext-real Element of REAL
lower_bound n is V21() V29() ext-real Element of REAL
A . (lower_bound n) is V21() V29() ext-real Element of REAL
(A . (upper_bound n)) - (A . (lower_bound n)) is V21() V29() ext-real Element of REAL
x . (upper_bound n) is V21() V29() ext-real Element of REAL
((A . (upper_bound n)) - (A . (lower_bound n))) + (x . (upper_bound n)) is V21() V29() ext-real Element of REAL
x . (lower_bound n) is V21() V29() ext-real Element of REAL
(((A . (upper_bound n)) - (A . (lower_bound n))) + (x . (upper_bound n))) - (x . (lower_bound n)) is V21() V29() ext-real Element of REAL
Z is V49() V50() V51() open Element of K19(REAL)
A `| Z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(A `| Z) | n is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x `| Z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(x `| Z) | n is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(A `| Z) + (x `| Z) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (((A `| Z) + (x `| Z)),n) is V21() V29() ext-real Element of REAL
((A `| Z) + (x `| Z)) || n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
K20(n,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(n,REAL)) is set
integral (((A `| Z) + (x `| Z)) || n) is V21() V29() ext-real Element of REAL
(A `| Z) || n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
(x `| Z) || n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
dom (x `| Z) is set
dom (A `| Z) is set
((A `| Z) || n) | n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
((x `| Z) || n) | n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
((A `| Z) || n) + ((x `| Z) || n) is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
integral (((A `| Z) || n) + ((x `| Z) || n)) is V21() V29() ext-real Element of REAL
integral ((A `| Z),n) is V21() V29() ext-real Element of REAL
integral ((A `| Z) || n) is V21() V29() ext-real Element of REAL
integral ((x `| Z),n) is V21() V29() ext-real Element of REAL
integral ((x `| Z) || n) is V21() V29() ext-real Element of REAL
(integral ((A `| Z),n)) + (integral ((x `| Z),n)) is V21() V29() ext-real Element of REAL
((A . (upper_bound n)) - (A . (lower_bound n))) + (integral ((x `| Z),n)) is V21() V29() ext-real Element of REAL
(x . (upper_bound n)) - (x . (lower_bound n)) is V21() V29() ext-real Element of REAL
((A . (upper_bound n)) - (A . (lower_bound n))) + ((x . (upper_bound n)) - (x . (lower_bound n))) is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
n is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound n is V21() V29() ext-real Element of REAL
A . (upper_bound n) is V21() V29() ext-real Element of REAL
lower_bound n is V21() V29() ext-real Element of REAL
A . (lower_bound n) is V21() V29() ext-real Element of REAL
(A . (upper_bound n)) - (A . (lower_bound n)) is V21() V29() ext-real Element of REAL
x . (upper_bound n) is V21() V29() ext-real Element of REAL
x . (lower_bound n) is V21() V29() ext-real Element of REAL
(x . (upper_bound n)) - (x . (lower_bound n)) is V21() V29() ext-real Element of REAL
((A . (upper_bound n)) - (A . (lower_bound n))) - ((x . (upper_bound n)) - (x . (lower_bound n))) is V21() V29() ext-real Element of REAL
Z is V49() V50() V51() open Element of K19(REAL)
A `| Z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(A `| Z) | n is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x `| Z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(x `| Z) | n is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(A `| Z) - (x `| Z) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
- (x `| Z) is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
K87(1) * (x `| Z) is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
(A `| Z) + (- (x `| Z)) is Relation-like REAL -defined V6() complex-valued ext-real-valued real-valued set
integral (((A `| Z) - (x `| Z)),n) is V21() V29() ext-real Element of REAL
((A `| Z) - (x `| Z)) || n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
K20(n,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(n,REAL)) is set
integral (((A `| Z) - (x `| Z)) || n) is V21() V29() ext-real Element of REAL
(A `| Z) || n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
(x `| Z) || n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
dom (x `| Z) is set
dom (A `| Z) is set
((A `| Z) || n) | n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
((x `| Z) || n) | n is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
((A `| Z) || n) - ((x `| Z) || n) is Relation-like n -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(n,REAL))
- ((x `| Z) || n) is Relation-like n -defined V6() complex-valued ext-real-valued real-valued set
K87(1) * ((x `| Z) || n) is Relation-like n -defined V6() complex-valued ext-real-valued real-valued set
((A `| Z) || n) + (- ((x `| Z) || n)) is Relation-like n -defined V6() complex-valued ext-real-valued real-valued set
integral (((A `| Z) || n) - ((x `| Z) || n)) is V21() V29() ext-real Element of REAL
integral ((A `| Z),n) is V21() V29() ext-real Element of REAL
integral ((A `| Z) || n) is V21() V29() ext-real Element of REAL
integral ((x `| Z) || n) is V21() V29() ext-real Element of REAL
(integral ((A `| Z),n)) - (integral ((x `| Z) || n)) is V21() V29() ext-real Element of REAL
integral ((x `| Z),n) is V21() V29() ext-real Element of REAL
((A . (upper_bound n)) - (A . (lower_bound n))) - (integral ((x `| Z),n)) is V21() V29() ext-real Element of REAL
A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
x is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound x is V21() V29() ext-real Element of REAL
A . (upper_bound x) is V21() V29() ext-real Element of REAL
lower_bound x is V21() V29() ext-real Element of REAL
A . (lower_bound x) is V21() V29() ext-real Element of REAL
n is V21() V29() ext-real Element of REAL
n * (A . (upper_bound x)) is V21() V29() ext-real Element of REAL
n * (A . (lower_bound x)) is V21() V29() ext-real Element of REAL
(n * (A . (upper_bound x))) - (n * (A . (lower_bound x))) is V21() V29() ext-real Element of REAL
Z is V49() V50() V51() open Element of K19(REAL)
A `| Z is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(A `| Z) | x is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
n (#) (A `| Z) is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral ((n (#) (A `| Z)),x) is V21() V29() ext-real Element of REAL
(n (#) (A `| Z)) || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
K20(x,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(x,REAL)) is set
integral ((n (#) (A `| Z)) || x) is V21() V29() ext-real Element of REAL
(A `| Z) || x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
((A `| Z) || x) | x is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
dom (A `| Z) is set
n (#) ((A `| Z) || x) is Relation-like x -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(x,REAL))
integral (n (#) ((A `| Z) || x)) is V21() V29() ext-real Element of REAL
integral ((A `| Z),x) is V21() V29() ext-real Element of REAL
integral ((A `| Z) || x) is V21() V29() ext-real Element of REAL
n * (integral ((A `| Z),x)) is V21() V29() ext-real Element of REAL
(A . (upper_bound x)) - (A . (lower_bound x)) is V21() V29() ext-real Element of REAL
n * ((A . (upper_bound x)) - (A . (lower_bound x))) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
sin | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
sin + cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin + cos),A) is V21() V29() ext-real Element of REAL
(sin + cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin + cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
(- cos) . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (lower_bound A) is V21() V29() ext-real Element of REAL
((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A)) is V21() V29() ext-real Element of REAL
sin . (upper_bound A) is V21() V29() ext-real Element of REAL
(((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) + (sin . (upper_bound A)) is V21() V29() ext-real Element of REAL
sin . (lower_bound A) is V21() V29() ext-real Element of REAL
((((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) + (sin . (upper_bound A))) - (sin . (lower_bound A)) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
sin | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
cos | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin + cos),A) is V21() V29() ext-real Element of REAL
(sin + cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin + cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (PI / 2) is V21() V29() ext-real Element of REAL
(- cos) . 0 is V21() V29() ext-real Element of REAL
((- cos) . (PI / 2)) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
sin . (PI / 2) is V21() V29() ext-real Element of REAL
(((- cos) . (PI / 2)) - ((- cos) . 0)) + (sin . (PI / 2)) is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
((((- cos) . (PI / 2)) - ((- cos) . 0)) + (sin . (PI / 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
cos . (PI / 2) is V21() V29() ext-real Element of REAL
- (cos . (PI / 2)) is V21() V29() ext-real Element of REAL
(- (cos . (PI / 2))) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
((- (cos . (PI / 2))) - ((- cos) . 0)) + (sin . (PI / 2)) is V21() V29() ext-real Element of REAL
(((- (cos . (PI / 2))) - ((- cos) . 0)) + (sin . (PI / 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
- 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos . 0) is V21() V29() ext-real Element of REAL
(- 0) - (- (cos . 0)) is V21() V29() ext-real Element of REAL
((- 0) - (- (cos . 0))) + 1 is V21() V29() ext-real Element of REAL
(((- 0) - (- (cos . 0))) + 1) - (sin . 0) is V21() V29() ext-real Element of REAL
- (- (cos . 0)) is V21() V29() ext-real Element of REAL
(- (- (cos . 0))) + 1 is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
((- (- (cos . 0))) + 1) - (sin . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
- (- (cos . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
(- (- (cos . (0 + (2 * PI))))) + 1 is V21() V29() ext-real Element of REAL
((- (- (cos . (0 + (2 * PI))))) + 1) - 0 is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin + cos),A) is V21() V29() ext-real Element of REAL
(sin + cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin + cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . PI is V21() V29() ext-real Element of REAL
(- cos) . 0 is V21() V29() ext-real Element of REAL
((- cos) . PI) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
sin . PI is V21() V29() ext-real Element of REAL
(((- cos) . PI) - ((- cos) . 0)) + (sin . PI) is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
((((- cos) . PI) - ((- cos) . 0)) + (sin . PI)) - (sin . 0) is V21() V29() ext-real Element of REAL
cos . PI is V21() V29() ext-real Element of REAL
- (cos . PI) is V21() V29() ext-real Element of REAL
(- (cos . PI)) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
((- (cos . PI)) - ((- cos) . 0)) + (sin . PI) is V21() V29() ext-real Element of REAL
(((- (cos . PI)) - ((- cos) . 0)) + (sin . PI)) - (sin . 0) is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos . 0) is V21() V29() ext-real Element of REAL
(- (cos . PI)) - (- (cos . 0)) is V21() V29() ext-real Element of REAL
((- (cos . PI)) - (- (cos . 0))) + (sin . PI) is V21() V29() ext-real Element of REAL
(((- (cos . PI)) - (- (cos . 0))) + (sin . PI)) - (sin . 0) is V21() V29() ext-real Element of REAL
- (- (cos . 0)) is V21() V29() ext-real Element of REAL
(- (- (cos . 0))) + 1 is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
((- (- (cos . 0))) + 1) - (sin . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
- (- (cos . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
(- (- (cos . (0 + (2 * PI))))) + 1 is V21() V29() ext-real Element of REAL
((- (- (cos . (0 + (2 * PI))))) + 1) - 0 is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin + cos),A) is V21() V29() ext-real Element of REAL
(sin + cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin + cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . ((PI * 3) / 2) is V21() V29() ext-real Element of REAL
(- cos) . 0 is V21() V29() ext-real Element of REAL
((- cos) . ((PI * 3) / 2)) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
sin . ((PI * 3) / 2) is V21() V29() ext-real Element of REAL
(((- cos) . ((PI * 3) / 2)) - ((- cos) . 0)) + (sin . ((PI * 3) / 2)) is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
((((- cos) . ((PI * 3) / 2)) - ((- cos) . 0)) + (sin . ((PI * 3) / 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
cos . ((PI * 3) / 2) is V21() V29() ext-real Element of REAL
- (cos . ((PI * 3) / 2)) is V21() V29() ext-real Element of REAL
(- (cos . ((PI * 3) / 2))) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
((- (cos . ((PI * 3) / 2))) - ((- cos) . 0)) + (sin . ((PI * 3) / 2)) is V21() V29() ext-real Element of REAL
(((- (cos . ((PI * 3) / 2))) - ((- cos) . 0)) + (sin . ((PI * 3) / 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos . 0) is V21() V29() ext-real Element of REAL
(- (cos . ((PI * 3) / 2))) - (- (cos . 0)) is V21() V29() ext-real Element of REAL
((- (cos . ((PI * 3) / 2))) - (- (cos . 0))) + (sin . ((PI * 3) / 2)) is V21() V29() ext-real Element of REAL
(((- (cos . ((PI * 3) / 2))) - (- (cos . 0))) + (sin . ((PI * 3) / 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(- (cos . ((PI * 3) / 2))) - (- (cos . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
((- (cos . ((PI * 3) / 2))) - (- (cos . (0 + (2 * PI))))) + (sin . ((PI * 3) / 2)) is V21() V29() ext-real Element of REAL
(((- (cos . ((PI * 3) / 2))) - (- (cos . (0 + (2 * PI))))) + (sin . ((PI * 3) / 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
- 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
(- 0) + 1 is non empty V21() V29() V30() ext-real positive non negative Element of REAL
((- 0) + 1) + (- 1) is V21() V29() V30() ext-real Element of REAL
(((- 0) + 1) + (- 1)) - 0 is V21() V29() V30() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin + cos),A) is V21() V29() ext-real Element of REAL
(sin + cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin + cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (PI * 2) is V21() V29() ext-real Element of REAL
(- cos) . 0 is V21() V29() ext-real Element of REAL
((- cos) . (PI * 2)) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
sin . (PI * 2) is V21() V29() ext-real Element of REAL
(((- cos) . (PI * 2)) - ((- cos) . 0)) + (sin . (PI * 2)) is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
((((- cos) . (PI * 2)) - ((- cos) . 0)) + (sin . (PI * 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
cos . (PI * 2) is V21() V29() ext-real Element of REAL
- (cos . (PI * 2)) is V21() V29() ext-real Element of REAL
(- (cos . (PI * 2))) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
((- (cos . (PI * 2))) - ((- cos) . 0)) + (sin . (PI * 2)) is V21() V29() ext-real Element of REAL
(((- (cos . (PI * 2))) - ((- cos) . 0)) + (sin . (PI * 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos . 0) is V21() V29() ext-real Element of REAL
(- (cos . (PI * 2))) - (- (cos . 0)) is V21() V29() ext-real Element of REAL
((- (cos . (PI * 2))) - (- (cos . 0))) + (sin . (PI * 2)) is V21() V29() ext-real Element of REAL
(((- (cos . (PI * 2))) - (- (cos . 0))) + (sin . (PI * 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(- (cos . (PI * 2))) - (- (cos . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
((- (cos . (PI * 2))) - (- (cos . (0 + (2 * PI))))) + (sin . (PI * 2)) is V21() V29() ext-real Element of REAL
(((- (cos . (PI * 2))) - (- (cos . (0 + (2 * PI))))) + (sin . (PI * 2))) - (sin . 0) is V21() V29() ext-real Element of REAL
(- 1) + 1 is V21() V29() V30() ext-real Element of REAL
((- 1) + 1) + 0 is V21() V29() V30() ext-real Element of REAL
(((- 1) + 1) + 0) - 0 is V21() V29() V30() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin + cos),A) is V21() V29() ext-real Element of REAL
(sin + cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin + cos) || A) is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) * PI is V21() V29() ext-real Element of REAL
(2 * x) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * x) + 1) * PI is V21() V29() ext-real Element of REAL
[.((2 * x) * PI),(((2 * x) + 1) * PI).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
(- cos) . ((2 * x) * PI) is V21() V29() ext-real Element of REAL
((- cos) . (((2 * x) + 1) * PI)) - ((- cos) . ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
sin . (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
(((- cos) . (((2 * x) + 1) * PI)) - ((- cos) . ((2 * x) * PI))) + (sin . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . ((2 * x) * PI) is V21() V29() ext-real Element of REAL
((((- cos) . (((2 * x) + 1) * PI)) - ((- cos) . ((2 * x) * PI))) + (sin . (((2 * x) + 1) * PI))) - (sin . ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
cos . (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
- (cos . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) - ((- cos) . ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) - ((- cos) . ((2 * x) * PI))) + (sin . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
(((- (cos . (((2 * x) + 1) * PI))) - ((- cos) . ((2 * x) * PI))) + (sin . (((2 * x) + 1) * PI))) - (sin . ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
0 + ((2 * x) * PI) is V21() V29() ext-real Element of REAL
cos (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
- (cos (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) - (- (cos (0 + ((2 * x) * PI)))) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) - (- (cos (0 + ((2 * x) * PI))))) + (sin . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
(((- (cos . (((2 * x) + 1) * PI))) - (- (cos (0 + ((2 * x) * PI))))) + (sin . (((2 * x) + 1) * PI))) - (sin . (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
cos 0 is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos 0) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) - (- (cos 0)) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) - (- (cos 0))) + (sin . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
(((- (cos . (((2 * x) + 1) * PI))) - (- (cos 0))) + (sin . (((2 * x) + 1) * PI))) - (sin . (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) + (cos 0) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) + (cos 0)) + (sin . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
(((- (cos . (((2 * x) + 1) * PI))) + (cos 0)) + (sin . (((2 * x) + 1) * PI))) - (sin . (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) + (cos (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) + (cos (0 + (2 * PI)))) + (sin . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
(((- (cos . (((2 * x) + 1) * PI))) + (cos (0 + (2 * PI)))) + (sin . (((2 * x) + 1) * PI))) - (sin . (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) + 1 is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) + 1) + (sin . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
(((- (cos . (((2 * x) + 1) * PI))) + 1) + (sin . (((2 * x) + 1) * PI))) - (sin (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
sin 0 is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
(((- (cos . (((2 * x) + 1) * PI))) + 1) + (sin . (((2 * x) + 1) * PI))) - (sin 0) is V21() V29() ext-real Element of REAL
sin (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(((- (cos . (((2 * x) + 1) * PI))) + 1) + (sin . (((2 * x) + 1) * PI))) - (sin (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
0 + (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
cos (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
- (cos (0 + (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
(- (cos (0 + (((2 * x) + 1) * PI)))) + 1 is V21() V29() ext-real Element of REAL
sin (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
((- (cos (0 + (((2 * x) + 1) * PI)))) + 1) + (sin (0 + (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
- (sin 0) is V21() V29() ext-real Element of REAL
((- (cos (0 + (((2 * x) + 1) * PI)))) + 1) + (- (sin 0)) is V21() V29() ext-real Element of REAL
- (- (cos 0)) is V21() V29() ext-real Element of REAL
(- (- (cos 0))) + 1 is V21() V29() ext-real Element of REAL
((- (- (cos 0))) + 1) + (- (sin 0)) is V21() V29() ext-real Element of REAL
(cos 0) + 1 is V21() V29() ext-real Element of REAL
((cos 0) + 1) - (sin 0) is V21() V29() ext-real Element of REAL
(cos (0 + (2 * PI))) + 1 is V21() V29() ext-real Element of REAL
((cos (0 + (2 * PI))) + 1) - (sin 0) is V21() V29() ext-real Element of REAL
((cos (0 + (2 * PI))) + 1) - (sin (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin + cos),A) is V21() V29() ext-real Element of REAL
(sin + cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin + cos) || A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
cos x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
2 * (cos x) is V21() V29() ext-real Element of REAL
sin x is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
2 * (sin x) is V21() V29() ext-real Element of REAL
(2 * (cos x)) - (2 * (sin x)) is V21() V29() ext-real Element of REAL
n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * n) * PI is V21() V29() ext-real Element of REAL
x + ((2 * n) * PI) is V21() V29() ext-real Element of REAL
(2 * n) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * n) + 1) * PI is V21() V29() ext-real Element of REAL
x + (((2 * n) + 1) * PI) is V21() V29() ext-real Element of REAL
[.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
(- cos) . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
((- cos) . (x + (((2 * n) + 1) * PI))) - ((- cos) . (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
sin . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
(((- cos) . (x + (((2 * n) + 1) * PI))) - ((- cos) . (x + ((2 * n) * PI)))) + (sin . (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
sin . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
((((- cos) . (x + (((2 * n) + 1) * PI))) - ((- cos) . (x + ((2 * n) * PI)))) + (sin . (x + (((2 * n) + 1) * PI)))) - (sin . (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
cos . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
- (cos . (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
(- (cos . (x + (((2 * n) + 1) * PI)))) - ((- cos) . (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
((- (cos . (x + (((2 * n) + 1) * PI)))) - ((- cos) . (x + ((2 * n) * PI)))) + (sin . (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
(((- (cos . (x + (((2 * n) + 1) * PI)))) - ((- cos) . (x + ((2 * n) * PI)))) + (sin . (x + (((2 * n) + 1) * PI)))) - (sin . (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
cos (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
- (cos (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
cos (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
cos . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
- (cos (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
(- (cos (x + (((2 * n) + 1) * PI)))) - (- (cos (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
sin (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
((- (cos (x + (((2 * n) + 1) * PI)))) - (- (cos (x + ((2 * n) * PI))))) + (sin (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
sin (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
sin . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
(((- (cos (x + (((2 * n) + 1) * PI)))) - (- (cos (x + ((2 * n) * PI))))) + (sin (x + (((2 * n) + 1) * PI)))) - (sin (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
- (cos x) is V21() V29() ext-real Element of REAL
- (- (cos x)) is V21() V29() ext-real Element of REAL
(- (- (cos x))) - (- (cos (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
((- (- (cos x))) - (- (cos (x + ((2 * n) * PI))))) + (sin (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
(((- (- (cos x))) - (- (cos (x + ((2 * n) * PI))))) + (sin (x + (((2 * n) + 1) * PI)))) - (sin (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
(- (- (cos x))) - (- (cos x)) is V21() V29() ext-real Element of REAL
((- (- (cos x))) - (- (cos x))) + (sin (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
(((- (- (cos x))) - (- (cos x))) + (sin (x + (((2 * n) + 1) * PI)))) - (sin (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
- (sin x) is V21() V29() ext-real Element of REAL
((- (- (cos x))) - (- (cos x))) + (- (sin x)) is V21() V29() ext-real Element of REAL
(((- (- (cos x))) - (- (cos x))) + (- (sin x))) - (sin (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
(cos x) + (cos x) is V21() V29() ext-real Element of REAL
((cos x) + (cos x)) - (sin x) is V21() V29() ext-real Element of REAL
(((cos x) + (cos x)) - (sin x)) - (sin x) is V21() V29() ext-real Element of REAL
sinh + cosh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sinh + cosh),A) is V21() V29() ext-real Element of REAL
(sinh + cosh) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sinh + cosh) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
cosh . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cosh . (lower_bound A) is V21() V29() ext-real Element of REAL
(cosh . (upper_bound A)) - (cosh . (lower_bound A)) is V21() V29() ext-real Element of REAL
sinh . (upper_bound A) is V21() V29() ext-real Element of REAL
((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A)) is V21() V29() ext-real Element of REAL
sinh . (lower_bound A) is V21() V29() ext-real Element of REAL
(((cosh . (upper_bound A)) - (cosh . (lower_bound A))) + (sinh . (upper_bound A))) - (sinh . (lower_bound A)) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
cosh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
sinh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sinh + cosh),A) is V21() V29() ext-real Element of REAL
(sinh + cosh) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sinh + cosh) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(cosh . 1) - (cosh . 0) is V21() V29() ext-real Element of REAL
((cosh . 1) - (cosh . 0)) + (sinh . 1) is V21() V29() ext-real Element of REAL
sinh . 0 is V21() V29() ext-real Element of REAL
(((cosh . 1) - (cosh . 0)) + (sinh . 1)) - (sinh . 0) is V21() V29() ext-real Element of REAL
(((number_e ^2) + 1) / (2 * number_e)) + (((number_e ^2) - 1) / (2 * number_e)) is V21() V29() ext-real Element of REAL
((((number_e ^2) + 1) / (2 * number_e)) + (((number_e ^2) - 1) / (2 * number_e))) - 1 is V21() V29() ext-real Element of REAL
((number_e ^2) + 1) + ((number_e ^2) - 1) is V21() V29() ext-real Element of REAL
(((number_e ^2) + 1) + ((number_e ^2) - 1)) / (2 * number_e) is V21() V29() ext-real Element of REAL
((((number_e ^2) + 1) + ((number_e ^2) - 1)) / (2 * number_e)) - 1 is V21() V29() ext-real Element of REAL
2 * (number_e ^2) is V21() V29() ext-real Element of REAL
(2 * (number_e ^2)) / (2 * number_e) is V21() V29() ext-real Element of REAL
((2 * (number_e ^2)) / (2 * number_e)) - 1 is V21() V29() ext-real Element of REAL
(number_e ^2) / number_e is V21() V29() ext-real Element of REAL
((number_e ^2) / number_e) - 1 is V21() V29() ext-real Element of REAL
number_e * number_e is V21() V29() ext-real Element of REAL
(number_e * number_e) / number_e is V21() V29() ext-real Element of REAL
((number_e * number_e) / number_e) - 1 is V21() V29() ext-real Element of REAL
sin - cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
- cos is Relation-like REAL -defined V6() total complex-valued ext-real-valued real-valued set
sin + (- cos) is Relation-like REAL -defined V6() total complex-valued ext-real-valued real-valued set
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin - cos),A) is V21() V29() ext-real Element of REAL
(sin - cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin - cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
(- cos) . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (lower_bound A) is V21() V29() ext-real Element of REAL
((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A)) is V21() V29() ext-real Element of REAL
sin . (upper_bound A) is V21() V29() ext-real Element of REAL
sin . (lower_bound A) is V21() V29() ext-real Element of REAL
(sin . (upper_bound A)) - (sin . (lower_bound A)) is V21() V29() ext-real Element of REAL
(((- cos) . (upper_bound A)) - ((- cos) . (lower_bound A))) - ((sin . (upper_bound A)) - (sin . (lower_bound A))) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
sin | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
cos | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin - cos),A) is V21() V29() ext-real Element of REAL
(sin - cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin - cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (PI / 2) is V21() V29() ext-real Element of REAL
(- cos) . 0 is V21() V29() ext-real Element of REAL
((- cos) . (PI / 2)) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
sin . (PI / 2) is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
(sin . (PI / 2)) - (sin . 0) is V21() V29() ext-real Element of REAL
(((- cos) . (PI / 2)) - ((- cos) . 0)) - ((sin . (PI / 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
cos . (PI / 2) is V21() V29() ext-real Element of REAL
- (cos . (PI / 2)) is V21() V29() ext-real Element of REAL
(- (cos . (PI / 2))) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
((- (cos . (PI / 2))) - ((- cos) . 0)) - ((sin . (PI / 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
- 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos . 0) is V21() V29() ext-real Element of REAL
(- 0) - (- (cos . 0)) is V21() V29() ext-real Element of REAL
1 - (sin . 0) is V21() V29() ext-real Element of REAL
((- 0) - (- (cos . 0))) - (1 - (sin . 0)) is V21() V29() ext-real Element of REAL
- (- (cos . 0)) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
1 - (sin . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(- (- (cos . 0))) - (1 - (sin . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
- (- (cos . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
1 - 0 is non empty V21() V29() V30() ext-real positive non negative Element of REAL
(- (- (cos . (0 + (2 * PI))))) - (1 - 0) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin - cos),A) is V21() V29() ext-real Element of REAL
(sin - cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin - cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . PI is V21() V29() ext-real Element of REAL
(- cos) . 0 is V21() V29() ext-real Element of REAL
((- cos) . PI) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
sin . PI is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
(sin . PI) - (sin . 0) is V21() V29() ext-real Element of REAL
(((- cos) . PI) - ((- cos) . 0)) - ((sin . PI) - (sin . 0)) is V21() V29() ext-real Element of REAL
cos . PI is V21() V29() ext-real Element of REAL
- (cos . PI) is V21() V29() ext-real Element of REAL
(- (cos . PI)) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
((- (cos . PI)) - ((- cos) . 0)) - ((sin . PI) - (sin . 0)) is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos . 0) is V21() V29() ext-real Element of REAL
(- (cos . PI)) - (- (cos . 0)) is V21() V29() ext-real Element of REAL
((- (cos . PI)) - (- (cos . 0))) - ((sin . PI) - (sin . 0)) is V21() V29() ext-real Element of REAL
- (- (cos . 0)) is V21() V29() ext-real Element of REAL
(- (- (cos . 0))) + 1 is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(sin . (0 + (2 * PI))) - 0 is V21() V29() ext-real Element of REAL
((- (- (cos . 0))) + 1) - ((sin . (0 + (2 * PI))) - 0) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
- (- (cos . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
(- (- (cos . (0 + (2 * PI))))) + 1 is V21() V29() ext-real Element of REAL
((- (- (cos . (0 + (2 * PI))))) + 1) - 0 is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin - cos),A) is V21() V29() ext-real Element of REAL
(sin - cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin - cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . ((PI * 3) / 2) is V21() V29() ext-real Element of REAL
(- cos) . 0 is V21() V29() ext-real Element of REAL
((- cos) . ((PI * 3) / 2)) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
sin . ((PI * 3) / 2) is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
(sin . ((PI * 3) / 2)) - (sin . 0) is V21() V29() ext-real Element of REAL
(((- cos) . ((PI * 3) / 2)) - ((- cos) . 0)) - ((sin . ((PI * 3) / 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
cos . ((PI * 3) / 2) is V21() V29() ext-real Element of REAL
- (cos . ((PI * 3) / 2)) is V21() V29() ext-real Element of REAL
(- (cos . ((PI * 3) / 2))) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
((- (cos . ((PI * 3) / 2))) - ((- cos) . 0)) - ((sin . ((PI * 3) / 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos . 0) is V21() V29() ext-real Element of REAL
(- (cos . ((PI * 3) / 2))) - (- (cos . 0)) is V21() V29() ext-real Element of REAL
((- (cos . ((PI * 3) / 2))) - (- (cos . 0))) - ((sin . ((PI * 3) / 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(- (cos . ((PI * 3) / 2))) - (- (cos . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
((- (cos . ((PI * 3) / 2))) - (- (cos . (0 + (2 * PI))))) - ((sin . ((PI * 3) / 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
- 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
(- 0) + 1 is non empty V21() V29() V30() ext-real positive non negative Element of REAL
(- 1) - 0 is V21() V29() V30() ext-real non positive Element of REAL
((- 0) + 1) - ((- 1) - 0) is non empty V21() V29() V30() ext-real positive non negative Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin - cos),A) is V21() V29() ext-real Element of REAL
(sin - cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin - cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (PI * 2) is V21() V29() ext-real Element of REAL
(- cos) . 0 is V21() V29() ext-real Element of REAL
((- cos) . (PI * 2)) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
sin . (PI * 2) is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
(sin . (PI * 2)) - (sin . 0) is V21() V29() ext-real Element of REAL
(((- cos) . (PI * 2)) - ((- cos) . 0)) - ((sin . (PI * 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
cos . (PI * 2) is V21() V29() ext-real Element of REAL
- (cos . (PI * 2)) is V21() V29() ext-real Element of REAL
(- (cos . (PI * 2))) - ((- cos) . 0) is V21() V29() ext-real Element of REAL
((- (cos . (PI * 2))) - ((- cos) . 0)) - ((sin . (PI * 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos . 0) is V21() V29() ext-real Element of REAL
(- (cos . (PI * 2))) - (- (cos . 0)) is V21() V29() ext-real Element of REAL
((- (cos . (PI * 2))) - (- (cos . 0))) - ((sin . (PI * 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
- (cos . (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(- (cos . (PI * 2))) - (- (cos . (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
((- (cos . (PI * 2))) - (- (cos . (0 + (2 * PI))))) - ((sin . (PI * 2)) - (sin . 0)) is V21() V29() ext-real Element of REAL
(- 1) + 1 is V21() V29() V30() ext-real Element of REAL
0 - 0 is empty V21() V29() V30() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of REAL
((- 1) + 1) - (0 - 0) is V21() V29() V30() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin - cos),A) is V21() V29() ext-real Element of REAL
(sin - cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin - cos) || A) is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) * PI is V21() V29() ext-real Element of REAL
(2 * x) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * x) + 1) * PI is V21() V29() ext-real Element of REAL
[.((2 * x) * PI),(((2 * x) + 1) * PI).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
(- cos) . ((2 * x) * PI) is V21() V29() ext-real Element of REAL
((- cos) . (((2 * x) + 1) * PI)) - ((- cos) . ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
sin . (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
sin . ((2 * x) * PI) is V21() V29() ext-real Element of REAL
(sin . (((2 * x) + 1) * PI)) - (sin . ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
(((- cos) . (((2 * x) + 1) * PI)) - ((- cos) . ((2 * x) * PI))) - ((sin . (((2 * x) + 1) * PI)) - (sin . ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
cos . (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
- (cos . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) - ((- cos) . ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) - ((- cos) . ((2 * x) * PI))) - ((sin . (((2 * x) + 1) * PI)) - (sin . ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
0 + ((2 * x) * PI) is V21() V29() ext-real Element of REAL
cos (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
- (cos (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) - (- (cos (0 + ((2 * x) * PI)))) is V21() V29() ext-real Element of REAL
sin . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
(sin . (((2 * x) + 1) * PI)) - (sin . (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) - (- (cos (0 + ((2 * x) * PI))))) - ((sin . (((2 * x) + 1) * PI)) - (sin . (0 + ((2 * x) * PI)))) is V21() V29() ext-real Element of REAL
cos 0 is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
- (cos 0) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) - (- (cos 0)) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) - (- (cos 0))) - ((sin . (((2 * x) + 1) * PI)) - (sin . (0 + ((2 * x) * PI)))) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) + (cos 0) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) + (cos 0)) - ((sin . (((2 * x) + 1) * PI)) - (sin . (0 + ((2 * x) * PI)))) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) + (cos (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) + (cos (0 + (2 * PI)))) - ((sin . (((2 * x) + 1) * PI)) - (sin . (0 + ((2 * x) * PI)))) is V21() V29() ext-real Element of REAL
(- (cos . (((2 * x) + 1) * PI))) + 1 is V21() V29() ext-real Element of REAL
sin (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
(sin . (((2 * x) + 1) * PI)) - (sin (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) + 1) - ((sin . (((2 * x) + 1) * PI)) - (sin (0 + ((2 * x) * PI)))) is V21() V29() ext-real Element of REAL
sin 0 is V21() V29() ext-real Element of REAL
sin . 0 is V21() V29() ext-real Element of REAL
(sin . (((2 * x) + 1) * PI)) - (sin 0) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) + 1) - ((sin . (((2 * x) + 1) * PI)) - (sin 0)) is V21() V29() ext-real Element of REAL
sin (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(sin . (((2 * x) + 1) * PI)) - (sin (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
((- (cos . (((2 * x) + 1) * PI))) + 1) - ((sin . (((2 * x) + 1) * PI)) - (sin (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
0 + (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
cos (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
- (cos (0 + (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
(- (cos (0 + (((2 * x) + 1) * PI)))) + 1 is V21() V29() ext-real Element of REAL
sin (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
((- (cos (0 + (((2 * x) + 1) * PI)))) + 1) - (sin (0 + (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
- (sin 0) is V21() V29() ext-real Element of REAL
((- (cos (0 + (((2 * x) + 1) * PI)))) + 1) - (- (sin 0)) is V21() V29() ext-real Element of REAL
- (- (cos 0)) is V21() V29() ext-real Element of REAL
(- (- (cos 0))) + 1 is V21() V29() ext-real Element of REAL
((- (- (cos 0))) + 1) - (- (sin 0)) is V21() V29() ext-real Element of REAL
(cos 0) + 1 is V21() V29() ext-real Element of REAL
((cos 0) + 1) + (sin 0) is V21() V29() ext-real Element of REAL
(cos (0 + (2 * PI))) + 1 is V21() V29() ext-real Element of REAL
((cos (0 + (2 * PI))) + 1) + (sin 0) is V21() V29() ext-real Element of REAL
((cos (0 + (2 * PI))) + 1) + (sin (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin - cos),A) is V21() V29() ext-real Element of REAL
(sin - cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin - cos) || A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
cos x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
2 * (cos x) is V21() V29() ext-real Element of REAL
sin x is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
2 * (sin x) is V21() V29() ext-real Element of REAL
(2 * (cos x)) + (2 * (sin x)) is V21() V29() ext-real Element of REAL
n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * n) * PI is V21() V29() ext-real Element of REAL
x + ((2 * n) * PI) is V21() V29() ext-real Element of REAL
(2 * n) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * n) + 1) * PI is V21() V29() ext-real Element of REAL
x + (((2 * n) + 1) * PI) is V21() V29() ext-real Element of REAL
[.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
(- cos) . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
((- cos) . (x + (((2 * n) + 1) * PI))) - ((- cos) . (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
sin . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
(sin . (x + (((2 * n) + 1) * PI))) - (sin . (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
(((- cos) . (x + (((2 * n) + 1) * PI))) - ((- cos) . (x + ((2 * n) * PI)))) - ((sin . (x + (((2 * n) + 1) * PI))) - (sin . (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
cos . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
- (cos . (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
(- (cos . (x + (((2 * n) + 1) * PI)))) - ((- cos) . (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
((- (cos . (x + (((2 * n) + 1) * PI)))) - ((- cos) . (x + ((2 * n) * PI)))) - ((sin . (x + (((2 * n) + 1) * PI))) - (sin . (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
cos (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
- (cos (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
cos (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
cos . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
- (cos (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
(- (cos (x + (((2 * n) + 1) * PI)))) - (- (cos (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
sin (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
sin (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
sin . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
(sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
((- (cos (x + (((2 * n) + 1) * PI)))) - (- (cos (x + ((2 * n) * PI))))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
- (cos x) is V21() V29() ext-real Element of REAL
- (- (cos x)) is V21() V29() ext-real Element of REAL
(- (- (cos x))) - (- (cos (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
((- (- (cos x))) - (- (cos (x + ((2 * n) * PI))))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
(- (- (cos x))) - (- (cos x)) is V21() V29() ext-real Element of REAL
((- (- (cos x))) - (- (cos x))) - ((sin (x + (((2 * n) + 1) * PI))) - (sin (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
- (sin x) is V21() V29() ext-real Element of REAL
(- (sin x)) - (sin (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
((- (- (cos x))) - (- (cos x))) - ((- (sin x)) - (sin (x + ((2 * n) * PI)))) is V21() V29() ext-real Element of REAL
(cos x) + (cos x) is V21() V29() ext-real Element of REAL
(- (sin x)) - (sin x) is V21() V29() ext-real Element of REAL
((cos x) + (cos x)) - ((- (sin x)) - (sin x)) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
(- cos) . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(- cos) . (lower_bound A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
x (#) sin is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
integral ((x (#) sin),A) is V21() V29() ext-real Element of REAL
(x (#) sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((x (#) sin) || A) is V21() V29() ext-real Element of REAL
x * ((- cos) . (upper_bound A)) is V21() V29() ext-real Element of REAL
x * ((- cos) . (lower_bound A)) is V21() V29() ext-real Element of REAL
(x * ((- cos) . (upper_bound A))) - (x * ((- cos) . (lower_bound A))) is V21() V29() ext-real Element of REAL
sin | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
sin . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sin . (lower_bound A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
x (#) cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
integral ((x (#) cos),A) is V21() V29() ext-real Element of REAL
(x (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((x (#) cos) || A) is V21() V29() ext-real Element of REAL
x * (sin . (upper_bound A)) is V21() V29() ext-real Element of REAL
x * (sin . (lower_bound A)) is V21() V29() ext-real Element of REAL
(x * (sin . (upper_bound A))) - (x * (sin . (lower_bound A))) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
cos | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
cosh . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cosh . (lower_bound A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
x (#) sinh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral ((x (#) sinh),A) is V21() V29() ext-real Element of REAL
(x (#) sinh) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((x (#) sinh) || A) is V21() V29() ext-real Element of REAL
x * (cosh . (upper_bound A)) is V21() V29() ext-real Element of REAL
x * (cosh . (lower_bound A)) is V21() V29() ext-real Element of REAL
(x * (cosh . (upper_bound A))) - (x * (cosh . (lower_bound A))) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
sinh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
sinh . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
sinh . (lower_bound A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
x (#) cosh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral ((x (#) cosh),A) is V21() V29() ext-real Element of REAL
(x (#) cosh) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((x (#) cosh) || A) is V21() V29() ext-real Element of REAL
x * (sinh . (upper_bound A)) is V21() V29() ext-real Element of REAL
x * (sinh . (lower_bound A)) is V21() V29() ext-real Element of REAL
(x * (sinh . (upper_bound A))) - (x * (sinh . (lower_bound A))) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
cosh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
exp_R . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
exp_R . (lower_bound A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
x (#) exp_R is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
integral ((x (#) exp_R),A) is V21() V29() ext-real Element of REAL
(x (#) exp_R) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((x (#) exp_R) || A) is V21() V29() ext-real Element of REAL
x * (exp_R . (upper_bound A)) is V21() V29() ext-real Element of REAL
x * (exp_R . (lower_bound A)) is V21() V29() ext-real Element of REAL
(x * (exp_R . (upper_bound A))) - (x * (exp_R . (lower_bound A))) is V21() V29() ext-real Element of REAL
exp_R | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
sin (#) cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
1 / 2 is V21() V29() ext-real non negative Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin (#) cos),A) is V21() V29() ext-real Element of REAL
(sin (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . (lower_bound A) is V21() V29() ext-real Element of REAL
(cos . (lower_bound A)) * (cos . (lower_bound A)) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
cos . (upper_bound A) is V21() V29() ext-real Element of REAL
(cos . (upper_bound A)) * (cos . (upper_bound A)) is V21() V29() ext-real Element of REAL
((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
sin | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
(- sin) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
((- cos) `| REAL) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(cos `| REAL) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(- cos) . (upper_bound A) is V21() V29() ext-real Element of REAL
((- cos) . (upper_bound A)) * (cos . (upper_bound A)) is V21() V29() ext-real Element of REAL
(- cos) . (lower_bound A) is V21() V29() ext-real Element of REAL
((- cos) . (lower_bound A)) * (cos . (lower_bound A)) is V21() V29() ext-real Element of REAL
(((- cos) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A))) is V21() V29() ext-real Element of REAL
(- cos) (#) (- sin) is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (((- cos) (#) (- sin)),A) is V21() V29() ext-real Element of REAL
((- cos) (#) (- sin)) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
integral (((- cos) (#) (- sin)) || A) is V21() V29() ext-real Element of REAL
((((- cos) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral (((- cos) (#) (- sin)),A)) is V21() V29() ext-real Element of REAL
((((- cos) . (upper_bound A)) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) is V21() V29() ext-real Element of REAL
- (cos . (upper_bound A)) is V21() V29() ext-real Element of REAL
(- (cos . (upper_bound A))) * (cos . (upper_bound A)) is V21() V29() ext-real Element of REAL
((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A))) is V21() V29() ext-real Element of REAL
(((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - (((- cos) . (lower_bound A)) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) is V21() V29() ext-real Element of REAL
- (cos . (lower_bound A)) is V21() V29() ext-real Element of REAL
(- (cos . (lower_bound A))) * (cos . (lower_bound A)) is V21() V29() ext-real Element of REAL
((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - ((- (cos . (lower_bound A))) * (cos . (lower_bound A))) is V21() V29() ext-real Element of REAL
(((- (cos . (upper_bound A))) * (cos . (upper_bound A))) - ((- (cos . (lower_bound A))) * (cos . (lower_bound A)))) - (integral ((sin (#) cos),A)) is V21() V29() ext-real Element of REAL
(((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A)))) - (integral ((sin (#) cos),A)) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin (#) cos),A) is V21() V29() ext-real Element of REAL
(sin (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
(cos . 0) * (cos . 0) is V21() V29() ext-real Element of REAL
cos . (PI / 2) is V21() V29() ext-real Element of REAL
(cos . (PI / 2)) * (cos . (PI / 2)) is V21() V29() ext-real Element of REAL
((cos . 0) * (cos . 0)) - ((cos . (PI / 2)) * (cos . (PI / 2))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . (PI / 2)) * (cos . (PI / 2)))) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(cos . (0 + (2 * PI))) * (cos . 0) is V21() V29() ext-real Element of REAL
((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI / 2)) * (cos . (PI / 2))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI / 2)) * (cos . (PI / 2)))) is V21() V29() ext-real Element of REAL
1 * 1 is V21() V28() V29() V30() V31() ext-real non negative V49() V50() V51() V52() V53() V54() V88() Element of NAT
0 * 0 is empty V21() V28() V29() V30() V31() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of NAT
(1 * 1) - (0 * 0) is V21() V29() V30() ext-real non negative Element of REAL
(1 / 2) * ((1 * 1) - (0 * 0)) is V21() V29() ext-real non negative Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin (#) cos),A) is V21() V29() ext-real Element of REAL
(sin (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
(cos . 0) * (cos . 0) is V21() V29() ext-real Element of REAL
cos . PI is V21() V29() ext-real Element of REAL
(cos . PI) * (cos . PI) is V21() V29() ext-real Element of REAL
((cos . 0) * (cos . 0)) - ((cos . PI) * (cos . PI)) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . PI) * (cos . PI))) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(cos . (0 + (2 * PI))) * (cos . 0) is V21() V29() ext-real Element of REAL
((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . PI) * (cos . PI)) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . PI) * (cos . PI))) is V21() V29() ext-real Element of REAL
1 * 1 is V21() V28() V29() V30() V31() ext-real non negative V49() V50() V51() V52() V53() V54() V88() Element of NAT
(- 1) * (- 1) is V21() V29() V30() ext-real non negative Element of REAL
(1 * 1) - ((- 1) * (- 1)) is V21() V29() V30() ext-real Element of REAL
(1 / 2) * ((1 * 1) - ((- 1) * (- 1))) is V21() V29() ext-real Element of REAL
3 / 2 is V21() V29() ext-real non negative Element of REAL
PI * (3 / 2) is V21() V29() ext-real Element of REAL
[.0,(PI * (3 / 2)).] is V49() V50() V51() V91() closed Element of K19(REAL)
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin (#) cos),A) is V21() V29() ext-real Element of REAL
(sin (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
(cos . 0) * (cos . 0) is V21() V29() ext-real Element of REAL
cos . (PI * (3 / 2)) is V21() V29() ext-real Element of REAL
(cos . (PI * (3 / 2))) * (cos . (PI * (3 / 2))) is V21() V29() ext-real Element of REAL
((cos . 0) * (cos . 0)) - ((cos . (PI * (3 / 2))) * (cos . (PI * (3 / 2)))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . (PI * (3 / 2))) * (cos . (PI * (3 / 2))))) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(cos . (0 + (2 * PI))) * (cos . 0) is V21() V29() ext-real Element of REAL
((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI * (3 / 2))) * (cos . (PI * (3 / 2)))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI * (3 / 2))) * (cos . (PI * (3 / 2))))) is V21() V29() ext-real Element of REAL
1 * 1 is V21() V28() V29() V30() V31() ext-real non negative V49() V50() V51() V52() V53() V54() V88() Element of NAT
0 * 0 is empty V21() V28() V29() V30() V31() ext-real non positive non negative V49() V50() V51() V52() V53() V54() V55() V88() V91() Element of NAT
(1 * 1) - (0 * 0) is V21() V29() V30() ext-real non negative Element of REAL
(1 / 2) * ((1 * 1) - (0 * 0)) is V21() V29() ext-real non negative Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin (#) cos),A) is V21() V29() ext-real Element of REAL
(sin (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
(cos . 0) * (cos . 0) is V21() V29() ext-real Element of REAL
cos . (PI * 2) is V21() V29() ext-real Element of REAL
(cos . (PI * 2)) * (cos . (PI * 2)) is V21() V29() ext-real Element of REAL
((cos . 0) * (cos . 0)) - ((cos . (PI * 2)) * (cos . (PI * 2))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . 0) * (cos . 0)) - ((cos . (PI * 2)) * (cos . (PI * 2)))) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(cos . (0 + (2 * PI))) * (cos . 0) is V21() V29() ext-real Element of REAL
((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI * 2)) * (cos . (PI * 2))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . (0 + (2 * PI))) * (cos . 0)) - ((cos . (PI * 2)) * (cos . (PI * 2)))) is V21() V29() ext-real Element of REAL
1 * 1 is V21() V28() V29() V30() V31() ext-real non negative V49() V50() V51() V52() V53() V54() V88() Element of NAT
(1 * 1) - (1 * 1) is V21() V29() V30() ext-real Element of REAL
(1 / 2) * ((1 * 1) - (1 * 1)) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin (#) cos),A) is V21() V29() ext-real Element of REAL
(sin (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V21() V29() ext-real Element of REAL
x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * x is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * x) * PI is V21() V29() ext-real Element of REAL
(2 * x) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * x) + 1) * PI is V21() V29() ext-real Element of REAL
[.((2 * x) * PI),(((2 * x) + 1) * PI).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . ((2 * x) * PI) is V21() V29() ext-real Element of REAL
(cos . ((2 * x) * PI)) * (cos . ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
cos . (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
(cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
((cos . ((2 * x) * PI)) * (cos . ((2 * x) * PI))) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . ((2 * x) * PI)) * (cos . ((2 * x) * PI))) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI)))) is V21() V29() ext-real Element of REAL
cos 0 is V21() V29() ext-real Element of REAL
cos . 0 is V21() V29() ext-real Element of REAL
0 + ((2 * x) * PI) is V21() V29() ext-real Element of REAL
cos (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + ((2 * x) * PI)) is V21() V29() ext-real Element of REAL
(cos 0) * (cos (0 + ((2 * x) * PI))) is V21() V29() ext-real Element of REAL
((cos 0) * (cos (0 + ((2 * x) * PI)))) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos 0) * (cos (0 + ((2 * x) * PI)))) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI)))) is V21() V29() ext-real Element of REAL
(cos 0) * (cos 0) is V21() V29() ext-real Element of REAL
((cos 0) * (cos 0)) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos 0) * (cos 0)) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI)))) is V21() V29() ext-real Element of REAL
0 + (2 * PI) is V21() V29() ext-real Element of REAL
cos (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + (2 * PI)) is V21() V29() ext-real Element of REAL
(cos (0 + (2 * PI))) * (cos 0) is V21() V29() ext-real Element of REAL
((cos (0 + (2 * PI))) * (cos 0)) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos (0 + (2 * PI))) * (cos 0)) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI)))) is V21() V29() ext-real Element of REAL
1 * 1 is V21() V28() V29() V30() V31() ext-real non negative V49() V50() V51() V52() V53() V54() V88() Element of NAT
(1 * 1) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
(1 / 2) * ((1 * 1) - ((cos . (((2 * x) + 1) * PI)) * (cos . (((2 * x) + 1) * PI)))) is V21() V29() ext-real Element of REAL
- (cos 0) is V21() V29() ext-real Element of REAL
0 + (((2 * x) + 1) * PI) is V21() V29() ext-real Element of REAL
cos (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (0 + (((2 * x) + 1) * PI)) is V21() V29() ext-real Element of REAL
(- (cos 0)) * (cos (0 + (((2 * x) + 1) * PI))) is V21() V29() ext-real Element of REAL
(1 * 1) - ((- (cos 0)) * (cos (0 + (((2 * x) + 1) * PI)))) is V21() V29() ext-real Element of REAL
(1 / 2) * ((1 * 1) - ((- (cos 0)) * (cos (0 + (((2 * x) + 1) * PI))))) is V21() V29() ext-real Element of REAL
(- (cos 0)) * (- (cos 0)) is V21() V29() ext-real Element of REAL
(1 * 1) - ((- (cos 0)) * (- (cos 0))) is V21() V29() ext-real Element of REAL
(1 / 2) * ((1 * 1) - ((- (cos 0)) * (- (cos 0)))) is V21() V29() ext-real Element of REAL
(1 * 1) - ((cos 0) * (cos 0)) is V21() V29() ext-real Element of REAL
(1 / 2) * ((1 * 1) - ((cos 0) * (cos 0))) is V21() V29() ext-real Element of REAL
(1 * 1) - ((cos (0 + (2 * PI))) * (cos 0)) is V21() V29() ext-real Element of REAL
(1 / 2) * ((1 * 1) - ((cos (0 + (2 * PI))) * (cos 0))) is V21() V29() ext-real Element of REAL
(cos (0 + (2 * PI))) * (cos (0 + (2 * PI))) is V21() V29() ext-real Element of REAL
(1 * 1) - ((cos (0 + (2 * PI))) * (cos (0 + (2 * PI)))) is V21() V29() ext-real Element of REAL
(1 / 2) * ((1 * 1) - ((cos (0 + (2 * PI))) * (cos (0 + (2 * PI))))) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin (#) cos),A) is V21() V29() ext-real Element of REAL
(sin (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V21() V29() ext-real Element of REAL
x is V21() V29() ext-real Element of REAL
n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
2 * n is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
(2 * n) * PI is V21() V29() ext-real Element of REAL
x + ((2 * n) * PI) is V21() V29() ext-real Element of REAL
(2 * n) + 1 is V21() V28() V29() V30() V31() ext-real V49() V50() V51() V52() V53() V54() V88() Element of NAT
((2 * n) + 1) * PI is V21() V29() ext-real Element of REAL
x + (((2 * n) + 1) * PI) is V21() V29() ext-real Element of REAL
[.(x + ((2 * n) * PI)),(x + (((2 * n) + 1) * PI)).] is V49() V50() V51() V91() closed Element of K19(REAL)
upper_bound A is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
(cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
cos . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
(cos . (x + (((2 * n) + 1) * PI))) * (cos . (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI)))) - ((cos . (x + (((2 * n) + 1) * PI))) * (cos . (x + (((2 * n) + 1) * PI)))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos . (x + ((2 * n) * PI))) * (cos . (x + ((2 * n) * PI)))) - ((cos . (x + (((2 * n) + 1) * PI))) * (cos . (x + (((2 * n) + 1) * PI))))) is V21() V29() ext-real Element of REAL
cos x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
cos (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
cos . (x + ((2 * n) * PI)) is V21() V29() ext-real Element of REAL
(cos x) * (cos (x + ((2 * n) * PI))) is V21() V29() ext-real Element of REAL
cos (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
cos . (x + (((2 * n) + 1) * PI)) is V21() V29() ext-real Element of REAL
(cos (x + (((2 * n) + 1) * PI))) * (cos (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
((cos x) * (cos (x + ((2 * n) * PI)))) - ((cos (x + (((2 * n) + 1) * PI))) * (cos (x + (((2 * n) + 1) * PI)))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos x) * (cos (x + ((2 * n) * PI)))) - ((cos (x + (((2 * n) + 1) * PI))) * (cos (x + (((2 * n) + 1) * PI))))) is V21() V29() ext-real Element of REAL
(cos x) * (cos x) is V21() V29() ext-real Element of REAL
((cos x) * (cos x)) - ((cos (x + (((2 * n) + 1) * PI))) * (cos (x + (((2 * n) + 1) * PI)))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos x) * (cos x)) - ((cos (x + (((2 * n) + 1) * PI))) * (cos (x + (((2 * n) + 1) * PI))))) is V21() V29() ext-real Element of REAL
- (cos x) is V21() V29() ext-real Element of REAL
(- (cos x)) * (cos (x + (((2 * n) + 1) * PI))) is V21() V29() ext-real Element of REAL
((cos x) * (cos x)) - ((- (cos x)) * (cos (x + (((2 * n) + 1) * PI)))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos x) * (cos x)) - ((- (cos x)) * (cos (x + (((2 * n) + 1) * PI))))) is V21() V29() ext-real Element of REAL
(- (cos x)) * (- (cos x)) is V21() V29() ext-real Element of REAL
((cos x) * (cos x)) - ((- (cos x)) * (- (cos x))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cos x) * (cos x)) - ((- (cos x)) * (- (cos x)))) is V21() V29() ext-real Element of REAL
cos (#) cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
(cos (#) cos) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
(dom cos) /\ (dom cos) is set
dom (cos (#) cos) is set
sin (#) sin is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sin (#) sin),A) is V21() V29() ext-real Element of REAL
(sin (#) sin) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sin (#) sin) || A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cos . (lower_bound A) is V21() V29() ext-real Element of REAL
sin . (lower_bound A) is V21() V29() ext-real Element of REAL
(cos . (lower_bound A)) * (sin . (lower_bound A)) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
cos . (upper_bound A) is V21() V29() ext-real Element of REAL
sin . (upper_bound A) is V21() V29() ext-real Element of REAL
(cos . (upper_bound A)) * (sin . (upper_bound A)) is V21() V29() ext-real Element of REAL
((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A))) is V21() V29() ext-real Element of REAL
integral ((cos (#) cos),A) is V21() V29() ext-real Element of REAL
(cos (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
integral ((cos (#) cos) || A) is V21() V29() ext-real Element of REAL
(((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) + (integral ((cos (#) cos),A)) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
((cos (#) cos) || A) | A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
sin | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
dom (cos (#) cos) is set
cos | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
((- cos) `| REAL) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(sin `| REAL) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(- cos) . (upper_bound A) is V21() V29() ext-real Element of REAL
((- cos) . (upper_bound A)) * (sin . (upper_bound A)) is V21() V29() ext-real Element of REAL
(- cos) . (lower_bound A) is V21() V29() ext-real Element of REAL
((- cos) . (lower_bound A)) * (sin . (lower_bound A)) is V21() V29() ext-real Element of REAL
(((- cos) . (upper_bound A)) * (sin . (upper_bound A))) - (((- cos) . (lower_bound A)) * (sin . (lower_bound A))) is V21() V29() ext-real Element of REAL
(- cos) (#) cos is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
integral (((- cos) (#) cos),A) is V21() V29() ext-real Element of REAL
((- cos) (#) cos) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
integral (((- cos) (#) cos) || A) is V21() V29() ext-real Element of REAL
((((- cos) . (upper_bound A)) * (sin . (upper_bound A))) - (((- cos) . (lower_bound A)) * (sin . (lower_bound A)))) - (integral (((- cos) (#) cos),A)) is V21() V29() ext-real Element of REAL
- (cos . (upper_bound A)) is V21() V29() ext-real Element of REAL
(- (cos . (upper_bound A))) * (sin . (upper_bound A)) is V21() V29() ext-real Element of REAL
((- (cos . (upper_bound A))) * (sin . (upper_bound A))) - (((- cos) . (lower_bound A)) * (sin . (lower_bound A))) is V21() V29() ext-real Element of REAL
(((- (cos . (upper_bound A))) * (sin . (upper_bound A))) - (((- cos) . (lower_bound A)) * (sin . (lower_bound A)))) - (integral (((- cos) (#) cos),A)) is V21() V29() ext-real Element of REAL
- (cos . (lower_bound A)) is V21() V29() ext-real Element of REAL
(- (cos . (lower_bound A))) * (sin . (lower_bound A)) is V21() V29() ext-real Element of REAL
((- (cos . (upper_bound A))) * (sin . (upper_bound A))) - ((- (cos . (lower_bound A))) * (sin . (lower_bound A))) is V21() V29() ext-real Element of REAL
(((- (cos . (upper_bound A))) * (sin . (upper_bound A))) - ((- (cos . (lower_bound A))) * (sin . (lower_bound A)))) - (integral (((- cos) (#) cos),A)) is V21() V29() ext-real Element of REAL
- (cos (#) cos) is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
K87(1) * (cos (#) cos) is Relation-like REAL -defined V6() total complex-valued ext-real-valued real-valued set
integral ((- (cos (#) cos)),A) is V21() V29() ext-real Element of REAL
(- (cos (#) cos)) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
integral ((- (cos (#) cos)) || A) is V21() V29() ext-real Element of REAL
(((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - (integral ((- (cos (#) cos)),A)) is V21() V29() ext-real Element of REAL
(- 1) (#) ((cos (#) cos) || A) is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
integral ((- 1) (#) ((cos (#) cos) || A)) is V21() V29() ext-real Element of REAL
(((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - (integral ((- 1) (#) ((cos (#) cos) || A))) is V21() V29() ext-real Element of REAL
(- 1) * (integral ((cos (#) cos),A)) is V21() V29() ext-real Element of REAL
(((cos . (lower_bound A)) * (sin . (lower_bound A))) - ((cos . (upper_bound A)) * (sin . (upper_bound A)))) - ((- 1) * (integral ((cos (#) cos),A))) is V21() V29() ext-real Element of REAL
sinh (#) sinh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
cosh (#) cosh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sinh (#) sinh),A) is V21() V29() ext-real Element of REAL
(sinh (#) sinh) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sinh (#) sinh) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
cosh . (upper_bound A) is V21() V29() ext-real Element of REAL
sinh . (upper_bound A) is V21() V29() ext-real Element of REAL
(cosh . (upper_bound A)) * (sinh . (upper_bound A)) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cosh . (lower_bound A) is V21() V29() ext-real Element of REAL
sinh . (lower_bound A) is V21() V29() ext-real Element of REAL
(cosh . (lower_bound A)) * (sinh . (lower_bound A)) is V21() V29() ext-real Element of REAL
((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A))) is V21() V29() ext-real Element of REAL
integral ((cosh (#) cosh),A) is V21() V29() ext-real Element of REAL
(cosh (#) cosh) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
integral ((cosh (#) cosh) || A) is V21() V29() ext-real Element of REAL
(((cosh . (upper_bound A)) * (sinh . (upper_bound A))) - ((cosh . (lower_bound A)) * (sinh . (lower_bound A)))) - (integral ((cosh (#) cosh),A)) is V21() V29() ext-real Element of REAL
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
(sinh `| REAL) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(cosh `| REAL) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
sinh (#) cosh is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((sinh (#) cosh),A) is V21() V29() ext-real Element of REAL
(sinh (#) cosh) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((sinh (#) cosh) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
cosh . (upper_bound A) is V21() V29() ext-real Element of REAL
(cosh . (upper_bound A)) * (cosh . (upper_bound A)) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
cosh . (lower_bound A) is V21() V29() ext-real Element of REAL
(cosh . (lower_bound A)) * (cosh . (lower_bound A)) is V21() V29() ext-real Element of REAL
((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A))) is V21() V29() ext-real Element of REAL
(1 / 2) * (((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A)))) is V21() V29() ext-real Element of REAL
sinh | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
(cosh `| REAL) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
(((cosh . (upper_bound A)) * (cosh . (upper_bound A))) - ((cosh . (lower_bound A)) * (cosh . (lower_bound A)))) - (integral ((sinh (#) cosh),A)) is V21() V29() ext-real Element of REAL
exp_R (#) exp_R is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((exp_R (#) exp_R),A) is V21() V29() ext-real Element of REAL
(exp_R (#) exp_R) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((exp_R (#) exp_R) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
exp_R . (upper_bound A) is V21() V29() ext-real Element of REAL
(exp_R . (upper_bound A)) ^2 is V21() V29() ext-real Element of REAL
K86((exp_R . (upper_bound A)),(exp_R . (upper_bound A))) is V21() V29() ext-real set
lower_bound A is V21() V29() ext-real Element of REAL
exp_R . (lower_bound A) is V21() V29() ext-real Element of REAL
(exp_R . (lower_bound A)) ^2 is V21() V29() ext-real Element of REAL
K86((exp_R . (lower_bound A)),(exp_R . (lower_bound A))) is V21() V29() ext-real set
((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) ^2) is V21() V29() ext-real Element of REAL
(1 / 2) * (((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) ^2)) is V21() V29() ext-real Element of REAL
exp_R | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
(exp_R `| REAL) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
(exp_R . (upper_bound A)) * (exp_R . (upper_bound A)) is V21() V29() ext-real Element of REAL
(exp_R . (lower_bound A)) * (exp_R . (lower_bound A)) is V21() V29() ext-real Element of REAL
((exp_R . (upper_bound A)) * (exp_R . (upper_bound A))) - ((exp_R . (lower_bound A)) * (exp_R . (lower_bound A))) is V21() V29() ext-real Element of REAL
(((exp_R . (upper_bound A)) * (exp_R . (upper_bound A))) - ((exp_R . (lower_bound A)) * (exp_R . (lower_bound A)))) - (integral ((exp_R (#) exp_R),A)) is V21() V29() ext-real Element of REAL
((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) * (exp_R . (lower_bound A))) is V21() V29() ext-real Element of REAL
(((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) * (exp_R . (lower_bound A)))) - (integral ((exp_R (#) exp_R),A)) is V21() V29() ext-real Element of REAL
(((exp_R . (upper_bound A)) ^2) - ((exp_R . (lower_bound A)) ^2)) - (integral ((exp_R (#) exp_R),A)) is V21() V29() ext-real Element of REAL
exp_R (#) (sin + cos) is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
(exp_R (#) (sin + cos)) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
dom (sin + cos) is set
(dom sin) /\ (dom cos) is set
(dom exp_R) /\ (dom (sin + cos)) is set
dom (exp_R (#) (sin + cos)) is set
cos - sin is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
- sin is Relation-like REAL -defined V6() total complex-valued ext-real-valued real-valued set
cos + (- sin) is Relation-like REAL -defined V6() total complex-valued ext-real-valued real-valued set
exp_R (#) (cos - sin) is Relation-like REAL -defined REAL -valued V6() non empty total quasi_total complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
(exp_R (#) (cos - sin)) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
dom (cos - sin) is set
(dom exp_R) /\ (dom (cos - sin)) is set
dom (exp_R (#) (cos - sin)) is set
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((exp_R (#) (sin + cos)),A) is V21() V29() ext-real Element of REAL
(exp_R (#) (sin + cos)) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((exp_R (#) (sin + cos)) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
(exp_R (#) sin) . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(exp_R (#) sin) . (lower_bound A) is V21() V29() ext-real Element of REAL
((exp_R (#) sin) . (upper_bound A)) - ((exp_R (#) sin) . (lower_bound A)) is V21() V29() ext-real Element of REAL
dom (sin + cos) is set
dom (exp_R (#) (sin + cos)) is set
(dom exp_R) /\ (dom (sin + cos)) is set
REAL /\ (dom (sin + cos)) is V49() V50() V51() set
(exp_R (#) (sin + cos)) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
dom (exp_R (#) sin) is set
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
(exp_R (#) sin) `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ((exp_R (#) sin) `| REAL) is set
x is V21() V29() ext-real Element of REAL
((exp_R (#) sin) `| REAL) . x is V21() V29() ext-real Element of REAL
(exp_R (#) (sin + cos)) . x is V21() V29() ext-real Element of REAL
exp_R . x is V21() V29() ext-real Element of REAL
(sin + cos) . x is V21() V29() ext-real Element of REAL
(exp_R . x) * ((sin + cos) . x) is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
(sin . x) + (cos . x) is V21() V29() ext-real Element of REAL
(exp_R . x) * ((sin . x) + (cos . x)) is V21() V29() ext-real Element of REAL
A is non empty V49() V50() V51() closed_interval V88() V89() V90() V91() compact closed Element of K19(REAL)
integral ((exp_R (#) (cos - sin)),A) is V21() V29() ext-real Element of REAL
(exp_R (#) (cos - sin)) || A is Relation-like A -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(A,REAL))
K20(A,REAL) is complex-valued ext-real-valued real-valued set
K19(K20(A,REAL)) is set
integral ((exp_R (#) (cos - sin)) || A) is V21() V29() ext-real Element of REAL
upper_bound A is V21() V29() ext-real Element of REAL
(exp_R (#) cos) . (upper_bound A) is V21() V29() ext-real Element of REAL
lower_bound A is V21() V29() ext-real Element of REAL
(exp_R (#) cos) . (lower_bound A) is V21() V29() ext-real Element of REAL
((exp_R (#) cos) . (upper_bound A)) - ((exp_R (#) cos) . (lower_bound A)) is V21() V29() ext-real Element of REAL
dom (exp_R (#) cos) is set
[#] REAL is V49() V50() V51() closed open Element of K19(REAL)
dom (cos - sin) is set
(exp_R (#) cos) `| REAL is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued Element of K19(K20(REAL,REAL))
dom ((exp_R (#) cos) `| REAL) is set
x is V21() V29() ext-real Element of REAL
((exp_R (#) cos) `| REAL) . x is V21() V29() ext-real Element of REAL
(exp_R (#) (cos - sin)) . x is V21() V29() ext-real Element of REAL
exp_R . x is V21() V29() ext-real Element of REAL
(cos - sin) . x is V21() V29() ext-real Element of REAL
(exp_R . x) * ((cos - sin) . x) is V21() V29() ext-real Element of REAL
cos . x is V21() V29() ext-real Element of REAL
sin . x is V21() V29() ext-real Element of REAL
(cos . x) - (sin . x) is V21() V29() ext-real Element of REAL
(exp_R . x) * ((cos . x) - (sin . x)) is V21() V29() ext-real Element of REAL
(exp_R (#) (cos - sin)) | A is Relation-like REAL -defined REAL -valued V6() complex-valued ext-real-valued real-valued continuous Element of K19(K20(REAL,REAL))
dom (exp_R (#) (cos - sin)) is set
(dom exp_R) /\ (dom (cos - sin)) is set
REAL /\ (dom (cos - sin)) is V49() V50() V51() set