:: Several Integrability Formulas of Special Functions -- Part {II} :: by Bo Li , Yanping Zhuang , Yanhong Men and Xiquan Liang :: :: Received October 14, 2008 :: Copyright (c) 2008-2018 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 REAL_1, SUBSET_1, NUMBERS, INTEGRA1, RCOMP_1, RELAT_1, JGRAPH_2, ARYTM_3, CARD_1, SIN_COS, VALUED_1, ARYTM_1, FDIFF_1, FUNCT_1, SQUARE_1, PREPOWER, SIN_COS2, ORDINAL2, XXREAL_2, XXREAL_1, INTEGRA5, XBOOLE_0, PARTFUN1, TARSKI, ORDINAL4, SIN_COS4, SIN_COS9, XXREAL_0, TAYLOR_1, SIN_COS6, SEQ_4, MEASURE5; notations TARSKI, XBOOLE_0, FUNCT_1, SIN_COS, SUBSET_1, ORDINAL1, NUMBERS, RELAT_1, VALUED_1, XXREAL_0, XCMPLX_0, REAL_1, XREAL_0, PARTFUN1, PARTFUN2, RCOMP_1, RFUNCT_1, MEASURE5, FCONT_1, SQUARE_1, INTEGRA5, PREPOWER, TAYLOR_1, FDIFF_1, SEQ_2, SIN_COS2, FDIFF_9, SIN_COS4, SIN_COS6, SIN_COS9, SEQ_4; constructors SIN_COS, TAYLOR_1, REAL_1, FDIFF_1, FCONT_1, SQUARE_1, PREPOWER, INTEGRA5, SIN_COS2, SEQ_4, SIN_COS9, PARTFUN2, SIN_COS6, RFUNCT_1, FDIFF_9, SIN_COS4, RELSET_1, INTEGRA1, COMSEQ_2, COMPLEX1, SERIES_1, BINOP_2; registrations VALUED_1, NAT_1, NUMBERS, MEMBERED, VALUED_0, INT_1, RELAT_1, ORDINAL1, FUNCT_2, RCOMP_1, FCONT_1, TOPREALB, FCONT_3, MEASURE5, XREAL_0, SIN_COS, PREPOWER, SQUARE_1; requirements NUMERALS, BOOLE, SUBSET, ARITHM; equalities SIN_COS, VALUED_1, SUBSET_1, SQUARE_1, SIN_COS4, FDIFF_9, XBOOLE_0; theorems PARTFUN1, RFUNCT_1, FUNCT_1, FDIFF_1, FUNCT_2, SQUARE_1, XCMPLX_1, INTEGRA5, INTEGRA8, SIN_COS, FDIFF_4, TAYLOR_1, VALUED_1, FCONT_1, SIN_COS5, SIN_COS4, SIN_COS2, SIN_COS6, XXREAL_1, XBOOLE_1, FDIFF_5, FDIFF_7, FDIFF_8, FDIFF_9, SIN_COS9, PREPOWER, FDIFF_6, XREAL_0; begin :: Differentiation Formulas reserve r,x,x0,a,b for Real; reserve n,m for Element of NAT; reserve A for non empty closed_interval Subset of REAL; reserve Z for open Subset of REAL; Lm1: [#]REAL = dom (AffineMap(1/2,0)) by FUNCT_2:def 1; Lm2: [#]REAL = dom (sin*AffineMap(2,0)) by FUNCT_2:def 1; Lm3: dom ((1/4)(#)(sin*AffineMap(2,0)))=[#]REAL by FUNCT_2:def 1; :: f.x = (1/2)*x-(1/4)*sin(2*x) theorem Th1: AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL & for x holds ((AffineMap(1/2,0)-(1/4)(#)(sin* AffineMap(2,0)))`|REAL).x = (sin.x)^2 proof A1: for x st x in REAL holds AffineMap(2,0).x=2*x + 0 by FCONT_1:def 4; then A2: sin*AffineMap(2,0) is_differentiable_on REAL by Lm2,FDIFF_4:37; then A3: (1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL by Lm3,FDIFF_1:20; A4: dom (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))) = [#]REAL by FUNCT_2:def 1; A5: for x st x in REAL holds AffineMap(1/2,0).x=(1/2)*x + 0 by FCONT_1:def 4; then A6: AffineMap(1/2,0) is_differentiable_on REAL by Lm1,FDIFF_1:23; hence AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL by A4,A3,FDIFF_1:19; A7: for x st x in REAL holds (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/2) *cos(2*x) proof let x; assume A8: x in REAL; (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/4)*diff((sin*AffineMap(2, 0)),x) by A2,Lm3,FDIFF_1:20,A8 .=(1/4)*((sin*AffineMap(2,0))`|REAL).x by A2,FDIFF_1:def 7,A8 .=(1/4)*(2*cos.(2*x+0)) by A1,Lm2,FDIFF_4:37,A8 .=(1/2)*cos(2*x); hence thesis; end; A9: for x st x in REAL holds ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)) )`|REAL).x = (sin.x)^2 proof let x; assume A10: x in REAL; ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =diff( AffineMap(1/2,0),x) - diff((1/4)(#)(sin*AffineMap(2,0)),x) by A4,A6,A3, FDIFF_1:19,A10 .=((AffineMap(1/2,0))`|REAL).x -diff((1/4)(#)(sin*AffineMap(2,0)),x) by A6,FDIFF_1:def 7,A10 .=(1/2)-diff((1/4)(#)(sin*AffineMap(2,0)),x) by A5,Lm1,FDIFF_1:23,A10 .=(1/2)-(((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x by A3,FDIFF_1:def 7,A10 .=(1/2)-(1/2)*cos(2*x) by A7,A10 .=(1-cos(2*x))/2 .=(sin(x))^2 by SIN_COS5:20; hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A9; end; :: f.x = (1/2)*x+(1/4)*sin(2*x) theorem Th2: AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL & for x holds ((AffineMap(1/2,0)+(1/4)(#)(sin* AffineMap(2,0)))`|REAL).x = (cos.x)^2 proof A1: for x st x in REAL holds AffineMap(2,0).x=2*x + 0 by FCONT_1:def 4; then A2: sin*AffineMap(2,0) is_differentiable_on REAL by Lm2,FDIFF_4:37; then A3: (1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL by Lm3,FDIFF_1:20; A4: dom (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))) = [#]REAL by FUNCT_2:def 1; A5: for x st x in REAL holds AffineMap(1/2,0).x=(1/2)*x + 0 by FCONT_1:def 4; then A6: AffineMap(1/2,0) is_differentiable_on REAL by Lm1,FDIFF_1:23; hence AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)) is_differentiable_on REAL by A4,A3,FDIFF_1:18; A7: for x st x in REAL holds (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/2) *cos(2*x) proof let x; assume A8: x in REAL; (((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =(1/4)*diff((sin*AffineMap(2, 0)),x) by A2,Lm3,FDIFF_1:20,A8 .=(1/4)*((sin*AffineMap(2,0))`|REAL).x by A2,FDIFF_1:def 7,A8 .=(1/4)*(2*cos.(2*x+0)) by A1,Lm2,FDIFF_4:37,A8 .=(1/2)*cos(2*x); hence thesis; end; A9: for x st x in REAL holds ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)) )`|REAL).x = (cos.x)^2 proof let x; assume A10: x in REAL; ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x =diff( AffineMap(1/2,0),x) + diff((1/4)(#)(sin*AffineMap(2,0)),x) by A4,A6,A3, FDIFF_1:18,A10 .=((AffineMap(1/2,0))`|REAL).x +diff((1/4)(#)(sin*AffineMap(2,0)),x) by A6,FDIFF_1:def 7,A10 .=(1/2)+diff((1/4)(#)(sin*AffineMap(2,0)),x) by A5,Lm1,FDIFF_1:23,A10 .=(1/2)+(((1/4)(#)(sin*AffineMap(2,0)))`|REAL).x by A3,FDIFF_1:def 7,A10 .=(1/2)+(1/2)*cos(2*x) by A7,A10 .=(1+cos(2*x))/2 .=(cos(x))^2 by SIN_COS5:21; hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A9; end; :: f.x = (1/(n+1))*(sin.x)^(n+1) theorem Th3: (1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL & for x holds (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x = ((sin.x) #Z n)*cos.x proof A1: [#]REAL = dom((1/(n+1))(#)( #Z (n+1)*sin)) by FUNCT_2:def 1; #Z (n+1)*sin is_differentiable_in x0 proof sin is_differentiable_in x0 by SIN_COS:64; hence thesis by TAYLOR_1:3; end; then [#]REAL = dom ( #Z (n+1)*sin) & for x0 st x0 in REAL holds #Z (n+1)*sin is_differentiable_in x0 by FUNCT_2:def 1; then A2: #Z (n+1)*sin is_differentiable_on REAL by FDIFF_1:9; hence (1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL by A1,FDIFF_1:20; A3: for x st x in REAL holds (( #Z (n+1)*sin)`|REAL).x=(n+1) * ((sin.x) #Z n )*cos.x proof set m=n+1; let x; assume A4: x in REAL; sin is_differentiable_in x by SIN_COS:64; then diff(( #Z m*sin),x) = m * (sin.x) #Z (m-1) *diff(sin,x) by TAYLOR_1:3 .= m * (sin.x) #Z (m-1) *(cos .x) by SIN_COS:64; hence thesis by A2,FDIFF_1:def 7,A4; end; A5: for x st x in REAL holds (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(sin.x ) #Z n *cos.x proof let x; assume A6: x in REAL; (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(1/(n+1))*diff( #Z (n+1)*sin ,x) by A1,A2,FDIFF_1:20,A6 .=(1/(n+1))*((( #Z (n+1)*sin)`|REAL).x) by A2,FDIFF_1:def 7,A6 .=(1/(n+1))*((n+1) * (sin.x) #Z n *cos.x) by A3,A6 .=(1/(n+1))*(n+1) * (sin.x) #Z n *cos.x .=(n+1)/(n+1) * (sin.x) #Z n *cos.x by XCMPLX_1:99 .=1*(sin.x) #Z n *cos.x by XCMPLX_1:60; hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A5; end; :: f.x = (-1/(n+1))*(cos.x)^(n+1) theorem Th4: (-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL & for x holds (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x = ((cos.x) #Z n)*sin.x proof A1: [#]REAL = dom((-1/(n+1))(#)( #Z (n+1)*cos)) by FUNCT_2:def 1; #Z (n+1)*cos is_differentiable_in x0 proof cos is_differentiable_in x0 by SIN_COS:63; hence thesis by TAYLOR_1:3; end; then A2: for x0 st x0 in REAL holds #Z (n+1)*cos is_differentiable_in x0; [#]REAL = dom ( #Z (n+1)) & REAL = dom ( #Z (n+1)*cos) by FUNCT_2:def 1; then A3: #Z (n+1)*cos is_differentiable_on REAL by A2,FDIFF_1:9; hence(-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL by A1,FDIFF_1:20; A4: for x st x in REAL holds (( #Z (n+1)*cos)`|REAL).x=(-(n+1)) * ((cos.x) #Z n)*sin.x proof set m=n+1; let x; assume A5:x in REAL; cos is_differentiable_in x by SIN_COS:63; then diff(( #Z m*cos),x) = m * (cos.x) #Z (m-1) *diff(cos,x) by TAYLOR_1:3 .= m * (cos.x) #Z (m-1) *(-sin .x) by SIN_COS:63 .= (-m) * (cos.x) #Z (m-1) *sin .x; hence thesis by A3,FDIFF_1:def 7,A5; end; A6: for x st x in REAL holds (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(cos .x) #Z n *sin.x proof let x; assume A7:x in REAL; (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(-1/(n+1))*diff( #Z (n+1)* cos,x) by A1,A3,FDIFF_1:20,A7 .=(-1/(n+1))*((( #Z (n+1)*cos)`|REAL).x) by A3,FDIFF_1:def 7,A7 .=(-1/(n+1))*((-(n+1)) * (cos.x) #Z n *sin.x) by A4,A7 .=(1/(n+1))*(n+1) * (cos.x) #Z n *sin.x .=(n+1)/(n+1) * (cos.x) #Z n *sin.x by XCMPLX_1:99 .=1*(cos.x) #Z n *sin.x by XCMPLX_1:60; hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A6; end; :: f.x=sin.((m+n)*x)/(2*(m+n))+sin.((m-n)*x)/(2*(m-n)) theorem Th5: m+n<>0 & m-n<>0 implies ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) is_differentiable_on REAL & for x holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0) ))`|REAL).x = cos.(m*x) *cos.(n*x) proof assume that A1: m+n <> 0 and A2: m-n<>0; A3: dom (sin*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A4: sin*AffineMap(m-n,0) is_differentiable_on REAL by FDIFF_4:37; A5: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1; then A6: (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)) is_differentiable_on REAL by A4, FDIFF_1:20; A7: for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`| REAL).x=(1/2)*cos((m-n)*x) proof let x; assume A8: x in REAL; (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))* diff((sin*AffineMap(m-n,0)),x) by A5,A4,FDIFF_1:20,A8 .=(1/(2*(m-n)))*((sin*AffineMap(m-n,0))`|REAL).x by A4,FDIFF_1:def 7,A8 .=(1/(2*(m-n)))*((m-n)* cos.((m-n)*x+0)) by A3,FDIFF_4:37,A8 .=(m-n)*(1/(2*(m-n)))* cos.((m-n)*x+0) .=((1*(m-n))/(2*(m-n)))* cos.((m-n)*x+0) by XCMPLX_1:74 .=(1/2)* cos((m-n)*x) by A2,XCMPLX_1:91; hence thesis; end; A9: dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin* AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1; A10: dom (sin*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A11: sin*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:37; A12: [#]REAL = dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) by FUNCT_2:def 1; then A13: (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)) is_differentiable_on REAL by A11, FDIFF_1:20; hence((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) is_differentiable_on REAL by A9,A6,FDIFF_1:18; A14: for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL ).x=(1/2)*cos((m+n)*x) proof let x; assume A15: x in REAL; (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x =(1/(2*(m+n)))* diff((sin*AffineMap(m+n,0)),x) by A12,A11,FDIFF_1:20,A15 .=(1/(2*(m+n)))*((sin*AffineMap(m+n,0))`|REAL).x by A11,FDIFF_1:def 7,A15 .=(1/(2*(m+n)))*((m+n)* cos.((m+n)*x+0)) by A10,FDIFF_4:37,A15 .=(m+n)*(1/(2*(m+n)))* cos.((m+n)*x+0) .=((1*(m+n))/(2*(m+n)))* cos.((m+n)*x+0) by XCMPLX_1:74 .=(1/2)* cos((m+n)*x) by A1,XCMPLX_1:91; hence thesis; end; A16: for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/( 2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x = cos.(m*x) *cos.(n*x) proof let x; assume A17: x in REAL; (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin* AffineMap(m-n,0)))`|REAL).x = diff((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)),x) + diff((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)),x) by A9,A13,A6,FDIFF_1:18,A17 .= (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x +diff((1/(2*(m-n )))(#)(sin*AffineMap(m-n,0)),x) by A13,FDIFF_1:def 7,A17 .= (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x +(((1/(2*(m-n))) (#)(sin*AffineMap(m-n,0)))`|REAL).x by A6,FDIFF_1:def 7,A17 .= (1/2)*cos((m+n)*x)+(((1/(2*(m-n))) (#)(sin*AffineMap(m-n,0)))`|REAL ).x by A14,A17 .= (1/2)*cos((m+n)*x)+(1/2)* cos((m-n)*x) by A7,A17 .= (1/2)*(cos((m+n)*x)+cos((m-n)*x)) .= (1/2)*(2*(cos(((m+n)*x+(m-n)*x)/2) *cos(((m+n)*x-(m-n)*x)/2))) by SIN_COS4:17 .= cos.(m*x)*cos.(n*x); hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A16; end; :: f.x=sin.((m-n)*x)/(2*(m-n))-sin.((m+n)*x)/(2*(m+n)) theorem Th6: m+n<>0 & m-n<>0 implies ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) is_differentiable_on REAL & for x holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0) ))`|REAL).x = sin.(m*x)*sin.(n*x) proof assume that A1: m+n <> 0 and A2: m-n <> 0; A3: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1; A4: dom (sin*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A5: sin*AffineMap(m-n,0) is_differentiable_on REAL by FDIFF_4:37; then A6: (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)) is_differentiable_on REAL by A3, FDIFF_1:20; A7: for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`| REAL).x=(1/2)*cos((m-n)*x) proof let x; assume A8: x in REAL; (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))* diff((sin*AffineMap(m-n,0)),x) by A3,A5,FDIFF_1:20,A8 .=(1/(2*(m-n)))*((sin*AffineMap(m-n,0))`|REAL).x by A5,FDIFF_1:def 7,A8 .=(1/(2*(m-n)))*((m-n)* cos.((m-n)*x+0)) by A4,FDIFF_4:37,A8 .=(m-n)*(1/(2*(m-n)))* cos.((m-n)*x+0) .=((1*(m-n))/(2*(m-n)))* cos.((m-n)*x+0) by XCMPLX_1:74 .=(1/2)* cos((m-n)*x) by A2,XCMPLX_1:91; hence thesis; end; A9: dom ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin* AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1; A10: dom (sin*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A11: sin*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:37; A12: REAL = dom ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) by FUNCT_2:def 1; then A13: (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)) is_differentiable_on REAL by A3,A11 ,FDIFF_1:20; hence ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))) is_differentiable_on REAL by A9,A6,FDIFF_1:19; A14: for x st x in REAL holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL ).x=(1/2)*cos((m+n)*x) proof let x; assume A15: x in REAL; (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x =(1/(2*(m+n)))* diff((sin*AffineMap(m+n,0)),x) by A12,A3,A11,FDIFF_1:20,A15 .=(1/(2*(m+n)))*((sin*AffineMap(m+n,0))`|REAL).x by A11,FDIFF_1:def 7,A15 .=(1/(2*(m+n)))*((m+n)* cos.((m+n)*x+0)) by A10,FDIFF_4:37,A15 .=(m+n)*(1/(2*(m+n)))* cos.((m+n)*x+0) .=((1*(m+n))/(2*(m+n)))* cos.((m+n)*x+0) by XCMPLX_1:74 .=(1/2)* cos((m+n)*x) by A1,XCMPLX_1:91; hence thesis; end; A16: for x st x in REAL holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/( 2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x = sin.(m*x) *sin.(n*x) proof let x; assume A17: x in REAL; (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin* AffineMap(m+n,0)))`|REAL).x = diff((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)),x) - diff((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)),x) by A9,A13,A6,FDIFF_1:19,A17 .= (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x -diff((1/(2*(m+n )))(#)(sin*AffineMap(m+n,0)),x) by A6,FDIFF_1:def 7,A17 .= (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x -(((1/(2*(m+n))) (#)(sin*AffineMap(m+n,0)))`|REAL).x by A13,FDIFF_1:def 7,A17 .= (1/2)*cos((m-n)*x)-(((1/(2*(m+n))) (#)(sin*AffineMap(m+n,0)))`|REAL ).x by A7,A17 .= (1/2)*cos((m-n)*x)-(1/2)* cos((m+n)*x) by A14,A17 .= (1/2)*(cos((m-n)*x)-cos((m+n)*x)) .= (1/2)*(-2*(sin(((m-n)*x+(m+n)*x)/2) *sin(((m-n)*x-(m+n)*x)/2))) by SIN_COS4:18 .= (1/2)*(-2*(sin(m*x)*sin(-(n*x)))) .= (1/2)*(-2*(sin(m*x)*(-sin(n*x)))) by SIN_COS:31 .= sin.(m*x)*sin.(n*x); hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A16; end; :: f.x=-cos.((m+n)*x)/(2*(m+n))-cos.((m-n)*x)/(2*(m-n)) theorem Th7: m+n<>0 & m-n<>0 implies ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)) ) - (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) is_differentiable_on REAL & for x holds ((-((1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos* AffineMap(m-n,0)))`|REAL).x = sin.(m*x) * cos.(n*x) proof assume that A1: m+n <> 0 and A2: m-n <> 0; A3: dom (cos*AffineMap(m+n,0)) = [#]REAL & for x st x in REAL holds AffineMap(m+ n,0).x=(m+n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A4: cos*AffineMap(m+n,0) is_differentiable_on REAL by FDIFF_4:38; A5: for x st x in REAL holds ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`| REAL).x=(1/2)*sin((m+n)*x) proof let x; assume A6: x in REAL; A7: dom (((-1)/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))=[#]REAL by FUNCT_2:def 1; ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x =((((-1)*(1/(2*(m +n)))) (#)(cos*AffineMap(m+n,0)))`|REAL).x by RFUNCT_1:17 .=(((-(1/(2*(m+n))))(#)(cos*AffineMap(m+n,0)))`|REAL).x .=((((-1)/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x by XCMPLX_1:187 .=((-1)/(2*(m+n)))*diff((cos*AffineMap(m+n,0)),x) by A4,A7,FDIFF_1:20,A6 .=((-1)/(2*(m+n)))*((cos*AffineMap(m+n,0))`|REAL).x by A4,FDIFF_1:def 7, A6 .=((-1)/(2*(m+n)))*(-(m+n)* sin.((m+n)*x+0)) by A3,FDIFF_4:38,A6 .=(-(-1)/(2*(m+n)))*(m+n)* sin.((m+n)*x+0) .=(1/(2*(m+n)))*(m+n)* sin.((m+n)*x+0) by XCMPLX_1:190 .=((1*(m+n))/(2*(m+n)))* sin.((m+n)*x+0) by XCMPLX_1:74 .=(1/2)* sin((m+n)*x) by A1,XCMPLX_1:91; hence thesis; end; A8: dom (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1; dom ((1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = [#]REAL by FUNCT_2:def 1; then (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) = (-1)(#) ((1/(2*(m+n)))(#)( cos* AffineMap(m+n,0))) & (1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)) is_differentiable_on REAL by A4,FDIFF_1:20; then A9: (-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) is_differentiable_on REAL by A8, FDIFF_1:20; A10: REAL = dom ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)( cos*AffineMap(m-n,0))) by FUNCT_2:def 1; A11: dom (cos*AffineMap(m-n,0)) = [#]REAL & for x st x in REAL holds AffineMap(m- n,0).x=(m-n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A12: cos*(AffineMap(m-n,0)) is_differentiable_on REAL by FDIFF_4:38; A13: dom ((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) = [#]REAL by FUNCT_2:def 1; then A14: (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)) is_differentiable_on REAL by A12, FDIFF_1:20; hence ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)) ) - (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0))) is_differentiable_on REAL by A8,A10,A9,FDIFF_1:19; A15: for x st x in REAL holds (((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`| REAL).x=-(1/2)*sin((m-n)*x) proof let x; assume A16: x in REAL; (((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x =(1/(2*(m-n)))* diff((cos*AffineMap(m-n,0)),x) by A13,A12,FDIFF_1:20,A16 .=(1/(2*(m-n)))*((cos*AffineMap(m-n,0))`|REAL).x by A12,FDIFF_1:def 7,A16 .=(1/(2*(m-n)))*(-(m-n)* sin.((m-n)*x+0)) by A11,FDIFF_4:38,A16 .=(-1/(2*(m-n)))*(m-n)* sin.((m-n)*x+0) .=((-1)/(2*(m-n)))*(m-n)* sin.((m-n)*x+0) by XCMPLX_1:187 .=(((-1)*(m-n))/(2*(m-n)))* sin.((m-n)*x+0) by XCMPLX_1:74 .=(-1)/2* sin((m-n)*x) by A2,XCMPLX_1:91; hence thesis; end; A17: for x st x in REAL holds ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))- (1/ (2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x = sin.(m*x) *cos.(n*x) proof let x; assume A18: x in REAL; ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))- (1/(2*(m-n)))(#)(cos* AffineMap(m-n,0)))`|REAL).x = diff((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))),x) -diff((1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)),x) by A8,A10,A9,A14,FDIFF_1:19,A18 .= ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x -diff((1/(2*(m- n)))(#)(cos*AffineMap(m-n,0)),x) by A9,FDIFF_1:def 7,A18 .= ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))`|REAL).x -(((1/(2*(m-n)) )(#)(cos*AffineMap(m-n,0)))`|REAL).x by A14,FDIFF_1:def 7,A18 .= (1/2)*sin((m+n)*x)-(((1/(2*(m-n))) (#)(cos*AffineMap(m-n,0)))`|REAL ).x by A5,A18 .= (1/2)*sin((m+n)*x)-(-(1/2)* sin((m-n)*x)) by A15,A18 .= (1/2)*(sin((m+n)*x)+sin((m-n)*x)) .= (1/2)*(2*(cos(((m+n)*x-(m-n)*x)/2) *sin(((m+n)*x+(m-n)*x)/2))) by SIN_COS4:15 .= sin.(m*x)*cos.(n*x); hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A17; end; :: f.x = (1/(n^2))*sin.(n*x)-(1/n)*x*cos.(n*x) theorem Th8: n<>0 implies ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0) )(#)(cos*AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/(n^2)) (#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x=x* sin.(n*x) proof A1: dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos* AffineMap(n,0)))) = [#]REAL by FUNCT_2:def 1; A2: dom (AffineMap(1/n,0))=REAL & for x st x in REAL holds AffineMap(1/n,0) .x=(1 /n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A3: AffineMap(1/n,0) is_differentiable_on REAL by A1,FDIFF_1:23; A4: for x st x in REAL holds AffineMap(n,0).x=n*x + 0 by FCONT_1:def 4; A5: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; then A6: sin*(AffineMap(n,0)) is_differentiable_on REAL by A4,FDIFF_4:37; A7: dom ((1/(n^2))(#)(sin*AffineMap(n,0)))=REAL by FUNCT_2:def 1; then A8: (1/(n^2))(#)(sin*AffineMap(n,0)) is_differentiable_on REAL by A1,A6, FDIFF_1:20; assume A9: n<>0; A10: for x st x in REAL holds (((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x = (1/n)*cos(n*x) proof let x; assume A11: x in REAL; (((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x =(1/(n^2))*diff((sin* AffineMap(n,0)),x) by A7,A1,A6,FDIFF_1:20,A11 .=(1/(n^2))*((sin*AffineMap(n,0))`|REAL).x by A6,FDIFF_1:def 7,A11 .=(1/(n^2))*(n * cos.(n*x+0)) by A5,A4,FDIFF_4:37,A11 .= n*(1/(n*n))*(cos.(n*x+0)) .= (n*1)/(n*n)*(cos.(n*x+0)) by XCMPLX_1:74 .= (1/n)*(cos.(n*x+0)) by A9,XCMPLX_1:91; hence thesis; end; A12: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; then A13: cos*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:38; A14: dom ((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))=REAL by FUNCT_2:def 1; then A15: ((AffineMap(1/n,0))(#)(cos*AffineMap(n,0))) is_differentiable_on REAL by A1,A3,A13,FDIFF_1:21; hence ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0) )(#)(cos*AffineMap(n,0))) is_differentiable_on REAL by A1,A8,FDIFF_1:19; A16: for x st x in REAL holds (((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`| REAL).x = (1/n)*cos.(n*x)-x* sin.(n*x) proof let x; assume A17: x in REAL; (((AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = ((cos* AffineMap(n,0)).x)*diff(AffineMap(1/n,0),x) + (AffineMap(1/n,0).x)*diff(cos*( AffineMap(n,0)),x) by A14,A1,A3,A13,FDIFF_1:21,A17 .= ((cos*AffineMap(n,0)).x)*((AffineMap(1/n,0)`|REAL).x) +(AffineMap(1 /n,0).x)*diff((cos*AffineMap(n,0)),x) by A3,FDIFF_1:def 7,A17 .= ((cos*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *diff((cos* AffineMap(n,0)),x) by A1,A2,FDIFF_1:23,A17 .= ((cos*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *(((cos* AffineMap(n,0))`|REAL).x) by A13,FDIFF_1:def 7,A17 .= ((cos*AffineMap(n,0)).x)*(1/n) +(AffineMap(1/n,0).x)*(-n* sin.(n*x+ 0)) by A12,A4,FDIFF_4:38,A17 .= ((cos*AffineMap(n,0)).x)*(1/n) +((1/n)*x + 0)*(-n* sin.(n*x+0)) by FCONT_1:def 4 .= (cos.(AffineMap(n,0).x))*(1/n) +((1/n)*x)*(-n* sin.(n*x+0)) by A12, FUNCT_1:12,A17 .= (1/n)*cos.(n*x)+(-((1/n)*n*x* sin.(n*x))) by FCONT_1:def 4 .= (1/n)*cos.(n*x)+(-(1*x* sin.(n*x))) by A9,XCMPLX_1:87 .= (1/n)*cos.(n*x)-x* sin.(n*x); hence thesis; end; A18: for x st x in REAL holds (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap (1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = x*sin.(n*x) proof let x; assume A19: x in REAL; (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos* AffineMap(n,0)))`|REAL).x = diff((1/(n^2))(#)(sin*AffineMap(n,0)),x) - diff(( AffineMap(1/n,0))(#)(cos*AffineMap(n,0)),x) by A1,A8,A15,FDIFF_1:19,A19 .= ((((1/(n^2))(#)(sin*AffineMap(n,0)))`|REAL).x) - diff(AffineMap(1/n ,0)(#)(cos*AffineMap(n,0)),x) by A8,FDIFF_1:def 7,A19 .= (1/n)*cos(n*x)-diff(AffineMap(1/n,0) (#)(cos*AffineMap(n,0)),x) by A10,A19 .= (1/n)*cos(n*x)-(((AffineMap(1/n,0) (#)(cos*AffineMap(n,0)))`|REAL). x) by A15,FDIFF_1:def 7,A19 .= (1/n)*cos(n*x)-((1/n)*cos.(n*x)-x* sin.(n*x)) by A16,A19 .= x* sin.(n*x); hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A18; end; :: f.x = (1/(n^2))*cos.(n*x)+(1/n)*x*sin.(n*x) theorem Th9: n<>0 implies ((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0) )(#)(sin*AffineMap(n,0))) is_differentiable_on REAL & for x holds (((1/(n^2)) (#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x=x* cos.(n*x) proof A1: dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin* AffineMap(n,0)))) = [#]REAL by FUNCT_2:def 1; A2: dom (AffineMap(1/n,0))=REAL & for x st x in REAL holds AffineMap(1/n,0) .x=(1 /n)*x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A3: AffineMap(1/n,0) is_differentiable_on REAL by A1,FDIFF_1:23; A4: for x st x in REAL holds AffineMap(n,0).x=n*x + 0 by FCONT_1:def 4; A5: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; then A6: cos*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:38; A7: dom ((1/(n^2))(#)(cos*AffineMap(n,0)))=REAL by FUNCT_2:def 1; then A8: (1/(n^2))(#)(cos*AffineMap(n,0)) is_differentiable_on REAL by A1,A6, FDIFF_1:20; assume A9: n<>0; A10: for x st x in REAL holds (((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x = -(1/n)*sin(n*x) proof let x; assume A11: x in REAL; (((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x =(1/(n^2))*diff((cos* AffineMap(n,0)),x) by A7,A1,A6,FDIFF_1:20,A11 .=(1/(n^2))*((cos*AffineMap(n,0))`|REAL).x by A6,FDIFF_1:def 7,A11 .=(1/(n^2))*(-n * sin.(n*x+0)) by A5,A4,FDIFF_4:38,A11 .=(-1)*(n*(1/(n*n)))*(sin.(n*x+0)) .=(-1)*(n/((n*n)/1))*(sin.(n*x+0)) by XCMPLX_1:79 .=(-1)*((n*1)/(n*n))*(sin.(n*x+0)) .=(-1)*(1/n)*(sin.(n*x+0)) by A9,XCMPLX_1:91; hence thesis; end; A12: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; then A13: sin*AffineMap(n,0) is_differentiable_on REAL by A4,FDIFF_4:37; A14: dom ((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))=REAL by FUNCT_2:def 1; then A15: ((AffineMap(1/n,0))(#)(sin*AffineMap(n,0))) is_differentiable_on REAL by A1,A3,A13,FDIFF_1:21; hence((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0) )(#)(sin*AffineMap(n,0))) is_differentiable_on REAL by A1,A8,FDIFF_1:18; A16: for x st x in REAL holds (((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`| REAL).x = (1/n)*sin.(n*x)+x* cos.(n*x) proof let x; assume A17: x in REAL; (((AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = ((sin* AffineMap(n,0)).x)*diff((AffineMap(1/n,0)),x) + ((AffineMap(1/n,0)).x)*diff(( sin*AffineMap(n,0)),x) by A14,A1,A3,A13,FDIFF_1:21,A17 .= ((sin*AffineMap(n,0)).x)*((AffineMap(1/n,0)`|REAL).x) +((AffineMap( 1/n,0)).x)*diff((sin*AffineMap(n,0)),x) by A3,FDIFF_1:def 7,A17 .= ((sin*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *diff((sin* AffineMap(n,0)),x) by A1,A2,FDIFF_1:23,A17 .= ((sin*AffineMap(n,0)).x)*(1/n)+(AffineMap(1/n,0).x) *(((sin* AffineMap(n,0))`|REAL).x) by A13,FDIFF_1:def 7,A17 .= ((sin*AffineMap(n,0)).x)*(1/n) +(AffineMap(1/n,0).x)*(n* cos.(n*x+0 )) by A12,A4,FDIFF_4:37,A17 .= ((sin*AffineMap(n,0)).x)*(1/n) +((1/n)*x + 0)*(n* cos.(n*x+0)) by FCONT_1:def 4 .= (sin.(AffineMap(n,0).x))*(1/n) +((1/n)*x)*(n* cos.(n*x+0)) by A12, FUNCT_1:12,A17 .= (1/n)*sin.(n*x)+(1/n)*n*x* cos.(n*x) by FCONT_1:def 4 .= (1/n)*sin.(n*x)+1*x* cos.(n*x) by A9,XCMPLX_1:87 .= (1/n)*sin.(n*x)+x* cos.(n*x); hence thesis; end; A18: for x st x in REAL holds (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap (1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = x*cos.(n*x) proof let x; assume A19: x in REAL; (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin* AffineMap(n,0)))`|REAL).x = diff((1/(n^2))(#)(cos*AffineMap(n,0)),x) + diff(( AffineMap(1/n,0))(#)(sin*AffineMap(n,0)),x) by A1,A8,A15,FDIFF_1:18,A19 .= ((((1/(n^2))(#)(cos*AffineMap(n,0)))`|REAL).x) + diff((AffineMap(1/ n,0))(#)(sin*AffineMap(n,0)),x) by A8,FDIFF_1:def 7,A19 .= -(1/n)*sin(n*x)+diff(AffineMap(1/n,0) (#)(sin*AffineMap(n,0)),x) by A10,A19 .= -(1/n)*sin(n*x)+(((AffineMap(1/n,0) (#)(sin*AffineMap(n,0)))`|REAL) .x) by A15,FDIFF_1:def 7,A19 .= -(1/n)*sin(n*x)+((1/n)*sin.(n*x)+x* cos.(n*x)) by A16,A19 .= x* cos.(n*x); hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A18; end; :: f.x = x*cosh.x-sinh.x theorem Th10: (AffineMap(1,0))(#)cosh-sinh is_differentiable_on REAL & for x holds (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x=x*sinh.x proof A1: dom ((AffineMap(1,0))(#)cosh-sinh) = [#]REAL by FUNCT_2:def 1; A2: dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0) .x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A3: AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23; A4: dom ((AffineMap(1,0))(#)cosh) = [#]REAL by FUNCT_2:def 1; then A5: ((AffineMap(1,0))(#)cosh) is_differentiable_on REAL by A3,FDIFF_1:21 ,SIN_COS2:35; hence (AffineMap(1,0))(#)cosh-sinh is_differentiable_on REAL by A1,FDIFF_1:19,SIN_COS2:34; A6: for x st x in REAL holds (((AffineMap(1,0))(#)cosh)`|REAL).x = cosh.x+x* sinh.x proof let x; assume A7: x in REAL; (((AffineMap(1,0))(#)cosh)`|REAL).x = cosh.x*diff((AffineMap(1,0)),x)+ ((AffineMap(1,0)).x) *diff(cosh,x) by A4,A3,FDIFF_1:21,SIN_COS2:35,A7 .= cosh.x*(((AffineMap(1,0))`|REAL).x) +((AffineMap(1,0)).x)*diff(cosh ,x) by A3,FDIFF_1:def 7,A7 .= cosh.x*1+((AffineMap(1,0)).x)*diff(cosh,x) by A2,FDIFF_1:23,A7 .= cosh.x+((AffineMap(1,0)).x)*sinh.x by SIN_COS2:35 .= cosh.x+(1*x + 0)*sinh.x by FCONT_1:def 4 .= cosh.x+x*sinh.x; hence thesis; end; A8: for x st x in REAL holds (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x = x* sinh.x proof let x; assume A9: x in REAL; (((AffineMap(1,0))(#)cosh - sinh)`|REAL).x = diff(((AffineMap(1,0))(#) cosh),x) - diff(sinh,x) by A1,A5,FDIFF_1:19,SIN_COS2:34,A9 .= (((AffineMap(1,0))(#)cosh)`|REAL).x - diff(sinh,x) by A5,FDIFF_1:def 7,A9 .= cosh.x+x*sinh.x-diff(sinh,x) by A6,A9 .= cosh.x+x*sinh.x-cosh.x by SIN_COS2:34 .= x*sinh.x; hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A8; end; :: f.x = x*sinh.x-cosh.x theorem Th11: (AffineMap(1,0))(#)sinh-cosh is_differentiable_on REAL & for x holds (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x=x*cosh.x proof A1: dom ((AffineMap(1,0))(#)sinh-cosh) = [#]REAL by FUNCT_2:def 1; A2: dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0) .x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then A3: AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23; A4: dom ((AffineMap(1,0))(#)sinh) = [#]REAL by FUNCT_2:def 1; then A5: ((AffineMap(1,0))(#)sinh) is_differentiable_on REAL by A3,FDIFF_1:21 ,SIN_COS2:34; hence (AffineMap(1,0))(#)sinh-cosh is_differentiable_on REAL by A1,FDIFF_1:19,SIN_COS2:35; A6: for x st x in REAL holds (((AffineMap(1,0))(#)sinh)`|REAL).x = sinh.x+x* cosh.x proof let x; assume A7: x in REAL; (((AffineMap(1,0))(#)sinh)`|REAL).x = sinh.x*diff((AffineMap(1,0)),x)+ ((AffineMap(1,0)).x) *diff(sinh,x) by A4,A3,FDIFF_1:21,SIN_COS2:34,A7 .= sinh.x*(((AffineMap(1,0))`|REAL).x) +((AffineMap(1,0)).x)*diff(sinh ,x) by A3,FDIFF_1:def 7,A7 .= sinh.x*1+((AffineMap(1,0)).x)*diff(sinh,x) by A2,FDIFF_1:23,A7 .= sinh.x+((AffineMap(1,0)).x)*(cosh.x) by SIN_COS2:34 .= sinh.x+(1*x + 0)*cosh.x by FCONT_1:def 4 .= sinh.x+x*cosh.x; hence thesis; end; A8: for x st x in REAL holds (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x = x*( cosh.x) proof let x; assume A9: x in REAL; (((AffineMap(1,0))(#)sinh - cosh)`|REAL).x = diff(((AffineMap(1,0))(#) sinh),x) - diff(cosh,x) by A1,A5,FDIFF_1:19,SIN_COS2:35,A9 .= (((AffineMap(1,0))(#)sinh)`|REAL).x - diff(cosh,x) by A5,FDIFF_1:def 7,A9 .= sinh.x+x*cosh.x-diff(cosh,x) by A6,A9 .= sinh.x+x*cosh.x-sinh.x by SIN_COS2:35 .= x*cosh.x; hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A8; end; :: f.x = (1/(a*(n+1)))*(a*x+b)^(n+1) theorem Th12: a*(n+1) <> 0 implies (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)) is_differentiable_on REAL & for x holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap( a,b)))`|REAL).x = (a*x+b) #Z n proof assume A1: a*(n+1) <> 0; A2: [#]REAL = dom((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))) by FUNCT_2:def 1; A3: [#]REAL = dom (AffineMap(a,b)) by FUNCT_2:def 1; A4: for x st x in REAL holds AffineMap(a,b).x=a*x + b by FCONT_1:def 4; then A5: AffineMap(a,b) is_differentiable_on REAL by A3,FDIFF_1:23; #Z (n+1)*AffineMap(a,b) is_differentiable_in x proof x in REAL by XREAL_0:def 1; then AffineMap(a,b) is_differentiable_in x by A3,A5,FDIFF_1:9; hence thesis by TAYLOR_1:3; end; then [#]REAL = dom ( #Z (n+1)*AffineMap(a,b)) & for x st x in REAL holds #Z ( n+1) *AffineMap(a,b) is_differentiable_in x by FUNCT_2:def 1; then A6: #Z (n+1)*AffineMap(a,b) is_differentiable_on REAL by FDIFF_1:9; hence (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)) is_differentiable_on REAL by A2,FDIFF_1:20; A7: for x st x in REAL holds (( #Z (n+1)*AffineMap(a,b))`|REAL).x=a*(n+1)*( AffineMap(a,b).x) #Z n proof set m=n+1; let x; assume A8: x in REAL; AffineMap(a,b) is_differentiable_in x by A3,A5,FDIFF_1:9,A8; then diff(( #Z m*AffineMap(a,b)),x) = m * (AffineMap(a,b).x) #Z (m-1) * diff(AffineMap(a,b),x) by TAYLOR_1:3 .= m * (AffineMap(a,b).x) #Z (m-1) * ((AffineMap(a,b))`|REAL).x by A5, FDIFF_1:def 7,A8 .= m * (AffineMap(a,b).x) #Z (m-1) *a by A3,A4,FDIFF_1:23,A8; hence thesis by A6,FDIFF_1:def 7,A8; end; A9: for x st x in REAL holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b))) `|REAL).x =(a*x+b) #Z n proof let x; assume A10: x in REAL; (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x =(1/(a*(n+1))) *diff( #Z (n+1)*AffineMap(a,b),x) by A2,A6,FDIFF_1:20,A10 .=(1/(a*(n+1)))*((( #Z (n+1)*AffineMap(a,b))`|REAL).x) by A6, FDIFF_1:def 7,A10 .=(1/(a*(n+1)))*(a*(n+1) * (AffineMap(a,b).x) #Z n ) by A7,A10 .=(1/(a*(n+1)))*(a*(n+1)) * (AffineMap(a,b).x) #Z n .=(a*(n+1))/(a*(n+1)) * (AffineMap(a,b).x) #Z n by XCMPLX_1:99 .=1*(AffineMap(a,b).x) #Z n by A1,XCMPLX_1:60 .=(a*x+b) #Z n by FCONT_1:def 4; hence thesis; end; let x; x in REAL by XREAL_0:def 1; hence thesis by A9; end; begin :: Integrability Formulas :: f.x = (sin.x)^2 theorem Th13: integral(sin^2,A) = (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0 ))).(upper_bound A) -(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))). (lower_bound A) proof A1: for x being Element of REAL st x in dom ((AffineMap(1/2,0) -(1/4)(#)(sin*AffineMap(2,0)))`|REAL ) holds ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (sin^2).x proof let x be Element of REAL; assume x in dom ((AffineMap(1/2,0) -(1/4)(#)(sin*AffineMap(2,0)))`|REAL); ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (sin.x)^2 by Th1 .= (sin^2).x by VALUED_1:11; hence thesis; end; A2: dom (sin^2)=REAL by SIN_COS:24,VALUED_1:11; then dom ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = dom (sin^2 ) by Th1,FDIFF_1:def 7; then A3: ((AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = sin^2 by A1, PARTFUN1:5; (sin^2)|A is bounded by A2,INTEGRA5:10; hence thesis by A2,A3,Th1,INTEGRA5:11,13; end; Lm4: dom (AffineMap(2,0)) = [#]REAL by FUNCT_2:def 1; Lm5: dom (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0)))=REAL by FUNCT_2:def 1; reconsider pp = PI as Element of REAL by XREAL_0:def 1; Lm6: 0 in REAL by XREAL_0:def 1; theorem A = [.0,PI.] implies integral(sin^2,A) = PI/2 proof assume A=[.0,PI.]; then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37; then integral(sin^2,A) =(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).pp - (AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Th13 .= AffineMap(1/2,0).(PI)-((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap (1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Lm5,VALUED_1:13 .= AffineMap(1/2,0).(PI)-((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap (1/2,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by Lm5,VALUED_1:13,Lm6 .= (1/2)*(PI)+0 -((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap(1/2,0). 0-((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4 .= (1/2)*(PI)-(1/4)*(sin*AffineMap(2,0)).pp -(AffineMap(1/2,0).0-((1/4 )(#)(sin*AffineMap(2,0))).0) by VALUED_1:6 .= (1/2)*(PI)-(1/4)*(sin.(AffineMap(2,0).(PI))) -(AffineMap(1/2,0).0-((1 /4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13 .= (1/2)*(PI)-(1/4)*(sin.(2*PI+0)) -(AffineMap(1/2,0).0-((1/4)(#)(sin* AffineMap(2,0))).0) by FCONT_1:def 4 .= (1/2)*(PI)-(1/4)*sin.(2*PI+0) -(0-((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:48 .= (1/2)*(PI)-(1/4)*sin.(2*PI+0) -0+((1/4)(#)(sin*AffineMap(2,0))).0 .= (1/2)*(PI)-(1/4)*sin.(2*PI+0) +(1/4)*(sin*AffineMap(2,0)).0 by VALUED_1:6 .= (1/2)*(PI)-(1/4)*sin.(2*PI+0) +(1/4)*(sin.(AffineMap(2,0).0)) by Lm4, FUNCT_1:13,Lm6 .= (1/2)*(PI)-(1/4)*sin.(0+2*PI*1)+(1/4)*sin.0 by FCONT_1:48 .= (1/2)*(PI)-(1/4)*sin.0+(1/4)*sin.0 by SIN_COS6:8 .= PI/2; hence thesis; end; reconsider dp = 2*PI, ddp = 2*(2*PI)+0 as Element of REAL by XREAL_0:def 1; theorem A = [.0,2*PI.] implies integral(sin^2,A) = PI proof assume A=[.0,2*PI.]; then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37; then integral(sin^2,A) =(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).dp -(AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Th13 .= AffineMap(1/2,0).(2*PI)-((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -( AffineMap(1/2,0)-(1/4)(#)(sin*AffineMap(2,0))).0 by Lm5,VALUED_1:13 .= AffineMap(1/2,0).(2*PI)-((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -( AffineMap(1/2,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by Lm5,VALUED_1:13,Lm6 .= (1/2)*(2*PI)+0 -((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(AffineMap(1/2 ,0).0-((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4 .= (1/2)*(2*PI)-(1/4)*(sin*AffineMap(2,0)).(2*PI) -(AffineMap(1/2,0).0-( (1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:6 .= (1/2)*(2*PI)-(1/4)*(sin.(AffineMap(2,0).dp)) -(AffineMap(1/2,0).0 -((1/4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13 .= (1/2)*(2*PI)-(1/4)*(sin.ddp) -(AffineMap(1/2,0).0-((1/4)(#)( sin*AffineMap(2,0))).0) by FCONT_1:def 4 .= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) -(0-((1/4)(#)(sin*AffineMap(2,0))). 0) by FCONT_1:48 .= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) -0+((1/4)(#)(sin*AffineMap(2,0))).0 .= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) +(1/4)*(sin*AffineMap(2,0)).0 by VALUED_1:6 .= (1/2)*(2*PI)-(1/4)*sin.(2*2*PI+0) +(1/4)*(sin.(AffineMap(2,0).0)) by Lm4,Lm6 ,FUNCT_1:13 .= (1/2)*(2*PI)-(1/4)*sin.(0+2*PI*2)+(1/4)*sin.0 by FCONT_1:48 .= (1/2)*(2*PI)-(1/4)*sin.0+(1/4)*sin.0 by SIN_COS6:8 .= PI; hence thesis; end; :: f.x = (cos.x)^2 theorem Th16: integral(cos^2,A) = (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0 ))).(upper_bound A) -(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))). (lower_bound A) proof A1: for x being Element of REAL st x in dom ((AffineMap(1/2,0) +(1/4)(#)(sin*AffineMap(2,0)))`| REAL) holds ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (cos^2) .x proof let x be Element of REAL; assume x in dom ((AffineMap(1/2,0) +(1/4)(#)(sin*AffineMap(2,0)))`|REAL); ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL).x = (cos.x)^2 by Th2 .= (cos^2).x by VALUED_1:11; hence thesis; end; A2: dom (cos^2)=REAL by SIN_COS:24,VALUED_1:11; then dom ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = dom (cos^2 ) by Th2,FDIFF_1:def 7; then A3: ((AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0)))`|REAL) = cos^2 by A1, PARTFUN1:5; (cos^2)|A is bounded by A2,INTEGRA5:10; hence thesis by A2,A3,Th2,INTEGRA5:11,13; end; theorem A = [.0,PI.] implies integral(cos^2,A) = PI/2 proof assume A=[.0,PI.]; then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37; then integral(cos^2,A)=(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).(PI) - (AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by Th16 .= AffineMap(1/2,0).(PI)+((1/4)(#)(sin*AffineMap(2,0))).pp -(AffineMap (1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by VALUED_1:1 .= AffineMap(1/2,0).(PI)+((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap (1/2,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:1,Lm6 .= (1/2)*(PI)+0 +((1/4)(#)(sin*AffineMap(2,0))).(PI) -(AffineMap(1/2,0). 0+((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4 .= (1/2)*(PI)+(1/4)*(sin*AffineMap(2,0)).(PI) -(AffineMap(1/2,0).0+((1/4 )(#)(sin*AffineMap(2,0))).0) by VALUED_1:6 .= (1/2)*(PI)+(1/4)*(sin.(AffineMap(2,0).pp)) -(AffineMap(1/2,0).0+((1 /4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13 .= (1/2)*(PI)+(1/4)*(sin.(2*PI+0)) -(AffineMap(1/2,0).0+((1/4)(#)(sin* AffineMap(2,0))).0) by FCONT_1:def 4 .= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(0+((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:48 .= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(1/4)*(sin*AffineMap(2,0)).0 by VALUED_1:6 .= (1/2)*(PI)+(1/4)*sin.(2*PI+0) -(1/4)*(sin.(AffineMap(2,0).0)) by Lm4, FUNCT_1:13,Lm6 .= (1/2)*(PI)+(1/4)*sin.(0+2*PI*1)-(1/4)*sin.0 by FCONT_1:48 .= (1/2)*(PI)+(1/4)*sin.0-(1/4)*sin.0 by SIN_COS6:8 .= PI/2; hence thesis; end; theorem A = [.0,2*PI.] implies integral(cos^2,A) = PI proof assume A=[.0,2*PI.]; then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37; then integral(cos^2,A)=(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).(2*PI) -(AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by Th16 .= AffineMap(1/2,0).(2*PI)+((1/4)(#)(sin*AffineMap(2,0))).dp -( AffineMap(1/2,0)+(1/4)(#)(sin*AffineMap(2,0))).0 by VALUED_1:1 .= AffineMap(1/2,0).(2*PI)+((1/4)(#)(sin*AffineMap(2,0))).(2*PI) -( AffineMap(1/2,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:1,Lm6 .= (1/2)*(2*PI)+0 +((1/4)(#)(sin*AffineMap(2,0))).dp -(AffineMap(1/2 ,0).0+((1/4)(#)(sin*AffineMap(2,0))).0) by FCONT_1:def 4 .= (1/2)*(2*PI)+(1/4)*(sin*AffineMap(2,0)).(2*PI) -(AffineMap(1/2,0).0+( (1/4)(#)(sin*AffineMap(2,0))).0) by VALUED_1:6 .= (1/2)*(2*PI)+(1/4)*(sin.(AffineMap(2,0).dp)) -(AffineMap(1/2,0).0 +((1/4)(#)(sin*AffineMap(2,0))).0) by Lm4,FUNCT_1:13 .= (1/2)*(2*PI)+(1/4)*(sin.ddp) -(AffineMap(1/2,0).0+((1/4)(#)( sin*AffineMap(2,0))).0) by FCONT_1:def 4 .= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(0+((1/4)(#)(sin*AffineMap(2,0))). 0) by FCONT_1:48 .= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(1/4)*(sin*AffineMap(2,0)).0 by VALUED_1:6 .= (1/2)*(2*PI)+(1/4)*sin.(2*2*PI+0) -(1/4)*(sin.(AffineMap(2,0).0)) by Lm4 ,FUNCT_1:13,Lm6 .= (1/2)*(2*PI)+(1/4)*sin.(0+2*PI*2)-(1/4)*sin.0 by FCONT_1:48 .= (1/2)*(2*PI)+(1/4)*sin.0-(1/4)*sin.0 by SIN_COS6:8 .= PI; hence thesis; end; :: f.x = (sin.x)^n*(cos.x) theorem Th19: integral(( #Z n*sin)(#)cos,A) = ((1/(n+1))(#)( #Z (n+1)*sin)).( upper_bound A) -((1/(n+1))(#)( #Z (n+1)*sin)).(lower_bound A) proof A1: [#]REAL = dom (( #Z n*sin)(#)cos) by FUNCT_2:def 1; A2: for x being Element of REAL st x in dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) holds (((1/(n+1) )(#)( #Z (n+1)*sin))`|REAL).x = (( #Z n*sin)(#)cos).x proof let x be Element of REAL; assume x in dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL); (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL).x =(sin.x) #Z n *cos.x by Th3 .=( #Z n).(sin.x)*cos.x by TAYLOR_1:def 1 .=(( #Zn)*sin).x*cos.x by FUNCT_1:13,SIN_COS:24 .= ((( #Z n)*sin)(#)cos).x by A1,VALUED_1:def 4; hence thesis; end; #Z n*sin is_differentiable_in x0 proof sin is_differentiable_in x0 by SIN_COS:64; hence thesis by TAYLOR_1:3; end; then dom ( #Z n*sin)=REAL & for x0 st x0 in REAL holds #Z n*sin is_differentiable_in x0 by FUNCT_2:def 1; then #Z n*sin is_differentiable_on REAL by A1,FDIFF_1:9; then A3: (( #Z n*sin)(#)cos)|REAL is continuous by A1,FDIFF_1:21,25,SIN_COS:67; then (( #Z n*sin)(#)cos)|A is continuous by FCONT_1:16; then A4: ( #Z n)*sin(#)cos is_integrable_on A by A1,INTEGRA5:11; (1/(n+1))(#)( #Z (n+1)*sin) is_differentiable_on REAL by Th3; then dom (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) = dom (( #Z n*sin)(#)cos) by A1,FDIFF_1:def 7; then A5: (((1/(n+1))(#)( #Z (n+1)*sin))`|REAL) = (( #Z n*sin)(#)cos) by A2, PARTFUN1:5; (( #Z n)*sin(#)cos)|A is bounded by A1,A3,INTEGRA5:10; hence thesis by A4,A5,Th3,INTEGRA5:13; end; theorem A = [.0,PI.] implies integral(( #Z n*sin)(#)cos,A) = 0 proof assume A=[.0,PI.]; then upper_bound A=PI & lower_bound A=0 by INTEGRA8:37; then integral(( #Z n*sin)(#)cos,A)=((1/(n+1))(#)( #Z (n+1)*sin)).(PI) -((1/(n +1))(#)( #Z (n+1)*sin)).0 by Th19 .= 1/(n+1)*( #Z (n+1)*sin).PI -((1/(n+1))(#)( #Z (n+1)*sin)).0 by VALUED_1:6 .= 1/(n+1)*( #Z (n+1)*sin).PI -1/(n+1)*( #Z (n+1)*sin).0 by VALUED_1:6 .= 1/(n+1)*(( #Z (n+1)).(sin.pp)) -1/(n+1)*( #Z (n+1)*sin).0 by FUNCT_1:13 ,SIN_COS:24 .= 1/(n+1)*(( #Z (n+1)).(sin.PI)) -1/(n+1)*(( #Z (n+1)).(sin.0)) by FUNCT_1:13,SIN_COS:24,Lm6 .= 0 by SIN_COS:30,76; hence thesis; end; theorem A = [.0,2*PI.] implies integral(( #Z n*sin)(#)cos,A) = 0 proof assume A=[.0,2*PI.]; then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37; then integral(( #Z n*sin)(#)cos,A)=((1/(n+1))(#)( #Z (n+1)*sin)).(2*PI) -((1/ (n+1))(#)( #Z (n+1)*sin)).0 by Th19 .= 1/(n+1)*( #Z (n+1)*sin).(2*PI) -((1/(n+1))(#)( #Z (n+1)*sin)).0 by VALUED_1:6 .= 1/(n+1)*( #Z (n+1)*sin).dp -1/(n+1)*( #Z (n+1)*sin).0 by VALUED_1:6 .= 1/(n+1)*(( #Z (n+1)).(sin.(2*PI))) -1/(n+1)*( #Z (n+1)*sin).0 by FUNCT_1:13,SIN_COS:24 .= 1/(n+1)*(( #Z (n+1)).(sin.(2*PI))) -1/(n+1)*(( #Z (n+1)).(sin.0)) by FUNCT_1:13,SIN_COS:24,Lm6 .= 0 by SIN_COS:30,76; hence thesis; end; :: f.x = (cos.x)^n*(sin.x) theorem Th22: integral(( #Z n*cos)(#)sin,A) = ((-1/(n+1))(#)( #Z (n+1)*cos)).( upper_bound A) -((-1/(n+1))(#)( #Z (n+1)*cos)).(lower_bound A) proof A1: [#]REAL=dom (( #Z n*cos)(#)sin) by FUNCT_2:def 1; A2: for x being Element of REAL st x in dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) holds (((-1/(n+ 1))(#)( #Z (n+1)*cos))`|REAL).x = (( #Z n*cos)(#)sin).x proof let x be Element of REAL; assume x in dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL); (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL).x =(cos.x) #Z n *sin.x by Th4 .=( #Z n).(cos.x)*sin.x by TAYLOR_1:def 1 .=(( #Zn)*cos).x*sin.x by FUNCT_1:13,SIN_COS:24 .= ((( #Z n)*cos)(#)sin).x by A1,VALUED_1:def 4; hence thesis; end; #Z n*cos is_differentiable_in x0 proof cos is_differentiable_in x0 by SIN_COS:63; hence thesis by TAYLOR_1:3; end; then dom ( #Z n*cos)=REAL & for x0 st x0 in REAL holds #Z n*cos is_differentiable_in x0 by FUNCT_2:def 1; then #Z n*cos is_differentiable_on REAL by A1,FDIFF_1:9; then A3: (( #Z n*cos)(#)sin)|REAL is continuous by A1,FDIFF_1:21,25,SIN_COS:68; then (( #Z n*cos)(#)sin)|A is continuous by FCONT_1:16; then A4: ( #Z n*cos)(#)sin is_integrable_on A by A1,INTEGRA5:11; (-1/(n+1))(#)( #Z (n+1)*cos) is_differentiable_on REAL by Th4; then dom (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) = dom (( #Z n*cos)(#)sin) by A1, FDIFF_1:def 7; then A5: (((-1/(n+1))(#)( #Z (n+1)*cos))`|REAL) = (( #Z n*cos)(#)sin) by A2, PARTFUN1:5; (( #Z n*cos)(#)sin)|A is bounded by A1,A3,INTEGRA5:10; hence thesis by A4,A5,Th4,INTEGRA5:13; end; theorem A = [.0,2*PI.] implies integral(( #Z n*cos)(#)sin,A) = 0 proof assume A=[.0,2*PI.]; then upper_bound A=2*PI & lower_bound A=0 by INTEGRA8:37; then integral(( #Z n*cos)(#)sin,A)=((-1/(n+1))(#)( #Z (n+1)*cos)).(2*PI) -((- 1/(n+1))(#)( #Z (n+1)*cos)).0 by Th22 .= (-1/(n+1))*( #Z (n+1)*cos).(2*PI) -((-1/(n+1))(#)( #Z (n+1)*cos)).0 by VALUED_1:6 .= (-1/(n+1))*( #Z (n+1)*cos).(2*PI) -(-1/(n+1))*( #Z (n+1)*cos).0 by VALUED_1:6 .= (-1/(n+1))*(( #Z (n+1)).(cos.dp)) -(-1/(n+1))*( #Z (n+1)*cos).0 by FUNCT_1:13,SIN_COS:24 .= (-1/(n+1))*(( #Z (n+1)).(cos.(2*PI))) -(-1/(n+1))*(( #Z (n+1)).(cos.0 )) by FUNCT_1:13,SIN_COS:24,Lm6 .= 0 by SIN_COS:30,76; hence thesis; end; reconsider pd = PI/2, mpd = - PI/2 as Element of REAL by XREAL_0:def 1; theorem A = [.-PI/2,PI/2.] implies integral(( #Z n*cos)(#)sin,A) = 0 proof assume A=[.-PI/2,PI/2.]; then upper_bound A=PI/2 & lower_bound A=-PI/2 by INTEGRA8:37; then integral(( #Z n*cos)(#)sin,A)=((-1/(n+1))(#)( #Z (n+1)*cos)).(PI/2) -((- 1/(n+1))(#)( #Z (n+1)*cos)).(-PI/2) by Th22 .= (-1/(n+1))*( #Z (n+1)*cos).(PI/2) -((-1/(n+1))(#)( #Z (n+1)*cos)).(- PI/2) by VALUED_1:6 .= (-1/(n+1))*( #Z (n+1)*cos).(PI/2) -(-1/(n+1))*( #Z (n+1)*cos).(-PI/2) by VALUED_1:6 .= (-1/(n+1))*(( #Z (n+1)).(cos.pd)) -(-1/(n+1))*( #Z (n+1)*cos).mpd by FUNCT_1:13,SIN_COS:24 .= (-1/(n+1))*(( #Z (n+1)).(cos.pd)) -(-1/(n+1))*(( #Z (n+1)).(cos.( -PI/2))) by FUNCT_1:13,SIN_COS:24 .= (-1/(n+1))*(( #Z (n+1)).(cos.(PI/2))) -(-1/(n+1))*(( #Z (n+1)).(cos.( PI/2))) by SIN_COS:30 .= 0; hence thesis; end; :: f.x = cos.(m*x)*cos.(n*x) theorem m+n<>0 & m-n<>0 implies integral((cos*AffineMap(m,0))(#)(cos*AffineMap (n,0)),A) = ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin* AffineMap(m-n,0))).(upper_bound A) -((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n )))(#)(sin*AffineMap(m-n,0))).(lower_bound A) proof assume A1: m+n<>0 & m-n<>0; A2: for x st x in REAL holds AffineMap(n,0).x=n*x proof let x; assume x in REAL; (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4 .=n*x; hence thesis; end; A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; A4: dom (cos*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1; A5: for x st x in REAL holds AffineMap(m,0).x=m*x proof let x; assume x in REAL; (AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4 .=m*x; hence thesis; end; A6: for x being Element of REAL st x in dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n) ))(#)(sin*AffineMap(m-n,0)))`|REAL) holds (((1/(2*(m+n)))(#)(sin*AffineMap(m+n, 0))+ (1/(2*(m-n)))(#)(sin*AffineMap(m-n,0)))`|REAL).x = ((cos*AffineMap(m,0)) (#)(cos*AffineMap(n,0))).x proof let x be Element of REAL; assume x in dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)( sin*AffineMap(m-n,0)))`|REAL); (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin* AffineMap(m-n,0)))`|REAL).x = cos.(m*x)*cos.(n*x) by A1,Th5 .= cos.(AffineMap(m,0).x)*cos.(n*x) by A5 .= (cos.(AffineMap(m,0).x))*(cos.((AffineMap(n,0)).x)) by A2 .= ((cos*AffineMap(m,0)).x) *(cos.(AffineMap(n,0).x)) by A4,FUNCT_1:12 .= ((cos*AffineMap(m,0)).x)*((cos*AffineMap(n,0)).x) by A3,FUNCT_1:12 .= ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5; hence thesis; end; A7: [#]REAL = dom ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))) by FUNCT_2:def 1; ((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin*AffineMap (m-n,0))) is_differentiable_on REAL by A1,Th5; then dom (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin* AffineMap(m-n,0)))`|REAL) = dom ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))) by A7,FDIFF_1:def 7; then A8: (((1/(2*(m+n)))(#)(sin*AffineMap(m+n,0))+ (1/(2*(m-n)))(#)(sin* AffineMap(m-n,0)))`|REAL) = (cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)) by A6, PARTFUN1:5; ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is continuous; then A9: ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A7, INTEGRA5:11; ((cos*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10; hence thesis by A1,A9,A8,Th5,INTEGRA5:13; end; :: f.x = sin.(m*x)*sin.(n*x) theorem m+n<>0 & m-n<>0 implies integral((sin*AffineMap(m,0))(#)(sin*AffineMap (n,0)),A) = ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin* AffineMap(m+n,0))).(upper_bound A) -((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n )))(#)(sin*AffineMap(m+n,0))).(lower_bound A) proof assume A1: m+n<>0 & m-n<>0; A2: for x st x in REAL holds AffineMap(n,0).x=n*x proof let x; assume x in REAL; (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4 .=n*x; hence thesis; end; A3: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; A4: dom (sin*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1; A5: for x st x in REAL holds AffineMap(m,0).x=m*x proof let x; assume x in REAL; (AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4 .=m*x; hence thesis; end; A6: for x being Element of REAL st x in dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n) ))(#)(sin*AffineMap(m+n,0)))`|REAL) holds (((1/(2*(m-n)))(#)(sin*AffineMap(m-n, 0))- (1/(2*(m+n)))(#)(sin*AffineMap(m+n,0)))`|REAL).x = ((sin*AffineMap(m,0)) (#)(sin*AffineMap(n,0))).x proof let x be Element of REAL; assume x in dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)( sin*AffineMap(m+n,0)))`|REAL); (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin* AffineMap(m+n,0)))`|REAL).x = sin.(m*x)*sin.(n*x) by A1,Th6 .= sin.(AffineMap(m,0).x)*sin.(n*x) by A5 .= (sin.(AffineMap(m,0).x))*(sin.(AffineMap(n,0).x)) by A2 .= ((sin*(AffineMap(m,0))).x) *(sin.(AffineMap(n,0).x)) by A4,FUNCT_1:12 .= ((sin*AffineMap(m,0)).x)*((sin*AffineMap(n,0)).x) by A3,FUNCT_1:12 .= ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))).x by VALUED_1:5; hence thesis; end; A7: REAL=dom ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))) by FUNCT_2:def 1; ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)))|A is continuous; then A8: ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))) is_integrable_on A by A7, INTEGRA5:11; ((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin*AffineMap (m+n,0))) is_differentiable_on REAL by A1,Th6; then dom (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin* AffineMap(m+n,0)))`|REAL) = dom ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0))) by A7,FDIFF_1:def 7; then A9: (((1/(2*(m-n)))(#)(sin*AffineMap(m-n,0))- (1/(2*(m+n)))(#)(sin* AffineMap(m+n,0)))`|REAL) = (sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)) by A6, PARTFUN1:5; ((sin*AffineMap(m,0))(#)(sin*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10; hence thesis by A1,A8,A9,Th6,INTEGRA5:13; end; :: f.x = sin.(m*x)*cos.(n*x) theorem m+n<>0 & m-n<>0 implies integral((sin*AffineMap(m,0))(#)(cos*AffineMap (n,0)),A) = ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos* AffineMap(m-n,0))).(upper_bound A) -((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0))) - (1/(2*( m-n)))(#)(cos*AffineMap(m-n,0))).(lower_bound A) proof assume A1: m+n<>0 & m-n<>0; A2: for x st x in REAL holds AffineMap(n,0).x=n*x proof let x; assume x in REAL; (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4 .=n*x; hence thesis; end; A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; A4: dom (sin*AffineMap(m,0)) = [#]REAL by FUNCT_2:def 1; A5: for x st x in REAL holds AffineMap(m,0).x=m*x proof let x; assume x in REAL; (AffineMap(m,0)).x = m*x + 0 by FCONT_1:def 4 .=m*x; hence thesis; end; A6: for x being Element of REAL st x in dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m -n)))(#)(cos*AffineMap(m-n,0)))`|REAL) holds (((-(1/(2*(m+n)))(#)(cos*AffineMap (m+n,0)))- (1/(2*(m-n)))(#)(cos*AffineMap(m-n,0)))`|REAL).x = ((sin*AffineMap(m ,0))(#)(cos*AffineMap(n,0))).x proof let x be Element of REAL; assume x in dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#) (cos*AffineMap(m-n,0)))`|REAL); (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos* AffineMap(m-n,0)))`|REAL).x = sin.(m*x)*cos.(n*x) by A1,Th7 .= sin.(AffineMap(m,0).x)*cos.(n*x) by A5 .= (sin.(AffineMap(m,0).x))*(cos.(AffineMap(n,0).x)) by A2 .= ((sin*AffineMap(m,0)).x)*(cos.(AffineMap(n,0).x)) by A4,FUNCT_1:12 .= ((sin*AffineMap(m,0)).x)*((cos*AffineMap(n,0)).x) by A3,FUNCT_1:12 .= ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5; hence thesis; end; A7: [#]REAL=dom ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))) by FUNCT_2:def 1; ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is continuous; then A8: ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A7, INTEGRA5:11; ((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos* AffineMap(m-n,0))) is_differentiable_on REAL by A1,Th7; then dom (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos* AffineMap(m-n,0)))`|REAL) = dom ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0))) by A7,FDIFF_1:def 7; then A9: (((-(1/(2*(m+n)))(#)(cos*AffineMap(m+n,0)))- (1/(2*(m-n)))(#)(cos* AffineMap(m-n,0)))`|REAL) = (sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)) by A6, PARTFUN1:5; ((sin*AffineMap(m,0))(#)(cos*AffineMap(n,0)))|A is bounded by A7,INTEGRA5:10; hence thesis by A1,A8,A9,Th7,INTEGRA5:13; end; :: f.x = x*sin.(n*x) theorem n<>0 implies integral((AffineMap(1,0))(#)(sin*AffineMap(n,0)),A) = ((1 /(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0))). (upper_bound A) -((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap(n,0) )).(lower_bound A) proof assume A1: n<>0; A2: for x st x in REAL holds AffineMap(n,0).x=n*x proof let x; assume x in REAL; (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4 .=n*x; hence thesis; end; A3: dom (sin*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; A4: for x st x in REAL holds AffineMap(1,0).x=x proof let x; assume x in REAL; (AffineMap(1,0)).x = 1*x + 0 by FCONT_1:def 4 .=x; hence thesis; end; A5: for x being Element of REAL st x in dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0)) (#)(cos*AffineMap(n,0)))`|REAL) holds (((1/(n^2))(#)(sin*AffineMap(n,0))- ( AffineMap(1/n,0))(#)(cos*AffineMap(n,0)))`|REAL).x = ((AffineMap(1,0))(#)(sin* AffineMap(n,0))).x proof let x be Element of REAL; assume x in dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos *AffineMap(n,0)))`|REAL); (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos* AffineMap(n,0)))`|REAL).x = x*sin.(n*x) by A1,Th8 .= x*(sin.(AffineMap(n,0).x)) by A2 .= x*(sin*AffineMap(n,0)).x by A3,FUNCT_1:12 .= (AffineMap(1,0).x)*(sin*AffineMap(n,0)).x by A4 .= ((AffineMap(1,0))(#)(sin*AffineMap(n,0))).x by VALUED_1:5; hence thesis; end; A6: dom ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) = [#]REAL by FUNCT_2:def 1; ((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap( n,0))) is_differentiable_on REAL by A1,Th8; then dom (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos* AffineMap(n,0)))`|REAL) = dom ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) by A6, FDIFF_1:def 7; then A7: (((1/(n^2))(#)(sin*AffineMap(n,0))- (AffineMap(1/n,0))(#)(cos*AffineMap (n,0)))`|REAL) = (AffineMap(1,0))(#)(sin*AffineMap(n,0)) by A5,PARTFUN1:5; ((AffineMap(1,0))(#)(sin*AffineMap(n,0)))|A is continuous; then A8: ((AffineMap(1,0))(#)(sin*AffineMap(n,0))) is_integrable_on A by A6, INTEGRA5:11; ((AffineMap(1,0))(#)(sin*AffineMap(n,0)))|A is bounded by A6,INTEGRA5:10; hence thesis by A1,A8,A7,Th8,INTEGRA5:13; end; :: f.x = x*cos.(n*x) theorem n<>0 implies integral((AffineMap(1,0))(#)(cos*AffineMap(n,0)),A) = ((1 /(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0))). (upper_bound A) -((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap(n,0) )).(lower_bound A) proof assume A1: n<>0; A2: for x st x in REAL holds AffineMap(n,0).x=n*x proof let x; assume x in REAL; (AffineMap(n,0)).x = n*x + 0 by FCONT_1:def 4 .=n*x; hence thesis; end; A3: dom (cos*AffineMap(n,0)) = [#]REAL by FUNCT_2:def 1; A4: for x st x in REAL holds AffineMap(1,0).x=x proof let x; assume x in REAL; (AffineMap(1,0)).x = 1*x + 0 by FCONT_1:def 4 .=x; hence thesis; end; A5: for x being Element of REAL st x in dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0)) (#)(sin*AffineMap(n,0)))`|REAL) holds (((1/(n^2))(#)(cos*AffineMap(n,0))+ ( AffineMap(1/n,0))(#)(sin*AffineMap(n,0)))`|REAL).x = ((AffineMap(1,0))(#)(cos* AffineMap(n,0))).x proof let x be Element of REAL; assume x in dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin *AffineMap(n,0)))`|REAL); (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin* AffineMap(n,0)))`|REAL).x = x*cos.(n*x) by A1,Th9 .= x*(cos.(AffineMap(n,0).x)) by A2 .= x*(cos*AffineMap(n,0)).x by A3,FUNCT_1:12 .= (AffineMap(1,0).x)*(cos*AffineMap(n,0)).x by A4 .= ((AffineMap(1,0))(#)(cos*AffineMap(n,0))).x by VALUED_1:5; hence thesis; end; A6: dom ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) = [#]REAL by FUNCT_2:def 1; ((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap( n,0))) is_differentiable_on REAL by A1,Th9; then dom (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin* AffineMap(n,0)))`|REAL) = dom ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) by A6, FDIFF_1:def 7; then A7: (((1/(n^2))(#)(cos*AffineMap(n,0))+ (AffineMap(1/n,0))(#)(sin*AffineMap (n,0)))`|REAL) = (AffineMap(1,0))(#)(cos*AffineMap(n,0)) by A5,PARTFUN1:5; ((AffineMap(1,0))(#)(cos*AffineMap(n,0)))|A is continuous; then A8: ((AffineMap(1,0))(#)(cos*AffineMap(n,0))) is_integrable_on A by A6, INTEGRA5:11; ((AffineMap(1,0))(#)(cos*AffineMap(n,0)))|A is bounded by A6,INTEGRA5:10; hence thesis by A1,A8,A7,Th9,INTEGRA5:13; end; theorem integral((AffineMap(1,0))(#)sinh,A) = ((AffineMap(1,0))(#)cosh-sinh).( upper_bound A) -((AffineMap(1,0))(#)cosh-sinh).(lower_bound A) proof A1: for x being Element of REAL st x in dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL) holds ((( AffineMap(1,0))(#)cosh-sinh)`|REAL).x = ((AffineMap(1,0))(#)sinh).x proof let x be Element of REAL; assume x in dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL); (((AffineMap(1,0))(#)cosh-sinh)`|REAL).x = (1*x+0)*sinh.x by Th10 .= ((AffineMap(1,0)).x)*sinh.x by FCONT_1:def 4 .= ((AffineMap(1,0))(#)sinh).x by VALUED_1:5; hence thesis; end; A2: dom ((AffineMap(1,0))(#)sinh) = [#]REAL by FUNCT_2:def 1; then dom (((AffineMap(1,0))(#)cosh-sinh)`|REAL) = dom ((AffineMap(1,0))(#) sinh) by Th10,FDIFF_1:def 7; then A3: (((AffineMap(1,0))(#)cosh-sinh)`|REAL) = (AffineMap(1,0))(#)sinh by A1, PARTFUN1:5; dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0) .x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23; then A4: ((AffineMap(1,0))(#)sinh)|REAL is continuous by A2,FDIFF_1:21,25 ,SIN_COS2:34; then A5: ((AffineMap(1,0))(#)sinh)|A is continuous by FCONT_1:16; ((AffineMap(1,0))(#)sinh)|A is bounded by A2,A4,INTEGRA5:10; hence thesis by A2,A5,A3,Th10,INTEGRA5:11,13; end; theorem integral((AffineMap(1,0))(#)cosh,A) = ((AffineMap(1,0))(#)sinh-cosh).( upper_bound A) -((AffineMap(1,0))(#)sinh-cosh).(lower_bound A) proof A1: for x being Element of REAL st x in dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL) holds ((( AffineMap(1,0))(#)sinh-cosh)`|REAL).x = ((AffineMap(1,0))(#)cosh).x proof let x be Element of REAL; assume x in dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL); (((AffineMap(1,0))(#)sinh-cosh)`|REAL).x = (1*x+0)*cosh.x by Th11 .= ((AffineMap(1,0)).x)*(cosh.x) by FCONT_1:def 4 .= ((AffineMap(1,0))(#)cosh).x by VALUED_1:5; hence thesis; end; A2: dom ((AffineMap(1,0))(#)cosh) = [#]REAL by FUNCT_2:def 1; then dom (((AffineMap(1,0))(#)sinh-cosh)`|REAL) = dom ((AffineMap(1,0))(#) cosh) by Th11,FDIFF_1:def 7; then A3: (((AffineMap(1,0))(#)sinh-cosh)`|REAL) = (AffineMap(1,0))(#)cosh by A1, PARTFUN1:5; dom (AffineMap(1,0)) = [#]REAL & for x st x in REAL holds AffineMap(1,0) .x=1 *x + 0 by FCONT_1:def 4,FUNCT_2:def 1; then AffineMap(1,0) is_differentiable_on REAL by FDIFF_1:23; then A4: ((AffineMap(1,0))(#)cosh)|REAL is continuous by A2,FDIFF_1:21,25 ,SIN_COS2:35; then A5: ((AffineMap(1,0))(#)cosh)|A is continuous by FCONT_1:16; ((AffineMap(1,0))(#)cosh)|A is bounded by A2,A4,INTEGRA5:10; hence thesis by A2,A5,A3,Th11,INTEGRA5:11,13; end; :: f.x = (a*x+b)^n theorem a*(n+1) <> 0 implies integral( #Z n*AffineMap(a,b),A) = ((1/(a*(n+1))) (#)( #Z (n+1)*AffineMap(a,b))).(upper_bound A) - ((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a ,b))).(lower_bound A) proof assume A1: a*(n+1) <> 0; A2: [#]REAL=dom (AffineMap(a,b)) by FUNCT_2:def 1; A3: for x being Element of REAL st x in dom (((1/(a*(n+1))) (#)( #Z (n+1)*AffineMap(a,b)))`|REAL) holds (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x = ( #Z n*AffineMap (a,b)).x proof let x be Element of REAL; assume x in dom (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL); (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL).x =(a*x+b) #Z n by A1,Th12 .= (AffineMap(a,b).x) #Z n by FCONT_1:def 4 .= ( #Z n).(AffineMap(a,b).x) by TAYLOR_1:def 1 .=( #Z n*AffineMap(a,b)).x by A2,FUNCT_1:13; hence thesis; end; A4: [#]REAL=dom ( #Z n*AffineMap(a,b)) by FUNCT_2:def 1; for x st x in REAL holds AffineMap(a,b).x=a*x + b by FCONT_1:def 4; then A5: AffineMap(a,b) is_differentiable_on REAL by A2,FDIFF_1:23; #Z n*AffineMap(a,b) is_differentiable_in x proof x in REAL by XREAL_0:def 1; then AffineMap(a,b) is_differentiable_in x by A2,A5,FDIFF_1:9; hence thesis by TAYLOR_1:3; end; then for x st x in REAL holds #Z n*AffineMap(a,b) is_differentiable_in x; then #Z n*AffineMap(a,b) is_differentiable_on REAL by A4,FDIFF_1:9; then A6: ( #Z n*AffineMap(a,b))|REAL is continuous by FDIFF_1:25; then ( #Z n*AffineMap(a,b))|A is continuous by FCONT_1:16; then A7: #Z n*AffineMap(a,b) is_integrable_on A by A4,INTEGRA5:11; (1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)) is_differentiable_on REAL by A1 ,Th12; then dom (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL) = dom ( #Z n* AffineMap(a,b)) by A4,FDIFF_1:def 7; then A8: (((1/(a*(n+1)))(#)( #Z (n+1)*AffineMap(a,b)))`|REAL) = #Z n*AffineMap(a ,b) by A3,PARTFUN1:5; ( #Z n*AffineMap(a,b))|A is bounded by A4,A6,INTEGRA5:10; hence thesis by A1,A7,A8,Th12,INTEGRA5:13; end; begin :: Addenda reserve f, f1, f2, f3 for PartFunc of REAL, REAL; :: f.x = (1/2)*x^2 theorem Th33: Z c= dom ((1/2)(#)f) & f=#Z 2 implies (1/2)(#)f is_differentiable_on Z & for x st x in Z holds (((1/2)(#)f)`|Z).x = x proof assume that A1: Z c= dom ((1/2)(#)f) and A2: f=#Z 2; Z c= dom f & for x st x in Z holds f is_differentiable_in x by A1,A2, TAYLOR_1:2,VALUED_1:def 5; then A3: f is_differentiable_on Z by FDIFF_1:9; A4: for x st x in Z holds (f`|Z).x=2*x proof let x; 2 * (x #Z (2-1)) = 2 * x by PREPOWER:35; then A5: diff(f,x) = 2 * x by A2,TAYLOR_1:2; assume x in Z; hence thesis by A3,A5,FDIFF_1:def 7; end; for x st x in Z holds (((1/2)(#)f)`|Z).x=x proof let x; assume A6: x in Z; then (((1/2)(#)f)`|Z).x=(1/2)*diff(f,x) by A1,A3,FDIFF_1:20 .=(1/2)*(f`|Z).x by A3,A6,FDIFF_1:def 7 .=(1/2)*(2*x) by A4,A6 .=x; hence thesis; end; hence thesis by A1,A3,FDIFF_1:20; end; :: f.x = x theorem A c= Z & f=#Z 2 & Z = dom ((1/2)(#)f) implies integral(id Z,A) = ((1/2 )(#)f).(upper_bound A)-((1/2)(#)f).(lower_bound A) proof assume that A1: A c= Z and A2: f=#Z 2 & Z = dom ((1/2)(#)f); A3: A c= dom id Z by A1; then A4: (id Z)|A is bounded by INTEGRA5:10; A5: ((1/2)(#)f) is_differentiable_on Z by A2,Th33; A6: for x being Element of REAL st x in dom (((1/2)(#)f)`|Z) holds (((1/2)(#)f)`|Z).x = (id Z).x proof let x be Element of REAL; assume x in dom (((1/2)(#)f)`|Z); then A7: x in Z by A5,FDIFF_1:def 7; then (((1/2)(#)f)`|Z).x = x by A2,Th33 .= (id Z).x by A7,FUNCT_1:18; hence thesis; end; dom (((1/2)(#)f)`|Z) = dom (id Z) by A5,FDIFF_1:def 7; then A8: (((1/2)(#)f)`|Z) = id Z by A6,PARTFUN1:5; (id Z)|A is continuous; then id Z is_integrable_on A by A3,INTEGRA5:11; hence thesis by A1,A2,A4,A8,Th33,INTEGRA5:13; end; :: f.x = -1/x^2 :: INTEGRA9 theorem not 0 in Z & A c= Z & (for x st x in Z holds x<>0 & f.x = -1/x^2) & dom f = Z & f|A is continuous implies integral(f,A) = ((id Z)^).(upper_bound A)-((id Z) ^).(lower_bound A) proof set g = id Z; assume that A1: not 0 in Z and A2: A c= Z and A3: for x st x in Z holds x<>0 & f.x = -1/x^2 and A4: dom f = Z and A5: f|A is continuous; A6: f is_integrable_on A by A2,A4,A5,INTEGRA5:11; A7: g^ is_differentiable_on Z by A1,FDIFF_5:4; A8: for x being Element of REAL st x in dom ((g^)`|Z) holds ((g^)`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((g^)`|Z); then A9: x in Z by A7,FDIFF_1:def 7; then ((g^)`|Z).x = -1/x^2 by A1,FDIFF_5:4 .= f.x by A3,A9; hence thesis; end; dom ((g^)`|Z) = dom f by A4,A7,FDIFF_1:def 7; then ((g^)`|Z) = f by A8,PARTFUN1:5; hence thesis by A2,A4,A5,A6,A7,INTEGRA5:10,13; end; :: f.x = 2*x/(1+x^2)^2 theorem A c= Z & f1=#Z 2 & (for x st x in Z holds f2.x=1 & x<>0 & f.x=2*x/(1+x ^2)^2) & dom (f1/(f2+f1))=Z & Z = dom f & f|A is continuous implies integral(f, A) = (f1/(f2+f1)).(upper_bound A)-(f1/(f2+f1)).(lower_bound A) proof assume that A1: A c= Z and A2: f1=#Z 2 and A3: for x st x in Z holds f2.x=1 & x<>0 & f.x=2*x/(1+x^2)^2 and A4: dom (f1/(f2+f1))=Z and A5: Z = dom f and A6: f|A is continuous; A7: f is_integrable_on A by A1,A5,A6,INTEGRA5:11; A8: for x st x in Z holds f2.x=1 & x<>0 by A3; then A9: (f1/(f2+f1)) is_differentiable_on Z by A2,A4,FDIFF_6:7; A10: for x being Element of REAL st x in dom ((f1/(f2+f1))`|Z) holds ((f1/(f2+f1))`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((f1/(f2+f1))`|Z); then A11: x in Z by A9,FDIFF_1:def 7; then ((f1/(f2+f1))`|Z).x = 2*x/(1+x^2)^2 by A2,A4,A8,FDIFF_6:7 .= f.x by A3,A11; hence thesis; end; dom ((f1/(f2+f1))`|Z) = dom f by A5,A9,FDIFF_1:def 7; then ((f1/(f2+f1))`|Z) = f by A10,PARTFUN1:5; hence thesis by A1,A5,A6,A7,A9,INTEGRA5:10,13; end; theorem Th37: (Z c= dom (tan+sec) & for x st x in Z holds (1+sin.x)<>0 & (1- sin.x)<>0) implies tan+sec is_differentiable_on Z & for x st x in Z holds ((tan +sec)`|Z).x = 1/(1-sin.x) proof assume that A1: Z c= dom (tan+sec) and A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0; Z c= dom tan /\ dom (cos^) by A1,VALUED_1:def 1; then A3: Z c= dom tan by XBOOLE_1:18; then A4: for x st x in Z holds cos.x<>0 by FDIFF_8:1; then A5: cos^ is_differentiable_on Z by FDIFF_4:39; for x st x in Z holds tan is_differentiable_in x proof let x; assume x in Z; then cos.x<>0 by A3,FDIFF_8:1; hence thesis by FDIFF_7:46; end; then A6: tan is_differentiable_on Z by A3,FDIFF_1:9; for x st x in Z holds ((tan+sec)`|Z).x = 1/(1-sin.x) proof let x; assume A7: x in Z; then A8: cos.x<>0 by A3,FDIFF_8:1; A9: 1+sin.x<>0 by A2,A7; ((tan+sec)`|Z).x = diff(tan,x) + diff(cos^,x) by A1,A5,A6,A7,FDIFF_1:18 .=1/(cos.x)^2 + diff(cos^,x) by A8,FDIFF_7:46 .=1/(cos.x)^2 + ((cos^)`|Z).x by A5,A7,FDIFF_1:def 7 .=1/(cos.x)^2 + sin.x/(cos.x)^2 by A4,A7,FDIFF_4:39 .=(1+sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2) by XCMPLX_1:62 .=(1+sin.x)/(1-(sin.x)^2) by SIN_COS:28 .=(1+sin.x)/((1+sin.x)*(1-sin.x)) .=(1+sin.x)/(1+sin.x)/(1-sin.x) by XCMPLX_1:78 .=1/(1-sin.x) by A9,XCMPLX_1:60; hence thesis; end; hence thesis by A1,A5,A6,FDIFF_1:18; end; :: f.x = 1/(1-sin.x) theorem A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/ (1-sin.x)) & dom (tan+sec)=Z & Z = dom f & f|A is continuous implies integral(f ,A) = (tan+sec).(upper_bound A)-(tan+sec).(lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/(1-sin. x) and A3: dom (tan+sec)=Z and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2; then A8: (tan+sec) is_differentiable_on Z by A3,Th37; A9: 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 A10: x in Z by A8,FDIFF_1:def 7; then ((tan+sec)`|Z).x = 1/(1-sin.x) by A3,A7,Th37 .= f.x by A2,A10; hence thesis; end; dom ((tan+sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7; then ((tan+sec)`|Z) = f by A9,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13; end; theorem Th39: (Z c= dom (tan-sec) & for x st x in Z holds (1+sin.x)<>0 & (1- sin.x)<>0) implies tan-sec is_differentiable_on Z & for x st x in Z holds ((tan -sec)`|Z).x = 1/(1+sin.x) proof assume that A1: Z c= dom (tan-sec) and A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0; Z c= dom tan /\ dom (cos^) by A1,VALUED_1:12; then A3: Z c= dom tan by XBOOLE_1:18; then A4: for x st x in Z holds cos.x<>0 by FDIFF_8:1; then A5: cos^ is_differentiable_on Z by FDIFF_4:39; for x st x in Z holds tan is_differentiable_in x proof let x; assume x in Z; then cos.x<>0 by A3,FDIFF_8:1; hence thesis by FDIFF_7:46; end; then A6: tan is_differentiable_on Z by A3,FDIFF_1:9; for x st x in Z holds ((tan-sec)`|Z).x = 1/(1+sin.x) proof let x; assume A7: x in Z; then A8: cos.x<>0 by A3,FDIFF_8:1; A9: 1-sin.x<>0 by A2,A7; ((tan-sec)`|Z).x = diff(tan,x) - diff(cos^,x) by A1,A5,A6,A7,FDIFF_1:19 .=1/(cos.x)^2 - diff(cos^,x) by A8,FDIFF_7:46 .=1/(cos.x)^2 - ((cos^)`|Z).x by A5,A7,FDIFF_1:def 7 .=1/(cos.x)^2 - sin.x/(cos.x)^2 by A4,A7,FDIFF_4:39 .=(1-sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2) by XCMPLX_1:120 .=(1-sin.x)/(1-(sin.x)^2) by SIN_COS:28 .=(1-sin.x)/((1+sin.x)*(1-sin.x)) .=(1-sin.x)/(1-sin.x)/(1+sin.x) by XCMPLX_1:78 .=1/(1+sin.x) by A9,XCMPLX_1:60; hence thesis; end; hence thesis by A1,A5,A6,FDIFF_1:19; end; :: f.x = 1/(1+sin.x) theorem A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/ (1+sin.x)) & dom (tan-sec)=Z & Z = dom f & f|A is continuous implies integral(f ,A) = (tan-sec).(upper_bound A)-(tan-sec).(lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = 1/(1+sin. x) and A3: dom (tan-sec)=Z and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2; then A8: (tan-sec) is_differentiable_on Z by A3,Th39; A9: 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 A10: x in Z by A8,FDIFF_1:def 7; then ((tan-sec)`|Z).x = 1/(1+sin.x) by A3,A7,Th39 .= f.x by A2,A10; hence thesis; end; dom ((tan-sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7; then ((tan-sec)`|Z) = f by A9,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13; end; theorem Th41: (Z c= dom (-cot+cosec) & for x st x in Z holds (1+cos.x)<>0 & (1 -cos.x)<>0) implies -cot+cosec is_differentiable_on Z & for x st x in Z holds ( (-cot+cosec)`|Z).x = 1/(1+cos.x) proof assume that A1: Z c= dom (-cot+cosec) and A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0; Z c= dom (-cot) /\ dom (sin^) by A1,VALUED_1:def 1; then A3: Z c= dom (-cot) by XBOOLE_1:18; then A4: Z c= dom cot by VALUED_1:8; for x st x in Z holds cot is_differentiable_in x proof let x; assume x in Z; then sin.x<>0 by A4,FDIFF_8:2; hence thesis by FDIFF_7:47; end; then A5: cot is_differentiable_on Z by A4,FDIFF_1:9; then A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20; A7: for x st x in Z holds sin.x<>0 by A4,FDIFF_8:2; then A8: sin^ is_differentiable_on Z by FDIFF_4:40; for x st x in Z holds ((-cot+cosec)`|Z).x = 1/(1+cos.x) proof let x; assume A9: x in Z; then A10: sin.x<>0 by A4,FDIFF_8:2; A11: 1-cos.x<>0 by A2,A9; ((-cot+cosec)`|Z).x = diff(-cot,x) + diff(sin^,x) by A1,A8,A6,A9,FDIFF_1:18 .=(((-1)(#)cot)`|Z).x + diff(sin^,x) by A6,A9,FDIFF_1:def 7 .=(-1)*diff(cot,x) + diff(sin^,x) by A3,A5,A9,FDIFF_1:20 .=(-1)*(-1/(sin.x)^2)+ diff(sin^,x) by A10,FDIFF_7:47 .=1/(sin.x)^2 + ((sin^)`|Z).x by A8,A9,FDIFF_1:def 7 .=1/(sin.x)^2 + (-cos.x/(sin.x)^2) by A7,A9,FDIFF_4:40 .=1/(sin.x)^2 - cos.x/(sin.x)^2 .=(1-cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2) by XCMPLX_1:120 .=(1-cos.x)/(1-(cos.x)^2) by SIN_COS:28 .=(1-cos.x)/((1-cos.x)*(1+cos.x)) .=(1-cos.x)/(1-cos.x)/(1+cos.x) by XCMPLX_1:78 .=1/(1+cos.x) by A11,XCMPLX_1:60; hence thesis; end; hence thesis by A1,A8,A6,FDIFF_1:18; end; :: f.x = 1/(1+cos.x) theorem A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/ (1+cos.x)) & dom (-cot+cosec)=Z & Z = dom f & f|A is continuous implies integral(f,A) = (-cot+cosec).(upper_bound A)-(-cot+cosec).(lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/(1+cos. x) and A3: dom (-cot+cosec)=Z and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2; then A8: (-cot+cosec) is_differentiable_on Z by A3,Th41; A9: 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 A10: x in Z by A8,FDIFF_1:def 7; then ((-cot+cosec)`|Z).x = 1/(1+cos.x) by A3,A7,Th41 .= f.x by A2,A10; hence thesis; end; dom ((-cot+cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7; then ((-cot+cosec)`|Z) = f by A9,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13; end; theorem Th43: (Z c= dom (-cot-cosec) & for x st x in Z holds (1+cos.x)<>0 & (1 -cos.x)<>0) implies -cot-cosec is_differentiable_on Z & for x st x in Z holds ( (-cot-cosec)`|Z).x = 1/(1-cos.x) proof assume that A1: Z c= dom (-cot-cosec) and A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0; Z c= dom (-cot) /\ dom (sin^) by A1,VALUED_1:12; then A3: Z c= dom (-cot) by XBOOLE_1:18; then A4: Z c= dom cot by VALUED_1:8; for x st x in Z holds cot is_differentiable_in x proof let x; assume x in Z; then sin.x<>0 by A4,FDIFF_8:2; hence thesis by FDIFF_7:47; end; then A5: cot is_differentiable_on Z by A4,FDIFF_1:9; then A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20; A7: for x st x in Z holds sin.x<>0 by A4,FDIFF_8:2; then A8: sin^ is_differentiable_on Z by FDIFF_4:40; for x st x in Z holds ((-cot-cosec)`|Z).x = 1/(1-cos.x) proof let x; assume A9: x in Z; then A10: sin.x<>0 by A4,FDIFF_8:2; A11: 1+cos.x<>0 by A2,A9; ((-cot-cosec)`|Z).x = diff(-cot,x) - diff(sin^,x) by A1,A8,A6,A9,FDIFF_1:19 .=(((-1)(#)cot)`|Z).x - diff(sin^,x) by A6,A9,FDIFF_1:def 7 .=(-1)*diff(cot,x) - diff(sin^,x) by A3,A5,A9,FDIFF_1:20 .=(-1)*(-1/(sin.x)^2)- diff(sin^,x) by A10,FDIFF_7:47 .=1/(sin.x)^2 - ((sin^)`|Z).x by A8,A9,FDIFF_1:def 7 .=1/(sin.x)^2 - (-cos.x/(sin.x)^2) by A7,A9,FDIFF_4:40 .=1/(sin.x)^2 + cos.x/(sin.x)^2 .=(1+cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2) by XCMPLX_1:62 .=(1+cos.x)/(1-(cos.x)^2) by SIN_COS:28 .=(1+cos.x)/((1+cos.x)*(1-cos.x)) .=(1+cos.x)/(1+cos.x)/(1-cos.x) by XCMPLX_1:78 .=1/(1-cos.x) by A11,XCMPLX_1:60; hence thesis; end; hence thesis by A1,A8,A6,FDIFF_1:19; end; :: f.x = 1/(1-cos.x) theorem A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/ (1-cos.x)) & dom (-cot-cosec)=Z & Z = dom f & f|A is continuous implies integral(f,A) = (-cot-cosec).(upper_bound A)-(-cot-cosec).(lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = 1/(1-cos. x) and A3: dom (-cot-cosec)=Z and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2; then A8: (-cot-cosec) is_differentiable_on Z by A3,Th43; A9: 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 A10: x in Z by A8,FDIFF_1:def 7; then ((-cot-cosec)`|Z).x = 1/(1-cos.x) by A3,A7,Th43 .= f.x by A2,A10; hence thesis; end; dom ((-cot-cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7; then ((-cot-cosec)`|Z) = f by A9,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13; end; :: f.x = 1/(1+x^2) theorem A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=1/(1+x^2)) & Z = dom f & f|A is continuous implies integral(f,A) = arctan.(upper_bound A) - arctan.(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ and A3: for x st x in Z holds f.x=1/(1+x^2) and A4: Z = dom f and A5: f|A is continuous; A6: arctan is_differentiable_on Z by A2,SIN_COS9:81; A7: for x being Element of REAL st x in dom ((arctan)`|Z) holds ((arctan)`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((arctan)`|Z); then A8: x in Z by A6,FDIFF_1:def 7; then ((arctan)`|Z).x = 1/(1+x^2) by A2,SIN_COS9:81 .= f.x by A3,A8; hence thesis; end; dom ((arctan)`|Z) = dom f by A4,A6,FDIFF_1:def 7; then A9: ((arctan)`|Z) = f by A7,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11; hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:81; end; :: f.x = r/(1+x^2) theorem A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=r/(1+x^2)) & Z = dom f & f|A is continuous implies integral(f,A) = (r(#)arctan).(upper_bound A) - (r(#) arctan).(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ and A3: for x st x in Z holds f.x=r/(1+x^2) and A4: Z = dom f and A5: f|A is continuous; A6: r(#)arctan is_differentiable_on Z by A2,SIN_COS9:83; A7: for x being Element of REAL st x in dom ((r(#)arctan)`|Z) holds ((r(#)arctan)`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((r(#)arctan)`|Z); then A8: x in Z by A6,FDIFF_1:def 7; then ((r(#)arctan)`|Z).x = r/(1+x^2) by A2,SIN_COS9:83 .= f.x by A3,A8; hence thesis; end; dom ((r(#)arctan)`|Z) = dom f by A4,A6,FDIFF_1:def 7; then A9: ((r(#)arctan)`|Z) = f by A7,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11; hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:83; end; :: f.x = -1/(1+x^2) theorem A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-1/(1+x^2)) & Z = dom f & f|A is continuous implies integral(f,A) = arccot.(upper_bound A) - arccot.( lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ and A3: for x st x in Z holds f.x=-1/(1+x^2) and A4: Z = dom f and A5: f|A is continuous; A6: arccot is_differentiable_on Z by A2,SIN_COS9:82; A7: for x being Element of REAL st x in dom ((arccot)`|Z) holds ((arccot)`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((arccot)`|Z); then A8: x in Z by A6,FDIFF_1:def 7; then ((arccot)`|Z).x = -1/(1+x^2) by A2,SIN_COS9:82 .= f.x by A3,A8; hence thesis; end; dom ((arccot)`|Z) = dom f by A4,A6,FDIFF_1:def 7; then A9: ((arccot)`|Z) = f by A7,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11; hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:82; end; :: f.x = -r/(1+x^2) theorem A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-r/(1+x^2)) & Z = dom f & f|A is continuous implies integral(f,A) = (r(#)arccot).(upper_bound A) - (r (#)arccot).(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ and A3: for x st x in Z holds f.x=-r/(1+x^2) and A4: Z = dom f and A5: f|A is continuous; A6: r(#)arccot is_differentiable_on Z by A2,SIN_COS9:84; A7: for x being Element of REAL st x in dom ((r(#)arccot)`|Z) holds ((r(#)arccot)`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((r(#)arccot)`|Z); then A8: x in Z by A6,FDIFF_1:def 7; then ((r(#)arccot)`|Z).x = -r/(1+x^2) by A2,SIN_COS9:84 .= f.x by A3,A8; hence thesis; end; dom ((r(#)arccot)`|Z) = dom f by A4,A6,FDIFF_1:def 7; then A9: ((r(#)arccot)`|Z) = f by A7,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11; hence thesis by A1,A2,A9,INTEGRA5:13,SIN_COS9:84; end; :: f.x = x+cot.x-cosec.x theorem Th49: (Z c= dom ((id Z)+cot-cosec) & for x st x in Z holds (1+cos.x)<> 0 & (1-cos.x)<>0) implies (id Z)+cot-cosec is_differentiable_on Z & for x st x in Z holds ((id Z+cot-cosec)`|Z).x = cos.x/(1+cos.x) proof assume that A1: Z c= dom ((id Z)+cot-cosec) and A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0; A3: Z c= dom ((id Z)+cot) /\ dom cosec by A1,VALUED_1:12; then A4: Z c= dom (id Z+cot) by XBOOLE_1:18; then Z c= dom id Z /\ dom cot by VALUED_1:def 1; then A5: Z c= dom cot by XBOOLE_1:18; A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18; A7: Z c= dom id Z; then A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23; for x st x in Z holds cot is_differentiable_in x proof let x; assume x in Z; then sin.x<>0 by A5,FDIFF_8:2; hence thesis by FDIFF_7:47; end; then A9: cot is_differentiable_on Z by A5,FDIFF_1:9; then A10: id Z + cot is_differentiable_on Z by A4,A8,FDIFF_1:18; A11: Z c= dom cosec by A3,XBOOLE_1:18; then A12: cosec is_differentiable_on Z by FDIFF_9:5; A13: for x st x in Z holds (((id Z) + cot)`|Z).x = -(cos.x)^2/(sin.x)^2 proof let x; assume A14: x in Z; then A15: sin.x<>0 by A5,FDIFF_8:2; then A16: (sin.x)^2 >0 by SQUARE_1:12; ((id Z + cot)`|Z).x = diff((id Z),x) + diff(cot,x) by A4,A9,A8,A14, FDIFF_1:18 .=((id Z)`|Z).x + diff(cot,x) by A8,A14,FDIFF_1:def 7 .=1+diff(cot,x) by A7,A6,A14,FDIFF_1:23 .=1+(-1/(sin.x)^2) by A15,FDIFF_7:47 .=1-1/(sin.x)^2 .=(sin.x)^2/(sin.x)^2-1/(sin.x)^2 by A16,XCMPLX_1:60 .=((sin.x)^2-1)/(sin.x)^2 by XCMPLX_1:120 .=((sin.x)^2-((sin.x)^2+(cos.x)^2))/(sin.x)^2 by SIN_COS:28 .=(-(cos.x)^2)/(sin.x)^2 .=-(cos.x)^2/(sin.x)^2 by XCMPLX_1:187; hence thesis; end; for x st x in Z holds ((id Z + cot-cosec)`|Z).x = cos.x/(1+cos.x) proof let x; assume A17: x in Z; then A18: 1-cos.x<>0 by A2; ((id Z + cot-cosec)`|Z).x=diff((id Z + cot),x) -diff(cosec,x) by A1,A12,A10 ,A17,FDIFF_1:19 .=((id Z + cot)`|Z).x-diff(cosec,x) by A10,A17,FDIFF_1:def 7 .=-(cos.x)^2/(sin.x)^2-diff(cosec,x) by A13,A17 .=-(cos.x)^2/(sin.x)^2-((cosec)`|Z).x by A12,A17,FDIFF_1:def 7 .=-(cos.x)^2/(sin.x)^2-(-cos.x/(sin.x)^2) by A11,A17,FDIFF_9:5 .=cos.x/(sin.x)^2-(cos.x)^2/(sin.x)^2 .=(cos.x-(cos.x)*(cos.x))/(sin.x)^2 by XCMPLX_1:120 .=cos.x*(1-cos.x)/((sin.x)^2+(cos.x)^2-(cos.x)^2) .=cos.x*(1-cos.x)/(1-(cos.x)^2) by SIN_COS:28 .=cos.x*(1-cos.x)/((1-cos.x)*(1+cos.x)) .=cos.x*(1-cos.x)/(1-cos.x)/(1+cos.x) by XCMPLX_1:78 .=cos.x*((1-cos.x)/(1-cos.x))/(1+cos.x) by XCMPLX_1:74 .=cos.x*1/(1+cos.x) by A18,XCMPLX_1:60 .=cos.x/(1+cos.x); hence thesis; end; hence thesis by A1,A12,A10,FDIFF_1:19; end; :: f.x = cos.x/(1+cos.x) theorem A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = cos.x/(1+cos.x)) & dom (id Z+cot-cosec)=Z & Z = dom f & f|A is continuous implies integral(f,A) = (id Z+cot-cosec).(upper_bound A)-(id Z+cot-cosec).(lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = cos.x/(1+ cos.x) and A3: dom (id Z+cot-cosec)=Z and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2; then A8: (id Z+cot-cosec) is_differentiable_on Z by A3,Th49; A9: for x being Element of REAL st x in dom ((id Z+cot-cosec)`|Z) holds ((id Z+cot-cosec)`|Z).x = f .x proof let x be Element of REAL; assume x in dom ((id Z+cot-cosec)`|Z); then A10: x in Z by A8,FDIFF_1:def 7; then ((id Z+cot-cosec)`|Z).x = cos.x/(1+cos.x) by A3,A7,Th49 .= f.x by A2,A10; hence thesis; end; dom ((id Z+cot-cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7; then ((id Z+cot-cosec)`|Z) = f by A9,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13; end; :: f.x = x+cot.x+cosec.x theorem Th51: (Z c= dom ((id Z)+cot+cosec) & for x st x in Z holds (1+cos.x)<> 0 & (1-cos.x)<>0) implies (id Z)+cot+cosec is_differentiable_on Z & for x st x in Z holds ((id Z+cot+cosec)`|Z).x = cos.x/(cos.x-1) proof assume that A1: Z c= dom ((id Z)+cot+cosec) and A2: for x st x in Z holds 1+cos.x<>0 & 1-cos.x<>0; A3: Z c= dom ((id Z)+cot) /\ dom cosec by A1,VALUED_1:def 1; then A4: Z c= dom (id Z+cot) by XBOOLE_1:18; then Z c= dom id Z /\ dom cot by VALUED_1:def 1; then A5: Z c= dom cot by XBOOLE_1:18; A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18; A7: Z c= dom id Z; then A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23; for x st x in Z holds cot is_differentiable_in x proof let x; assume x in Z; then sin.x<>0 by A5,FDIFF_8:2; hence thesis by FDIFF_7:47; end; then A9: cot is_differentiable_on Z by A5,FDIFF_1:9; then A10: id Z + cot is_differentiable_on Z by A4,A8,FDIFF_1:18; A11: Z c= dom cosec by A3,XBOOLE_1:18; then A12: cosec is_differentiable_on Z by FDIFF_9:5; A13: for x st x in Z holds (((id Z) + cot)`|Z).x = -(cos.x)^2/(sin.x)^2 proof let x; assume A14: x in Z; then A15: sin.x<>0 by A5,FDIFF_8:2; then A16: (sin.x)^2 >0 by SQUARE_1:12; ((id Z + cot)`|Z).x = diff((id Z),x) + diff(cot,x) by A4,A9,A8,A14, FDIFF_1:18 .=((id Z)`|Z).x + diff(cot,x) by A8,A14,FDIFF_1:def 7 .=1+diff(cot,x) by A7,A6,A14,FDIFF_1:23 .=1+(-1/(sin.x)^2) by A15,FDIFF_7:47 .=1-1/(sin.x)^2 .=(sin.x)^2/(sin.x)^2-1/(sin.x)^2 by A16,XCMPLX_1:60 .=((sin.x)^2-1)/(sin.x)^2 by XCMPLX_1:120 .=((sin.x)^2-((sin.x)^2+(cos.x)^2))/(sin.x)^2 by SIN_COS:28 .=(-(cos.x)^2)/(sin.x)^2 .=-(cos.x)^2/(sin.x)^2 by XCMPLX_1:187; hence thesis; end; for x st x in Z holds ((id Z + cot+cosec)`|Z).x = cos.x/(cos.x-1) proof let x; assume A17: x in Z; then A18: 1+cos.x<>0 by A2; ((id Z + cot+cosec)`|Z).x=diff((id Z + cot),x) +diff(cosec,x) by A1,A12,A10 ,A17,FDIFF_1:18 .=((id Z + cot)`|Z).x+diff(cosec,x) by A10,A17,FDIFF_1:def 7 .=-(cos.x)^2/(sin.x)^2+diff(cosec,x) by A13,A17 .=-(cos.x)^2/(sin.x)^2+((cosec)`|Z).x by A12,A17,FDIFF_1:def 7 .=-(cos.x)^2/(sin.x)^2+(-cos.x/(sin.x)^2) by A11,A17,FDIFF_9:5 .=-((cos.x)^2/(sin.x)^2+cos.x/(sin.x)^2) .=-((cos.x)*(cos.x)+cos.x)/(sin.x)^2 by XCMPLX_1:62 .=-(cos.x)*(cos.x+1)/((sin.x)^2+(cos.x)^2-(cos.x)^2) .=-(cos.x)*(cos.x+1)/(1-(cos.x)^2) by SIN_COS:28 .=-(cos.x)*(cos.x+1)/((1+cos.x)*(1-cos.x)) .=-(cos.x)*(cos.x+1)/(1+cos.x)/(1-cos.x) by XCMPLX_1:78 .=-(cos.x)*((1+cos.x)/(1+cos.x))/(1-cos.x) by XCMPLX_1:74 .=-(cos.x)*1/(1-cos.x) by A18,XCMPLX_1:60 .=(cos.x)/(-(1-cos.x)) by XCMPLX_1:188 .=(cos.x)/(cos.x-1); hence thesis; end; hence thesis by A1,A12,A10,FDIFF_1:18; end; :: f.x = cos.x/(cos.x-1) theorem A c= Z & (for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = cos.x/(cos.x-1)) & dom (id Z+cot+cosec)=Z & Z = dom f & f|A is continuous implies integral(f,A) = (id Z+cot+cosec).(upper_bound A)-(id Z+cot+cosec).(lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 & f.x = cos.x/( cos.x-1) and A3: dom (id Z+cot+cosec)=Z and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: for x st x in Z holds (1+cos.x)<>0 & (1-cos.x)<>0 by A2; then A8: (id Z+cot+cosec) is_differentiable_on Z by A3,Th51; A9: for x being Element of REAL st x in dom ((id Z+cot+cosec)`|Z) holds ((id Z+cot+cosec)`|Z).x = f .x proof let x be Element of REAL; assume x in dom ((id Z+cot+cosec)`|Z); then A10: x in Z by A8,FDIFF_1:def 7; then ((id Z+cot+cosec)`|Z).x = cos.x/(cos.x-1) by A3,A7,Th51 .= f.x by A2,A10; hence thesis; end; dom ((id Z+cot+cosec)`|Z) = dom f by A4,A8,FDIFF_1:def 7; then ((id Z+cot+cosec)`|Z) = f by A9,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13; end; :: f.x = x-tan.x+sec.x theorem Th53: (Z c= dom (id Z-tan+sec) & for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0) implies (id Z)-tan+sec is_differentiable_on Z & for x st x in Z holds ((id Z-tan+sec)`|Z).x = sin.x/(sin.x+1) proof assume that A1: Z c= dom (id Z-tan+sec) and A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0; A3: Z c= dom (id Z-tan) /\ dom sec by A1,VALUED_1:def 1; then A4: Z c= dom (id Z-tan) by XBOOLE_1:18; then A5: Z c= dom id Z /\ dom tan by VALUED_1:12; A6: Z c= dom (id Z); A7: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18; then A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23; A9: Z c= dom tan by A5,XBOOLE_1:18; for x st x in Z holds tan is_differentiable_in x proof let x; assume x in Z; then cos.x<>0 by A9,FDIFF_8:1; hence thesis by FDIFF_7:46; end; then A10: tan is_differentiable_on Z by A9,FDIFF_1:9; then A11: id Z-tan is_differentiable_on Z by A4,A8,FDIFF_1:19; A12: Z c= dom sec by A3,XBOOLE_1:18; then A13: sec is_differentiable_on Z by FDIFF_9:4; A14: for x st x in Z holds ((id Z - tan)`|Z).x = -(sin.x)^2/(cos.x)^2 proof let x; assume A15: x in Z; then A16: cos.x<>0 by A9,FDIFF_8:1; then A17: (cos.x)^2 >0 by SQUARE_1:12; ((id Z - tan)`|Z).x = diff(id Z,x) - diff(tan,x) by A4,A10,A8,A15, FDIFF_1:19 .=((id Z)`|Z).x - diff(tan,x) by A8,A15,FDIFF_1:def 7 .=1-diff(tan,x) by A6,A7,A15,FDIFF_1:23 .=1-1/(cos.x)^2 by A16,FDIFF_7:46 .=1-((cos.x)^2+(sin.x)^2)/(cos.x)^2 by SIN_COS:28 .=1-((cos.x)^2/(cos.x)^2+(sin.x)^2/(cos.x)^2) by XCMPLX_1:62 .=1-(1+(sin.x)^2/(cos.x)^2) by A17,XCMPLX_1:60 .=-(sin.x)^2/(cos.x)^2; hence thesis; end; for x st x in Z holds ((id Z-tan+sec)`|Z).x = sin.x/(sin.x+1) proof let x; assume A18: x in Z; then A19: 1-sin.x<>0 by A2; ((id Z-tan+sec)`|Z).x=diff((id Z-tan),x) +diff(sec,x) by A1,A13,A11,A18, FDIFF_1:18 .=((id Z-tan)`|Z).x+diff(sec,x) by A11,A18,FDIFF_1:def 7 .=-(sin.x)^2/(cos.x)^2+diff(sec,x) by A14,A18 .=-(sin.x)^2/(cos.x)^2+((sec)`|Z).x by A13,A18,FDIFF_1:def 7 .=-(sin.x)^2/(cos.x)^2+sin.x/(cos.x)^2 by A12,A18,FDIFF_9:4 .=sin.x/(cos.x)^2-(sin.x)^2/(cos.x)^2 .=(sin.x-(sin.x)*(sin.x))/(cos.x)^2 by XCMPLX_1:120 .=(sin.x)*(1-sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2) .=(sin.x)*(1-sin.x)/(1-(sin.x)^2) by SIN_COS:28 .=(sin.x)*(1-sin.x)/((1-sin.x)*(1+sin.x)) .=(sin.x)*(1-sin.x)/(1-sin.x)/(1+sin.x) by XCMPLX_1:78 .=(sin.x)*((1-sin.x)/(1-sin.x))/(1+sin.x) by XCMPLX_1:74 .=(sin.x)*1/(1+sin.x) by A19,XCMPLX_1:60 .=sin.x/(1+sin.x); hence thesis; end; hence thesis by A1,A13,A11,FDIFF_1:18; end; :: f.x = sin.x/(1+sin.x) theorem A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = sin.x/(1+sin.x)) & Z c= dom (id Z-tan+sec) & Z = dom f & f|A is continuous implies integral(f,A) = (id Z-tan+sec).(upper_bound A)-(id Z-tan+sec).(lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = sin.x/(1+ sin.x) and A3: Z c= dom (id Z-tan+sec) and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2; then A8: (id Z-tan+sec) is_differentiable_on Z by A3,Th53; A9: for x being Element of REAL st x in dom ((id Z-tan+sec)`|Z) holds ((id Z-tan+sec)`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((id Z-tan+sec)`|Z); then A10: x in Z by A8,FDIFF_1:def 7; then ((id Z-tan+sec)`|Z).x = sin.x/(1+sin.x) by A3,A7,Th53 .= f.x by A2,A10; hence thesis; end; dom ((id Z-tan+sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7; then ((id Z-tan+sec)`|Z) = f by A9,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13; end; :: f.x = x-tan.x-sec.x theorem Th55: (Z c= dom (id Z-tan-sec) & for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0) implies id Z-tan-sec is_differentiable_on Z & for x st x in Z holds ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1) proof assume that A1: Z c= dom (id Z-tan-sec) and A2: for x st x in Z holds 1+sin.x<>0 & 1-sin.x<>0; A3: Z c= dom (id Z-tan) /\ dom sec by A1,VALUED_1:12; then A4: Z c= dom (id Z-tan) by XBOOLE_1:18; then Z c= dom id Z /\ dom tan by VALUED_1:12; then A5: Z c= dom tan by XBOOLE_1:18; A6: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18; A7: Z c= dom id Z; then A8: (id Z) is_differentiable_on Z by A6,FDIFF_1:23; for x st x in Z holds tan is_differentiable_in x proof let x; assume x in Z; then cos.x<>0 by A5,FDIFF_8:1; hence thesis by FDIFF_7:46; end; then A9: tan is_differentiable_on Z by A5,FDIFF_1:9; then A10: id Z-tan is_differentiable_on Z by A4,A8,FDIFF_1:19; A11: Z c= dom sec by A3,XBOOLE_1:18; then A12: sec is_differentiable_on Z by FDIFF_9:4; A13: for x st x in Z holds ((id Z-tan)`|Z).x = -(sin.x)^2/(cos.x)^2 proof let x; assume A14: x in Z; then A15: cos.x<>0 by A5,FDIFF_8:1; then A16: (cos.x)^2 >0 by SQUARE_1:12; ((id Z - tan)`|Z).x = diff(id Z,x) - diff(tan,x) by A4,A9,A8,A14,FDIFF_1:19 .=((id Z)`|Z).x - diff(tan,x) by A8,A14,FDIFF_1:def 7 .=1-diff(tan,x) by A7,A6,A14,FDIFF_1:23 .=1-1/(cos.x)^2 by A15,FDIFF_7:46 .=1-((cos.x)^2+(sin.x)^2)/(cos.x)^2 by SIN_COS:28 .=1-((cos.x)^2/(cos.x)^2+(sin.x)^2/(cos.x)^2) by XCMPLX_1:62 .=1-(1+(sin.x)^2/(cos.x)^2) by A16,XCMPLX_1:60 .=-(sin.x)^2/(cos.x)^2; hence thesis; end; for x st x in Z holds ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1) proof let x; assume A17: x in Z; then A18: 1+sin.x<>0 by A2; ((id Z-tan-sec)`|Z).x=diff((id Z-tan),x) -diff(sec,x) by A1,A12,A10,A17, FDIFF_1:19 .=((id Z-tan)`|Z).x-diff(sec,x) by A10,A17,FDIFF_1:def 7 .=-(sin.x)^2/(cos.x)^2-diff(sec,x) by A13,A17 .=-(sin.x)^2/(cos.x)^2-((sec)`|Z).x by A12,A17,FDIFF_1:def 7 .=-(sin.x)^2/(cos.x)^2-sin.x/(cos.x)^2 by A11,A17,FDIFF_9:4 .=-(sin.x/(cos.x)^2+(sin.x)^2/(cos.x)^2) .=-((sin.x+(sin.x)^2)/(cos.x)^2) by XCMPLX_1:62 .=-(sin.x)*(1+sin.x)/((cos.x)^2+(sin.x)^2-(sin.x)^2) .=-(sin.x)*(1+sin.x)/(1-(sin.x)^2) by SIN_COS:28 .=-(sin.x)*(1+sin.x)/((1+sin.x)*(1-sin.x)) .=-(sin.x)*(1+sin.x)/(1+sin.x)/(1-sin.x) by XCMPLX_1:78 .=-(sin.x)*((1+sin.x)/(1+sin.x))/(1-sin.x) by XCMPLX_1:74 .=-(sin.x)*1/(1-sin.x) by A18,XCMPLX_1:60 .=sin.x/(-(1-sin.x)) by XCMPLX_1:188 .=sin.x/(sin.x-1); hence thesis; end; hence thesis by A1,A12,A10,FDIFF_1:19; end; :: f.x = sin.x/(sin.x-1) theorem A c= Z & (for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = sin.x/(sin.x-1)) & Z c= dom (id Z-tan-sec) & Z = dom f & f|A is continuous implies integral(f,A) = (id Z-tan-sec).(upper_bound A)-(id Z-tan-sec).(lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 & f.x = sin.x/( sin.x-1) and A3: Z c= dom (id Z-tan-sec) and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: for x st x in Z holds (1+sin.x)<>0 & (1-sin.x)<>0 by A2; then A8: (id Z-tan-sec) is_differentiable_on Z by A3,Th55; A9: for x being Element of REAL st x in dom ((id Z-tan-sec)`|Z) holds ((id Z-tan-sec)`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((id Z-tan-sec)`|Z); then A10: x in Z by A8,FDIFF_1:def 7; then ((id Z-tan-sec)`|Z).x = sin.x/(sin.x-1) by A3,A7,Th55 .= f.x by A2,A10; hence thesis; end; dom ((id Z-tan-sec)`|Z) = dom f by A4,A8,FDIFF_1:def 7; then ((id Z-tan-sec)`|Z) = f by A9,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A8,INTEGRA5:10,13; end; :: f.x = tan.x-x theorem Th57: 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=(tan.x)^2 proof A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18; assume A2: Z c= dom (tan-id Z); then Z c= dom tan /\ dom (id Z) by VALUED_1:12; then A3: Z c= dom tan by XBOOLE_1:18; A4: Z c= dom (id Z); then A5: id Z is_differentiable_on Z by A1,FDIFF_1:23; for x st x in Z holds tan is_differentiable_in x proof let x; assume x in Z; then cos.x<>0 by A3,FDIFF_8:1; hence thesis by FDIFF_7:46; end; then A6: tan is_differentiable_on Z by A3,FDIFF_1:9; for x st x in Z holds ((tan-id Z)`|Z).x=(tan.x)^2 proof let x; assume A7: x in Z; then A8: cos.x<>0 by A3,FDIFF_8:1; then A9: (cos.x)^2 >0 by SQUARE_1:12; ((tan-id Z)`|Z).x= diff(tan,x) - diff(id Z,x) by A2,A5,A6,A7,FDIFF_1:19 .=1/(cos.x)^2-diff(id Z,x) by A8,FDIFF_7:46 .=1/(cos.x)^2-((id Z)`|Z).x by A5,A7,FDIFF_1:def 7 .=1/(cos.x)^2-1 by A4,A1,A7,FDIFF_1:23 .=1/(cos.x)^2-(cos.x)^2/(cos.x)^2 by A9,XCMPLX_1:60 .=(1-(cos.x)^2)/(cos.x)^2 by XCMPLX_1:120 .=((sin.x)^2+(cos.x)^2-(cos.x)^2)/(cos.x)^2 by SIN_COS:28 .=(sin(x)/cos(x))*((sin.x)/(cos.x)) by XCMPLX_1:76 .=(tan.x)*tan(x) by A3,A7,FDIFF_8:1,SIN_COS9:15 .=(tan.x)^2 by A3,A7,FDIFF_8:1,SIN_COS9:15; hence thesis; end; hence thesis by A2,A5,A6,FDIFF_1:19; end; :: f.x = (tan.x)^2 theorem A c= Z & (for x st x in Z holds cos.x >0 & f.x = (tan.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 that A1: A c= Z and A2: for x st x in Z holds cos.x >0 & f.x = (tan.x)^2 and A3: Z c= dom (tan-id Z) and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: (tan-id Z) is_differentiable_on Z by A3,Th57; A8: 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 A9: x in Z by A7,FDIFF_1:def 7; then ((tan-id Z)`|Z).x = (tan.x)^2 by A3,Th57 .= f.x by A2,A9; hence thesis; end; dom ((tan-id Z)`|Z) = dom f by A4,A7,FDIFF_1:def 7; then ((tan-id Z)`|Z) = f by A8,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13; end; :: f.x = -cot.x-x theorem Th59: Z c= dom (-cot-id Z) implies -cot-id Z is_differentiable_on Z & for x st x in Z holds ((-cot-id Z)`|Z).x = (cot.x)^2 proof set f = -cot; A1: for x st x in Z holds (id Z).x = 1*x+0 by FUNCT_1:18; assume A2: Z c= dom (-cot-id Z); then Z c= dom (-cot) /\ dom (id Z) by VALUED_1:12; then A3: Z c= dom (-cot) by XBOOLE_1:18; then A4: Z c= dom cot by VALUED_1:8; for x st x in Z holds cot is_differentiable_in x proof let x; assume x in Z; then sin.x<>0 by A4,FDIFF_8:2; hence thesis by FDIFF_7:47; end; then A5: cot is_differentiable_on Z by A4,FDIFF_1:9; then A6: (-1)(#)cot is_differentiable_on Z by A3,FDIFF_1:20; A7: Z c= dom (id Z); then A8: id Z is_differentiable_on Z by A1,FDIFF_1:23; for x st x in Z holds ((-cot-id Z)`|Z).x = (cot.x)^2 proof let x; assume A9: x in Z; then A10: sin.x<>0 by A4,FDIFF_8:2; then A11: (sin.x)^2 >0 by SQUARE_1:12; ((f-id Z)`|Z).x=diff(f,x) - diff(id Z,x) by A2,A8,A6,A9,FDIFF_1:19 .=(((-1)(#)cot)`|Z).x-diff(id Z,x) by A6,A9,FDIFF_1:def 7 .=(-1)*diff(cot,x)-diff(id Z,x) by A3,A5,A9,FDIFF_1:20 .=(-1)*(-1/(sin.x)^2)-diff(id Z,x) by A10,FDIFF_7:47 .=1/(sin.x)^2-((id Z)`|Z).x by A8,A9,FDIFF_1:def 7 .=1/(sin.x)^2-1 by A7,A1,A9,FDIFF_1:23 .=1/(sin.x)^2-(sin.x)^2/(sin.x)^2 by A11,XCMPLX_1:60 .=(1-(sin.x)^2)/(sin.x)^2 by XCMPLX_1:120 .=((cos.x)^2+(sin.x)^2-(sin.x)^2)/(sin.x)^2 by SIN_COS:28 .=(cos(x)/sin(x))*((cos.x)/(sin.x)) by XCMPLX_1:76 .=(cot.x)*cot(x) by A4,A9,FDIFF_8:2,SIN_COS9:16 .=(cot.x)^2 by A4,A9,FDIFF_8:2,SIN_COS9:16; hence thesis; end; hence thesis by A2,A8,A6,FDIFF_1:19; end; :: f.x = (cot.x)^2 theorem A c= Z & (for x st x in Z holds sin.x >0 & f.x = (cot.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 that A1: A c= Z and A2: for x st x in Z holds sin.x >0 & f.x = (cot.x)^2 and A3: Z c= dom (-cot-id Z) and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: (-cot-id Z) is_differentiable_on Z by A3,Th59; A8: 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 A9: x in Z by A7,FDIFF_1:def 7; then ((-cot-id Z)`|Z).x = (cot.x)^2 by A3,Th59 .= f.x by A2,A9; hence thesis; end; dom ((-cot-id Z)`|Z) = dom f by A4,A7,FDIFF_1:def 7; then ((-cot-id Z)`|Z) = f by A8,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13; end; :: f.x = 1/(cos.x)^2 theorem A c= Z & (for x st x in Z holds f.x = 1/(cos.x)^2 & cos.x <> 0) & dom tan=Z & Z = dom f & f|A is continuous implies integral(f,A) = tan.(upper_bound A)-tan.( lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds f.x = 1/(cos.x)^2 & cos.x <> 0 and A3: dom tan=Z and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: tan is_differentiable_on Z by A3,INTEGRA8:33; A8: for x being Element of REAL st x in dom (tan`|Z) holds (tan`|Z).x = f.x proof let x be Element of REAL; assume x in dom (tan`|Z); then A9: x in Z by A7,FDIFF_1:def 7; then (tan`|Z).x = 1/(cos.x)^2 by A3,INTEGRA8:33 .= f.x by A2,A9; hence thesis; end; dom (tan`|Z) = dom f by A4,A7,FDIFF_1:def 7; then (tan`|Z) = f by A8,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13; end; :: f.x = -1/(sin.x)^2 theorem A c= Z & (for x st x in Z holds f.x = -1/(sin.x)^2 & sin.x <> 0) & dom cot=Z & Z = dom f & f|A is continuous implies integral(f,A) = cot.(upper_bound A)-cot.( lower_bound A) proof assume that A1: A c= Z and A2: for x st x in Z holds f.x = -1/(sin.x)^2 & sin.x <> 0 and A3: dom cot=Z and A4: Z = dom f and A5: f|A is continuous; A6: f is_integrable_on A by A1,A4,A5,INTEGRA5:11; A7: cot is_differentiable_on Z by A3,INTEGRA8:34; A8: for x being Element of REAL st x in dom (cot`|Z) holds (cot`|Z).x = f.x proof let x be Element of REAL; assume x in dom (cot`|Z); then A9: x in Z by A7,FDIFF_1:def 7; then (cot`|Z).x = -1/(sin.x)^2 by A3,INTEGRA8:34 .= f.x by A2,A9; hence thesis; end; dom (cot`|Z) = dom f by A4,A7,FDIFF_1:def 7; then (cot`|Z) = f by A8,PARTFUN1:5; hence thesis by A1,A4,A5,A6,A7,INTEGRA5:10,13; end; :: f.x = (sin.x-(cos.x)^2)/(cos.x)^2 theorem A c= Z & (for x st x in Z holds f.x = (sin.x-(cos.x)^2)/(cos.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 that A1: A c= Z and A2: for x st x in Z holds f.x = (sin.x-(cos.x)^2)/(cos.x)^2 and A3: Z c= dom (sec-id Z) and A4: Z = dom f and A5: f|A is continuous; A6: (sec-id Z) is_differentiable_on Z by A3,FDIFF_9:22; A7: 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 A8: x in Z by A6,FDIFF_1:def 7; then ((sec-id Z)`|Z).x = (sin.x-(cos.x)^2)/(cos.x)^2 by A3,FDIFF_9:22 .= f.x by A2,A8; hence thesis; end; dom ((sec-id Z)`|Z) = dom f by A4,A6,FDIFF_1:def 7; then A9: ((sec-id Z)`|Z) = f by A7,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11; hence thesis by A1,A3,A9,FDIFF_9:22,INTEGRA5:13; end; :: f.x = (cos.x-(sin.x)^2)/(sin.x)^2 theorem A c= Z & (for x st x in Z holds f.x = (cos.x-(sin.x)^2)/(sin.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 that A1: A c= Z and A2: for x st x in Z holds f.x = (cos.x-(sin.x)^2)/(sin.x)^2 and A3: Z c= dom (-cosec-id Z) and A4: Z = dom f and A5: f|A is continuous; A6: (-cosec-id Z) is_differentiable_on Z by A3,FDIFF_9:23; 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.x-(sin.x)^2)/(sin.x)^2 by A3,FDIFF_9:23 .= f.x by A2,A8; hence thesis; end; dom ((-cosec-id Z)`|Z) = dom f by A4,A6,FDIFF_1:def 7; then A9: ((-cosec-id Z)`|Z) = f by A7,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11; hence thesis by A1,A3,A9,FDIFF_9:23,INTEGRA5:13; end; :: f.x = cot(x) theorem A c= Z & (for x st x in Z holds sin.x >0) & Z c= dom (ln*sin) & Z = dom cot & cot|A is continuous implies integral(cot,A) = (ln*sin).(upper_bound A)-(ln* sin).(lower_bound A) proof set f = cot; assume that A1: A c= Z and A2: for x st x in Z holds sin.x >0 and A3: Z c= dom (ln*sin) and A4: Z = dom cot and A5: f|A is continuous; A6: (ln*sin) is_differentiable_on Z by A2,A3,FDIFF_4:43; A7: for x being Element of REAL st x in dom ((ln*sin)`|Z) holds ((ln*sin)`|Z).x = f.x proof let x be Element of REAL; assume x in dom ((ln*sin)`|Z); then A8: x in Z by A6,FDIFF_1:def 7; then A9: sin.x <> 0 by A2; ((ln*sin)`|Z).x = cot(x) by A2,A3,A8,FDIFF_4:43 .= f.x by A9,SIN_COS9:16; hence thesis; end; dom ((ln*sin)`|Z) = dom f by A4,A6,FDIFF_1:def 7; then A10: ((ln*sin)`|Z) = f by A7,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A4,A5,INTEGRA5:10,11; hence thesis by A1,A2,A3,A10,FDIFF_4:43,INTEGRA5:13; end; :: f.x = arcsin.x / sqrt(1-x^2) theorem A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=arcsin.x/sqrt(1- x^2)) & Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) & Z = dom f & f|A is continuous implies integral(f,A) = ((1/2)(#)(( #Z 2)*(arcsin))).(upper_bound A) -((1/2)(#)(( #Z 2) *(arcsin))).(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ and A3: for x st x in Z holds f.x=arcsin.x/sqrt(1-x^2) and A4: Z c= dom ((1/2)(#)(( #Z 2)*(arcsin))) and A5: Z = dom f and A6: f|A is continuous; A7: ((1/2)(#)(( #Z 2)*(arcsin))) is_differentiable_on Z by A2,A4,FDIFF_7:12; A8: for x being Element of REAL st x in dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) holds (((1/2)(#)(( #Z 2)*(arcsin)))`|Z).x = f.x proof let x be Element of REAL; assume x in dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z); then A9: x in Z by A7,FDIFF_1:def 7; then (((1/2)(#)(( #Z 2)*(arcsin)))`|Z).x = arcsin.x / sqrt(1-x^2) by A2,A4, FDIFF_7:12 .= f.x by A3,A9; hence thesis; end; dom (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) = dom f by A5,A7,FDIFF_1:def 7; then A10: (((1/2)(#)(( #Z 2)*(arcsin)))`|Z) = f by A8,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A5,A6,INTEGRA5:10,11; hence thesis by A1,A2,A4,A10,FDIFF_7:12,INTEGRA5:13; end; :: f.x = -arccos.x / sqrt(1-x^2) theorem A c= Z & Z c= ]. -1,1 .[ & (for x st x in Z holds f.x=-arccos.x / sqrt (1-x^2)) & Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) & Z = dom f & f|A is continuous implies integral(f,A) = ((1/2)(#)(( #Z 2)*(arccos))).(upper_bound A) -((1/2) (#)(( #Z 2)*(arccos))).(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ and A3: for x st x in Z holds f.x=-arccos.x / sqrt(1-x^2) and A4: Z c= dom ((1/2)(#)(( #Z 2)*(arccos))) and A5: Z = dom f and A6: f|A is continuous; A7: ((1/2)(#)(( #Z 2)*(arccos))) is_differentiable_on Z by A2,A4,FDIFF_7:13; A8: for x being Element of REAL st x in dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z) holds (((1/2)(#)(( #Z 2)*(arccos)))`|Z).x = f.x proof let x be Element of REAL; assume x in dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z); then A9: x in Z by A7,FDIFF_1:def 7; then (((1/2)(#)(( #Z 2)*(arccos)))`|Z).x = -arccos.x / sqrt(1-x^2) by A2,A4 ,FDIFF_7:13 .= f.x by A3,A9; hence thesis; end; dom (((1/2)(#)(( #Z 2)*(arccos)))`|Z) = dom f by A5,A7,FDIFF_1:def 7; then A10: (((1/2)(#)(( #Z 2)*(arccos)))`|Z) = f by A8,PARTFUN1:5; f is_integrable_on A & f|A is bounded by A1,A5,A6,INTEGRA5:10,11; hence thesis by A1,A2,A4,A10,FDIFF_7:13,INTEGRA5:13; end; :: f.x = arcsin.x theorem A c= Z & Z c= ]. -1,1 .[ & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=1 & f.x >0 & x<>0) & dom arcsin=Z & Z c= dom ((id Z)(#)(arcsin)+( #R (1/2) )*f) implies integral(arcsin,A) = ((id Z)(#)(arcsin)+( #R (1/2))*f).(upper_bound A) -(( id Z)(#)(arcsin) + ( #R (1/2))*f).(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ & f=f1-f2 &( f2=#Z 2 & for x st x in Z holds f1.x=1 & f.x >0 & x<>0 ) and A3: dom arcsin=Z and A4: Z c= dom ((id Z)(#)(arcsin)+( #R (1/2))*f); A5: arcsin|A is bounded by A1,A3,INTEGRA5:10; A6: ((id Z)(#)(arcsin)+( #R (1/2))*f) is_differentiable_on Z by A2,A4, FDIFF_7:23; A7: for x being Element of REAL st x in dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) holds (((id Z) (#)(arcsin)+( #R (1/2))*f)`|Z).x = arcsin.x proof let x be Element of REAL; assume x in dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z); then x in Z by A6,FDIFF_1:def 7; hence thesis by A2,A4,FDIFF_7:23; end; dom (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) = dom arcsin by A3,A6, FDIFF_1:def 7; then (((id Z)(#)(arcsin)+( #R (1/2))*f)`|Z) = arcsin by A7,PARTFUN1:5; hence thesis by A1,A3,A5,A6,INTEGRA5:11,13; end; :: f.x = arcsin.(x/a) theorem A c= Z & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3.x < 1 & x<>0 & a>0) & dom ((arcsin)*f3)=Z & Z c= dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) & ((arcsin)*f3)|A is continuous implies integral((arcsin)*f3,A) = ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f).(upper_bound A ) -((id Z)(#)((arcsin)*f3)+( #R (1/2))*f).(lower_bound A) proof assume that A1: A c= Z and A2: f=f1-f2 & f2=#Z 2 and A3: for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3 .x < 1 & x<>0 & a>0 and A4: dom ((arcsin)*f3)=Z and A5: Z c= dom ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) and A6: ((arcsin)*f3)|A is continuous; A7: (arcsin)*f3 is_integrable_on A by A1,A4,A6,INTEGRA5:11; A8: ((id Z)(#)((arcsin)*f3)+( #R (1/2))*f) is_differentiable_on Z by A2,A3,A5, FDIFF_7:28; A9: for x being Element of REAL st x in dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) holds (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x = ((arcsin)*f3).x proof let x be Element of REAL; assume x in dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z); then A10: x in Z by A8,FDIFF_1:def 7; then (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z).x = arcsin.(x/a) by A2,A3,A5, FDIFF_7:28 .= arcsin.(f3.x) by A3,A10 .= ((arcsin)*f3).x by A4,A10,FUNCT_1:12; hence thesis; end; dom (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) = dom ((arcsin)*f3) by A4,A8, FDIFF_1:def 7; then (((id Z)(#)((arcsin)*f3)+( #R (1/2))*f)`|Z) = (arcsin)*f3 by A9, PARTFUN1:5; hence thesis by A1,A4,A6,A7,A8,INTEGRA5:10,13; end; :: f.x = arccos.x theorem A c= Z & Z c= ]. -1,1 .[ & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=1 & f.x >0 & x<>0) & dom arccos=Z & Z c= dom ((id Z)(#)(arccos)-( #R (1/2) )*f) implies integral(arccos,A) = ((id Z)(#)(arccos)-( #R (1/2))*f).(upper_bound A) -(( id Z)(#)(arccos)-( #R (1/2))*f).(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ & f=f1-f2 &( f2=#Z 2 & for x st x in Z holds f1.x=1 & f.x >0 & x<>0 ) and A3: dom arccos=Z and A4: Z c= dom ((id Z)(#)(arccos)-( #R (1/2))*f); A5: arccos|A is bounded by A1,A3,INTEGRA5:10; A6: ((id Z)(#)(arccos)-( #R (1/2))*f) is_differentiable_on Z by A2,A4, FDIFF_7:24; A7: for x being Element of REAL st x in dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) holds (((id Z) (#)(arccos)-( #R (1/2))*f)`|Z).x = arccos.x proof let x be Element of REAL; assume x in dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z); then x in Z by A6,FDIFF_1:def 7; hence thesis by A2,A4,FDIFF_7:24; end; dom (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) = dom arccos by A3,A6, FDIFF_1:def 7; then (((id Z)(#)(arccos)-( #R (1/2))*f)`|Z) = arccos by A7,PARTFUN1:5; hence thesis by A1,A3,A5,A6,INTEGRA5:11,13; end; :: f.x = arccos.(x/a) theorem A c= Z & f=f1-f2 & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3.x < 1 & x<>0 & a>0) & dom ((arccos)*f3)=Z & Z = dom ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) & ((arccos)*f3)|A is continuous implies integral((arccos)*f3,A) = ((id Z)(#)((arccos)*f3)-( #R (1/2))*f).(upper_bound A) -((id Z)(#)((arccos)*f3)-( #R (1/2))*f).(lower_bound A) proof assume that A1: A c= Z and A2: f=f1-f2 & f2=#Z 2 and A3: for x st x in Z holds f1.x=a^2 & f.x >0 & f3.x=x/a & f3.x > -1 & f3 .x < 1 & x<>0 & a>0 and A4: dom ((arccos)*f3)=Z and A5: Z = dom ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) and A6: ((arccos)*f3)|A is continuous; A7: (arccos)*f3 is_integrable_on A by A1,A4,A6,INTEGRA5:11; A8: ((id Z)(#)((arccos)*f3)-( #R (1/2))*f) is_differentiable_on Z by A2,A3,A5, FDIFF_7:29; A9: for x being Element of REAL st x in dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) holds (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x = ((arccos)*f3).x proof let x be Element of REAL; assume x in dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z); then A10: x in Z by A8,FDIFF_1:def 7; then (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z).x = arccos.(x/a) by A2,A3,A5, FDIFF_7:29 .= arccos.(f3.x) by A3,A10 .= ((arccos)*f3).x by A4,A10,FUNCT_1:12; hence thesis; end; dom (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) = dom ((arccos)*f3) by A4,A8, FDIFF_1:def 7; then (((id Z)(#)((arccos)*f3)-( #R (1/2))*f)`|Z) = (arccos)*f3 by A9, PARTFUN1:5; hence thesis by A1,A4,A6,A7,A8,INTEGRA5:10,13; end; :: f.x = arctan.x theorem A c= Z & Z c= ]. -1,1 .[ & f2=#Z 2 & (for x st x in Z holds f1.x=1 ) & Z = dom arctan & Z = dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) implies integral(arctan,A) = ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z) (#)(arctan)-(1/2)(#)(ln*(f1+f2))).(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ and A3: f2=#Z 2 & for x st x in Z holds f1.x=1 and A4: Z = dom arctan and A5: Z = dom ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))); ].-1,1 .[ c= [.-1,1 .] & A c= ].-1,1 .[ by A1,A2,XBOOLE_1:1,XXREAL_1:25; then arctan|A is continuous by FCONT_1:16,SIN_COS9:53,XBOOLE_1:1; then A6: arctan is_integrable_on A & arctan|A is bounded by A1,A4,INTEGRA5:10,11; A7: ((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A2,A3,A5 ,SIN_COS9:103; A8: for x being Element of REAL st x in dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) holds (( (id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z).x = arctan.x proof let x be Element of REAL; assume x in dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z); then x in Z by A7,FDIFF_1:def 7; hence thesis by A2,A3,A5,SIN_COS9:103; end; dom (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) = dom arctan by A4,A7, FDIFF_1:def 7; then (((id Z)(#)(arctan)-(1/2)(#)(ln*(f1+f2)))`|Z) = arctan by A8,PARTFUN1:5; hence thesis by A1,A2,A3,A5,A6,INTEGRA5:13,SIN_COS9:103; end; :: f.x = arccot.x theorem A c= Z & Z c= ]. -1,1 .[ & f2=#Z 2 & (for x st x in Z holds f1.x=1) & dom arccot=Z & Z = dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) implies integral(arccot,A) = ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))).(upper_bound A) -((id Z) (#)(arccot)+(1/2)(#)(ln*(f1+f2))).(lower_bound A) proof assume that A1: A c= Z and A2: Z c= ]. -1,1 .[ and A3: f2=#Z 2 & for x st x in Z holds f1.x=1 and A4: dom arccot=Z and A5: Z = dom ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))); ].-1,1 .[ c= [.-1,1 .] & A c= ].-1,1 .[ by A1,A2,XBOOLE_1:1,XXREAL_1:25; then arccot|A is continuous by FCONT_1:16,SIN_COS9:54,XBOOLE_1:1; then A6: arccot is_integrable_on A & arccot|A is bounded by A1,A4,INTEGRA5:10,11; A7: ((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2))) is_differentiable_on Z by A2,A3,A5 ,SIN_COS9:104; A8: for x being Element of REAL st x in dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) holds (( (id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z).x = arccot.x proof let x be Element of REAL; assume x in dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z); then x in Z by A7,FDIFF_1:def 7; hence thesis by A2,A3,A5,SIN_COS9:104; end; dom (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) = dom arccot by A4,A7, FDIFF_1:def 7; then (((id Z)(#)(arccot)+(1/2)(#)(ln*(f1+f2)))`|Z) = arccot by A8,PARTFUN1:5; hence thesis by A1,A2,A3,A5,A6,INTEGRA5:13,SIN_COS9:104; end;