:: INTEGRA9 semantic presentation

REAL is non empty V51() V52() V53() V57() V73() set
NAT is non empty V21() V22() V23() V51() V52() V53() V54() V55() V56() V57() Element of K19(REAL)
K19(REAL) is set
COMPLEX is non empty V51() V57() V73() set
K20(NAT,REAL) is V34() V35() V36() set
K19(K20(NAT,REAL)) is set
K20(NAT,COMPLEX) is V34() set
K19(K20(NAT,COMPLEX)) is set
K20(COMPLEX,COMPLEX) is V34() set
K19(K20(COMPLEX,COMPLEX)) is set
K20(REAL,REAL) is V34() V35() V36() set
K19(K20(REAL,REAL)) is set
PFuncs (REAL,REAL) is set
K20(NAT,(PFuncs (REAL,REAL))) is set
K19(K20(NAT,(PFuncs (REAL,REAL)))) is set
ExtREAL is non empty V52() set
RAT is non empty V51() V52() V53() V54() V57() V73() set
INT is non empty V51() V52() V53() V54() V55() V57() V73() set
NAT is non empty V21() V22() V23() V51() V52() V53() V54() V55() V56() V57() set
K19(NAT) is set
K19(NAT) is set
K20(COMPLEX,REAL) is V34() V35() V36() set
K19(K20(COMPLEX,REAL)) is set
{} is empty V21() V22() V23() V25() V26() V27() V29() V30() non negative V51() V52() V53() V54() V55() V56() V57() set
1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
{{},1} is non empty V51() V52() V53() V54() V55() V56() set
0 is empty V21() V22() V23() V25() V26() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() V57() Element of NAT
{0} is non empty V51() V52() V53() V54() V55() V56() set
2 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
PI is V28() V29() ext-real Element of REAL
sin is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
- sin is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) is V28() V29() V30() set
K98(1) (#) sin is V1() V4( REAL ) V6() total V34() V35() V36() set
cos is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
- cos is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) cos is V1() V4( REAL ) V6() total V34() V35() V36() set
sin (#) cos is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / 2 is V28() V29() ext-real Element of REAL
[.0,PI.] is V51() V52() V53() closed Element of K19(REAL)
PI * 2 is V28() V29() ext-real Element of REAL
[.0,(PI * 2).] is V51() V52() V53() closed Element of K19(REAL)
dom sin is V51() V52() V53() Element of K19(REAL)
dom cos is V51() V52() V53() Element of K19(REAL)
cos . 0 is V28() V29() ext-real Element of REAL
sin . 0 is V28() V29() ext-real Element of REAL
cos 0 is V28() V29() ext-real Element of REAL
sin 0 is V28() V29() ext-real Element of REAL
exp_R is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
ln is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- 1 is V28() V29() V30() ext-real Element of REAL
3 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
3 / 2 is V28() V29() ext-real Element of REAL
#R (3 / 2) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
2 / 3 is V28() V29() ext-real Element of REAL
- (2 / 3) is V28() V29() ext-real Element of REAL
#R (1 / 2) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (1 / 2) is V28() V29() ext-real Element of REAL
- 2 is V28() V29() V30() ext-real Element of REAL
[#] REAL is V51() V52() V53() closed open Element of K19(REAL)
dom exp_R is V51() V52() V53() Element of K19(REAL)
rng exp_R is V51() V52() V53() Element of K19(REAL)
K231(0) is V51() V52() V53() open Element of K19(REAL)
{0} is non empty V51() V52() V53() V54() V55() V56() Element of K19(REAL)
K48(ln) is set
sec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
cos ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom sec is V51() V52() V53() Element of K19(REAL)
AffineMap ((- 1),0) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
exp_R * (AffineMap ((- 1),0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
- (exp_R * (AffineMap ((- 1),0))) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (exp_R * (AffineMap ((- 1),0))) is V1() V4( REAL ) V6() total V34() V35() V36() set
dom (- (exp_R * (AffineMap ((- 1),0)))) is V51() V52() V53() Element of K19(REAL)
(- (exp_R * (AffineMap ((- 1),0)))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (exp_R * (AffineMap ((- 1),0))) is V51() V52() V53() Element of K19(REAL)
dom (AffineMap ((- 1),0)) is V51() V52() V53() Element of K19(REAL)
A is V28() V29() ext-real Element of REAL
(AffineMap ((- 1),0)) . A is V28() V29() ext-real Element of REAL
(- 1) * A is V28() V29() ext-real Element of REAL
((- 1) * A) + 0 is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . A is V28() V29() ext-real Element of REAL
- A is V28() V29() ext-real Element of REAL
exp_R (- A) is V28() V29() ext-real Element of REAL
exp_R . (- A) is V28() V29() ext-real Element of REAL
diff ((exp_R * (AffineMap ((- 1),0))),A) is V28() V29() ext-real Element of REAL
(- 1) * (diff ((exp_R * (AffineMap ((- 1),0))),A)) is V28() V29() ext-real Element of REAL
(AffineMap ((- 1),0)) . A is V28() V29() ext-real Element of REAL
exp_R . ((AffineMap ((- 1),0)) . A) is V28() V29() ext-real Element of REAL
diff ((AffineMap ((- 1),0)),A) is V28() V29() ext-real Element of REAL
(exp_R . ((AffineMap ((- 1),0)) . A)) * (diff ((AffineMap ((- 1),0)),A)) is V28() V29() ext-real Element of REAL
(- 1) * ((exp_R . ((AffineMap ((- 1),0)) . A)) * (diff ((AffineMap ((- 1),0)),A))) is V28() V29() ext-real Element of REAL
(AffineMap ((- 1),0)) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((AffineMap ((- 1),0)) `| REAL) . A is V28() V29() ext-real Element of REAL
(exp_R . ((AffineMap ((- 1),0)) . A)) * (((AffineMap ((- 1),0)) `| REAL) . A) is V28() V29() ext-real Element of REAL
(- 1) * ((exp_R . ((AffineMap ((- 1),0)) . A)) * (((AffineMap ((- 1),0)) `| REAL) . A)) is V28() V29() ext-real Element of REAL
(exp_R . ((AffineMap ((- 1),0)) . A)) * (- 1) is V28() V29() ext-real Element of REAL
(- 1) * ((exp_R . ((AffineMap ((- 1),0)) . A)) * (- 1)) is V28() V29() ext-real Element of REAL
(- 1) * A is V28() V29() ext-real Element of REAL
((- 1) * A) + 0 is V28() V29() ext-real Element of REAL
exp_R . (((- 1) * A) + 0) is V28() V29() ext-real Element of REAL
(exp_R . (((- 1) * A) + 0)) * (- 1) is V28() V29() ext-real Element of REAL
(- 1) * ((exp_R . (((- 1) * A) + 0)) * (- 1)) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
((- (exp_R * (AffineMap ((- 1),0)))) `| REAL) . A is V28() V29() ext-real Element of REAL
- A is V28() V29() ext-real Element of REAL
exp_R (- A) is V28() V29() ext-real Element of REAL
exp_R . (- A) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
AffineMap (A,0) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
exp_R * (AffineMap (A,0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / A is V28() V29() ext-real Element of REAL
(1 / A) (#) (exp_R * (AffineMap (A,0))) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
((1 / A) (#) (exp_R * (AffineMap (A,0)))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (exp_R * (AffineMap (A,0))) is V51() V52() V53() Element of K19(REAL)
dom (AffineMap (A,0)) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) . f is V28() V29() ext-real Element of REAL
A * f is V28() V29() ext-real Element of REAL
(A * f) + 0 is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
dom ((1 / A) (#) (exp_R * (AffineMap (A,0)))) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(((1 / A) (#) (exp_R * (AffineMap (A,0)))) `| REAL) . f is V28() V29() ext-real Element of REAL
(exp_R * (AffineMap (A,0))) . f is V28() V29() ext-real Element of REAL
diff ((exp_R * (AffineMap (A,0))),f) is V28() V29() ext-real Element of REAL
(1 / A) * (diff ((exp_R * (AffineMap (A,0))),f)) is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) . f is V28() V29() ext-real Element of REAL
exp_R . ((AffineMap (A,0)) . f) is V28() V29() ext-real Element of REAL
diff ((AffineMap (A,0)),f) is V28() V29() ext-real Element of REAL
(exp_R . ((AffineMap (A,0)) . f)) * (diff ((AffineMap (A,0)),f)) is V28() V29() ext-real Element of REAL
(1 / A) * ((exp_R . ((AffineMap (A,0)) . f)) * (diff ((AffineMap (A,0)),f))) is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((AffineMap (A,0)) `| REAL) . f is V28() V29() ext-real Element of REAL
(exp_R . ((AffineMap (A,0)) . f)) * (((AffineMap (A,0)) `| REAL) . f) is V28() V29() ext-real Element of REAL
(1 / A) * ((exp_R . ((AffineMap (A,0)) . f)) * (((AffineMap (A,0)) `| REAL) . f)) is V28() V29() ext-real Element of REAL
(exp_R . ((AffineMap (A,0)) . f)) * A is V28() V29() ext-real Element of REAL
(1 / A) * ((exp_R . ((AffineMap (A,0)) . f)) * A) is V28() V29() ext-real Element of REAL
A * (1 / A) is V28() V29() ext-real Element of REAL
(A * (1 / A)) * (exp_R . ((AffineMap (A,0)) . f)) is V28() V29() ext-real Element of REAL
A / A is V28() V29() ext-real Element of REAL
(A / A) * (exp_R . ((AffineMap (A,0)) . f)) is V28() V29() ext-real Element of REAL
1 * (exp_R . ((AffineMap (A,0)) . f)) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((1 / A) (#) (exp_R * (AffineMap (A,0)))) `| REAL) . f is V28() V29() ext-real Element of REAL
(exp_R * (AffineMap (A,0))) . f is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
AffineMap (A,0) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
exp_R * (AffineMap (A,0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / A is V28() V29() ext-real Element of REAL
(1 / A) (#) (exp_R * (AffineMap (A,0))) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
integral ((exp_R * (AffineMap (A,0))),f) is V28() V29() ext-real Element of REAL
(exp_R * (AffineMap (A,0))) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral ((exp_R * (AffineMap (A,0))) || f) is V28() V29() ext-real Element of REAL
upper_bound f is V28() V29() ext-real Element of REAL
((1 / A) (#) (exp_R * (AffineMap (A,0)))) . (upper_bound f) is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
((1 / A) (#) (exp_R * (AffineMap (A,0)))) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((1 / A) (#) (exp_R * (AffineMap (A,0)))) . (upper_bound f)) - (((1 / A) (#) (exp_R * (AffineMap (A,0)))) . (lower_bound f)) is V28() V29() ext-real Element of REAL
dom (exp_R * (AffineMap (A,0))) is V51() V52() V53() Element of K19(REAL)
(AffineMap (A,0)) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
((1 / A) (#) (exp_R * (AffineMap (A,0)))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((1 / A) (#) (exp_R * (AffineMap (A,0)))) `| REAL) is V51() V52() V53() Element of K19(REAL)
exp_R | REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(AffineMap (A,0)) .: f is V51() V52() V53() Element of K19(REAL)
exp_R | ((AffineMap (A,0)) .: f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(exp_R * (AffineMap (A,0))) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V28() V29() ext-real Element of REAL
(((1 / A) (#) (exp_R * (AffineMap (A,0)))) `| REAL) . Z is V28() V29() ext-real Element of REAL
(exp_R * (AffineMap (A,0))) . Z is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
AffineMap (A,0) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
cos * (AffineMap (A,0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / A is V28() V29() ext-real Element of REAL
- (1 / A) is V28() V29() ext-real Element of REAL
(- (1 / A)) (#) (cos * (AffineMap (A,0))) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
((- (1 / A)) (#) (cos * (AffineMap (A,0)))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (1 / A)) (#) (cos * (AffineMap (A,0)))) is V51() V52() V53() Element of K19(REAL)
dom (cos * (AffineMap (A,0))) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) . f is V28() V29() ext-real Element of REAL
A * f is V28() V29() ext-real Element of REAL
(A * f) + 0 is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((- (1 / A)) (#) (cos * (AffineMap (A,0)))) `| REAL) . f is V28() V29() ext-real Element of REAL
A * f is V28() V29() ext-real Element of REAL
sin (A * f) is V28() V29() ext-real Element of REAL
sin . (A * f) is V28() V29() ext-real Element of REAL
diff ((cos * (AffineMap (A,0))),f) is V28() V29() ext-real Element of REAL
(- (1 / A)) * (diff ((cos * (AffineMap (A,0))),f)) is V28() V29() ext-real Element of REAL
(cos * (AffineMap (A,0))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((cos * (AffineMap (A,0))) `| REAL) . f is V28() V29() ext-real Element of REAL
(- (1 / A)) * (((cos * (AffineMap (A,0))) `| REAL) . f) is V28() V29() ext-real Element of REAL
(A * f) + 0 is V28() V29() ext-real Element of REAL
sin . ((A * f) + 0) is V28() V29() ext-real Element of REAL
A * (sin . ((A * f) + 0)) is V28() V29() ext-real Element of REAL
- (A * (sin . ((A * f) + 0))) is V28() V29() ext-real Element of REAL
(- (1 / A)) * (- (A * (sin . ((A * f) + 0)))) is V28() V29() ext-real Element of REAL
(1 / A) * A is V28() V29() ext-real Element of REAL
((1 / A) * A) * (sin . ((A * f) + 0)) is V28() V29() ext-real Element of REAL
A / A is V28() V29() ext-real Element of REAL
(A / A) * (sin . ((A * f) + 0)) is V28() V29() ext-real Element of REAL
1 * (sin . ((A * f) + 0)) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((- (1 / A)) (#) (cos * (AffineMap (A,0)))) `| REAL) . f is V28() V29() ext-real Element of REAL
A * f is V28() V29() ext-real Element of REAL
sin (A * f) is V28() V29() ext-real Element of REAL
sin . (A * f) is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
AffineMap (A,0) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin * (AffineMap (A,0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
cos * (AffineMap (A,0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / A is V28() V29() ext-real Element of REAL
- (1 / A) is V28() V29() ext-real Element of REAL
(- (1 / A)) (#) (cos * (AffineMap (A,0))) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
integral ((sin * (AffineMap (A,0))),f) is V28() V29() ext-real Element of REAL
(sin * (AffineMap (A,0))) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral ((sin * (AffineMap (A,0))) || f) is V28() V29() ext-real Element of REAL
upper_bound f is V28() V29() ext-real Element of REAL
((- (1 / A)) (#) (cos * (AffineMap (A,0)))) . (upper_bound f) is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
((- (1 / A)) (#) (cos * (AffineMap (A,0)))) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((- (1 / A)) (#) (cos * (AffineMap (A,0)))) . (upper_bound f)) - (((- (1 / A)) (#) (cos * (AffineMap (A,0)))) . (lower_bound f)) is V28() V29() ext-real Element of REAL
dom (sin * (AffineMap (A,0))) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) . Z is V28() V29() ext-real Element of REAL
A * Z is V28() V29() ext-real Element of REAL
(A * Z) + 0 is V28() V29() ext-real Element of REAL
((- (1 / A)) (#) (cos * (AffineMap (A,0)))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((- (1 / A)) (#) (cos * (AffineMap (A,0)))) `| REAL) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((- (1 / A)) (#) (cos * (AffineMap (A,0)))) `| REAL) . Z is V28() V29() ext-real Element of REAL
(sin * (AffineMap (A,0))) . Z is V28() V29() ext-real Element of REAL
A * Z is V28() V29() ext-real Element of REAL
sin (A * Z) is V28() V29() ext-real Element of REAL
sin . (A * Z) is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) . Z is V28() V29() ext-real Element of REAL
sin . ((AffineMap (A,0)) . Z) is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin | REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(AffineMap (A,0)) .: f is V51() V52() V53() Element of K19(REAL)
sin | ((AffineMap (A,0)) .: f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(sin * (AffineMap (A,0))) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
AffineMap (A,0) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
sin * (AffineMap (A,0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / A is V28() V29() ext-real Element of REAL
(1 / A) (#) (sin * (AffineMap (A,0))) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
((1 / A) (#) (sin * (AffineMap (A,0)))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((1 / A) (#) (sin * (AffineMap (A,0)))) is V51() V52() V53() Element of K19(REAL)
dom (sin * (AffineMap (A,0))) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) . f is V28() V29() ext-real Element of REAL
A * f is V28() V29() ext-real Element of REAL
(A * f) + 0 is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((1 / A) (#) (sin * (AffineMap (A,0)))) `| REAL) . f is V28() V29() ext-real Element of REAL
A * f is V28() V29() ext-real Element of REAL
cos (A * f) is V28() V29() ext-real Element of REAL
cos . (A * f) is V28() V29() ext-real Element of REAL
diff ((sin * (AffineMap (A,0))),f) is V28() V29() ext-real Element of REAL
(1 / A) * (diff ((sin * (AffineMap (A,0))),f)) is V28() V29() ext-real Element of REAL
(sin * (AffineMap (A,0))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((sin * (AffineMap (A,0))) `| REAL) . f is V28() V29() ext-real Element of REAL
(1 / A) * (((sin * (AffineMap (A,0))) `| REAL) . f) is V28() V29() ext-real Element of REAL
(A * f) + 0 is V28() V29() ext-real Element of REAL
cos . ((A * f) + 0) is V28() V29() ext-real Element of REAL
A * (cos . ((A * f) + 0)) is V28() V29() ext-real Element of REAL
(1 / A) * (A * (cos . ((A * f) + 0))) is V28() V29() ext-real Element of REAL
A * (1 / A) is V28() V29() ext-real Element of REAL
(A * (1 / A)) * (cos . ((A * f) + 0)) is V28() V29() ext-real Element of REAL
A / A is V28() V29() ext-real Element of REAL
(A / A) * (cos . ((A * f) + 0)) is V28() V29() ext-real Element of REAL
1 * (cos . ((A * f) + 0)) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((1 / A) (#) (sin * (AffineMap (A,0)))) `| REAL) . f is V28() V29() ext-real Element of REAL
A * f is V28() V29() ext-real Element of REAL
cos (A * f) is V28() V29() ext-real Element of REAL
cos . (A * f) is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
AffineMap (A,0) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
cos * (AffineMap (A,0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
sin * (AffineMap (A,0)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / A is V28() V29() ext-real Element of REAL
(1 / A) (#) (sin * (AffineMap (A,0))) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
integral ((cos * (AffineMap (A,0))),f) is V28() V29() ext-real Element of REAL
(cos * (AffineMap (A,0))) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral ((cos * (AffineMap (A,0))) || f) is V28() V29() ext-real Element of REAL
upper_bound f is V28() V29() ext-real Element of REAL
((1 / A) (#) (sin * (AffineMap (A,0)))) . (upper_bound f) is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
((1 / A) (#) (sin * (AffineMap (A,0)))) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((1 / A) (#) (sin * (AffineMap (A,0)))) . (upper_bound f)) - (((1 / A) (#) (sin * (AffineMap (A,0)))) . (lower_bound f)) is V28() V29() ext-real Element of REAL
dom (cos * (AffineMap (A,0))) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) . Z is V28() V29() ext-real Element of REAL
A * Z is V28() V29() ext-real Element of REAL
(A * Z) + 0 is V28() V29() ext-real Element of REAL
((1 / A) (#) (sin * (AffineMap (A,0)))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((1 / A) (#) (sin * (AffineMap (A,0)))) `| REAL) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((1 / A) (#) (sin * (AffineMap (A,0)))) `| REAL) . Z is V28() V29() ext-real Element of REAL
(cos * (AffineMap (A,0))) . Z is V28() V29() ext-real Element of REAL
A * Z is V28() V29() ext-real Element of REAL
cos (A * Z) is V28() V29() ext-real Element of REAL
cos . (A * Z) is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) . Z is V28() V29() ext-real Element of REAL
cos . ((AffineMap (A,0)) . Z) is V28() V29() ext-real Element of REAL
(AffineMap (A,0)) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
cos | REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(AffineMap (A,0)) .: f is V51() V52() V53() Element of K19(REAL)
cos | ((AffineMap (A,0)) .: f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(cos * (AffineMap (A,0))) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V51() V52() V53() open Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id f) (#) sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((id f) (#) sin),A) is V28() V29() ext-real Element of REAL
((id f) (#) sin) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (((id f) (#) sin) || A) is V28() V29() ext-real Element of REAL
- (id f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (id f) is V1() V4( REAL ) V6() V34() V35() V36() set
(- (id f)) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- (id f)) (#) cos) + sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(((- (id f)) (#) cos) + sin) . (upper_bound A) is V28() V29() ext-real Element of REAL
(((- (id f)) (#) cos) + sin) . (lower_bound A) is V28() V29() ext-real Element of REAL
((((- (id f)) (#) cos) + sin) . (upper_bound A)) - ((((- (id f)) (#) cos) + sin) . (lower_bound A)) is V28() V29() ext-real Element of REAL
dom (- (id f)) is V51() V52() V53() Element of K19(REAL)
dom (id f) is V51() V52() V53() Element of K19(REAL)
dom (((- (id f)) (#) cos) + sin) is V51() V52() V53() Element of K19(REAL)
dom ((- (id f)) (#) cos) is V51() V52() V53() Element of K19(REAL)
(dom ((- (id f)) (#) cos)) /\ REAL is V51() V52() V53() Element of K19(REAL)
(dom (- (id f))) /\ REAL is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((id f) (#) sin) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
Z * (sin . Z) is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
((id f) . Z) * (sin . Z) is V28() V29() ext-real Element of REAL
(((- (id f)) (#) cos) + sin) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((((- (id f)) (#) cos) + sin) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((((- (id f)) (#) cos) + sin) `| f) . Z is V28() V29() ext-real Element of REAL
((id f) (#) sin) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
Z * (sin . Z) is V28() V29() ext-real Element of REAL
dom ((id f) (#) sin) is V51() V52() V53() Element of K19(REAL)
(dom (id f)) /\ REAL is V51() V52() V53() Element of K19(REAL)
((id f) (#) sin) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id f) (#) sin) | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V51() V52() V53() open Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id f) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((id f) (#) cos),A) is V28() V29() ext-real Element of REAL
((id f) (#) cos) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (((id f) (#) cos) || A) is V28() V29() ext-real Element of REAL
(id f) (#) sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id f) (#) sin) + cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(((id f) (#) sin) + cos) . (upper_bound A) is V28() V29() ext-real Element of REAL
(((id f) (#) sin) + cos) . (lower_bound A) is V28() V29() ext-real Element of REAL
((((id f) (#) sin) + cos) . (upper_bound A)) - ((((id f) (#) sin) + cos) . (lower_bound A)) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
1 * Z is V28() V29() ext-real Element of REAL
(1 * Z) + 0 is V28() V29() ext-real Element of REAL
dom (((id f) (#) sin) + cos) is V51() V52() V53() Element of K19(REAL)
dom ((id f) (#) sin) is V51() V52() V53() Element of K19(REAL)
(dom ((id f) (#) sin)) /\ REAL is V51() V52() V53() Element of K19(REAL)
dom (id f) is V51() V52() V53() Element of K19(REAL)
(dom (id f)) /\ REAL is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((id f) (#) cos) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
Z * (cos . Z) is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
((id f) . Z) * (cos . Z) is V28() V29() ext-real Element of REAL
(((id f) (#) sin) + cos) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((((id f) (#) sin) + cos) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((((id f) (#) sin) + cos) `| f) . Z is V28() V29() ext-real Element of REAL
((id f) (#) cos) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
Z * (cos . Z) is V28() V29() ext-real Element of REAL
dom ((id f) (#) cos) is V51() V52() V53() Element of K19(REAL)
(dom (id f)) /\ (dom cos) is V51() V52() V53() Element of K19(REAL)
((id f) (#) cos) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id f) (#) cos) | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is V51() V52() V53() open Element of K19(REAL)
id A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id A) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id A) (#) cos) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((id A) (#) cos) is V51() V52() V53() Element of K19(REAL)
dom (id A) is V51() V52() V53() Element of K19(REAL)
(dom (id A)) /\ REAL is V51() V52() V53() Element of K19(REAL)
(dom (id A)) /\ (dom cos) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(id A) . f is V28() V29() ext-real Element of REAL
1 * f is V28() V29() ext-real Element of REAL
(1 * f) + 0 is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(id A) . f is V28() V29() ext-real Element of REAL
1 * f is V28() V29() ext-real Element of REAL
(1 * f) + 0 is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((id A) (#) cos) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
diff ((id A),f) is V28() V29() ext-real Element of REAL
(cos . f) * (diff ((id A),f)) is V28() V29() ext-real Element of REAL
(id A) . f is V28() V29() ext-real Element of REAL
diff (cos,f) is V28() V29() ext-real Element of REAL
((id A) . f) * (diff (cos,f)) is V28() V29() ext-real Element of REAL
((cos . f) * (diff ((id A),f))) + (((id A) . f) * (diff (cos,f))) is V28() V29() ext-real Element of REAL
(id A) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id A) `| A) . f is V28() V29() ext-real Element of REAL
(cos . f) * (((id A) `| A) . f) is V28() V29() ext-real Element of REAL
((cos . f) * (((id A) `| A) . f)) + (((id A) . f) * (diff (cos,f))) is V28() V29() ext-real Element of REAL
(cos . f) * 1 is V28() V29() ext-real Element of REAL
((cos . f) * 1) + (((id A) . f) * (diff (cos,f))) is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
- (sin . f) is V28() V29() ext-real Element of REAL
((id A) . f) * (- (sin . f)) is V28() V29() ext-real Element of REAL
((cos . f) * 1) + (((id A) . f) * (- (sin . f))) is V28() V29() ext-real Element of REAL
f * (- (sin . f)) is V28() V29() ext-real Element of REAL
(cos . f) + (f * (- (sin . f))) is V28() V29() ext-real Element of REAL
f * (sin . f) is V28() V29() ext-real Element of REAL
(cos . f) - (f * (sin . f)) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((id A) (#) cos) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
f * (sin . f) is V28() V29() ext-real Element of REAL
(cos . f) - (f * (sin . f)) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
diff ((- sin),A) is V28() V29() ext-real Element of REAL
cos . A is V28() V29() ext-real Element of REAL
- (cos . A) is V28() V29() ext-real Element of REAL
diff (sin,A) is V28() V29() ext-real Element of REAL
- (diff (sin,A)) is V28() V29() ext-real Element of REAL
A is V51() V52() V53() open Element of K19(REAL)
id A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id A) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- sin) + ((id A) (#) cos) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- sin) + ((id A) (#) cos)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- sin) + ((id A) (#) cos)) is V51() V52() V53() Element of K19(REAL)
dom (- sin) is V51() V52() V53() Element of K19(REAL)
dom ((id A) (#) cos) is V51() V52() V53() Element of K19(REAL)
(dom (- sin)) /\ (dom ((id A) (#) cos)) is V51() V52() V53() Element of K19(REAL)
REAL /\ (dom ((id A) (#) cos)) is V51() V52() V53() Element of K19(REAL)
dom (id A) is V51() V52() V53() Element of K19(REAL)
(dom (id A)) /\ REAL is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(((- sin) + ((id A) (#) cos)) `| A) . f is V28() V29() ext-real Element of REAL
diff ((- sin),f) is V28() V29() ext-real Element of REAL
diff (((id A) (#) cos),f) is V28() V29() ext-real Element of REAL
(diff ((- sin),f)) + (diff (((id A) (#) cos),f)) is V28() V29() ext-real Element of REAL
((id A) (#) cos) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(((id A) (#) cos) `| A) . f is V28() V29() ext-real Element of REAL
((((id A) (#) cos) `| A) . f) + (diff ((- sin),f)) is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
f * (sin . f) is V28() V29() ext-real Element of REAL
(cos . f) - (f * (sin . f)) is V28() V29() ext-real Element of REAL
((cos . f) - (f * (sin . f))) + (diff ((- sin),f)) is V28() V29() ext-real Element of REAL
- (cos . f) is V28() V29() ext-real Element of REAL
((cos . f) - (f * (sin . f))) + (- (cos . f)) is V28() V29() ext-real Element of REAL
- (f * (sin . f)) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((- sin) + ((id A) (#) cos)) `| A) . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
f * (sin . f) is V28() V29() ext-real Element of REAL
- (f * (sin . f)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V51() V52() V53() open Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
- (id f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (id f) is V1() V4( REAL ) V6() V34() V35() V36() set
(- (id f)) (#) sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((- (id f)) (#) sin),A) is V28() V29() ext-real Element of REAL
((- (id f)) (#) sin) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (((- (id f)) (#) sin) || A) is V28() V29() ext-real Element of REAL
(id f) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- sin) + ((id f) (#) cos) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- sin) + ((id f) (#) cos)) . (upper_bound A) is V28() V29() ext-real Element of REAL
((- sin) + ((id f) (#) cos)) . (lower_bound A) is V28() V29() ext-real Element of REAL
(((- sin) + ((id f) (#) cos)) . (upper_bound A)) - (((- sin) + ((id f) (#) cos)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(- (id f)) . Z is V28() V29() ext-real Element of REAL
(- 1) * Z is V28() V29() ext-real Element of REAL
((- 1) * Z) + 0 is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
- ((id f) . Z) is V28() V29() ext-real Element of REAL
- Z is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
((- (id f)) (#) sin) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
Z * (sin . Z) is V28() V29() ext-real Element of REAL
- (Z * (sin . Z)) is V28() V29() ext-real Element of REAL
(- (id f)) . Z is V28() V29() ext-real Element of REAL
((- (id f)) . Z) * (sin . Z) is V28() V29() ext-real Element of REAL
(- 1) * Z is V28() V29() ext-real Element of REAL
((- 1) * Z) + 0 is V28() V29() ext-real Element of REAL
(((- 1) * Z) + 0) * (sin . Z) is V28() V29() ext-real Element of REAL
((- sin) + ((id f) (#) cos)) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((- sin) + ((id f) (#) cos)) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((- sin) + ((id f) (#) cos)) `| f) . Z is V28() V29() ext-real Element of REAL
((- (id f)) (#) sin) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
Z * (sin . Z) is V28() V29() ext-real Element of REAL
- (Z * (sin . Z)) is V28() V29() ext-real Element of REAL
dom ((- (id f)) (#) sin) is V51() V52() V53() Element of K19(REAL)
dom (- (id f)) is V51() V52() V53() Element of K19(REAL)
(dom (- (id f))) /\ REAL is V51() V52() V53() Element of K19(REAL)
dom (id f) is V51() V52() V53() Element of K19(REAL)
(dom (- (id f))) /\ (dom sin) is V51() V52() V53() Element of K19(REAL)
((- (id f)) (#) sin) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- (id f)) (#) sin) | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is V51() V52() V53() open Element of K19(REAL)
id A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id A) (#) sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- cos) - ((id A) (#) sin) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- ((id A) (#) sin) is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) ((id A) (#) sin) is V1() V4( REAL ) V6() V34() V35() V36() set
(- cos) + (- ((id A) (#) sin)) is V1() V4( REAL ) V6() V34() V35() V36() set
((- cos) - ((id A) (#) sin)) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- cos) - ((id A) (#) sin)) is V51() V52() V53() Element of K19(REAL)
dom (- cos) is V51() V52() V53() Element of K19(REAL)
dom ((id A) (#) sin) is V51() V52() V53() Element of K19(REAL)
(dom (- cos)) /\ (dom ((id A) (#) sin)) is V51() V52() V53() Element of K19(REAL)
REAL /\ (dom ((id A) (#) sin)) is V51() V52() V53() Element of K19(REAL)
dom (id A) is V51() V52() V53() Element of K19(REAL)
(dom (id A)) /\ REAL is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(((- cos) - ((id A) (#) sin)) `| A) . f is V28() V29() ext-real Element of REAL
diff ((- cos),f) is V28() V29() ext-real Element of REAL
diff (((id A) (#) sin),f) is V28() V29() ext-real Element of REAL
(diff ((- cos),f)) - (diff (((id A) (#) sin),f)) is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) - (diff (((id A) (#) sin),f)) is V28() V29() ext-real Element of REAL
((id A) (#) sin) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(((id A) (#) sin) `| A) . f is V28() V29() ext-real Element of REAL
(sin . f) - ((((id A) (#) sin) `| A) . f) is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
f * (cos . f) is V28() V29() ext-real Element of REAL
(sin . f) + (f * (cos . f)) is V28() V29() ext-real Element of REAL
(sin . f) - ((sin . f) + (f * (cos . f))) is V28() V29() ext-real Element of REAL
- (f * (cos . f)) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((- cos) - ((id A) (#) sin)) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
f * (cos . f) is V28() V29() ext-real Element of REAL
- (f * (cos . f)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V51() V52() V53() open Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
- (id f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (id f) is V1() V4( REAL ) V6() V34() V35() V36() set
(- (id f)) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((- (id f)) (#) cos),A) is V28() V29() ext-real Element of REAL
((- (id f)) (#) cos) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (((- (id f)) (#) cos) || A) is V28() V29() ext-real Element of REAL
(id f) (#) sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- cos) - ((id f) (#) sin) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- ((id f) (#) sin) is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) ((id f) (#) sin) is V1() V4( REAL ) V6() V34() V35() V36() set
(- cos) + (- ((id f) (#) sin)) is V1() V4( REAL ) V6() V34() V35() V36() set
((- cos) - ((id f) (#) sin)) . (upper_bound A) is V28() V29() ext-real Element of REAL
((- cos) - ((id f) (#) sin)) . (lower_bound A) is V28() V29() ext-real Element of REAL
(((- cos) - ((id f) (#) sin)) . (upper_bound A)) - (((- cos) - ((id f) (#) sin)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(- (id f)) . Z is V28() V29() ext-real Element of REAL
(- 1) * Z is V28() V29() ext-real Element of REAL
((- 1) * Z) + 0 is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
- ((id f) . Z) is V28() V29() ext-real Element of REAL
- Z is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
((- (id f)) (#) cos) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
Z * (cos . Z) is V28() V29() ext-real Element of REAL
- (Z * (cos . Z)) is V28() V29() ext-real Element of REAL
(- (id f)) . Z is V28() V29() ext-real Element of REAL
((- (id f)) . Z) * (cos . Z) is V28() V29() ext-real Element of REAL
(- 1) * Z is V28() V29() ext-real Element of REAL
((- 1) * Z) + 0 is V28() V29() ext-real Element of REAL
(((- 1) * Z) + 0) * (cos . Z) is V28() V29() ext-real Element of REAL
((- cos) - ((id f) (#) sin)) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((- cos) - ((id f) (#) sin)) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((- cos) - ((id f) (#) sin)) `| f) . Z is V28() V29() ext-real Element of REAL
((- (id f)) (#) cos) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
Z * (cos . Z) is V28() V29() ext-real Element of REAL
- (Z * (cos . Z)) is V28() V29() ext-real Element of REAL
dom ((- (id f)) (#) cos) is V51() V52() V53() Element of K19(REAL)
dom (- (id f)) is V51() V52() V53() Element of K19(REAL)
(dom (- (id f))) /\ REAL is V51() V52() V53() Element of K19(REAL)
dom (id f) is V51() V52() V53() Element of K19(REAL)
(dom (- (id f))) /\ (dom cos) is V51() V52() V53() Element of K19(REAL)
((- (id f)) (#) cos) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- (id f)) (#) cos) | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V51() V52() V53() open Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id f) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sin + ((id f) (#) cos) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((sin + ((id f) (#) cos)),A) is V28() V29() ext-real Element of REAL
(sin + ((id f) (#) cos)) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral ((sin + ((id f) (#) cos)) || A) is V28() V29() ext-real Element of REAL
(id f) (#) sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((id f) (#) sin) . (upper_bound A) is V28() V29() ext-real Element of REAL
((id f) (#) sin) . (lower_bound A) is V28() V29() ext-real Element of REAL
(((id f) (#) sin) . (upper_bound A)) - (((id f) (#) sin) . (lower_bound A)) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
1 * Z is V28() V29() ext-real Element of REAL
(1 * Z) + 0 is V28() V29() ext-real Element of REAL
dom (sin + ((id f) (#) cos)) is V51() V52() V53() Element of K19(REAL)
dom ((id f) (#) cos) is V51() V52() V53() Element of K19(REAL)
REAL /\ (dom ((id f) (#) cos)) is V51() V52() V53() Element of K19(REAL)
dom (id f) is V51() V52() V53() Element of K19(REAL)
(dom (id f)) /\ REAL is V51() V52() V53() Element of K19(REAL)
(dom sin) /\ (dom ((id f) (#) cos)) is V51() V52() V53() Element of K19(REAL)
(dom (id f)) /\ (dom cos) is V51() V52() V53() Element of K19(REAL)
(sin + ((id f) (#) cos)) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(sin + ((id f) (#) cos)) | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((id f) (#) sin) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(sin + ((id f) (#) cos)) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
Z * (cos . Z) is V28() V29() ext-real Element of REAL
(sin . Z) + (Z * (cos . Z)) is V28() V29() ext-real Element of REAL
((id f) (#) cos) . Z is V28() V29() ext-real Element of REAL
(sin . Z) + (((id f) (#) cos) . Z) is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
((id f) . Z) * (cos . Z) is V28() V29() ext-real Element of REAL
(sin . Z) + (((id f) . Z) * (cos . Z)) is V28() V29() ext-real Element of REAL
((id f) (#) sin) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id f) (#) sin) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((id f) (#) sin) `| f) . Z is V28() V29() ext-real Element of REAL
(sin + ((id f) (#) cos)) . Z is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
Z * (cos . Z) is V28() V29() ext-real Element of REAL
(sin . Z) + (Z * (cos . Z)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V51() V52() V53() open Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id f) (#) sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- cos) + ((id f) (#) sin) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((- cos) + ((id f) (#) sin)),A) is V28() V29() ext-real Element of REAL
((- cos) + ((id f) (#) sin)) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (((- cos) + ((id f) (#) sin)) || A) is V28() V29() ext-real Element of REAL
- (id f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (id f) is V1() V4( REAL ) V6() V34() V35() V36() set
(- (id f)) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- (id f)) (#) cos) . (upper_bound A) is V28() V29() ext-real Element of REAL
((- (id f)) (#) cos) . (lower_bound A) is V28() V29() ext-real Element of REAL
(((- (id f)) (#) cos) . (upper_bound A)) - (((- (id f)) (#) cos) . (lower_bound A)) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
1 * Z is V28() V29() ext-real Element of REAL
(1 * Z) + 0 is V28() V29() ext-real Element of REAL
dom ((- cos) + ((id f) (#) sin)) is V51() V52() V53() Element of K19(REAL)
dom (- cos) is V51() V52() V53() Element of K19(REAL)
dom ((id f) (#) sin) is V51() V52() V53() Element of K19(REAL)
(dom (- cos)) /\ (dom ((id f) (#) sin)) is V51() V52() V53() Element of K19(REAL)
REAL /\ (dom ((id f) (#) sin)) is V51() V52() V53() Element of K19(REAL)
dom (id f) is V51() V52() V53() Element of K19(REAL)
(dom (id f)) /\ REAL is V51() V52() V53() Element of K19(REAL)
(dom (id f)) /\ (dom sin) is V51() V52() V53() Element of K19(REAL)
((- cos) + ((id f) (#) sin)) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- cos) + ((id f) (#) sin)) | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (id f)) (#) cos) is V51() V52() V53() Element of K19(REAL)
dom (- (id f)) is V51() V52() V53() Element of K19(REAL)
(dom (- (id f))) /\ REAL is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((- cos) + ((id f) (#) sin)) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
- (cos . Z) is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
Z * (sin . Z) is V28() V29() ext-real Element of REAL
(- (cos . Z)) + (Z * (sin . Z)) is V28() V29() ext-real Element of REAL
(- cos) . Z is V28() V29() ext-real Element of REAL
((id f) (#) sin) . Z is V28() V29() ext-real Element of REAL
((- cos) . Z) + (((id f) (#) sin) . Z) is V28() V29() ext-real Element of REAL
(id f) . Z is V28() V29() ext-real Element of REAL
((id f) . Z) * (sin . Z) is V28() V29() ext-real Element of REAL
((- cos) . Z) + (((id f) . Z) * (sin . Z)) is V28() V29() ext-real Element of REAL
((- cos) . Z) + (Z * (sin . Z)) is V28() V29() ext-real Element of REAL
((- (id f)) (#) cos) `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((- (id f)) (#) cos) `| f) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((- (id f)) (#) cos) `| f) . Z is V28() V29() ext-real Element of REAL
((- cos) + ((id f) (#) sin)) . Z is V28() V29() ext-real Element of REAL
cos . Z is V28() V29() ext-real Element of REAL
- (cos . Z) is V28() V29() ext-real Element of REAL
sin . Z is V28() V29() ext-real Element of REAL
Z * (sin . Z) is V28() V29() ext-real Element of REAL
(- (cos . Z)) + (Z * (sin . Z)) is V28() V29() ext-real Element of REAL
AffineMap (1,0) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
(AffineMap (1,0)) (#) exp_R is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
AffineMap (1,(- 1)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
exp_R (#) (AffineMap (1,(- 1))) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
integral (((AffineMap (1,0)) (#) exp_R),A) is V28() V29() ext-real Element of REAL
((AffineMap (1,0)) (#) exp_R) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (((AffineMap (1,0)) (#) exp_R) || A) is V28() V29() ext-real Element of REAL
upper_bound A is V28() V29() ext-real Element of REAL
(exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A) is V28() V29() ext-real Element of REAL
((exp_R (#) (AffineMap (1,(- 1)))) . (upper_bound A)) - ((exp_R (#) (AffineMap (1,(- 1)))) . (lower_bound A)) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(AffineMap (1,(- 1))) . f is V28() V29() ext-real Element of REAL
f - 1 is V28() V29() ext-real Element of REAL
1 * f is V28() V29() ext-real Element of REAL
(1 * f) + (- 1) is V28() V29() ext-real Element of REAL
dom (exp_R (#) (AffineMap (1,(- 1)))) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
((AffineMap (1,0)) (#) exp_R) . f is V28() V29() ext-real Element of REAL
exp_R . f is V28() V29() ext-real Element of REAL
f * (exp_R . f) is V28() V29() ext-real Element of REAL
(AffineMap (1,0)) . f is V28() V29() ext-real Element of REAL
((AffineMap (1,0)) . f) * (exp_R . f) is V28() V29() ext-real Element of REAL
1 * f is V28() V29() ext-real Element of REAL
(1 * f) + 0 is V28() V29() ext-real Element of REAL
((1 * f) + 0) * (exp_R . f) is V28() V29() ext-real Element of REAL
(exp_R (#) (AffineMap (1,(- 1)))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
((exp_R (#) (AffineMap (1,(- 1)))) `| REAL) . f is V28() V29() ext-real Element of REAL
((AffineMap (1,0)) (#) exp_R) . f is V28() V29() ext-real Element of REAL
exp_R . f is V28() V29() ext-real Element of REAL
f * (exp_R . f) is V28() V29() ext-real Element of REAL
dom ((AffineMap (1,0)) (#) exp_R) is V51() V52() V53() Element of K19(REAL)
dom (AffineMap (1,0)) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(AffineMap (1,0)) . f is V28() V29() ext-real Element of REAL
1 * f is V28() V29() ext-real Element of REAL
(1 * f) + 0 is V28() V29() ext-real Element of REAL
((AffineMap (1,0)) (#) exp_R) | REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((AffineMap (1,0)) (#) exp_R) | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
A + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
#Z (A + 1) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
1 / (A + 1) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) (#) (#Z (A + 1)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
((1 / (A + 1)) (#) (#Z (A + 1))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((1 / (A + 1)) (#) (#Z (A + 1))) is V51() V52() V53() Element of K19(REAL)
dom (#Z (A + 1)) is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
(#Z (A + 1)) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V28() V29() ext-real Element of REAL
((#Z (A + 1)) `| REAL) . Z is V28() V29() ext-real Element of REAL
Z #Z A is V28() V29() ext-real Element of REAL
(A + 1) * (Z #Z A) is V28() V29() ext-real Element of REAL
diff ((#Z (A + 1)),Z) is V28() V29() ext-real Element of REAL
(A + 1) - 1 is V28() V29() V30() ext-real Element of REAL
Z #Z ((A + 1) - 1) is V28() V29() ext-real Element of REAL
(A + 1) * (Z #Z ((A + 1) - 1)) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((1 / (A + 1)) (#) (#Z (A + 1))) `| REAL) . f is V28() V29() ext-real Element of REAL
f #Z A is V28() V29() ext-real Element of REAL
diff ((#Z (A + 1)),f) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * (diff ((#Z (A + 1)),f)) is V28() V29() ext-real Element of REAL
((#Z (A + 1)) `| REAL) . f is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * (((#Z (A + 1)) `| REAL) . f) is V28() V29() ext-real Element of REAL
(A + 1) * (f #Z A) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * ((A + 1) * (f #Z A)) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * (A + 1) is V28() V29() ext-real Element of REAL
((1 / (A + 1)) * (A + 1)) * (f #Z A) is V28() V29() ext-real Element of REAL
(A + 1) / (A + 1) is V28() V29() ext-real Element of REAL
((A + 1) / (A + 1)) * (f #Z A) is V28() V29() ext-real Element of REAL
1 * (f #Z A) is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
(((1 / (A + 1)) (#) (#Z (A + 1))) `| REAL) . f is V28() V29() ext-real Element of REAL
f #Z A is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
#Z A is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
A + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
1 / (A + 1) is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
integral ((#Z A),f) is V28() V29() ext-real Element of REAL
(#Z A) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral ((#Z A) || f) is V28() V29() ext-real Element of REAL
upper_bound f is V28() V29() ext-real Element of REAL
(upper_bound f) |^ (A + 1) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * ((upper_bound f) |^ (A + 1)) is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
(lower_bound f) |^ (A + 1) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * ((lower_bound f) |^ (A + 1)) is V28() V29() ext-real Element of REAL
((1 / (A + 1)) * ((upper_bound f) |^ (A + 1))) - ((1 / (A + 1)) * ((lower_bound f) |^ (A + 1))) is V28() V29() ext-real Element of REAL
dom (#Z A) is V51() V52() V53() Element of K19(REAL)
#Z (A + 1) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
(1 / (A + 1)) (#) (#Z (A + 1)) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
((1 / (A + 1)) (#) (#Z (A + 1))) `| REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((1 / (A + 1)) (#) (#Z (A + 1))) `| REAL) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((1 / (A + 1)) (#) (#Z (A + 1))) `| REAL) . Z is V28() V29() ext-real Element of REAL
(#Z A) . Z is V28() V29() ext-real Element of REAL
Z #Z A is V28() V29() ext-real Element of REAL
dom (#Z (A + 1)) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
dom ((1 / (A + 1)) (#) (#Z (A + 1))) is V51() V52() V53() Element of K19(REAL)
(#Z (A + 1)) . (upper_bound f) is V28() V29() ext-real Element of REAL
(upper_bound f) #Z (A + 1) is V28() V29() ext-real Element of REAL
Z is V28() V29() ext-real Element of REAL
(#Z A) | REAL is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(#Z A) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(#Z (A + 1)) . (lower_bound f) is V28() V29() ext-real Element of REAL
(lower_bound f) #Z (A + 1) is V28() V29() ext-real Element of REAL
((1 / (A + 1)) (#) (#Z (A + 1))) . (upper_bound f) is V28() V29() ext-real Element of REAL
((1 / (A + 1)) (#) (#Z (A + 1))) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((1 / (A + 1)) (#) (#Z (A + 1))) . (upper_bound f)) - (((1 / (A + 1)) (#) (#Z (A + 1))) . (lower_bound f)) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * ((#Z (A + 1)) . (upper_bound f)) is V28() V29() ext-real Element of REAL
((1 / (A + 1)) * ((#Z (A + 1)) . (upper_bound f))) - (((1 / (A + 1)) (#) (#Z (A + 1))) . (lower_bound f)) is V28() V29() ext-real Element of REAL
(1 / (A + 1)) * ((#Z (A + 1)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
((1 / (A + 1)) * ((#Z (A + 1)) . (upper_bound f))) - ((1 / (A + 1)) * ((#Z (A + 1)) . (lower_bound f))) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A - f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) f is V1() V4( REAL ) V6() V34() V35() V36() set
A + (- f) is V1() V4( REAL ) V6() V34() V35() V36() set
Z is non empty V51() V52() V53() Element of K19(REAL)
(A - f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
A || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
f || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(A || Z) - (f || Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
- (f || Z) is V1() V4(Z) V6() V34() V35() V36() set
K98(1) (#) (f || Z) is V1() V4(Z) V6() V34() V35() V36() set
(A || Z) + (- (f || Z)) is V1() V4(Z) V6() V34() V35() V36() set
dom ((A || Z) - (f || Z)) is V51() V52() V53() Element of K19(Z)
K19(Z) is set
A | Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (A | Z) is V51() V52() V53() Element of K19(REAL)
f | Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (f | Z) is V51() V52() V53() Element of K19(REAL)
(dom (A | Z)) /\ (dom (f | Z)) is V51() V52() V53() Element of K19(REAL)
dom A is V51() V52() V53() Element of K19(REAL)
(dom A) /\ Z is V51() V52() V53() Element of K19(REAL)
((dom A) /\ Z) /\ (dom (f | Z)) is V51() V52() V53() Element of K19(REAL)
dom f is V51() V52() V53() Element of K19(REAL)
(dom f) /\ Z is V51() V52() V53() Element of K19(REAL)
((dom A) /\ Z) /\ ((dom f) /\ Z) is V51() V52() V53() Element of K19(REAL)
Z /\ ((dom f) /\ Z) is V51() V52() V53() Element of K19(REAL)
(dom A) /\ (Z /\ ((dom f) /\ Z)) is V51() V52() V53() Element of K19(REAL)
Z /\ Z is V51() V52() V53() Element of K19(REAL)
(dom f) /\ (Z /\ Z) is V51() V52() V53() Element of K19(REAL)
(dom A) /\ ((dom f) /\ (Z /\ Z)) is V51() V52() V53() Element of K19(REAL)
(dom A) /\ ((dom f) /\ Z) is V51() V52() V53() Element of K19(REAL)
dom ((A - f) || Z) is V51() V52() V53() Element of K19(Z)
dom (A - f) is V51() V52() V53() Element of K19(REAL)
(dom (A - f)) /\ Z is V51() V52() V53() Element of K19(REAL)
(dom A) /\ (dom f) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ Z is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of Z
((A - f) || Z) . x is V28() V29() ext-real Element of REAL
((A || Z) - (f || Z)) . x is V28() V29() ext-real Element of REAL
dom (A || Z) is V51() V52() V53() Element of K19(Z)
dom (f || Z) is V51() V52() V53() Element of K19(Z)
(dom (A || Z)) /\ (dom (f || Z)) is V51() V52() V53() Element of K19(Z)
(A - f) . x is V28() V29() ext-real Element of REAL
A . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
(A . x) - (f . x) is V28() V29() ext-real Element of REAL
(A || Z) . x is V28() V29() ext-real Element of REAL
(f || Z) . x is V28() V29() ext-real Element of REAL
((A || Z) . x) - ((f || Z) . x) is V28() V29() ext-real Element of REAL
(f | Z) . x is V28() V29() ext-real Element of REAL
(A . x) - ((f | Z) . x) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A + f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(A (#) Z) + (f (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is non empty V51() V52() V53() Element of K19(REAL)
(A + f) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
K20(x,REAL) is V34() V35() V36() set
K19(K20(x,REAL)) is set
Z || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A + f) || x) (#) (Z || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A (#) Z) + (f (#) Z)) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
dom (((A (#) Z) + (f (#) Z)) || x) is V51() V52() V53() Element of K19(x)
K19(x) is set
dom ((A (#) Z) + (f (#) Z)) is V51() V52() V53() Element of K19(REAL)
(dom ((A (#) Z) + (f (#) Z))) /\ x is V51() V52() V53() Element of K19(REAL)
dom (A (#) Z) is V51() V52() V53() Element of K19(REAL)
dom (f (#) Z) is V51() V52() V53() Element of K19(REAL)
(dom (A (#) Z)) /\ (dom (f (#) Z)) is V51() V52() V53() Element of K19(REAL)
((dom (A (#) Z)) /\ (dom (f (#) Z))) /\ x is V51() V52() V53() Element of K19(REAL)
dom A is V51() V52() V53() Element of K19(REAL)
dom Z is V51() V52() V53() Element of K19(REAL)
(dom A) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom Z)) /\ (dom (f (#) Z)) is V51() V52() V53() Element of K19(REAL)
(((dom A) /\ (dom Z)) /\ (dom (f (#) Z))) /\ x is V51() V52() V53() Element of K19(REAL)
dom f is V51() V52() V53() Element of K19(REAL)
(dom f) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom Z)) /\ ((dom f) /\ (dom Z)) is V51() V52() V53() Element of K19(REAL)
(((dom A) /\ (dom Z)) /\ ((dom f) /\ (dom Z))) /\ x is V51() V52() V53() Element of K19(REAL)
(dom Z) /\ (dom f) is V51() V52() V53() Element of K19(REAL)
((dom Z) /\ (dom f)) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
(dom A) /\ (((dom Z) /\ (dom f)) /\ (dom Z)) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (((dom Z) /\ (dom f)) /\ (dom Z))) /\ x is V51() V52() V53() Element of K19(REAL)
(dom Z) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
(dom f) /\ ((dom Z) /\ (dom Z)) is V51() V52() V53() Element of K19(REAL)
(dom A) /\ ((dom f) /\ ((dom Z) /\ (dom Z))) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ ((dom f) /\ ((dom Z) /\ (dom Z)))) /\ x is V51() V52() V53() Element of K19(REAL)
(dom A) /\ (dom f) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
(((dom A) /\ (dom f)) /\ (dom Z)) /\ x is V51() V52() V53() Element of K19(REAL)
dom (((A + f) || x) (#) (Z || x)) is V51() V52() V53() Element of K19(x)
dom ((A + f) || x) is V51() V52() V53() Element of K19(x)
dom (Z || x) is V51() V52() V53() Element of K19(x)
(dom ((A + f) || x)) /\ (dom (Z || x)) is V51() V52() V53() Element of K19(x)
dom (A + f) is V51() V52() V53() Element of K19(REAL)
(dom (A + f)) /\ x is V51() V52() V53() Element of K19(REAL)
Z | x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (Z | x) is V51() V52() V53() Element of K19(REAL)
((dom (A + f)) /\ x) /\ (dom (Z | x)) is V51() V52() V53() Element of K19(REAL)
(dom Z) /\ x is V51() V52() V53() Element of K19(REAL)
((dom (A + f)) /\ x) /\ ((dom Z) /\ x) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ x is V51() V52() V53() Element of K19(REAL)
(((dom A) /\ (dom f)) /\ x) /\ ((dom Z) /\ x) is V51() V52() V53() Element of K19(REAL)
x /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
(x /\ (dom Z)) /\ x is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ ((x /\ (dom Z)) /\ x) is V51() V52() V53() Element of K19(REAL)
x /\ x is V51() V52() V53() Element of K19(REAL)
(dom Z) /\ (x /\ x) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ ((dom Z) /\ (x /\ x)) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of x
(((A + f) || x) (#) (Z || x)) . Z is V28() V29() ext-real Element of REAL
(((A (#) Z) + (f (#) Z)) || x) . Z is V28() V29() ext-real Element of REAL
(A + f) | x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((A + f) | x) is V51() V52() V53() Element of K19(REAL)
((A + f) || x) . Z is V28() V29() ext-real Element of REAL
(Z || x) . Z is V28() V29() ext-real Element of REAL
(((A + f) || x) . Z) * ((Z || x) . Z) is V28() V29() ext-real Element of REAL
(A + f) . Z is V28() V29() ext-real Element of REAL
(Z | x) . Z is V28() V29() ext-real Element of REAL
((A + f) . Z) * ((Z | x) . Z) is V28() V29() ext-real Element of REAL
A . Z is V28() V29() ext-real Element of REAL
f . Z is V28() V29() ext-real Element of REAL
(A . Z) + (f . Z) is V28() V29() ext-real Element of REAL
((A . Z) + (f . Z)) * ((Z | x) . Z) is V28() V29() ext-real Element of REAL
((A (#) Z) + (f (#) Z)) . Z is V28() V29() ext-real Element of REAL
(A (#) Z) . Z is V28() V29() ext-real Element of REAL
(f (#) Z) . Z is V28() V29() ext-real Element of REAL
((A (#) Z) . Z) + ((f (#) Z) . Z) is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
(A . Z) * (Z . Z) is V28() V29() ext-real Element of REAL
((A . Z) * (Z . Z)) + ((f (#) Z) . Z) is V28() V29() ext-real Element of REAL
(f . Z) * (Z . Z) is V28() V29() ext-real Element of REAL
((A . Z) * (Z . Z)) + ((f . Z) * (Z . Z)) is V28() V29() ext-real Element of REAL
((A . Z) + (f . Z)) * (Z . Z) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A - f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) f is V1() V4( REAL ) V6() V34() V35() V36() set
A + (- f) is V1() V4( REAL ) V6() V34() V35() V36() set
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(A (#) Z) - (f (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (f (#) Z) is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) (f (#) Z) is V1() V4( REAL ) V6() V34() V35() V36() set
(A (#) Z) + (- (f (#) Z)) is V1() V4( REAL ) V6() V34() V35() V36() set
x is non empty V51() V52() V53() Element of K19(REAL)
(A - f) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
K20(x,REAL) is V34() V35() V36() set
K19(K20(x,REAL)) is set
Z || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A - f) || x) (#) (Z || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A (#) Z) - (f (#) Z)) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
dom (((A (#) Z) - (f (#) Z)) || x) is V51() V52() V53() Element of K19(x)
K19(x) is set
dom ((A (#) Z) - (f (#) Z)) is V51() V52() V53() Element of K19(REAL)
(dom ((A (#) Z) - (f (#) Z))) /\ x is V51() V52() V53() Element of K19(REAL)
dom (A (#) Z) is V51() V52() V53() Element of K19(REAL)
dom (f (#) Z) is V51() V52() V53() Element of K19(REAL)
(dom (A (#) Z)) /\ (dom (f (#) Z)) is V51() V52() V53() Element of K19(REAL)
((dom (A (#) Z)) /\ (dom (f (#) Z))) /\ x is V51() V52() V53() Element of K19(REAL)
dom A is V51() V52() V53() Element of K19(REAL)
dom Z is V51() V52() V53() Element of K19(REAL)
(dom A) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom Z)) /\ (dom (f (#) Z)) is V51() V52() V53() Element of K19(REAL)
(((dom A) /\ (dom Z)) /\ (dom (f (#) Z))) /\ x is V51() V52() V53() Element of K19(REAL)
dom f is V51() V52() V53() Element of K19(REAL)
(dom f) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom Z)) /\ ((dom f) /\ (dom Z)) is V51() V52() V53() Element of K19(REAL)
(((dom A) /\ (dom Z)) /\ ((dom f) /\ (dom Z))) /\ x is V51() V52() V53() Element of K19(REAL)
(dom Z) /\ (dom f) is V51() V52() V53() Element of K19(REAL)
((dom Z) /\ (dom f)) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
(dom A) /\ (((dom Z) /\ (dom f)) /\ (dom Z)) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (((dom Z) /\ (dom f)) /\ (dom Z))) /\ x is V51() V52() V53() Element of K19(REAL)
(dom Z) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
(dom f) /\ ((dom Z) /\ (dom Z)) is V51() V52() V53() Element of K19(REAL)
(dom A) /\ ((dom f) /\ ((dom Z) /\ (dom Z))) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ ((dom f) /\ ((dom Z) /\ (dom Z)))) /\ x is V51() V52() V53() Element of K19(REAL)
(dom A) /\ (dom f) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
(((dom A) /\ (dom f)) /\ (dom Z)) /\ x is V51() V52() V53() Element of K19(REAL)
dom (((A - f) || x) (#) (Z || x)) is V51() V52() V53() Element of K19(x)
(A - f) | x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((A - f) | x) is V51() V52() V53() Element of K19(REAL)
Z | x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (Z | x) is V51() V52() V53() Element of K19(REAL)
(dom ((A - f) | x)) /\ (dom (Z | x)) is V51() V52() V53() Element of K19(REAL)
dom (A - f) is V51() V52() V53() Element of K19(REAL)
(dom (A - f)) /\ x is V51() V52() V53() Element of K19(REAL)
((dom (A - f)) /\ x) /\ (dom (Z | x)) is V51() V52() V53() Element of K19(REAL)
(dom Z) /\ x is V51() V52() V53() Element of K19(REAL)
((dom (A - f)) /\ x) /\ ((dom Z) /\ x) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ x is V51() V52() V53() Element of K19(REAL)
(((dom A) /\ (dom f)) /\ x) /\ ((dom Z) /\ x) is V51() V52() V53() Element of K19(REAL)
x /\ (dom Z) is V51() V52() V53() Element of K19(REAL)
(x /\ (dom Z)) /\ x is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ ((x /\ (dom Z)) /\ x) is V51() V52() V53() Element of K19(REAL)
x /\ x is V51() V52() V53() Element of K19(REAL)
(dom Z) /\ (x /\ x) is V51() V52() V53() Element of K19(REAL)
((dom A) /\ (dom f)) /\ ((dom Z) /\ (x /\ x)) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of x
(((A - f) || x) (#) (Z || x)) . Z is V28() V29() ext-real Element of REAL
(((A (#) Z) - (f (#) Z)) || x) . Z is V28() V29() ext-real Element of REAL
dom ((A - f) || x) is V51() V52() V53() Element of K19(x)
dom (Z || x) is V51() V52() V53() Element of K19(x)
(dom ((A - f) || x)) /\ (dom (Z || x)) is V51() V52() V53() Element of K19(x)
((A - f) | x) . Z is V28() V29() ext-real Element of REAL
(Z | x) . Z is V28() V29() ext-real Element of REAL
(((A - f) | x) . Z) * ((Z | x) . Z) is V28() V29() ext-real Element of REAL
(A - f) . Z is V28() V29() ext-real Element of REAL
((A - f) . Z) * ((Z | x) . Z) is V28() V29() ext-real Element of REAL
A . Z is V28() V29() ext-real Element of REAL
f . Z is V28() V29() ext-real Element of REAL
(A . Z) - (f . Z) is V28() V29() ext-real Element of REAL
((A . Z) - (f . Z)) * ((Z | x) . Z) is V28() V29() ext-real Element of REAL
((A (#) Z) - (f (#) Z)) . Z is V28() V29() ext-real Element of REAL
(A (#) Z) . Z is V28() V29() ext-real Element of REAL
(f (#) Z) . Z is V28() V29() ext-real Element of REAL
((A (#) Z) . Z) - ((f (#) Z) . Z) is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
(A . Z) * (Z . Z) is V28() V29() ext-real Element of REAL
((A . Z) * (Z . Z)) - ((f (#) Z) . Z) is V28() V29() ext-real Element of REAL
(f . Z) * (Z . Z) is V28() V29() ext-real Element of REAL
((A . Z) * (Z . Z)) - ((f . Z) * (Z . Z)) is V28() V29() ext-real Element of REAL
((A . Z) - (f . Z)) * (Z . Z) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is non empty V51() V52() V53() Element of K19(REAL)
(A (#) f) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
K20(x,REAL) is V34() V35() V36() set
K19(K20(x,REAL)) is set
Z || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A (#) f) || x) (#) (Z || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
A || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
(f (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
(A || x) (#) ((f (#) Z) || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
f || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
(A || x) (#) (f || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A || x) (#) (f || x)) (#) (Z || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
(f || x) (#) (Z || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
(A || x) (#) ((f || x) (#) (Z || x)) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((f (#) Z),A) is V28() V29() ext-real Element of REAL
(f (#) Z) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral ((f (#) Z) || A) is V28() V29() ext-real Element of REAL
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(Z,A,f) is V28() V29() ext-real Element of REAL
A (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((A (#) f),Z) is V28() V29() ext-real Element of REAL
(A (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral ((A (#) f) || Z) is V28() V29() ext-real Element of REAL
(Z,f,A) is V28() V29() ext-real Element of REAL
f (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((f (#) A),Z) is V28() V29() ext-real Element of REAL
(f (#) A) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((f (#) A) || Z) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A + f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
K20(x,REAL) is V34() V35() V36() set
K19(K20(x,REAL)) is set
(f (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A (#) Z) || x) | x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((f (#) Z) || x) | x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
(x,(A + f),Z) is V28() V29() ext-real Element of REAL
(A + f) (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A + f) (#) Z),x) is V28() V29() ext-real Element of REAL
((A + f) (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral (((A + f) (#) Z) || x) is V28() V29() ext-real Element of REAL
(x,A,Z) is V28() V29() ext-real Element of REAL
integral ((A (#) Z),x) is V28() V29() ext-real Element of REAL
integral ((A (#) Z) || x) is V28() V29() ext-real Element of REAL
(x,f,Z) is V28() V29() ext-real Element of REAL
integral ((f (#) Z),x) is V28() V29() ext-real Element of REAL
integral ((f (#) Z) || x) is V28() V29() ext-real Element of REAL
(x,A,Z) + (x,f,Z) is V28() V29() ext-real Element of REAL
(A + f) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
Z || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A + f) || x) (#) (Z || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral (((A + f) || x) (#) (Z || x)) is V28() V29() ext-real Element of REAL
(A (#) Z) + (f (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((A (#) Z) + (f (#) Z)) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral (((A (#) Z) + (f (#) Z)) || x) is V28() V29() ext-real Element of REAL
((A (#) Z) || x) + ((f (#) Z) || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral (((A (#) Z) || x) + ((f (#) Z) || x)) is V28() V29() ext-real Element of REAL
(integral ((A (#) Z) || x)) + (integral ((f (#) Z) || x)) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A - f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- f is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) f is V1() V4( REAL ) V6() V34() V35() V36() set
A + (- f) is V1() V4( REAL ) V6() V34() V35() V36() set
x is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
K20(x,REAL) is V34() V35() V36() set
K19(K20(x,REAL)) is set
(f (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A (#) Z) || x) | x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((f (#) Z) || x) | x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
(x,(A - f),Z) is V28() V29() ext-real Element of REAL
(A - f) (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A - f) (#) Z),x) is V28() V29() ext-real Element of REAL
((A - f) (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral (((A - f) (#) Z) || x) is V28() V29() ext-real Element of REAL
(x,A,Z) is V28() V29() ext-real Element of REAL
integral ((A (#) Z),x) is V28() V29() ext-real Element of REAL
integral ((A (#) Z) || x) is V28() V29() ext-real Element of REAL
(x,f,Z) is V28() V29() ext-real Element of REAL
integral ((f (#) Z),x) is V28() V29() ext-real Element of REAL
integral ((f (#) Z) || x) is V28() V29() ext-real Element of REAL
(x,A,Z) - (x,f,Z) is V28() V29() ext-real Element of REAL
(A - f) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
Z || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
((A - f) || x) (#) (Z || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral (((A - f) || x) (#) (Z || x)) is V28() V29() ext-real Element of REAL
(A (#) Z) - (f (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (f (#) Z) is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) (f (#) Z) is V1() V4( REAL ) V6() V34() V35() V36() set
(A (#) Z) + (- (f (#) Z)) is V1() V4( REAL ) V6() V34() V35() V36() set
((A (#) Z) - (f (#) Z)) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral (((A (#) Z) - (f (#) Z)) || x) is V28() V29() ext-real Element of REAL
((A (#) Z) || x) - ((f (#) Z) || x) is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
- ((f (#) Z) || x) is V1() V4(x) V6() V34() V35() V36() set
K98(1) (#) ((f (#) Z) || x) is V1() V4(x) V6() V34() V35() V36() set
((A (#) Z) || x) + (- ((f (#) Z) || x)) is V1() V4(x) V6() V34() V35() V36() set
integral (((A (#) Z) || x) - ((f (#) Z) || x)) is V28() V29() ext-real Element of REAL
(integral ((A (#) Z) || x)) - (integral ((f (#) Z) || x)) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (A (#) f) is V51() V52() V53() Element of K19(REAL)
- A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) A is V1() V4( REAL ) V6() V34() V35() V36() set
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A (#) f) | Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(Z,(- A),f) is V28() V29() ext-real Element of REAL
(- A) (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((- A) (#) f),Z) is V28() V29() ext-real Element of REAL
((- A) (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral (((- A) (#) f) || Z) is V28() V29() ext-real Element of REAL
(Z,A,f) is V28() V29() ext-real Element of REAL
integral ((A (#) f),Z) is V28() V29() ext-real Element of REAL
(A (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((A (#) f) || Z) is V28() V29() ext-real Element of REAL
- (Z,A,f) is V28() V29() ext-real Element of REAL
(- 1) (#) (A (#) f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((- 1) (#) (A (#) f)),Z) is V28() V29() ext-real Element of REAL
((- 1) (#) (A (#) f)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral (((- 1) (#) (A (#) f)) || Z) is V28() V29() ext-real Element of REAL
(- 1) * (integral ((A (#) f),Z)) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (f (#) Z) is V51() V52() V53() Element of K19(REAL)
A (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(f (#) Z) | x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(x,(A (#) f),Z) is V28() V29() ext-real Element of REAL
(A (#) f) (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A (#) f) (#) Z),x) is V28() V29() ext-real Element of REAL
((A (#) f) (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
K20(x,REAL) is V34() V35() V36() set
K19(K20(x,REAL)) is set
integral (((A (#) f) (#) Z) || x) is V28() V29() ext-real Element of REAL
(x,f,Z) is V28() V29() ext-real Element of REAL
integral ((f (#) Z),x) is V28() V29() ext-real Element of REAL
(f (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral ((f (#) Z) || x) is V28() V29() ext-real Element of REAL
A * (x,f,Z) is V28() V29() ext-real Element of REAL
A (#) (f (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((A (#) (f (#) Z)),x) is V28() V29() ext-real Element of REAL
(A (#) (f (#) Z)) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral ((A (#) (f (#) Z)) || x) is V28() V29() ext-real Element of REAL
A * (integral ((f (#) Z),x)) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
A * f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z (#) x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (Z (#) x) is V51() V52() V53() Element of K19(REAL)
A (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(Z (#) x) | Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(Z,(A (#) Z),(f (#) x)) is V28() V29() ext-real Element of REAL
(A (#) Z) (#) (f (#) x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A (#) Z) (#) (f (#) x)),Z) is V28() V29() ext-real Element of REAL
((A (#) Z) (#) (f (#) x)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral (((A (#) Z) (#) (f (#) x)) || Z) is V28() V29() ext-real Element of REAL
(Z,Z,x) is V28() V29() ext-real Element of REAL
integral ((Z (#) x),Z) is V28() V29() ext-real Element of REAL
(Z (#) x) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((Z (#) x) || Z) is V28() V29() ext-real Element of REAL
(A * f) * (Z,Z,x) is V28() V29() ext-real Element of REAL
Z (#) (f (#) x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) (Z (#) (f (#) x)) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((A (#) (Z (#) (f (#) x))),Z) is V28() V29() ext-real Element of REAL
(A (#) (Z (#) (f (#) x))) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((A (#) (Z (#) (f (#) x))) || Z) is V28() V29() ext-real Element of REAL
f (#) (Z (#) x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) (f (#) (Z (#) x)) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((A (#) (f (#) (Z (#) x))),Z) is V28() V29() ext-real Element of REAL
(A (#) (f (#) (Z (#) x))) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((A (#) (f (#) (Z (#) x))) || Z) is V28() V29() ext-real Element of REAL
(A * f) (#) (Z (#) x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A * f) (#) (Z (#) x)),Z) is V28() V29() ext-real Element of REAL
((A * f) (#) (Z (#) x)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral (((A * f) (#) (Z (#) x)) || Z) is V28() V29() ext-real Element of REAL
(A * f) * (integral ((Z (#) x),Z)) is V28() V29() ext-real Element of REAL
x is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(x,(A (#) f),Z) is V28() V29() ext-real Element of REAL
(A (#) f) (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A (#) f) (#) Z),x) is V28() V29() ext-real Element of REAL
((A (#) f) (#) Z) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
K20(x,REAL) is V34() V35() V36() set
K19(K20(x,REAL)) is set
integral (((A (#) f) (#) Z) || x) is V28() V29() ext-real Element of REAL
f (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(x,A,(f (#) Z)) is V28() V29() ext-real Element of REAL
A (#) (f (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((A (#) (f (#) Z)),x) is V28() V29() ext-real Element of REAL
(A (#) (f (#) Z)) || x is V1() V4(x) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(x,REAL))
integral ((A (#) (f (#) Z)) || x) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A + f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A (#) A) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
(A (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(f (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((A (#) A) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((A (#) f) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((f (#) f) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(Z,(A + f),(A + f)) is V28() V29() ext-real Element of REAL
(A + f) (#) (A + f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A + f) (#) (A + f)),Z) is V28() V29() ext-real Element of REAL
((A + f) (#) (A + f)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral (((A + f) (#) (A + f)) || Z) is V28() V29() ext-real Element of REAL
(Z,A,A) is V28() V29() ext-real Element of REAL
integral ((A (#) A),Z) is V28() V29() ext-real Element of REAL
integral ((A (#) A) || Z) is V28() V29() ext-real Element of REAL
(Z,A,f) is V28() V29() ext-real Element of REAL
integral ((A (#) f),Z) is V28() V29() ext-real Element of REAL
integral ((A (#) f) || Z) is V28() V29() ext-real Element of REAL
2 * (Z,A,f) is V28() V29() ext-real Element of REAL
(Z,A,A) + (2 * (Z,A,f)) is V28() V29() ext-real Element of REAL
(Z,f,f) is V28() V29() ext-real Element of REAL
integral ((f (#) f),Z) is V28() V29() ext-real Element of REAL
integral ((f (#) f) || Z) is V28() V29() ext-real Element of REAL
((Z,A,A) + (2 * (Z,A,f))) + (Z,f,f) is V28() V29() ext-real Element of REAL
((A (#) f) || Z) + ((f (#) f) || Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((A (#) A) || Z) + ((A (#) f) || Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
Z /\ Z is V51() V52() V53() Element of K19(REAL)
(((A (#) A) || Z) + ((A (#) f) || Z)) | (Z /\ Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(((A (#) f) || Z) + ((f (#) f) || Z)) | (Z /\ Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
A (#) (A + f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) (A + f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(A (#) (A + f)) + (f (#) (A + f)) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((A (#) (A + f)) + (f (#) (A + f))) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral (((A (#) (A + f)) + (f (#) (A + f))) || Z) is V28() V29() ext-real Element of REAL
(A (#) (A + f)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(f (#) (A + f)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((A (#) (A + f)) || Z) + ((f (#) (A + f)) || Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral (((A (#) (A + f)) || Z) + ((f (#) (A + f)) || Z)) is V28() V29() ext-real Element of REAL
(A (#) A) + (A (#) f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((A (#) A) + (A (#) f)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(((A (#) A) + (A (#) f)) || Z) + ((f (#) (A + f)) || Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((((A (#) A) + (A (#) f)) || Z) + ((f (#) (A + f)) || Z)) is V28() V29() ext-real Element of REAL
f (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(f (#) A) + (f (#) f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((f (#) A) + (f (#) f)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(((A (#) A) + (A (#) f)) || Z) + (((f (#) A) + (f (#) f)) || Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((((A (#) A) + (A (#) f)) || Z) + (((f (#) A) + (f (#) f)) || Z)) is V28() V29() ext-real Element of REAL
(((A (#) A) || Z) + ((A (#) f) || Z)) + (((f (#) A) + (f (#) f)) || Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((((A (#) A) || Z) + ((A (#) f) || Z)) + (((f (#) A) + (f (#) f)) || Z)) is V28() V29() ext-real Element of REAL
(f (#) A) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((f (#) A) || Z) + ((f (#) f) || Z) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(((A (#) A) || Z) + ((A (#) f) || Z)) + (((f (#) A) || Z) + ((f (#) f) || Z)) is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral ((((A (#) A) || Z) + ((A (#) f) || Z)) + (((f (#) A) || Z) + ((f (#) f) || Z))) is V28() V29() ext-real Element of REAL
integral (((A (#) A) || Z) + ((A (#) f) || Z)) is V28() V29() ext-real Element of REAL
integral (((A (#) f) || Z) + ((f (#) f) || Z)) is V28() V29() ext-real Element of REAL
(integral (((A (#) A) || Z) + ((A (#) f) || Z))) + (integral (((A (#) f) || Z) + ((f (#) f) || Z))) is V28() V29() ext-real Element of REAL
(integral ((A (#) A) || Z)) + (integral ((A (#) f) || Z)) is V28() V29() ext-real Element of REAL
((integral ((A (#) A) || Z)) + (integral ((A (#) f) || Z))) + (integral (((A (#) f) || Z) + ((f (#) f) || Z))) is V28() V29() ext-real Element of REAL
(integral ((A (#) f) || Z)) + (integral ((f (#) f) || Z)) is V28() V29() ext-real Element of REAL
((integral ((A (#) A) || Z)) + (integral ((A (#) f) || Z))) + ((integral ((A (#) f) || Z)) + (integral ((f (#) f) || Z))) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A + f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A (#) A) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
(A (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(f (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((A (#) A) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((A (#) f) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((f (#) f) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(Z,(A + f),(A + f)) is V28() V29() ext-real Element of REAL
(A + f) (#) (A + f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A + f) (#) (A + f)),Z) is V28() V29() ext-real Element of REAL
((A + f) (#) (A + f)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral (((A + f) (#) (A + f)) || Z) is V28() V29() ext-real Element of REAL
(Z,A,A) is V28() V29() ext-real Element of REAL
integral ((A (#) A),Z) is V28() V29() ext-real Element of REAL
integral ((A (#) A) || Z) is V28() V29() ext-real Element of REAL
(Z,f,f) is V28() V29() ext-real Element of REAL
integral ((f (#) f),Z) is V28() V29() ext-real Element of REAL
integral ((f (#) f) || Z) is V28() V29() ext-real Element of REAL
(Z,A,A) + (Z,f,f) is V28() V29() ext-real Element of REAL
(Z,A,f) is V28() V29() ext-real Element of REAL
integral ((A (#) f),Z) is V28() V29() ext-real Element of REAL
integral ((A (#) f) || Z) is V28() V29() ext-real Element of REAL
2 * (Z,A,f) is V28() V29() ext-real Element of REAL
(Z,A,A) + (2 * (Z,A,f)) is V28() V29() ext-real Element of REAL
((Z,A,A) + (2 * (Z,A,f))) + (Z,f,f) is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(A (#) A) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
((A (#) A) || f) | f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
(f,A,A) is V28() V29() ext-real Element of REAL
integral ((A (#) A),f) is V28() V29() ext-real Element of REAL
integral ((A (#) A) || f) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),A) is V28() V29() ext-real Element of REAL
(sin (#) cos) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),A) is V28() V29() ext-real Element of REAL
(sin (#) cos) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 * A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
(2 * A) * PI is V28() V29() ext-real Element of REAL
(2 * A) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
((2 * A) + 1) * PI is V28() V29() ext-real Element of REAL
[.((2 * A) * PI),(((2 * A) + 1) * PI).] is V51() V52() V53() closed Element of K19(REAL)
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(f,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),f) is V28() V29() ext-real Element of REAL
(sin (#) cos) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral ((sin (#) cos) || f) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 * f is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
(2 * f) * PI is V28() V29() ext-real Element of REAL
A + ((2 * f) * PI) is V28() V29() ext-real Element of REAL
(2 * f) + 1 is non empty V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
((2 * f) + 1) * PI is V28() V29() ext-real Element of REAL
A + (((2 * f) + 1) * PI) is V28() V29() ext-real Element of REAL
[.(A + ((2 * f) * PI)),(A + (((2 * f) + 1) * PI)).] is V51() V52() V53() closed Element of K19(REAL)
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(Z,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),Z) is V28() V29() ext-real Element of REAL
(sin (#) cos) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral ((sin (#) cos) || Z) is V28() V29() ext-real Element of REAL
- PI is V28() V29() ext-real Element of REAL
[.(- PI),PI.] is V51() V52() V53() closed Element of K19(REAL)
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(A,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),A) is V28() V29() ext-real Element of REAL
(sin (#) cos) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V28() V29() ext-real Element of REAL
cos . (lower_bound A) is V28() V29() ext-real Element of REAL
(cos . (lower_bound A)) * (cos . (lower_bound A)) is V28() V29() ext-real Element of REAL
cos . (upper_bound A) is V28() V29() ext-real Element of REAL
(cos . (upper_bound A)) * (cos . (upper_bound A)) is V28() V29() ext-real Element of REAL
((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))) is V28() 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 V28() V29() ext-real Element of REAL
cos . PI is V28() V29() ext-real Element of REAL
cos . (- PI) is V28() V29() ext-real Element of REAL
(cos . PI) * (cos . (- PI)) is V28() V29() ext-real Element of REAL
(cos . PI) * (cos . PI) is V28() V29() ext-real Element of REAL
((cos . PI) * (cos . (- PI))) - ((cos . PI) * (cos . PI)) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . PI) * (cos . (- PI))) - ((cos . PI) * (cos . PI))) is V28() V29() ext-real Element of REAL
((cos . PI) * (cos . PI)) - ((cos . PI) * (cos . PI)) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . PI) * (cos . PI)) - ((cos . PI) * (cos . PI))) is V28() V29() ext-real Element of REAL
PI / 2 is V28() V29() ext-real Element of REAL
- (PI / 2) is V28() V29() ext-real Element of REAL
[.(- (PI / 2)),(PI / 2).] is V51() V52() V53() closed Element of K19(REAL)
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(A,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),A) is V28() V29() ext-real Element of REAL
(sin (#) cos) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V28() V29() ext-real Element of REAL
cos . (lower_bound A) is V28() V29() ext-real Element of REAL
(cos . (lower_bound A)) * (cos . (lower_bound A)) is V28() V29() ext-real Element of REAL
cos . (upper_bound A) is V28() V29() ext-real Element of REAL
(cos . (upper_bound A)) * (cos . (upper_bound A)) is V28() V29() ext-real Element of REAL
((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))) is V28() 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 V28() V29() ext-real Element of REAL
cos . (PI / 2) is V28() V29() ext-real Element of REAL
cos . (- (PI / 2)) is V28() V29() ext-real Element of REAL
(cos . (PI / 2)) * (cos . (- (PI / 2))) is V28() V29() ext-real Element of REAL
(cos . (PI / 2)) * (cos . (PI / 2)) is V28() V29() ext-real Element of REAL
((cos . (PI / 2)) * (cos . (- (PI / 2)))) - ((cos . (PI / 2)) * (cos . (PI / 2))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . (PI / 2)) * (cos . (- (PI / 2)))) - ((cos . (PI / 2)) * (cos . (PI / 2)))) is V28() V29() ext-real Element of REAL
((cos . (PI / 2)) * (cos . (PI / 2))) - ((cos . (PI / 2)) * (cos . (PI / 2))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . (PI / 2)) * (cos . (PI / 2))) - ((cos . (PI / 2)) * (cos . (PI / 2)))) is V28() V29() ext-real Element of REAL
2 * PI is V28() V29() ext-real Element of REAL
- (2 * PI) is V28() V29() ext-real Element of REAL
[.(- (2 * PI)),(2 * PI).] is V51() V52() V53() closed Element of K19(REAL)
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(A,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),A) is V28() V29() ext-real Element of REAL
(sin (#) cos) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral ((sin (#) cos) || A) is V28() V29() ext-real Element of REAL
cos . (lower_bound A) is V28() V29() ext-real Element of REAL
(cos . (lower_bound A)) * (cos . (lower_bound A)) is V28() V29() ext-real Element of REAL
cos . (upper_bound A) is V28() V29() ext-real Element of REAL
(cos . (upper_bound A)) * (cos . (upper_bound A)) is V28() V29() ext-real Element of REAL
((cos . (lower_bound A)) * (cos . (lower_bound A))) - ((cos . (upper_bound A)) * (cos . (upper_bound A))) is V28() 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 V28() V29() ext-real Element of REAL
cos . (2 * PI) is V28() V29() ext-real Element of REAL
cos . (- (2 * PI)) is V28() V29() ext-real Element of REAL
(cos . (2 * PI)) * (cos . (- (2 * PI))) is V28() V29() ext-real Element of REAL
(cos . (2 * PI)) * (cos . (2 * PI)) is V28() V29() ext-real Element of REAL
((cos . (2 * PI)) * (cos . (- (2 * PI)))) - ((cos . (2 * PI)) * (cos . (2 * PI))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . (2 * PI)) * (cos . (- (2 * PI)))) - ((cos . (2 * PI)) * (cos . (2 * PI)))) is V28() V29() ext-real Element of REAL
((cos . (2 * PI)) * (cos . (2 * PI))) - ((cos . (2 * PI)) * (cos . (2 * PI))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . (2 * PI)) * (cos . (2 * PI))) - ((cos . (2 * PI)) * (cos . (2 * PI)))) is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 * A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
(2 * A) * PI is V28() V29() ext-real Element of REAL
- ((2 * A) * PI) is V28() V29() ext-real Element of REAL
[.(- ((2 * A) * PI)),((2 * A) * PI).] is V51() V52() V53() closed Element of K19(REAL)
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
(f,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),f) is V28() V29() ext-real Element of REAL
(sin (#) cos) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral ((sin (#) cos) || f) is V28() V29() ext-real Element of REAL
cos . (lower_bound f) is V28() V29() ext-real Element of REAL
(cos . (lower_bound f)) * (cos . (lower_bound f)) is V28() V29() ext-real Element of REAL
cos . (upper_bound f) is V28() V29() ext-real Element of REAL
(cos . (upper_bound f)) * (cos . (upper_bound f)) is V28() V29() ext-real Element of REAL
((cos . (lower_bound f)) * (cos . (lower_bound f))) - ((cos . (upper_bound f)) * (cos . (upper_bound f))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . (lower_bound f)) * (cos . (lower_bound f))) - ((cos . (upper_bound f)) * (cos . (upper_bound f)))) is V28() V29() ext-real Element of REAL
cos . ((2 * A) * PI) is V28() V29() ext-real Element of REAL
cos . (- ((2 * A) * PI)) is V28() V29() ext-real Element of REAL
(cos . ((2 * A) * PI)) * (cos . (- ((2 * A) * PI))) is V28() V29() ext-real Element of REAL
(cos . ((2 * A) * PI)) * (cos . ((2 * A) * PI)) is V28() V29() ext-real Element of REAL
((cos . ((2 * A) * PI)) * (cos . (- ((2 * A) * PI)))) - ((cos . ((2 * A) * PI)) * (cos . ((2 * A) * PI))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . ((2 * A) * PI)) * (cos . (- ((2 * A) * PI)))) - ((cos . ((2 * A) * PI)) * (cos . ((2 * A) * PI)))) is V28() V29() ext-real Element of REAL
((cos . ((2 * A) * PI)) * (cos . ((2 * A) * PI))) - ((cos . ((2 * A) * PI)) * (cos . ((2 * A) * PI))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . ((2 * A) * PI)) * (cos . ((2 * A) * PI))) - ((cos . ((2 * A) * PI)) * (cos . ((2 * A) * PI)))) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
2 * f is V21() V22() V23() V27() V28() V29() V30() ext-real non negative Element of REAL
(2 * f) * PI is V28() V29() ext-real Element of REAL
A - ((2 * f) * PI) is V28() V29() ext-real Element of REAL
A + ((2 * f) * PI) is V28() V29() ext-real Element of REAL
[.(A - ((2 * f) * PI)),(A + ((2 * f) * PI)).] is V51() V52() V53() closed Element of K19(REAL)
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound Z is V28() V29() ext-real Element of REAL
lower_bound Z is V28() V29() ext-real Element of REAL
(Z,sin,cos) is V28() V29() ext-real Element of REAL
integral ((sin (#) cos),Z) is V28() V29() ext-real Element of REAL
(sin (#) cos) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral ((sin (#) cos) || Z) is V28() V29() ext-real Element of REAL
cos . (lower_bound Z) is V28() V29() ext-real Element of REAL
(cos . (lower_bound Z)) * (cos . (lower_bound Z)) is V28() V29() ext-real Element of REAL
cos . (upper_bound Z) is V28() V29() ext-real Element of REAL
(cos . (upper_bound Z)) * (cos . (upper_bound Z)) is V28() V29() ext-real Element of REAL
((cos . (lower_bound Z)) * (cos . (lower_bound Z))) - ((cos . (upper_bound Z)) * (cos . (upper_bound Z))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . (lower_bound Z)) * (cos . (lower_bound Z))) - ((cos . (upper_bound Z)) * (cos . (upper_bound Z)))) is V28() V29() ext-real Element of REAL
((2 * f) * PI) - A is V28() V29() ext-real Element of REAL
cos . (((2 * f) * PI) - A) is V28() V29() ext-real Element of REAL
- (((2 * f) * PI) - A) is V28() V29() ext-real Element of REAL
cos . (- (((2 * f) * PI) - A)) is V28() V29() ext-real Element of REAL
(cos . (((2 * f) * PI) - A)) * (cos . (- (((2 * f) * PI) - A))) is V28() V29() ext-real Element of REAL
cos . (A + ((2 * f) * PI)) is V28() V29() ext-real Element of REAL
(cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI))) is V28() V29() ext-real Element of REAL
((cos . (((2 * f) * PI) - A)) * (cos . (- (((2 * f) * PI) - A)))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI)))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . (((2 * f) * PI) - A)) * (cos . (- (((2 * f) * PI) - A)))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI))))) is V28() V29() ext-real Element of REAL
- A is V28() V29() ext-real Element of REAL
(- A) + ((2 * f) * PI) is V28() V29() ext-real Element of REAL
cos . ((- A) + ((2 * f) * PI)) is V28() V29() ext-real Element of REAL
(cos . ((- A) + ((2 * f) * PI))) * (cos . ((- A) + ((2 * f) * PI))) is V28() V29() ext-real Element of REAL
((cos . ((- A) + ((2 * f) * PI))) * (cos . ((- A) + ((2 * f) * PI)))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI)))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos . ((- A) + ((2 * f) * PI))) * (cos . ((- A) + ((2 * f) * PI)))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI))))) is V28() V29() ext-real Element of REAL
cos (- A) is V28() V29() ext-real Element of REAL
cos . (- A) is V28() V29() ext-real Element of REAL
cos ((- A) + ((2 * f) * PI)) is V28() V29() ext-real Element of REAL
(cos (- A)) * (cos ((- A) + ((2 * f) * PI))) is V28() V29() ext-real Element of REAL
((cos (- A)) * (cos ((- A) + ((2 * f) * PI)))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI)))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos (- A)) * (cos ((- A) + ((2 * f) * PI)))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI))))) is V28() V29() ext-real Element of REAL
(cos (- A)) * (cos (- A)) is V28() V29() ext-real Element of REAL
((cos (- A)) * (cos (- A))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI)))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos (- A)) * (cos (- A))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI))))) is V28() V29() ext-real Element of REAL
cos A is V28() V29() ext-real Element of REAL
cos . A is V28() V29() ext-real Element of REAL
(cos A) * (cos (- A)) is V28() V29() ext-real Element of REAL
((cos A) * (cos (- A))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI)))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos A) * (cos (- A))) - ((cos . (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI))))) is V28() V29() ext-real Element of REAL
(cos A) * (cos A) is V28() V29() ext-real Element of REAL
cos (A + ((2 * f) * PI)) is V28() V29() ext-real Element of REAL
(cos (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI))) is V28() V29() ext-real Element of REAL
((cos A) * (cos A)) - ((cos (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI)))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos A) * (cos A)) - ((cos (A + ((2 * f) * PI))) * (cos . (A + ((2 * f) * PI))))) is V28() V29() ext-real Element of REAL
(cos A) * (cos (A + ((2 * f) * PI))) is V28() V29() ext-real Element of REAL
((cos A) * (cos A)) - ((cos A) * (cos (A + ((2 * f) * PI)))) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos A) * (cos A)) - ((cos A) * (cos (A + ((2 * f) * PI))))) is V28() V29() ext-real Element of REAL
((cos A) * (cos A)) - ((cos A) * (cos A)) is V28() V29() ext-real Element of REAL
(1 / 2) * (((cos A) * (cos A)) - ((cos A) * (cos A))) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(A,f,f) is V28() V29() ext-real Element of REAL
f (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((f (#) f),A) is V28() V29() ext-real Element of REAL
(f (#) f) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral ((f (#) f) || A) is V28() V29() ext-real Element of REAL
sqrt (A,f,f) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A (#) A) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
((A (#) A) || f) | f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
(f,A) is V28() V29() ext-real Element of REAL
(f,A,A) is V28() V29() ext-real Element of REAL
integral ((A (#) A),f) is V28() V29() ext-real Element of REAL
integral ((A (#) A) || f) is V28() V29() ext-real Element of REAL
sqrt (f,A,A) is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
1 (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(f,(1 (#) A)) is V28() V29() ext-real Element of REAL
(f,(1 (#) A),(1 (#) A)) is V28() V29() ext-real Element of REAL
(1 (#) A) (#) (1 (#) A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((1 (#) A) (#) (1 (#) A)),f) is V28() V29() ext-real Element of REAL
((1 (#) A) (#) (1 (#) A)) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (((1 (#) A) (#) (1 (#) A)) || f) is V28() V29() ext-real Element of REAL
sqrt (f,(1 (#) A),(1 (#) A)) is V28() V29() ext-real Element of REAL
(f,A) is V28() V29() ext-real Element of REAL
(f,A,A) is V28() V29() ext-real Element of REAL
A (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral ((A (#) A),f) is V28() V29() ext-real Element of REAL
(A (#) A) || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
integral ((A (#) A) || f) is V28() V29() ext-real Element of REAL
sqrt (f,A,A) is V28() V29() ext-real Element of REAL
A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f (#) f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A + f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
(A (#) A) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
(A (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(f (#) f) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((A (#) A) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((A (#) f) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
((f (#) f) || Z) | Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
(Z,(A + f)) is V28() V29() ext-real Element of REAL
(Z,(A + f),(A + f)) is V28() V29() ext-real Element of REAL
(A + f) (#) (A + f) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((A + f) (#) (A + f)),Z) is V28() V29() ext-real Element of REAL
((A + f) (#) (A + f)) || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
integral (((A + f) (#) (A + f)) || Z) is V28() V29() ext-real Element of REAL
sqrt (Z,(A + f),(A + f)) is V28() V29() ext-real Element of REAL
(Z,(A + f)) ^2 is V28() V29() ext-real Element of REAL
(Z,A) is V28() V29() ext-real Element of REAL
(Z,A,A) is V28() V29() ext-real Element of REAL
integral ((A (#) A),Z) is V28() V29() ext-real Element of REAL
integral ((A (#) A) || Z) is V28() V29() ext-real Element of REAL
sqrt (Z,A,A) is V28() V29() ext-real Element of REAL
(Z,A) ^2 is V28() V29() ext-real Element of REAL
(Z,f) is V28() V29() ext-real Element of REAL
(Z,f,f) is V28() V29() ext-real Element of REAL
integral ((f (#) f),Z) is V28() V29() ext-real Element of REAL
integral ((f (#) f) || Z) is V28() V29() ext-real Element of REAL
sqrt (Z,f,f) is V28() V29() ext-real Element of REAL
(Z,f) ^2 is V28() V29() ext-real Element of REAL
((Z,A) ^2) + ((Z,f) ^2) is V28() V29() ext-real Element of REAL
(Z,A,A) + (Z,f,f) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
- A is V28() V29() ext-real Element of REAL
AffineMap (1,A) is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
(AffineMap (1,A)) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
((AffineMap (1,A)) ^) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(AffineMap (1,A)) | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous Element of K19(K20(REAL,REAL))
rng ((AffineMap (1,A)) | f) is V51() V52() V53() Element of K19(REAL)
dom ((AffineMap (1,A)) | f) is V51() V52() V53() Element of K19(REAL)
Z is set
((AffineMap (1,A)) | f) . Z is V28() V29() ext-real Element of REAL
x is V28() V29() ext-real Element of REAL
(AffineMap (1,A)) . x is V28() V29() ext-real Element of REAL
1 * x is V28() V29() ext-real Element of REAL
A + (1 * x) is V28() V29() ext-real Element of REAL
A + x is V28() V29() ext-real Element of REAL
((AffineMap (1,A)) | f) " {0} is V51() V52() V53() Element of K19(REAL)
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(Z ^) . (upper_bound f) is V28() V29() ext-real Element of REAL
(Z ^) . (lower_bound f) is V28() V29() ext-real Element of REAL
((Z ^) . (upper_bound f)) - ((Z ^) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(Z ^) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((Z ^) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((Z ^) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A + x is V28() V29() ext-real Element of REAL
(A + x) ^2 is V28() V29() ext-real Element of REAL
1 / ((A + x) ^2) is V28() V29() ext-real Element of REAL
- (1 / ((A + x) ^2)) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 1) (#) (Z ^) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- 1) (#) (Z ^)) is V51() V52() V53() Element of K19(REAL)
((- 1) (#) (Z ^)) . (upper_bound f) is V28() V29() ext-real Element of REAL
((- 1) (#) (Z ^)) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((- 1) (#) (Z ^)) . (upper_bound f)) - (((- 1) (#) (Z ^)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
((- 1) (#) (Z ^)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((- 1) (#) (Z ^)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(((- 1) (#) (Z ^)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A + x is V28() V29() ext-real Element of REAL
(A + x) ^2 is V28() V29() ext-real Element of REAL
1 / ((A + x) ^2) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(Z ^) . (upper_bound f) is V28() V29() ext-real Element of REAL
(Z ^) . (lower_bound f) is V28() V29() ext-real Element of REAL
((Z ^) . (upper_bound f)) - ((Z ^) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(Z ^) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((Z ^) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((Z ^) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A - x is V28() V29() ext-real Element of REAL
(A - x) ^2 is V28() V29() ext-real Element of REAL
1 / ((A - x) ^2) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln * Z) is V51() V52() V53() Element of K19(REAL)
(ln * Z) . (upper_bound f) is V28() V29() ext-real Element of REAL
(ln * Z) . (lower_bound f) is V28() V29() ext-real Element of REAL
((ln * Z) . (upper_bound f)) - ((ln * Z) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(ln * Z) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((ln * Z) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((ln * Z) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A + x is V28() V29() ext-real Element of REAL
1 / (A + x) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln * Z) is V51() V52() V53() Element of K19(REAL)
(ln * Z) . (upper_bound f) is V28() V29() ext-real Element of REAL
(ln * Z) . (lower_bound f) is V28() V29() ext-real Element of REAL
((ln * Z) . (upper_bound f)) - ((ln * Z) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(ln * Z) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((ln * Z) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((ln * Z) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
x - A is V28() V29() ext-real Element of REAL
1 / (x - A) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (ln * Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (ln * Z) is V1() V4( REAL ) V6() V34() V35() V36() set
dom (- (ln * Z)) is V51() V52() V53() Element of K19(REAL)
(- (ln * Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
(- (ln * Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
((- (ln * Z)) . (upper_bound f)) - ((- (ln * Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- (ln * Z)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (ln * Z)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- (ln * Z)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A - x is V28() V29() ext-real Element of REAL
1 / (A - x) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
A (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
Z || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (Z || f) is V28() V29() ext-real Element of REAL
x is V51() V52() V53() open Element of K19(REAL)
id x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id x) - (A (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (A (#) Z) is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) (A (#) Z) is V1() V4( REAL ) V6() V34() V35() V36() set
(id x) + (- (A (#) Z)) is V1() V4( REAL ) V6() V34() V35() V36() set
dom ((id x) - (A (#) Z)) is V51() V52() V53() Element of K19(REAL)
((id x) - (A (#) Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
((id x) - (A (#) Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((id x) - (A (#) Z)) . (upper_bound f)) - (((id x) - (A (#) Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
((id x) - (A (#) Z)) `| x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id x) - (A (#) Z)) `| x) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((id x) - (A (#) Z)) `| x) . Z is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
A + Z is V28() V29() ext-real Element of REAL
Z / (A + Z) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(2 * A) (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
Z || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (Z || f) is V28() V29() ext-real Element of REAL
x is V51() V52() V53() open Element of K19(REAL)
id x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
((2 * A) (#) Z) - (id x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- (id x) is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) (id x) is V1() V4( REAL ) V6() V34() V35() V36() set
((2 * A) (#) Z) + (- (id x)) is V1() V4( REAL ) V6() V34() V35() V36() set
dom (((2 * A) (#) Z) - (id x)) is V51() V52() V53() Element of K19(REAL)
(((2 * A) (#) Z) - (id x)) . (upper_bound f) is V28() V29() ext-real Element of REAL
(((2 * A) (#) Z) - (id x)) . (lower_bound f) is V28() V29() ext-real Element of REAL
((((2 * A) (#) Z) - (id x)) . (upper_bound f)) - ((((2 * A) (#) Z) - (id x)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
(((2 * A) (#) Z) - (id x)) `| x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((((2 * A) (#) Z) - (id x)) `| x) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((((2 * A) (#) Z) - (id x)) `| x) . Z is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
A - Z is V28() V29() ext-real Element of REAL
A + Z is V28() V29() ext-real Element of REAL
(A - Z) / (A + Z) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(2 * A) (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
Z || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (Z || f) is V28() V29() ext-real Element of REAL
x is V51() V52() V53() open Element of K19(REAL)
id x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id x) - ((2 * A) (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- ((2 * A) (#) Z) is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) ((2 * A) (#) Z) is V1() V4( REAL ) V6() V34() V35() V36() set
(id x) + (- ((2 * A) (#) Z)) is V1() V4( REAL ) V6() V34() V35() V36() set
dom ((id x) - ((2 * A) (#) Z)) is V51() V52() V53() Element of K19(REAL)
((id x) - ((2 * A) (#) Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
((id x) - ((2 * A) (#) Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((id x) - ((2 * A) (#) Z)) . (upper_bound f)) - (((id x) - ((2 * A) (#) Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
((id x) - ((2 * A) (#) Z)) `| x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id x) - ((2 * A) (#) Z)) `| x) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((id x) - ((2 * A) (#) Z)) `| x) . Z is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
Z - A is V28() V29() ext-real Element of REAL
Z + A is V28() V29() ext-real Element of REAL
(Z - A) / (Z + A) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
2 * A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(2 * A) (#) Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
Z || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (Z || f) is V28() V29() ext-real Element of REAL
x is V51() V52() V53() open Element of K19(REAL)
id x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id x) + ((2 * A) (#) Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((id x) + ((2 * A) (#) Z)) is V51() V52() V53() Element of K19(REAL)
((id x) + ((2 * A) (#) Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
((id x) + ((2 * A) (#) Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((id x) + ((2 * A) (#) Z)) . (upper_bound f)) - (((id x) + ((2 * A) (#) Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
((id x) + ((2 * A) (#) Z)) `| x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id x) + ((2 * A) (#) Z)) `| x) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
(((id x) + ((2 * A) (#) Z)) `| x) . Z is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
Z + A is V28() V29() ext-real Element of REAL
Z - A is V28() V29() ext-real Element of REAL
(Z + A) / (Z - A) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
f - A is V28() V29() ext-real Element of REAL
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound Z is V28() V29() ext-real Element of REAL
lower_bound Z is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(f - A) (#) x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,Z) is V28() V29() ext-real Element of REAL
x || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral (x || Z) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id Z) + ((f - A) (#) x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((id Z) + ((f - A) (#) x)) is V51() V52() V53() Element of K19(REAL)
((id Z) + ((f - A) (#) x)) . (upper_bound Z) is V28() V29() ext-real Element of REAL
((id Z) + ((f - A) (#) x)) . (lower_bound Z) is V28() V29() ext-real Element of REAL
(((id Z) + ((f - A) (#) x)) . (upper_bound Z)) - (((id Z) + ((f - A) (#) x)) . (lower_bound Z)) is V28() V29() ext-real Element of REAL
((id Z) + ((f - A) (#) x)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id Z) + ((f - A) (#) x)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(((id Z) + ((f - A) (#) x)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
x + f is V28() V29() ext-real Element of REAL
x + A is V28() V29() ext-real Element of REAL
(x + f) / (x + A) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
f + A is V28() V29() ext-real Element of REAL
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound Z is V28() V29() ext-real Element of REAL
lower_bound Z is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(f + A) (#) x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,Z) is V28() V29() ext-real Element of REAL
x || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral (x || Z) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id Z) + ((f + A) (#) x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((id Z) + ((f + A) (#) x)) is V51() V52() V53() Element of K19(REAL)
((id Z) + ((f + A) (#) x)) . (upper_bound Z) is V28() V29() ext-real Element of REAL
((id Z) + ((f + A) (#) x)) . (lower_bound Z) is V28() V29() ext-real Element of REAL
(((id Z) + ((f + A) (#) x)) . (upper_bound Z)) - (((id Z) + ((f + A) (#) x)) . (lower_bound Z)) is V28() V29() ext-real Element of REAL
((id Z) + ((f + A) (#) x)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id Z) + ((f + A) (#) x)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(((id Z) + ((f + A) (#) x)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
x + f is V28() V29() ext-real Element of REAL
x - A is V28() V29() ext-real Element of REAL
(x + f) / (x - A) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
f + A is V28() V29() ext-real Element of REAL
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound Z is V28() V29() ext-real Element of REAL
lower_bound Z is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(f + A) (#) x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,Z) is V28() V29() ext-real Element of REAL
x || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral (x || Z) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id Z) - ((f + A) (#) x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- ((f + A) (#) x) is V1() V4( REAL ) V6() V34() V35() V36() set
K98(1) (#) ((f + A) (#) x) is V1() V4( REAL ) V6() V34() V35() V36() set
(id Z) + (- ((f + A) (#) x)) is V1() V4( REAL ) V6() V34() V35() V36() set
dom ((id Z) - ((f + A) (#) x)) is V51() V52() V53() Element of K19(REAL)
((id Z) - ((f + A) (#) x)) . (upper_bound Z) is V28() V29() ext-real Element of REAL
((id Z) - ((f + A) (#) x)) . (lower_bound Z) is V28() V29() ext-real Element of REAL
(((id Z) - ((f + A) (#) x)) . (upper_bound Z)) - (((id Z) - ((f + A) (#) x)) . (lower_bound Z)) is V28() V29() ext-real Element of REAL
((id Z) - ((f + A) (#) x)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id Z) - ((f + A) (#) x)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(((id Z) - ((f + A) (#) x)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
x - f is V28() V29() ext-real Element of REAL
x + A is V28() V29() ext-real Element of REAL
(x - f) / (x + A) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
A - f is V28() V29() ext-real Element of REAL
Z is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound Z is V28() V29() ext-real Element of REAL
lower_bound Z is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(A - f) (#) x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,Z) is V28() V29() ext-real Element of REAL
x || Z is V1() V4(Z) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(Z,REAL))
K20(Z,REAL) is V34() V35() V36() set
K19(K20(Z,REAL)) is set
integral (x || Z) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id Z) + ((A - f) (#) x) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((id Z) + ((A - f) (#) x)) is V51() V52() V53() Element of K19(REAL)
((id Z) + ((A - f) (#) x)) . (upper_bound Z) is V28() V29() ext-real Element of REAL
((id Z) + ((A - f) (#) x)) . (lower_bound Z) is V28() V29() ext-real Element of REAL
(((id Z) + ((A - f) (#) x)) . (upper_bound Z)) - (((id Z) + ((A - f) (#) x)) . (lower_bound Z)) is V28() V29() ext-real Element of REAL
((id Z) + ((A - f) (#) x)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((id Z) + ((A - f) (#) x)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(((id Z) + ((A - f) (#) x)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
x - f is V28() V29() ext-real Element of REAL
x - A is V28() V29() ext-real Element of REAL
(x - f) / (x - A) is V28() V29() ext-real Element of REAL
dom ln is V51() V52() V53() Element of K19(REAL)
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
ln . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
ln . (lower_bound A) is V28() V29() ext-real Element of REAL
(ln . (upper_bound A)) - (ln . (lower_bound A)) is V28() V29() ext-real Element of REAL
f is V51() V52() V53() open Element of K19(REAL)
id f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id f) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((id f) ^) is V51() V52() V53() Element of K19(REAL)
((id f) ^) | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (((id f) ^),A) is V28() V29() ext-real Element of REAL
((id f) ^) || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (((id f) ^) || A) is V28() V29() ext-real Element of REAL
ln `| f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln `| f) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(ln `| f) . x is V28() V29() ext-real Element of REAL
((id f) ^) . x is V28() V29() ext-real Element of REAL
1 / x is V28() V29() ext-real Element of REAL
x " is V28() V29() ext-real Element of REAL
(id f) . x is V28() V29() ext-real Element of REAL
((id f) . x) " is V28() V29() ext-real Element of REAL
A is V21() V22() V23() V27() V28() V29() V30() ext-real non negative V50() V51() V52() V53() V54() V55() V56() Element of NAT
#Z A is V1() V4( REAL ) V5( REAL ) V6() non empty total V18( REAL , REAL ) V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * (#Z A) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln * (#Z A)) is V51() V52() V53() Element of K19(REAL)
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
(ln * (#Z A)) . (upper_bound f) is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
(ln * (#Z A)) . (lower_bound f) is V28() V29() ext-real Element of REAL
((ln * (#Z A)) . (upper_bound f)) - ((ln * (#Z A)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom Z is V51() V52() V53() Element of K19(REAL)
Z | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (Z,f) is V28() V29() ext-real Element of REAL
Z || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (Z || f) is V28() V29() ext-real Element of REAL
x is V51() V52() V53() open Element of K19(REAL)
(ln * (#Z A)) `| x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((ln * (#Z A)) `| x) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((ln * (#Z A)) `| x) . Z is V28() V29() ext-real Element of REAL
Z . Z is V28() V29() ext-real Element of REAL
A / Z is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
f || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (f || A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
(id Z) ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
ln * ((id Z) ^) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (ln * ((id Z) ^)) is V51() V52() V53() Element of K19(REAL)
(ln * ((id Z) ^)) . (upper_bound A) is V28() V29() ext-real Element of REAL
(ln * ((id Z) ^)) . (lower_bound A) is V28() V29() ext-real Element of REAL
((ln * ((id Z) ^)) . (upper_bound A)) - ((ln * ((id Z) ^)) . (lower_bound A)) is V28() V29() ext-real Element of REAL
(ln * ((id Z) ^)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((ln * ((id Z) ^)) `| Z) is V51() V52() V53() Element of K19(REAL)
Z is V28() V29() ext-real Element of REAL
((ln * ((id Z) ^)) `| Z) . Z is V28() V29() ext-real Element of REAL
f . Z is V28() V29() ext-real Element of REAL
1 / Z is V28() V29() ext-real Element of REAL
- (1 / Z) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(#R (3 / 2)) * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(2 / 3) (#) ((#R (3 / 2)) * Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((2 / 3) (#) ((#R (3 / 2)) * Z)) is V51() V52() V53() Element of K19(REAL)
((2 / 3) (#) ((#R (3 / 2)) * Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
((2 / 3) (#) ((#R (3 / 2)) * Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((2 / 3) (#) ((#R (3 / 2)) * Z)) . (upper_bound f)) - (((2 / 3) (#) ((#R (3 / 2)) * Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
((2 / 3) (#) ((#R (3 / 2)) * Z)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((2 / 3) (#) ((#R (3 / 2)) * Z)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(((2 / 3) (#) ((#R (3 / 2)) * Z)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A + x is V28() V29() ext-real Element of REAL
(A + x) #R (1 / 2) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(#R (3 / 2)) * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- (2 / 3)) (#) ((#R (3 / 2)) * Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- (2 / 3)) (#) ((#R (3 / 2)) * Z)) is V51() V52() V53() Element of K19(REAL)
((- (2 / 3)) (#) ((#R (3 / 2)) * Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
((- (2 / 3)) (#) ((#R (3 / 2)) * Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((- (2 / 3)) (#) ((#R (3 / 2)) * Z)) . (upper_bound f)) - (((- (2 / 3)) (#) ((#R (3 / 2)) * Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
((- (2 / 3)) (#) ((#R (3 / 2)) * Z)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((- (2 / 3)) (#) ((#R (3 / 2)) * Z)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(((- (2 / 3)) (#) ((#R (3 / 2)) * Z)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A - x is V28() V29() ext-real Element of REAL
(A - x) #R (1 / 2) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(#R (1 / 2)) * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
2 (#) ((#R (1 / 2)) * Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (2 (#) ((#R (1 / 2)) * Z)) is V51() V52() V53() Element of K19(REAL)
(2 (#) ((#R (1 / 2)) * Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
(2 (#) ((#R (1 / 2)) * Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
((2 (#) ((#R (1 / 2)) * Z)) . (upper_bound f)) - ((2 (#) ((#R (1 / 2)) * Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(2 (#) ((#R (1 / 2)) * Z)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((2 (#) ((#R (1 / 2)) * Z)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((2 (#) ((#R (1 / 2)) * Z)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A + x is V28() V29() ext-real Element of REAL
(A + x) #R (- (1 / 2)) is V28() V29() ext-real Element of REAL
A is V28() V29() ext-real Element of REAL
f is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound f is V28() V29() ext-real Element of REAL
lower_bound f is V28() V29() ext-real Element of REAL
Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(#R (1 / 2)) * Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
(- 2) (#) ((#R (1 / 2)) * Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- 2) (#) ((#R (1 / 2)) * Z)) is V51() V52() V53() Element of K19(REAL)
((- 2) (#) ((#R (1 / 2)) * Z)) . (upper_bound f) is V28() V29() ext-real Element of REAL
((- 2) (#) ((#R (1 / 2)) * Z)) . (lower_bound f) is V28() V29() ext-real Element of REAL
(((- 2) (#) ((#R (1 / 2)) * Z)) . (upper_bound f)) - (((- 2) (#) ((#R (1 / 2)) * Z)) . (lower_bound f)) is V28() V29() ext-real Element of REAL
x is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom x is V51() V52() V53() Element of K19(REAL)
x | f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (x,f) is V28() V29() ext-real Element of REAL
x || f is V1() V4(f) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(f,REAL))
K20(f,REAL) is V34() V35() V36() set
K19(K20(f,REAL)) is set
integral (x || f) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
((- 2) (#) ((#R (1 / 2)) * Z)) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((- 2) (#) ((#R (1 / 2)) * Z)) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(((- 2) (#) ((#R (1 / 2)) * Z)) `| Z) . x is V28() V29() ext-real Element of REAL
x . x is V28() V29() ext-real Element of REAL
A - x is V28() V29() ext-real Element of REAL
(A - x) #R (- (1 / 2)) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
f || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (f || A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
id Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() continuous V49() Element of K19(K20(REAL,REAL))
- (id Z) is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) (id Z) is V1() V4( REAL ) V6() V34() V35() V36() set
(- (id Z)) (#) cos is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
((- (id Z)) (#) cos) + sin is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (((- (id Z)) (#) cos) + sin) is V51() V52() V53() Element of K19(REAL)
(((- (id Z)) (#) cos) + sin) . (upper_bound A) is V28() V29() ext-real Element of REAL
(((- (id Z)) (#) cos) + sin) . (lower_bound A) is V28() V29() ext-real Element of REAL
((((- (id Z)) (#) cos) + sin) . (upper_bound A)) - ((((- (id Z)) (#) cos) + sin) . (lower_bound A)) is V28() V29() ext-real Element of REAL
(((- (id Z)) (#) cos) + sin) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((((- (id Z)) (#) cos) + sin) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((((- (id Z)) (#) cos) + sin) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
x * (sin . x) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
sec . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
sec . (lower_bound A) is V28() V29() ext-real Element of REAL
(sec . (upper_bound A)) - (sec . (lower_bound A)) is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
f || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (f || A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
sec `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom (sec `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
(sec `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
(cos . x) ^2 is V28() V29() ext-real Element of REAL
(sin . x) / ((cos . x) ^2) is V28() V29() ext-real Element of REAL
cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
sin ^ is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
- cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
K98(1) (#) cosec is V1() V4( REAL ) V6() V34() V35() V36() set
dom (- cosec) is V51() V52() V53() Element of K19(REAL)
A is V51() V52() V53() open Element of K19(REAL)
(- cosec) `| A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom cosec is V51() V52() V53() Element of K19(REAL)
f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
f is V28() V29() ext-real Element of REAL
((- cosec) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
(cos . f) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
diff ((sin ^),f) is V28() V29() ext-real Element of REAL
(- 1) * (diff ((sin ^),f)) is V28() V29() ext-real Element of REAL
diff (sin,f) is V28() V29() ext-real Element of REAL
(diff (sin,f)) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
- ((diff (sin,f)) / ((sin . f) ^2)) is V28() V29() ext-real Element of REAL
(- 1) * (- ((diff (sin,f)) / ((sin . f) ^2))) is V28() V29() ext-real Element of REAL
(- 1) (#) cosec is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
f is V28() V29() ext-real Element of REAL
((- cosec) `| A) . f is V28() V29() ext-real Element of REAL
cos . f is V28() V29() ext-real Element of REAL
sin . f is V28() V29() ext-real Element of REAL
(sin . f) ^2 is V28() V29() ext-real Element of REAL
(cos . f) / ((sin . f) ^2) is V28() V29() ext-real Element of REAL
A is non empty V51() V52() V53() closed_interval V87() Element of K19(REAL)
upper_bound A is V28() V29() ext-real Element of REAL
(- cosec) . (upper_bound A) is V28() V29() ext-real Element of REAL
lower_bound A is V28() V29() ext-real Element of REAL
(- cosec) . (lower_bound A) is V28() V29() ext-real Element of REAL
((- cosec) . (upper_bound A)) - ((- cosec) . (lower_bound A)) is V28() V29() ext-real Element of REAL
f is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom f is V51() V52() V53() Element of K19(REAL)
f | A is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
integral (f,A) is V28() V29() ext-real Element of REAL
f || A is V1() V4(A) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(A,REAL))
K20(A,REAL) is V34() V35() V36() set
K19(K20(A,REAL)) is set
integral (f || A) is V28() V29() ext-real Element of REAL
Z is V51() V52() V53() open Element of K19(REAL)
(- cosec) `| Z is V1() V4( REAL ) V5( REAL ) V6() V34() V35() V36() Element of K19(K20(REAL,REAL))
dom ((- cosec) `| Z) is V51() V52() V53() Element of K19(REAL)
x is V28() V29() ext-real Element of REAL
((- cosec) `| Z) . x is V28() V29() ext-real Element of REAL
f . x is V28() V29() ext-real Element of REAL
cos . x is V28() V29() ext-real Element of REAL
sin . x is V28() V29() ext-real Element of REAL
(sin . x) ^2 is V28() V29() ext-real Element of REAL
(cos . x) / ((sin . x) ^2) is V28() V29() ext-real Element of REAL