Processing math: 0%
:: Integrability Formulas -- Part {III}
:: by Bo Li and Na Ma
::
:: Received February 4, 2010
:: Copyright (c) 2010-2021 Association of Mizar Users
Lm1
:
for
Z
being
open
Subset
of
REAL
st
0
in
Z
holds
(
id
Z
)
"
{
0
}
=
{
0
}
proof
end;
theorem
Th1
:
:: INTEGR14:1
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sec
*
(
(
id
Z
)
^
)
)
holds
(
-
(
sec
*
(
(
id
Z
)
^
)
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
sec
*
(
(
id
Z
)
^
)
)
)
`|
Z
)
.
x
=
(
sin
.
(
1
/
x
)
)
/
(
(
x
^2
)
*
(
(
cos
.
(
1
/
x
)
)
^2
)
)
) )
proof
end;
::f.x=-cosec.
exp_R.x
theorem
Th2
:
:: INTEGR14:2
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cosec
*
exp_R
)
holds
(
-
(
cosec
*
exp_R
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
cosec
*
exp_R
)
)
`|
Z
)
.
x
=
(
(
exp_R
.
x
)
*
(
cos
.
(
exp_R
.
x
)
)
)
/
(
(
sin
.
(
exp_R
.
x
)
)
^2
)
) )
proof
end;
:: f.x = -cosec.
ln.x
theorem
Th3
:
:: INTEGR14:3
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cosec
*
ln
)
holds
(
-
(
cosec
*
ln
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
cosec
*
ln
)
)
`|
Z
)
.
x
=
(
cos
.
(
ln
.
x
)
)
/
(
x
*
(
(
sin
.
(
ln
.
x
)
)
^2
)
)
) )
proof
end;
:: f.x = -exp_R.
cosec.x
theorem
Th4
:
:: INTEGR14:4
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
exp_R
*
cosec
)
holds
(
-
(
exp_R
*
cosec
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
exp_R
*
cosec
)
)
`|
Z
)
.
x
=
(
(
exp_R
.
(
cosec
.
x
)
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
) )
proof
end;
:: f.x = -ln.
cosec.x
theorem
Th5
:
:: INTEGR14:5
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
ln
*
cosec
)
holds
(
-
(
ln
*
cosec
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
ln
*
cosec
)
)
`|
Z
)
.
x
=
cot
.
x
) )
proof
end;
::f.x=-
cosec.x
#Z n
theorem
Th6
:
:: INTEGR14:6
for
n
being
Nat
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
#Z
n
)
*
cosec
)
& 1
<=
n
holds
(
-
(
(
#Z
n
)
*
cosec
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
(
#Z
n
)
*
cosec
)
)
`|
Z
)
.
x
=
(
n
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
#Z
(
n
+
1
)
)
) )
proof
end;
::f.x= -1/x*sec.x
theorem
Th7
:
:: INTEGR14:7
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
(
id
Z
)
^
)
(#)
sec
)
holds
(
-
(
(
(
id
Z
)
^
)
(#)
sec
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
(
(
id
Z
)
^
)
(#)
sec
)
)
`|
Z
)
.
x
=
(
(
1
/
(
cos
.
x
)
)
/
(
x
^2
)
)
-
(
(
(
sin
.
x
)
/
x
)
/
(
(
cos
.
x
)
^2
)
)
) )
proof
end;
::f.x=-1/x*cosec.x
theorem
Th8
:
:: INTEGR14:8
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
(
id
Z
)
^
)
(#)
cosec
)
holds
(
-
(
(
(
id
Z
)
^
)
(#)
cosec
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
(
(
id
Z
)
^
)
(#)
cosec
)
)
`|
Z
)
.
x
=
(
(
1
/
(
sin
.
x
)
)
/
(
x
^2
)
)
+
(
(
(
cos
.
x
)
/
x
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x = -cosec.
sin.x
theorem
Th9
:
:: INTEGR14:9
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cosec
*
sin
)
holds
(
-
(
cosec
*
sin
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
cosec
*
sin
)
)
`|
Z
)
.
x
=
(
(
cos
.
x
)
*
(
cos
.
(
sin
.
x
)
)
)
/
(
(
sin
.
(
sin
.
x
)
)
^2
)
) )
proof
end;
::f.x=-sec.
cot.x
theorem
Th10
:
:: INTEGR14:10
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
sec
*
cot
)
holds
(
-
(
sec
*
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
sec
*
cot
)
)
`|
Z
)
.
x
=
(
(
sin
.
(
cot
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
/
(
(
cos
.
(
cot
.
x
)
)
^2
)
) )
proof
end;
::f.x=-cosec.
tan.x
theorem
Th11
:
:: INTEGR14:11
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cosec
*
tan
)
holds
(
-
(
cosec
*
tan
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
cosec
*
tan
)
)
`|
Z
)
.
x
=
(
(
cos
.
(
tan
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
/
(
(
sin
.
(
tan
.
x
)
)
^2
)
) )
proof
end;
::f.x=-cot.x*sec.x
theorem
Th12
:
:: INTEGR14:12
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cot
(#)
sec
)
holds
(
-
(
cot
(#)
sec
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
cot
(#)
sec
)
)
`|
Z
)
.
x
=
(
(
1
/
(
(
sin
.
x
)
^2
)
)
/
(
cos
.
x
)
)
-
(
(
(
cot
.
x
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
) )
proof
end;
::f.x=-cot.x*cosec.x
theorem
Th13
:
:: INTEGR14:13
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cot
(#)
cosec
)
holds
(
-
(
cot
(#)
cosec
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
cot
(#)
cosec
)
)
`|
Z
)
.
x
=
(
(
1
/
(
(
sin
.
x
)
^2
)
)
/
(
sin
.
x
)
)
+
(
(
(
cot
.
x
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x=-cos.x * cot.x
theorem
Th14
:
:: INTEGR14:14
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
cos
(#)
cot
)
holds
(
-
(
cos
(#)
cot
)
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
-
(
cos
(#)
cot
)
)
`|
Z
)
.
x
=
(
cos
.
x
)
+
(
(
cos
.
x
)
/
(
(
sin
.
x
)
^2
)
)
) )
proof
end;
::f.x=sin.
1/x
/
x^2*(cos.(1/x
)^2)
theorem
:: INTEGR14:15
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
sin
.
(
1
/
x
)
)
/
(
(
x
^2
)
*
(
(
cos
.
(
1
/
x
)
)
^2
)
)
) &
Z
c=
dom
(
sec
*
(
(
id
Z
)
^
)
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
sec
*
(
(
id
Z
)
^
)
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
sec
*
(
(
id
Z
)
^
)
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.
1/x
/
x^2*(sin.(1/x
)^2)
theorem
:: INTEGR14:16
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
cos
.
(
1
/
x
)
)
/
(
(
x
^2
)
*
(
(
sin
.
(
1
/
x
)
)
^2
)
)
) &
Z
c=
dom
(
cosec
*
(
(
id
Z
)
^
)
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
cosec
*
(
(
id
Z
)
^
)
)
.
(
upper_bound
A
)
)
-
(
(
cosec
*
(
(
id
Z
)
^
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x*sin.
exp_R.x
/
cos.(exp_R.x
)^2
theorem
:: INTEGR14:17
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
exp_R
.
x
)
*
(
sin
.
(
exp_R
.
x
)
)
)
/
(
(
cos
.
(
exp_R
.
x
)
)
^2
)
) &
Z
c=
dom
(
sec
*
exp_R
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
sec
*
exp_R
)
.
(
upper_bound
A
)
)
-
(
(
sec
*
exp_R
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x*cos.
exp_R.x
/
sin.(exp_R.x
)^2
theorem
:: INTEGR14:18
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
exp_R
.
x
)
*
(
cos
.
(
exp_R
.
x
)
)
)
/
(
(
sin
.
(
exp_R
.
x
)
)
^2
)
) &
Z
c=
dom
(
cosec
*
exp_R
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cosec
*
exp_R
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cosec
*
exp_R
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.
ln.x
/
x*(cos.(ln.x
)^2)
theorem
:: INTEGR14:19
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
sin
.
(
ln
.
x
)
)
/
(
x
*
(
(
cos
.
(
ln
.
x
)
)
^2
)
)
) &
Z
c=
dom
(
sec
*
ln
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
sec
*
ln
)
.
(
upper_bound
A
)
)
-
(
(
sec
*
ln
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.
ln.x
/
x*(sin.(ln.x
)^2)
theorem
:: INTEGR14:20
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
cos
.
(
ln
.
x
)
)
/
(
x
*
(
(
sin
.
(
ln
.
x
)
)
^2
)
)
) &
Z
c=
dom
(
cosec
*
ln
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cosec
*
ln
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cosec
*
ln
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.
sec.x
*sin.x/
cos.x
^2
theorem
:: INTEGR14:21
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
f
=
(
exp_R
*
sec
)
(#)
(
sin
/
(
cos
^2
)
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
exp_R
*
sec
)
.
(
upper_bound
A
)
)
-
(
(
exp_R
*
sec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.
cosec.x
*cos.x/
sin.x
^2
theorem
:: INTEGR14:22
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
f
=
(
exp_R
*
cosec
)
(#)
(
cos
/
(
sin
^2
)
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
exp_R
*
cosec
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
exp_R
*
cosec
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=tan.x
theorem
:: INTEGR14:23
for
A
being non
empty
closed_interval
Subset
of
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
dom
(
ln
*
sec
)
&
Z
=
dom
tan
&
tan
|
A
is
continuous
holds
integral
(
tan
,
A
)
=
(
(
ln
*
sec
)
.
(
upper_bound
A
)
)
-
(
(
ln
*
sec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=-cot.x
theorem
:: INTEGR14:24
for
A
being non
empty
closed_interval
Subset
of
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
dom
(
ln
*
cosec
)
&
Z
=
dom
cot
&
(
-
cot
)
|
A
is
continuous
holds
integral
(
(
-
cot
)
,
A
)
=
(
(
ln
*
cosec
)
.
(
upper_bound
A
)
)
-
(
(
ln
*
cosec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cot.x
theorem
:: INTEGR14:25
for
A
being non
empty
closed_interval
Subset
of
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
dom
(
ln
*
cosec
)
&
Z
=
dom
cot
&
cot
|
A
is
continuous
holds
integral
(
cot
,
A
)
=
(
(
-
(
ln
*
cosec
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
ln
*
cosec
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=n*sin.x/
cos.x
#Z
n+1
theorem
:: INTEGR14:26
for
n
being
Nat
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
n
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
#Z
(
n
+
1
)
)
) &
Z
c=
dom
(
(
#Z
n
)
*
sec
)
& 1
<=
n
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
(
#Z
n
)
*
sec
)
.
(
upper_bound
A
)
)
-
(
(
(
#Z
n
)
*
sec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=n*cos.x/
sin.x
#Z
n+1
theorem
:: INTEGR14:27
for
n
being
Nat
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
n
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
#Z
(
n
+
1
)
)
) &
Z
c=
dom
(
(
#Z
n
)
*
cosec
)
& 1
<=
n
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
(
#Z
n
)
*
cosec
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
(
#Z
n
)
*
cosec
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x/cos.x+exp_R.x*sin.x/
cos.x
^2
theorem
:: INTEGR14:28
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
exp_R
.
x
)
/
(
cos
.
x
)
)
+
(
(
(
exp_R
.
x
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
) &
Z
c=
dom
(
exp_R
(#)
sec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
exp_R
(#)
sec
)
.
(
upper_bound
A
)
)
-
(
(
exp_R
(#)
sec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x/sin.x-exp_R.x*cos.x/
sin.x
^2
theorem
:: INTEGR14:29
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
exp_R
.
x
)
/
(
sin
.
x
)
)
-
(
(
(
exp_R
.
x
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
exp_R
(#)
cosec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
exp_R
(#)
cosec
)
.
(
upper_bound
A
)
)
-
(
(
exp_R
(#)
cosec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=
sin.(a*x
-
cos.(a*x
)^2)/
cos.(a*x
)^2
theorem
:: INTEGR14:30
for
a
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
sin
.
(
a
*
x
)
)
-
(
(
cos
.
(
a
*
x
)
)
^2
)
)
/
(
(
cos
.
(
a
*
x
)
)
^2
)
) &
Z
c=
dom
(
(
(
1
/
a
)
(#)
(
sec
*
f1
)
)
-
(
id
Z
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
*
x
&
a
<>
0
) ) &
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
(
(
1
/
a
)
(#)
(
sec
*
f1
)
)
-
(
id
Z
)
)
.
(
upper_bound
A
)
)
-
(
(
(
(
1
/
a
)
(#)
(
sec
*
f1
)
)
-
(
id
Z
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=
cos.(a*x
-
sin.(a*x
)^2)/
sin.(a*x
)^2
theorem
:: INTEGR14:31
for
a
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
f1
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
cos
.
(
a
*
x
)
)
-
(
(
sin
.
(
a
*
x
)
)
^2
)
)
/
(
(
sin
.
(
a
*
x
)
)
^2
)
) &
Z
c=
dom
(
(
(
-
(
1
/
a
)
)
(#)
(
cosec
*
f1
)
)
-
(
id
Z
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
*
x
&
a
<>
0
) ) &
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
(
(
-
(
1
/
a
)
)
(#)
(
cosec
*
f1
)
)
-
(
id
Z
)
)
.
(
upper_bound
A
)
)
-
(
(
(
(
-
(
1
/
a
)
)
(#)
(
cosec
*
f1
)
)
-
(
id
Z
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/cos.x/x+ln.x*sin.x/
cos.x
^2
theorem
:: INTEGR14:32
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
1
/
(
cos
.
x
)
)
/
x
)
+
(
(
(
ln
.
x
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
) &
Z
c=
dom
(
ln
(#)
sec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
ln
(#)
sec
)
.
(
upper_bound
A
)
)
-
(
(
ln
(#)
sec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/sin.x/x-ln.x*cos.x/
sin.x
^2
theorem
:: INTEGR14:33
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
1
/
(
sin
.
x
)
)
/
x
)
-
(
(
(
ln
.
x
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
ln
(#)
cosec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
ln
(#)
cosec
)
.
(
upper_bound
A
)
)
-
(
(
ln
(#)
cosec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/cos.x/x^2-sin.x/x/
cos.x
^2
theorem
:: INTEGR14:34
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
1
/
(
cos
.
x
)
)
/
(
x
^2
)
)
-
(
(
(
sin
.
x
)
/
x
)
/
(
(
cos
.
x
)
^2
)
)
) &
Z
c=
dom
(
(
(
id
Z
)
^
)
(#)
sec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
(
(
id
Z
)
^
)
(#)
sec
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
(
(
id
Z
)
^
)
(#)
sec
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/sin.x/x^2+cos.x/x/
sin.x
^2
theorem
:: INTEGR14:35
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
1
/
(
sin
.
x
)
)
/
(
x
^2
)
)
+
(
(
(
cos
.
x
)
/
x
)
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
(
(
id
Z
)
^
)
(#)
cosec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
(
(
id
Z
)
^
)
(#)
cosec
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
(
(
id
Z
)
^
)
(#)
cosec
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.x*sin.
sin.x
/
cos.(sin.x
)^2
theorem
:: INTEGR14:36
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
cos
.
x
)
*
(
sin
.
(
sin
.
x
)
)
)
/
(
(
cos
.
(
sin
.
x
)
)
^2
)
) &
Z
c=
dom
(
sec
*
sin
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
sec
*
sin
)
.
(
upper_bound
A
)
)
-
(
(
sec
*
sin
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.x*sin.
cos.x
/
cos.(cos.x
)^2
theorem
:: INTEGR14:37
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
sin
.
x
)
*
(
sin
.
(
cos
.
x
)
)
)
/
(
(
cos
.
(
cos
.
x
)
)
^2
)
) &
Z
c=
dom
(
sec
*
cos
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
sec
*
cos
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
sec
*
cos
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.x*cos.
sin.x
/
sin.(sin.x
)^2
theorem
:: INTEGR14:38
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
cos
.
x
)
*
(
cos
.
(
sin
.
x
)
)
)
/
(
(
sin
.
(
sin
.
x
)
)
^2
)
) &
Z
c=
dom
(
cosec
*
sin
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cosec
*
sin
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cosec
*
sin
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.x*cos.
cos.x
/
sin.(cos.x
)^2
theorem
:: INTEGR14:39
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
sin
.
x
)
*
(
cos
.
(
cos
.
x
)
)
)
/
(
(
sin
.
(
cos
.
x
)
)
^2
)
) &
Z
c=
dom
(
cosec
*
cos
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
cosec
*
cos
)
.
(
upper_bound
A
)
)
-
(
(
cosec
*
cos
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.
tan.x
/
cos.x
^2/
cos.(tan.x
)^2
theorem
:: INTEGR14:40
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
sin
.
(
tan
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
/
(
(
cos
.
(
tan
.
x
)
)
^2
)
) &
Z
c=
dom
(
sec
*
tan
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
sec
*
tan
)
.
(
upper_bound
A
)
)
-
(
(
sec
*
tan
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.
cot.x
/
sin.x
^2/
cos.(cot.x
)^2
theorem
:: INTEGR14:41
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
sin
.
(
cot
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
/
(
(
cos
.
(
cot
.
x
)
)
^2
)
) &
Z
c=
dom
(
sec
*
cot
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
sec
*
cot
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
sec
*
cot
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x= cos.
tan.x
/
cos.x
^2/
sin.(tan.x
)^2
theorem
:: INTEGR14:42
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
cos
.
(
tan
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
/
(
(
sin
.
(
tan
.
x
)
)
^2
)
) &
Z
c=
dom
(
cosec
*
tan
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cosec
*
tan
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cosec
*
tan
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.
cot.x
/
sin.x
^2/
sin.(cot.x
)^2
theorem
:: INTEGR14:43
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
cos
.
(
cot
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
/
(
(
sin
.
(
cot
.
x
)
)
^2
)
) &
Z
c=
dom
(
cosec
*
cot
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
cosec
*
cot
)
.
(
upper_bound
A
)
)
-
(
(
cosec
*
cot
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/
cos.x
^2/cos.x+tan.x*sin.x/
cos.x
^2
theorem
:: INTEGR14:44
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
1
/
(
(
cos
.
x
)
^2
)
)
/
(
cos
.
x
)
)
+
(
(
(
tan
.
x
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
) &
Z
c=
dom
(
tan
(#)
sec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
tan
(#)
sec
)
.
(
upper_bound
A
)
)
-
(
(
tan
(#)
sec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/
sin.x
^2/cos.x-cot.x*sin.x/
cos.x
^2
theorem
:: INTEGR14:45
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
1
/
(
(
sin
.
x
)
^2
)
)
/
(
cos
.
x
)
)
-
(
(
(
cot
.
x
)
*
(
sin
.
x
)
)
/
(
(
cos
.
x
)
^2
)
)
) &
Z
c=
dom
(
cot
(#)
sec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cot
(#)
sec
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cot
(#)
sec
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/
cos.x
^2/sin.x-tan.x*cos.x/
sin.x
^2
theorem
:: INTEGR14:46
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
1
/
(
(
cos
.
x
)
^2
)
)
/
(
sin
.
x
)
)
-
(
(
(
tan
.
x
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
tan
(#)
cosec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
tan
(#)
cosec
)
.
(
upper_bound
A
)
)
-
(
(
tan
(#)
cosec
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/
sin.x
^2/sin.x+cot.x*cos.x/
sin.x
^2
theorem
:: INTEGR14:47
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
(
1
/
(
(
sin
.
x
)
^2
)
)
/
(
sin
.
x
)
)
+
(
(
(
cot
.
x
)
*
(
cos
.
x
)
)
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
cot
(#)
cosec
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cot
(#)
cosec
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cot
(#)
cosec
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/
cos.(cot.x
)^2*
1/(sin.x
^2)
theorem
:: INTEGR14:48
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
1
/
(
(
cos
.
(
cot
.
x
)
)
^2
)
)
*
(
1
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
tan
*
cot
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
tan
*
cot
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
tan
*
cot
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/
cos.(tan.x
)^2 *
1/(cos.x
^2)
theorem
:: INTEGR14:49
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
1
/
(
(
cos
.
(
tan
.
x
)
)
^2
)
)
*
(
1
/
(
(
cos
.
x
)
^2
)
)
) &
Z
c=
dom
(
tan
*
tan
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
tan
*
tan
)
.
(
upper_bound
A
)
)
-
(
(
tan
*
tan
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=
1/(sin.(cot.x
)^2) *
1/(sin.x
^2)
theorem
:: INTEGR14:50
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
1
/
(
(
sin
.
(
cot
.
x
)
)
^2
)
)
*
(
1
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
cot
*
cot
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
cot
*
cot
)
.
(
upper_bound
A
)
)
-
(
(
cot
*
cot
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=
1/(sin.(tan.x
)^2)*
1/(cos.x
^2)
theorem
:: INTEGR14:51
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
1
/
(
(
sin
.
(
tan
.
x
)
)
^2
)
)
*
(
1
/
(
(
cos
.
x
)
^2
)
)
) &
Z
c=
dom
(
cot
*
tan
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cot
*
tan
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cot
*
tan
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/
cos.x
^2+1/
sin.x
^2
theorem
:: INTEGR14:52
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
1
/
(
(
cos
.
x
)
^2
)
)
+
(
1
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
tan
-
cot
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
tan
-
cot
)
.
(
upper_bound
A
)
)
-
(
(
tan
-
cot
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/
cos.x
^2-1/
sin.x
^2
theorem
:: INTEGR14:53
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
1
/
(
(
cos
.
x
)
^2
)
)
-
(
1
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
tan
+
cot
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
tan
+
cot
)
.
(
upper_bound
A
)
)
-
(
(
tan
+
cot
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.
sin.x
*cos.x
theorem
:: INTEGR14:54
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
cos
.
(
sin
.
x
)
)
*
(
cos
.
x
)
) &
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
sin
*
sin
)
.
(
upper_bound
A
)
)
-
(
(
sin
*
sin
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.
cos.x
*sin.x
theorem
:: INTEGR14:55
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
cos
.
(
cos
.
x
)
)
*
(
sin
.
x
)
) &
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
sin
*
cos
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
sin
*
cos
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.
sin.x
*cos.x
theorem
:: INTEGR14:56
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
sin
.
(
sin
.
x
)
)
*
(
cos
.
x
)
) &
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cos
*
sin
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cos
*
sin
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.
cos.x
*sin.x
theorem
:: INTEGR14:57
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
sin
.
(
cos
.
x
)
)
*
(
sin
.
x
)
) &
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
cos
*
cos
)
.
(
upper_bound
A
)
)
-
(
(
cos
*
cos
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.x+cos.x/
sin.x
^2
theorem
:: INTEGR14:58
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
cos
.
x
)
+
(
(
cos
.
x
)
/
(
(
sin
.
x
)
^2
)
)
) &
Z
c=
dom
(
cos
(#)
cot
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
cos
(#)
cot
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cos
(#)
cot
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.x + sin.x/
cos.x
^2
theorem
:: INTEGR14:59
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
& ( for
x
being
Real
st
x
in
Z
holds
f
.
x
=
(
sin
.
x
)
+
(
(
sin
.
x
)
/
(
(
cos
.
x
)
^2
)
)
) &
Z
c=
dom
(
sin
(#)
tan
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
sin
(#)
tan
)
.
(
upper_bound
A
)
)
-
(
(
sin
(#)
tan
)
.
(
lower_bound
A
)
)
proof
end;