:: Integrability Formulas -- Part {III}
:: by Bo Li and Na Ma
::
:: Received February 4, 2010
:: Copyright (c) 2010-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies RELAT_1, FUNCT_1, ARYTM_1, SIN_COS, VALUED_1, NAT_1, INTEGRA1,
FDIFF_1, SQUARE_1, ARYTM_3, ORDINAL2, PREPOWER, REAL_1, PARTFUN1,
TAYLOR_1, CARD_1, ORDINAL4, RCOMP_1, INTEGRA5, XXREAL_0, SIN_COS4,
SUBSET_1, XBOOLE_0, TARSKI, NUMBERS, XXREAL_2, SEQ_4, MEASURE5;
notations TARSKI, XBOOLE_0, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS, VALUED_1,
XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, FUNCT_1, RELSET_1, PARTFUN1,
PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA5,
PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2, FDIFF_9, SIN_COS4, SEQ_4;
constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER,
INTEGRA5, SEQ_4, PARTFUN2, RFUNCT_1, FDIFF_9, SIN_COS4, RELSET_1,
INTEGRA1, COMSEQ_2, BINOP_2;
registrations NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1, RCOMP_1, RELSET_1,
MEASURE5, XREAL_0, SQUARE_1, PREPOWER;
requirements NUMERALS, SUBSET, ARITHM;
definitions TARSKI, XBOOLE_0;
equalities SIN_COS, VALUED_1, SIN_COS4, FDIFF_9, XCMPLX_0;
expansions TARSKI;
theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, TARSKI, XBOOLE_0, INTEGRA5,
SIN_COS, VALUED_1, XBOOLE_1, FDIFF_7, FDIFF_8, FDIFF_9, FDIFF_10,
SIN_COS9, RELAT_1, FDIFF_2;
begin :: Differentiation Formulas
reserve a,x for Real;
reserve n for Nat;
reserve A for non empty closed_interval Subset of REAL;
reserve f,f1 for PartFunc of REAL,REAL;
reserve Z for open Subset of REAL;
Lm1:
0 in Z implies (id Z)"{0} = {0}
proof
assume A1: 0 in Z;
thus (id Z)"{0} c= {0}
proof
let x be object; assume
A2: x in (id Z)"{0};
then x in dom id Z by FUNCT_1:def 7; then
A3: x in Z;
(id Z).x in {0} by A2,FUNCT_1:def 7;
hence thesis by A3,FUNCT_1:18;
end;
let x be object; assume x in {0}; then
A4: x = 0 by TARSKI:def 1; then
(id Z).x = 0 by A1,FUNCT_1:18; then
A5: (id Z).x in {0} by TARSKI:def 1;
x in dom id Z by A1,A4;
hence thesis by A5,FUNCT_1:def 7;
end;
theorem Th1:
Z c= dom (sec*((id Z)^)) implies (-sec*((id Z)^)) is_differentiable_on Z &
for x st x in Z holds
((-sec*((id Z)^))`|Z).x = sin.(1/x)/(x^2*(cos.(1/x))^2)
proof
assume
A1:Z c= dom (sec*((id Z)^));
then A2:Z c= dom (-sec*((id Z)^)) by VALUED_1:def 5;
A3:Z c= dom ((id Z)^) by A1,FUNCT_1:101;
A4:not 0 in Z
proof
assume A5: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A5; then
not 0 in {0} by A5,A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
then A6:(sec*((id Z)^)) is_differentiable_on Z by A1,FDIFF_9:8;
then A7:(-1)(#)(sec*((id Z)^)) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-sec*((id Z)^))`|Z).x = sin.(1/x)/(x^2*(cos.(1/x))^2)
proof
let x;
assume
A8:x in Z;
((-sec*((id Z)^))`|Z).x=((-1)(#)((sec*((id Z)^))`|Z)).x by A6,FDIFF_2:19
.=(-1)*(((sec*((id Z)^))`|Z).x) by VALUED_1:6
.=(-1)*(-sin.(1/x)/(x^2*(cos.(1/x))^2)) by A1,A4,A8,FDIFF_9:8
.=sin.(1/x)/(x^2*(cos.(1/x))^2);
hence thesis;
end;
hence thesis by A7;
end;
::f.x=-cosec.(exp_R.x)
theorem Th2:
Z c= dom (cosec*exp_R) implies -cosec*exp_R is_differentiable_on Z &
for x st x in Z holds ((-cosec*exp_R)`|Z).x
= exp_R.x*cos.(exp_R.x)/(sin.(exp_R.x))^2
proof
assume
A1:Z c= dom (cosec*exp_R);
then A2:Z c= dom (-cosec*exp_R) by VALUED_1:8;
A3:cosec*exp_R is_differentiable_on Z by A1,FDIFF_9:13;
then A4:(-1)(#)(cosec*exp_R) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-cosec*exp_R)`|Z).x
= exp_R.x*cos.(exp_R.x)/(sin.(exp_R.x))^2
proof
let x;
assume
A5:x in Z;
((-cosec*exp_R)`|Z).x=((-1)(#)((cosec*exp_R)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((cosec*exp_R)`|Z).x) by VALUED_1:6
.=(-1)*(-exp_R.x*cos.(exp_R.x)/(sin.(exp_R.x))^2)
by A1,A5,FDIFF_9:13
.=exp_R.x*cos.(exp_R.x)/(sin.(exp_R.x))^2;
hence thesis;
end;
hence thesis by A4;
end;
:: f.x = -cosec.(ln.x)
theorem Th3:
Z c= dom (cosec*ln) implies -cosec*ln is_differentiable_on Z &
for x st x in Z holds ((-cosec*ln)`|Z).x = cos.(ln.x)/(x*(sin.(ln.x))^2)
proof
assume
A1:Z c= dom (cosec*ln);
then A2:Z c= dom (-cosec*ln) by VALUED_1:8;
A3:cosec*ln is_differentiable_on Z by A1,FDIFF_9:15;
then A4:(-1)(#)(cosec*ln) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-cosec*ln)`|Z).x = cos.(ln.x)/(x*(sin.(ln.x))^2)
proof
let x;
assume
A5: x in Z;
((-cosec*ln)`|Z).x=((-1)(#)((cosec*ln)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((cosec*ln)`|Z).x) by VALUED_1:6
.=(-1)*(-cos.(ln.x)/(x*(sin.(ln.x))^2))
by A1,A5,FDIFF_9:15
.=cos.(ln.x)/(x*(sin.(ln.x))^2);
hence thesis;
end;
hence thesis by A4;
end;
:: f.x = -exp_R.(cosec.x)
theorem Th4:
Z c= dom (exp_R*cosec) implies -exp_R*cosec is_differentiable_on Z
& for x st x in Z holds
((-exp_R*cosec)`|Z).x = exp_R.(cosec.x)*cos.x/(sin.x)^2
proof
assume
A1:Z c= dom (exp_R*cosec);
then A2:Z c= dom (-exp_R*cosec) by VALUED_1:8;
A3:exp_R*cosec is_differentiable_on Z by A1,FDIFF_9:17;
then A4:(-1)(#)(exp_R*cosec) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-exp_R*cosec)`|Z).x = exp_R.(cosec.x)*cos.x/(sin.x)^2
proof
let x;
assume
A5:x in Z;
((-exp_R*cosec)`|Z).x=((-1)(#)((exp_R*cosec)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((exp_R*cosec)`|Z).x) by VALUED_1:6
.=(-1)*(-exp_R.(cosec.x)*cos.x/(sin.x)^2)
by A1,A5,FDIFF_9:17
.=exp_R.(cosec.x)*cos.x/(sin.x)^2;
hence thesis;
end;
hence thesis by A4;
end;
:: f.x = -ln.(cosec.x)
theorem Th5:
Z c= dom (ln*cosec) implies -ln*cosec is_differentiable_on Z
& for x st x in Z holds ((-ln*cosec)`|Z).x = cot.x
proof
assume
A1:Z c= dom (ln*cosec);
then A2:Z c= dom (-ln*cosec) by VALUED_1:8;
A3:ln*cosec is_differentiable_on Z by A1,FDIFF_9:19;
then A4:(-1)(#)(ln*cosec) is_differentiable_on Z by A2,FDIFF_1:20;
A5:for x st x in Z holds sin.x<>0
proof
let x;
assume x in Z;
then x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
for x st x in Z holds ((-ln*cosec)`|Z).x = cot.x
proof
let x;
assume
A6: x in Z;
((-ln*cosec)`|Z).x =((-1)(#)((ln*cosec)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((ln*cosec)`|Z).x) by VALUED_1:6
.=(-1)*(-cos.x/sin.x) by A1,A6,FDIFF_9:19
.=cot(x)
.=cot.x by A5,A6,SIN_COS9:16;
hence thesis;
end;
hence thesis by A4;
end;
::f.x=-(cosec.x) #Z n
theorem Th6:
Z c= dom (( #Z n)*cosec) & 1<=n
implies -( #Z n)*cosec is_differentiable_on Z & for x st x in Z holds
((-( #Z n)*cosec)`|Z).x = n*cos.x/(sin.x) #Z (n+1)
proof
assume
A1:Z c= dom (( #Z n)*cosec) & 1<=n;
then A2:Z c= dom (-( #Z n)*cosec) & 1<=n by VALUED_1:8;
A3:( #Z n)*cosec is_differentiable_on Z by A1,FDIFF_9:21;
then A4:(-1)(#)(( #Z n)*cosec) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-( #Z n)*cosec)`|Z).x = n*cos.x/(sin.x) #Z (n+1)
proof
let x;
assume
A5:x in Z;
((-( #Z n)*cosec)`|Z).x=((-1)(#)((( #Z n)*cosec)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((( #Z n)*cosec)`|Z).x) by VALUED_1:6
.=(-1)*(-n*cos.x/(sin.x) #Z (n+1)) by A1,A5,FDIFF_9:21
.=n*cos.x/(sin.x) #Z (n+1);
hence thesis;
end;
hence thesis by A4;
end;
::f.x= -1/x*sec.x
theorem Th7:
Z c= dom ((id Z)^(#)sec)
implies (-(id Z)^(#)sec) is_differentiable_on Z & for x st x in Z holds
((-(id Z)^(#)sec)`|Z).x = 1/cos.x/x^2-sin.x/x/(cos.x)^2
proof
assume
A1:Z c= dom ((id Z)^(#)sec);
then A2:Z c= dom (-(id Z)^(#)sec) by VALUED_1:8;
Z c= dom ((id Z)^) /\ dom sec by A1,VALUED_1:def 4;then
A3:Z c= dom ((id Z)^) by XBOOLE_1:18;
A4:not 0 in Z
proof
assume A5: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A5; then
not 0 in {0} by A5,A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
then A6:((id Z)^(#)sec) is_differentiable_on Z by A1,FDIFF_9:32;
then A7:(-1)(#)((id Z)^(#)sec) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-(id Z)^(#)sec)`|Z).x = 1/cos.x/x^2-sin.x/x/(cos.x)^2
proof
let x;
assume
A8: x in Z;
((-(id Z)^(#)sec)`|Z).x
= ((-1)(#)(((id Z)^(#)sec)`|Z)).x by A6,FDIFF_2:19
.= (-1)*((((id Z)^(#)sec)`|Z).x) by VALUED_1:6
.= (-1)*(-1/cos.x/x^2+sin.x/x/(cos.x)^2) by A1,A4,A8,FDIFF_9:32
.= 1/cos.x/x^2-sin.x/x/(cos.x)^2;
hence thesis;
end;
hence thesis by A7;
end;
::f.x=-1/x*cosec.x
theorem Th8:
Z c= dom ((id Z)^(#)cosec)
implies (-(id Z)^(#)cosec) is_differentiable_on Z & for x st x in Z holds
((-(id Z)^(#)cosec)`|Z).x = 1/sin.x/x^2+cos.x/x/(sin.x)^2
proof
assume
A1:Z c= dom ((id Z)^(#)cosec);
then A2:Z c= dom (-(id Z)^(#)cosec) by VALUED_1:8;
Z c= dom ((id Z)^) /\ dom cosec by A1,VALUED_1:def 4;then
A3:Z c= dom ((id Z)^) by XBOOLE_1:18;
A4:not 0 in Z
proof
assume A5: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A5; then
not 0 in {0} by A5,A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
then A6:((id Z)^(#)cosec) is_differentiable_on Z by A1,FDIFF_9:33;
then A7:(-1)(#)((id Z)^(#)cosec) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds
((-(id Z)^(#)cosec)`|Z).x = 1/sin.x/x^2+cos.x/x/(sin.x)^2
proof
let x;
assume
A8:x in Z;
((-(id Z)^(#)cosec)`|Z).x
= ((-1)(#)(((id Z)^(#)cosec)`|Z)).x by A6,FDIFF_2:19
.= (-1)*((((id Z)^(#)cosec)`|Z).x) by VALUED_1:6
.= (-1)*(-1/sin.x/x^2-cos.x/x/(sin.x)^2) by A1,A4,A8,FDIFF_9:33
.= 1/sin.x/x^2+cos.x/x/(sin.x)^2;
hence thesis;
end;
hence thesis by A7;
end;
::f.x = -cosec.(sin.x)
theorem Th9:
Z c= dom (cosec*sin) implies -cosec*sin is_differentiable_on Z &
for x st x in Z holds ((-cosec*sin)`|Z).x
= cos.x*cos.(sin.x)/(sin.(sin.x))^2
proof
assume
A1:Z c= dom (cosec*sin);
then A2:Z c= dom (-cosec*sin) by VALUED_1:8;
A3:cosec*sin is_differentiable_on Z by A1,FDIFF_9:36;
then A4:(-1)(#)(cosec*sin) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-cosec*sin)`|Z).x = cos.x*cos.(sin.x)/(sin.(sin.x))^2
proof
let x;
assume
A5:x in Z;
((-cosec*sin)`|Z).x=((-1)(#)((cosec*sin)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((cosec*sin)`|Z).x) by VALUED_1:6
.=(-1)*(-cos.x*cos.(sin.x)/(sin.(sin.x))^2) by A1,A5,FDIFF_9:36
.=cos.x*cos.(sin.x)/(sin.(sin.x))^2;
hence thesis;
end;
hence thesis by A4;
end;
::f.x=-sec.(cot.x)
theorem Th10:
Z c= dom (sec*cot) implies -sec*cot is_differentiable_on Z &
for x st x in Z holds ((-sec*cot)`|Z).x
= sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2
proof
assume
A1:Z c= dom (sec*cot);
then A2:Z c= dom (-sec*cot) by VALUED_1:8;
A3:sec*cot is_differentiable_on Z by A1,FDIFF_9:39;
then A4:(-1)(#)(sec*cot) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds
((-sec*cot)`|Z).x = sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2
proof
let x;
assume
A5: x in Z;
((-sec*cot)`|Z).x=((-1)(#)((sec*cot)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((sec*cot)`|Z).x) by VALUED_1:6
.=(-1)*(-sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2) by A1,A5,FDIFF_9:39
.=sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2;
hence thesis;
end;
hence thesis by A4;
end;
::f.x=-cosec.(tan.x)
theorem Th11:
Z c= dom (cosec*tan) implies -cosec*tan is_differentiable_on Z &
for x st x in Z holds ((-cosec*tan)`|Z).x
= cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2
proof
assume
A1:Z c= dom (cosec*tan);
then A2:Z c= dom (-cosec*tan) by VALUED_1:8;
A3:cosec*tan is_differentiable_on Z by A1,FDIFF_9:40;
dom (cosec*tan) c= dom tan by RELAT_1:25; then
A4: Z c= dom tan by A1;
A5:(-1)(#)(cosec*tan) is_differentiable_on Z by A2,A3,FDIFF_1:20;
A6:for x st x in Z holds sin.(tan.x)<>0
proof
let x;
assume x in Z;
then tan.x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
for x st x in Z holds ((-cosec*tan)`|Z).x
= cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2
proof
let x;
assume
A7: x in Z; then
A8: cos.x<>0 by A4,FDIFF_8:1; then
A9: tan is_differentiable_in x by FDIFF_7:46;
A10: sin.(tan.x)<>0 by A6,A7;then
A11: cosec is_differentiable_in tan.x by FDIFF_9:2;
A12: cosec*tan is_differentiable_in x by A3,A7,FDIFF_1:9;
((-cosec*tan)`|Z).x=diff(-cosec*tan,x) by A5,A7,FDIFF_1:def 7
.=(-1)*(diff(cosec*tan,x)) by A12,FDIFF_1:15
.=(-1)*(diff(cosec, tan.x)*diff(tan,x)) by A9,A11,FDIFF_2:13
.=(-1)*((-cos.(tan.x)/(sin.(tan.x))^2) * diff(tan,x)) by A10,FDIFF_9:2
.=(-1)*((1/(cos.x)^2)*(-cos.(tan.x)/(sin.(tan.x))^2)) by A8,FDIFF_7:46
.=cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2;
hence thesis;
end;
hence thesis by A5;
end;
::f.x=-cot.x*sec.x
theorem Th12:
Z c= dom (cot(#)sec) implies (-cot(#)sec) is_differentiable_on Z &
for x st x in Z holds
((-cot(#)sec)`|Z).x = 1/(sin.x)^2/cos.x-cot.x*sin.x/(cos.x)^2
proof
assume
A1:Z c= dom (cot(#)sec);
then A2:Z c= dom (-cot(#)sec) by VALUED_1:8;
A3:cot(#)sec is_differentiable_on Z by A1,FDIFF_9:43;
then A4:(-1)(#)(cot(#)sec) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds
((-cot(#)sec)`|Z).x = 1/(sin.x)^2/cos.x-cot.x*sin.x/(cos.x)^2
proof
let x;
assume
A5: x in Z;
((-cot(#)sec)`|Z).x = ((-1)(#)((cot(#)sec)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((cot(#)sec)`|Z).x) by VALUED_1:6
.=(-1)*(-1/(sin.x)^2/cos.x+cot.x*sin.x/(cos.x)^2) by A1,A5,FDIFF_9:43
.=1/(sin.x)^2/cos.x-cot.x*sin.x/(cos.x)^2;
hence thesis;
end;
hence thesis by A4;
end;
::f.x=-cot.x*cosec.x
theorem Th13:
Z c= dom (cot(#)cosec) implies (-cot(#)cosec) is_differentiable_on Z &
for x st x in Z holds
((-cot(#)cosec)`|Z).x = 1/(sin.x)^2/sin.x+cot.x*cos.x/(sin.x)^2
proof
assume
A1:Z c= dom (cot(#)cosec);
then A2:Z c= dom (-cot(#)cosec) by VALUED_1:8;
A3:(cot(#)cosec) is_differentiable_on Z by A1,FDIFF_9:45;
then A4:(-1)(#)(cot(#)cosec) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds
((-cot(#)cosec)`|Z).x = 1/(sin.x)^2/sin.x+cot.x*cos.x/(sin.x)^2
proof
let x;
assume
A5:x in Z;
((-cot(#)cosec)`|Z).x = ((-1)(#)((cot(#)cosec)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((cot(#)cosec)`|Z).x) by VALUED_1:6
.=(-1)*(-1/(sin.x)^2/sin.x-cot.x*cos.x/(sin.x)^2) by A1,A5,FDIFF_9:45
.=1/(sin.x)^2/sin.x+cot.x*cos.x/(sin.x)^2;
hence thesis;
end;
hence thesis by A4;
end;
::f.x=-cos.x * cot.x
theorem Th14:
Z c= dom (cos (#) cot) implies (-cos (#) cot) is_differentiable_on Z &
for x st x in Z holds((-cos (#) cot)`|Z).x = cos.x+cos.x/(sin.x)^2
proof
assume
A1:Z c= dom (cos (#) cot);
then A2:Z c= dom (-cos (#) cot) by VALUED_1:8;
A3:(cos (#) cot) is_differentiable_on Z by A1,FDIFF_10:11;
then A4:(-1)(#)(cos (#) cot) is_differentiable_on Z by A2,FDIFF_1:20;
for x st x in Z holds ((-cos (#) cot)`|Z).x = cos.x+cos.x/(sin.x)^2
proof
let x;
assume
A5: x in Z;
((-cos (#) cot)`|Z).x = ((-1)(#)((cos (#) cot)`|Z)).x by A3,FDIFF_2:19
.=(-1)*(((cos (#) cot)`|Z).x) by VALUED_1:6
.=(-1)*(-cos.x-cos.x/(sin.x)^2) by A1,A5,FDIFF_10:11
.=cos.x+cos.x/(sin.x)^2;
hence thesis;
end;
hence thesis by A4;
end;
begin :: Integrability Formulas
::f.x=sin.(1/x)/(x^2*(cos.(1/x))^2)
theorem
A c= Z & (for x 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
implies integral(f,A)=(-sec*((id Z)^)).(upper_bound A)-
(-sec*((id Z)^)).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(-sec*((id Z)^)) is_differentiable_on Z by A1,Th1;
A4:for x being Element of REAL
st x in dom ((-sec*((id Z)^))`|Z) holds ((-sec*((id Z)^))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-sec*((id Z)^))`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-sec*((id Z)^))`|Z).x = sin.(1/x)/(x^2*(cos.(1/x))^2) by A1,Th1
.=f.x by A1,A5;
hence thesis;
end;
dom ((-sec*((id Z)^))`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-sec*((id Z)^))`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=cos.(1/x)/(x^2*(sin.(1/x))^2)
theorem
A c= Z & (for x 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
implies integral(f,A)=(cosec*((id Z)^)).(upper_bound A)-
(cosec*((id Z)^)).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z c= dom ((id Z)^) by A1,FUNCT_1:101;
A4:not 0 in Z
proof
assume A5: 0 in Z;
dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2
.= dom id Z \ {0} by Lm1,A5; then
not 0 in {0} by A5,A3,XBOOLE_0:def 5;
hence thesis by TARSKI:def 1;
end;
then A6:(cosec*((id Z)^)) is_differentiable_on Z by A1,FDIFF_9:9;
A7:for x being Element of REAL
st x in dom ((cosec*((id Z)^))`|Z) holds ((cosec*((id Z)^))`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((cosec*((id Z)^))`|Z);then
A8:x in Z by A6,FDIFF_1:def 7;then
((cosec*((id Z)^))`|Z).x = cos.(1/x)/(x^2*(sin.(1/x))^2) by A1,A4,FDIFF_9:9
.=f.x by A1,A8;
hence thesis;
end;
dom ((cosec*((id Z)^))`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then ((cosec*((id Z)^))`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13;
end;
::f.x=exp_R.x*sin.(exp_R.x)/(cos.(exp_R.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(sec*exp_R).(upper_bound A)-(sec*exp_R).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:sec*exp_R is_differentiable_on Z by A1,FDIFF_9:12;
A4:for x being Element of REAL
st x in dom ((sec*exp_R)`|Z) holds ((sec*exp_R)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((sec*exp_R)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((sec*exp_R)`|Z).x=exp_R.x*sin.(exp_R.x)/(cos.(exp_R.x))^2 by A1,FDIFF_9:12
.=f.x by A1,A5;
hence thesis;
end;
dom ((sec*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((sec*exp_R)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=exp_R.x*cos.(exp_R.x)/(sin.(exp_R.x))^2
theorem
A c= Z & (for x 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 implies
integral(f,A)=(-cosec*exp_R).(upper_bound A)-(-cosec*exp_R).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cosec*exp_R is_differentiable_on Z by A1,Th2;
A4:for x being Element of REAL
st x in dom ((-cosec*exp_R)`|Z) holds ((-cosec*exp_R)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cosec*exp_R)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-cosec*exp_R)`|Z).x=exp_R.x*cos.(exp_R.x)/(sin.(exp_R.x))^2 by A1,Th2
.=f.x by A1,A5;
hence thesis;
end;
dom ((-cosec*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cosec*exp_R)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=sin.(ln.x)/(x*(cos.(ln.x))^2)
theorem
A c= Z & (for x 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
implies integral(f,A)=(sec*ln).(upper_bound A)-(sec*ln).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:sec*ln is_differentiable_on Z by A1,FDIFF_9:14;
A4:for x being Element of REAL st x in dom ((sec*ln)`|Z)
holds ((sec*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((sec*ln)`|Z);then
A5: x in Z by A3,FDIFF_1:def 7;then
((sec*ln)`|Z).x=sin.(ln.x)/(x*(cos.(ln.x))^2) by A1,FDIFF_9:14
.=f.x by A1,A5;
hence thesis;
end;
dom((sec*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((sec*ln)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=cos.(ln.x)/(x*(sin.(ln.x))^2)
theorem
A c= Z & (for x 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
implies integral(f,A)=(-cosec*ln).(upper_bound A)-(-cosec*ln).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cosec*ln is_differentiable_on Z by A1,Th3;
A4:for x being Element of REAL
st x in dom ((-cosec*ln)`|Z) holds ((-cosec*ln)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cosec*ln)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-cosec*ln)`|Z).x=cos.(ln.x)/(x*(sin.(ln.x))^2) by A1,Th3
.=f.x by A1,A5;
hence thesis;
end;
dom ((-cosec*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cosec*ln)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=exp_R.(sec.x)*sin.x/(cos.x)^2
theorem
A c= Z & f=(exp_R*sec)(#)(sin/cos^2) & Z = dom f & f|A is continuous
implies integral(f,A)=(exp_R*sec).(upper_bound A)-(exp_R*sec).(lower_bound A)
proof
assume
A1:A c= Z & f=(exp_R*sec)(#)(sin/cos^2) & Z = dom f & f|A is continuous;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom (exp_R*sec) /\ dom (sin/cos^2) by A1,VALUED_1:def 4;then
A3:Z c= dom (exp_R*sec) & Z c= dom (sin/cos^2) by XBOOLE_1:18;
then A4:exp_R*sec is_differentiable_on Z by FDIFF_9:16;
A5:for x st x in Z holds f.x=exp_R.(sec.x)*sin.x/(cos.x)^2
proof
let x;
assume
A6:x in Z;
((exp_R*sec)(#)(sin/cos^2)).x =(exp_R*sec).x*(sin/cos^2).x by VALUED_1:5
.=exp_R.(sec.x)*(sin/cos^2).x by A6,A3,FUNCT_1:12
.=exp_R.(sec.x)*(sin.x/(cos^2).x) by A3,A6,RFUNCT_1:def 1
.=exp_R.(sec.x)*(sin.x/(cos.x)^2) by VALUED_1:11
.=exp_R.(sec.x)*sin.x/(cos.x)^2 ;
hence thesis by A1;
end;
A7:for x being Element of REAL
st x in dom ((exp_R*sec)`|Z) holds ((exp_R*sec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((exp_R*sec)`|Z);then
A8:x in Z by A4,FDIFF_1:def 7;then
((exp_R*sec)`|Z).x=exp_R.(sec.x)*sin.x/(cos.x)^2 by A3,FDIFF_9:16
.=f.x by A5,A8;
hence thesis;
end;
dom ((exp_R*sec)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((exp_R*sec)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,A4,INTEGRA5:13;
end;
::f.x=exp_R.(cosec.x)*cos.x/(sin.x)^2
theorem
A c= Z & f=(exp_R*cosec)(#)(cos/sin^2) & Z = dom f & f|A is continuous
implies integral(f,A)=(-exp_R*cosec).(upper_bound A)-
(-exp_R*cosec).(lower_bound A)
proof
assume
A1:A c= Z & f=(exp_R*cosec)(#)(cos/sin^2) & Z = dom f & f|A is continuous;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
Z = dom (exp_R*cosec) /\ dom (cos/sin^2) by A1,VALUED_1:def 4;then
A3:Z c= dom (exp_R*cosec) & Z c= dom (cos/sin^2) by XBOOLE_1:18;
then A4:-exp_R*cosec is_differentiable_on Z by Th4;
A5:for x st x in Z holds f.x=exp_R.(cosec.x)*cos.x/(sin.x)^2
proof
let x;
assume
A6:x in Z;
((exp_R*cosec)(#)(cos/sin^2)).x =(exp_R*cosec).x*(cos/sin^2).x by VALUED_1:5
.=exp_R.(cosec.x)*(cos/sin^2).x by A6,A3,FUNCT_1:12
.=exp_R.(cosec.x)*(cos.x/(sin^2).x) by A3,A6,RFUNCT_1:def 1
.=exp_R.(cosec.x)*(cos.x/(sin.x)^2) by VALUED_1:11
.=exp_R.(cosec.x)*cos.x/(sin.x)^2 ;
hence thesis by A1;
end;
A7:for x being Element of REAL
st x in dom ((-exp_R*cosec)`|Z) holds ((-exp_R*cosec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-exp_R*cosec)`|Z);then
A8:x in Z by A4,FDIFF_1:def 7;then
((-exp_R*cosec)`|Z).x=exp_R.(cosec.x)*cos.x/(sin.x)^2 by A3,Th4
.=f.x by A5,A8;
hence thesis;
end;
dom ((-exp_R*cosec)`|Z)=dom f by A1,A4,FDIFF_1:def 7;
then ((-exp_R*cosec)`|Z)= f by A7,PARTFUN1:5;
hence thesis by A1,A2,A4,INTEGRA5:13;
end;
::f.x=tan.x
theorem
A c= Z & Z c= dom (ln*sec) & Z = dom tan & tan|A is continuous
implies integral(tan,A)=(ln*sec).(upper_bound A)-(ln*sec).(lower_bound A)
proof
assume
A1:A c= Z & Z c= dom (ln*sec) & Z = dom tan & tan|A is continuous;
then
A2:tan is_integrable_on A & tan|A is bounded by INTEGRA5:10,11;
A3:ln*sec is_differentiable_on Z by A1,FDIFF_9:18;
A4:for x st x in Z holds cos.x<>0
proof
let x;
assume x in Z;
then x in dom sec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A5:for x being Element of REAL
st x in dom ((ln*sec)`|Z) holds ((ln*sec)`|Z).x = tan.x
proof
let x be Element of REAL;
assume x in dom ((ln*sec)`|Z);then
A6: x in Z by A3,FDIFF_1:def 7;then
A7: cos.x<>0 by A4;
((ln*sec)`|Z).x = tan x by A1,A6,FDIFF_9:18
.=tan.x by A7,SIN_COS9:15;
hence thesis;
end;
dom ((ln*sec)`|Z)=dom tan by A1,A3,FDIFF_1:def 7;
then ((ln*sec)`|Z)= tan by A5,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=-cot.x
theorem
A c= Z & Z c= dom (ln*cosec) & Z = dom cot & (-cot)|A is continuous
implies integral((-cot),A)=(ln*cosec).(upper_bound A)-
(ln*cosec).(lower_bound A)
proof
assume
A1:A c= Z & Z c= dom (ln*cosec) & Z = dom cot & (-cot)|A is continuous;
then A2:Z = dom (-cot) by VALUED_1:8;
then
A3:(-cot) is_integrable_on A & (-cot)|A is bounded by A1,INTEGRA5:10,11;
A4:ln*cosec is_differentiable_on Z by A1,FDIFF_9:19;
A5:for x st x in Z holds sin.x<>0
proof
let x;
assume x in Z;
then x in dom cosec by A1,FUNCT_1:11;
hence thesis by RFUNCT_1:3;
end;
A6:for x being Element of REAL
st x in dom ((ln*cosec)`|Z) holds ((ln*cosec)`|Z).x = (-cot).x
proof
let x be Element of REAL;
assume x in dom ((ln*cosec)`|Z);then
A7: x in Z by A4,FDIFF_1:def 7;then
A8: sin.x<>0 by A5;
((ln*cosec)`|Z).x = -cot(x) by A1,A7,FDIFF_9:19
.=-cot.x by A8,SIN_COS9:16
.=(-cot).x by VALUED_1:8;
hence thesis;
end;
dom ((ln*cosec)`|Z)=dom (-cot) by A2,A4,FDIFF_1:def 7;
then ((ln*cosec)`|Z)= -cot by A6,PARTFUN1:5;
hence thesis by A1,A3,A4,INTEGRA5:13;
end;
::f.x=cot.x
theorem
A c= Z & Z c= dom (ln*cosec) & Z = dom cot & cot|A is continuous
implies integral(cot,A)=(-ln*cosec).(upper_bound A)-(-ln*cosec).(lower_bound A)
proof
assume
A1:A c= Z & Z c= dom (ln*cosec) & Z = dom cot & cot|A is continuous;
then
A2:cot is_integrable_on A & cot|A is bounded by INTEGRA5:10,11;
A3:-ln*cosec is_differentiable_on Z by A1,Th5;
A4:for x being Element of REAL
st x in dom ((-ln*cosec)`|Z) holds ((-ln*cosec)`|Z).x = cot.x
proof
let x be Element of REAL;
assume x in dom ((-ln*cosec)`|Z);then
x in Z by A3,FDIFF_1:def 7;
then ((-ln*cosec)`|Z).x=cot.x by A1,Th5;
hence thesis;
end;
dom ((-ln*cosec)`|Z)=dom cot by A1,A3,FDIFF_1:def 7;
then ((-ln*cosec)`|Z)= cot by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=n*sin.x/(cos.x) #Z (n+1)
theorem
A c= Z & (for x 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
implies integral(f,A)=(( #Z n)*sec).(upper_bound A)-
(( #Z n)*sec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:( #Z n)*sec is_differentiable_on Z by A1,FDIFF_9:20;
A4:for x being Element of REAL
st x in dom ((( #Z n)*sec)`|Z) holds ((( #Z n)*sec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((( #Z n)*sec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((( #Z n)*sec)`|Z).x=n*sin.x/(cos.x) #Z (n+1) by A1,FDIFF_9:20
.=f.x by A1,A5;
hence thesis;
end;
dom ((( #Z n)*sec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((( #Z n)*sec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=n*cos.x/(sin.x) #Z (n+1)
theorem
A c= Z & (for x 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
implies integral(f,A)=(-( #Z n)*cosec).(upper_bound A)-
(-( #Z n)*cosec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-( #Z n)*cosec is_differentiable_on Z by A1,Th6;
A4:for x being Element of REAL
st x in dom ((-( #Z n)*cosec)`|Z) holds ((-( #Z n)*cosec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((-( #Z n)*cosec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-( #Z n)*cosec)`|Z).x=n*cos.x/(sin.x) #Z (n+1) by A1,Th6
.=f.x by A1,A5;
hence thesis;
end;
dom ((-( #Z n)*cosec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-( #Z n)*cosec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=exp_R.x/cos.x+exp_R.x*sin.x/(cos.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(exp_R(#)sec).(upper_bound A)-
(exp_R(#)sec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:exp_R(#)sec is_differentiable_on Z by A1,FDIFF_9:24;
A4:for x being Element of REAL
st x in dom ((exp_R(#)sec)`|Z) holds ((exp_R(#)sec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((exp_R(#)sec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((exp_R(#)sec)`|Z).x = exp_R.x/cos.x+exp_R.x*sin.x/(cos.x)^2
by A1,FDIFF_9:24
.=f.x by A1,A5;
hence thesis;
end;
dom ((exp_R(#)sec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((exp_R(#)sec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=exp_R.x/sin.x-exp_R.x*cos.x/(sin.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(exp_R(#)cosec).(upper_bound A)-
(exp_R(#)cosec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:exp_R(#)cosec is_differentiable_on Z by A1,FDIFF_9:25;
A4:for x being Element of REAL
st x in dom ((exp_R(#)cosec)`|Z) holds ((exp_R(#)cosec)`|Z).x = f.x
proof
let x be Element of REAL;
assume x in dom ((exp_R(#)cosec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((exp_R(#)cosec)`|Z).x = exp_R.x/sin.x-exp_R.x*cos.x/(sin.x)^2
by A1,FDIFF_9:25
.=f.x by A1,A5;
hence thesis;
end;
dom ((exp_R(#)cosec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((exp_R(#)cosec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=(sin.(a*x)-(cos.(a*x))^2)/(cos.(a*x))^2
theorem
A c= Z & (for x 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 st x in Z holds f1.x=a*x & a<>0)
& Z = dom f & f|A is continuous implies
integral(f,A)=((1/a)(#)(sec*f1)-id Z).(upper_bound A)-
((1/a)(#)(sec*f1)-id Z).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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 st x in Z holds f1.x=a*x & a<>0)
& Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(1/a)(#)(sec*f1)-id Z is_differentiable_on Z by A1,FDIFF_9:26;
A4:for x being Element of REAL st x in dom (((1/a)(#)(sec*f1)-id Z)`|Z) holds
(((1/a)(#)(sec*f1)-id Z)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (((1/a)(#)(sec*f1)-id Z)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
(((1/a)(#)(sec*f1)-id Z)`|Z).x
= (sin.(a*x)-(cos.(a*x))^2)/(cos.(a*x))^2 by A1,FDIFF_9:26
.= f.x by A1,A5;
hence thesis;
end;
dom (((1/a)(#)(sec*f1)-id Z)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then (((1/a)(#)(sec*f1)-id Z)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=(cos.(a*x)-(sin.(a*x))^2)/(sin.(a*x))^2
theorem
A c= Z & (for x 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 st x in Z holds f1.x=a*x & a<>0)
& Z = dom f & f|A is continuous implies
integral(f,A)=((-1/a)(#)(cosec*f1)-id Z).(upper_bound A)
-((-1/a)(#)(cosec*f1)-id Z).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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 st x in Z holds f1.x=a*x & a<>0)
& Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:(-1/a)(#)(cosec*f1)-id Z is_differentiable_on Z by A1,FDIFF_9:27;
A4:for x being Element of REAL st x in dom (((-1/a)(#)(cosec*f1)-id Z)`|Z)
holds
(((-1/a)(#)(cosec*f1)-id Z)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom (((-1/a)(#)(cosec*f1)-id Z)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
(((-1/a)(#)(cosec*f1)-id Z)`|Z).x
= (cos.(a*x)-(sin.(a*x))^2)/(sin.(a*x))^2 by A1,FDIFF_9:27
.= f.x by A1,A5;
hence thesis;
end;
dom (((-1/a)(#)(cosec*f1)-id Z)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then (((-1/a)(#)(cosec*f1)-id Z)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/cos.x/x+ln.x*sin.x/(cos.x)^2
theorem
A c= Z & (for x 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 implies
integral(f,A)=(ln(#)sec).(upper_bound A)-(ln(#)sec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:ln(#)sec is_differentiable_on Z by A1,FDIFF_9:30;
A4:for x being Element of REAL st x in dom ((ln(#)sec)`|Z)
holds ((ln(#)sec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((ln(#)sec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((ln(#)sec)`|Z).x = 1/cos.x/x+ln.x*sin.x/(cos.x)^2 by A1,FDIFF_9:30
.= f.x by A1,A5;
hence thesis;
end;
dom ((ln(#)sec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((ln(#)sec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/sin.x/x-ln.x*cos.x/(sin.x)^2
theorem
A c= Z & (for x 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 implies
integral(f,A)=(ln(#)cosec).(upper_bound A)-(ln(#)cosec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:ln(#)cosec is_differentiable_on Z by A1,FDIFF_9:31;
A4:for x being Element of REAL
st x in dom ((ln(#)cosec)`|Z) holds ((ln(#)cosec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((ln(#)cosec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((ln(#)cosec)`|Z).x = 1/sin.x/x-ln.x*cos.x/(sin.x)^2 by A1,FDIFF_9:31
.= f.x by A1,A5;
hence thesis;
end;
dom ((ln(#)cosec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((ln(#)cosec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/cos.x/x^2-sin.x/x/(cos.x)^2
theorem
A c= Z & (for x 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 implies
integral(f,A)=(-(id Z)^(#)sec).(upper_bound A)-(-(id Z)^(#)sec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-(id Z)^(#)sec is_differentiable_on Z by A1,Th7;
A4:for x being Element of REAL
st x in dom ((-(id Z)^(#)sec)`|Z) holds ((-(id Z)^(#)sec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-(id Z)^(#)sec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-(id Z)^(#)sec)`|Z).x = 1/cos.x/x^2-sin.x/x/(cos.x)^2 by A1,Th7
.= f.x by A1,A5;
hence thesis;
end;
dom ((-(id Z)^(#)sec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-(id Z)^(#)sec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/sin.x/x^2+cos.x/x/(sin.x)^2
theorem
A c= Z & (for x 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 implies
integral(f,A)=(-(id Z)^(#)cosec).(upper_bound A)-
(-(id Z)^(#)cosec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-(id Z)^(#)cosec is_differentiable_on Z by A1,Th8;
A4:for x being Element of REAL st x in dom ((-(id Z)^(#)cosec)`|Z) holds
((-(id Z)^(#)cosec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-(id Z)^(#)cosec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-(id Z)^(#)cosec)`|Z).x = 1/sin.x/x^2+cos.x/x/(sin.x)^2 by A1,Th8
.= f.x by A1,A5;
hence thesis;
end;
dom ((-(id Z)^(#)cosec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-(id Z)^(#)cosec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=cos.x*sin.(sin.x)/(cos.(sin.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(sec*sin).(upper_bound A)-(sec*sin).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:sec*sin is_differentiable_on Z by A1,FDIFF_9:34;
A4:for x being Element of REAL st x in dom ((sec*sin)`|Z)
holds ((sec*sin)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((sec*sin)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((sec*sin)`|Z).x = cos.x*sin.(sin.x)/(cos.(sin.x))^2 by A1,FDIFF_9:34
.= f.x by A1,A5;
hence thesis;
end;
dom ((sec*sin)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((sec*sin)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=sin.x*sin.(cos.x)/(cos.(cos.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(-sec*cos).(upper_bound A)-(-sec*cos).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z c= dom (-sec*cos) by A1,VALUED_1:8;
A4:sec*cos is_differentiable_on Z by A1,FDIFF_9:35;
then A5:(-1)(#)(sec*cos) is_differentiable_on Z by A3,FDIFF_1:20;
A6:for x st x in Z holds ((-sec*cos)`|Z).x = sin.x*sin.(cos.x)/(cos.(cos.x))^2
proof
let x;
assume
A7:x in Z;
((-sec*cos)`|Z).x=((-1)(#)((sec*cos)`|Z)).x by A4,FDIFF_2:19
.=(-1)*(((sec*cos)`|Z).x) by VALUED_1:6
.=(-1)*(-sin.x*sin.(cos.x)/(cos.(cos.x))^2) by A1,A7,FDIFF_9:35
.=sin.x*sin.(cos.x)/(cos.(cos.x))^2;
hence thesis;
end;
A8:for x being Element of REAL st x in dom ((-sec*cos)`|Z)
holds ((-sec*cos)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-sec*cos)`|Z);then
A9:x in Z by A5,FDIFF_1:def 7;then
((-sec*cos)`|Z).x = sin.x*sin.(cos.x)/(cos.(cos.x))^2 by A6
.= f.x by A1,A9;
hence thesis;
end;
dom ((-sec*cos)`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then ((-sec*cos)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,A5,INTEGRA5:13;
end;
::f.x=cos.x*cos.(sin.x)/(sin.(sin.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(-cosec*sin).(upper_bound A)-(-cosec*sin).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cosec*sin is_differentiable_on Z by A1,Th9;
A4:for x being Element of REAL
st x in dom ((-cosec*sin)`|Z) holds ((-cosec*sin)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cosec*sin)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-cosec*sin)`|Z).x = cos.x*cos.(sin.x)/(sin.(sin.x))^2 by A1,Th9
.= f.x by A1,A5;
hence thesis;
end;
dom ((-cosec*sin)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cosec*sin)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=sin.x*cos.(cos.x)/(sin.(cos.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(cosec*cos).(upper_bound A)-(cosec*cos).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:cosec*cos is_differentiable_on Z by A1,FDIFF_9:37;
A4:for x being Element of REAL st x in dom ((cosec*cos)`|Z)
holds ((cosec*cos)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((cosec*cos)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((cosec*cos)`|Z).x = sin.x*cos.(cos.x)/(sin.(cos.x))^2 by A1,FDIFF_9:37
.= f.x by A1,A5;
hence thesis;
end;
dom ((cosec*cos)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((cosec*cos)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=sin.(tan.x)/(cos.x)^2/(cos.(tan.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(sec*tan).(upper_bound A)-(sec*tan).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:sec*tan is_differentiable_on Z by A1,FDIFF_9:38;
A4:for x being Element of REAL st x in dom ((sec*tan)`|Z)
holds ((sec*tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((sec*tan)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((sec*tan)`|Z).x = sin.(tan.x)/(cos.x)^2/(cos.(tan.x))^2 by A1,FDIFF_9:38
.= f.x by A1,A5;
hence thesis;
end;
dom ((sec*tan)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((sec*tan)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(-sec*cot).(upper_bound A)-(-sec*cot).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-sec*cot is_differentiable_on Z by A1,Th10;
A4:for x being Element of REAL st x in dom ((-sec*cot)`|Z)
holds ((-sec*cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-sec*cot)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-sec*cot)`|Z).x = sin.(cot.x)/(sin.x)^2/(cos.(cot.x))^2 by A1,Th10
.= f.x by A1,A5;
hence thesis;
end;
dom ((-sec*cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-sec*cot)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x= cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(-cosec*tan).(upper_bound A)-(-cosec*tan).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cosec*tan is_differentiable_on Z by A1,Th11;
A4:for x being Element of REAL
st x in dom ((-cosec*tan)`|Z) holds ((-cosec*tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cosec*tan)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-cosec*tan)`|Z).x = cos.(tan.x)/(cos.x)^2/(sin.(tan.x))^2 by A1,Th11
.= f.x by A1,A5;
hence thesis;
end;
dom ((-cosec*tan)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cosec*tan)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=cos.(cot.x)/(sin.x)^2/(sin.(cot.x))^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(cosec*cot).(upper_bound A)-(cosec*cot).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:cosec*cot is_differentiable_on Z by A1,FDIFF_9:41;
A4:for x being Element of REAL
st x in dom ((cosec*cot)`|Z) holds ((cosec*cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((cosec*cot)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((cosec*cot)`|Z).x = cos.(cot.x)/(sin.x)^2/(sin.(cot.x))^2 by A1,FDIFF_9:41
.= f.x by A1,A5;
hence thesis;
end;
dom ((cosec*cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((cosec*cot)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/(cos.x)^2/cos.x+tan.x*sin.x/(cos.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(tan(#)sec).(upper_bound A)-(tan(#)sec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan(#)sec is_differentiable_on Z by A1,FDIFF_9:42;
A4:for x being Element of REAL st x in dom ((tan(#)sec)`|Z)
holds ((tan(#)sec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((tan(#)sec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((tan(#)sec)`|Z).x = 1/(cos.x)^2/cos.x+tan.x*sin.x/(cos.x)^2 by A1,FDIFF_9:42
.= f.x by A1,A5;
hence thesis;
end;
dom ((tan(#)sec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((tan(#)sec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/(sin.x)^2/cos.x-cot.x*sin.x/(cos.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(-cot(#)sec).(upper_bound A)-(-cot(#)sec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cot(#)sec is_differentiable_on Z by A1,Th12;
A4:for x being Element of REAL
st x in dom ((-cot(#)sec)`|Z) holds ((-cot(#)sec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cot(#)sec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-cot(#)sec)`|Z).x = 1/(sin.x)^2/cos.x-cot.x*sin.x/(cos.x)^2 by A1,Th12
.= f.x by A1,A5;
hence thesis;
end;
dom ((-cot(#)sec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cot(#)sec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/(cos.x)^2/sin.x-tan.x*cos.x/(sin.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(tan(#)cosec).(upper_bound A)-
(tan(#)cosec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan(#)cosec is_differentiable_on Z by A1,FDIFF_9:44;
A4:for x being Element of REAL
st x in dom ((tan(#)cosec)`|Z) holds ((tan(#)cosec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((tan(#)cosec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((tan(#)cosec)`|Z).x
= 1/(cos.x)^2/sin.x-tan.x*cos.x/(sin.x)^2 by A1,FDIFF_9:44
.= f.x by A1,A5;
hence thesis;
end;
dom ((tan(#)cosec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((tan(#)cosec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/(sin.x)^2/sin.x+cot.x*cos.x/(sin.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(-cot(#)cosec).(upper_bound A)-
(-cot(#)cosec).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cot(#)cosec is_differentiable_on Z by A1,Th13;
A4:for x being Element of REAL
st x in dom ((-cot(#)cosec)`|Z) holds ((-cot(#)cosec)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cot(#)cosec)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((-cot(#)cosec)`|Z).x = 1/(sin.x)^2/sin.x+cot.x*cos.x/(sin.x)^2 by A1,Th13
.= f.x by A1,A5;
hence thesis;
end;
dom ((-cot(#)cosec)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cot(#)cosec)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/(cos.(cot.x))^2*(1/(sin.x)^2)
theorem
A c= Z & (for x 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
implies integral(f,A)=(-tan*cot).(upper_bound A)-(-tan*cot).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z c= dom (-tan*cot) by A1,VALUED_1:8;
A4:tan*cot is_differentiable_on Z by A1,FDIFF_10:1;
then A5:(-1)(#)(tan*cot) is_differentiable_on Z by A3,FDIFF_1:20;
A6:for x st x in Z holds ((-tan*cot)`|Z).x = 1/(cos.(cot.x))^2*(1/(sin.x)^2)
proof
let x;
assume
A7:x in Z;
((-tan*cot)`|Z).x=((-1)(#)((tan*cot)`|Z)).x by A4,FDIFF_2:19
.=(-1)*(((tan*cot)`|Z).x) by VALUED_1:6
.=(-1)*(1/(cos.(cot.x))^2*(-1/(sin.x)^2)) by A1,A7,FDIFF_10:1
.=1/(cos.(cot.x))^2*(1/(sin.x)^2);
hence thesis;
end;
A8:for x being Element of REAL
st x in dom ((-tan*cot)`|Z) holds ((-tan*cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-tan*cot)`|Z);then
A9:x in Z by A5,FDIFF_1:def 7;then
((-tan*cot)`|Z).x = 1/(cos.(cot.x))^2*(1/(sin.x)^2) by A6
.= f.x by A1,A9;
hence thesis;
end;
dom ((-tan*cot)`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then ((-tan*cot)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,A5,INTEGRA5:13;
end;
::f.x=1/(cos.(tan.x))^2 *(1/(cos.x)^2)
theorem
A c= Z & (for x 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
implies integral(f,A)=(tan*tan).(upper_bound A)-(tan*tan).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan*tan is_differentiable_on Z by A1,FDIFF_10:2;
A4:for x being Element of REAL
st x in dom ((tan*tan)`|Z) holds ((tan*tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((tan*tan)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((tan*tan)`|Z).x = 1/(cos.(tan.x))^2 *(1/(cos.x)^2) by A1,FDIFF_10:2
.= f.x by A1,A5;
hence thesis;
end;
dom ((tan*tan)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((tan*tan)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=(1/(sin.(cot.x))^2) *(1/(sin.x)^2)
theorem
A c= Z & (for x 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
implies integral(f,A)=(cot*cot).(upper_bound A)-(cot*cot).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:cot*cot is_differentiable_on Z by A1,FDIFF_10:3;
A4:for x being Element of REAL st x in dom ((cot*cot)`|Z)
holds ((cot*cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((cot*cot)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((cot*cot)`|Z).x = (1/(sin.(cot.x))^2) *(1/(sin.x)^2) by A1,FDIFF_10:3
.= f.x by A1,A5;
hence thesis;
end;
dom ((cot*cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((cot*cot)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=(1/(sin.(tan.x))^2)*(1/(cos.x)^2)
theorem
A c= Z & (for x 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
implies integral(f,A)=(-cot*tan).(upper_bound A)-(-cot*tan).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:Z c= dom (-cot*tan) by A1,VALUED_1:8;
A4:cot*tan is_differentiable_on Z by A1,FDIFF_10:4;
then A5:(-1)(#)(cot*tan) is_differentiable_on Z by A3,FDIFF_1:20;
A6:for x st x in Z holds ((-cot*tan)`|Z).x = (1/(sin.(tan.x))^2)*(1/(cos.x)^2)
proof
let x;
assume
A7:x in Z;
((-cot*tan)`|Z).x=((-1)(#)((cot*tan)`|Z)).x by A4,FDIFF_2:19
.=(-1)*(((cot*tan)`|Z).x) by VALUED_1:6
.=(-1)*((-1/(sin.(tan.x))^2)*(1/(cos.x)^2)) by A1,A7,FDIFF_10:4
.=(1/(sin.(tan.x))^2)*(1/(cos.x)^2);
hence thesis;
end;
A8:for x being Element of REAL st x in dom ((-cot*tan)`|Z)
holds ((-cot*tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cot*tan)`|Z);then
A9:x in Z by A5,FDIFF_1:def 7;then
((-cot*tan)`|Z).x =(1/(sin.(tan.x))^2)*(1/(cos.x)^2) by A6
.= f.x by A1,A9;
hence thesis;
end;
dom ((-cot*tan)`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then ((-cot*tan)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,A5,INTEGRA5:13;
end;
::f.x=1/(cos.x)^2+1/(sin.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(tan-cot).(upper_bound A)-(tan-cot).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan-cot is_differentiable_on Z by A1,FDIFF_10:5;
A4:for x being Element of REAL st x in dom ((tan-cot)`|Z)
holds ((tan-cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((tan-cot)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((tan-cot)`|Z).x = 1/(cos.x)^2+1/(sin.x)^2 by A1,FDIFF_10:5
.= f.x by A1,A5;
hence thesis;
end;
dom ((tan-cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((tan-cot)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=1/(cos.x)^2-1/(sin.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(tan+cot).(upper_bound A)-(tan+cot).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:tan+cot is_differentiable_on Z by A1,FDIFF_10:6;
A4:for x being Element of REAL st x in dom ((tan+cot)`|Z)
holds ((tan+cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((tan+cot)`|Z);then
A5:x in Z by A3,FDIFF_1:def 7;then
((tan+cot)`|Z).x = 1/(cos.x)^2-1/(sin.x)^2 by A1,FDIFF_10:6
.= f.x by A1,A5;
hence thesis;
end;
dom ((tan+cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((tan+cot)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=cos.(sin.x)*cos.x
theorem
A c= Z & (for x st x in Z holds f.x=cos.(sin.x)*cos.x)
& Z = dom f & f|A is continuous
implies integral(f,A)=(sin*sin).(upper_bound A)-(sin*sin).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f.x=cos.(sin.x)*cos.x)
& Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:sin*sin is_differentiable_on Z by FDIFF_10:7;
A4:for x being Element of REAL st x in dom ((sin*sin)`|Z)
holds ((sin*sin)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((sin*sin)`|Z);then
A5: x in Z by A3,FDIFF_1:def 7;then
((sin*sin)`|Z).x = cos.(sin.x)*cos.x by FDIFF_10:7
.= f.x by A1,A5;
hence thesis;
end;
dom ((sin*sin)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((sin*sin)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=cos.(cos.x)*sin.x
theorem
A c= Z & (for x st x in Z holds f.x=cos.(cos.x)*sin.x)
& Z = dom f & f|A is continuous
implies integral(f,A)=(-sin*cos).(upper_bound A)-(-sin*cos).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f.x=cos.(cos.x)*sin.x)
& Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
dom cos = REAL & rng cos c= dom cos & dom sin = dom cos by SIN_COS:24;
then
dom (sin*cos) = REAL by RELAT_1:27;
then A3: dom (-sin*cos) = REAL by VALUED_1:8;
A4:sin*cos is_differentiable_on Z by FDIFF_10:8;
then A5:(-1)(#)(sin*cos) is_differentiable_on Z by A3,FDIFF_1:20;
A6:for x st x in Z holds ((-sin*cos)`|Z).x = cos.(cos.x)*sin.x
proof
let x;
assume
A7:x in Z;
((-sin*cos)`|Z).x=((-1)(#)((sin*cos)`|Z)).x by A4,FDIFF_2:19
.=(-1)*(((sin*cos)`|Z).x) by VALUED_1:6
.=(-1)*((-cos.(cos.x)*sin.x)) by A7,FDIFF_10:8
.=cos.(cos.x)*sin.x;
hence thesis;
end;
A8:for x being Element of REAL st x in dom ((-sin*cos)`|Z)
holds ((-sin*cos)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-sin*cos)`|Z);then
A9:x in Z by A5,FDIFF_1:def 7;then
((-sin*cos)`|Z).x = cos.(cos.x)*sin.x by A6
.= f.x by A1,A9;
hence thesis;
end;
dom ((-sin*cos)`|Z)=dom f by A1,A5,FDIFF_1:def 7;
then ((-sin*cos)`|Z)= f by A8,PARTFUN1:5;
hence thesis by A1,A2,A5,INTEGRA5:13;
end;
::f.x=sin.(sin.x)*cos.x
theorem
A c= Z & (for x st x in Z holds f.x=sin.(sin.x)*cos.x) &
Z = dom f & f|A is continuous
implies integral(f,A)=(-cos*sin).(upper_bound A)-(-cos*sin).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f.x=sin.(sin.x)*cos.x)
& Z = dom f & f|A is continuous; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3: dom sin = REAL by SIN_COS:24;
rng sin c= dom sin & dom sin = dom cos by SIN_COS:24; then
dom (cos*sin) = REAL by A3,RELAT_1:27;
then A4:dom (-cos*sin) = REAL by VALUED_1:8;
A5:cos*sin is_differentiable_on Z by FDIFF_10:9;
then A6:(-1)(#)(cos*sin) is_differentiable_on Z by A4,FDIFF_1:20;
A7:for x st x in Z holds ((-cos*sin)`|Z).x = sin.(sin.x)*cos.x
proof
let x;
assume
A8:x in Z;
((-cos*sin)`|Z).x=((-1)(#)((cos*sin)`|Z)).x by A5,FDIFF_2:19
.=(-1)*(((cos*sin)`|Z).x) by VALUED_1:6
.=(-1)*((-sin.(sin.x)*cos.x)) by A8,FDIFF_10:9
.=sin.(sin.x)*cos.x;
hence thesis;
end;
A9:for x being Element of REAL st x in dom ((-cos*sin)`|Z)
holds ((-cos*sin)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cos*sin)`|Z);then
A10: x in Z by A6,FDIFF_1:def 7;then
((-cos*sin)`|Z).x =sin.(sin.x)*cos.x by A7
.= f.x by A1,A10;
hence thesis;
end;
dom ((-cos*sin)`|Z)=dom f by A1,A6,FDIFF_1:def 7;
then ((-cos*sin)`|Z)= f by A9,PARTFUN1:5;
hence thesis by A1,A2,A6,INTEGRA5:13;
end;
::f.x=sin.(cos.x)*sin.x
theorem
A c= Z & (for x st x in Z holds f.x=sin.(cos.x)*sin.x)
& Z = dom f & f|A is continuous
implies integral(f,A)=(cos*cos).(upper_bound A)-(cos*cos).(lower_bound A)
proof
assume
A1:A c= Z & (for x st x in Z holds f.x=sin.(cos.x)*sin.x)
& Z = dom f & f|A is continuous;then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:cos*cos is_differentiable_on Z by FDIFF_10:10;
A4:for x being Element of REAL st x in dom ((cos*cos)`|Z)
holds ((cos*cos)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((cos*cos)`|Z);then
A5: x in Z by A3,FDIFF_1:def 7;then
((cos*cos)`|Z).x = sin.(cos.x)*sin.x by FDIFF_10:10
.= f.x by A1,A5;
hence thesis;
end;
dom ((cos*cos)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((cos*cos)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=cos.x+cos.x/(sin.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(-cos (#) cot).(upper_bound A)-
(-cos (#) cot).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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;
then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:-cos (#) cot is_differentiable_on Z by A1,Th14;
A4:for x being Element of REAL
st x in dom ((-cos (#) cot)`|Z) holds ((-cos (#) cot)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((-cos (#) cot)`|Z);then
A5: x in Z by A3,FDIFF_1:def 7;then
((-cos (#) cot)`|Z).x =cos.x+cos.x/(sin.x)^2 by A1,Th14
.= f.x by A1,A5;
hence thesis;
end;
dom ((-cos (#) cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((-cos (#) cot)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;
::f.x=sin.x + sin.x/(cos.x)^2
theorem
A c= Z & (for x 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
implies integral(f,A)=(sin (#) tan).(upper_bound A)-
(sin (#) tan).(lower_bound A)
proof
assume
A1:A c= Z & (for x 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; then
A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11;
A3:sin (#) tan is_differentiable_on Z by A1,FDIFF_10:12;
A4:for x being Element of REAL
st x in dom ((sin (#) tan)`|Z) holds ((sin (#) tan)`|Z).x=f.x
proof
let x be Element of REAL;
assume x in dom ((sin (#) tan)`|Z);then
A5: x in Z by A3,FDIFF_1:def 7;then
((sin (#) tan)`|Z).x =sin.x + sin.x/(cos.x)^2 by A1,FDIFF_10:12
.= f.x by A1,A5;
hence thesis;
end;
dom ((sin (#) tan)`|Z)=dom f by A1,A3,FDIFF_1:def 7;
then ((sin (#) tan)`|Z)= f by A4,PARTFUN1:5;
hence thesis by A1,A2,A3,INTEGRA5:13;
end;