:: Integrability Formulas -- Part {II} :: by Bo Li , Na Ma and Xiquan Liang :: :: Received February 4, 2010 :: Copyright (c) 2010-2019 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, INTEGRA1, FDIFF_1, XBOOLE_0, SQUARE_1, ARYTM_3, ORDINAL2, RCOMP_1, PREPOWER, LIMFUNC1, PARTFUN1, TAYLOR_1, SIN_COS9, SUBSET_1, TARSKI, NUMBERS, REAL_1, CARD_1, INTEGRA5, XXREAL_2, ORDINAL4, VALUED_1, XXREAL_1, XXREAL_0, 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, SIN_COS4, SIN_COS9, LIMFUNC1, SEQ_4; constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER, INTEGRA5, SEQ_4, SIN_COS9, PARTFUN2, RFUNCT_1, SIN_COS4, LIMFUNC1, RELSET_1, INTEGRA1, COMSEQ_2, COMPLEX1, 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, SQUARE_1, SIN_COS4, LIMFUNC1, XCMPLX_0; expansions TARSKI; theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, XCMPLX_1, INTEGRA5, SIN_COS, TAYLOR_1, VALUED_1, XREAL_0, XBOOLE_0, XXREAL_1, XBOOLE_1, FDIFF_5, FDIFF_7, FDIFF_8, SIN_COS9, PREPOWER, TARSKI, RELAT_1, FDIFF_2; begin reserve a,x for Real; reserve n for Element of NAT; reserve A for non empty closed_interval Subset of REAL; reserve f,h,f1,f2 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; Lm2: right_open_halfline 0 = {g where g is Real: 00 by SIN_COS:54; (((-1/2)(#)((sin+cos)/exp_R))`|Z).x=(-1/2)*(diff((sin+cos)/exp_R,x)) by A1,A5,A8,FDIFF_1:20 .=(-1/2)*((diff(sin+cos,x) * exp_R.x - diff(exp_R,x) *(sin+cos).x)/(exp_R.x)^2) by A9,A10,A12,FDIFF_2:14 .=(-1/2)*((((sin+cos)`|Z).x* exp_R.x - diff(exp_R,x) *(sin+cos).x)/(exp_R.x)^2) by A4,A8,FDIFF_1:def 7 .=(-1/2)*(((cos.x-sin.x)* exp_R.x - diff(exp_R,x) *(sin+cos).x)/(exp_R.x)^2) by A3,A8,FDIFF_7:38 .=(-1/2)*(((cos.x-sin.x)* exp_R.x - exp_R.x*(sin.x+cos.x))/(exp_R.x)^2) by A11,SIN_COS:65 .=(-1/2)*((-2*sin.x)*(exp_R.x/((exp_R.x)*(exp_R.x)))) .=(-1/2)*((-2*sin.x)*((exp_R.x)/(exp_R.x)/(exp_R.x))) by XCMPLX_1:78 .=(-1/2)*((-2*sin.x)*(1/exp_R.x)) by A12,XCMPLX_1:60 .=sin.x/exp_R.x; hence thesis; end; hence thesis by A6; end; ::f.x=sin.x/exp_R.x theorem A c= Z & f=sin/exp_R & Z c= dom ((-1/2)(#)((sin+cos)/exp_R)) & Z = dom f & f|A is continuous implies integral(f,A)=((-1/2)(#)((sin+cos)/exp_R)).(upper_bound A) -((-1/2)(#)((sin+cos)/exp_R)).(lower_bound A) proof assume A1:A c= Z & f=sin/exp_R & Z c= dom ((-1/2)(#)((sin+cos)/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:(-1/2)(#)((sin+cos)/exp_R) is_differentiable_on Z by A1,Th7; A4:for x st x in Z holds f.x=sin.x/exp_R.x by A1,RFUNCT_1:def 1; A5:for x being Element of REAL st x in dom (((-1/2)(#)((sin+cos)/exp_R))`|Z) holds (((-1/2)(#)((sin+cos)/exp_R))`|Z).x=f.x proof let x be Element of REAL; assume x in dom (((-1/2)(#)((sin+cos)/exp_R))`|Z);then A6:x in Z by A3,FDIFF_1:def 7;then (((-1/2)(#)((sin+cos)/exp_R))`|Z).x=sin.x/exp_R.x by A1,Th7 .=f.x by A6,A4; hence thesis; end; dom (((-1/2)(#)((sin+cos)/exp_R))`|Z)=dom f by A1,A3,FDIFF_1:def 7; then (((-1/2)(#)((sin+cos)/exp_R))`|Z)= f by A5,PARTFUN1:5; hence thesis by A1,A2,Th7,INTEGRA5:13; end; theorem Th9: Z c= dom ((1/2)(#)((sin-cos)/exp_R)) implies (1/2)(#)((sin-cos)/exp_R) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)((sin-cos)/exp_R))`|Z).x =cos.x/exp_R.x proof assume A1:Z c= dom ((1/2)(#)((sin-cos)/exp_R)); then A2:Z c= dom ((sin-cos)/exp_R) by VALUED_1:def 5;then Z c= dom (sin-cos) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1; then A3:Z c= dom (sin-cos) by XBOOLE_1:18; then A4:sin-cos is_differentiable_on Z & for x st x in Z holds ((sin-cos)`|Z).x =cos.x+sin.x by FDIFF_7:39; A5:(sin-cos)/exp_R is_differentiable_on Z by A2,FDIFF_7:43;then A6:(1/2)(#)((sin-cos)/exp_R) is_differentiable_on Z by FDIFF_2:19; for x st x in Z holds (((1/2)(#)((sin-cos)/exp_R))`|Z).x =cos.x/exp_R.x proof let x; assume A7:x in Z; A8:exp_R is_differentiable_in x by SIN_COS:65; A9:sin-cos is_differentiable_in x by A4,A7,FDIFF_1:9; A10:(sin-cos).x=sin.x-cos.x by A3,A7,VALUED_1:13; A11:exp_R.x <>0 by SIN_COS:54; (((1/2)(#)((sin-cos)/exp_R))`|Z).x=(1/2)*(diff((sin-cos)/exp_R,x)) by A1,A5,A7,FDIFF_1:20 .=(1/2)*((diff(sin-cos,x) * exp_R.x - diff(exp_R,x) *(sin-cos).x)/(exp_R.x)^2) by A8,A9,A11,FDIFF_2:14 .=(1/2)*((((sin-cos)`|Z).x* exp_R.x - diff(exp_R,x) *(sin-cos).x)/(exp_R.x)^2) by A4,A7,FDIFF_1:def 7 .=(1/2)*(((cos.x+sin.x)* exp_R.x - diff(exp_R,x) *(sin-cos).x)/(exp_R.x)^2) by A3,A7,FDIFF_7:39 .=(1/2)*(((cos.x+sin.x)* exp_R.x - exp_R.x*(sin.x-cos.x))/(exp_R.x)^2) by A10,SIN_COS:65 .=(1/2)*((2*cos.x)*(exp_R.x/((exp_R.x)*(exp_R.x)))) .=(1/2)*((2*cos.x)*((exp_R.x)/(exp_R.x)/(exp_R.x))) by XCMPLX_1:78 .=(1/2)*((2*cos.x)*(1/exp_R.x)) by A11,XCMPLX_1:60 .=cos.x/exp_R.x; hence thesis; end; hence thesis by A6; end; ::f.x=cos.x/exp_R.x theorem A c= Z & f=cos/exp_R & Z c= dom ((1/2)(#)((sin-cos)/exp_R)) & Z = dom f & f|A is continuous implies integral(f,A)=((1/2)(#)((sin-cos)/exp_R)).(upper_bound A) -((1/2)(#)((sin-cos)/exp_R)).(lower_bound A) proof assume A1:A c= Z & f=cos/exp_R & Z c= dom ((1/2)(#)((sin-cos)/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:(1/2)(#)((sin-cos)/exp_R) is_differentiable_on Z by A1,Th9; A4:for x st x in Z holds f.x=cos.x/exp_R.x by A1,RFUNCT_1:def 1; A5:for x being Element of REAL st x in dom (((1/2)(#)((sin-cos)/exp_R))`|Z) holds (((1/2)(#)((sin-cos)/exp_R))`|Z).x=f.x proof let x be Element of REAL; assume x in dom (((1/2)(#)((sin-cos)/exp_R))`|Z);then A6:x in Z by A3,FDIFF_1:def 7;then (((1/2)(#)((sin-cos)/exp_R))`|Z).x=cos.x/exp_R.x by A1,Th9 .=f.x by A4,A6; hence thesis; end; dom (((1/2)(#)((sin-cos)/exp_R))`|Z)=dom f by A1,A3,FDIFF_1:def 7; then (((1/2)(#)((sin-cos)/exp_R))`|Z)= f by A5,PARTFUN1:5; hence thesis by A1,A2,Th9,INTEGRA5:13; end; ::f.x=exp_R.x*(sin.x+cos.x) theorem A c= Z & f=exp_R(#)(sin+cos) & Z c= dom (exp_R(#)sin) & Z = dom f & f|A is continuous implies integral(f,A)=(exp_R(#)sin).(upper_bound A)-(exp_R(#)sin).(lower_bound A) proof assume A1:A c= Z & f=exp_R(#)(sin+cos) & Z c= dom (exp_R(#)sin) & 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(#)sin is_differentiable_on Z by A1,FDIFF_7:44; dom f = dom exp_R /\ dom (sin+cos) by A1,VALUED_1:def 4;then A4:Z c= dom (sin+cos) by A1,XBOOLE_1:18; A5:for x st x in Z holds f.x=exp_R.x*(sin.x+cos.x) proof let x; assume A6:x in Z; (exp_R(#)(sin+cos)).x=exp_R.x*((sin+cos).x) by VALUED_1:5 .=exp_R.x*(sin.x+cos.x) by A4,A6,VALUED_1:def 1; hence thesis by A1; end; A7:for x being Element of REAL st x in dom ((exp_R(#)sin)`|Z) holds ((exp_R(#)sin)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((exp_R(#)sin)`|Z);then A8:x in Z by A3,FDIFF_1:def 7;then ((exp_R(#)sin)`|Z).x=exp_R.x*(sin.x+cos.x) by A1,FDIFF_7:44 .=f.x by A5,A8; hence thesis; end; dom ((exp_R(#)sin)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((exp_R(#)sin)`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,FDIFF_7:44,INTEGRA5:13; end; ::f.x=exp_R.x*(cos.x-sin.x) theorem A c= Z & f=exp_R(#)(cos-sin) & Z c= dom (exp_R(#)cos) & Z = dom f & f|A is continuous implies integral(f,A)=(exp_R(#)cos).(upper_bound A)-(exp_R(#)cos).(lower_bound A) proof assume A1:A c= Z & f=exp_R(#)(cos-sin) & Z c= dom (exp_R(#)cos) & 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(#)cos is_differentiable_on Z by A1,FDIFF_7:45; dom f = dom exp_R /\ dom (cos-sin) by A1,VALUED_1:def 4;then A4:Z c= dom (cos-sin) by A1,XBOOLE_1:18; A5:for x st x in Z holds f.x=exp_R.x*(cos.x-sin.x) proof let x; assume A6:x in Z; (exp_R(#)(cos-sin)).x=exp_R.x*((cos-sin).x) by VALUED_1:5 .=exp_R.x*(cos.x-sin.x) by A4,A6,VALUED_1:13; hence thesis by A1; end; A7:for x being Element of REAL st x in dom ((exp_R(#)cos)`|Z) holds ((exp_R(#)cos)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((exp_R(#)cos)`|Z);then A8:x in Z by A3,FDIFF_1:def 7;then ((exp_R(#)cos)`|Z).x=exp_R.x*(cos.x-sin.x) by A1,FDIFF_7:45 .=f.x by A5,A8; hence thesis; end; dom ((exp_R(#)cos)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((exp_R(#)cos)`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,FDIFF_7:45,INTEGRA5:13; end; ::f.x=-sin.x/cos.x/x^2+1/x/(cos.x)^2 theorem A c= Z & f1=#Z 2 & f=-sin/cos/f1 + (id Z)^/cos^2 & Z c= dom ((id Z)^(#)tan) & Z = dom f & f|A is continuous implies integral(f,A)=((id Z)^(#)tan).(upper_bound A)-((id Z)^(#)tan).(lower_bound A) proof assume A1:A c= Z & f1=#Z 2 & f= -sin/cos/f1 + (id Z)^/cos^2 & Z c= dom ((id Z)^(#)tan) & Z = dom f & f|A is continuous; then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; set g = id Z; Z c= dom (g^) /\ dom tan by A1,VALUED_1:def 4; then A3:Z c= dom (g^) 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)^(#)tan is_differentiable_on Z by A1,FDIFF_8:34; dom f = dom (-sin/cos/f1) /\ dom ((id Z)^/cos^2) by A1,VALUED_1:def 1;then dom f c= dom (-sin/cos/f1) & dom f c= dom ((id Z)^/cos^2) by XBOOLE_1:18; then A7:Z c= dom (sin/cos/f1) & Z c= dom ((id Z)^/cos^2) by A1,VALUED_1:8; dom (sin/cos/f1) = dom (sin/cos) /\ (dom f1 \ f1"{0}) by RFUNCT_1:def 1;then A8:Z c= dom (sin/cos) by A7,XBOOLE_1:18; dom ((id Z)^/cos^2) c= dom ((id Z)^) /\ (dom (cos^2) \ (cos^2)"{0}) by RFUNCT_1:def 1;then dom ((id Z)^/cos^2) c= dom ((id Z)^) & dom ((id Z)^/cos^2) c= dom (cos^2) \ (cos^2)"{0} by XBOOLE_1:18;then A9:Z c= dom ((id Z)^) & Z c= dom (cos^2) \ (cos^2)"{0} by A7; A10:for x st x in Z holds f.x=-sin.x/cos.x/x^2+1/x/(cos.x)^2 proof let x; assume A11:x in Z;then (-sin/cos/f1 + (id Z)^/cos^2).x =(-sin/cos/f1).x+((id Z)^/cos^2).x by A1,VALUED_1:def 1 .=-(sin/cos/f1).x+((id Z)^/cos^2).x by VALUED_1:8 .=-((sin/cos).x/f1.x)+((id Z)^/cos^2).x by A11,A7,RFUNCT_1:def 1 .=-((sin.x*(cos.x)")/f1.x)+((id Z)^/cos^2).x by A8,A11,RFUNCT_1:def 1 .=-sin.x/cos.x/f1.x+((id Z)^).x/(cos^2).x by A7,A11,RFUNCT_1:def 1 .=-sin.x/cos.x/f1.x+(((id Z).x)")/(cos^2).x by A9,A11,RFUNCT_1:def 2 .=-sin.x/cos.x/f1.x+1/x/(cos^2).x by A11,FUNCT_1:18 .=-sin.x/cos.x/f1.x+1/x/(cos.x)^2 by VALUED_1:11 .=-sin.x/cos.x/(x #Z 2)+1/x/(cos.x)^2 by A1,TAYLOR_1:def 1 .=-sin.x/cos.x/x^2+1/x/(cos.x)^2 by FDIFF_7:1; hence thesis by A1; end; A12:for x being Element of REAL st x in dom(((id Z)^(#)tan)`|Z) holds (((id Z)^(#)tan)`|Z).x=f.x proof let x be Element of REAL; assume x in dom(((id Z)^(#)tan)`|Z);then A13:x in Z by A6,FDIFF_1:def 7;then (((id Z)^(#)tan)`|Z).x=-sin.x/cos.x/x^2+1/x/(cos.x)^2 by A4,A1,FDIFF_8:34 .=f.x by A13,A10; hence thesis; end; dom(((id Z)^(#)tan)`|Z)=dom f by A1,A6,FDIFF_1:def 7; then(((id Z)^(#)tan)`|Z)= f by A12,PARTFUN1:5; hence thesis by A1,A2,A6,INTEGRA5:13; end; ::f.x=-cos.x/sin.x/x^2-1/x/(sin.x)^2 theorem A c= Z & f=-cos/sin/f1-(id Z)^/sin^2 & f1=#Z 2 & Z c= dom ((id Z)^(#)cot) & Z = dom f & f|A is continuous implies integral(f,A)=((id Z)^(#)cot).(upper_bound A)-((id Z)^(#)cot).(lower_bound A) proof assume A1:A c= Z & f=-cos/sin/f1-(id Z)^/sin^2 & f1=#Z 2 & Z c= dom ((id Z)^(#)cot) & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; set g = id Z; Z c= dom (g^(#)cot) by A1; then Z c= dom (g^) /\ dom cot by VALUED_1:def 4;then A3:Z c= dom (g^) 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)^(#)cot is_differentiable_on Z by A1,FDIFF_8:35; dom f = dom (-cos/sin/f1) /\ dom ((id Z)^/sin^2) by A1,VALUED_1:12;then A7:dom f c= dom (-cos/sin/f1) & dom f c= dom ((id Z)^/sin^2) by XBOOLE_1:18; then dom f c= dom (cos/sin/f1) by VALUED_1:8; then A8:Z c= dom (cos/sin/f1) & Z c= dom ((id Z)^/sin^2) by A1,A7; dom (cos/sin/f1) = dom (cos/sin) /\ (dom f1 \ f1"{0}) by RFUNCT_1:def 1;then A9:Z c= dom (cos/sin) by A8,XBOOLE_1:18; dom ((id Z)^/sin^2) c= dom ((id Z)^) /\ (dom (sin^2) \ (sin^2)"{0}) by RFUNCT_1:def 1;then dom ((id Z)^/sin^2) c= dom ((id Z)^) & dom ((id Z)^/sin^2) c= dom (sin^2) \ (sin^2)"{0} by XBOOLE_1:18;then A10:Z c= dom ((id Z)^) & Z c= dom (sin^2) \ (sin^2)"{0} by A8; A11:for x st x in Z holds f.x=-cos.x/sin.x/x^2-1/x/(sin.x)^2 proof let x; assume A12:x in Z;then (-cos/sin/f1 - (id Z)^/sin^2).x =(-cos/sin/f1).x-((id Z)^/sin^2).x by A1,VALUED_1:13 .=-(cos/sin/f1).x-((id Z)^/sin^2).x by VALUED_1:8 .=-((cos/sin).x/f1.x)-((id Z)^/sin^2).x by A12,A8,RFUNCT_1:def 1 .=-cos.x/sin.x/f1.x-((id Z)^/sin^2).x by A9,A12,RFUNCT_1:def 1 .=-cos.x/sin.x/f1.x-((id Z)^).x/(sin^2).x by A8,A12,RFUNCT_1:def 1 .=-cos.x/sin.x/f1.x-(((id Z).x)")/(sin^2).x by A10,A12,RFUNCT_1:def 2 .=-cos.x/sin.x/f1.x-1/x/(sin^2).x by A12,FUNCT_1:18 .=-cos.x/sin.x/f1.x-1/x/(sin.x)^2 by VALUED_1:11 .=-cos.x/sin.x/(x #Z 2)-1/x/(sin.x)^2 by A1,TAYLOR_1:def 1 .=-cos.x/sin.x/x^2-1/x/(sin.x)^2 by FDIFF_7:1; hence thesis by A1; end; A13:for x being Element of REAL st x in dom(((id Z)^(#)cot)`|Z) holds (((id Z)^(#)cot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom(((id Z)^(#)cot)`|Z);then A14:x in Z by A6,FDIFF_1:def 7;then (((id Z)^(#)cot)`|Z).x=-cos.x/sin.x/x^2-1/x/(sin.x)^2 by A1,A4,FDIFF_8:35 .=f.x by A11,A14; hence thesis; end; dom(((id Z)^(#)cot)`|Z)=dom f by A1,A6,FDIFF_1:def 7; then(((id Z)^(#)cot)`|Z)= f by A13,PARTFUN1:5; hence thesis by A1,A2,A6,INTEGRA5:13; end; ::f.x=sin.x/cos.x/x+ln.x/(cos.x)^2 theorem A c= Z & f=sin/cos/(id Z)+ln/cos^2 & Z c= dom (ln(#)tan) & Z = dom f & f|A is continuous implies integral(f,A)=(ln(#)tan).(upper_bound A)-(ln(#)tan).(lower_bound A) proof assume A1:A c= Z & f=sin/cos/(id Z)+ln/cos^2 & Z c= dom (ln(#)tan) & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:(ln(#)tan) is_differentiable_on Z by A1,FDIFF_8:32; Z = dom (sin/cos/(id Z)) /\ dom (ln/cos^2) by A1,VALUED_1:def 1; then A4:Z c= dom (sin/cos/(id Z)) & Z c= dom (ln/cos^2) by XBOOLE_1:18; dom (sin/cos/(id Z)) c= dom (sin/cos) /\ (dom (id Z) \ (id Z)"{0}) by RFUNCT_1:def 1;then dom (sin/cos/(id Z)) c= dom (sin/cos) by XBOOLE_1:18;then A5:Z c= dom (sin/cos) by A4; A6:for x st x in Z holds f.x=sin.x/cos.x/x+ln.x/(cos.x)^2 proof let x; assume A7:x in Z;then (sin/cos/(id Z)+ln/cos^2).x=(sin/cos/(id Z)).x+(ln/cos^2).x by A1,VALUED_1:def 1 .=(sin/cos).x/(id Z).x+(ln/cos^2).x by A7,A4,RFUNCT_1:def 1 .=sin.x/cos.x/(id Z).x+(ln/cos^2).x by A5,A7,RFUNCT_1:def 1 .=sin.x/cos.x/x+(ln/cos^2).x by A7,FUNCT_1:18 .=sin.x/cos.x/x+ln.x/(cos^2).x by A7,A4,RFUNCT_1:def 1 .=sin.x/cos.x/x+ln.x/(cos.x)^2 by VALUED_1:11; hence thesis by A1; end; A8:for x being Element of REAL st x in dom ((ln(#)tan)`|Z) holds ((ln(#)tan)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((ln(#)tan)`|Z);then A9:x in Z by A3,FDIFF_1:def 7;then ((ln(#)tan)`|Z).x=sin.x/cos.x/x+ln.x/(cos.x)^2 by A1,FDIFF_8:32 .=f.x by A9,A6; hence thesis; end; dom ((ln(#)tan)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((ln(#)tan)`|Z)= f by A8,PARTFUN1:5; hence thesis by A1,A2,FDIFF_8:32,INTEGRA5:13; end; ::f.x=cos.x/sin.x/x-ln.x/(sin.x)^2 theorem A c= Z & f=cos/sin/(id Z)-ln/sin^2 & Z c= dom (ln(#)cot) & Z = dom f & f|A is continuous implies integral(f,A)=(ln(#)cot).(upper_bound A)-(ln(#)cot).(lower_bound A) proof assume A1:A c= Z & f=cos/sin/(id Z)-ln/sin^2 & Z c= dom (ln(#)cot) & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:(ln(#)cot) is_differentiable_on Z by A1,FDIFF_8:33; Z = dom (cos/sin/(id Z)) /\ dom (ln/sin^2) by A1,VALUED_1:12; then A4:Z c= dom (cos/sin/(id Z)) & Z c= dom (ln/sin^2) by XBOOLE_1:18; dom (cos/sin/(id Z)) c= dom (cos/sin) /\ (dom (id Z) \ (id Z)"{0}) by RFUNCT_1:def 1;then dom (cos/sin/(id Z)) c= dom (cos/sin) by XBOOLE_1:18;then A5:Z c= dom (cos/sin) by A4; A6:for x st x in Z holds f.x=cos.x/sin.x/x-ln.x/(sin.x)^2 proof let x; assume A7:x in Z;then (cos/sin/(id Z)-ln/sin^2).x=(cos/sin/(id Z)).x-(ln/sin^2).x by A1,VALUED_1:13 .=(cos/sin).x/(id Z).x-(ln/sin^2).x by A7,A4,RFUNCT_1:def 1 .=cos.x/sin.x/(id Z).x-(ln/sin^2).x by A5,A7,RFUNCT_1:def 1 .=cos.x/sin.x/x-(ln/sin^2).x by A7,FUNCT_1:18 .=cos.x/sin.x/x-ln.x/(sin^2).x by A7,A4,RFUNCT_1:def 1 .=cos.x/sin.x/x-ln.x/(sin.x)^2 by VALUED_1:11; hence thesis by A1; end; A8:for x being Element of REAL st x in dom ((ln(#)cot)`|Z) holds ((ln(#)cot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((ln(#)cot)`|Z);then A9:x in Z by A3,FDIFF_1:def 7;then ((ln(#)cot)`|Z).x=cos.x/sin.x/x-ln.x/(sin.x)^2 by A1,FDIFF_8:33 .=f.x by A9,A6; hence thesis; end; dom ((ln(#)cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((ln(#)cot)`|Z)= f by A8,PARTFUN1:5; hence thesis by A1,A2,FDIFF_8:33,INTEGRA5:13; end; ::f.x=tan.x/x+ln.x/(cos.x)^2 theorem A c= Z & f=tan/(id Z)+ln/cos^2 & Z c= dom (ln(#)tan) & Z c= dom tan & Z = dom f & f|A is continuous implies integral(f,A)=(ln(#)tan).(upper_bound A)-(ln(#)tan).(lower_bound A) proof assume A1:A c= Z & f=tan/(id Z)+ln/cos^2 & Z c= dom (ln(#)tan) & Z c= dom tan & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:(ln(#)tan) is_differentiable_on Z by A1,FDIFF_8:32; Z = dom (tan/(id Z)) /\ dom(ln/cos^2) by A1,VALUED_1:def 1;then A4:Z c= dom (tan/(id Z)) & Z c= dom(ln/cos^2) by XBOOLE_1:18; A5:for x st x in Z holds f.x=tan.x/x+ln.x/(cos.x)^2 proof let x; assume A6:x in Z;then (tan/(id Z)+ln/cos^2).x =(tan/(id Z)).x+(ln/cos^2).x by A1,VALUED_1:def 1 .=tan.x/(id Z).x+(ln/cos^2).x by A6,A4,RFUNCT_1:def 1 .=tan.x/x+(ln/cos^2).x by A6,FUNCT_1:18 .=tan.x/x+ln.x/(cos^2).x by A6,A4,RFUNCT_1:def 1 .=tan.x/x+ln.x/(cos.x)^2 by VALUED_1:11; hence thesis by A1; end; A7:for x being Element of REAL st x in dom ((ln(#)tan)`|Z) holds ((ln(#)tan)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((ln(#)tan)`|Z);then A8:x in Z by A3,FDIFF_1:def 7;then ((ln(#)tan)`|Z).x=tan(x)/x+ln.x/(cos.x)^2 by A1,FDIFF_8:32 .=tan.x/x+ln.x/(cos.x)^2 by A1,A8,FDIFF_8:1,SIN_COS9:15 .=f.x by A8,A5; hence thesis; end; dom ((ln(#)tan)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((ln(#)tan)`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,FDIFF_8:32,INTEGRA5:13; end; ::f.x=cot.x/x-ln.x/(sin.x)^2 theorem A c= Z & f=cot/(id Z)-ln/sin^2 & Z c= dom (ln(#)cot) & Z c= dom cot & Z = dom f & f|A is continuous implies integral(f,A)=(ln(#)cot).(upper_bound A)-(ln(#)cot).(lower_bound A) proof assume A1:A c= Z & f=cot/(id Z)-ln/sin^2 & Z c= dom (ln(#)cot) & Z c= dom cot & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:(ln(#)cot) is_differentiable_on Z by A1,FDIFF_8:33; Z = dom (cot/(id Z)) /\ dom(ln/sin^2) by A1,VALUED_1:12;then A4:Z c= dom (cot/(id Z)) & Z c= dom(ln/sin^2) by XBOOLE_1:18; A5:for x st x in Z holds f.x=cot.x/x-ln.x/(sin.x)^2 proof let x; assume A6:x in Z;then (cot/(id Z)-ln/sin^2).x =(cot/(id Z)).x-(ln/sin^2).x by A1,VALUED_1:13 .=cot.x/(id Z).x-(ln/sin^2).x by A6,A4,RFUNCT_1:def 1 .=cot.x/x-(ln/sin^2).x by A6,FUNCT_1:18 .=cot.x/x-ln.x/(sin^2).x by A6,A4,RFUNCT_1:def 1 .=cot.x/x-ln.x/(sin.x)^2 by VALUED_1:11; hence thesis by A1; end; A7:for x being Element of REAL st x in dom ((ln(#)cot)`|Z) holds ((ln(#)cot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((ln(#)cot)`|Z);then A8:x in Z by A3,FDIFF_1:def 7;then ((ln(#)cot)`|Z).x=cot(x)/x-ln.x/(sin.x)^2 by A1,FDIFF_8:33 .=cot.x/x-ln.x/(sin.x)^2 by A1,A8,FDIFF_8:2,SIN_COS9:16 .=f.x by A5,A8; hence thesis; end; dom ((ln(#)cot)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((ln(#)cot)`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,FDIFF_8:33,INTEGRA5:13; end; ::f.x=arctan.x/x+ln.x/(1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/(id Z)+ln/(f1+( #Z 2)) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies integral(f,A)=(ln(#)arctan).(upper_bound A)-(ln(#)arctan).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/(id Z)+ln/(f1+( #Z 2)) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous; then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; Z = dom (arctan/(id Z)) /\ dom (ln/(f1+( #Z 2))) by A1,VALUED_1:def 1; then A3:Z c= dom (arctan/(id Z)) & Z c= dom (ln/(f1+( #Z 2))) by XBOOLE_1:18; then Z c= dom (arctan) /\ (dom (id Z) \ (id Z)"{0}) by RFUNCT_1:def 1;then A4:Z c= dom (arctan) by XBOOLE_1:18; Z c= dom ln /\ (dom (f1+( #Z 2)) \ (f1+( #Z 2))"{0}) by A3,RFUNCT_1:def 1; then A5:Z c= dom ln & Z c= (dom (f1+( #Z 2)) \ (f1+( #Z 2))"{0}) by XBOOLE_1:18; then Z c= dom (arctan) /\ dom ln by A4,XBOOLE_1:19;then A6:Z c= dom (ln(#)arctan) by VALUED_1:def 4; then A7:ln(#)arctan is_differentiable_on Z by A1,SIN_COS9:127; A8:Z c= dom ((f1+#Z 2)^) by A5,RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A9:Z c= dom (f1+#Z 2) by A8; A10:for x st x in Z holds f.x=arctan.x/x+ln.x/(1+x^2) proof let x; assume A11:x in Z; then (arctan/(id Z)+ln/(f1+( #Z 2))).x =(arctan/(id Z)).x+(ln/(f1+( #Z 2))).x by A1,VALUED_1:def 1 .=arctan.x*((id Z).x)" +(ln/(f1+( #Z 2))).x by A3,A11,RFUNCT_1:def 1 .=arctan.x*((id Z).x)"+(ln.x*((f1+( #Z 2)).x)") by A3,A11,RFUNCT_1:def 1 .=arctan.x/x+(ln.x/(f1+( #Z 2)).x) by A11,FUNCT_1:18 .=arctan.x/x+ln.x/(f1.x+( #Z 2).x) by A9,A11,VALUED_1:def 1 .=arctan.x/x+ln.x/(1+( #Z 2).x) by A1,A11 .=arctan.x/x+ln.x/(1+(x #Z 2)) by TAYLOR_1:def 1 .=arctan.x/x+ln.x/(1+x^2) by FDIFF_7:1; hence thesis by A1; end; A12:for x being Element of REAL st x in dom((ln(#)arctan)`|Z) holds ((ln(#)arctan)`|Z).x=f.x proof let x be Element of REAL; assume x in dom((ln(#)arctan)`|Z);then A13: x in Z by A7,FDIFF_1:def 7;then ((ln(#)arctan)`|Z).x=arctan.x/x+ln.x/(1+x^2) by A1,A6,SIN_COS9:127 .=f.x by A13,A10; hence thesis; end; dom((ln(#)arctan)`|Z)=dom f by A1,A7,FDIFF_1:def 7; then ((ln(#)arctan)`|Z)= f by A12,PARTFUN1:5; hence thesis by A1,A2,A6,INTEGRA5:13,SIN_COS9:127; end; ::f.x=arccot.x/x-ln.x/(1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/(id Z)-ln/(f1+( #Z 2)) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies integral(f,A)=(ln(#)arccot).(upper_bound A)-(ln(#)arccot).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/(id Z)-ln/(f1+( #Z 2)) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous; then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; Z = dom (arccot/(id Z)) /\ dom (ln/(f1+( #Z 2))) by A1,VALUED_1:12; then A3:Z c= dom (arccot/(id Z)) & Z c= dom (ln/(f1+( #Z 2))) by XBOOLE_1:18; then Z c= dom (arccot) /\ (dom (id Z) \ (id Z)"{0}) by RFUNCT_1:def 1;then A4:Z c= dom (arccot) by XBOOLE_1:18; Z c= dom ln /\ (dom (f1+( #Z 2)) \ (f1+( #Z 2))"{0}) by A3,RFUNCT_1:def 1; then A5:Z c= dom ln & Z c= (dom (f1+( #Z 2)) \ (f1+( #Z 2))"{0}) by XBOOLE_1:18; then Z c= dom (arccot) /\ dom ln by A4,XBOOLE_1:19;then A6:Z c= dom (ln(#)arccot) by VALUED_1:def 4; then A7:ln(#)arccot is_differentiable_on Z by A1,SIN_COS9:128; A8:Z c= dom ((f1+#Z 2)^) by A5,RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A9:Z c= dom (f1+#Z 2) by A8; A10:for x st x in Z holds f.x=arccot.x/x-ln.x/(1+x^2) proof let x; assume A11:x in Z; then (arccot/(id Z)-ln/(f1+( #Z 2))).x =(arccot/(id Z)).x-(ln/(f1+( #Z 2))).x by A1,VALUED_1:13 .=arccot.x*((id Z).x)" -(ln/(f1+( #Z 2))).x by A3,A11,RFUNCT_1:def 1 .=arccot.x*((id Z).x)"-(ln.x*((f1+( #Z 2)).x)") by A3,A11,RFUNCT_1:def 1 .=arccot.x/x-(ln.x/(f1+( #Z 2)).x) by A11,FUNCT_1:18 .=arccot.x/x-ln.x/(f1.x+( #Z 2).x) by A9,A11,VALUED_1:def 1 .=arccot.x/x-ln.x/(1+( #Z 2).x) by A1,A11 .=arccot.x/x-ln.x/(1+(x #Z 2)) by TAYLOR_1:def 1 .=arccot.x/x-ln.x/(1+x^2) by FDIFF_7:1; hence thesis by A1; end; A12:for x being Element of REAL st x in dom((ln(#)arccot)`|Z) holds ((ln(#)arccot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom((ln(#)arccot)`|Z);then A13:x in Z by A7,FDIFF_1:def 7;then ((ln(#)arccot)`|Z).x=arccot.x/x-ln.x/(1+x^2) by A1,A6,SIN_COS9:128 .=f.x by A10,A13; hence thesis; end; dom((ln(#)arccot)`|Z)=dom f by A1,A7,FDIFF_1:def 7; then ((ln(#)arccot)`|Z)= f by A12,PARTFUN1:5; hence thesis by A1,A2,A6,INTEGRA5:13,SIN_COS9:128; end; ::f.x=exp_R.(tan.x)/(cos.x)^2 theorem A c= Z & f=exp_R*tan/cos^2 & Z = dom f & f|A is continuous implies integral(f,A)=(exp_R*tan).(upper_bound A)-(exp_R*tan).(lower_bound A) proof assume A1:A c= Z & f=exp_R*tan/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*tan) /\ (dom (cos^2) \ (cos^2)"{0}) by A1,RFUNCT_1:def 1;then A3:Z c= dom (exp_R*tan) by XBOOLE_1:18; then A4:exp_R*tan is_differentiable_on Z by FDIFF_8:16; A5:for x st x in Z holds f.x=exp_R.(tan.x)/(cos.x)^2 proof let x; assume A6:x in Z; then (exp_R*tan/cos^2).x=(exp_R*tan).x/(cos^2).x by A1,RFUNCT_1:def 1 .=exp_R.(tan.x)/(cos^2).x by A3,A6,FUNCT_1:12 .=exp_R.(tan.x)/(cos.x)^2 by VALUED_1:11; hence thesis by A1; end; A7:for x being Element of REAL st x in dom ((exp_R*tan)`|Z) holds ((exp_R*tan)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((exp_R*tan)`|Z);then A8:x in Z by A4,FDIFF_1:def 7;then ((exp_R*tan)`|Z).x=exp_R.(tan.x)/(cos.x)^2 by A3,FDIFF_8:16 .=f.x by A5,A8; hence thesis; end; dom ((exp_R*tan)`|Z)=dom f by A1,A4,FDIFF_1:def 7; then ((exp_R*tan)`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,A3,FDIFF_8:16,INTEGRA5:13; end; ::f.x=-exp_R.(cot.x)/(sin.x)^2 theorem A c= Z & f=-exp_R*cot/sin^2 & Z = dom f & f|A is continuous implies integral(f,A)=(exp_R*cot).(upper_bound A)-(exp_R*cot).(lower_bound A) proof assume A1:A c= Z & f=-exp_R*cot/sin^2 & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:Z = dom (exp_R*cot/sin^2) by A1,VALUED_1:8; then Z c= dom (exp_R*cot) /\ (dom (sin^2) \ (sin^2)"{0}) by RFUNCT_1:def 1;then A4:Z c= dom (exp_R*cot) by XBOOLE_1:18; then A5:exp_R*cot is_differentiable_on Z by FDIFF_8:17; A6:for x st x in Z holds f.x=-exp_R.(cot.x)/(sin.x)^2 proof let x; assume A7:x in Z; (-exp_R*cot/sin^2).x =-(exp_R*cot/sin^2).x by VALUED_1:8 .=-(exp_R*cot).x/(sin^2).x by A7,A3,RFUNCT_1:def 1 .=-exp_R.(cot.x)/(sin^2).x by A4,A7,FUNCT_1:12 .=-exp_R.(cot.x)/(sin.x)^2 by VALUED_1:11; hence thesis by A1; end; A8:for x being Element of REAL st x in dom ((exp_R*cot)`|Z) holds ((exp_R*cot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((exp_R*cot)`|Z);then A9:x in Z by A5,FDIFF_1:def 7;then ((exp_R*cot)`|Z).x=-exp_R.(cot.x)/(sin.x)^2 by A4,FDIFF_8:17 .=f.x by A6,A9; hence thesis; end; dom ((exp_R*cot)`|Z)=dom f by A1,A5,FDIFF_1:def 7; then ((exp_R*cot)`|Z)= f by A8,PARTFUN1:5; hence thesis by A1,A2,A4,FDIFF_8:17,INTEGRA5:13; end; theorem Th23: Z c= dom (exp_R*cot) implies -exp_R*cot is_differentiable_on Z & for x st x in Z holds ((-exp_R*cot)`|Z).x = exp_R.(cot.x)/(sin.x)^2 proof assume A1:Z c= dom (exp_R*cot); then A2:Z c= dom (-exp_R*cot) by VALUED_1:8; A3:for x st x in Z holds sin.x<>0 proof let x; assume x in Z; then x in dom (cos/sin) by A1,FUNCT_1:11; hence thesis by FDIFF_8:2; end; A4:exp_R*cot is_differentiable_on Z by A1,FDIFF_8:17; then A5:(-1)(#)(exp_R*cot) is_differentiable_on Z by A2,FDIFF_1:20; for x st x in Z holds ((-exp_R*cot)`|Z).x = exp_R.(cot.x)/(sin.x)^2 proof let x; assume A6:x in Z; then A7:sin.x<>0 by A3; then A8:cot is_differentiable_in x by FDIFF_7:47; A9:exp_R is_differentiable_in cot.x by SIN_COS:65; A10:exp_R*cot is_differentiable_in x by A4,A6,FDIFF_1:9; ((-exp_R*cot)`|Z).x=diff(-exp_R*cot,x) by A5,A6,FDIFF_1:def 7 .=(-1)*(diff(exp_R*cot,x)) by A10,FDIFF_1:15 .=(-1)*(diff(exp_R,cot.x)*diff(cot,x)) by A8,A9,FDIFF_2:13 .=(-1)*(diff(exp_R,cot.x)*(-1/(sin.x)^2)) by A7,FDIFF_7:47 .=(-1)*(exp_R.(cot.x) * (-1/(sin.x)^2)) by SIN_COS:65 .=exp_R.(cot.x)/(sin.x)^2; hence thesis; end; hence thesis by A2,A4,FDIFF_1:20; end; ::f.x=exp_R.(cot.x)/(sin.x)^2 theorem A c= Z & f=exp_R*cot/sin^2 & Z = dom f & f|A is continuous implies integral(f,A)=(-exp_R*cot).(upper_bound A)- (-exp_R*cot).(lower_bound A) proof assume A1: A c= Z & f=exp_R*cot/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*cot) /\ (dom (sin^2) \ (sin^2)"{0}) by A1,RFUNCT_1:def 1;then A3:Z c= dom (exp_R*cot) by XBOOLE_1:18; then A4:-exp_R*cot is_differentiable_on Z by Th23; A5:for x st x in Z holds f.x=exp_R.(cot.x)/(sin.x)^2 proof let x; assume A6:x in Z; then (exp_R*cot/sin^2).x=(exp_R*cot).x/(sin^2).x by A1,RFUNCT_1:def 1 .=exp_R.(cot.x)/(sin^2).x by A3,A6,FUNCT_1:12 .=exp_R.(cot.x)/(sin.x)^2 by VALUED_1:11; hence thesis by A1; end; A7:for x being Element of REAL st x in dom ((-exp_R*cot)`|Z) holds ((-exp_R*cot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((-exp_R*cot)`|Z);then A8:x in Z by A4,FDIFF_1:def 7;then ((-exp_R*cot)`|Z).x=exp_R.(cot.x)/(sin.x)^2 by Th23,A3 .=f.x by A5,A8; hence thesis; end; dom ((-exp_R*cot)`|Z)=dom f by A1,A4,FDIFF_1:def 7; then ((-exp_R*cot)`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,Th23,A3,INTEGRA5:13; end; ::f.x=1/(x*(cos.(ln.x))^2) theorem A c= Z & f=((id Z)(#)(cos*ln)^2)^ & Z c= dom (tan*ln) & Z = dom f & f|A is continuous implies integral(f,A)=(tan*ln).(upper_bound A)-(tan*ln).(lower_bound A) proof assume A1:A c= Z & f=((id Z)(#)(cos*ln)^2)^ & Z c= dom (tan*ln) & Z = dom f & f|A is continuous; then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:tan*ln is_differentiable_on Z by A1,FDIFF_8:14; Z c= dom ((id Z)(#)(cos*ln)^2) by A1,RFUNCT_1:1; then Z c= dom (id Z) /\ dom ((cos*ln)^2) by VALUED_1:def 4;then Z c= dom ((cos*ln)^2) by XBOOLE_1:18; then A4:Z c= dom (cos*ln) by VALUED_1:11; A5:for x st x in Z holds f.x=1/(x*(cos.(ln.x))^2) proof let x; assume A6:x in Z; then (((id Z)(#)(cos*ln)^2)^).x =1/(((id Z)(#)(cos*ln)^2).x) by A1,RFUNCT_1:def 2 .=1/((id Z).x*((cos*ln)^2).x) by VALUED_1:5 .=1/(x*((cos*ln)^2).x) by A6,FUNCT_1:18 .=1/(x*((cos*ln).x)^2) by VALUED_1:11 .=1/(x*(cos.(ln.x))^2) by A4,A6,FUNCT_1:12; hence thesis by A1; end; A7:for x being Element of REAL st x in dom ((tan*ln)`|Z) holds ((tan*ln)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((tan*ln)`|Z);then A8:x in Z by A3,FDIFF_1:def 7;then ((tan*ln)`|Z).x=1/(x*(cos.(ln.x))^2) by A1,FDIFF_8:14 .=f.x by A5,A8; hence thesis; end; dom ((tan*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((tan*ln)`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,FDIFF_8:14,INTEGRA5:13; end; ::f.x= -1/(x*(sin.(ln.x))^2) theorem A c= Z & f=-((id Z)(#)(sin*ln)^2)^ & Z c= dom (cot*ln) & Z = dom f & f|A is continuous implies integral(f,A)=(cot*ln).(upper_bound A)-(cot*ln).(lower_bound A) proof assume A1:A c= Z & f=-((id Z)(#)(sin*ln)^2)^ & Z c= dom (cot*ln) & Z = dom f & f|A is continuous; then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:cot*ln is_differentiable_on Z by A1,FDIFF_8:15; A4:Z = dom (((id Z)(#)(sin*ln)^2)^) by A1,VALUED_1:8; then Z c= dom ((id Z)(#)(sin*ln)^2) by RFUNCT_1:1; then Z c= dom (id Z) /\ dom ((sin*ln)^2) by VALUED_1:def 4;then Z c= dom ((sin*ln)^2) by XBOOLE_1:18; then A5:Z c= dom (sin*ln) by VALUED_1:11; A6:for x st x in Z holds f.x=-1/(x*(sin.(ln.x))^2) proof let x; assume A7:x in Z; (-((id Z)(#)(sin*ln)^2)^).x =-(((id Z)(#)(sin*ln)^2)^).x by VALUED_1:8 .=-1/(((id Z)(#)(sin*ln)^2).x) by A4,A7,RFUNCT_1:def 2 .=-1/((id Z).x*((sin*ln)^2).x) by VALUED_1:5 .=-1/(x*((sin*ln)^2).x) by A7,FUNCT_1:18 .=-1/(x*((sin*ln).x)^2) by VALUED_1:11 .=-1/(x*(sin.(ln.x))^2) by A5,A7,FUNCT_1:12; hence thesis by A1; end; A8:for x being Element of REAL st x in dom ((cot*ln)`|Z) holds ((cot*ln)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((cot*ln)`|Z);then A9:x in Z by A3,FDIFF_1:def 7;then ((cot*ln)`|Z).x= -1/(x*(sin.(ln.x))^2) by A1,FDIFF_8:15 .=f.x by A6,A9; hence thesis; end; dom ((cot*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((cot*ln)`|Z)= f by A8,PARTFUN1:5; hence thesis by A1,A2,FDIFF_8:15,INTEGRA5:13; end; theorem Th27: Z c= dom (cot*ln) implies -cot*ln is_differentiable_on Z & for x st x in Z holds ((-cot*ln)`|Z).x = 1/(x*(sin.(ln.x))^2) proof assume A1:Z c= dom (cot*ln); then A2:Z c= dom (-cot*ln) by VALUED_1:8; dom (cot*ln) c= dom ln by RELAT_1:25; then A3:Z c= dom ln by A1; A4: for x st x in Z holds x>0 proof let x; assume x in Z; then x in right_open_halfline(0) by A3,TAYLOR_1:18; then ex g being Real st x=g & 00 proof let x; assume x in Z; then ln.x in dom (cos/sin) by A1,FUNCT_1:11; hence thesis by FDIFF_8:2; end; A6:for x st x in Z holds diff(ln,x) = 1/x proof let x; assume x in Z; then x>0 by A4; then x in right_open_halfline(0) by Lm2; hence thesis by TAYLOR_1:18; end; A7:cot*ln is_differentiable_on Z by A1,FDIFF_8:15; then A8:(-1)(#)(cot*ln) is_differentiable_on Z by A2,FDIFF_1:20; for x st x in Z holds ((-cot*ln)`|Z).x = 1/(x*(sin.(ln.x))^2) proof let x; assume A9:x in Z; then A10:ln is_differentiable_in x by A4,TAYLOR_1:18; A11:x>0 & sin.(ln.x)<>0 by A4,A5,A9;then A12:cot is_differentiable_in ln.x by FDIFF_7:47; A13:cot*ln is_differentiable_in x by A7,A9,FDIFF_1:9; ((-cot*ln)`|Z).x=diff(-cot*ln,x) by A8,A9,FDIFF_1:def 7 .=(-1)*(diff(cot*ln,x)) by A13,FDIFF_1:15 .=(-1)*(diff(cot,ln.x)*diff(ln,x)) by A10,A12,FDIFF_2:13 .=(-1)*((-1/(sin.(ln.x))^2) * diff(ln,x)) by A11,FDIFF_7:47 .=(-1)*(-diff(ln,x)/(sin.(ln.x))^2) .=(-1)*(-(1/x)/(sin.(ln.x))^2) by A6,A9 .=1/(x*(sin.(ln.x))^2) by XCMPLX_1:78; hence thesis; end; hence thesis by A2,A7,FDIFF_1:20; end; ::f.x= 1/(x*(sin.(ln.x))^2) theorem A c= Z & f=((id Z)(#)(sin*ln)^2)^ & Z c= dom (cot*ln) & Z = dom f & f|A is continuous implies integral(f,A)=(-cot*ln).(upper_bound A)-(-cot*ln).(lower_bound A) proof assume A1:A c= Z & f=((id Z)(#)(sin*ln)^2)^ & Z c= dom (cot*ln) & Z = dom f & f|A is continuous; then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:-cot*ln is_differentiable_on Z by A1,Th27; Z c= dom ((id Z)(#)(sin*ln)^2) by A1,RFUNCT_1:1; then Z c= dom (id Z) /\ dom ((sin*ln)^2) by VALUED_1:def 4;then Z c= dom ((sin*ln)^2) by XBOOLE_1:18; then A4:Z c= dom (sin*ln) by VALUED_1:11; A5:for x st x in Z holds f.x=1/(x*(sin.(ln.x))^2) proof let x; assume A6:x in Z; then (((id Z)(#)(sin*ln)^2)^).x =1/(((id Z)(#)(sin*ln)^2).x) by A1,RFUNCT_1:def 2 .=1/((id Z).x*((sin*ln)^2).x) by VALUED_1:5 .=1/(x*((sin*ln)^2).x) by A6,FUNCT_1:18 .=1/(x*((sin*ln).x)^2) by VALUED_1:11 .=1/(x*(sin.(ln.x))^2) by A4,A6,FUNCT_1:12; hence thesis by A1; end; A7:for x being Element of REAL st x in dom ((-cot*ln)`|Z) holds ((-cot*ln)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((-cot*ln)`|Z);then A8:x in Z by A3,FDIFF_1:def 7;then ((-cot*ln)`|Z).x= 1/(x*(sin.(ln.x))^2) by A1,Th27 .=f.x by A5,A8; hence thesis; end; dom ((-cot*ln)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((-cot*ln)`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,Th27,INTEGRA5:13; end; ::f.x=exp_R.x/(cos.(exp_R.x))^2 theorem A c= Z & f=exp_R/(cos*exp_R)^2 & Z c= dom (tan*exp_R) & Z = dom f & f|A is continuous implies integral(f,A)=(tan*exp_R).(upper_bound A)-(tan*exp_R).(lower_bound A) proof assume A1:A c= Z & f=exp_R/(cos*exp_R)^2 & Z c= dom (tan*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:tan*exp_R is_differentiable_on Z by A1,FDIFF_8:12; Z = dom exp_R /\ (dom ((cos*exp_R)^2) \ ((cos*exp_R)^2)"{0}) by A1,RFUNCT_1:def 1;then Z c= dom ((cos*exp_R)^2) \ ((cos*exp_R)^2)"{0} by XBOOLE_1:18; then A4:Z c= dom (((cos*exp_R)^2)^) by RFUNCT_1:def 2; dom (((cos*exp_R)^2)^) c= dom ((cos*exp_R)^2) by RFUNCT_1:1;then Z c= dom ((cos*exp_R)^2) by A4; then A5:Z c= dom (cos*exp_R) by VALUED_1:11; A6:for x st x in Z holds f.x=exp_R.x/(cos.(exp_R.x))^2 proof let x; assume A7:x in Z; then (exp_R/(cos*exp_R)^2).x =exp_R.x/((cos*exp_R)^2).x by A1,RFUNCT_1:def 1 .=exp_R.x/((cos*exp_R).x)^2 by VALUED_1:11 .=exp_R.x/(cos.(exp_R.x))^2 by A5,A7,FUNCT_1:12; hence thesis by A1; end; A8:for x being Element of REAL st x in dom ((tan*exp_R)`|Z) holds ((tan*exp_R)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((tan*exp_R)`|Z);then A9:x in Z by A3,FDIFF_1:def 7;then ((tan*exp_R)`|Z).x=exp_R.x/(cos.(exp_R.x))^2 by A1,FDIFF_8:12 .=f.x by A6,A9; hence thesis; end; dom ((tan*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((tan*exp_R)`|Z)= f by A8,PARTFUN1:5; hence thesis by A1,A2,FDIFF_8:12,INTEGRA5:13; end; ::f.x=-exp_R.x/(sin.(exp_R.x))^2 theorem A c= Z & f=-exp_R/(sin*exp_R)^2 & Z c= dom (cot*exp_R) & Z = dom f & f|A is continuous implies integral(f,A)=(cot*exp_R).(upper_bound A)-(cot*exp_R).(lower_bound A) proof assume A1:A c= Z & f=-exp_R/(sin*exp_R)^2 & Z c= dom (cot*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:cot*exp_R is_differentiable_on Z by A1,FDIFF_8:13; A4:Z = dom (exp_R/(sin*exp_R)^2) by A1,VALUED_1:8; then Z c= dom (exp_R) /\ (dom ((sin*exp_R)^2) \ ((sin*exp_R)^2)"{0}) by RFUNCT_1:def 1;then Z c= dom ((sin*exp_R)^2) \ ((sin*exp_R)^2)"{0} by XBOOLE_1:18; then A5:Z c= dom (((sin*exp_R)^2)^) by RFUNCT_1:def 2; dom (((sin*exp_R)^2)^) c= dom ((sin*exp_R)^2) by RFUNCT_1:1;then Z c= dom ((sin*exp_R)^2) by A5; then A6:Z c= dom (sin*exp_R) by VALUED_1:11; A7:for x st x in Z holds f.x=-exp_R.x/(sin.(exp_R.x))^2 proof let x; assume A8:x in Z; (-exp_R/(sin*exp_R)^2).x =-(exp_R/(sin*exp_R)^2).x by VALUED_1:8 .=-exp_R.x/((sin*exp_R)^2).x by A4,A8,RFUNCT_1:def 1 .=-exp_R.x/((sin*exp_R).x)^2 by VALUED_1:11 .=-exp_R.x/(sin.(exp_R.x))^2 by A6,A8,FUNCT_1:12; hence thesis by A1; end; A9:for x being Element of REAL st x in dom ((cot*exp_R)`|Z) holds ((cot*exp_R)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((cot*exp_R)`|Z);then A10:x in Z by A3,FDIFF_1:def 7;then ((cot*exp_R)`|Z).x=-exp_R.x/(sin.(exp_R.x))^2 by A1,FDIFF_8:13 .=f.x by A7,A10; hence thesis; end; dom ((cot*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((cot*exp_R)`|Z)= f by A9,PARTFUN1:5; hence thesis by A1,A2,FDIFF_8:13,INTEGRA5:13; end; theorem Th31: Z c= dom (cot*exp_R) implies -cot*exp_R is_differentiable_on Z & for x st x in Z holds ((-cot*exp_R)`|Z).x = exp_R.x/(sin.(exp_R.x))^2 proof assume A1:Z c= dom (cot*exp_R); then A2:Z c= dom (-cot*exp_R) by VALUED_1:8; A3:cot*exp_R is_differentiable_on Z by A1,FDIFF_8:13; then A4:(-1)(#)(cot*exp_R) is_differentiable_on Z by A2,FDIFF_1:20; A5:for x st x in Z holds sin.(exp_R.x)<>0 proof let x; assume x in Z; then exp_R.x in dom (cos/sin) by A1,FUNCT_1:11; hence thesis by FDIFF_8:2; end; for x st x in Z holds ((-cot*exp_R)`|Z).x = exp_R.x/(sin.(exp_R.x))^2 proof let x; assume A6: x in Z; A7: exp_R is_differentiable_in x by SIN_COS:65; A8: sin.(exp_R.x)<>0 by A5,A6;then A9: cot is_differentiable_in exp_R.x by FDIFF_7:47; A10:cot*exp_R is_differentiable_in x by A3,A6,FDIFF_1:9; ((-cot*exp_R)`|Z).x=diff(-cot*exp_R,x) by A4,A6,FDIFF_1:def 7 .=(-1)*(diff(cot*exp_R,x)) by A10,FDIFF_1:15 .=(-1)*(diff(cot, exp_R.x)*diff(exp_R,x)) by A7,A9,FDIFF_2:13 .=(-1)*((-1/(sin.(exp_R.x))^2) * diff(exp_R,x)) by A8,FDIFF_7:47 .=(-1)*(-diff(exp_R,x)/(sin.(exp_R.x))^2) .=exp_R.x/(sin.(exp_R.x))^2 by SIN_COS:65; hence thesis; end; hence thesis by A4; end; ::f.x=exp_R.x/(sin.(exp_R.x))^2 theorem A c= Z & f=exp_R/(sin*exp_R)^2 & Z c= dom (cot*exp_R) & Z = dom f & f|A is continuous implies integral(f,A)=(-cot*exp_R).(upper_bound A)- (-cot*exp_R).(lower_bound A) proof assume A1:A c= Z & f=exp_R/(sin*exp_R)^2 & Z c= dom (cot*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:-cot*exp_R is_differentiable_on Z by A1,Th31; Z c= dom (exp_R) /\ (dom ((sin*exp_R)^2) \ ((sin*exp_R)^2)"{0}) by A1,RFUNCT_1:def 1;then Z c= dom ((sin*exp_R)^2) \ ((sin*exp_R)^2)"{0} by XBOOLE_1:18; then A4:Z c= dom (((sin*exp_R)^2)^) by RFUNCT_1:def 2; dom (((sin*exp_R)^2)^) c= dom ((sin*exp_R)^2) by RFUNCT_1:1;then Z c= dom ((sin*exp_R)^2) by A4; then A5:Z c= dom (sin*exp_R) by VALUED_1:11; A6:for x st x in Z holds f.x=exp_R.x/(sin.(exp_R.x))^2 proof let x; assume A7:x in Z;then (exp_R/(sin*exp_R)^2).x=exp_R.x/((sin*exp_R)^2).x by A1,RFUNCT_1:def 1 .=exp_R.x/((sin*exp_R).x)^2 by VALUED_1:11 .=exp_R.x/(sin.(exp_R.x))^2 by A5,A7,FUNCT_1:12; hence thesis by A1; end; A8:for x being Element of REAL st x in dom ((-cot*exp_R)`|Z) holds ((-cot*exp_R)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((-cot*exp_R)`|Z);then A9:x in Z by A3,FDIFF_1:def 7;then ((-cot*exp_R)`|Z).x=exp_R.x/(sin.(exp_R.x))^2 by A1,Th31 .=f.x by A6,A9; hence thesis; end; dom ((-cot*exp_R)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((-cot*exp_R)`|Z)= f by A8,PARTFUN1:5; hence thesis by A1,A2,Th31,INTEGRA5:13; end; ::f.x=-1/(x^2*(cos.(1/x))^2) theorem A c= Z & (for x st x in Z holds f.x=-1/(x^2*(cos.(1/x))^2)) & Z c= dom (tan*((id Z)^)) & Z = dom f & f|A is continuous implies integral(f,A)=(tan*((id Z)^)).(upper_bound A)- (tan*((id Z)^)).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f.x=-1/(x^2*(cos.(1/x))^2)) & Z c= dom (tan*((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:(tan*((id Z)^)) is_differentiable_on Z by A1,FDIFF_8:8; A7:for x being Element of REAL st x in dom ((tan*((id Z)^))`|Z) holds ((tan*((id Z)^))`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((tan*((id Z)^))`|Z);then A8:x in Z by A6,FDIFF_1:def 7;then ((tan*((id Z)^))`|Z).x=-1/(x^2*(cos.(1/x))^2) by A1,A4,FDIFF_8:8 .=f.x by A1,A8; hence thesis; end; dom ((tan*((id Z)^))`|Z)=dom f by A1,A6,FDIFF_1:def 7; then ((tan*((id Z)^))`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,A6,INTEGRA5:13; end; theorem Th34: Z c= dom (tan*((id Z)^)) implies (-tan*((id Z)^)) is_differentiable_on Z & for x st x in Z holds ((-tan*((id Z)^))`|Z).x = 1/(x^2*(cos.(1/x))^2) proof set f = id Z; assume A1:Z c= dom (tan*((id Z)^)); dom (tan*(f^)) c= dom (f^) by RELAT_1:25; then A2:Z c= dom (f^) by A1; A3:not 0 in Z proof assume A4: 0 in Z; dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2 .= dom id Z \ {0} by Lm1,A4; then not 0 in {0} by A4,A2,XBOOLE_0:def 5; hence thesis by TARSKI:def 1; end; A5:Z c= dom (-tan*((id Z)^)) by A1,VALUED_1:8; A6:(tan*((id Z)^)) is_differentiable_on Z by A1,A3,FDIFF_8:8; then A7:(-1)(#)(tan*((id Z)^)) is_differentiable_on Z by A5,FDIFF_1:20; A8:f^ is_differentiable_on Z & for x st x in Z holds ((f^)`|Z).x = -1/x^2 by A3,FDIFF_5:4; A9: for x st x in Z holds (cos.((f^).x))<>0 proof let x; assume x in Z; then f^.x in dom (sin/cos) by A1,FUNCT_1:11; hence thesis by FDIFF_8:1; end; for x st x in Z holds ((-tan*(f^))`|Z).x = 1/(x^2*(cos.(1/x))^2) proof let x; assume A10: x in Z; then A11: f^ is_differentiable_in x by A8,FDIFF_1:9; A12: cos.((f^).x)<>0 by A9,A10;then A13:tan is_differentiable_in (f^).x by FDIFF_7:46; A14:tan*(f^) is_differentiable_in x by A6,A10,FDIFF_1:9; ((-tan*(f^))`|Z).x=diff(-tan*(f^),x) by A7,A10,FDIFF_1:def 7 .=(-1)*(diff(tan*(f^),x)) by A14,FDIFF_1:15 .=(-1)*(diff(tan,(f^).x)*diff((f^),x)) by A11,A13,FDIFF_2:13 .=(-1)*((1/(cos.((f^).x))^2) * diff((f^),x)) by A12,FDIFF_7:46 .=(-1)*(diff((f^),x)/(cos.((f.x)"))^2) by A2,A10,RFUNCT_1:def 2 .=(-1)*(diff((f^),x)/(cos.(1*x"))^2) by A10,FUNCT_1:18 .=(-1)*(((f^)`|Z).x/(cos.(1*x"))^2) by A8,A10,FDIFF_1:def 7 .=(-1)*((-1/x^2)/(cos.(1*x"))^2) by A10,A3,FDIFF_5:4 .=(-1)*((-1)/x^2/(cos.(1/x))^2) .=(-1)*((-1)/(x^2*(cos.(1/x))^2)) by XCMPLX_1:78 .=1/(x^2*(cos.(1/x))^2); hence thesis; end; hence thesis by A7; end; ::f.x=1/(x^2*(cos.(1/x))^2) theorem A c= Z & (for x st x in Z holds f.x=1/(x^2*(cos.(1/x))^2)) & Z c= dom (tan*((id Z)^)) & Z = dom f & f|A is continuous implies integral(f,A)=(-tan*((id Z)^)).(upper_bound A) - (-tan*((id Z)^)).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f.x=1/(x^2*(cos.(1/x))^2)) & Z c= dom (tan*((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:(-tan*((id Z)^)) is_differentiable_on Z by A1,Th34; A4:for x being Element of REAL st x in dom ((-tan*((id Z)^))`|Z) holds ((-tan*((id Z)^))`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((-tan*((id Z)^))`|Z);then A5:x in Z by A3,FDIFF_1:def 7;then ((-tan*((id Z)^))`|Z).x=1/(x^2*(cos.(1/x))^2) by A1,Th34 .=f.x by A1,A5; hence thesis; end; dom ((-tan*((id Z)^))`|Z)=dom f by A1,A3,FDIFF_1:def 7; then ((-tan*((id Z)^))`|Z)= f by A4,PARTFUN1:5; hence thesis by A1,A2,A3,INTEGRA5:13; end; ::f.x=1/(x^2*(sin.(1/x))^2) theorem A c= Z & (for x st x in Z holds f.x=1/(x^2*(sin.(1/x))^2)) & Z c= dom (cot*((id Z)^)) & Z = dom f & f|A is continuous implies integral(f,A)=(cot*((id Z)^)).(upper_bound A) - (cot*((id Z)^)).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f.x=1/(x^2*(sin.(1/x))^2)) & Z c= dom (cot*((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:(cot*((id Z)^)) is_differentiable_on Z by A1,FDIFF_8:9; A7:for x being Element of REAL st x in dom ((cot*((id Z)^))`|Z) holds ((cot*((id Z)^))`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((cot*((id Z)^))`|Z);then A8:x in Z by A6,FDIFF_1:def 7;then ((cot*((id Z)^))`|Z).x=1/(x^2*(sin.(1/x))^2) by A1,A4,FDIFF_8:9 .=f.x by A1,A8; hence thesis; end; dom ((cot*((id Z)^))`|Z)=dom f by A1,A6,FDIFF_1:def 7; then ((cot*((id Z)^))`|Z)= f by A7,PARTFUN1:5; hence thesis by A1,A2,A6,INTEGRA5:13; end; ::f.x=1/((1+x^2)*arctan.x) theorem A c= Z & (for x st x in Z holds f1.x=1 & arctan.x>0) & f=((f1+#Z 2)(#)arctan)^ & Z c= ]. -1,1 .[ & Z c= dom (ln*(arctan)) & Z = dom f & f|A is continuous implies integral(f,A)=(ln*(arctan)).(upper_bound A)-(ln* (arctan)).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1 & arctan.x>0) & f=((f1+#Z 2)(#)arctan)^ & Z c= ]. -1,1 .[ & Z c= dom (ln*(arctan)) & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:for x st x in Z holds arctan.x>0 by A1; then A4:ln*(arctan) is_differentiable_on Z by A1,SIN_COS9:89; Z c= dom ((f1+#Z 2)(#)arctan) by A1,RFUNCT_1:1; then Z c= dom (f1+#Z 2) /\ dom arctan by VALUED_1:def 4;then A5:Z c= dom (f1+#Z 2) by XBOOLE_1:18; A6:for x st x in Z holds f.x=1/((1+x^2)*arctan.x) proof let x; assume A7:x in Z; then (((f1+#Z 2)(#)arctan)^).x =1/((f1+#Z 2)(#)arctan).x by A1,RFUNCT_1:def 2 .=1/((f1+#Z 2).x*arctan.x) by VALUED_1:5 .=1/((f1.x+( #Z 2).x)*arctan.x) by A5,A7,VALUED_1:def 1 .=1/((f1.x+(x #Z 2))*arctan.x) by TAYLOR_1:def 1 .=1/((1+(x #Z 2))*arctan.x) by A1,A7 .=1/((1+x^2)*arctan.x) by FDIFF_7:1; hence thesis by A1; end; A8:for x being Element of REAL st x in dom ((ln*(arctan))`|Z) holds ((ln*(arctan))`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((ln*(arctan))`|Z);then A9:x in Z by A4,FDIFF_1:def 7;then ((ln*(arctan))`|Z).x=1/((1+x^2)*arctan.x) by A1,A3,SIN_COS9:89 .=f.x by A6,A9; hence thesis; end; dom ((ln*(arctan))`|Z)=dom f by A1,A4,FDIFF_1:def 7; then ((ln*(arctan))`|Z)= f by A8,PARTFUN1:5; hence thesis by A1,A2,A4,INTEGRA5:13; end; ::f.x=n*(arctan.x) #Z (n-1) / (1+x^2) theorem A c= Z & f=n(#)((( #Z (n-1))*arctan)/(f1+#Z 2)) & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*(arctan)) & Z = dom f & f|A is continuous implies integral(f,A)=(( #Z n)*arctan).(upper_bound A)- (( #Z n)*arctan).(lower_bound A) proof assume A1:A c= Z & f=n(#)((( #Z (n-1))*arctan)/(f1+#Z 2)) & (for x st x in Z holds f1.x=1) & Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*(arctan)) & 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)*(arctan) is_differentiable_on Z by A1,SIN_COS9:91; A4:Z = dom ((( #Z (n-1))*arctan)/(f1+#Z 2)) by A1,VALUED_1:def 5; then Z c= dom (( #Z (n-1))*arctan) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1;then A5:Z c= dom (( #Z (n-1))*arctan) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A6:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A7:Z c= dom (f1+#Z 2) by A6; A8:for x st x in Z holds f.x=n*(arctan.x) #Z (n-1) / (1+x^2) proof let x; assume A9:x in Z; (n(#)((( #Z (n-1))*arctan)/(f1+#Z 2))).x =n*(((( #Z (n-1))*arctan)/(f1+#Z 2)).x) by VALUED_1:6 .=n*((( #Z (n-1))*arctan).x*((f1+#Z 2).x)") by A4,A9,RFUNCT_1:def 1 .=n*(( #Z (n-1))*arctan).x/(f1+#Z 2).x .=n*(( #Z (n-1)).(arctan.x))/(f1+#Z 2).x by A5,A9,FUNCT_1:12 .=n*(arctan.x) #Z (n-1)/(f1+#Z 2).x by TAYLOR_1:def 1 .=n*(arctan.x) #Z (n-1)/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1 .=n*(arctan.x) #Z (n-1)/(1+( #Z 2).x) by A1,A9 .=n*(arctan.x) #Z (n-1)/(1+(x #Z 2)) by TAYLOR_1:def 1 .=n*(arctan.x) #Z (n-1) / (1+x^2) by FDIFF_7:1; hence thesis by A1; end; A10:for x being Element of REAL st x in dom((( #Z n)*(arctan))`|Z) holds ((( #Z n)*(arctan))`|Z).x=f.x proof let x be Element of REAL; assume x in dom((( #Z n)*(arctan))`|Z);then A11:x in Z by A3,FDIFF_1:def 7;then ((( #Z n)*(arctan))`|Z).x=n*(arctan.x) #Z (n-1) / (1+x^2) by A1,SIN_COS9:91 .=f.x by A8,A11; hence thesis; end; dom((( #Z n)*(arctan))`|Z)=dom f by A1,A3,FDIFF_1:def 7; then((( #Z n)*(arctan))`|Z)= f by A10,PARTFUN1:5; hence thesis by A1,A2,INTEGRA5:13,SIN_COS9:91; end; ::f.x=-n*(arccot.x) #Z (n-1) / (1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=-(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))) & Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*arccot) & Z = dom f & f|A is continuous implies integral(f,A)=(( #Z n)*arccot).(upper_bound A)- (( #Z n)*arccot).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=-(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))) & Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*arccot) & 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)*(arccot) is_differentiable_on Z by A1,SIN_COS9:92; Z = dom (n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))) by A1,VALUED_1:8; then A4:Z = dom ((( #Z (n-1))*arccot)/(f1+#Z 2)) by VALUED_1:def 5; then Z c= dom (( #Z (n-1))*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1;then A5:Z c= dom (( #Z (n-1))*arccot) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A6:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A7:Z c= dom (f1+#Z 2) by A6; A8:for x st x in Z holds f.x=-n*(arccot.x) #Z (n-1) / (1+x^2) proof let x; assume A9: x in Z; (-(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2)))).x =-(n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))).x by VALUED_1:8 .=-n*(((( #Z (n-1))*arccot)/(f1+#Z 2))).x by VALUED_1:6 .=-n*((( #Z (n-1))*arccot).x*((f1+#Z 2).x)") by A4,A9,RFUNCT_1:def 1 .=-n*(( #Z (n-1))*arccot).x/(f1+#Z 2).x .=-n*(( #Z (n-1)).(arccot.x))/(f1+#Z 2).x by A5,A9,FUNCT_1:12 .=-n*(arccot.x) #Z (n-1)/(f1+#Z 2).x by TAYLOR_1:def 1 .=-n*(arccot.x) #Z (n-1)/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1 .=-n*(arccot.x) #Z (n-1)/(1+( #Z 2).x) by A1,A9 .=-n*(arccot.x) #Z (n-1)/(1+(x #Z 2)) by TAYLOR_1:def 1 .=-n*(arccot.x) #Z (n-1) / (1+x^2) by FDIFF_7:1; hence thesis by A1; end; A10:for x being Element of REAL st x in dom((( #Z n)*(arccot))`|Z) holds ((( #Z n)*(arccot))`|Z).x=f.x proof let x be Element of REAL; assume x in dom((( #Z n)*(arccot))`|Z);then A11:x in Z by A3,FDIFF_1:def 7;then ((( #Z n)*arccot)`|Z).x=-n*(arccot.x) #Z (n-1) / (1+x^2) by A1,SIN_COS9:92 .=f.x by A11,A8; hence thesis; end; dom((( #Z n)*arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then((( #Z n)*arccot)`|Z)= f by A10,PARTFUN1:5; hence thesis by A1,A2,INTEGRA5:13,SIN_COS9:92; end; theorem Th40: Z c= dom (( #Z n)*arccot) & Z c= ]. -1,1 .[ implies -( #Z n)*arccot is_differentiable_on Z & for x st x in Z holds ((-( #Z n)*arccot)`|Z).x = n*(arccot.x) #Z (n-1) / (1+x^2) proof assume A1:Z c= dom (( #Z n)*arccot) & Z c= ]. -1,1 .[; then A2:Z c= dom (-( #Z n)*arccot) by VALUED_1:8; A3:( #Z n)*(arccot) is_differentiable_on Z by A1,SIN_COS9:92; then A4:(-1)(#)(( #Z n)*(arccot)) is_differentiable_on Z by A2,FDIFF_1:20; for x st x in Z holds ((-( #Z n)*arccot)`|Z).x = n*(arccot.x) #Z (n-1) / (1+x^2) proof let x; assume A5:x in Z;then A6:-1 < x & x < 1 by A1,XXREAL_1:4; arccot is_differentiable_on Z by A1,SIN_COS9:82; then A7:arccot is_differentiable_in x by A5,FDIFF_1:9; A8:( #Z n)*(arccot) is_differentiable_in x by A3,A5,FDIFF_1:9; ((-( #Z n)*arccot)`|Z).x=diff(-( #Z n)*arccot,x) by A4,A5,FDIFF_1:def 7 .=(-1)*(diff(( #Z n)*arccot,x)) by A8,FDIFF_1:15 .=(-1)*((n*((arccot.x) #Z (n-1))) * diff(arccot,x)) by A7,TAYLOR_1:3 .=(-1)*((n*((arccot.x) #Z (n-1))) * (-1/(1+x^2))) by A6,SIN_COS9:76 .=n*(arccot.x) #Z (n-1) / (1+x^2); hence thesis; end; hence thesis by A2,A3,FDIFF_1:20; end; ::f.x=n*(arccot.x) #Z (n-1) / (1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=n(#)((( #Z (n-1))*arccot)/(f1+#Z 2)) & Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*arccot) & Z = dom f & f|A is continuous implies integral(f,A)=(-( #Z n)*arccot).(upper_bound A)- (-( #Z n)*arccot).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=n(#)((( #Z (n-1))*arccot)/(f1+#Z 2)) & Z c= ]. -1,1 .[ & Z c= dom (( #Z n)*arccot) & 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)*(arccot) is_differentiable_on Z by A1,Th40; A4:Z = dom ((( #Z (n-1))*arccot)/(f1+#Z 2)) by A1,VALUED_1:def 5; then Z c= dom (( #Z (n-1))*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1;then A5:Z c= dom (( #Z (n-1))*arccot) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A6:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A7:Z c= dom (f1+#Z 2) by A6; A8:for x st x in Z holds f.x=n*(arccot.x) #Z (n-1) / (1+x^2) proof let x; assume A9:x in Z; (n(#)((( #Z (n-1))*arccot)/(f1+#Z 2))).x =n*(((( #Z (n-1))*arccot)/(f1+#Z 2)).x) by VALUED_1:6 .=n*((( #Z (n-1))*arccot).x*((f1+#Z 2).x)") by A4,A9,RFUNCT_1:def 1 .=n*(( #Z (n-1))*arccot).x/(f1+#Z 2).x .=n*(( #Z (n-1)).(arccot.x))/(f1+#Z 2).x by A5,A9,FUNCT_1:12 .=n*(arccot.x) #Z (n-1)/(f1+#Z 2).x by TAYLOR_1:def 1 .=n*(arccot.x) #Z (n-1)/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1 .=n*(arccot.x) #Z (n-1)/(1+( #Z 2).x) by A1,A9 .=n*(arccot.x) #Z (n-1)/(1+(x #Z 2)) by TAYLOR_1:def 1 .=n*(arccot.x) #Z (n-1) / (1+x^2) by FDIFF_7:1; hence thesis by A1; end; A10:for x being Element of REAL st x in dom((-( #Z n)*(arccot))`|Z) holds ((-( #Z n)*arccot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom((-( #Z n)*(arccot))`|Z);then A11:x in Z by A3,FDIFF_1:def 7;then ((-( #Z n)*arccot)`|Z).x=n*(arccot.x) #Z (n-1) / (1+x^2) by A1,Th40 .=f.x by A11,A8; hence thesis; end; dom((-( #Z n)*arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then((-( #Z n)*arccot)`|Z)= f by A10,PARTFUN1:5; hence thesis by A1,A2,Th40,INTEGRA5:13; end; ::f.x=arctan.x / (1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arctan)) & Z = dom f & f|A is continuous implies integral(f,A)=((1/2)(#)(( #Z 2)*(arctan))).(upper_bound A) -((1/2)(#)(( #Z 2)*(arctan))).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arctan)) & Z = dom f & f|A is continuous;then A2:Z c= dom((1/2)(#)(( #Z 2)*(arctan))) by VALUED_1:def 5; A3:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11; A4:(1/2)(#)(( #Z 2)*arctan) is_differentiable_on Z by A1,A2,SIN_COS9:93; Z c= dom (arctan) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by A1,RFUNCT_1:def 1;then Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A5:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A6:Z c= dom (f1+#Z 2) by A5; A7:for x st x in Z holds f.x=arctan.x / (1+x^2) proof let x; assume A8:x in Z;then (arctan/(f1+#Z 2)).x =arctan.x/(f1+#Z 2).x by A1,RFUNCT_1:def 1 .=arctan.x/(f1.x+(( #Z 2).x)) by A6,A8,VALUED_1:def 1 .=arctan.x/(f1.x+(x #Z 2)) by TAYLOR_1:def 1 .=arctan.x/(1+(x #Z 2)) by A1,A8 .=arctan.x / (1+x^2) by FDIFF_7:1; hence thesis by A1; end; A9:for x being Element of REAL st x in dom(((1/2)(#)(( #Z 2)*(arctan)))`|Z) holds (((1/2)(#)(( #Z 2)*arctan))`|Z).x=f.x proof let x be Element of REAL; assume x in dom(((1/2)(#)(( #Z 2)*arctan))`|Z);then A10:x in Z by A4,FDIFF_1:def 7;then (((1/2)(#)(( #Z 2)*arctan))`|Z).x=arctan.x / (1+x^2) by A1,A2,SIN_COS9:93 .=f.x by A7,A10; hence thesis; end; dom(((1/2)(#)(( #Z 2)*arctan))`|Z)=dom f by A1,A4,FDIFF_1:def 7; then(((1/2)(#)(( #Z 2)*arctan))`|Z)= f by A9,PARTFUN1:5; hence thesis by A1,A2,A3,INTEGRA5:13,SIN_COS9:93; end; ::f.x=-arccot.x / (1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=-arccot/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arccot)) & Z = dom f & f|A is continuous implies integral(f,A)=((1/2)(#)(( #Z 2)*(arccot))).(upper_bound A) -((1/2)(#)(( #Z 2)*(arccot))).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=-arccot/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arccot)) & Z = dom f & f|A is continuous; then A2:Z c= dom((1/2)(#)(( #Z 2)*(arccot))) by VALUED_1:def 5; A3:f is_integrable_on A & f|A is bounded by A1,INTEGRA5:10,11; A4:(1/2)(#)(( #Z 2)*arccot) is_differentiable_on Z by A1,A2,SIN_COS9:94; A5:Z = dom (arccot/(f1+#Z 2)) by A1,VALUED_1:8; then Z c= dom (arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1;then Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A6:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A7:Z c= dom (f1+#Z 2) by A6; A8:for x st x in Z holds f.x=-arccot.x / (1+x^2) proof let x; assume A9:x in Z; (-arccot/(f1+#Z 2)).x =-(arccot/(f1+#Z 2)).x by VALUED_1:8 .=-arccot.x/(f1+#Z 2).x by A5,A9,RFUNCT_1:def 1 .=-arccot.x/(f1.x+(( #Z 2).x)) by A7,A9,VALUED_1:def 1 .=-arccot.x/(f1.x+(x #Z 2)) by TAYLOR_1:def 1 .=-arccot.x/(1+(x #Z 2)) by A1,A9 .=-arccot.x / (1+x^2) by FDIFF_7:1; hence thesis by A1; end; A10:for x being Element of REAL st x in dom(((1/2)(#)(( #Z 2)*arccot))`|Z) holds (((1/2)(#)(( #Z 2)*arccot))`|Z).x=f.x proof let x be Element of REAL; assume x in dom(((1/2)(#)(( #Z 2)*arccot))`|Z);then A11:x in Z by A4,FDIFF_1:def 7;then (((1/2)(#)(( #Z 2)*arccot))`|Z).x=-arccot.x / (1+x^2) by A1,A2,SIN_COS9:94 .=f.x by A8,A11; hence thesis; end; dom(((1/2)(#)(( #Z 2)*(arccot)))`|Z)=dom f by A1,A4,FDIFF_1:def 7; then(((1/2)(#)(( #Z 2)*(arccot)))`|Z)= f by A10,PARTFUN1:5; hence thesis by A1,A2,A3,INTEGRA5:13,SIN_COS9:94; end; theorem Th44: Z c= dom (( #Z 2)*(arccot)) & Z c= ]. -1,1 .[ implies -(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_on Z & for x st x in Z holds ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x = arccot.x / (1+x^2) proof assume A1:Z c= dom (( #Z 2)*(arccot)) & Z c= ]. -1,1 .[; then A2:Z c= dom((1/2)(#)(( #Z 2)*(arccot))) by VALUED_1:def 5; then A3:Z c= dom (-(1/2)(#)(( #Z 2)*(arccot))) by VALUED_1:8; A4:(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_on Z by A2,A1,SIN_COS9:94; then A5:(-1)(#)((1/2)(#)(( #Z 2)*(arccot))) is_differentiable_on Z by A3,FDIFF_1:20; A6:( #Z 2)*(arccot) is_differentiable_on Z & for x st x in Z holds ((( #Z 2)*(arccot))`|Z).x = -2*(arccot.x) #Z (2-1) / (1+x^2) by A1,SIN_COS9:92; for x st x in Z holds ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x = arccot.x / (1+x^2) proof let x; assume A7: x in Z;then A8:(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_in x by A4,FDIFF_1:9; A9:( #Z 2)*(arccot) is_differentiable_in x by A6,A7,FDIFF_1:9; ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=diff(-(1/2)(#)(( #Z 2)*(arccot)),x) by A5,A7,FDIFF_1:def 7 .=(-1)*(diff((1/2)(#)(( #Z 2)*(arccot)),x)) by A8,FDIFF_1:15 .=(-1)*((1/2)*diff(( #Z 2)*(arccot),x)) by A9,FDIFF_1:15 .=(-1)*((1/2)*((( #Z 2)*(arccot))`|Z).x) by A6,A7,FDIFF_1:def 7 .=(-1)*((1/2)*(-2*(arccot.x) #Z (2-1) / (1+x^2))) by A1,A7,SIN_COS9:92 .=(-1)*(-(1/2)*(2*(arccot.x) #Z 1 / (1+x^2))) .=(-1)*(-(1/2)*(2*arccot.x / (1+x^2))) by PREPOWER:35 .=arccot.x / (1+x^2); hence thesis; end; hence thesis by A3,A4,FDIFF_1:20; end; ::f.x=arccot.x / (1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arccot)) & Z = dom f & f|A is continuous implies integral(f,A)=(-(1/2)(#)(( #Z 2)*(arccot))).(upper_bound A) -(-(1/2)(#)(( #Z 2)*(arccot))).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z c= dom (( #Z 2)*(arccot)) & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:-(1/2)(#)(( #Z 2)*(arccot)) is_differentiable_on Z by A1,Th44; Z c= dom (arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by A1,RFUNCT_1:def 1;then Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A4:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A5:Z c= dom (f1+#Z 2) by A4; A6:for x st x in Z holds f.x=arccot.x / (1+x^2) proof let x; assume A7:x in Z;then (arccot/(f1+#Z 2)).x =arccot.x/(f1+#Z 2).x by A1,RFUNCT_1:def 1 .=arccot.x/(f1.x+(( #Z 2).x)) by A5,A7,VALUED_1:def 1 .=arccot.x/(f1.x+(x #Z 2)) by TAYLOR_1:def 1 .=arccot.x/(1+(x #Z 2)) by A1,A7 .=arccot.x / (1+x^2) by FDIFF_7:1; hence thesis by A1; end; A8:for x being Element of REAL st x in dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z) holds ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=f.x proof let x be Element of REAL; assume x in dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z);then A9:x in Z by A3,FDIFF_1:def 7;then ((-(1/2)(#)(( #Z 2)*(arccot)))`|Z).x=arccot.x / (1+x^2) by A1,Th44 .=f.x by A6,A9; hence thesis; end; dom((-(1/2)(#)(( #Z 2)*(arccot)))`|Z)=dom f by A1,A3,FDIFF_1:def 7; then((-(1/2)(#)(( #Z 2)*(arccot)))`|Z)= f by A8,PARTFUN1:5; hence thesis by A1,A2,Th44,INTEGRA5:13; end; ::f.x=arctan.x + x/(1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=arctan+(id Z)/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies integral(f,A)=((id Z)(#)(arctan)).(upper_bound A)- ((id Z)(#)(arctan)).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arctan+(id Z)/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; Z = dom arctan /\ dom ((id Z)/(f1+#Z 2)) by A1,VALUED_1:def 1; then A3:Z c= dom arctan & Z c= dom ((id Z)/(f1+#Z 2)) by XBOOLE_1:18; then Z c= dom (id Z) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1; then A4: Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; A5:(id Z)(#)(arctan) is_differentiable_on Z by A1,SIN_COS9:95; A6:Z c= dom ((f1+#Z 2)^) by A4,RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A7:Z c= dom (f1+#Z 2) by A6; A8:for x st x in Z holds f.x=arctan.x + x/(1+x^2) proof let x; assume A9: x in Z; then (arctan+(id Z)/(f1+#Z 2)).x =arctan.x+((id Z)/(f1+#Z 2)).x by A1,VALUED_1:def 1 .=arctan.x+(id Z).x/(f1+#Z 2).x by A3,A9,RFUNCT_1:def 1 .=arctan.x+x/(f1+#Z 2).x by A9,FUNCT_1:18 .=arctan.x+x/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1 .=arctan.x+x/(1+( #Z 2).x) by A1,A9 .=arctan.x+x/(1+(x #Z 2)) by TAYLOR_1:def 1 .=arctan.x + x/(1+x^2) by FDIFF_7:1; hence thesis by A1; end; A10:for x being Element of REAL st x in dom(((id Z)(#)(arctan))`|Z) holds (((id Z)(#)(arctan))`|Z).x=f.x proof let x be Element of REAL; assume x in dom(((id Z)(#)(arctan))`|Z);then A11:x in Z by A5,FDIFF_1:def 7;then (((id Z)(#)(arctan))`|Z).x=arctan.x + x/(1+x^2) by A1,SIN_COS9:95 .=f.x by A8,A11; hence thesis; end; dom(((id Z)(#)(arctan))`|Z)=dom f by A1,A5,FDIFF_1:def 7; then(((id Z)(#)(arctan))`|Z)= f by A10,PARTFUN1:5; hence thesis by A1,A2,INTEGRA5:13,SIN_COS9:95; end; ::f.x=arccot.x - x/(1+x^2) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=arccot-(id Z)/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies integral(f,A)=((id Z)(#)(arccot)).(upper_bound A)- ((id Z)(#)(arccot)).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arccot-(id Z)/(f1+#Z 2) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous;then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; Z = dom arccot /\ dom ((id Z)/(f1+#Z 2)) by A1,VALUED_1:12; then A3:Z c= dom arccot & Z c= dom ((id Z)/(f1+#Z 2)) by XBOOLE_1:18; then Z c= dom (id Z) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1; then A4:Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; A5:(id Z)(#)(arccot) is_differentiable_on Z by A1,SIN_COS9:96; A6:Z c= dom ((f1+#Z 2)^) by A4,RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A7:Z c= dom (f1+#Z 2) by A6; A8:for x st x in Z holds f.x=arccot.x - x/(1+x^2) proof let x; assume A9: x in Z; then (arccot-(id Z)/(f1+#Z 2)).x =arccot.x-((id Z)/(f1+#Z 2)).x by A1,VALUED_1:13 .=arccot.x-(id Z).x/(f1+#Z 2).x by A3,A9,RFUNCT_1:def 1 .=arccot.x-x/(f1+#Z 2).x by A9,FUNCT_1:18 .=arccot.x-x/(f1.x+( #Z 2).x) by A7,A9,VALUED_1:def 1 .=arccot.x-x/(1+( #Z 2).x) by A1,A9 .=arccot.x-x/(1+(x #Z 2)) by TAYLOR_1:def 1 .=arccot.x-x/(1+x^2) by FDIFF_7:1; hence thesis by A1; end; A10:for x being Element of REAL st x in dom(((id Z)(#)(arccot))`|Z) holds (((id Z)(#)(arccot))`|Z).x=f.x proof let x be Element of REAL; assume x in dom(((id Z)(#)(arccot))`|Z);then A11:x in Z by A5,FDIFF_1:def 7;then (((id Z)(#)(arccot))`|Z).x=arccot.x - x/(1+x^2) by A1,SIN_COS9:96 .=f.x by A11,A8; hence thesis; end; dom(((id Z)(#)(arccot))`|Z)=dom f by A1,A5,FDIFF_1:def 7; then(((id Z)(#)(arccot))`|Z)= f by A10,PARTFUN1:5; hence thesis by A1,A2,INTEGRA5:13,SIN_COS9:96; end; ::f.x=exp_R.(arctan.x)/(1+x^2) theorem A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arctan/(f1+#Z 2) & (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous implies integral(f,A)=(exp_R*arctan).(upper_bound A) - (exp_R*arctan).(lower_bound A) proof assume A1:A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arctan/(f1+#Z 2) & (for x st x in Z holds f1.x=1) & 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*arctan) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by A1,RFUNCT_1:def 1;then A3:Z c= dom (exp_R*arctan) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A4:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A5:Z c= dom (f1+#Z 2) by A4; A6:exp_R*arctan is_differentiable_on Z by A1,A3,SIN_COS9:119; A7:for x st x in Z holds f.x=exp_R.(arctan.x)/(1+x^2) proof let x; assume A8:x in Z; then (exp_R*arctan/(f1+#Z 2)).x =(exp_R*arctan).x/(f1+#Z 2).x by A1,RFUNCT_1:def 1 .=exp_R.(arctan.x)/(f1+#Z 2).x by A3,A8,FUNCT_1:12 .=exp_R.(arctan.x)/(f1.x+( #Z 2).x) by A5,A8,VALUED_1:def 1 .=exp_R.(arctan.x)/(1+( #Z 2).x) by A1,A8 .=exp_R.(arctan.x)/(1+(x #Z 2)) by TAYLOR_1:def 1 .=exp_R.(arctan.x)/(1+x^2) by FDIFF_7:1; hence thesis by A1; end; A9:for x being Element of REAL st x in dom ((exp_R*arctan)`|Z) holds ((exp_R*arctan)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((exp_R*arctan)`|Z);then A10: x in Z by A6,FDIFF_1:def 7;then ((exp_R*arctan)`|Z).x=exp_R.(arctan.x)/(1+x^2) by A1,A3,SIN_COS9:119 .=f.x by A10,A7; hence thesis; end; dom ((exp_R*arctan)`|Z)=dom f by A1,A6,FDIFF_1:def 7; then ((exp_R*arctan)`|Z)= f by A9,PARTFUN1:5; hence thesis by A1,A2,A3,INTEGRA5:13,SIN_COS9:119; end; ::f.x=-exp_R.(arccot.x)/(1+x^2) theorem A c= Z & Z c= ]. -1,1 .[ & f=-exp_R*arccot/(f1+#Z 2) & (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous implies integral(f,A)=(exp_R*arccot).(upper_bound A) - (exp_R*arccot).(lower_bound A) proof assume A1:A c= Z & Z c= ]. -1,1 .[ & f=-exp_R*arccot/(f1+#Z 2) & (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous; then A2:f is_integrable_on A & f|A is bounded by INTEGRA5:10,11; A3:Z = dom (exp_R*arccot/(f1+#Z 2)) by A1,VALUED_1:8; then Z = dom (exp_R*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by RFUNCT_1:def 1;then A4:Z c= dom (exp_R*arccot) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A5:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A6:Z c= dom (f1+#Z 2) by A5; A7:exp_R*arccot is_differentiable_on Z by A1,A4,SIN_COS9:120; A8:for x st x in Z holds f.x=-exp_R.(arccot.x)/(1+x^2) proof let x; assume A9:x in Z; (-exp_R*arccot/(f1+#Z 2)).x =-(exp_R*arccot/(f1+#Z 2)).x by VALUED_1:8 .=-(exp_R*arccot).x/(f1+#Z 2).x by A9,A3,RFUNCT_1:def 1 .=-exp_R.(arccot.x)/(f1+#Z 2).x by A4,A9,FUNCT_1:12 .=-exp_R.(arccot.x)/(f1.x+( #Z 2).x) by A6,A9,VALUED_1:def 1 .=-exp_R.(arccot.x)/(1+( #Z 2).x) by A1,A9 .=-exp_R.(arccot.x)/(1+(x #Z 2)) by TAYLOR_1:def 1 .=-exp_R.(arccot.x)/(1+x^2) by FDIFF_7:1; hence thesis by A1; end; A10:for x being Element of REAL st x in dom ((exp_R*arccot)`|Z) holds ((exp_R*arccot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((exp_R*arccot)`|Z);then A11: x in Z by A7,FDIFF_1:def 7;then ((exp_R*arccot)`|Z).x=-exp_R.(arccot.x)/(1+x^2) by A1,A4,SIN_COS9:120 .=f.x by A11,A8; hence thesis; end; dom ((exp_R*arccot)`|Z)=dom f by A1,A7,FDIFF_1:def 7; then ((exp_R*arccot)`|Z)= f by A10,PARTFUN1:5; hence thesis by A1,A2,A4,INTEGRA5:13,SIN_COS9:120; end; theorem Th50: Z c= dom (exp_R*arccot) & Z c= ]. -1,1 .[ implies -exp_R*arccot is_differentiable_on Z & for x st x in Z holds ((-exp_R*arccot)`|Z).x = exp_R.(arccot.x)/(1+x^2) proof assume A1:Z c= dom (exp_R*arccot) & Z c= ]. -1,1 .[; then A2:Z c= dom (-exp_R*arccot) by VALUED_1:8; A3:exp_R*arccot is_differentiable_on Z by A1,SIN_COS9:120; then A4:(-1)(#)(exp_R*arccot) is_differentiable_on Z by A2,FDIFF_1:20; for x st x in Z holds ((-exp_R*arccot)`|Z).x = exp_R.(arccot.x)/(1+x^2) proof let x; assume A5:x in Z; A6:arccot is_differentiable_on Z by A1,SIN_COS9:82;then A7:arccot is_differentiable_in x by A5,FDIFF_1:9; A8:exp_R is_differentiable_in arccot.x by SIN_COS:65; A9:exp_R*arccot is_differentiable_in x by A3,A5,FDIFF_1:9; ((-exp_R*arccot)`|Z).x=diff(-exp_R*arccot,x) by A4,A5,FDIFF_1:def 7 .=(-1)*(diff(exp_R*arccot,x)) by A9,FDIFF_1:15 .=(-1)*(diff(exp_R,arccot.x)*diff(arccot,x)) by A7,A8,FDIFF_2:13 .=(-1)*(diff(exp_R,arccot.x)*((arccot)`|Z).x) by A5,A6,FDIFF_1:def 7 .=(-1)*(diff(exp_R,arccot.x)*(-1/(1+x^2))) by A5,A1,SIN_COS9:82 .=(-1)*(-diff(exp_R,arccot.x)*(1/(1+x^2))) .=exp_R.(arccot.x)/(1+x^2) by SIN_COS:65; hence thesis; end; hence thesis by A2,A3,FDIFF_1:20; end; ::f.x=exp_R.(arccot.x)/(1+x^2) theorem A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arccot/(f1+#Z 2) & (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous implies integral(f,A)=(-exp_R*arccot).(upper_bound A) -(-exp_R*arccot).(lower_bound A) proof assume A1:A c= Z & Z c= ]. -1,1 .[ & f=exp_R*arccot/(f1+#Z 2) & (for x st x in Z holds f1.x=1) & 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*arccot) /\ (dom (f1+#Z 2) \ (f1+#Z 2)"{0}) by A1,RFUNCT_1:def 1;then A3:Z c= dom (exp_R*arccot) & Z c= dom (f1+#Z 2) \ (f1+#Z 2)"{0} by XBOOLE_1:18; then A4:Z c= dom ((f1+#Z 2)^) by RFUNCT_1:def 2; dom ((f1+#Z 2)^) c= dom (f1+#Z 2) by RFUNCT_1:1;then A5:Z c= dom (f1+#Z 2) by A4; A6:-exp_R*arccot is_differentiable_on Z by A1,A3,Th50; A7:for x st x in Z holds f.x=exp_R.(arccot.x)/(1+x^2) proof let x; assume A8:x in Z; then (exp_R*arccot/(f1+#Z 2)).x =(exp_R*arccot).x/(f1+#Z 2).x by A1,RFUNCT_1:def 1 .=exp_R.(arccot.x)/(f1+#Z 2).x by A3,A8,FUNCT_1:12 .=exp_R.(arccot.x)/(f1.x+( #Z 2).x) by A5,A8,VALUED_1:def 1 .=exp_R.(arccot.x)/(1+( #Z 2).x) by A1,A8 .=exp_R.(arccot.x)/(1+(x #Z 2)) by TAYLOR_1:def 1 .=exp_R.(arccot.x)/(1+x^2) by FDIFF_7:1; hence thesis by A1; end; A9:for x being Element of REAL st x in dom ((-exp_R*arccot)`|Z) holds ((-exp_R*arccot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom ((-exp_R*arccot)`|Z);then A10: x in Z by A6,FDIFF_1:def 7;then ((-exp_R*arccot)`|Z).x=exp_R.(arccot.x)/(1+x^2) by A1,A3,Th50 .=f.x by A7,A10; hence thesis; end; dom ((-exp_R*arccot)`|Z)=dom f by A1,A6,FDIFF_1:def 7; then ((-exp_R*arccot)`|Z)= f by A9,PARTFUN1:5; hence thesis by A1,A2,A3,Th50,INTEGRA5:13; end; ::f.x=x/(1+x^2) theorem A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(f1+f2) & f2=#Z 2 & (for x st x in Z holds f1.x=1) & Z = dom f & f|A is continuous implies integral(f,A)=((1/2)(#)(ln*(f1+f2))).(upper_bound A) -((1/2)(#)(ln*(f1+f2))).(lower_bound A) proof assume A1:A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(f1+f2) & f2=#Z 2 & (for x st x in Z holds f1.x=1) & 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 ((1/2)(#)(ln*(f1+f2))) by A1,VALUED_1:def 5; Z c= dom (id Z) /\ (dom (f1+f2) \ (f1+f2)"{0}) by A1,RFUNCT_1:def 1; then Z c= dom (f1+f2) \ (f1+f2)"{0} by XBOOLE_1:18;then A4:Z c= dom ((f1+f2)^) by RFUNCT_1:def 2; dom ((f1+f2)^) c= dom (f1+f2) by RFUNCT_1:1;then A5:Z c= dom (f1+f2) by A4; A6:(1/2)(#)(ln*(f1+f2)) is_differentiable_on Z by A1,A3,SIN_COS9:102; A7: for x st x in Z holds f.x=x/(1+x^2) proof let x; assume A8: x in Z; then ((id Z)/(f1+f2)).x=(id Z).x/(f1+f2).x by A1,RFUNCT_1:def 1 .=x/(f1+f2).x by A8,FUNCT_1:18 .=x/(f1.x+f2.x) by A5,A8,VALUED_1:def 1 .=x/(1+( #Z 2).x) by A1,A8 .=x/(1+(x #Z 2)) by TAYLOR_1:def 1 .=x/(1+x^2) by FDIFF_7:1; hence thesis by A1; end; A9:for x being Element of REAL st x in dom(((1/2)(#)(ln*(f1+f2)))`|Z) holds (((1/2)(#)(ln*(f1+f2)))`|Z).x=f.x proof let x be Element of REAL; assume x in dom(((1/2)(#)(ln*(f1+f2)))`|Z);then A10: x in Z by A6,FDIFF_1:def 7;then (((1/2)(#)(ln*(f1+f2)))`|Z).x=x/(1+x^2) by A1,A3,SIN_COS9:102 .=f.x by A10,A7; hence thesis; end; dom(((1/2)(#)(ln*(f1+f2)))`|Z)=dom f by A1,A6,FDIFF_1:def 7; then(((1/2)(#)(ln*(f1+f2)))`|Z)= f by A9,PARTFUN1:5; hence thesis by A1,A2,A6,INTEGRA5:13; end; ::f.x=x/(a*(1+(x/a)^2)) theorem A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(a(#)(f1+f2)) & (for x st x in Z holds h.x=x/a & f1.x=1) & a <> 0 & f2=( #Z 2)*h & Z = dom f & f|A is continuous implies integral(f,A)=((a/2)(#)(ln*(f1+f2))).(upper_bound A) -((a/2)(#)(ln*(f1+f2))).(lower_bound A) proof assume A1:A c= Z & Z c= dom (ln*(f1+f2)) & f=(id Z)/(a(#)(f1+f2)) & (for x st x in Z holds h.x=x/a & f1.x=1) & a <> 0 & f2=( #Z 2)*h & 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 ((a/2)(#)(ln*(f1+f2))) by A1,VALUED_1:def 5; A4:for x st x in Z holds f1.x=1 by A1; A5:for x st x in Z holds h.x=x/a by A1; then A6:((a/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A1,A3,A4,SIN_COS9:108; A7:for x st x in Z holds f.x=x/(a*(1+(x/a)^2)) proof let x; assume A8:x in Z; then A9:x in dom (f1+f2) by A1,FUNCT_1:11; dom (f1+f2) = dom f1 /\ dom f2 by VALUED_1:def 1;then dom (f1+f2) c= dom f2 by XBOOLE_1:18;then A10:x in dom f2 by A9; ((id Z)/(a(#)(f1+f2))).x=(id Z).x/(a(#)(f1+f2)).x by A1,A8,RFUNCT_1:def 1 .=x/(a(#)(f1+f2)).x by A8,FUNCT_1:18 .=x/(a*(f1+f2).x) by VALUED_1:6 .=x/(a*(f1.x+f2.x)) by A9,VALUED_1:def 1 .=x/(a*(1+f2.x)) by A4,A8 .=x/(a*(1+( #Z 2).(h.x))) by A1,A10,FUNCT_1:12 .=x/(a*(1+((h.x) #Z 2))) by TAYLOR_1:def 1 .=x/(a*(1+(h.x)^2)) by FDIFF_7:1 .=x/(a*(1+(x/a)^2)) by A5,A8; hence thesis by A1; end; A11:for x being Element of REAL st x in dom(((a/2)(#)(ln*(f1+f2)))`|Z) holds (((a/2)(#)(ln*(f1+f2)))`|Z).x=f.x proof let x be Element of REAL; assume x in dom(((a/2)(#)(ln*(f1+f2)))`|Z);then A12: x in Z by A6,FDIFF_1:def 7;then (((a/2)(#)(ln*(f1+f2)))`|Z).x =x/(a*(1+(x/a)^2)) by A1,A3,A4,A5,SIN_COS9:108 .=f.x by A7,A12; hence thesis; end; dom(((a/2)(#)(ln*(f1+f2)))`|Z) = dom f by A1,A6,FDIFF_1:def 7; then (((a/2)(#)(ln*(f1+f2)))`|Z) = f by A11,PARTFUN1:5; hence thesis by A1,A2,A6,INTEGRA5:13; end; theorem Th54: Z c= dom ((id Z)^(#)arctan) & Z c= ]. -1,1 .[ implies (-(id Z)^(#)arctan) is_differentiable_on Z & for x st x in Z holds ((-(id Z)^(#)arctan)`|Z).x = arctan.x/(x^2)-1/(x*(1+x^2)) proof set f = id Z; assume that A1:Z c= dom (f^(#)arctan) and A2: Z c= ]. -1,1 .[; A3:Z c= dom (-f^(#)arctan) by A1,VALUED_1:8; A4:for x st x in Z holds f.x=x by FUNCT_1:18; Z c= dom (f^) /\ dom arctan by A1,VALUED_1:def 4;then A5: Z c= dom (f^) by XBOOLE_1:18; A6:not 0 in Z proof assume A7: 0 in Z; dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2 .= dom id Z \ {0} by Lm1,A7; then not 0 in {0} by A7,A5,XBOOLE_0:def 5; hence thesis by TARSKI:def 1; end; then A8:f^ is_differentiable_on Z & for x st x in Z holds ((f^)`|Z).x = -1/x^2 by FDIFF_5:4; A9:arctan is_differentiable_on Z by A2,SIN_COS9:81; A10:(f^(#)arctan) is_differentiable_on Z by A1,A2,A6,SIN_COS9:129; then A11:(-1)(#)(f^(#)arctan) is_differentiable_on Z by A3,FDIFF_1:20; for x st x in Z holds ((-f^(#)arctan)`|Z).x = arctan.x/(x^2)-1/(x*(1+x^2)) proof let x; assume A12: x in Z; then A13:(f^(#)arctan) is_differentiable_in x by A10,FDIFF_1:9; A14:f^ is_differentiable_in x by A8,A12,FDIFF_1:9; A15:arctan is_differentiable_in x by A9,A12,FDIFF_1:9; ((-f^(#)arctan)`|Z).x=diff(-f^(#)arctan,x) by A11,A12,FDIFF_1:def 7 .=(-1)*(diff(f^(#)arctan,x)) by A13,FDIFF_1:15 .=(-1)*((arctan.x)*diff(f^,x)+((f^).x)*diff(arctan,x)) by A14,A15,FDIFF_1:16 .=(-1)*((arctan.x)*((f^)`|Z).x+((f^).x)*diff(arctan,x)) by A8,A12,FDIFF_1:def 7 .=(-1)*((arctan.x)*(-1/x^2)+((f^).x)*diff(arctan,x)) by A6,A12,FDIFF_5:4 .=(-1)*(-(arctan.x)*(1/x^2)+((f^).x)*((arctan)`|Z).x) by A9,A12,FDIFF_1:def 7 .=(-1)*(-((arctan.x)*1)/(x^2)+((f^).x)*(1/(1+x^2))) by A2,A12,SIN_COS9:81 .=(-1)*(-arctan.x/(x^2)+(f.x)"*(1/(1+x^2))) by A5,A12,RFUNCT_1:def 2 .=(-1)*(-arctan.x/(x^2)+(1/x)*(1/(1+x^2))) by A4,A12 .=(-1)*(-arctan.x/(x^2)+(1*1)/(x*(1+x^2))) by XCMPLX_1:76 .=arctan.x/(x^2)-1/(x*(1+x^2)); hence thesis; end; hence thesis by A3,A10,FDIFF_1:20; end; theorem Th55: Z c= dom ((id Z)^(#)arccot) & Z c= ]. -1,1 .[ implies (-(id Z)^(#)arccot) is_differentiable_on Z & for x st x in Z holds ((-(id Z)^(#)arccot)`|Z).x = arccot.x/(x^2)+1/(x*(1+x^2)) proof set f = id Z; assume that A1:Z c= dom (f^(#)arccot) and A2: Z c= ]. -1,1 .[; A3:Z c= dom (-f^(#)arccot) by A1,VALUED_1:8; A4:for x st x in Z holds f.x=x by FUNCT_1:18; Z c= dom (f^) /\ dom arccot by A1,VALUED_1:def 4;then A5:Z c= dom (f^) by XBOOLE_1:18; A6:not 0 in Z proof assume A7: 0 in Z; dom ((id Z)^) = dom id Z \ (id Z)"{0} by RFUNCT_1:def 2 .= dom id Z \ {0} by Lm1,A7; then not 0 in {0} by A7,A5,XBOOLE_0:def 5; hence thesis by TARSKI:def 1; end; then A8:f^ is_differentiable_on Z & for x st x in Z holds ((f^)`|Z).x = -1/x^2 by FDIFF_5:4; A9:arccot is_differentiable_on Z by A2,SIN_COS9:82; A10:(f^(#)arccot) is_differentiable_on Z by A6,A1,A2,SIN_COS9:130; then A11:(-1)(#)(f^(#)arccot) is_differentiable_on Z by A3,FDIFF_1:20; for x st x in Z holds ((-f^(#)arccot)`|Z).x = arccot.x/(x^2)+1/(x*(1+x^2)) proof let x; assume A12: x in Z; then A13: (f^(#)arccot) is_differentiable_in x by A10,FDIFF_1:9; A14: f^ is_differentiable_in x by A8,A12,FDIFF_1:9; A15: arccot is_differentiable_in x by A9,A12,FDIFF_1:9; ((-f^(#)arccot)`|Z).x=diff(-f^(#)arccot,x) by A11,A12,FDIFF_1:def 7 .=(-1)*(diff(f^(#)arccot,x)) by A13,FDIFF_1:15 .=(-1)*((arccot.x)*diff(f^,x)+((f^).x)*diff(arccot,x)) by A14,A15,FDIFF_1:16 .=(-1)*((arccot.x)*((f^)`|Z).x+((f^).x)*diff(arccot,x)) by A8,A12,FDIFF_1:def 7 .=(-1)*((arccot.x)*(-1/x^2)+((f^).x)*diff(arccot,x)) by A12,A6,FDIFF_5:4 .=(-1)*(-(arccot.x)*(1/x^2)+((f^).x)*((arccot)`|Z).x) by A9,A12,FDIFF_1:def 7 .=(-1)*(-(arccot.x)*(1/x^2)+((f^).x)*(-1/(1+x^2))) by A2,A12,SIN_COS9:82 .=(-1)*(-((arccot.x)*1)/(x^2)-((f^).x)*(1/(1+x^2))) .=(-1)*(-arccot.x/(x^2)-(f.x)"*(1/(1+x^2))) by A5,A12,RFUNCT_1:def 2 .=(-1)*(-arccot.x/(x^2)-(1/x)*(1/(1+x^2))) by A4,A12 .=(-1)*(-arccot.x/(x^2)-(1*1)/(x*(1+x^2))) by XCMPLX_1:76 .=arccot.x/(x^2)+1/(x*(1+x^2)); hence thesis; end; hence thesis by A11; end; ::f.x=arctan.x/(x^2)-1/(x*(1+x^2)) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/( #Z 2)-((id Z)(#)(f1+#Z 2))^ & Z c= dom ((id Z)^(#)arctan) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies integral(f,A)=(-(id Z)^(#)arctan).(upper_bound A)- (-(id Z)^(#)arctan).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arctan/( #Z 2)-((id Z)(#)(f1+#Z 2))^ & Z c= dom ((id Z)^(#)arctan) & Z c= ]. -1,1 .[ & 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)^(#)arctan) is_differentiable_on Z by A1,Th54; A4:Z=dom (arctan/( #Z 2)) /\ dom (((id Z)(#)(f1+#Z 2))^) by A1,VALUED_1:12;then A5:Z c= dom (arctan/( #Z 2)) by XBOOLE_1:18; A6:Z c= dom (((id Z)(#)(f1+#Z 2))^) by A4,XBOOLE_1:18; dom (((id Z)(#)(f1+#Z 2))^) c= dom ((id Z)(#)(f1+#Z 2)) by RFUNCT_1:1;then Z c= dom ((id Z)(#)(f1+#Z 2)) by A6; then Z c= dom (id Z) /\ dom (f1+#Z 2) by VALUED_1:def 4;then A7:Z c= dom (f1+#Z 2) by XBOOLE_1:18; A8:for x st x in Z holds f.x=arctan.x/(x^2)-1/(x*(1+x^2)) proof let x; assume A9:x in Z;then A10:x in dom (((id Z)(#)(f1+#Z 2))^) by A6; (arctan/( #Z 2)-((id Z)(#)(f1+#Z 2))^).x =(arctan/( #Z 2)).x-(((id Z)(#)(f1+#Z 2))^).x by A1,A9,VALUED_1:13 .=(arctan/( #Z 2)).x-1/(((id Z)(#)(f1+#Z 2)).x) by A10,RFUNCT_1:def 2 .=(arctan/( #Z 2)).x-1/((id Z).x*(f1+#Z 2).x) by VALUED_1:5 .=(arctan/( #Z 2)).x-1/((id Z).x*(f1.x+( #Z 2).x)) by A7,A9,VALUED_1:def 1 .=(arctan/( #Z 2)).x-1/(x*(f1.x+( #Z 2).x)) by A9,FUNCT_1:18 .=(arctan/( #Z 2)).x-1/(x*(1+( #Z 2).x)) by A1,A9 .=arctan.x/( #Z 2).x-1/(x*(1+( #Z 2).x)) by A9,A5,RFUNCT_1:def 1 .=arctan.x/(x #Z 2)-1/(x*(1+( #Z 2).x)) by TAYLOR_1:def 1 .=arctan.x/(x #Z 2)-1/(x*(1+( x #Z 2))) by TAYLOR_1:def 1 .=arctan.x/(x^2)-1/(x*(1+( x #Z 2))) by FDIFF_7:1 .=arctan.x/(x^2)-1/(x*(1+x^2)) by FDIFF_7:1; hence thesis by A1; end; A11:for x being Element of REAL st x in dom((-(id Z)^(#)arctan)`|Z) holds ((-(id Z)^(#)arctan)`|Z).x=f.x proof let x be Element of REAL; assume x in dom((-(id Z)^(#)arctan)`|Z);then A12: x in Z by A3,FDIFF_1:def 7;then ((-(id Z)^(#)arctan)`|Z).x=arctan.x/(x^2)-1/(x*(1+x^2)) by A1,Th54 .=f.x by A8,A12; hence thesis; end; dom((-(id Z)^(#)arctan)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then((-(id Z)^(#)arctan)`|Z)= f by A11,PARTFUN1:5; hence thesis by A1,A2,A3,INTEGRA5:13; end; ::f.x=arccot.x/(x^2)+1/(x*(1+x^2)) theorem A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/( #Z 2)+((id Z)(#)(f1+#Z 2))^ & Z c= dom ((id Z)^(#)arccot) & Z c= ]. -1,1 .[ & Z = dom f & f|A is continuous implies integral(f,A)=(-(id Z)^(#)arccot).(upper_bound A)- (-(id Z)^(#)arccot).(lower_bound A) proof assume A1:A c= Z & (for x st x in Z holds f1.x=1) & f=arccot/( #Z 2)+((id Z)(#)(f1+#Z 2))^ & Z c= dom ((id Z)^(#)arccot) & Z c= ]. -1,1 .[ & 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)^(#)arccot) is_differentiable_on Z by A1,Th55; A4:Z=dom (arccot/( #Z 2)) /\ dom (((id Z)(#)(f1+#Z 2))^) by A1,VALUED_1:def 1; then A5:Z c= dom (arccot/( #Z 2)) by XBOOLE_1:18; A6:Z c= dom (((id Z)(#)(f1+#Z 2))^) by A4,XBOOLE_1:18; dom (((id Z)(#)(f1+#Z 2))^) c= dom ((id Z)(#)(f1+#Z 2)) by RFUNCT_1:1;then Z c= dom ((id Z)(#)(f1+#Z 2)) by A6; then Z c= dom (id Z) /\ dom (f1+#Z 2) by VALUED_1:def 4;then A7:Z c= dom (f1+#Z 2) by XBOOLE_1:18; A8:for x st x in Z holds f.x=arccot.x/(x^2)+1/(x*(1+x^2)) proof let x; assume A9:x in Z;then A10:x in dom (((id Z)(#)(f1+#Z 2))^) by A6; (arccot/( #Z 2)+((id Z)(#)(f1+#Z 2))^).x =(arccot/( #Z 2)).x+(((id Z)(#)(f1+#Z 2))^).x by A1,A9,VALUED_1:def 1 .=(arccot/( #Z 2)).x+1/(((id Z)(#)(f1+#Z 2)).x) by A10,RFUNCT_1:def 2 .=(arccot/( #Z 2)).x+1/((id Z).x*(f1+#Z 2).x) by VALUED_1:5 .=(arccot/( #Z 2)).x+1/((id Z).x*(f1.x+( #Z 2).x)) by A7,A9,VALUED_1:def 1 .=(arccot/( #Z 2)).x+1/(x*(f1.x+( #Z 2).x)) by A9,FUNCT_1:18 .=(arccot/( #Z 2)).x+1/(x*(1+( #Z 2).x)) by A1,A9 .=arccot.x/( #Z 2).x+1/(x*(1+( #Z 2).x)) by A9,A5,RFUNCT_1:def 1 .=arccot.x/(x #Z 2)+1/(x*(1+( #Z 2).x)) by TAYLOR_1:def 1 .=arccot.x/(x #Z 2)+1/(x*(1+( x #Z 2))) by TAYLOR_1:def 1 .=arccot.x/(x^2)+1/(x*(1+( x #Z 2))) by FDIFF_7:1 .=arccot.x/(x^2)+1/(x*(1+x^2)) by FDIFF_7:1; hence thesis by A1; end; A11:for x being Element of REAL st x in dom((-(id Z)^(#)arccot)`|Z) holds ((-(id Z)^(#)arccot)`|Z).x=f.x proof let x be Element of REAL; assume x in dom((-(id Z)^(#)arccot)`|Z);then A12:x in Z by A3,FDIFF_1:def 7;then ((-(id Z)^(#)arccot)`|Z).x=arccot.x/(x^2)+1/(x*(1+x^2)) by A1,Th55 .=f.x by A12,A8; hence thesis; end; dom((-(id Z)^(#)arccot)`|Z)=dom f by A1,A3,FDIFF_1:def 7; then((-(id Z)^(#)arccot)`|Z)= f by A11,PARTFUN1:5; hence thesis by A1,A2,Th55,INTEGRA5:13; end;