:: 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;