:: Integrability Formulas -- Part {I}
:: by Bo Li and Na Ma
::
:: Received November 7, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users
theorem
Th1
:
:: INTEGR12:1
for
f1
,
f2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
Z
c=
dom
(
(
f1
+
f2
)
^
)
& ( for
x
being
Real
st
x
in
Z
holds
f1
.
x
=
1 ) &
f2
=
#Z
2 holds
(
(
f1
+
f2
)
^
is_differentiable_on
Z
& ( for
x
being
Real
st
x
in
Z
holds
(
(
(
f1
+
f2
)
^
)
`|
Z
)
.
x
=
-
(
(
2
*
x
)
/
(
(
1
+
(
x
|^
2
)
)
^2
)
)
) )
proof
end;
::f.x=1/((1+x^2)*arccot.x)
theorem
:: INTEGR12:2
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
f2
,
g1
,
g2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
f
=
(
(
g1
+
g2
)
^
)
/
f2
&
f2
=
arccot
&
Z
c=
].
(
-
1
)
,1
.[
&
g2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
g1
.
x
=
1 &
f2
.
x
>
0
) ) &
Z
=
dom
f
holds
integral
(
f
,
A
)
=
(
(
-
(
ln
*
arccot
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
ln
*
arccot
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x/(1+(exp_R.x)^2)
theorem
:: INTEGR12:3
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
(
exp_R
.
x
<
1 &
f1
.
x
=
1 ) ) &
Z
c=
dom
(
arctan
*
exp_R
)
&
Z
=
dom
f
&
f
=
exp_R
/
(
f1
+
(
exp_R
^2
)
)
holds
integral
(
f
,
A
)
=
(
(
arctan
*
exp_R
)
.
(
upper_bound
A
)
)
-
(
(
arctan
*
exp_R
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=-exp_R.x/(1+(exp_R.x)^2)
theorem
:: INTEGR12:4
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
(
exp_R
.
x
<
1 &
f1
.
x
=
1 ) ) &
Z
c=
dom
(
arccot
*
exp_R
)
&
Z
=
dom
f
&
f
=
(
-
exp_R
)
/
(
f1
+
(
exp_R
^2
)
)
holds
integral
(
f
,
A
)
=
(
(
arccot
*
exp_R
)
.
(
upper_bound
A
)
)
-
(
(
arccot
*
exp_R
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x*sin.x/cos.x+exp_R.x/(cos.x)^2
theorem
:: INTEGR12:5
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
&
Z
=
dom
f
&
f
=
(
exp_R
(#)
(
sin
/
cos
)
)
+
(
exp_R
/
(
cos
^2
)
)
holds
integral
(
f
,
A
)
=
(
(
exp_R
(#)
tan
)
.
(
upper_bound
A
)
)
-
(
(
exp_R
(#)
tan
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x*cos.x/sin.x-exp_R.x/(sin.x)^2
theorem
:: INTEGR12:6
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
&
Z
=
dom
f
&
f
=
(
exp_R
(#)
(
cos
/
sin
)
)
-
(
exp_R
/
(
sin
^2
)
)
holds
integral
(
f
,
A
)
=
(
(
exp_R
(#)
cot
)
.
(
upper_bound
A
)
)
-
(
(
exp_R
(#)
cot
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x*arctan.x+exp_R.x/(1+x^2)
theorem
:: INTEGR12:7
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
f1
.
x
=
1 ) &
Z
c=
].
(
-
1
)
,1
.[
&
Z
=
dom
f
&
f
=
(
exp_R
(#)
arctan
)
+
(
exp_R
/
(
f1
+
(
#Z
2
)
)
)
holds
integral
(
f
,
A
)
=
(
(
exp_R
(#)
arctan
)
.
(
upper_bound
A
)
)
-
(
(
exp_R
(#)
arctan
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x*arccot.x-exp_R.x/(1+x^2)
theorem
:: INTEGR12:8
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
f1
.
x
=
1 ) &
Z
c=
].
(
-
1
)
,1
.[
&
Z
=
dom
f
&
f
=
(
exp_R
(#)
arccot
)
-
(
exp_R
/
(
f1
+
(
#Z
2
)
)
)
holds
integral
(
f
,
A
)
=
(
(
exp_R
(#)
arccot
)
.
(
upper_bound
A
)
)
-
(
(
exp_R
(#)
arccot
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.(sin.x) * cos.x
theorem
:: INTEGR12:9
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
&
Z
=
dom
f
&
f
=
(
exp_R
*
sin
)
(#)
cos
holds
integral
(
f
,
A
)
=
(
(
exp_R
*
sin
)
.
(
upper_bound
A
)
)
-
(
(
exp_R
*
sin
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.(cos.x) * sin.x
theorem
:: INTEGR12:10
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
&
Z
=
dom
f
&
f
=
(
exp_R
*
cos
)
(#)
sin
holds
integral
(
f
,
A
)
=
(
(
-
(
exp_R
*
cos
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
exp_R
*
cos
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.(ln.x)/x
theorem
:: INTEGR12:11
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
x
>
0
) &
Z
=
dom
f
&
f
=
(
cos
*
ln
)
(#)
(
(
id
Z
)
^
)
holds
integral
(
f
,
A
)
=
(
(
sin
*
ln
)
.
(
upper_bound
A
)
)
-
(
(
sin
*
ln
)
.
(
lower_bound
A
)
)
proof
end;
Lm1
:
right_open_halfline
0
=
{
g
where
g
is
Real
:
0
<
g
}
by
XXREAL_1:230
;
::f.x=sin.(ln.x)/x
theorem
:: INTEGR12:12
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
x
>
0
) &
Z
=
dom
f
&
f
=
(
sin
*
ln
)
(#)
(
(
id
Z
)
^
)
holds
integral
(
f
,
A
)
=
(
(
-
(
cos
*
ln
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cos
*
ln
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=exp_R.x * cos.(exp_R.x)
theorem
:: INTEGR12:13
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
&
Z
=
dom
f
&
f
=
exp_R
(#)
(
cos
*
exp_R
)
holds
integral
(
f
,
A
)
=
(
(
sin
*
exp_R
)
.
(
upper_bound
A
)
)
-
(
(
sin
*
exp_R
)
.
(
lower_bound
A
)
)
proof
end;
::f.x = exp_R.x * sin.(exp_R.x)
theorem
:: INTEGR12:14
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
&
Z
=
dom
f
&
f
=
exp_R
(#)
(
sin
*
exp_R
)
holds
integral
(
f
,
A
)
=
(
(
-
(
cos
*
exp_R
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
cos
*
exp_R
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=arctan.(x/r)
theorem
:: INTEGR12:15
for
r
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
g
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
dom
(
ln
*
(
f1
+
f2
)
)
&
r
<>
0
& ( for
x
being
Real
st
x
in
Z
holds
(
g
.
x
=
x
/
r
&
g
.
x
>
-
1 &
g
.
x
<
1 &
f1
.
x
=
1 ) ) &
f2
=
(
#Z
2
)
*
g
&
Z
=
dom
f
&
f
=
arctan
*
g
holds
integral
(
f
,
A
)
=
(
(
(
(
id
Z
)
(#)
(
arctan
*
g
)
)
-
(
(
r
/
2
)
(#)
(
ln
*
(
f1
+
f2
)
)
)
)
.
(
upper_bound
A
)
)
-
(
(
(
(
id
Z
)
(#)
(
arctan
*
g
)
)
-
(
(
r
/
2
)
(#)
(
ln
*
(
f1
+
f2
)
)
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=arccot.(x/r)
theorem
:: INTEGR12:16
for
r
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
g
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
dom
(
ln
*
(
f1
+
f2
)
)
&
r
<>
0
& ( for
x
being
Real
st
x
in
Z
holds
(
g
.
x
=
x
/
r
&
g
.
x
>
-
1 &
g
.
x
<
1 &
f1
.
x
=
1 ) ) &
f2
=
(
#Z
2
)
*
g
&
Z
=
dom
f
&
f
=
arccot
*
g
holds
integral
(
f
,
A
)
=
(
(
(
(
id
Z
)
(#)
(
arccot
*
g
)
)
+
(
(
r
/
2
)
(#)
(
ln
*
(
f1
+
f2
)
)
)
)
.
(
upper_bound
A
)
)
-
(
(
(
(
id
Z
)
(#)
(
arccot
*
g
)
)
+
(
(
r
/
2
)
(#)
(
ln
*
(
f1
+
f2
)
)
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=arctan.(x/r)+x/(r*(1+(x/r)^2))
theorem
:: INTEGR12:17
for
r
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
g
,
f1
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
f
=
(
arctan
*
f1
)
+
(
(
id
Z
)
/
(
r
(#)
(
g
+
(
f1
^2
)
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
g
.
x
=
1 &
f1
.
x
=
x
/
r
&
f1
.
x
>
-
1 &
f1
.
x
<
1 ) ) &
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
(
id
Z
)
(#)
(
arctan
*
f1
)
)
.
(
upper_bound
A
)
)
-
(
(
(
id
Z
)
(#)
(
arctan
*
f1
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=arccot.(x/r)-x/(r*(1+(x/r)^2))
theorem
:: INTEGR12:18
for
r
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
g
,
f1
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
f
=
(
arccot
*
f1
)
-
(
(
id
Z
)
/
(
r
(#)
(
g
+
(
f1
^2
)
)
)
)
& ( for
x
being
Real
st
x
in
Z
holds
(
g
.
x
=
1 &
f1
.
x
=
x
/
r
&
f1
.
x
>
-
1 &
f1
.
x
<
1 ) ) &
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
(
id
Z
)
(#)
(
arccot
*
f1
)
)
.
(
upper_bound
A
)
)
-
(
(
(
id
Z
)
(#)
(
arccot
*
f1
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=n*(arcsin.x) #Z (n-1) / sqrt(1-x^2)
theorem
:: INTEGR12:19
for
n
being
Element
of
NAT
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
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
f1
.
x
=
1 ) &
Z
=
dom
f
&
Z
c=
dom
(
(
#Z
n
)
*
arcsin
)
& 1
<
n
&
f
=
(
n
(#)
(
(
#Z
(
n
-
1
)
)
*
arcsin
)
)
/
(
(
#R
(
1
/
2
)
)
*
(
f1
-
(
#Z
2
)
)
)
holds
integral
(
f
,
A
)
=
(
(
(
#Z
n
)
*
arcsin
)
.
(
upper_bound
A
)
)
-
(
(
(
#Z
n
)
*
arcsin
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=n*(arccos.x) #Z (n-1) / sqrt(1-x^2)
theorem
:: INTEGR12:20
for
n
being
Element
of
NAT
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
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
f1
.
x
=
1 ) &
Z
c=
dom
(
(
#Z
n
)
*
arccos
)
&
Z
=
dom
f
& 1
<
n
&
f
=
(
n
(#)
(
(
#Z
(
n
-
1
)
)
*
arccos
)
)
/
(
(
#R
(
1
/
2
)
)
*
(
f1
-
(
#Z
2
)
)
)
holds
integral
(
f
,
A
)
=
(
(
-
(
(
#Z
n
)
*
arccos
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
(
#Z
n
)
*
arccos
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=arcsin.x+x/sqrt(1-x^2)
theorem
:: INTEGR12:21
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
f1
.
x
=
1 ) &
Z
c=
].
(
-
1
)
,1
.[
&
Z
=
dom
f
&
f
=
arcsin
+
(
(
id
Z
)
/
(
(
#R
(
1
/
2
)
)
*
(
f1
-
(
#Z
2
)
)
)
)
holds
integral
(
f
,
A
)
=
(
(
(
id
Z
)
(#)
arcsin
)
.
(
upper_bound
A
)
)
-
(
(
(
id
Z
)
(#)
arcsin
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=arccos.x-x/sqrt(1-x^2)
theorem
:: INTEGR12:22
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
f1
.
x
=
1 ) &
Z
c=
].
(
-
1
)
,1
.[
&
Z
=
dom
f
&
f
=
arccos
-
(
(
id
Z
)
/
(
(
#R
(
1
/
2
)
)
*
(
f1
-
(
#Z
2
)
)
)
)
holds
integral
(
f
,
A
)
=
(
(
(
id
Z
)
(#)
arccos
)
.
(
upper_bound
A
)
)
-
(
(
(
id
Z
)
(#)
arccos
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=a*arcsin.x+(a*x+b)/sqrt(1-x^2)
theorem
:: INTEGR12:23
for
a
,
b
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
(
a
*
x
)
+
b
&
f2
.
x
=
1 ) ) &
Z
=
dom
f
&
f
=
(
a
(#)
arcsin
)
+
(
f1
/
(
(
#R
(
1
/
2
)
)
*
(
f2
-
(
#Z
2
)
)
)
)
holds
integral
(
f
,
A
)
=
(
(
f1
(#)
arcsin
)
.
(
upper_bound
A
)
)
-
(
(
f1
(#)
arcsin
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=a*arccos.x-(a*x+b)/sqrt(1-x^2)
theorem
:: INTEGR12:24
for
a
,
b
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
(
a
*
x
)
+
b
&
f2
.
x
=
1 ) ) &
Z
=
dom
f
&
f
=
(
a
(#)
arccos
)
-
(
f1
/
(
(
#R
(
1
/
2
)
)
*
(
f2
-
(
#Z
2
)
)
)
)
holds
integral
(
f
,
A
)
=
(
(
f1
(#)
arccos
)
.
(
upper_bound
A
)
)
-
(
(
f1
(#)
arccos
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=arcsin.(x/a)+x/(a*sqrt(1-(x/a)^2))
theorem
:: INTEGR12:25
for
a
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
g
,
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
(
g
.
x
=
1 &
f1
.
x
=
x
/
a
&
f1
.
x
>
-
1 &
f1
.
x
<
1 ) ) &
Z
=
dom
f
&
f
|
A
is
continuous
&
f
=
(
arcsin
*
f1
)
+
(
(
id
Z
)
/
(
a
(#)
(
(
#R
(
1
/
2
)
)
*
(
g
-
(
f1
^2
)
)
)
)
)
holds
integral
(
f
,
A
)
=
(
(
(
id
Z
)
(#)
(
arcsin
*
f1
)
)
.
(
upper_bound
A
)
)
-
(
(
(
id
Z
)
(#)
(
arcsin
*
f1
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=arccos.(x/a)-x/(a*sqrt(1-(x/a)^2))
theorem
:: INTEGR12:26
for
a
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
g
,
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
(
g
.
x
=
1 &
f1
.
x
=
x
/
a
&
f1
.
x
>
-
1 &
f1
.
x
<
1 ) ) &
Z
=
dom
f
&
f
|
A
is
continuous
&
f
=
(
arccos
*
f1
)
-
(
(
id
Z
)
/
(
a
(#)
(
(
#R
(
1
/
2
)
)
*
(
g
-
(
f1
^2
)
)
)
)
)
holds
integral
(
f
,
A
)
=
(
(
(
id
Z
)
(#)
(
arccos
*
f1
)
)
.
(
upper_bound
A
)
)
-
(
(
(
id
Z
)
(#)
(
arccos
*
f1
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x = n*(sin.x) #Z (n-1)/(cos.x) #Z (n+1)
theorem
:: INTEGR12:27
for
n
being
Element
of
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
&
f
=
(
n
(#)
(
(
#Z
(
n
-
1
)
)
*
sin
)
)
/
(
(
#Z
(
n
+
1
)
)
*
cos
)
& 1
<=
n
&
Z
c=
dom
(
(
#Z
n
)
*
tan
)
&
Z
=
dom
f
holds
integral
(
f
,
A
)
=
(
(
(
#Z
n
)
*
tan
)
.
(
upper_bound
A
)
)
-
(
(
(
#Z
n
)
*
tan
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=n*(cos.x) #Z (n-1)/(sin.x) #Z (n+1)
theorem
:: INTEGR12:28
for
n
being
Element
of
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
&
f
=
(
n
(#)
(
(
#Z
(
n
-
1
)
)
*
cos
)
)
/
(
(
#Z
(
n
+
1
)
)
*
sin
)
& 1
<=
n
&
Z
c=
dom
(
(
#Z
n
)
*
cot
)
&
Z
=
dom
f
holds
integral
(
f
,
A
)
=
(
(
-
(
(
#Z
n
)
*
cot
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
(
#Z
n
)
*
cot
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=(sin.(a*x))^2/(cos.(a*x))^2
theorem
:: INTEGR12:29
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
&
Z
c=
dom
(
tan
*
f1
)
&
f
=
(
(
sin
*
f1
)
^2
)
/
(
(
cos
*
f1
)
^2
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
*
x
&
a
<>
0
) ) &
Z
=
dom
f
holds
integral
(
f
,
A
)
=
(
(
(
(
1
/
a
)
(#)
(
tan
*
f1
)
)
-
(
id
Z
)
)
.
(
upper_bound
A
)
)
-
(
(
(
(
1
/
a
)
(#)
(
tan
*
f1
)
)
-
(
id
Z
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=(cos.(a*x))^2/(sin.(a*x))^2
theorem
:: INTEGR12: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
&
Z
c=
dom
(
cot
*
f1
)
&
f
=
(
(
cos
*
f1
)
^2
)
/
(
(
sin
*
f1
)
^2
)
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
a
*
x
&
a
<>
0
) ) &
Z
=
dom
f
holds
integral
(
f
,
A
)
=
(
(
(
(
-
(
1
/
a
)
)
(#)
(
cot
*
f1
)
)
-
(
id
Z
)
)
.
(
upper_bound
A
)
)
-
(
(
(
(
-
(
1
/
a
)
)
(#)
(
cot
*
f1
)
)
-
(
id
Z
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=a*sin.x/cos.x+(a*x+b)/(cos.x)^2
theorem
:: INTEGR12:31
for
a
,
b
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
f1
.
x
=
(
a
*
x
)
+
b
) &
Z
=
dom
f
&
f
=
(
a
(#)
(
sin
/
cos
)
)
+
(
f1
/
(
cos
^2
)
)
holds
integral
(
f
,
A
)
=
(
(
f1
(#)
tan
)
.
(
upper_bound
A
)
)
-
(
(
f1
(#)
tan
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=a*cos.x/sin.x-(a*x+b)/(sin.x)^2
theorem
:: INTEGR12:32
for
a
,
b
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
f1
.
x
=
(
a
*
x
)
+
b
) &
Z
=
dom
f
&
f
=
(
a
(#)
(
cos
/
sin
)
)
-
(
f1
/
(
sin
^2
)
)
holds
integral
(
f
,
A
)
=
(
(
f1
(#)
cot
)
.
(
upper_bound
A
)
)
-
(
(
f1
(#)
cot
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=(sin.x)^2/(cos.x)^2
theorem
:: INTEGR12: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
=
(
(
sin
.
x
)
^2
)
/
(
(
cos
.
x
)
^2
)
) &
Z
c=
dom
(
tan
-
(
id
Z
)
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
tan
-
(
id
Z
)
)
.
(
upper_bound
A
)
)
-
(
(
tan
-
(
id
Z
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=(cos.x)^2/(sin.x)^2
theorem
:: INTEGR12: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
=
(
(
cos
.
x
)
^2
)
/
(
(
sin
.
x
)
^2
)
) &
Z
c=
dom
(
(
-
cot
)
-
(
id
Z
)
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
(
-
cot
)
-
(
id
Z
)
)
.
(
upper_bound
A
)
)
-
(
(
(
-
cot
)
-
(
id
Z
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/(x*(1+(ln.x)^2))
theorem
:: INTEGR12: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
/
(
x
*
(
1
+
(
(
ln
.
x
)
^2
)
)
)
&
ln
.
x
>
-
1 &
ln
.
x
<
1 ) ) &
Z
c=
dom
(
arctan
*
ln
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
arctan
*
ln
)
.
(
upper_bound
A
)
)
-
(
(
arctan
*
ln
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=-1/(x*(1+(ln.x)^2))
theorem
:: INTEGR12: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
=
-
(
1
/
(
x
*
(
1
+
(
(
ln
.
x
)
^2
)
)
)
)
&
ln
.
x
>
-
1 &
ln
.
x
<
1 ) ) &
Z
c=
dom
(
arccot
*
ln
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
arccot
*
ln
)
.
(
upper_bound
A
)
)
-
(
(
arccot
*
ln
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=a / sqrt(1-(a*x+b)^2)
theorem
:: INTEGR12:37
for
a
,
b
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
=
a
/
(
sqrt
(
1
-
(
(
(
a
*
x
)
+
b
)
^2
)
)
)
&
f1
.
x
=
(
a
*
x
)
+
b
&
f1
.
x
>
-
1 &
f1
.
x
<
1 ) ) &
Z
c=
dom
(
arcsin
*
f1
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
arcsin
*
f1
)
.
(
upper_bound
A
)
)
-
(
(
arcsin
*
f1
)
.
(
lower_bound
A
)
)
proof
end;
theorem
:: INTEGR12:38
for
a
,
b
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
=
a
/
(
sqrt
(
1
-
(
(
(
a
*
x
)
+
b
)
^2
)
)
)
&
f1
.
x
=
(
a
*
x
)
+
b
&
f1
.
x
>
-
1 &
f1
.
x
<
1 ) ) &
Z
c=
dom
(
arccos
*
f1
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
arccos
*
f1
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
arccos
*
f1
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=x*(1-x #Z 2) #R (-1/2)
theorem
:: INTEGR12:39
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
g
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
f1
=
g
-
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
x
*
(
(
1
-
(
x
#Z
2
)
)
#R
(
-
(
1
/
2
)
)
)
&
g
.
x
=
1 &
f1
.
x
>
0
) ) &
Z
c=
dom
(
(
#R
(
1
/
2
)
)
*
f1
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
(
#R
(
1
/
2
)
)
*
f1
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
(
#R
(
1
/
2
)
)
*
f1
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=x*(a^2-x #Z 2) #R (-1/2)
theorem
:: INTEGR12:40
for
a
being
Real
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
g
,
f1
,
f2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
g
=
f1
-
f2
&
f2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
x
*
(
(
(
a
^2
)
-
(
x
#Z
2
)
)
#R
(
-
(
1
/
2
)
)
)
&
f1
.
x
=
a
^2
&
g
.
x
>
0
) ) &
Z
c=
dom
(
(
#R
(
1
/
2
)
)
*
g
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
-
(
(
#R
(
1
/
2
)
)
*
g
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
(
#R
(
1
/
2
)
)
*
g
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=cos.x/((sin.x) #Z (n+1))
theorem
:: INTEGR12:41
for
n
being
Element
of
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
&
n
>
0
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
(
cos
.
x
)
/
(
(
sin
.
x
)
#Z
(
n
+
1
)
)
&
sin
.
x
<>
0
) ) &
Z
c=
dom
(
(
#Z
n
)
*
(
sin
^
)
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
(
-
(
1
/
n
)
)
(#)
(
(
#Z
n
)
*
(
sin
^
)
)
)
.
(
upper_bound
A
)
)
-
(
(
(
-
(
1
/
n
)
)
(#)
(
(
#Z
n
)
*
(
sin
^
)
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=sin.x/((cos.x) #Z (n+1))
theorem
:: INTEGR12:42
for
n
being
Element
of
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
&
n
>
0
& ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
(
sin
.
x
)
/
(
(
cos
.
x
)
#Z
(
n
+
1
)
)
&
cos
.
x
<>
0
) ) &
Z
c=
dom
(
(
#Z
n
)
*
(
cos
^
)
)
&
Z
=
dom
f
&
f
|
A
is
continuous
holds
integral
(
f
,
A
)
=
(
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
cos
^
)
)
)
.
(
upper_bound
A
)
)
-
(
(
(
1
/
n
)
(#)
(
(
#Z
n
)
*
(
cos
^
)
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1/((1+x^2)*arccot.x)
theorem
:: INTEGR12:43
for
A
being non
empty
closed_interval
Subset
of
REAL
for
f
,
f2
,
g1
,
g2
being
PartFunc
of
REAL
,
REAL
for
Z
being
open
Subset
of
REAL
st
A
c=
Z
&
f
=
(
(
g1
+
g2
)
^
)
/
f2
&
f2
=
arccot
&
Z
c=
].
(
-
1
)
,1
.[
&
g2
=
#Z
2 & ( for
x
being
Real
st
x
in
Z
holds
(
f
.
x
=
1
/
(
(
1
+
(
x
^2
)
)
*
(
arccot
.
x
)
)
&
g1
.
x
=
1 &
f2
.
x
>
0
) ) &
Z
=
dom
f
holds
integral
(
f
,
A
)
=
(
(
-
(
ln
*
arccot
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
ln
*
arccot
)
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1 / (sqrt(1-x^2)*arcsin.x)
theorem
:: INTEGR12:44
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
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
(
arcsin
.
x
>
0
&
f1
.
x
=
1 ) ) &
Z
c=
dom
(
ln
*
arcsin
)
&
Z
=
dom
f
&
f
=
(
(
(
#R
(
1
/
2
)
)
*
(
f1
-
(
#Z
2
)
)
)
(#)
arcsin
)
^
holds
integral
(
f
,
A
)
=
(
(
ln
*
arcsin
)
.
(
upper_bound
A
)
)
-
(
(
ln
*
arcsin
)
.
(
lower_bound
A
)
)
proof
end;
::f.x=1 / (sqrt(1-x^2)*arccos.x)
theorem
:: INTEGR12:45
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
&
Z
c=
].
(
-
1
)
,1
.[
& ( for
x
being
Real
st
x
in
Z
holds
(
f1
.
x
=
1 &
arccos
.
x
>
0
) ) &
Z
c=
dom
(
ln
*
arccos
)
&
Z
=
dom
f
&
f
=
(
(
(
#R
(
1
/
2
)
)
*
(
f1
-
(
#Z
2
)
)
)
(#)
arccos
)
^
holds
integral
(
f
,
A
)
=
(
(
-
(
ln
*
arccos
)
)
.
(
upper_bound
A
)
)
-
(
(
-
(
ln
*
arccos
)
)
.
(
lower_bound
A
)
)
proof
end;