:: Several Differentiable Formulas of Special Functions -- Part {II} :: by Yan Zhang , Bo Li and Xiquan Liang :: :: Received November 23, 2005 :: Copyright (c) 2005-2017 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 NUMBERS, REAL_1, SUBSET_1, RCOMP_1, PARTFUN1, ARYTM_1, SIN_COS, RELAT_1, SQUARE_1, ARYTM_3, FUNCT_1, XXREAL_0, CARD_1, PREPOWER, POWER, TARSKI, FDIFF_1, VALUED_1, NEWTON, XBOOLE_0, TAYLOR_1, ORDINAL4, COMPLEX1, LIMFUNC1; notations TARSKI, XBOOLE_0, SUBSET_1, RELAT_1, FUNCT_1, PARTFUN1, LIMFUNC1, RCOMP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, XREAL_0, REAL_1, NAT_1, VALUED_1, FDIFF_1, NEWTON, INT_2, PREPOWER, POWER, TAYLOR_1, SIN_COS, RFUNCT_1, SQUARE_1; constructors PARTFUN1, REAL_1, SQUARE_1, NAT_1, RCOMP_1, PARTFUN2, RFUNCT_1, LIMFUNC1, FDIFF_1, PREPOWER, POWER, SIN_COS, TAYLOR_1, VALUED_1, RELSET_1, NEWTON; registrations ORDINAL1, RELSET_1, XXREAL_0, INT_1, MEMBERED, RCOMP_1, VALUED_0, XREAL_0, NEWTON, SIN_COS, SQUARE_1, PREPOWER; requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM; equalities SQUARE_1, TAYLOR_1, VALUED_1; theorems FDIFF_2, TAYLOR_1, XBOOLE_1, XCMPLX_1, FDIFF_1, FUNCT_1, TARSKI, PREPOWER, RFUNCT_1, SQUARE_1, XREAL_1, XCMPLX_0, NEWTON, SIN_COS, SIN_COS2, WSIERP_1, FDIFF_4, POWER, ABSVALUE, VALUED_1; begin reserve y for set, x,a for Real, n for Element of NAT, Z for open Subset of REAL, f,f1,f2 for PartFunc of REAL,REAL; Lm1: 1-cos(2*x)=2*(sin x)^2 proof 1-cos(2*x)=1-cos(x+x) .=1-((cos x) *(cos x)-(sin x) * (sin x)) by SIN_COS:75 .=(cos x)^2+(sin x)^2-((cos x)^2-(sin x)^2) by SIN_COS:29 .=2*(sin x)^2; hence thesis; end; Lm2: 1+cos(2*x)=2*(cos x)^2 proof 1+cos(2*x)=1+cos(x+x) .=1+((cos x)^2-(sin x)^2) by SIN_COS:75 .=(cos x)^2+(sin x)^2+((cos x)^2-(sin x)^2) by SIN_COS:29 .=2*(cos x)^2; hence thesis; end; :: 39 f.x=2*(1-cos.x) #R (1/2) Lm3: sin.x>0 implies sin.x=((1-cos.x)*(1+cos.x)) #R (1/2) proof assume A1: sin.x>0; then sin.x=(sin.x) #R (2*(1/2)) by PREPOWER:72 .=(sin.x) #R (1+1) #R (1/2) by A1,PREPOWER:91 .=((sin.x) #R 1 * (sin.x) #R 1) #R (1/2) by A1,PREPOWER:75 .=(sin.x * (sin.x) #R 1) #R (1/2) by A1,PREPOWER:72 .=((sin.x)^2+(cos.x)^2-(cos.x)^2) #R (1/2) by A1,PREPOWER:72 .=(1^2-(cos.x)^2) #R (1/2) by SIN_COS:28 .=((1-cos.x)*(1+cos.x)) #R (1/2); hence thesis; end; Lm4: sin.x>0 & cos.x<1 & cos.x>-1 implies sin.x/(1-cos.x) #R (1/2) =(1+cos.x) #R (1/2) proof assume that A1: sin.x>0 and A2: cos.x<1 and A3: cos.x>-1; A4: 1-cos.x>1-1 by A2,XREAL_1:15; 1+cos.x>1+-1 by A3,XREAL_1:8; then A5: (1-cos.x)*(1+cos.x)>0 by A4,XREAL_1:129; sin.x/(1-cos.x) #R (1/2) =((1-cos.x)*(1+cos.x)) #R (1/2)/(1-cos.x) #R (1 /2) by A1,Lm3 .=(((1-cos.x)*(1+cos.x))/(1-cos.x)) #R (1/2) by A4,A5,PREPOWER:80 .=(1+cos.x) #R (1/2) by A4,XCMPLX_1:89; hence thesis; end; :: a #R x=exp.(x*ln a) theorem Th1: a>0 implies exp_R.(x*log(number_e,a))=a #R x proof assume A1: a>0; number_e<>1 by TAYLOR_1:11; then exp_R.(x*log(number_e,a)) =exp_R.(log(number_e,a to_power x)) by A1, POWER:55,TAYLOR_1:11 .=exp_R.(log(number_e,a #R x)) by A1,POWER:def 2 .=a #R x by A1,PREPOWER:81,TAYLOR_1:15; hence thesis; end; :: 15 a #R (-x)=exp.(-x*ln a) theorem Th2: a>0 implies exp_R.(-x*log(number_e,a))=a #R (-x) proof A1: number_e<>1 by TAYLOR_1:11; assume A2: a>0; exp_R.(-x*log(number_e,a)) =exp_R.((-x)*log(number_e,a)) .=exp_R.(log(number_e,a to_power (-x))) by A2,A1,POWER:55,TAYLOR_1:11 .=exp_R.(log(number_e,a #R (-x))) by A2,POWER:def 2 .=a #R (-x) by A2,PREPOWER:81,TAYLOR_1:15; hence thesis; end; :: 40 f.x=-2*(1+cos.x) #R (1/2) Lm5: sin.x>0 & cos.x<1 & cos.x>-1 implies sin.x/(1+cos.x) #R (1/2) =(1-cos.x) #R (1/2) proof assume that A1: sin.x>0 and A2: cos.x<1 and A3: cos.x>-1; A4: 1+cos.x>1+-1 by A3,XREAL_1:8; 1-cos.x>1-1 by A2,XREAL_1:15; then A5: (1-cos.x)*(1+cos.x)>0 by A4,XREAL_1:129; sin.x/(1+cos.x) #R (1/2) =((1-cos.x)*(1+cos.x)) #R (1/2)/(1+cos.x) #R (1 /2) by A1,Lm3 .=(((1-cos.x)*(1+cos.x))/(1+cos.x)) #R (1/2) by A4,A5,PREPOWER:80 .=(1-cos.x) #R (1/2) by A4,XCMPLX_1:89; hence thesis; end; :: 1 f.x=a^2-x^2 theorem Th3: Z c= dom (f1-f2) & (for x st x in Z holds f1.x=a^2) & f2=#Z 2 implies f1-f2 is_differentiable_on Z & for x st x in Z holds ((f1-f2)`|Z).x = - 2*x proof assume that A1: Z c= dom (f1-f2) and A2: for x st x in Z holds f1.x=a^2 and A3: f2=#Z 2; A4: for x st x in Z holds f1.x=a^2+0*x by A2; for x st x in Z holds ((f1-f2)`|Z).x = -2*x proof let x; assume x in Z; hence ((f1-f2)`|Z).x =0+2*(-1)*x by A1,A3,A4,FDIFF_4:12 .=-2*x; end; hence thesis by A1,A3,A4,FDIFF_4:12; end; :: 2 f.x=(a^2+x^2)/(a^2-x^2) theorem Th4: Z c= dom ((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x st x in Z holds f1. x=a^2 & (f1-f2).x<>0) implies (f1+f2)/(f1-f2) is_differentiable_on Z & for x st x in Z holds (((f1+f2)/(f1-f2))`|Z).x = 4*a^2*x/(a^2-x|^2)^2 proof assume that A1: Z c= dom ((f1+f2)/(f1-f2)) and A2: f2=#Z 2 and A3: for x st x in Z holds f1.x=a^2 & (f1-f2).x<>0; A4: for x st x in Z holds f1.x=a^2 by A3; A5: Z c=dom (f1+f2) /\ (dom (f1-f2) \ (f1-f2)"{0}) by A1,RFUNCT_1:def 1; then A6: Z c= dom (f1+f2) by XBOOLE_1:18; then A7: f1+f2 is_differentiable_on Z by A2,A4,FDIFF_4:17; A8: Z c= dom (f1-f2) by A5,XBOOLE_1:1; then A9: f1-f2 is_differentiable_on Z by A2,A4,Th3; A10: for x st x in Z holds (f1-f2).x <> 0 by A3; then A11: (f1+f2)/(f1-f2) is_differentiable_on Z by A7,A9,FDIFF_2:21; for x st x in Z holds (((f1+f2)/(f1-f2))`|Z).x=4*a^2*x/(a^2-x|^2)^2 proof let x; A12: f2.x=x #Z 2 by A2,TAYLOR_1:def 1 .=x |^2 by PREPOWER:36; assume A13: x in Z; then A14: (f1-f2).x<>0 by A3; A15: (f1-f2).x=f1.x-f2.x by A8,A13,VALUED_1:13 .=a^2-x |^2 by A3,A13,A12; A16: (f1+f2).x=f1.x+f2.x by A6,A13,VALUED_1:def 1 .=a^2+x |^2 by A3,A13,A12; f1+f2 is_differentiable_in x & f1-f2 is_differentiable_in x by A7,A9,A13, FDIFF_1:9; then diff((f1+f2)/(f1-f2),x) =(diff(f1+f2,x)*(f1-f2).x - diff(f1-f2,x)*(f1 +f2).x)/((f1-f2).x)^2 by A14,FDIFF_2:14 .=(((f1+f2)`|Z).x * (f1-f2).x-diff(f1-f2,x) * (f1+f2).x)/((f1-f2).x)^2 by A7,A13,FDIFF_1:def 7 .= (((f1+f2)`|Z).x * (f1-f2).x-((f1-f2)`|Z).x * (f1+f2).x)/((f1-f2).x) ^2 by A9,A13,FDIFF_1:def 7 .=((2*x)*(f1-f2).x-((f1-f2)`|Z).x * (f1+f2).x)/((f1-f2).x)^2 by A2,A6,A4 ,A13,FDIFF_4:17 .=((2*x)*(f1-f2).x-(-2*x) * (f1+f2).x)/((f1-f2).x)^2 by A2,A8,A4,A13,Th3 .=4*a^2*x/(a^2-x|^2)^2 by A16,A15; hence thesis by A11,A13,FDIFF_1:def 7; end; hence thesis by A7,A9,A10,FDIFF_2:21; end; :: 3 f.x=ln((a^2+x^2)/(a^2-x^2)) theorem Th5: Z c= dom f & f=ln*((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =4*a^2*x/(a|^4-x|^4) proof assume that A1: Z c= dom f and A2: f=ln*((f1+f2)/(f1-f2)) and A3: f2=#Z 2 and A4: for x st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0; for y being object st y in Z holds y in dom ((f1+f2)/(f1-f2)) by A1,A2,FUNCT_1:11; then A5: Z c= dom ((f1+f2)/(f1-f2)) by TARSKI:def 3; then A6: Z c=dom (f1+f2) /\ (dom (f1-f2) \ (f1-f2)"{0}) by RFUNCT_1:def 1; then A7: Z c= dom (f1-f2) by XBOOLE_1:1; A8: for x st x in Z holds f1.x=a^2 & (f1-f2).x<>0 by A4; then A9: (f1+f2)/(f1-f2) is_differentiable_on Z by A3,A5,Th4; A10: Z c= dom (f1+f2) by A6,XBOOLE_1:18; A11: for x st x in Z holds ((f1+f2)/(f1-f2)).x >0 proof let x; A12: f2.x=x #Z 2 by A3,TAYLOR_1:def 1 .=x |^2 by PREPOWER:36; assume A13: x in Z; then A14: (f1-f2).x>0 by A4; a<>0 by A4,A13; then A15: a^2>0 by SQUARE_1:12; x |^2 = x^2 by NEWTON:81; then A16: a^2+x |^2>0+0 by A15,XREAL_1:8,63; A17: ((f1+f2)/(f1-f2)).x =(f1+f2).x * ((f1-f2).x)" by A5,A13,RFUNCT_1:def 1 .=(f1+f2).x / (f1-f2).x by XCMPLX_0:def 9; (f1+f2).x=f1.x+f2.x by A10,A13,VALUED_1:def 1 .=a^2+x |^2 by A4,A13,A12; hence thesis by A14,A16,A17,XREAL_1:139; end; A18: for x st x in Z holds ln*((f1+f2)/(f1-f2)) is_differentiable_in x proof let x; assume x in Z; then (f1+f2)/(f1-f2) is_differentiable_in x & ((f1+f2)/(f1-f2)).x >0 by A9 ,A11,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A19: f is_differentiable_on Z by A1,A2,FDIFF_1:9; for x st x in Z holds (f`|Z).x = 4*a^2*x/(a|^4-x|^4) proof let x; A20: (a^2)^2=(a|^2)*(a^2) by NEWTON:81 .=(a|^2)*(a|^2) by NEWTON:81 .=(a|^2)|^2 by WSIERP_1:1 .=a|^(2*2) by NEWTON:9 .=a|^4; A21: (x |^2)^2=(x |^2)|^2 by WSIERP_1:1 .=x|^(2*2) by NEWTON:9 .=x|^4; A22: f2.x=x #Z 2 by A3,TAYLOR_1:def 1 .=x |^2 by PREPOWER:36; assume A23: x in Z; then A24: (f1+f2).x=f1.x+f2.x by A10,VALUED_1:def 1 .=a^2+x |^2 by A4,A23,A22; A25: (f1-f2).x=f1.x-f2.x by A7,A23,VALUED_1:13 .=a^2-x |^2 by A4,A23,A22; then A26: a^2-x |^2>0 by A4,A23; A27: ((f1+f2)/(f1-f2)).x =(f1+f2).x * ((f1-f2).x)" by A5,A23,RFUNCT_1:def 1 .=(a^2+x |^2)/(a^2-x |^2) by A24,A25,XCMPLX_0:def 9; (f1+f2)/(f1-f2) is_differentiable_in x & ((f1+f2)/(f1-f2)).x >0 by A9,A11 ,A23,FDIFF_1:9; then diff(ln*((f1+f2)/(f1-f2)),x) =diff(((f1+f2)/(f1-f2)),x)/(((f1+f2)/(f1 -f2)).x) by TAYLOR_1:20 .=(((f1+f2)/(f1-f2))`|Z).x/(((f1+f2)/(f1-f2)).x) by A9,A23,FDIFF_1:def 7 .= (4*a^2*x/(a^2-x|^2)^2)/((a^2+x |^2)/(a^2-x |^2)) by A3,A5,A8,A23,A27 ,Th4 .=(4*a^2*x/(a^2-x|^2)/(a^2-x|^2))/((a^2+x |^2)/(a^2-x |^2)) by XCMPLX_1:78 .=(4*a^2*x/(a^2-x|^2))/((a^2+x |^2)/(a^2-x |^2))/(a^2-x|^2) by XCMPLX_1:48 .=(4*a^2*x)/(a^2+x |^2)/(a^2-x|^2) by A26,XCMPLX_1:55 .=(4*a^2*x)/((a^2+x |^2)*(a^2-x|^2)) by XCMPLX_1:78 .=4*a^2*x/(a|^4-x|^4) by A20,A21; hence thesis by A2,A19,A23,FDIFF_1:def 7; end; hence thesis by A1,A2,A18,FDIFF_1:9; end; :: 4 f.x=(1/(4*a^2))*ln((a^2+x^2)/(a^2-x^2)) theorem Z c= dom ((1/(4*a^2))(#)f) & f=ln*((f1+f2)/(f1-f2)) & f2=#Z 2 & (for x st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0) implies (1/(4*a^2))(#)f is_differentiable_on Z & for x st x in Z holds (((1/(4*a^2))(#)f)`|Z).x =x/(a|^ 4-x|^4) proof assume that A1: Z c= dom ((1/(4*a^2))(#)f) and A2: f=ln*((f1+f2)/(f1-f2)) & f2=#Z 2 and A3: for x st x in Z holds f1.x=a^2 & (f1-f2).x>0 & a<>0; A4: Z c= dom f by A1,VALUED_1:def 5; then A5: f is_differentiable_on Z by A2,A3,Th5; for x st x in Z holds (((1/(4*a^2))(#)f)`|Z).x =x/(a|^4-x|^4) proof let x; assume A6: x in Z; then a<>0 by A3; then a^2>0 by SQUARE_1:12; then A7: 4*a^2>4*0 by XREAL_1:68; (((1/(4*a^2))(#)f)`|Z).x =(1/(4*a^2))*diff(f,x) by A1,A5,A6,FDIFF_1:20 .=(1/(4*a^2))*(f`|Z).x by A5,A6,FDIFF_1:def 7 .=(1/(4*a^2))*(4*a^2*x/(a|^4-x|^4)) by A2,A3,A4,A6,Th5 .=(1/(4*a^2))*((4*a^2)*(x/(a|^4-x|^4))) by XCMPLX_1:74 .=(x/(a|^4-x|^4))*(1/(4*a^2)*(4*a^2)) .=x/(a|^4-x|^4) by A7,XCMPLX_1:108; hence thesis; end; hence thesis by A1,A5,FDIFF_1:20; end; :: 5 f.x=x^2/(1+x^2) theorem Th7: Z c= dom (f1/(f2+f1)) & f1=#Z 2 & (for x st x in Z holds f2.x=1 & x<>0) implies f1/(f2+f1) is_differentiable_on Z & for x st x in Z holds ((f1/( f2+f1))`|Z).x =2*x/(1+x^2)^2 proof assume that A1: Z c= dom (f1/(f2+f1)) and A2: f1=#Z 2 and A3: for x st x in Z holds f2.x=1 & x<>0; A4: Z c= dom f1 /\ (dom (f2+f1) \ (f2+f1)"{0}) by A1,RFUNCT_1:def 1; then A5: Z c= dom (f2+f1) by XBOOLE_1:1; A6: for x st x in Z holds f1 is_differentiable_in x by A2,TAYLOR_1:2; Z c= dom f1 by A4,XBOOLE_1:18; then A7: f1 is_differentiable_on Z by A6,FDIFF_1:9; A8: for x st x in Z holds (f1`|Z).x=2*x proof let x; 2 * (x #Z (2-1))=2 * x by PREPOWER:35; then A9: diff(f1,x) =2 * x by A2,TAYLOR_1:2; assume x in Z; hence thesis by A7,A9,FDIFF_1:def 7; end; A10: for x st x in Z holds f2.x=1^2 by A3; then A11: f2+f1 is_differentiable_on Z by A2,A5,FDIFF_4:17; A12: for x st x in Z holds (f2+f1).x <> 0 proof let x; A13: 1+x^2>0+0 by XREAL_1:8,63; assume A14: x in Z; then (f2+f1).x=f2.x+f1.x by A5,VALUED_1:def 1 .=1+f1.x by A3,A14 .=1+x #Z 2 by A2,TAYLOR_1:def 1 .=1+x |^2 by PREPOWER:36 .=1+x^2 by NEWTON:81; hence thesis by A13; end; then A15: f1/(f2+f1) is_differentiable_on Z by A11,A7,FDIFF_2:21; for x st x in Z holds ((f1/(f2+f1))`|Z).x =2*x/(1+x^2)^2 proof let x; A16: f1 is_differentiable_in x by A2,TAYLOR_1:2; A17: f1.x=x #Z 2 by A2,TAYLOR_1:def 1 .=x |^2 by PREPOWER:36 .=x^2 by NEWTON:81; assume A18: x in Z; then A19: (f2+f1).x=f2.x+f1.x by A5,VALUED_1:def 1 .=1+f1.x by A3,A18 .=1+x #Z 2 by A2,TAYLOR_1:def 1 .=1+x |^2 by PREPOWER:36 .=1+x^2 by NEWTON:81; f2+f1 is_differentiable_in x & (f2+f1).x<>0 by A11,A12,A18,FDIFF_1:9; then diff(f1/(f2+f1),x) =(diff(f1,x)*(f2+f1).x - diff(f2+f1,x)*f1.x)/((f2+ f1).x)^2 by A16,FDIFF_2:14 .=((f1`|Z).x * (f2+f1).x-diff(f2+f1,x) * f1.x)/((f2+f1).x)^2 by A7,A18, FDIFF_1:def 7 .= ((f1`|Z).x * (f2+f1).x-((f2+f1)`|Z).x * f1.x)/((f2+f1).x)^2 by A11,A18 ,FDIFF_1:def 7 .=((2*x)*(f2+f1).x-((f2+f1)`|Z).x * f1.x)/((f2+f1).x)^2 by A8,A18 .=((2*x)*(1+x^2)-(2*x)*x^2)/(1+x^2)^2 by A2,A10,A5,A18,A17,A19,FDIFF_4:17 .=2*x/(1+x^2)^2; hence thesis by A15,A18,FDIFF_1:def 7; end; hence thesis by A11,A7,A12,FDIFF_2:21; end; :: 6 f.x=(1/2)*ln(x^2/(1+x^2)) theorem Z c= dom ((1/2)(#)f) & f=ln*(f1/(f2+f1)) & f1=#Z 2 & (for x st x in Z holds f2.x=1 & x<>0) implies (1/2)(#)f is_differentiable_on Z & for x st x in Z holds (((1/2)(#)f)`|Z).x =1/(x*(1+x^2)) proof assume that A1: Z c= dom ((1/2)(#)f) and A2: f=ln*(f1/(f2+f1)) and A3: f1=#Z 2 and A4: for x st x in Z holds f2.x=1 & x<>0; A5: Z c= dom f by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom (f1/(f2+f1)) by A2,FUNCT_1:11; then A6: Z c= dom (f1/(f2+f1)) by TARSKI:def 3; then A7: f1/(f2+f1) is_differentiable_on Z by A3,A4,Th7; Z c= dom f1 /\ (dom (f2+f1) \ (f2+f1)"{0}) by A6,RFUNCT_1:def 1; then A8: Z c= dom (f2+f1) by XBOOLE_1:1; A9: for x st x in Z holds (f1/(f1+f2)).x >0 proof let x; assume A10: x in Z; then A11: (f1/(f2+f1)).x=f1.x * ((f2+f1).x)" by A6,RFUNCT_1:def 1 .=f1.x/(f2+f1).x by XCMPLX_0:def 9; A12: x<>0 by A4,A10; then A13: 1+x^2>0+0 by SQUARE_1:12,XREAL_1:8; A14: f1.x=x #Z 2 by A3,TAYLOR_1:def 1 .=x |^2 by PREPOWER:36 .=x^2 by NEWTON:81; then A15: f1.x>0 by A12,SQUARE_1:12; (f2+f1).x=f2.x+f1.x by A8,A10,VALUED_1:def 1 .=1+x^2 by A4,A10,A14; hence thesis by A15,A13,A11,XREAL_1:139; end; for x st x in Z holds ln*(f1/(f2+f1)) is_differentiable_in x proof let x; assume x in Z; then f1/(f2+f1) is_differentiable_in x & (f1/(f1+f2)).x >0 by A7,A9, FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A16: f is_differentiable_on Z by A2,A5,FDIFF_1:9; for x st x in Z holds (((1/2)(#)f)`|Z).x =1/(x*(1+x^2)) proof let x; A17: f1.x=x #Z 2 by A3,TAYLOR_1:def 1 .=x |^2 by PREPOWER:36 .=x^2 by NEWTON:81; assume A18: x in Z; then A19: f1/(f2+f1) is_differentiable_in x & (f1/(f1+f2)).x >0 by A7,A9,FDIFF_1:9; x<>0 by A4,A18; then A20: 1+x^2>0+0 by SQUARE_1:12,XREAL_1:8; A21: (f2+f1).x=f2.x+f1.x by A8,A18,VALUED_1:def 1 .=1+x^2 by A4,A18,A17; A22: (f1/(f2+f1)).x=f1.x * ((f2+f1).x)" by A6,A18,RFUNCT_1:def 1 .=x^2/(1+x^2) by A17,A21,XCMPLX_0:def 9; (((1/2)(#)f)`|Z).x =(1/2)*diff(ln*(f1/(f2+f1)),x) by A1,A2,A16,A18, FDIFF_1:20 .=(1/2)*(diff((f1/(f2+f1)),x)/(f1/(f2+f1)).x) by A19,TAYLOR_1:20 .=(1/2)*(((f1/(f2+f1))`|Z).x/(f1/(f2+f1)).x) by A7,A18,FDIFF_1:def 7 .=(1/2)*((2*x/(1+x^2)^2)/(x^2/(1+x^2))) by A3,A4,A6,A18,A22,Th7 .=(1/2)*((2*x)/(1+x^2)^2)/(x^2/(1+x^2)) by XCMPLX_1:74 .=((1/2)*(2*x))/(1+x^2)^2/(x^2/(1+x^2)) by XCMPLX_1:74 .=x/(1+x^2)/(1+x^2)/(x^2/(1+x^2)) by XCMPLX_1:78 .=x/(1+x^2)/(x^2/(1+x^2))/(1+x^2) by XCMPLX_1:48 .=x/x^2/(1+x^2) by A20,XCMPLX_1:55 .=x/x/x/(1+x^2) by XCMPLX_1:78 .=1/x/(1+x^2) by A4,A18,XCMPLX_1:60 .=1/(x*(1+x^2)) by XCMPLX_1:78; hence thesis; end; hence thesis by A1,A16,FDIFF_1:20; end; :: 7 f.x=ln(x|^n) theorem Z c= dom (ln*( #Z n)) & (for x st x in Z holds x>0) implies ln*( #Z n) is_differentiable_on Z & for x st x in Z holds ((ln*( #Z n))`|Z).x =n/x proof assume that A1: Z c= dom (ln*( #Z n)) and A2: for x st x in Z holds x > 0; A3: for x st x in Z holds ln*( #Z n) is_differentiable_in x proof let x; A4: #Z n.x=x #Z n by TAYLOR_1:def 1; assume x in Z; then #Z n is_differentiable_in x & #Z n.x>0 by A2,A4,PREPOWER:39,TAYLOR_1:2 ; hence thesis by TAYLOR_1:20; end; then A5: ln*( #Z n) is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((ln*( #Z n))`|Z).x =n/x proof let x; A6: #Z n is_differentiable_in x & diff(( #Z n),x) = n * x #Z (n-1) by TAYLOR_1:2; assume A7: x in Z; then A8: x>0 by A2; A9: x |^n >0 by A2,A7,NEWTON:83; A10: #Z n.x=x #Z n by TAYLOR_1:def 1; then #Z n.x>0 by A2,A7,PREPOWER:39; then diff(ln*( #Z n),x) = n * x #Z (n-1)/x #Z n by A6,A10,TAYLOR_1:20 .=n * x #Z (n-1)/x |^ n by PREPOWER:36 .=n * (x |^ n/x |^ 1)/x |^ n by A8,PREPOWER:43 .=n * (x |^ n/x |^ 1/x |^ n) by XCMPLX_1:74 .=n * (x |^ n/x |^ n/x |^ 1) by XCMPLX_1:48 .=n * (1/(x |^ 1)) by A9,XCMPLX_1:60 .=n * (1/x) .=n*1/x by XCMPLX_1:74 .=n/x; hence thesis by A5,A7,FDIFF_1:def 7; end; hence thesis by A1,A3,FDIFF_1:9; end; :: 8 f.x=1/x+ln((x-1)/x) theorem Z c= dom (f2^+ln*(f1/f2)) & (for x st x in Z holds f2.x = x & f2.x>0 & f1.x=x-1 & f1.x >0 ) implies f2^+ln*(f1/f2) is_differentiable_on Z & for x st x in Z holds ( (f2^+ln*(f1/f2))`|Z).x= 1/(x^2*(x-1)) proof assume that A1: Z c= dom (f2^+ln*(f1/f2)) and A2: for x st x in Z holds f2.x = x & f2.x>0 & f1.x=x-1 & f1.x >0; A3: Z c= dom (f2^) /\ dom (ln*(f1/f2)) by A1,VALUED_1:def 1; then A4: Z c=dom (ln*(f1/f2)) by XBOOLE_1:18; A5: dom (f2^) c= dom f2 by RFUNCT_1:1; Z c= dom (f2^) by A3,XBOOLE_1:18; then A6: Z c= dom f2 by A5,XBOOLE_1:1; A7: for x st x in Z holds f1.x=x-1 & f1.x >0 & f2.x = x-0 & f2.x>0 by A2; then A8: ln*(f1/f2) is_differentiable_on Z by A4,FDIFF_4:24; A9: for x st x in Z holds f2.x = 0+x & f2.x<>0 by A2; then A10: f2^ is_differentiable_on Z by A6,FDIFF_4:14; for x st x in Z holds ((f2^+ln*(f1/f2))`|Z).x= 1/(x^2*(x-1)) proof let x; assume A11: x in Z; then A12: f2.x = x & f2.x>0 by A2; A13: f1.x=x-1 & f1.x >0 by A2,A11; ((f2^+ln*(f1/f2))`|Z).x =diff(f2^,x) + diff(ln*(f1/f2),x) by A1,A10,A8,A11, FDIFF_1:18 .=((f2^)`|Z).x+ diff(ln*(f1/f2),x) by A10,A11,FDIFF_1:def 7 .=((f2^)`|Z).x+((ln*(f1/f2))`|Z).x by A8,A11,FDIFF_1:def 7 .= -1/(0+x)^2+((ln*(f1/f2))`|Z).x by A6,A9,A11,FDIFF_4:14 .=-1/(0+x)^2+(1-0)/((x-1)*(x-0)) by A4,A7,A11,FDIFF_4:24 .=-(1*(x-1))/(x^2*(x-1))+1/((x-1)*x) by A13,XCMPLX_1:91 .=-(1*(x-1))/(x^2*(x-1))+(1*x)/((x-1)*x*x) by A12,XCMPLX_1:91 .=(-(x-1))/(x^2*(x-1))+x/(x^2*(x-1)) by XCMPLX_1:187 .=((-x+1)+x)/(x^2*(x-1)) by XCMPLX_1:62 .=1/(x^2*(x-1)); hence thesis; end; hence thesis by A1,A10,A8,FDIFF_1:18; end; :: 10 f.x=a #R x=exp.(x*ln a) theorem Th11: Z c= dom (exp_R*f) & (for x st x in Z holds f.x=x*log(number_e,a )) & a>0 implies exp_R*f is_differentiable_on Z & for x st x in Z holds ((exp_R *f)`|Z).x =a #R x*log(number_e,a) proof assume that A1: Z c= dom (exp_R*f) and A2: for x st x in Z holds f.x=x*log(number_e,a) and A3: a>0; for y being object st y in Z holds y in dom f by A1,FUNCT_1:11; then A4: Z c= dom f by TARSKI:def 3; A5: for x st x in Z holds f.x = log(number_e,a)*x+0 by A2; then A6: f is_differentiable_on Z by A4,FDIFF_1:23; A7: for x st x in Z holds exp_R*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x by A6,FDIFF_1:9; hence thesis by TAYLOR_1:19; end; then A8: exp_R*f is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((exp_R*f)`|Z).x = a #R x*log(number_e,a) proof let x; assume A9: x in Z; then f is_differentiable_in x by A6,FDIFF_1:9; then diff(exp_R*f,x) = exp_R.(f.x)*diff(f,x) by TAYLOR_1:19 .=exp_R.(f.x)*(f`|Z).x by A6,A9,FDIFF_1:def 7 .=exp_R.(f.x)*(log(number_e,a)) by A4,A5,A9,FDIFF_1:23 .=exp_R.(x*log(number_e,a))*(log(number_e,a)) by A2,A9 .=a #R x*log(number_e,a) by A3,Th1; hence thesis by A8,A9,FDIFF_1:def 7; end; hence thesis by A1,A7,FDIFF_1:9; end; :: 11 f.x=(a #R x)*(x-1/ln a)/ln a theorem Z c= dom ((1/log(number_e,a))(#)((exp_R*f1)(#)f2)) & (for x st x in Z holds f1.x=x*log(number_e,a) & f2.x=x-1/log(number_e,a)) & a>0 & a<>1 implies ( 1/log(number_e,a))(#)((exp_R*f1)(#)f2) is_differentiable_on Z & for x st x in Z holds (((1/log(number_e,a))(#)((exp_R*f1)(#)f2))`|Z).x =x * a #R x proof assume that A1: Z c= dom ((1/log(number_e,a))(#)((exp_R*f1)(#)f2)) and A2: for x st x in Z holds f1.x=x*log(number_e,a) & f2.x=x-1/log( number_e,a) and A3: a>0 and A4: a<>1; A5: Z c= dom ((exp_R*f1)(#)f2) by A1,VALUED_1:def 5; then A6: Z c= dom (exp_R*f1) /\ dom f2 by VALUED_1:def 4; then A7: Z c= dom (exp_R*f1) by XBOOLE_1:18; A8: for x st x in Z holds f2.x = 1*x+-1/log(number_e,a) proof let x; A9: 1*x+-1/log(number_e,a)=1*x-1/log(number_e,a); assume x in Z; hence thesis by A2,A9; end; A10: for x st x in Z holds f1.x=x*log(number_e,a) by A2; then A11: exp_R*f1 is_differentiable_on Z by A3,A7,Th11; A12: Z c= dom f2 by A6,XBOOLE_1:18; then A13: f2 is_differentiable_on Z by A8,FDIFF_1:23; then A14: ((exp_R*f1)(#)f2) is_differentiable_on Z by A5,A11,FDIFF_1:21; A15: log(number_e,a)<>0 proof A16: number_e<>1 by TAYLOR_1:11; assume log(number_e,a)=0; then log(number_e,a)=log(number_e,1) by SIN_COS2:13,TAYLOR_1:13; then a=(number_e) to_power log(number_e,1) by A3,A16,POWER:def 3 ,TAYLOR_1:11 .=1 by A16,POWER:def 3,TAYLOR_1:11; hence contradiction by A4; end; for x st x in Z holds (((1/log(number_e,a))(#)((exp_R*f1)(#)f2))`|Z).x =x * a #R x proof let x; assume A17: x in Z; then A18: (exp_R*f1).x=exp_R.(f1.x) by A7,FUNCT_1:12 .=exp_R.(x*log(number_e,a)) by A2,A17 .=a #R x by A3,Th1; (((1/log(number_e,a))(#)((exp_R*f1)(#)f2))`|Z).x =(1/log(number_e,a)) *diff((exp_R*f1)(#)f2,x) by A1,A14,A17,FDIFF_1:20 .=(1/log(number_e,a))*(((exp_R*f1)(#)f2)`|Z).x by A14,A17,FDIFF_1:def 7 .=(1/log(number_e,a))*(f2.x*diff(exp_R*f1,x)+(exp_R*f1).x*diff(f2,x)) by A5,A11,A13,A17,FDIFF_1:21 .=(1/log(number_e,a))*(f2.x*((exp_R*f1)`|Z).x+(exp_R*f1).x*diff(f2,x)) by A11,A17,FDIFF_1:def 7 .=(1/log(number_e,a))*(f2.x*((exp_R*f1)`|Z).x+(exp_R*f1).x*(f2`|Z).x) by A13,A17,FDIFF_1:def 7 .=(1/log(number_e,a))*(f2.x*(a #R x*log(number_e,a)) +(exp_R*f1).x*(f2 `|Z).x) by A3,A10,A7,A17,Th11 .=(1/log(number_e,a))*(f2.x*(a#R x*log(number_e,a))+(exp_R*f1).x*1) by A12,A8,A17,FDIFF_1:23 .=(1/log(number_e,a))*((f2.x*log(number_e,a)+1)*a #R x) by A18 .=(1/log(number_e,a))*(((x-1/log(number_e,a))* log(number_e,a)+1)*a #R x) by A2,A17 .=(1/log(number_e,a))*(x*log(number_e,a) -1/log(number_e,a)*log( number_e,a)+1)*a #R x .=(1/log(number_e,a))*(x*log(number_e,a)-1+1)*a #R x by A15,XCMPLX_1:106 .=1/log(number_e,a)*log(number_e,a)*x*a #R x .=1*x*a #R x by A15,XCMPLX_1:106 .=x*a #R x; hence thesis; end; hence thesis by A1,A14,FDIFF_1:20; end; :: 12 f.x=a #R x*exp(x)/(1+ln a) theorem Z c= dom ((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R)) & (for x st x in Z holds f.x=x*log(number_e,a)) & a>0 & a<>1/number_e implies (1/(1+log( number_e,a)))(#)((exp_R*f)(#)exp_R) is_differentiable_on Z & for x st x in Z holds (((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R))`|Z).x =a #R x*exp_R.x proof assume that A1: Z c= dom ((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R)) and A2: for x st x in Z holds f.x=x*log(number_e,a) and A3: a>0 and A4: a<>1/number_e; A5: Z c= dom ((exp_R*f)(#)exp_R) by A1,VALUED_1:def 5; then Z c= dom (exp_R*f) /\ dom exp_R by VALUED_1:def 4; then A6: Z c= dom (exp_R*f) by XBOOLE_1:18; then A7: exp_R*f is_differentiable_on Z by A2,A3,Th11; A8: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; then A9: (exp_R*f)(#)exp_R is_differentiable_on Z by A5,A7,FDIFF_1:21; A10: 1+log(number_e,a)<>0 proof A11: number_e*a>0*a by A3,TAYLOR_1:11,XREAL_1:68; assume A12: 1+log(number_e,a)=0; A13: number_e<>1 by TAYLOR_1:11; log(number_e,1)=0 by SIN_COS2:13,TAYLOR_1:13 .=log(number_e,number_e)+log(number_e,a) by A12,A13,POWER:52,TAYLOR_1:11 .=log(number_e,number_e*a) by A3,A13,POWER:53,TAYLOR_1:11; then number_e*a=(number_e) to_power log(number_e,1) by A13,A11,POWER:def 3 ,TAYLOR_1:11 .=1 by A13,POWER:def 3,TAYLOR_1:11; hence contradiction by A4,XCMPLX_1:73; end; for x st x in Z holds (((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R)) `|Z).x =a #R x*exp_R.x proof let x; assume A14: x in Z; then A15: (exp_R*f).x=exp_R.(f.x) by A6,FUNCT_1:12 .=exp_R.(x*log(number_e,a)) by A2,A14 .=a #R x by A3,Th1; (((1/(1+log(number_e,a)))(#)((exp_R*f)(#)exp_R))`|Z).x =(1/(1+log( number_e,a)))*diff((exp_R*f)(#)exp_R,x) by A1,A9,A14,FDIFF_1:20 .=(1/(1+log(number_e,a)))*(((exp_R*f)(#)exp_R)`|Z).x by A9,A14, FDIFF_1:def 7 .=(1/(1+log(number_e,a)))*(exp_R.x*diff(exp_R*f,x)+ (exp_R*f).x*diff( exp_R,x)) by A5,A7,A8,A14,FDIFF_1:21 .=(1/(1+log(number_e,a)))*(exp_R.x*((exp_R*f)`|Z).x+ (exp_R*f).x*diff( exp_R,x)) by A7,A14,FDIFF_1:def 7 .=(1/(1+log(number_e,a)))*(exp_R.x*((exp_R*f)`|Z).x+(exp_R*f).x*exp_R. x) by TAYLOR_1:16 .=(1/(1+log(number_e,a)))*((((exp_R*f)`|Z).x+(exp_R*f).x)*exp_R.x) .=(1/(1+log(number_e,a)))*((a #R x*log(number_e,a)+(exp_R*f).x)*exp_R. x) by A2,A3,A6,A14,Th11 .=(1/(1+log(number_e,a)))*(log(number_e,a)+1)*a #R x*exp_R.x by A15 .=1*a #R x*exp_R.x by A10,XCMPLX_1:106 .=a #R x*exp_R.x; hence thesis; end; hence thesis by A1,A9,FDIFF_1:20; end; :: 13 f.x=exp_R(-x) theorem Th14: Z c= dom (exp_R*f) & (for x st x in Z holds f.x=-x) implies exp_R*f is_differentiable_on Z & for x st x in Z holds ((exp_R*f)`|Z).x = - exp_R(-x) proof assume that A1: Z c= dom (exp_R*f) and A2: for x st x in Z holds f.x=-x; A3: for x st x in Z holds f.x=(-1)*x+0 proof let x; assume x in Z; then f.x=-x by A2 .=(-1)*x+0; hence thesis; end; for y being object st y in Z holds y in dom f by A1,FUNCT_1:11; then A4: Z c= dom f by TARSKI:def 3; then A5: f is_differentiable_on Z by A3,FDIFF_1:23; A6: for x st x in Z holds exp_R*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x by A5,FDIFF_1:9; hence thesis by TAYLOR_1:19; end; then A7: exp_R*f is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((exp_R*f)`|Z).x = -exp_R(-x) proof let x; assume A8: x in Z; then f is_differentiable_in x by A5,FDIFF_1:9; then diff(exp_R*f,x) = exp_R.(f.x)*diff(f,x) by TAYLOR_1:19 .=exp_R.(f.x)*(f`|Z).x by A5,A8,FDIFF_1:def 7 .=exp_R.(f.x)*(-1) by A4,A3,A8,FDIFF_1:23 .=exp_R.(-x)*(-1) by A2,A8 .=-exp_R.(-x) .=-exp_R(-x) by SIN_COS:def 23; hence thesis by A7,A8,FDIFF_1:def 7; end; hence thesis by A1,A6,FDIFF_1:9; end; :: 14 f.x=-(x+1)*exp_R(-x) theorem Z c= dom (f1(#)(exp_R*f2)) & (for x st x in Z holds f1.x=-x-1 & f2.x=- x) implies f1(#)(exp_R*f2) is_differentiable_on Z & for x st x in Z holds ((f1 (#)(exp_R*f2))`|Z).x = x/exp_R(x) proof assume that A1: Z c= dom (f1(#)(exp_R*f2)) and A2: for x st x in Z holds f1.x=-x-1 & f2.x=-x; A3: Z c= dom f1 /\ dom (exp_R*f2) by A1,VALUED_1:def 4; then A4: Z c= dom f1 by XBOOLE_1:18; A5: Z c= dom (exp_R*f2) by A3,XBOOLE_1:18; A6: for x st x in Z holds f1.x=(-1)*x+-1 proof let x; assume x in Z; then f1.x=-x-1 by A2 .=(-1)*x+-1; hence thesis; end; then A7: f1 is_differentiable_on Z by A4,FDIFF_1:23; A8: for x st x in Z holds f2.x=-x by A2; then A9: exp_R*f2 is_differentiable_on Z by A5,Th14; for x st x in Z holds ((f1(#)(exp_R*f2))`|Z).x = x/exp_R(x) proof let x; assume A10: x in Z; then A11: (exp_R*f2).x=exp_R.(f2.x) by A5,FUNCT_1:12 .=exp_R.(-x) by A2,A10 .=exp_R(-x) by SIN_COS:def 23; ((f1(#)(exp_R*f2))`|Z).x =((exp_R*f2).x)*diff(f1,x) + (f1.x)*diff( exp_R*f2,x) by A1,A7,A9,A10,FDIFF_1:21 .=exp_R(-x)*diff(f1,x) + (-x-1)*diff(exp_R*f2,x) by A2,A10,A11 .=exp_R(-x)*(f1`|Z).x + (-x-1)*diff(exp_R*f2,x) by A7,A10,FDIFF_1:def 7 .=exp_R(-x)*(f1`|Z).x + (-x-1)*((exp_R*f2)`|Z).x by A9,A10,FDIFF_1:def 7 .=exp_R(-x)*(-1) + (-x-1)*((exp_R*f2)`|Z).x by A4,A6,A10,FDIFF_1:23 .=exp_R(-x)*(-1) + (-x-1)*(-exp_R(-x)) by A8,A5,A10,Th14 .=x*exp_R(-x) .=x*(1/exp_R(x)) by TAYLOR_1:4 .=x/exp_R(x) by XCMPLX_1:99; hence thesis; end; hence thesis by A1,A7,A9,FDIFF_1:21; end; :: 16 f.x=a #R (-x)=exp_R.(-x*ln a) theorem Th16: Z c= dom -(exp_R*f) & (for x st x in Z holds f.x=-x*log(number_e ,a)) & a>0 implies -(exp_R*f) is_differentiable_on Z & for x st x in Z holds (( -(exp_R*f))`|Z).x =a #R (-x)*log(number_e,a) proof assume that A1: Z c= dom -(exp_R*f) and A2: for x st x in Z holds f.x=-x*log(number_e,a) and A3: a>0; A4: Z c= dom (exp_R*f) by A1,VALUED_1:8; then for y being object st y in Z holds y in dom f by FUNCT_1:11; then A5: Z c= dom f by TARSKI:def 3; A6: for x st x in Z holds f.x = (-log(number_e,a))*x+0 proof let x; assume x in Z; then f.x=-log(number_e,a)*x by A2 .=(-log(number_e,a))*x+0; hence thesis; end; then A7: f is_differentiable_on Z by A5,FDIFF_1:23; for x st x in Z holds exp_R*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x by A7,FDIFF_1:9; hence thesis by TAYLOR_1:19; end; then A8: exp_R*f is_differentiable_on Z by A4,FDIFF_1:9; A9: for x st x in Z holds ((-(exp_R*f))`|Z).x = a #R (-x)*log(number_e,a) proof let x; assume A10: x in Z; then A11: f is_differentiable_in x by A7,FDIFF_1:9; ((-(exp_R*f))`|Z).x=(-1)*diff(exp_R*f,x) by A1,A8,A10,FDIFF_1:20 .=(-1)*(exp_R.(f.x)*diff(f,x)) by A11,TAYLOR_1:19 .=(-1)*(exp_R.(f.x)*(f`|Z).x ) by A7,A10,FDIFF_1:def 7 .=(-1)*(exp_R.(f.x)*(-log(number_e,a))) by A5,A6,A10,FDIFF_1:23 .=(-1)*(exp_R.(-x*log(number_e,a))*(-log(number_e,a))) by A2,A10 .=(-1)*(a #R (-x)*(-log(number_e,a))) by A3,Th2 .=a #R (-x)*log(number_e,a); hence thesis; end; Z c= dom ((-1)(#)(exp_R*f)) by A1; hence thesis by A8,A9,FDIFF_1:20; end; :: 17 f.x=-(a #R -x)*(x+1/ln a)/ln a theorem Z c= dom ((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2)) & (for x st x in Z holds f1.x=-x*log(number_e,a) & f2.x=x+1/log(number_e,a)) & a>0 & a<>1 implies (1/log(number_e,a))(#)((-(exp_R*f1))(#)f2) is_differentiable_on Z & for x st x in Z holds (((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2))`|Z).x =x /a #R x proof assume that A1: Z c= dom ((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2)) and A2: for x st x in Z holds f1.x=-x*log(number_e,a) & f2.x=x+1/log( number_e,a) and A3: a>0 and A4: a<>1; A5: for x st x in Z holds f2.x = 1*x+1/log(number_e,a) by A2; A6: Z c= dom ((-(exp_R*f1))(#)f2) by A1,VALUED_1:def 5; then A7: Z c= dom (-(exp_R*f1)) /\ dom f2 by VALUED_1:def 4; then A8: Z c= dom (-(exp_R*f1)) by XBOOLE_1:18; A9: for x st x in Z holds f1.x=-x*log(number_e,a) by A2; then A10: -(exp_R*f1) is_differentiable_on Z by A3,A8,Th16; A11: Z c= dom f2 by A7,XBOOLE_1:18; then A12: f2 is_differentiable_on Z by A5,FDIFF_1:23; then A13: (-(exp_R*f1))(#)f2 is_differentiable_on Z by A6,A10,FDIFF_1:21; A14: log(number_e,a)<>0 proof A15: number_e<>1 by TAYLOR_1:11; assume log(number_e,a)=0; then log(number_e,a)=log(number_e,1) by SIN_COS2:13,TAYLOR_1:13; then a=(number_e) to_power log(number_e,1) by A3,A15,POWER:def 3 ,TAYLOR_1:11 .=1 by A15,POWER:def 3,TAYLOR_1:11; hence contradiction by A4; end; for x st x in Z holds (((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2))`|Z) .x =x /a #R x proof let x; assume A16: x in Z; then x in dom -(exp_R*f1) by A8; then A17: x in dom (exp_R*f1) by VALUED_1:8; A18: (-(exp_R*f1)).x=-((exp_R*f1).x) by VALUED_1:8 .=-(exp_R.(f1.x)) by A17,FUNCT_1:12 .=-(exp_R.(-x*log(number_e,a))) by A2,A16 .=-a #R (-x) by A3,Th2; (((1/log(number_e,a))(#)((-(exp_R*f1))(#)f2))`|Z).x =(1/log(number_e, a))*diff((-(exp_R*f1))(#)f2,x) by A1,A13,A16,FDIFF_1:20 .=(1/log(number_e,a))*(((-(exp_R*f1))(#)f2)`|Z).x by A13,A16, FDIFF_1:def 7 .=(1/log(number_e,a))*(f2.x*diff(-(exp_R*f1),x)+ (-(exp_R*f1)).x*diff( f2,x)) by A6,A10,A12,A16,FDIFF_1:21 .=(1/log(number_e,a))*(f2.x*((-(exp_R*f1))`|Z).x+ (-(exp_R*f1)).x*diff (f2,x)) by A10,A16,FDIFF_1:def 7 .=(1/log(number_e,a))*(f2.x*((-(exp_R*f1))`|Z).x+ (-(exp_R*f1)).x*(f2 `|Z).x) by A12,A16,FDIFF_1:def 7 .=(1/log(number_e,a))*(f2.x*(a #R (-x)*log(number_e,a)) +(-(exp_R*f1)) .x*(f2`|Z).x) by A3,A9,A8,A16,Th16 .=(1/log(number_e,a))*(f2.x*(a #R (-x)*log(number_e,a)) +(-(exp_R*f1)) .x*1) by A11,A5,A16,FDIFF_1:23 .=(1/log(number_e,a))*((f2.x*log(number_e,a)-1)*a #R (-x)) by A18 .=(1/log(number_e,a))*(((x+1/log(number_e,a))* log(number_e,a)-1)*a #R (-x)) by A2,A16 .=(1/log(number_e,a))* (x*log(number_e,a)+1/log(number_e,a)*log( number_e,a)-1)*a #R (-x) .=(1/log(number_e,a))*(x*log(number_e,a)+1-1)*a #R (-x) by A14, XCMPLX_1:106 .=(1/log(number_e,a))*log(number_e,a)*x*a #R (-x) .=1*x*a #R (-x) by A14,XCMPLX_1:106 .=x*(1/a #R x) by A3,PREPOWER:76 .=x/a #R x by XCMPLX_1:99; hence thesis; end; hence thesis by A1,A13,FDIFF_1:20; end; :: 18 f.x=(1/(ln a-1))*a #R x/exp_R(x) theorem Z c= dom ((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R)) & (for x st x in Z holds f.x=x*log(number_e,a)) & a>0 & a<>number_e implies (1/(log(number_e, a)-1))(#)((exp_R*f)/exp_R) is_differentiable_on Z & for x st x in Z holds (((1/ (log(number_e,a)-1))(#)((exp_R*f)/exp_R))`|Z).x =a #R x/exp_R.x proof assume that A1: Z c= dom ((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R)) and A2: for x st x in Z holds f.x=x*log(number_e,a) and A3: a>0 and A4: a<>number_e; Z c= dom ((exp_R*f)/exp_R) by A1,VALUED_1:def 5; then Z c= dom (exp_R*f) /\ (dom exp_R \ (exp_R)"{0}) by RFUNCT_1:def 1; then A5: Z c= dom (exp_R*f) by XBOOLE_1:18; then A6: exp_R*f is_differentiable_on Z by A2,A3,Th11; exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by FDIFF_1:26 ,SIN_COS:54,TAYLOR_1:16; then A7: (exp_R*f)/exp_R is_differentiable_on Z by A6,FDIFF_2:21; A8: log(number_e,a)-1<>0 proof A9: number_e<>1 by TAYLOR_1:11; assume log(number_e,a)-1=0; then log(number_e,a)=log(number_e,number_e) by A9,POWER:52,TAYLOR_1:11; then a=(number_e) to_power log(number_e,number_e) by A3,A9,POWER:def 3 ,TAYLOR_1:11 .=number_e by A9,POWER:def 3,TAYLOR_1:11; hence contradiction by A4; end; for x st x in Z holds (((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R))`|Z ).x =a #R x/exp_R.x proof let x; A10: exp_R.x <>0 by SIN_COS:54; assume A11: x in Z; then A12: (exp_R*f).x=exp_R.(f.x) by A5,FUNCT_1:12 .=exp_R.(x*log(number_e,a)) by A2,A11 .=a #R x by A3,Th1; A13: exp_R is_differentiable_in x & exp_R*f is_differentiable_in x by A6,A11, FDIFF_1:9,SIN_COS:65; (((1/(log(number_e,a)-1))(#)((exp_R*f)/exp_R))`|Z).x =(1/(log( number_e,a)-1))*diff(((exp_R*f)/exp_R),x) by A1,A7,A11,FDIFF_1:20 .=(1/(log(number_e,a)-1))* ((diff(exp_R*f,x) * exp_R.x - diff(exp_R,x) *(exp_R*f).x)/(exp_R.x)^2) by A13,A10,FDIFF_2:14 .=(1/(log(number_e,a)-1))*((diff(exp_R*f,x)* exp_R.x-exp_R.x*a #R x)/( exp_R.x)^2) by A12,SIN_COS:65 .=(1/(log(number_e,a)-1))*(((diff(exp_R*f,x)-a #R x)*exp_R.x)/ ((exp_R .x)*(exp_R.x))) .=(1/(log(number_e,a)-1))*((diff(exp_R*f,x)-a #R x)/(exp_R.x)) by A10, XCMPLX_1:91 .=(1/(log(number_e,a)-1))*(diff(exp_R*f,x)-a #R x)/(exp_R.x) by XCMPLX_1:74 .=(1/(log(number_e,a)-1))*(((exp_R*f)`|Z).x-a #R x)/(exp_R.x) by A6,A11, FDIFF_1:def 7 .=(1/(log(number_e,a)-1))*(a #R x*log(number_e,a)-a #R x)/(exp_R.x) by A2 ,A3,A5,A11,Th11 .=(1/(log(number_e,a)-1))*(log(number_e,a)-1)*a #R x/exp_R.x .=1* a #R x/exp_R.x by A8,XCMPLX_1:106 .=a #R x/exp_R.x; hence thesis; end; hence thesis by A1,A7,FDIFF_1:20; end; :: 19 f.x=(1/(1-ln a))*exp_R(x)/a #R x theorem Z c= dom ((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f))) & (for x st x in Z holds f.x=x*log(number_e,a)) & a>0 & a<>number_e implies (1/(1-log( number_e,a)))(#)(exp_R/(exp_R*f)) is_differentiable_on Z & for x st x in Z holds (((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f)))`|Z).x =exp_R.x/a #R x proof assume that A1: Z c= dom ((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f))) and A2: for x st x in Z holds f.x=x*log(number_e,a) and A3: a>0 and A4: a<>number_e; Z c= dom (exp_R/(exp_R*f)) by A1,VALUED_1:def 5; then Z c= dom exp_R /\ (dom (exp_R*f) \ (exp_R*f)"{0}) by RFUNCT_1:def 1; then A5: Z c= dom (exp_R*f) by XBOOLE_1:1; then A6: exp_R*f is_differentiable_on Z by A2,A3,Th11; A7: for x st x in Z holds (exp_R*f).x<>0 proof let x; assume x in Z; then (exp_R*f).x=exp_R.(f.x) by A5,FUNCT_1:12; hence thesis by SIN_COS:54; end; exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; then A8: exp_R/(exp_R*f) is_differentiable_on Z by A6,A7,FDIFF_2:21; A9: 1-log(number_e,a)<>0 proof A10: number_e<>1 by TAYLOR_1:11; assume 1-log(number_e,a)=0; then log(number_e,a)=log(number_e,number_e) by A10,POWER:52,TAYLOR_1:11; then a=(number_e) to_power log(number_e,number_e) by A3,A10,POWER:def 3 ,TAYLOR_1:11 .=number_e by A10,POWER:def 3,TAYLOR_1:11; hence contradiction by A4; end; for x st x in Z holds (((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f)))`|Z ).x =exp_R.x/a #R x proof let x; A11: exp_R is_differentiable_in x by SIN_COS:65; A12: a #R x >0 by A3,PREPOWER:81; assume A13: x in Z; then A14: (exp_R*f).x=exp_R.(f.x) by A5,FUNCT_1:12 .=exp_R.(x*log(number_e,a)) by A2,A13 .=a #R x by A3,Th1; A15: exp_R*f is_differentiable_in x & (exp_R*f).x <>0 by A6,A7,A13,FDIFF_1:9; (((1/(1-log(number_e,a)))(#)(exp_R/(exp_R*f)))`|Z).x =(1/(1-log( number_e,a)))*diff((exp_R/(exp_R*f)),x) by A1,A8,A13,FDIFF_1:20 .=(1/(1-log(number_e,a)))* ((diff(exp_R,x) * (exp_R*f).x - diff((exp_R *f),x) * exp_R.x)/((exp_R*f).x)^2) by A11,A15,FDIFF_2:14 .=(1/(1-log(number_e,a)))* ((exp_R.x * a #R x - diff((exp_R*f),x)* exp_R.x)/(a #R x)^2) by A14,SIN_COS:65 .=(1/(1-log(number_e,a)))*((exp_R.x*(a #R x -diff((exp_R*f),x)))/(a #R x)^2) .=(1/(1-log(number_e,a)))*((exp_R.x*(a #R x - ((exp_R*f)`|Z).x))/(a #R x)^2) by A6,A13,FDIFF_1:def 7 .=(1/(1-log(number_e,a)))* ((exp_R.x*(a #R x -a #R x*log(number_e,a))) /(a #R x)^2) by A2,A3,A5,A13,Th11 .=(1/(1-log(number_e,a)))*((1-log(number_e,a))*exp_R.x*a #R x)/ (a #R x)^2 by XCMPLX_1:74 .=(1/(1-log(number_e,a)))*(1-log(number_e,a))*exp_R.x*a #R x/(a #R x) ^2 .=1*exp_R.x*a #R x/(a #R x)^2 by A9,XCMPLX_1:106 .=exp_R.x/a #R x by A12,XCMPLX_1:91; hence thesis; end; hence thesis by A1,A8,FDIFF_1:20; end; :: 20 f.x=ln(exp_R.x+1) theorem Z c= dom (ln*(exp_R+f)) & (for x st x in Z holds f.x=1 ) implies ln*( exp_R+f) is_differentiable_on Z & for x st x in Z holds ((ln*(exp_R+f))`|Z).x = exp_R.x/(exp_R.x+1) proof assume that A1: Z c= dom (ln*(exp_R+f)) and A2: for x st x in Z holds f.x=1; A3: for x st x in Z holds f.x=0*x+1 by A2; for y being object st y in Z holds y in dom (exp_R+f) by A1,FUNCT_1:11; then A4: Z c= dom (exp_R+f) by TARSKI:def 3; then Z c= dom exp_R /\ dom f by VALUED_1:def 1; then A5: Z c= dom f by XBOOLE_1:18; then A6: f is_differentiable_on Z by A3,FDIFF_1:23; A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; then A8: exp_R+f is_differentiable_on Z by A4,A6,FDIFF_1:18; A9: for x st x in Z holds ((exp_R+f)`|Z).x =exp_R.x proof let x; assume A10: x in Z; hence ((exp_R+f)`|Z).x = diff(exp_R,x) + diff(f,x) by A4,A6,A7,FDIFF_1:18 .=exp_R.x+ diff(f,x) by SIN_COS:65 .=exp_R.x+(f`|Z).x by A6,A10,FDIFF_1:def 7 .=exp_R.x+0 by A5,A3,A10,FDIFF_1:23 .=exp_R.x; end; A11: for x st x in Z holds (exp_R+f).x>0 proof let x; assume A12: x in Z; then (exp_R+f).x=exp_R.x + f.x by A4,VALUED_1:def 1 .=exp_R.x +1 by A2,A12; hence thesis by SIN_COS:54,XREAL_1:34; end; A13: for x st x in Z holds ln*(exp_R+f) is_differentiable_in x proof let x; assume x in Z; then exp_R+f is_differentiable_in x & (exp_R+f).x >0 by A8,A11,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A14: ln*(exp_R+f) is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((ln*(exp_R+f))`|Z).x = exp_R.x/(exp_R.x+1) proof let x; assume A15: x in Z; then A16: (exp_R+f).x=exp_R.x + f.x by A4,VALUED_1:def 1 .=exp_R.x +1 by A2,A15; exp_R+f is_differentiable_in x & (exp_R+f).x>0 by A8,A11,A15,FDIFF_1:9; then diff(ln*(exp_R+f),x) =diff((exp_R+f),x)/((exp_R+f).x) by TAYLOR_1:20 .=((exp_R+f)`|Z).x/((exp_R+f).x) by A8,A15,FDIFF_1:def 7 .=exp_R.x/(exp_R.x +1) by A9,A15,A16; hence thesis by A14,A15,FDIFF_1:def 7; end; hence thesis by A1,A13,FDIFF_1:9; end; :: 21 f.x=ln(exp_R.x-1) theorem Z c= dom (ln*(exp_R-f)) & (for x st x in Z holds f.x=1 & (exp_R-f).x>0 ) implies ln*(exp_R-f) is_differentiable_on Z & for x st x in Z holds ((ln*( exp_R-f))`|Z).x = exp_R.x/(exp_R.x-1) proof assume that A1: Z c= dom (ln*(exp_R-f)) and A2: for x st x in Z holds f.x=1 & (exp_R-f).x>0; A3: for x st x in Z holds f.x=0*x+1 by A2; for y being object st y in Z holds y in dom (exp_R-f) by A1,FUNCT_1:11; then A4: Z c= dom (exp_R-f) by TARSKI:def 3; then Z c= dom exp_R /\ dom f by VALUED_1:12; then A5: Z c= dom f by XBOOLE_1:18; then A6: f is_differentiable_on Z by A3,FDIFF_1:23; A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; then A8: exp_R-f is_differentiable_on Z by A4,A6,FDIFF_1:19; A9: for x st x in Z holds ((exp_R-f)`|Z).x =exp_R.x proof let x; assume A10: x in Z; hence ((exp_R-f)`|Z).x = diff(exp_R,x) - diff(f,x) by A4,A6,A7,FDIFF_1:19 .= exp_R.x- diff(f,x) by SIN_COS:65 .= exp_R.x-(f`|Z).x by A6,A10,FDIFF_1:def 7 .= exp_R.x-0 by A5,A3,A10,FDIFF_1:23 .= exp_R.x; end; A11: for x st x in Z holds ln*(exp_R-f) is_differentiable_in x proof let x; assume x in Z; then exp_R-f is_differentiable_in x & (exp_R-f).x >0 by A2,A8,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A12: ln*(exp_R-f) is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((ln*(exp_R-f))`|Z).x = exp_R.x/(exp_R.x-1) proof let x; assume A13: x in Z; then A14: (exp_R-f).x=exp_R.x - f.x by A4,VALUED_1:13 .=exp_R.x -1 by A2,A13; (exp_R-f) is_differentiable_in x & (exp_R-f).x >0 by A2,A8,A13,FDIFF_1:9; then diff(ln*(exp_R-f),x) =diff((exp_R-f),x)/((exp_R-f).x) by TAYLOR_1:20 .=((exp_R-f)`|Z).x/((exp_R-f).x) by A8,A13,FDIFF_1:def 7 .=exp_R.x/(exp_R.x -1) by A9,A13,A14; hence thesis by A12,A13,FDIFF_1:def 7; end; hence thesis by A1,A11,FDIFF_1:9; end; :: 22 f.x=-ln(1-exp_R.x) theorem Z c= dom -(ln*(f-exp_R)) & (for x st x in Z holds f.x=1 & (f-exp_R).x> 0) implies -(ln*(f-exp_R)) is_differentiable_on Z & for x st x in Z holds ( (- ln*(f-exp_R)) `|Z).x = exp_R.x/(1-exp_R.x) proof assume that A1: Z c= dom -(ln*(f-exp_R)) and A2: for x st x in Z holds f.x=1 & (f-exp_R).x>0; A3: for x st x in Z holds f.x=0*x+1 by A2; A4: Z c= dom (ln*(f-exp_R)) by A1,VALUED_1:8; then for y being object st y in Z holds y in dom (f-exp_R) by FUNCT_1:11; then A5: Z c= dom (f-exp_R) by TARSKI:def 3; then Z c= dom exp_R /\ dom f by VALUED_1:12; then A6: Z c= dom f by XBOOLE_1:18; then A7: f is_differentiable_on Z by A3,FDIFF_1:23; A8: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; then A9: f-exp_R is_differentiable_on Z by A5,A7,FDIFF_1:19; for x st x in Z holds ln*(f-exp_R) is_differentiable_in x proof let x; assume x in Z; then f-exp_R is_differentiable_in x & (f-exp_R).x >0 by A2,A9,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A10: ln*(f-exp_R) is_differentiable_on Z by A4,FDIFF_1:9; A11: for x st x in Z holds ((f-exp_R)`|Z).x =-exp_R.x proof let x; assume A12: x in Z; hence ((f-exp_R)`|Z).x =diff(f,x)-diff(exp_R,x) by A5,A7,A8,FDIFF_1:19 .= diff(f,x)-exp_R.x by SIN_COS:65 .= (f`|Z).x-exp_R.x by A7,A12,FDIFF_1:def 7 .=0-exp_R.x by A6,A3,A12,FDIFF_1:23 .=-exp_R.x; end; A13: for x st x in Z holds ( (-ln*(f-exp_R)) `|Z).x = exp_R.x/(1-exp_R.x) proof let x; assume A14: x in Z; then A15: (f-exp_R).x=f.x-exp_R.x by A5,VALUED_1:13 .=1-exp_R.x by A2,A14; A16: (f-exp_R) is_differentiable_in x & (f-exp_R).x >0 by A2,A9,A14,FDIFF_1:9; (((-1)(#)(ln*(f-exp_R)))`|Z).x =(-1)*diff((ln*(f-exp_R)),x) by A1,A10,A14, FDIFF_1:20 .=(-1)*(diff((f-exp_R),x)/((f-exp_R).x)) by A16,TAYLOR_1:20 .=(-1)*(((f-exp_R)`|Z).x/(f-exp_R).x) by A9,A14,FDIFF_1:def 7 .=(-1)*((-exp_R.x)/(1-exp_R.x)) by A11,A14,A15 .=((-1)*(-exp_R.x))/(1-exp_R.x) by XCMPLX_1:74 .=exp_R.x/(1-exp_R.x); hence thesis; end; Z c= dom ((-1)(#)(ln*(f-exp_R))) by A1; hence thesis by A10,A13,FDIFF_1:20; end; :: 23 f.x=exp_R(2*x)+1 theorem Th23: Z c= dom ((( #Z 2)*exp_R)+f) & (for x st x in Z holds f.x=1) implies (( #Z 2)*exp_R)+f is_differentiable_on Z & for x st x in Z holds (((( #Z 2)*exp_R)+f)`|Z).x =2*exp_R(2*x) proof assume that A1: Z c= dom ((( #Z 2)*exp_R)+f) and A2: for x st x in Z holds f.x=1; A3: Z c= dom (( #Z 2)*exp_R) /\ dom f by A1,VALUED_1:def 1; then A4: Z c= dom f by XBOOLE_1:18; A5: now let x; assume x in Z; exp_R is_differentiable_in x by SIN_COS:65; hence ( #Z 2)*exp_R is_differentiable_in x by TAYLOR_1:3; end; A6: for x st x in Z holds f.x=0*x+1 by A2; then A7: f is_differentiable_on Z by A4,FDIFF_1:23; Z c= dom (( #Z 2)*exp_R) by A3,XBOOLE_1:18; then A8: ( #Z 2)*exp_R is_differentiable_on Z by A5,FDIFF_1:9; for x st x in Z holds (((( #Z 2)*exp_R)+f)`|Z).x =2*exp_R(2*x) proof let x; A9: exp_R is_differentiable_in x by SIN_COS:65; assume A10: x in Z; then (((( #Z 2)*exp_R)+f)`|Z).x =diff(( #Z 2)*exp_R,x)+diff(f,x) by A1,A7,A8, FDIFF_1:18 .=(2*( (exp_R.x) #Z (2-1)) * diff(exp_R,x))+diff(f,x) by A9,TAYLOR_1:3 .=2*( (exp_R.x) #Z (2-1)) * exp_R.x+diff(f,x) by SIN_COS:65 .=2* exp_R.x * exp_R.x+diff(f,x) by PREPOWER:35 .=2*( exp_R.x * exp_R.x)+diff(f,x) .=2*( exp_R( x )* exp_R.x)+diff(f,x) by SIN_COS:def 23 .=2*( exp_R( x )* exp_R(x))+diff(f,x) by SIN_COS:def 23 .=2*(exp_R(x+x))+diff(f,x) by SIN_COS:50 .=2* exp_R(2*x)+(f`|Z).x by A7,A10,FDIFF_1:def 7 .= 2* exp_R(2*x)+0 by A4,A6,A10,FDIFF_1:23 .=2* exp_R(2*x); hence thesis; end; hence thesis by A1,A7,A8,FDIFF_1:18; end; :: 24 f.x=(1/2)*ln(exp_R(2*x)+1) theorem Z c= dom ((1/2)(#)(ln*f)) & f=(( #Z 2)*exp_R)+f1 & (for x st x in Z holds f1.x=1) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)+exp_R(-x)) proof assume that A1: Z c= dom ((1/2)(#)(ln*f)) and A2: f=(( #Z 2)*exp_R)+f1 and A3: for x st x in Z holds f1.x=1; A4: Z c= dom (ln*f) by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom f by FUNCT_1:11; then A5: Z c= dom ((( #Z 2)*exp_R)+f1) by A2,TARSKI:def 3; then A6: (( #Z 2)*exp_R)+f1 is_differentiable_on Z by A3,Th23; Z c= dom (( #Z 2)*exp_R) /\ dom f1 by A5,VALUED_1:def 1; then A7: Z c= dom (( #Z 2)*exp_R) by XBOOLE_1:18; A8: for x st x in Z holds f.x >0 proof let x; A9: (exp_R.x) #Z 2>0 by PREPOWER:39,SIN_COS:54; assume A10: x in Z; then ((( #Z 2)*exp_R)+f1).x =(( #Z 2)*exp_R).x+f1.x by A5,VALUED_1:def 1 .=( #Z 2).(exp_R.x)+f1.x by A7,A10,FUNCT_1:12 .=(exp_R.x) #Z 2+f1.x by TAYLOR_1:def 1 .=(exp_R.x) #Z 2+1 by A3,A10; hence thesis by A2,A9; end; for x st x in Z holds ln*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A11: ln*f is_differentiable_on Z by A4,FDIFF_1:9; for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)+exp_R (-x)) proof let x; A12: exp_R(x)>0 by SIN_COS:55; assume A13: x in Z; then A14: f is_differentiable_in x & f.x >0 by A2,A6,A8,FDIFF_1:9; A15: ((( #Z 2)*exp_R)+f1).x =(( #Z 2)*exp_R).x+f1.x by A5,A13,VALUED_1:def 1 .=( #Z 2).(exp_R.x)+f1.x by A7,A13,FUNCT_1:12 .=(exp_R.x) #Z 2+f1.x by TAYLOR_1:def 1 .=(exp_R.x) #Z 2+1 by A3,A13 .=(exp_R(x)) #Z (1+1)+1 by SIN_COS:def 23 .=(exp_R(x)) #Z 1 * (exp_R(x)) #Z 1 +1 by A12,PREPOWER:44 .=exp_R(x) * (exp_R(x)) #Z 1 +1 by PREPOWER:35 .=exp_R(x) * exp_R(x) +1 by PREPOWER:35; (((1/2)(#)(ln*f))`|Z).x =(1/2)*diff((ln*f),x) by A1,A11,A13,FDIFF_1:20 .=(1/2)*(diff(f,x)/f.x) by A14,TAYLOR_1:20 .=(1/2)*((((( #Z 2)*exp_R)+f1)`|Z).x/((( #Z 2)*exp_R)+f1).x) by A2,A6,A13 ,FDIFF_1:def 7 .=(1/2)*((2*exp_R(2*x))/(exp_R(x) * exp_R(x) +1)) by A3,A5,A13,A15,Th23 .=(1/2)*(2*exp_R(2*x))/(exp_R(x) * exp_R(x) +1) by XCMPLX_1:74 .=(exp_R(x+x)/exp_R(x))/((exp_R(x) * exp_R(x)+1)/exp_R(x)) by A12, XCMPLX_1:55 .=((exp_R(x)*exp_R(x))/exp_R(x))/((exp_R(x) * exp_R(x)+1)/exp_R(x)) by SIN_COS:50 .=(exp_R(x)*exp_R(x)/exp_R(x))/(exp_R(x) * exp_R(x)/exp_R(x)+1/exp_R(x )) by XCMPLX_1:62 .=exp_R(x)/(exp_R(x) * exp_R(x)/exp_R(x)+1/exp_R(x)) by A12,XCMPLX_1:89 .=exp_R(x)/(exp_R(x)+1/exp_R(x)) by A12,XCMPLX_1:89 .=exp_R(x)/(exp_R(x)+exp_R(-x)) by TAYLOR_1:4; hence thesis; end; hence thesis by A1,A11,FDIFF_1:20; end; :: 25 f.x=exp_R(2*x)-1 theorem Th25: Z c= dom ((( #Z 2)*exp_R)-f) & (for x st x in Z holds f.x=1) implies (( #Z 2)*exp_R)-f is_differentiable_on Z & for x st x in Z holds (((( #Z 2)*exp_R)-f)`|Z).x =2*exp_R(2*x) proof assume that A1: Z c= dom ((( #Z 2)*exp_R)-f) and A2: for x st x in Z holds f.x=1; A3: Z c= dom (( #Z 2)*exp_R) /\ dom f by A1,VALUED_1:12; then A4: Z c= dom f by XBOOLE_1:18; A5: now let x; assume x in Z; exp_R is_differentiable_in x by SIN_COS:65; hence ( #Z 2)*exp_R is_differentiable_in x by TAYLOR_1:3; end; A6: for x st x in Z holds f.x=0*x+1 by A2; then A7: f is_differentiable_on Z by A4,FDIFF_1:23; Z c= dom (( #Z 2)*exp_R) by A3,XBOOLE_1:18; then A8: ( #Z 2)*exp_R is_differentiable_on Z by A5,FDIFF_1:9; for x st x in Z holds (((( #Z 2)*exp_R)-f)`|Z).x =2*exp_R(2*x) proof let x; A9: exp_R is_differentiable_in x by SIN_COS:65; assume A10: x in Z; then (((( #Z 2)*exp_R)-f)`|Z).x =diff(( #Z 2)*exp_R,x)-diff(f,x) by A1,A7,A8, FDIFF_1:19 .=(2*((exp_R.x) #Z (2-1)) * diff(exp_R,x))-diff(f,x) by A9,TAYLOR_1:3 .=2*((exp_R.x) #Z 1) * exp_R.x-diff(f,x) by SIN_COS:65 .=2* exp_R.x * exp_R.x-diff(f,x) by PREPOWER:35 .=2*(exp_R.x * exp_R.x)-diff(f,x) .=2*(exp_R(x)* exp_R.x)-diff(f,x) by SIN_COS:def 23 .=2*(exp_R(x)* exp_R(x))-diff(f,x) by SIN_COS:def 23 .=2*(exp_R(x+x))-diff(f,x) by SIN_COS:50 .=2* exp_R(2*x)-(f`|Z).x by A7,A10,FDIFF_1:def 7 .= 2* exp_R(2*x)-0 by A4,A6,A10,FDIFF_1:23 .=2* exp_R(2*x); hence thesis; end; hence thesis by A1,A7,A8,FDIFF_1:19; end; :: 26 f.x=(1/2)*ln(exp_R(2*x)-1) theorem Z c= dom ((1/2)(#)(ln*f)) & f=(( #Z 2)*exp_R)-f1 & (for x st x in Z holds f1.x=1 & f.x>0) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)-exp_R(-x)) proof assume that A1: Z c= dom ((1/2)(#)(ln*f)) and A2: f=(( #Z 2)*exp_R)-f1 and A3: for x st x in Z holds f1.x=1 & f.x>0; A4: Z c= dom (ln*f) by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom f by FUNCT_1:11; then A5: Z c= dom ((( #Z 2)*exp_R)-f1) by A2,TARSKI:def 3; A6: for x st x in Z holds f1.x=1 by A3; then A7: (( #Z 2)*exp_R)-f1 is_differentiable_on Z by A5,Th25; for x st x in Z holds ln*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x & f.x >0 by A2,A3,A7,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A8: ln*f is_differentiable_on Z by A4,FDIFF_1:9; Z c= dom (( #Z 2)*exp_R) /\ dom f1 by A5,VALUED_1:12; then A9: Z c= dom (( #Z 2)*exp_R) by XBOOLE_1:18; for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =exp_R(x)/(exp_R(x)-exp_R (-x)) proof let x; A10: exp_R(x)>0 by SIN_COS:55; assume A11: x in Z; then A12: f is_differentiable_in x & f.x >0 by A2,A3,A7,FDIFF_1:9; A13: ((( #Z 2)*exp_R)-f1).x =(( #Z 2)*exp_R).x-f1.x by A5,A11,VALUED_1:13 .=( #Z 2).(exp_R.x)-f1.x by A9,A11,FUNCT_1:12 .=(exp_R.x) #Z 2-f1.x by TAYLOR_1:def 1 .=(exp_R.x) #Z 2-1 by A3,A11 .=(exp_R(x)) #Z (1+1)-1 by SIN_COS:def 23 .=(exp_R(x)) #Z 1 * (exp_R(x)) #Z 1 -1 by A10,PREPOWER:44 .=exp_R(x) * (exp_R(x)) #Z 1 -1 by PREPOWER:35 .=exp_R(x) * exp_R(x) -1 by PREPOWER:35; (((1/2)(#)(ln*f))`|Z).x =(1/2)*diff((ln*f),x) by A1,A8,A11,FDIFF_1:20 .=(1/2)*(diff(f,x)/f.x) by A12,TAYLOR_1:20 .=(1/2)*((((( #Z 2)*exp_R)-f1)`|Z).x/((( #Z 2)*exp_R)-f1).x) by A2,A7,A11 ,FDIFF_1:def 7 .=(1/2)*((2*exp_R(2*x))/(exp_R(x) * exp_R(x) -1)) by A6,A5,A11,A13,Th25 .=(1/2)*(2*exp_R(2*x))/(exp_R(x) * exp_R(x) -1) by XCMPLX_1:74 .=(exp_R(x+x)/exp_R(x))/((exp_R(x) * exp_R(x)-1)/exp_R(x)) by A10, XCMPLX_1:55 .=((exp_R(x)*exp_R(x))/exp_R(x))/((exp_R(x) * exp_R(x)-1)/exp_R(x)) by SIN_COS:50 .=((exp_R(x)*exp_R(x))/exp_R(x))/((exp_R(x)*exp_R(x))/exp_R(x)- 1/ exp_R(x)) by XCMPLX_1:120 .=exp_R(x)/(exp_R(x) * exp_R(x)/exp_R(x)-1/exp_R(x)) by A10,XCMPLX_1:89 .=exp_R(x)/(exp_R(x)-1/exp_R(x)) by A10,XCMPLX_1:89 .=exp_R(x)/(exp_R(x)-exp_R(-x)) by TAYLOR_1:4; hence thesis; end; hence thesis by A1,A8,FDIFF_1:20; end; :: 27 f.x=(exp_R.x-1)^2 theorem Th27: Z c= dom (( #Z 2)*(exp_R-f)) & (for x st x in Z holds f.x=1) implies ( #Z 2)*(exp_R-f) is_differentiable_on Z & for x st x in Z holds ((( #Z 2)*(exp_R-f))`|Z).x =2*exp_R.x*(exp_R.x-1) proof assume that A1: Z c= dom (( #Z 2)*(exp_R-f)) and A2: for x st x in Z holds f.x=1; for y being object st y in Z holds y in dom (exp_R-f) by A1,FUNCT_1:11; then A3: Z c= dom (exp_R-f) by TARSKI:def 3; then Z c= dom exp_R /\ dom f by VALUED_1:12; then A4: Z c= dom f by XBOOLE_1:18; A5: for x st x in Z holds f.x=0*x+1 by A2; then A6: f is_differentiable_on Z by A4,FDIFF_1:23; A7: for x st x in Z holds ( #Z 2)*(exp_R-f) is_differentiable_in x proof let x; assume x in Z; then A8: f is_differentiable_in x by A6,FDIFF_1:9; exp_R is_differentiable_in x by SIN_COS:65; then exp_R-f is_differentiable_in x by A8,FDIFF_1:14; hence thesis by TAYLOR_1:3; end; then A9: ( #Z 2)*(exp_R-f) is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((( #Z 2)*(exp_R-f))`|Z).x =2*exp_R.x*(exp_R.x-1) proof let x; A10: exp_R is_differentiable_in x by SIN_COS:65; assume A11: x in Z; then A12: (exp_R-f).x=exp_R.x-f.x by A3,VALUED_1:13 .= exp_R.x-1 by A2,A11; A13: f is_differentiable_in x by A6,A11,FDIFF_1:9; then A14: diff((exp_R-f),x)=diff(exp_R,x)-diff(f,x) by A10,FDIFF_1:14 .=diff(exp_R,x)-(f`|Z).x by A6,A11,FDIFF_1:def 7 .=exp_R.x-(f`|Z).x by SIN_COS:65 .=exp_R.x-0 by A4,A5,A11,FDIFF_1:23 .=exp_R.x; A15: exp_R-f is_differentiable_in x by A13,A10,FDIFF_1:14; ((( #Z 2)*(exp_R-f))`|Z).x =diff((( #Z 2)*(exp_R-f)),x) by A9,A11, FDIFF_1:def 7 .=2* ((exp_R-f).x) #Z (2-1) * diff((exp_R-f),x) by A15,TAYLOR_1:3 .=2*(exp_R.x-1)*exp_R.x by A14,A12,PREPOWER:35 .=2*exp_R.x*(exp_R.x-1); hence thesis; end; hence thesis by A1,A7,FDIFF_1:9; end; :: 28 f.x=ln((exp_R.x-1)^2/exp_R.x) theorem Z c= dom f & f=ln*((( #Z 2)*(exp_R-f1))/exp_R) & (for x st x in Z holds f1.x=1 & (exp_R-f1).x>0) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =(exp_R.x+1)/(exp_R.x-1) proof assume that A1: Z c= dom f and A2: f=ln*((( #Z 2)*(exp_R-f1))/exp_R) and A3: for x st x in Z holds f1.x=1 & (exp_R-f1).x>0; for y being object st y in Z holds y in dom ((( #Z 2)*(exp_R-f1))/exp_R) by A1,A2, FUNCT_1:11; then A4: Z c= dom ((( #Z 2)*(exp_R-f1))/exp_R) by TARSKI:def 3; then Z c=dom (( #Z 2)*(exp_R-f1))/\(dom (exp_R)\(exp_R)"{0}) by RFUNCT_1:def 1; then A5: Z c= dom (( #Z 2)*(exp_R-f1)) by XBOOLE_1:18; then for y being object st y in Z holds y in dom (exp_R-f1) by FUNCT_1:11; then A6: Z c= dom (exp_R-f1) by TARSKI:def 3; A7: for x st x in Z holds ((( #Z 2)*(exp_R-f1))/exp_R).x >0 proof let x; A8: exp_R.x>0 by SIN_COS:54; assume A9: x in Z; then A10: ((exp_R-f1).x) #Z 2>0 by A3,PREPOWER:39; ((( #Z 2)*(exp_R-f1))/exp_R).x =(( #Z 2)*(exp_R-f1)).x*(exp_R.x)" by A4,A9, RFUNCT_1:def 1 .=(( #Z 2)*(exp_R-f1)).x*(1/exp_R.x) by XCMPLX_1:215 .=(( #Z 2)*(exp_R-f1)).x/exp_R.x by XCMPLX_1:99 .=( #Z 2).((exp_R-f1).x)/exp_R.x by A5,A9,FUNCT_1:12 .=((exp_R-f1).x) #Z 2/exp_R.x by TAYLOR_1:def 1; hence thesis by A10,A8,XREAL_1:139; end; A11: for x st x in Z holds f1.x=1 by A3; then A12: ( #Z 2)*(exp_R-f1) is_differentiable_on Z by A5,Th27; exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by FDIFF_1:26 ,SIN_COS:54,TAYLOR_1:16; then A13: (( #Z 2)*(exp_R-f1))/exp_R is_differentiable_on Z by A12,FDIFF_2:21; A14: for x st x in Z holds ln*((( #Z 2)*(exp_R-f1))/exp_R) is_differentiable_in x proof let x; assume x in Z; then (( #Z 2)*(exp_R-f1))/exp_R is_differentiable_in x & ((( #Z 2)*(exp_R- f1))/ exp_R).x >0 by A13,A7,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A15: f is_differentiable_on Z by A1,A2,FDIFF_1:9; for x st x in Z holds (f`|Z).x =(exp_R.x+1)/(exp_R.x-1) proof let x; A16: exp_R.x>0 by SIN_COS:54; A17: exp_R is_differentiable_in x by SIN_COS:65; assume A18: x in Z; then A19: (exp_R-f1).x=exp_R.x - f1.x by A6,VALUED_1:13 .=exp_R.x -1 by A3,A18; then A20: exp_R.x-1>0 by A3,A18; A21: ((( #Z 2)*(exp_R-f1))/exp_R).x =(( #Z 2)*(exp_R-f1)).x*(exp_R.x)" by A4 ,A18,RFUNCT_1:def 1 .=(( #Z 2)*(exp_R-f1)).x*(1/exp_R.x) by XCMPLX_1:215 .=(( #Z 2)*(exp_R-f1)).x/exp_R.x by XCMPLX_1:99 .=( #Z 2).((exp_R-f1).x)/exp_R.x by A5,A18,FUNCT_1:12 .=((exp_R.x-1) #Z (1+1))/exp_R.x by A19,TAYLOR_1:def 1 .=((exp_R.x-1) #Z 1*(exp_R.x-1) #Z 1)/exp_R.x by A20,PREPOWER:44 .=((exp_R.x-1) *(exp_R.x-1) #Z 1)/exp_R.x by PREPOWER:35 .=((exp_R.x-1) *(exp_R.x-1))/exp_R.x by PREPOWER:35; A22: (( #Z 2)*(exp_R-f1))/exp_R is_differentiable_in x & ((( #Z 2)*(exp_R- f1))/ exp_R).x >0 by A13,A7,A18,FDIFF_1:9; ( #Z 2)*(exp_R-f1) is_differentiable_in x by A12,A18,FDIFF_1:9; then A23: diff(((( #Z 2)*(exp_R-f1))/exp_R),x) =(diff((( #Z 2)*(exp_R-f1)),x)* exp_R.x-diff(exp_R,x)* (( #Z 2)*(exp_R-f1)).x)/(exp_R.x)^2 by A16,A17, FDIFF_2:14 .=(((( #Z 2)*(exp_R-f1))`|Z).x*exp_R.x-diff(exp_R,x)* (( #Z 2)*(exp_R- f1)).x)/(exp_R.x)^2 by A12,A18,FDIFF_1:def 7 .=(2*exp_R.x*(exp_R.x-1)*exp_R.x- diff(exp_R,x)*(( #Z 2)*(exp_R-f1)).x )/(exp_R.x)^2 by A11,A5,A18,Th27 .=(2*exp_R.x*(exp_R.x-1)*exp_R.x-exp_R.x* (( #Z 2)*(exp_R-f1)).x)/( exp_R.x)^2 by SIN_COS:65 .=((2*exp_R.x*(exp_R.x-1)-(( #Z 2)*(exp_R-f1)).x)*exp_R.x)/ (exp_R.x* exp_R.x) .=(2*exp_R.x*(exp_R.x-1)-(( #Z 2)*(exp_R-f1)).x)/exp_R.x by A16, XCMPLX_1:91 .=(2*exp_R.x*(exp_R.x-1)-( #Z 2).((exp_R-f1).x))/exp_R.x by A5,A18, FUNCT_1:12 .=(2*exp_R.x*(exp_R.x-1)-((exp_R-f1).x) #Z 2)/exp_R.x by TAYLOR_1:def 1 .=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-f1.x) #Z 2)/exp_R.x by A6,A18, VALUED_1:13 .=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-1) #Z (1+1))/exp_R.x by A3,A18 .=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-1) #Z 1*(exp_R.x-1) #Z 1)/exp_R.x by A20,PREPOWER:44 .=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-1) *(exp_R.x-1) #Z 1)/exp_R.x by PREPOWER:35 .=(2*exp_R.x*(exp_R.x-1)-(exp_R.x-1) *(exp_R.x-1))/exp_R.x by PREPOWER:35 .=((exp_R.x+1)*(exp_R.x-1))/exp_R.x; (f`|Z).x =diff(ln*((( #Z 2)*(exp_R-f1))/exp_R),x) by A2,A15,A18, FDIFF_1:def 7 .=(((exp_R.x+1)*(exp_R.x-1))/exp_R.x)/(((exp_R.x-1)* (exp_R.x-1))/ exp_R.x) by A22,A23,A21,TAYLOR_1:20 .=((exp_R.x+1)*(exp_R.x-1))/((exp_R.x-1) *(exp_R.x-1)) by A16,XCMPLX_1:55 .=(exp_R.x+1)/(exp_R.x-1) by A20,XCMPLX_1:91; hence thesis; end; hence thesis by A1,A2,A14,FDIFF_1:9; end; :: 29 f.x=(exp_R.x+1)^2 theorem Th29: Z c= dom (( #Z 2)*(exp_R+f)) & (for x st x in Z holds f.x=1) implies ( #Z 2)*(exp_R+f) is_differentiable_on Z & for x st x in Z holds ((( #Z 2)*(exp_R+f))`|Z).x =2*exp_R.x*(exp_R.x+1) proof assume that A1: Z c= dom (( #Z 2)*(exp_R+f)) and A2: for x st x in Z holds f.x=1; for y being object st y in Z holds y in dom (exp_R+f) by A1,FUNCT_1:11; then A3: Z c= dom (exp_R+f) by TARSKI:def 3; then Z c= dom exp_R /\ dom f by VALUED_1:def 1; then A4: Z c= dom f by XBOOLE_1:18; A5: for x st x in Z holds f.x=0*x+1 by A2; then A6: f is_differentiable_on Z by A4,FDIFF_1:23; A7: for x st x in Z holds ( #Z 2)*(exp_R+f) is_differentiable_in x proof let x; assume x in Z; then A8: f is_differentiable_in x by A6,FDIFF_1:9; exp_R is_differentiable_in x by SIN_COS:65; then exp_R+f is_differentiable_in x by A8,FDIFF_1:13; hence thesis by TAYLOR_1:3; end; then A9: ( #Z 2)*(exp_R+f) is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((( #Z 2)*(exp_R+f))`|Z).x =2*exp_R.x*(exp_R.x+1) proof let x; A10: exp_R is_differentiable_in x by SIN_COS:65; assume A11: x in Z; then A12: (exp_R+f).x=exp_R.x+f.x by A3,VALUED_1:def 1 .= exp_R.x+1 by A2,A11; A13: f is_differentiable_in x by A6,A11,FDIFF_1:9; then A14: diff((exp_R+f),x)=diff(exp_R,x)+diff(f,x) by A10,FDIFF_1:13 .=diff(exp_R,x)+(f`|Z).x by A6,A11,FDIFF_1:def 7 .=exp_R.x+(f`|Z).x by SIN_COS:65 .=exp_R.x+0 by A4,A5,A11,FDIFF_1:23 .=exp_R.x; A15: exp_R+f is_differentiable_in x by A13,A10,FDIFF_1:13; ((( #Z 2)*(exp_R+f))`|Z).x =diff((( #Z 2)*(exp_R+f)),x) by A9,A11, FDIFF_1:def 7 .=2* ((exp_R+f).x) #Z (2-1) * diff((exp_R+f),x) by A15,TAYLOR_1:3 .=2*(exp_R.x+1)*exp_R.x by A14,A12,PREPOWER:35 .=2*exp_R.x*(exp_R.x+1); hence thesis; end; hence thesis by A1,A7,FDIFF_1:9; end; :: 30 f.x=ln((exp_R.x+1)^2/exp_R.x) theorem Z c= dom f & f=ln*((( #Z 2)*(exp_R+f1))/exp_R) & (for x st x in Z holds f1.x=1) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =(exp_R.x-1)/(exp_R.x+1) proof assume that A1: Z c= dom f and A2: f=ln*((( #Z 2)*(exp_R+f1))/exp_R) and A3: for x st x in Z holds f1.x=1; for y being object st y in Z holds y in dom ((( #Z 2)*(exp_R+f1))/exp_R) by A1,A2, FUNCT_1:11; then A4: Z c= dom ((( #Z 2)*(exp_R+f1))/exp_R) by TARSKI:def 3; then Z c=dom (( #Z 2)*(exp_R+f1))/\(dom (exp_R)\(exp_R)"{0}) by RFUNCT_1:def 1; then A5: Z c= dom (( #Z 2)*(exp_R+f1)) by XBOOLE_1:18; then A6: ( #Z 2)*(exp_R+f1) is_differentiable_on Z by A3,Th29; for y being object st y in Z holds y in dom (exp_R+f1) by A5,FUNCT_1:11; then A7: Z c= dom (exp_R+f1) by TARSKI:def 3; A8: for x st x in Z holds ((( #Z 2)*(exp_R+f1))/exp_R).x >0 proof let x; A9: exp_R.x>0 by SIN_COS:54; assume A10: x in Z; then (exp_R+f1).x=exp_R.x + f1.x by A7,VALUED_1:def 1 .=exp_R.x +1 by A3,A10; then (exp_R+f1).x>0 by SIN_COS:54,XREAL_1:34; then A11: ((exp_R+f1).x) #Z 2>0 by PREPOWER:39; ((( #Z 2)*(exp_R+f1))/exp_R).x =(( #Z 2)*(exp_R+f1)).x*(exp_R.x)" by A4,A10 ,RFUNCT_1:def 1 .=(( #Z 2)*(exp_R+f1)).x*(1/exp_R.x) by XCMPLX_1:215 .=(( #Z 2)*(exp_R+f1)).x/exp_R.x by XCMPLX_1:99 .=( #Z 2).((exp_R+f1).x)/exp_R.x by A5,A10,FUNCT_1:12 .=((exp_R+f1).x) #Z 2/exp_R.x by TAYLOR_1:def 1; hence thesis by A11,A9,XREAL_1:139; end; exp_R is_differentiable_on Z & for x st x in Z holds exp_R.x<>0 by FDIFF_1:26 ,SIN_COS:54,TAYLOR_1:16; then A12: (( #Z 2)*(exp_R+f1))/exp_R is_differentiable_on Z by A6,FDIFF_2:21; A13: for x st x in Z holds ln*((( #Z 2)*(exp_R+f1))/exp_R) is_differentiable_in x proof let x; assume x in Z; then (( #Z 2)*(exp_R+f1))/exp_R is_differentiable_in x & ((( #Z 2)*(exp_R+ f1))/ exp_R).x >0 by A12,A8,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A14: f is_differentiable_on Z by A1,A2,FDIFF_1:9; for x st x in Z holds (f`|Z).x =(exp_R.x-1)/(exp_R.x+1) proof let x; A15: exp_R.x>0 by SIN_COS:54; A16: exp_R is_differentiable_in x by SIN_COS:65; A17: exp_R.x +1>0 by SIN_COS:54,XREAL_1:34; assume A18: x in Z; then A19: (exp_R+f1).x=exp_R.x + f1.x by A7,VALUED_1:def 1 .=exp_R.x +1 by A3,A18; A20: (( #Z 2)*(exp_R+f1)).x =( #Z 2).((exp_R+f1).x) by A5,A18,FUNCT_1:12 .=(exp_R.x+1) #Z (1+1) by A19,TAYLOR_1:def 1 .=(exp_R.x+1) #Z 1*(exp_R.x+1) #Z 1 by A17,PREPOWER:44 .=(exp_R.x+1) *(exp_R.x+1) #Z 1 by PREPOWER:35 .=(exp_R.x+1) *(exp_R.x+1) by PREPOWER:35; A21: (( #Z 2)*(exp_R+f1))/exp_R is_differentiable_in x & ((( #Z 2)*(exp_R+ f1))/ exp_R).x >0 by A12,A8,A18,FDIFF_1:9; ( #Z 2)*(exp_R+f1) is_differentiable_in x by A6,A18,FDIFF_1:9; then A22: diff(((( #Z 2)*(exp_R+f1))/exp_R),x) =(diff((( #Z 2)*(exp_R+f1)),x)* exp_R.x-diff(exp_R,x)* (( #Z 2)*(exp_R+f1)).x)/(exp_R.x)^2 by A15,A16, FDIFF_2:14 .=(((( #Z 2)*(exp_R+f1))`|Z).x*exp_R.x-diff(exp_R,x)*(( #Z 2)* (exp_R+ f1)).x)/(exp_R.x)^2 by A6,A18,FDIFF_1:def 7 .=(2*exp_R.x*(exp_R.x+1)*exp_R.x-diff(exp_R,x)*(( #Z 2)* (exp_R+f1)).x )/(exp_R.x)^2 by A3,A5,A18,Th29 .=(2*exp_R.x*(exp_R.x+1)*exp_R.x-exp_R.x*(( #Z 2)* (exp_R+f1)).x)/( exp_R.x)^2 by SIN_COS:65 .=((2*exp_R.x*(exp_R.x+1)-(( #Z 2)*(exp_R+f1)).x)*exp_R.x)/ (exp_R.x* exp_R.x) .=(exp_R.x-1)*(exp_R.x+1)/exp_R.x by A15,A20,XCMPLX_1:91; A23: ((( #Z 2)*(exp_R+f1))/exp_R).x =(( #Z 2)*(exp_R+f1)).x*(exp_R.x)" by A4 ,A18,RFUNCT_1:def 1 .=(( #Z 2)*(exp_R+f1)).x*(1/exp_R.x) by XCMPLX_1:215 .=((exp_R.x+1) *(exp_R.x+1))/exp_R.x by A20,XCMPLX_1:99; (f`|Z).x =diff(ln*((( #Z 2)*(exp_R+f1))/exp_R),x) by A2,A14,A18, FDIFF_1:def 7 .=(((exp_R.x+1)*(exp_R.x-1))/exp_R.x)/(((exp_R.x+1) * (exp_R.x+1))/ exp_R.x) by A21,A22,A23,TAYLOR_1:20 .=((exp_R.x+1)*(exp_R.x-1))/((exp_R.x+1) *(exp_R.x+1)) by A15,XCMPLX_1:55 .=(exp_R.x-1)/(exp_R.x+1) by A17,XCMPLX_1:91; hence thesis; end; hence thesis by A1,A2,A13,FDIFF_1:9; end; :: 31 f.x=(1-exp_R.x)^2 theorem Th31: Z c= dom (( #Z 2)*(f-exp_R)) & (for x st x in Z holds f.x=1) implies ( #Z 2)*(f-exp_R) is_differentiable_on Z & for x st x in Z holds ((( #Z 2)*(f-exp_R))`|Z).x =-2*exp_R.x*(1-exp_R.x) proof assume that A1: Z c= dom (( #Z 2)*(f-exp_R)) and A2: for x st x in Z holds f.x=1; for y being object st y in Z holds y in dom (f-exp_R) by A1,FUNCT_1:11; then A3: Z c= dom (f-exp_R) by TARSKI:def 3; then Z c= dom exp_R /\ dom f by VALUED_1:12; then A4: Z c= dom f by XBOOLE_1:18; A5: for x st x in Z holds f.x=0*x+1 by A2; then A6: f is_differentiable_on Z by A4,FDIFF_1:23; A7: for x st x in Z holds ( #Z 2)*(f-exp_R) is_differentiable_in x proof let x; assume x in Z; then A8: f is_differentiable_in x by A6,FDIFF_1:9; exp_R is_differentiable_in x by SIN_COS:65; then f-exp_R is_differentiable_in x by A8,FDIFF_1:14; hence thesis by TAYLOR_1:3; end; then A9: ( #Z 2)*(f-exp_R) is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((( #Z 2)*(f-exp_R))`|Z).x =-2*exp_R.x*(1-exp_R.x ) proof let x; A10: exp_R is_differentiable_in x by SIN_COS:65; assume A11: x in Z; then A12: (f-exp_R).x=f.x-exp_R.x by A3,VALUED_1:13 .=1- exp_R.x by A2,A11; A13: f is_differentiable_in x by A6,A11,FDIFF_1:9; then A14: diff((f-exp_R),x)=diff(f,x)-diff(exp_R,x) by A10,FDIFF_1:14 .=(f`|Z).x-diff(exp_R,x) by A6,A11,FDIFF_1:def 7 .=(f`|Z).x-exp_R.x by SIN_COS:65 .=0-exp_R.x by A4,A5,A11,FDIFF_1:23 .=-exp_R.x; A15: f-exp_R is_differentiable_in x by A13,A10,FDIFF_1:14; ((( #Z 2)*(f-exp_R))`|Z).x =diff((( #Z 2)*(f-exp_R)),x) by A9,A11, FDIFF_1:def 7 .=2* ((f-exp_R).x) #Z (2-1) * diff((f-exp_R),x) by A15,TAYLOR_1:3 .=2*(1-exp_R.x)*(-exp_R.x) by A14,A12,PREPOWER:35 .=-2*exp_R.x*(1-exp_R.x); hence thesis; end; hence thesis by A1,A7,FDIFF_1:9; end; :: 32 f.x=ln(exp_R.x/(1-exp_R.x)^2) theorem Z c= dom f & f=ln*(exp_R/(( #Z 2)*(f1-exp_R))) & (for x st x in Z holds f1.x=1 & (f1-exp_R).x>0) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =(1+exp_R.x)/(1-exp_R.x) proof assume that A1: Z c= dom f and A2: f=ln*(exp_R/(( #Z 2)*(f1-exp_R))) and A3: for x st x in Z holds f1.x=1 & (f1-exp_R).x>0; for y being object st y in Z holds y in dom (exp_R/(( #Z 2)*(f1-exp_R))) by A1,A2, FUNCT_1:11; then A4: Z c= dom (exp_R/(( #Z 2)*(f1-exp_R))) by TARSKI:def 3; then Z c=dom exp_R/\(dom ((( #Z 2)*(f1-exp_R)))\((( #Z 2)*(f1-exp_R)))"{0} ) by RFUNCT_1:def 1; then A5: Z c= dom (( #Z 2)*(f1-exp_R)) by XBOOLE_1:1; then for y being object st y in Z holds y in dom (f1-exp_R) by FUNCT_1:11; then A6: Z c= dom (f1-exp_R) by TARSKI:def 3; A7: for x st x in Z holds (( #Z 2)*(f1-exp_R)).x>0 proof let x; assume A8: x in Z; then (( #Z 2)*(f1-exp_R)) .x =( #Z 2).((f1-exp_R).x) by A5,FUNCT_1:12 .=((f1-exp_R).x) #Z 2 by TAYLOR_1:def 1; hence thesis by A3,A8,PREPOWER:39; end; A9: for x st x in Z holds (exp_R/(( #Z 2)*(f1-exp_R))).x >0 proof let x; A10: exp_R.x>0 by SIN_COS:54; assume A11: x in Z; then A12: (( #Z 2)*(f1-exp_R)).x>0 by A7; (exp_R/(( #Z 2)*(f1-exp_R))).x =exp_R.x*((( #Z 2)*(f1-exp_R)).x)" by A4,A11 ,RFUNCT_1:def 1 .=exp_R.x*(1/(( #Z 2)*(f1-exp_R)).x) by XCMPLX_1:215 .=exp_R.x/(( #Z 2)*(f1-exp_R)).x by XCMPLX_1:99; hence thesis by A12,A10,XREAL_1:139; end; A13: for x st x in Z holds f1.x=1 by A3; then A14: ( #Z 2)*(f1-exp_R) is_differentiable_on Z by A5,Th31; exp_R is_differentiable_on Z & for x st x in Z holds (( #Z 2)*(f1-exp_R )).x <>0 by A7,FDIFF_1:26,TAYLOR_1:16; then A15: exp_R/(( #Z 2)*(f1-exp_R)) is_differentiable_on Z by A14,FDIFF_2:21; A16: for x st x in Z holds ln*(exp_R/(( #Z 2)*(f1-exp_R))) is_differentiable_in x proof let x; assume x in Z; then exp_R/(( #Z 2)*(f1-exp_R)) is_differentiable_in x & (exp_R/(( #Z 2)*( f1- exp_R))).x >0 by A15,A9,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A17: f is_differentiable_on Z by A1,A2,FDIFF_1:9; for x st x in Z holds (f`|Z).x =(1+exp_R.x)/(1-exp_R.x) proof let x; A18: exp_R is_differentiable_in x by SIN_COS:65; assume A19: x in Z; then A20: (( #Z 2)*(f1-exp_R)) .x =( #Z 2).((f1-exp_R).x) by A5,FUNCT_1:12 .=((f1-exp_R).x) #Z 2 by TAYLOR_1:def 1 .=(f1.x-exp_R.x) #Z 2 by A6,A19,VALUED_1:13 .=(1-exp_R.x) #Z 2 by A3,A19; A21: (exp_R/(( #Z 2)*(f1-exp_R))).x =exp_R.x*((( #Z 2)*(f1-exp_R)).x)" by A4 ,A19,RFUNCT_1:def 1 .=exp_R.x*(1/(( #Z 2)*(f1-exp_R)).x) by XCMPLX_1:215 .=exp_R.x/(1-exp_R.x) #Z 2 by A20,XCMPLX_1:99; A22: exp_R/(( #Z 2)*(f1-exp_R)) is_differentiable_in x & (exp_R/(( #Z 2)*( f1- exp_R))).x >0 by A15,A9,A19,FDIFF_1:9; A23: (f1-exp_R).x>0 by A3,A19; (( #Z 2)*(f1-exp_R)).x<>0 & ( #Z 2)*(f1-exp_R) is_differentiable_in x by A14,A7,A19,FDIFF_1:9; then A24: diff((exp_R/(( #Z 2)*(f1-exp_R))),x) =(diff(exp_R,x)*(( #Z 2)*(f1- exp_R)).x- diff((( #Z 2)*(f1-exp_R)),x)*exp_R.x) /((( #Z 2)*(f1-exp_R)).x)^2 by A18,FDIFF_2:14 .=(exp_R.x*(( #Z 2)*(f1-exp_R)).x-diff((( #Z 2)*(f1-exp_R)),x)*exp_R.x ) /((( #Z 2)*(f1-exp_R)).x)^2 by SIN_COS:65 .=(exp_R.x*(( #Z 2)*(f1-exp_R)).x-((( #Z 2)*(f1-exp_R))`|Z).x*exp_R.x) /((( #Z 2)*(f1-exp_R)).x)^2 by A14,A19,FDIFF_1:def 7 .=(exp_R.x*((1-exp_R.x) #Z 2)-(-2*exp_R.x*(1-exp_R.x))*exp_R.x)/ ((1- exp_R.x) #Z 2)^2 by A13,A5,A19,A20,Th31 .=(exp_R.x*((1-exp_R.x) #Z 2+2*(1-exp_R.x)*exp_R.x)) /((1-exp_R.x) #Z 2*(1-exp_R.x) #Z 2) .=((exp_R.x/(1-exp_R.x) #Z 2)*((1-exp_R.x) #Z 2+2*(1-exp_R.x)*exp_R.x) ) /(1-exp_R.x) #Z 2 by XCMPLX_1:83; A25: exp_R.x>0 by SIN_COS:54; A26: (f1-exp_R).x=f1.x-exp_R.x by A6,A19,VALUED_1:13 .=1-exp_R.x by A3,A19; then (1-exp_R.x) #Z 2>0 by A3,A19,PREPOWER:39; then A27: exp_R.x/(1-exp_R.x) #Z 2<>0 by A25,XREAL_1:139; A28: (1-exp_R.x) #Z 2=(1-exp_R.x) #Z (1+1) .=(1-exp_R.x) #Z 1 * (1-exp_R.x) #Z 1 by A23,A26,PREPOWER:44 .=(1-exp_R.x) * (1-exp_R.x) #Z 1 by PREPOWER:35 .=(1-exp_R.x) * (1-exp_R.x) by PREPOWER:35; (f`|Z).x =diff(ln*(exp_R/(( #Z 2)*(f1-exp_R))),x) by A2,A17,A19, FDIFF_1:def 7 .=((exp_R.x/(1-exp_R.x) #Z 2)*((1-exp_R.x) #Z 2+2*(1-exp_R.x)*exp_R.x) ) /(1-exp_R.x) #Z 2/(exp_R.x/(1-exp_R.x) #Z 2) by A22,A24,A21,TAYLOR_1:20 .=((exp_R.x/(1-exp_R.x) #Z 2)*((1-exp_R.x) #Z 2+2*(1-exp_R.x)*exp_R.x) ) /((exp_R.x/(1-exp_R.x) #Z 2)*(1-exp_R.x) #Z 2) by XCMPLX_1:78 .=((1-exp_R.x) * (1+exp_R.x))/((1-exp_R.x) * (1-exp_R.x)) by A27,A28, XCMPLX_1:91 .=(1+exp_R.x)/ (1-exp_R.x) by A23,A26,XCMPLX_1:91; hence thesis; end; hence thesis by A1,A2,A16,FDIFF_1:9; end; :: 33 f.x=ln(exp_R.x/(1+exp_R.x)^2) theorem Z c= dom f & f=ln*(exp_R/(( #Z 2)*(f1+exp_R))) & (for x st x in Z holds f1.x=1) implies f is_differentiable_on Z & for x st x in Z holds (f`|Z).x =(1-exp_R.x)/(1+exp_R.x) proof assume that A1: Z c= dom f and A2: f=ln*(exp_R/(( #Z 2)*(f1+exp_R))) and A3: for x st x in Z holds f1.x=1; for y being object st y in Z holds y in dom (exp_R/(( #Z 2)*(f1+exp_R))) by A1,A2, FUNCT_1:11; then A4: Z c= dom (exp_R/(( #Z 2)*(f1+exp_R))) by TARSKI:def 3; then Z c=dom exp_R/\(dom ((( #Z 2)*(f1+exp_R)))\((( #Z 2)*(f1+exp_R)))"{0} ) by RFUNCT_1:def 1; then A5: Z c= dom (( #Z 2)*(f1+exp_R)) by XBOOLE_1:1; then A6: ( #Z 2)*(f1+exp_R) is_differentiable_on Z by A3,Th29; for y being object st y in Z holds y in dom (f1+exp_R) by A5,FUNCT_1:11; then A7: Z c= dom (f1+exp_R) by TARSKI:def 3; A8: for x st x in Z holds (( #Z 2)*(f1+exp_R)).x>0 proof let x; assume A9: x in Z; then (f1+exp_R).x=f1.x+exp_R.x by A7,VALUED_1:def 1 .=1+exp_R.x by A3,A9; then A10: (f1+exp_R).x>0 by SIN_COS:54,XREAL_1:34; (( #Z 2)*(f1+exp_R)) .x =( #Z 2).((f1+exp_R).x) by A5,A9,FUNCT_1:12 .=((f1+exp_R).x) #Z 2 by TAYLOR_1:def 1; hence thesis by A10,PREPOWER:39; end; A11: for x st x in Z holds (exp_R/(( #Z 2)*(f1+exp_R))).x >0 proof let x; A12: exp_R.x>0 by SIN_COS:54; assume A13: x in Z; then A14: (( #Z 2)*(f1+exp_R)).x>0 by A8; (exp_R/(( #Z 2)*(f1+exp_R))).x =exp_R.x*((( #Z 2)*(f1+exp_R)).x)" by A4,A13 ,RFUNCT_1:def 1 .=exp_R.x*(1/(( #Z 2)*(f1+exp_R)).x) by XCMPLX_1:215 .=exp_R.x/(( #Z 2)*(f1+exp_R)).x by XCMPLX_1:99; hence thesis by A14,A12,XREAL_1:139; end; exp_R is_differentiable_on Z & for x st x in Z holds (( #Z 2)*(f1+exp_R )).x <>0 by A8,FDIFF_1:26,TAYLOR_1:16; then A15: exp_R/(( #Z 2)*(f1+exp_R)) is_differentiable_on Z by A6,FDIFF_2:21; A16: for x st x in Z holds ln*(exp_R/(( #Z 2)*(f1+exp_R))) is_differentiable_in x proof let x; assume x in Z; then exp_R/(( #Z 2)*(f1+exp_R)) is_differentiable_in x & (exp_R/(( #Z 2)*( f1+ exp_R))).x >0 by A15,A11,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A17: f is_differentiable_on Z by A1,A2,FDIFF_1:9; for x st x in Z holds (f`|Z).x =(1-exp_R.x)/(1+exp_R.x) proof let x; A18: exp_R is_differentiable_in x by SIN_COS:65; assume A19: x in Z; then A20: (( #Z 2)*(f1+exp_R)) .x =( #Z 2).((f1+exp_R).x) by A5,FUNCT_1:12 .=((f1+exp_R).x) #Z 2 by TAYLOR_1:def 1 .=(f1.x+exp_R.x) #Z 2 by A7,A19,VALUED_1:def 1 .=(1+exp_R.x) #Z 2 by A3,A19; (( #Z 2)*(f1+exp_R)).x<>0 & ( #Z 2)*(f1+exp_R) is_differentiable_in x by A6,A8,A19,FDIFF_1:9; then A21: diff((exp_R/(( #Z 2)*(f1+exp_R))),x) =(diff(exp_R,x)*(( #Z 2)*(f1+ exp_R)).x-diff((( #Z 2)*(f1+exp_R)),x)* exp_R.x) /((( #Z 2)*(f1+exp_R)).x)^2 by A18,FDIFF_2:14 .=(exp_R.x*(( #Z 2)*(f1+exp_R)).x-diff((( #Z 2)*(f1+exp_R)),x)*exp_R.x ) /((( #Z 2)*(f1+exp_R)).x)^2 by SIN_COS:65 .=(exp_R.x*(( #Z 2)*(f1+exp_R)).x-((( #Z 2)*(f1+exp_R))`|Z).x*exp_R.x) /((( #Z 2)*(f1+exp_R)).x)^2 by A6,A19,FDIFF_1:def 7 .=(exp_R.x*(1+exp_R.x) #Z 2-2*exp_R.x*(1+exp_R.x)*exp_R.x)/((1+exp_R.x ) #Z 2)^2 by A3,A5,A19,A20,Th29 .=(exp_R.x*((1+exp_R.x) #Z 2-2*(1+exp_R.x)*exp_R.x)) /((1+exp_R.x) #Z 2*(1+exp_R.x) #Z 2) .=((exp_R.x/(1+exp_R.x) #Z 2)*((1+exp_R.x) #Z 2-2*(1+exp_R.x)*exp_R.x) ) /(1+exp_R.x) #Z 2 by XCMPLX_1:83; A22: 1+exp_R.x>0 by SIN_COS:54,XREAL_1:34; then exp_R.x>0 & (1+exp_R.x) #Z 2>0 by PREPOWER:39,SIN_COS:54; then A23: exp_R.x/(1+exp_R.x) #Z 2<>0 by XREAL_1:139; A24: (exp_R/(( #Z 2)*(f1+exp_R))).x =exp_R.x*((( #Z 2)*(f1+exp_R)).x)" by A4 ,A19,RFUNCT_1:def 1 .=exp_R.x*(1/(( #Z 2)*(f1+exp_R)).x) by XCMPLX_1:215 .=exp_R.x/(1+exp_R.x) #Z 2 by A20,XCMPLX_1:99; A25: exp_R/(( #Z 2)*(f1+exp_R)) is_differentiable_in x & (exp_R/(( #Z 2)*( f1+ exp_R))).x >0 by A15,A11,A19,FDIFF_1:9; A26: (1+exp_R.x) #Z 2=(1+exp_R.x) #Z (1+1) .=(1+exp_R.x) #Z 1 * (1+exp_R.x) #Z 1 by A22,PREPOWER:44 .=(1+exp_R.x) * (1+exp_R.x) #Z 1 by PREPOWER:35 .=(1+exp_R.x) * (1+exp_R.x) by PREPOWER:35; (f`|Z).x =diff(ln*(exp_R/(( #Z 2)*(f1+exp_R))),x) by A2,A17,A19, FDIFF_1:def 7 .=((exp_R.x/(1+exp_R.x) #Z 2)*((1+exp_R.x) #Z 2-2*(1+exp_R.x)*exp_R.x) ) /(1+exp_R.x) #Z 2/(exp_R.x/(1+exp_R.x) #Z 2) by A25,A21,A24,TAYLOR_1:20 .=((exp_R.x/(1+exp_R.x) #Z 2)*((1+exp_R.x) #Z 2-2*(1+exp_R.x)*exp_R.x) ) /((exp_R.x/(1+exp_R.x) #Z 2)*(1+exp_R.x) #Z 2) by XCMPLX_1:78 .=((1+exp_R.x) * (1-exp_R.x))/((1+exp_R.x) * (1+exp_R.x)) by A23,A26, XCMPLX_1:91 .=(1-exp_R.x)/ (1+exp_R.x) by A22,XCMPLX_1:91; hence thesis; end; hence thesis by A1,A2,A16,FDIFF_1:9; end; :: 34 f.x=ln(exp_R(x)+exp_R(-x)) theorem Z c= dom (ln*f) & f=exp_R+(exp_R*f1) & (for x st x in Z holds f1.x=-x) implies ln*f is_differentiable_on Z & for x st x in Z holds ((ln*f)`|Z).x =( exp_R(x)-exp_R(-x))/(exp_R(x)+exp_R(-x)) proof assume that A1: Z c= dom (ln*f) and A2: f=exp_R+(exp_R*f1) and A3: for x st x in Z holds f1.x=-x; for y being object st y in Z holds y in dom f by A1,FUNCT_1:11; then A4: Z c= dom (exp_R+(exp_R*f1)) by A2,TARSKI:def 3; then Z c= dom exp_R /\ dom (exp_R*f1) by VALUED_1:def 1; then A5: Z c= dom (exp_R*f1) by XBOOLE_1:18; then A6: exp_R*f1 is_differentiable_on Z by A3,Th14; A7: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; then A8: f is_differentiable_on Z by A2,A4,A6,FDIFF_1:18; A9: for x st x in Z holds ((exp_R+(exp_R*f1))`|Z).x =exp_R(x)-exp_R(-x) proof let x; assume A10: x in Z; hence ((exp_R+(exp_R*f1))`|Z).x = diff(exp_R,x) + diff((exp_R*f1),x) by A4,A6,A7, FDIFF_1:18 .=exp_R.x+ diff((exp_R*f1),x) by SIN_COS:65 .=exp_R.x+((exp_R*f1)`|Z).x by A6,A10,FDIFF_1:def 7 .=exp_R.x+(-exp_R(-x)) by A3,A5,A10,Th14 .=exp_R(x)+(-exp_R(-x)) by SIN_COS:def 23 .=exp_R(x)-exp_R(-x); end; A11: for x st x in Z holds (exp_R+(exp_R*f1)).x>0 proof let x; A12: exp_R(x)>0 by SIN_COS:55; assume A13: x in Z; then (exp_R+(exp_R*f1)).x=exp_R.x + (exp_R*f1).x by A4,VALUED_1:def 1 .=exp_R.x +exp_R.(f1.x) by A5,A13,FUNCT_1:12 .=exp_R.x +exp_R.(-x) by A3,A13 .=exp_R(x) +exp_R.(-x) by SIN_COS:def 23 .=exp_R(x) +exp_R(-x) by SIN_COS:def 23; hence thesis by A12,SIN_COS:55,XREAL_1:34; end; A14: for x st x in Z holds ln*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x & f.x >0 by A2,A8,A11,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A15: ln*f is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((ln*f)`|Z).x =(exp_R(x)-exp_R(-x))/(exp_R(x)+ exp_R(-x)) proof let x; assume A16: x in Z; then A17: f.x=exp_R.x + (exp_R*f1).x by A2,A4,VALUED_1:def 1 .=exp_R.x +exp_R.(f1.x) by A5,A16,FUNCT_1:12 .=exp_R.x +exp_R.(-x) by A3,A16 .=exp_R(x) +exp_R.(-x) by SIN_COS:def 23 .=exp_R(x) +exp_R(-x) by SIN_COS:def 23; f is_differentiable_in x & f.x>0 by A2,A8,A11,A16,FDIFF_1:9; then diff((ln*f),x) =diff(f,x)/f.x by TAYLOR_1:20 .=(f`|Z).x/f.x by A8,A16,FDIFF_1:def 7 .=(exp_R(x)-exp_R(-x))/(exp_R(x) +exp_R(-x)) by A2,A9,A16,A17; hence thesis by A15,A16,FDIFF_1:def 7; end; hence thesis by A1,A14,FDIFF_1:9; end; :: 35 f.x=ln(exp_R(x)-exp_R(-x)) theorem Z c= dom (ln*f) & f=exp_R-(exp_R*f1) & (for x st x in Z holds f1.x=-x & f.x>0) implies ln*f is_differentiable_on Z & for x st x in Z holds ((ln*f)`|Z ).x=(exp_R(x)+exp_R(-x))/ (exp_R(x)-exp_R(-x)) proof assume that A1: Z c= dom (ln*f) and A2: f=exp_R-(exp_R*f1) and A3: for x st x in Z holds f1.x=-x & f.x>0; for y being object st y in Z holds y in dom f by A1,FUNCT_1:11; then A4: Z c= dom (exp_R-(exp_R*f1)) by A2,TARSKI:def 3; then Z c= dom exp_R /\ dom (exp_R*f1) by VALUED_1:12; then A5: Z c= dom (exp_R*f1) by XBOOLE_1:18; A6: for x st x in Z holds f1.x=-x by A3; then A7: exp_R*f1 is_differentiable_on Z by A5,Th14; A8: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; then A9: f is_differentiable_on Z by A2,A4,A7,FDIFF_1:19; A10: for x st x in Z holds ((exp_R-(exp_R*f1))`|Z).x =exp_R(x)+exp_R(-x) proof let x; assume A11: x in Z; hence ((exp_R-(exp_R*f1))`|Z).x = diff(exp_R,x) - diff((exp_R*f1),x) by A4,A7,A8, FDIFF_1:19 .=exp_R.x- diff((exp_R*f1),x) by SIN_COS:65 .=exp_R.x-((exp_R*f1)`|Z).x by A7,A11,FDIFF_1:def 7 .=exp_R.x-(-exp_R(-x)) by A6,A5,A11,Th14 .=exp_R.x+exp_R(-x) .=exp_R(x)+exp_R(-x) by SIN_COS:def 23; end; A12: for x st x in Z holds ln*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x & f.x >0 by A3,A9,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A13: ln*f is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((ln*f)`|Z).x =(exp_R(x)+exp_R(-x))/(exp_R(x)- exp_R(-x)) proof let x; assume A14: x in Z; then A15: f.x=exp_R.x - (exp_R*f1).x by A2,A4,VALUED_1:13 .=exp_R.x -exp_R.(f1.x) by A5,A14,FUNCT_1:12 .=exp_R.x -exp_R.(-x) by A3,A14 .=exp_R(x) -exp_R.(-x) by SIN_COS:def 23 .=exp_R(x) -exp_R(-x) by SIN_COS:def 23; f is_differentiable_in x & f.x>0 by A3,A9,A14,FDIFF_1:9; then diff((ln*f),x) =diff(f,x)/f.x by TAYLOR_1:20 .=(f`|Z).x/f.x by A9,A14,FDIFF_1:def 7 .=(exp_R(x)+exp_R(-x))/(exp_R(x) -exp_R(-x)) by A2,A10,A14,A15; hence thesis by A13,A14,FDIFF_1:def 7; end; hence thesis by A1,A12,FDIFF_1:9; end; :: 36 f.x=(2/3)*((1+exp_R.x) #R (3/2)) theorem Z c= dom ((2/3)(#)(( #R (3/2))*(f+exp_R))) & (for x st x in Z holds f. x=1) implies (2/3)(#)(( #R (3/2))*(f+exp_R)) is_differentiable_on Z & for x st x in Z holds (((2/3)(#)(( #R (3/2))*(f+exp_R)))`|Z).x =exp_R.x*(1+exp_R.x) #R ( 1/2) proof assume that A1: Z c= dom ((2/3)(#)(( #R (3/2))*(f+exp_R))) and A2: for x st x in Z holds f.x=1; A3: for x st x in Z holds f.x=0*x+1 by A2; A4: Z c= dom (( #R (3/2))*(f+exp_R)) by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom (f+exp_R) by FUNCT_1:11; then A5: Z c= dom (f+exp_R) by TARSKI:def 3; then Z c= dom exp_R /\ dom f by VALUED_1:def 1; then A6: Z c= dom f by XBOOLE_1:18; then A7: f is_differentiable_on Z by A3,FDIFF_1:23; A8: exp_R is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:16; then A9: f+exp_R is_differentiable_on Z by A5,A7,FDIFF_1:18; A10: for x st x in Z holds (f+exp_R).x>0 proof let x; assume A11: x in Z; then (f+exp_R).x=f.x+exp_R.x by A5,VALUED_1:def 1 .=1+exp_R.x by A2,A11; hence thesis by SIN_COS:54,XREAL_1:34; end; now let x; assume x in Z; then f+exp_R is_differentiable_in x & (f+exp_R).x>0 by A9,A10,FDIFF_1:9; hence ( #R (3/2))*(f+exp_R) is_differentiable_in x by TAYLOR_1:22; end; then A12: ( #R (3/2))*(f+exp_R) is_differentiable_on Z by A4,FDIFF_1:9; for x st x in Z holds (((2/3)(#)(( #R (3/2))*(f+exp_R)))`|Z).x =exp_R.x *(1+exp_R.x) #R (1/2) proof let x; assume A13: x in Z; then A14: ((f+exp_R)`|Z).x = diff(f,x)+diff(exp_R,x) by A5,A7,A8,FDIFF_1:18 .=diff(f,x)+exp_R.x by SIN_COS:65 .=(f`|Z).x+exp_R.x by A7,A13,FDIFF_1:def 7 .=0+exp_R.x by A6,A3,A13,FDIFF_1:23 .=exp_R.x; A15: f+exp_R is_differentiable_in x & (f+exp_R).x>0 by A9,A10,A13,FDIFF_1:9; A16: (f+exp_R).x=f.x+exp_R.x by A5,A13,VALUED_1:def 1 .=1+exp_R.x by A2,A13; (((2/3)(#)(( #R (3/2))*(f+exp_R)))`|Z).x =(2/3)*diff((( #R (3/2))*(f+ exp_R)),x) by A1,A12,A13,FDIFF_1:20 .=(2/3)*((3/2)*(((f+exp_R).x) #R (3/2-1)) * diff((f+exp_R),x)) by A15, TAYLOR_1:22 .=(2/3)*((3/2)*(((f+exp_R).x) #R (3/2-1)) *((f+exp_R)`|Z).x ) by A9,A13, FDIFF_1:def 7 .=exp_R.x*(1+exp_R.x) #R (1/2) by A16,A14; hence thesis; end; hence thesis by A1,A12,FDIFF_1:20; end; :: 37 f.x=(2/(3*lna))*((1+a |^x) #R (3/2)) theorem Z c= dom ((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1)))) & ( for x st x in Z holds f.x=1 & f1.x=x*log(number_e,a)) & a>0 & a<>1 implies (2/( 3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1))) is_differentiable_on Z & for x st x in Z holds (((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1))))`|Z) .x =a #R x * (1+a #R x) #R (1/2) proof assume that A1: Z c= dom ((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1)))) and A2: for x st x in Z holds f.x=1 & f1.x=x*log(number_e,a) and A3: a>0 and A4: a<>1; A5: for x st x in Z holds f.x=0*x+1 by A2; A6: Z c= dom (( #R (3/2))*(f+(exp_R*f1))) by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom (f+(exp_R*f1)) by FUNCT_1:11; then A7: Z c= dom (f+(exp_R*f1)) by TARSKI:def 3; then A8: Z c= dom (exp_R*f1) /\ dom f by VALUED_1:def 1; then A9: Z c= dom (exp_R*f1) by XBOOLE_1:18; A10: for x st x in Z holds f1.x=x*log(number_e,a) by A2; then A11: exp_R*f1 is_differentiable_on Z by A3,A9,Th11; A12: Z c= dom f by A8,XBOOLE_1:18; then A13: f is_differentiable_on Z by A5,FDIFF_1:23; then A14: f+(exp_R*f1) is_differentiable_on Z by A7,A11,FDIFF_1:18; A15: for x st x in Z holds (f+(exp_R*f1)).x>0 proof let x; assume A16: x in Z; then (f+(exp_R*f1)).x=f.x+(exp_R*f1).x by A7,VALUED_1:def 1 .=f.x+exp_R.(f1.x) by A9,A16,FUNCT_1:12 .=1+exp_R.(f1.x) by A2,A16 .=1+exp_R.(x*log(number_e,a)) by A2,A16; hence thesis by SIN_COS:54,XREAL_1:34; end; now let x; assume x in Z; then f+(exp_R*f1) is_differentiable_in x & (f+(exp_R*f1)).x>0 by A14,A15, FDIFF_1:9; hence ( #R (3/2))*(f+(exp_R*f1)) is_differentiable_in x by TAYLOR_1:22; end; then A17: ( #R (3/2))*(f+(exp_R*f1)) is_differentiable_on Z by A6,FDIFF_1:9; A18: log(number_e,a)<>0 proof A19: number_e<>1 by TAYLOR_1:11; assume log(number_e,a)=0; then log(number_e,a)=log(number_e,1) by SIN_COS2:13,TAYLOR_1:13; then a=(number_e) to_power log(number_e,1) by A3,A19,POWER:def 3 ,TAYLOR_1:11 .=1 by A19,POWER:def 3,TAYLOR_1:11; hence contradiction by A4; end; for x st x in Z holds (((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+( exp_R*f1))))`|Z).x =a #R x * (1+a #R x) #R (1/2) proof let x; A20: 3*log(number_e,a) <> 0 by A18; assume A21: x in Z; then A22: ((f+(exp_R*f1))`|Z).x=diff(f,x)+diff((exp_R*f1),x) by A7,A13,A11, FDIFF_1:18 .=diff(f,x)+((exp_R*f1)`|Z).x by A11,A21,FDIFF_1:def 7 .=(f`|Z).x+((exp_R*f1)`|Z).x by A13,A21,FDIFF_1:def 7 .=0+((exp_R*f1)`|Z).x by A12,A5,A21,FDIFF_1:23 .=a #R x*log(number_e,a) by A3,A10,A9,A21,Th11; A23: (f+(exp_R*f1)).x=f.x+(exp_R*f1).x by A7,A21,VALUED_1:def 1 .=f.x+exp_R.(f1.x) by A9,A21,FUNCT_1:12 .=1+exp_R.(f1.x) by A2,A21 .=1+exp_R.(x*log(number_e,a)) by A2,A21 .=1+a #R x by A3,Th1; f+(exp_R*f1) is_differentiable_in x & (f+(exp_R*f1)).x>0 by A14,A15,A21, FDIFF_1:9; then diff((( #R (3/2))*(f+(exp_R*f1))),x) =(3/2)*(((f+(exp_R*f1)).x) #R (3 /2-1)) * diff((f+(exp_R*f1)),x) by TAYLOR_1:22 .=(3/2)*((1+a #R x) #R (1/2)) *(a #R x*log(number_e,a)) by A14,A21,A23 ,A22,FDIFF_1:def 7 .=(3*log(number_e,a))/2*a #R x*(1+a #R x) #R (1/2); then (((2/(3*log(number_e,a)))(#)(( #R (3/2))*(f+(exp_R*f1))))`|Z).x =(2/( 3*log(number_e,a)))*((3*log(number_e,a))/2*a #R x*(1+a #R x) #R (1/2)) by A1 ,A17,A21,FDIFF_1:20 .=(2/(3*log(number_e,a)))*((3*log(number_e,a))/2) *a #R x*(1+a #R x) #R (1/2) .=1*a #R x*(1+a #R x) #R (1/2) by A20,XCMPLX_1:112 .=a #R x*(1+a #R x) #R (1/2); hence thesis; end; hence thesis by A1,A17,FDIFF_1:20; end; :: 38 f.x=(-1/2)*cos(2*x) theorem Z c= dom ((-1/2)(#)(cos*f)) & (for x st x in Z holds f.x=2*x) implies (-1/2)(#)(cos*f) is_differentiable_on Z & for x st x in Z holds (((-1/2)(#)(cos *f))`|Z).x =sin(2*x) proof assume that A1: Z c= dom ((-1/2)(#)(cos*f)) and A2: for x st x in Z holds f.x=2*x; A3: Z c= dom (cos*f) & for x st x in Z holds f.x=2*x+0 by A1,A2,VALUED_1:def 5; then A4: cos*f is_differentiable_on Z by FDIFF_4:38; for x st x in Z holds (((-1/2)(#)(cos*f))`|Z).x =sin(2*x) proof let x; assume A5: x in Z; then (((-1/2)(#)(cos*f))`|Z).x =(-1/2)*diff((cos*f),x) by A1,A4,FDIFF_1:20 .=(-1/2)*((cos*f)`|Z).x by A4,A5,FDIFF_1:def 7 .=(-1/2)*(-2* sin.(2*x+0)) by A3,A5,FDIFF_4:38 .=sin(2*x) by SIN_COS:def 17; hence thesis; end; hence thesis by A1,A4,FDIFF_1:20; end; theorem Z c= dom (2(#)(( #R (1/2))*(f-cos))) & (for x st x in Z holds f.x=1 & sin.x>0 & cos.x<1 & cos.x>-1) implies 2(#)(( #R (1/2))*(f-cos)) is_differentiable_on Z & for x st x in Z holds ((2(#)(( #R (1/2))*(f-cos)))`|Z) .x =(1+cos.x) #R (1/2) proof assume that A1: Z c= dom (2(#)(( #R (1/2))*(f-cos))) and A2: for x st x in Z holds f.x=1 & sin.x>0 & cos.x<1 & cos.x>-1; A3: for x st x in Z holds f.x=0*x+1 by A2; A4: Z c= dom (( #R (1/2))*(f-cos)) by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom (f-cos) by FUNCT_1:11; then A5: Z c= dom (f-cos) by TARSKI:def 3; then Z c= dom cos /\ dom f by VALUED_1:12; then A6: Z c= dom f by XBOOLE_1:18; then A7: f is_differentiable_on Z by A3,FDIFF_1:23; A8: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67; then A9: f-cos is_differentiable_on Z by A5,A7,FDIFF_1:19; A10: for x st x in Z holds (f-cos).x>0 proof let x; assume A11: x in Z; then cos.x<1 by A2; then A12: 1-cos.x>1-1 by XREAL_1:15; (f-cos).x=f.x-cos.x by A5,A11,VALUED_1:13 .=1-cos.x by A2,A11; hence thesis by A12; end; now let x; assume x in Z; then f-cos is_differentiable_in x & (f-cos).x >0 by A9,A10,FDIFF_1:9; hence ( #R (1/2))*(f-cos) is_differentiable_in x by TAYLOR_1:22; end; then A13: ( #R (1/2))*(f-cos) is_differentiable_on Z by A4,FDIFF_1:9; for x st x in Z holds ((2(#)(( #R (1/2))*(f-cos)))`|Z).x =(1+cos.x) #R (1/2) proof let x; assume A14: x in Z; then A15: diff((f-cos),x)=((f-cos)`|Z).x by A9,FDIFF_1:def 7 .=diff(f,x)-diff(cos,x) by A5,A7,A8,A14,FDIFF_1:19 .=(f`|Z).x-diff(cos,x) by A7,A14,FDIFF_1:def 7 .=0- diff(cos,x) by A6,A3,A14,FDIFF_1:23 .=0-(-sin.x) by SIN_COS:63 .=sin.x; A16: cos.x>-1 by A2,A14; A17: (f-cos).x=f.x-cos.x by A5,A14,VALUED_1:13 .=1-cos.x by A2,A14; A18: f-cos is_differentiable_in x & (f-cos).x >0 by A9,A10,A14,FDIFF_1:9; A19: sin.x>0 & cos.x<1 by A2,A14; ((2(#)(( #R (1/2))*(f-cos)))`|Z).x =2*diff((( #R (1/2))*(f-cos)),x) by A1,A13,A14,FDIFF_1:20 .=2*((1/2)*( ((f-cos).x) #R (1/2-1)) * diff((f-cos),x)) by A18, TAYLOR_1:22 .=sin.x*((1-cos.x) #R (-1/2)) by A17,A15 .=sin.x*(1 / (1-cos.x) #R (1/2)) by A10,A14,A17,PREPOWER:76 .=sin.x/(1-cos.x) #R (1/2) by XCMPLX_1:99 .=(1+cos.x) #R (1/2) by A19,A16,Lm4; hence thesis; end; hence thesis by A1,A13,FDIFF_1:20; end; theorem Z c= dom ((-2)(#)(( #R (1/2))*(f+cos))) & (for x st x in Z holds f.x=1 & sin.x>0 & cos.x<1 & cos.x>-1) implies (-2)(#)(( #R (1/2))*(f+cos)) is_differentiable_on Z & for x st x in Z holds (((-2)(#)(( #R (1/2))*(f+cos))) `|Z).x =(1-cos.x) #R (1/2) proof assume that A1: Z c= dom ((-2)(#)(( #R (1/2))*(f+cos))) and A2: for x st x in Z holds f.x=1 & sin.x>0 & cos.x<1 & cos.x>-1; A3: for x st x in Z holds f.x=0*x+1 by A2; A4: Z c= dom (( #R (1/2))*(f+cos)) by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom (f+cos) by FUNCT_1:11; then A5: Z c= dom (f+cos) by TARSKI:def 3; then Z c= dom cos /\ dom f by VALUED_1:def 1; then A6: Z c= dom f by XBOOLE_1:18; then A7: f is_differentiable_on Z by A3,FDIFF_1:23; A8: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67; then A9: f+cos is_differentiable_on Z by A5,A7,FDIFF_1:18; A10: for x st x in Z holds (f+cos).x>0 proof let x; assume A11: x in Z; then cos.x>-1 by A2; then A12: 1+cos.x>1+-1 by XREAL_1:8; (f+cos).x=f.x+cos.x by A5,A11,VALUED_1:def 1 .=1+cos.x by A2,A11; hence thesis by A12; end; now let x; assume x in Z; then f+cos is_differentiable_in x & (f+cos).x >0 by A9,A10,FDIFF_1:9; hence ( #R (1/2))*(f+cos) is_differentiable_in x by TAYLOR_1:22; end; then A13: ( #R (1/2))*(f+cos) is_differentiable_on Z by A4,FDIFF_1:9; for x st x in Z holds (((-2)(#)(( #R (1/2))*(f+cos)))`|Z).x =(1-cos.x) #R (1/2) proof let x; assume A14: x in Z; then A15: diff((f+cos),x)=((f+cos)`|Z).x by A9,FDIFF_1:def 7 .=diff(f,x)+diff(cos,x) by A5,A7,A8,A14,FDIFF_1:18 .=(f`|Z).x+diff(cos,x) by A7,A14,FDIFF_1:def 7 .=0+diff(cos,x) by A6,A3,A14,FDIFF_1:23 .=-sin.x by SIN_COS:63; A16: cos.x>-1 by A2,A14; A17: (f+cos).x=f.x+cos.x by A5,A14,VALUED_1:def 1 .=1+cos.x by A2,A14; A18: f+cos is_differentiable_in x & (f+cos).x >0 by A9,A10,A14,FDIFF_1:9; A19: sin.x>0 & cos.x<1 by A2,A14; (((-2)(#)(( #R (1/2))*(f+cos)))`|Z).x =(-2)*diff((( #R (1/2))*(f+cos) ),x) by A1,A13,A14,FDIFF_1:20 .=(-2)*((1/2)*( ((f+cos).x) #R (1/2-1)) * diff((f+cos),x)) by A18, TAYLOR_1:22 .=--sin.x*((1+cos.x) #R (-1/2)) by A17,A15 .=sin.x*(1/(1+cos.x) #R (1/2)) by A10,A14,A17,PREPOWER:76 .=sin.x/(1+cos.x) #R (1/2) by XCMPLX_1:99 .=(1-cos.x) #R (1/2) by A19,A16,Lm5; hence thesis; end; hence thesis by A1,A13,FDIFF_1:20; end; :: 41 f.x=1/2*ln(1+2*sin.x) Lm6: Z c= dom (f1+2(#)sin) & (for x st x in Z holds f1.x=1) implies f1+2(#)sin is_differentiable_on Z & for x st x in Z holds ((f1+2(#)sin)`|Z).x =2*cos.x proof assume that A1: Z c= dom (f1+2(#)sin) and A2: for x st x in Z holds f1.x=1; A3: Z c= dom f1 /\ dom (2(#)sin) by A1,VALUED_1:def 1; then A4: Z c= dom f1 by XBOOLE_1:18; A5: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68; A6: for x st x in Z holds f1.x=0*x+1 by A2; then A7: f1 is_differentiable_on Z by A4,FDIFF_1:23; Z c= dom (2(#)sin) by A3,XBOOLE_1:18; then A8: 2(#)sin is_differentiable_on Z by A5,FDIFF_1:20; for x st x in Z holds ((f1+2(#)sin)`|Z).x = 2*cos.x proof let x; A9: sin is_differentiable_in x by SIN_COS:64; assume A10: x in Z; then ((f1+2(#)sin)`|Z).x =diff(f1,x) + diff(2(#)sin,x) by A1,A7,A8, FDIFF_1:18 .=(f1`|Z).x+ diff(2(#)sin,x) by A7,A10,FDIFF_1:def 7 .=(f1`|Z).x+2*diff(sin,x) by A9,FDIFF_1:15 .=0+2*diff(sin,x) by A4,A6,A10,FDIFF_1:23 .=2*cos.x by SIN_COS:64; hence thesis; end; hence thesis by A1,A7,A8,FDIFF_1:18; end; theorem Z c= dom ((1/2)(#)(ln*f)) & f=f1+2(#)sin & (for x st x in Z holds f1.x =1 & f.x >0) implies (1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =cos.x/(1+2*sin.x) proof assume that A1: Z c= dom ((1/2)(#)(ln*f)) and A2: f=f1+2(#)sin and A3: for x st x in Z holds f1.x=1 & f.x >0; A4: Z c= dom (ln*f) by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom f by FUNCT_1:11; then A5: Z c= dom (f1+2(#)sin) by A2,TARSKI:def 3; A6: for x st x in Z holds f1.x=1 by A3; then A7: f is_differentiable_on Z by A2,A5,Lm6; for x st x in Z holds ln*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x & f.x >0 by A3,A7,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A8: ln*f is_differentiable_on Z by A4,FDIFF_1:9; Z c= dom f1 /\ dom (2(#)sin) by A5,VALUED_1:def 1; then A9: Z c= dom (2(#)sin) by XBOOLE_1:18; for x st x in Z holds (((1/2)(#)(ln*f))`|Z).x =cos.x/(1+2*sin.x) proof let x; assume A10: x in Z; then A11: f.x=f1.x+(2(#)sin).x by A2,A5,VALUED_1:def 1 .=1+(2(#)sin).x by A3,A10 .=1+2*sin.x by A9,A10,VALUED_1:def 5; A12: f is_differentiable_in x & f.x>0 by A3,A7,A10,FDIFF_1:9; (((1/2)(#)(ln*f))`|Z).x =(1/2)*diff((ln*f),x) by A1,A8,A10,FDIFF_1:20 .=(1/2)*(diff(f,x)/(f.x)) by A12,TAYLOR_1:20 .=(1/2)*((f`|Z).x/(f.x)) by A7,A10,FDIFF_1:def 7 .=(1/2)*((2*cos.x)/(f.x)) by A2,A6,A5,A10,Lm6 .=(1/2)*(2*cos.x)/(f.x) by XCMPLX_1:74 .=cos.x/(1+2*sin.x) by A11; hence thesis; end; hence thesis by A1,A8,FDIFF_1:20; end; :: 42 f.x=(-1/2)*ln(1+2*cos.x) Lm7: Z c= dom (f1+2(#)cos) & (for x st x in Z holds f1.x=1) implies f1+2(#)cos is_differentiable_on Z & for x st x in Z holds ((f1+2(#)cos)`|Z).x =-2*sin.x proof assume that A1: Z c= dom (f1+2(#)cos) and A2: for x st x in Z holds f1.x=1; A3: Z c= dom f1 /\ dom (2(#)cos) by A1,VALUED_1:def 1; then A4: Z c= dom f1 by XBOOLE_1:18; A5: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67; A6: for x st x in Z holds f1.x=0*x+1 by A2; then A7: f1 is_differentiable_on Z by A4,FDIFF_1:23; Z c= dom (2(#)cos) by A3,XBOOLE_1:18; then A8: 2(#)cos is_differentiable_on Z by A5,FDIFF_1:20; for x st x in Z holds ((f1+2(#)cos)`|Z).x = -2*sin.x proof let x; A9: cos is_differentiable_in x by SIN_COS:63; assume A10: x in Z; then ((f1+2(#)cos)`|Z).x =diff(f1,x) + diff(2(#)cos,x) by A1,A7,A8, FDIFF_1:18 .=(f1`|Z).x+ diff(2(#)cos,x) by A7,A10,FDIFF_1:def 7 .=(f1`|Z).x+2*diff(cos,x) by A9,FDIFF_1:15 .=0+2*diff(cos,x) by A4,A6,A10,FDIFF_1:23 .=0+2*(-sin.x) by SIN_COS:63 .=-2*sin.x; hence thesis; end; hence thesis by A1,A7,A8,FDIFF_1:18; end; theorem Z c= dom ((-1/2)(#)(ln*f)) & f=f1+2(#)cos & (for x st x in Z holds f1. x=1 & f.x >0) implies (-1/2)(#)(ln*f) is_differentiable_on Z & for x st x in Z holds (((-1/2)(#)(ln*f))`|Z).x =sin.x/(1+2*cos.x) proof assume that A1: Z c= dom ((-1/2)(#)(ln*f)) and A2: f=f1+2(#)cos and A3: for x st x in Z holds f1.x=1 & f.x >0; A4: Z c= dom (ln*f) by A1,VALUED_1:def 5; then for y being object st y in Z holds y in dom f by FUNCT_1:11; then A5: Z c= dom (f1+2(#)cos) by A2,TARSKI:def 3; A6: for x st x in Z holds f1.x=1 by A3; then A7: f is_differentiable_on Z by A2,A5,Lm7; for x st x in Z holds ln*f is_differentiable_in x proof let x; assume x in Z; then f is_differentiable_in x & f.x >0 by A3,A7,FDIFF_1:9; hence thesis by TAYLOR_1:20; end; then A8: ln*f is_differentiable_on Z by A4,FDIFF_1:9; Z c= dom f1 /\ dom (2(#)cos) by A5,VALUED_1:def 1; then A9: Z c= dom (2(#)cos) by XBOOLE_1:18; for x st x in Z holds (((-1/2)(#)(ln*f))`|Z).x =sin.x/(1+2*cos.x) proof let x; assume A10: x in Z; then A11: f.x=f1.x+(2(#)cos).x by A2,A5,VALUED_1:def 1 .=1+(2(#)cos).x by A3,A10 .=1+2*cos.x by A9,A10,VALUED_1:def 5; A12: f is_differentiable_in x & f.x>0 by A3,A7,A10,FDIFF_1:9; (((-1/2)(#)(ln*f))`|Z).x =(-1/2)*diff((ln*f),x) by A1,A8,A10,FDIFF_1:20 .=(-1/2)*(diff(f,x)/(f.x)) by A12,TAYLOR_1:20 .=(-1/2)*((f`|Z).x/(f.x)) by A7,A10,FDIFF_1:def 7 .=(-1/2)*((-2*sin.x)/(f.x)) by A2,A6,A5,A10,Lm7 .=(-1/2)*(-2*sin.x)/(f.x) by XCMPLX_1:74 .=sin.x/(1+2*cos.x) by A11; hence thesis; end; hence thesis by A1,A8,FDIFF_1:20; end; :: 43 f.x=1/(4*a)*sin(2*a*x) theorem Th43: Z c= dom ((1/(4*a))(#)(sin*f)) & (for x st x in Z holds f.x=2*a* x) & a<>0 implies (1/(4*a))(#)(sin*f) is_differentiable_on Z & for x st x in Z holds (((1/(4*a))(#)(sin*f))`|Z).x =1/2 * cos(2*a*x) proof assume that A1: Z c= dom ((1/(4*a))(#)(sin*f)) and A2: for x st x in Z holds f.x=2*a*x and A3: a<>0; A4: Z c= dom (sin*f) & for x st x in Z holds f.x=(2*a)*x+0 by A1,A2, VALUED_1:def 5; then A5: sin*f is_differentiable_on Z by FDIFF_4:37; for x st x in Z holds (((1/(4*a))(#)(sin*f))`|Z).x =1/2 * cos(2*a*x) proof let x; assume A6: x in Z; then (((1/(4*a))(#)(sin*f))`|Z).x =(1/(4*a))*diff((sin*f),x) by A1,A5, FDIFF_1:20 .=(1/(4*a))*((sin*f)`|Z).x by A5,A6,FDIFF_1:def 7 .=(1/(4*a))*((2*a)* cos.((2*a)*x+0)) by A4,A6,FDIFF_4:37 .=1/(4*a)*(2*a)* cos.((2*a)*x+0) .=(1/4)*(1/a)*(2*a)* cos.((2*a)*x) by XCMPLX_1:102 .=(1/4)*2*(1/a*a)* cos.(2*a*x) .=(1/2)*1*cos.(2*a*x) by A3,XCMPLX_1:106 .=1/2*cos(2*a*x) by SIN_COS:def 19; hence thesis; end; hence thesis by A1,A5,FDIFF_1:20; end; :: 44 f.x=x/2-1/(4*a)*sin(2*a*x) theorem Z c= dom (f1-((1/(4*a))(#)(sin*f))) & (for x st x in Z holds f1.x=x/2 & f.x=2*a*x) & a<>0 implies f1-((1/(4*a))(#)(sin*f)) is_differentiable_on Z & for x st x in Z holds ((f1-((1/(4*a))(#)(sin*f)))`|Z).x =(sin(a*x))^2 proof assume that A1: Z c= dom (f1-((1/(4*a))(#)(sin*f))) and A2: for x st x in Z holds f1.x=x/2 & f.x=2*a*x and A3: a<>0; A4: Z c= dom f1 /\ dom ((1/(4*a))(#)(sin*f)) by A1,VALUED_1:12; then A5: Z c= dom ((1/(4*a))(#)(sin*f)) by XBOOLE_1:18; A6: for x st x in Z holds f1.x=(1/2)*x+0 proof let x; assume x in Z; then f1.x=x/2 by A2 .= (1/2)*x+0; hence thesis; end; A7: for x st x in Z holds f.x=2*a*x by A2; then A8: (1/(4*a))(#)(sin*f) is_differentiable_on Z by A3,A5,Th43; A9: Z c= dom f1 by A4,XBOOLE_1:18; then A10: f1 is_differentiable_on Z by A6,FDIFF_1:23; for x st x in Z holds ((f1-((1/(4*a))(#)(sin*f)))`|Z).x =(sin(a*x))^2 proof let x; assume A11: x in Z; then ((f1-((1/(4*a))(#)(sin*f)))`|Z).x =diff(f1,x)-diff(((1/(4*a))(#)(sin* f)),x) by A1,A8,A10,FDIFF_1:19 .=(f1`|Z).x-diff(((1/(4*a))(#)(sin*f)),x) by A10,A11,FDIFF_1:def 7 .=(f1`|Z).x-(((1/(4*a))(#)(sin*f))`|Z).x by A8,A11,FDIFF_1:def 7 .=(f1`|Z).x-1/2 * cos(2*a*x) by A3,A7,A5,A11,Th43 .=1/2-1/2 * cos(2*a*x) by A9,A6,A11,FDIFF_1:23 .=(1/2)*(1-cos(2*(a*x))) .=(1/2)*(2*(sin(a*x))^2) by Lm1 .=(sin(a*x))^2; hence thesis; end; hence thesis by A1,A8,A10,FDIFF_1:19; end; :: 45 f.x=x/2+1/(4*a)*sin(2*a*x) theorem Z c= dom (f1+((1/(4*a))(#)(sin*f))) & (for x st x in Z holds f1.x=x/2 & f.x=2*a*x) & a<>0 implies f1+((1/(4*a))(#)(sin*f)) is_differentiable_on Z & for x st x in Z holds ((f1+((1/(4*a))(#)(sin*f)))`|Z).x =(cos(a*x))^2 proof assume that A1: Z c= dom (f1+((1/(4*a))(#)(sin*f))) and A2: for x st x in Z holds f1.x=x/2 & f.x=2*a*x and A3: a<>0; A4: Z c= dom f1 /\ dom ((1/(4*a))(#)(sin*f)) by A1,VALUED_1:def 1; then A5: Z c= dom ((1/(4*a))(#)(sin*f)) by XBOOLE_1:18; A6: for x st x in Z holds f1.x=(1/2)*x+0 proof let x; assume x in Z; then f1.x=x/2 by A2 .= (1/2)*x+0; hence thesis; end; A7: for x st x in Z holds f.x=2*a*x by A2; then A8: (1/(4*a))(#)(sin*f) is_differentiable_on Z by A3,A5,Th43; A9: Z c= dom f1 by A4,XBOOLE_1:18; then A10: f1 is_differentiable_on Z by A6,FDIFF_1:23; for x st x in Z holds ((f1+((1/(4*a))(#)(sin*f)))`|Z).x =(cos(a*x))^2 proof let x; assume A11: x in Z; then ((f1+((1/(4*a))(#)(sin*f)))`|Z).x =diff(f1,x)+diff(((1/(4*a))(#)(sin* f)),x) by A1,A8,A10,FDIFF_1:18 .=(f1`|Z).x+diff(((1/(4*a))(#)(sin*f)),x) by A10,A11,FDIFF_1:def 7 .=(f1`|Z).x+(((1/(4*a))(#)(sin*f))`|Z).x by A8,A11,FDIFF_1:def 7 .=(f1`|Z).x+1/2 * cos(2*a*x) by A3,A7,A5,A11,Th43 .=1/2+1/2 * cos(2*a*x) by A9,A6,A11,FDIFF_1:23 .=(1/2)*(1+cos(2*(a*x))) .=(1/2)*(2*(cos(a*x))^2) by Lm2 .=(cos(a*x))^2; hence thesis; end; hence thesis by A1,A8,A10,FDIFF_1:18; end; :: 46 f.x=(1/n)*(cos.x #Z n) theorem Th46: Z c= dom ((1/n)(#)(( #Z n)*cos)) & n>0 implies (1/n)(#)(( #Z n)* cos) is_differentiable_on Z & for x st x in Z holds (((1/n)(#)(( #Z n)*cos))`|Z ).x =-(cos.x) #Z (n-1)*sin.x proof assume that A1: Z c= dom ((1/n)(#)(( #Z n)*cos)) and A2: n>0; A3: now let x; assume x in Z; cos is_differentiable_in x by SIN_COS:63; hence ( #Z n)*cos is_differentiable_in x by TAYLOR_1:3; end; Z c= dom (( #Z n)*cos) by A1,VALUED_1:def 5; then A4: ( #Z n)*cos is_differentiable_on Z by A3,FDIFF_1:9; for x st x in Z holds (((1/n)(#)(( #Z n)*cos))`|Z).x =-(cos.x) #Z (n-1) *sin.x proof let x; A5: cos is_differentiable_in x by SIN_COS:63; assume x in Z; then (((1/n)(#)(( #Z n)*cos))`|Z).x =(1/n)*diff((( #Z n)*cos),x) by A1,A4, FDIFF_1:20 .=(1/n)*(n*( (cos.x) #Z (n-1)) * diff(cos,x)) by A5,TAYLOR_1:3 .=(1/n)*(n*( (cos.x) #Z (n-1)) *(-sin.x)) by SIN_COS:63 .=((1/n)*n)*( (cos.x) #Z (n-1)) *(-sin.x) .=((n")*n)*( (cos.x) #Z (n-1)) *(-sin.x) by XCMPLX_1:215 .=1*( (cos.x) #Z (n-1)) *(-sin.x) by A2,XCMPLX_0:def 7 .=-(cos.x) #Z (n-1) *sin.x; hence thesis; end; hence thesis by A1,A4,FDIFF_1:20; end; :: 47 f.x=(1/3)*(cos.x #Z 3)-cos.x theorem Z c= dom (((1/3)(#)(( #Z 3)*cos))-cos) implies (1/3)(#)(( #Z 3)*cos)- cos is_differentiable_on Z & for x st x in Z holds ((((1/3)(#)(( #Z 3)*cos))- cos)`|Z).x =(sin.x)|^3 proof assume A1: Z c= dom (((1/3)(#)(( #Z 3)*cos))-cos); then Z c= dom ((1/3)(#)(( #Z 3)*cos)) /\ dom cos by VALUED_1:12; then A2: Z c= dom ((1/3)(#)(( #Z 3)*cos)) by XBOOLE_1:18; then A3: ((1/3)(#)(( #Z 3)*cos)) is_differentiable_on Z by Th46; A4: cos is_differentiable_on Z by FDIFF_1:26,SIN_COS:67; now let x; assume A5: x in Z; then ((((1/3)(#)(( #Z 3)*cos))-cos)`|Z).x = diff(((1/3)(#)(( #Z 3)*cos)),x ) - diff(cos,x) by A1,A3,A4,FDIFF_1:19 .=diff(((1/3)(#)(( #Z 3)*cos)),x)-(-sin.x) by SIN_COS:63 .=(((1/3)(#)(( #Z 3)*cos))`|Z).x-(-sin.x) by A3,A5,FDIFF_1:def 7 .=-(cos.x) #Z (3-1)*sin.x--sin.x by A2,A5,Th46 .=sin.x*(1-(cos.x) #Z 2 ) .=sin.x*(1-(cos.x) |^ |.2.| ) by PREPOWER:def 3 .=sin.x*(1-(cos.x) |^ 2 ) by ABSVALUE:def 1 .=sin.x*(1-(cos.x)*(cos.x)) by WSIERP_1:1 .=sin.x*((cos.x)*(cos.x)+(sin.x)*(sin.x)-(cos.x)*(cos.x)) by SIN_COS:28 .=sin.x*((sin.x)|^2) by WSIERP_1:1 .=((sin.x)|^(2+1)) by NEWTON:6 .=(sin.x)|^3; hence ((((1/3)(#)(( #Z 3)*cos))-cos)`|Z).x =(sin.x)|^3; end; hence thesis by A1,A3,A4,FDIFF_1:19; end; :: 48 f.x=sin.x-(1/3)*(sin.x #Z 3) theorem Z c= dom (sin-((1/3)(#)(( #Z 3)*sin))) implies sin-((1/3)(#)(( #Z 3)* sin)) is_differentiable_on Z & for x st x in Z holds ((sin-((1/3)(#)(( #Z 3)* sin)))`|Z).x =(cos.x)|^3 proof assume A1: Z c= dom (sin-((1/3)(#)(( #Z 3)*sin))); then Z c= dom ((1/3)(#)(( #Z 3)*sin)) /\ dom sin by VALUED_1:12; then A2: Z c= dom ((1/3)(#)(( #Z 3)*sin)) by XBOOLE_1:18; then A3: ((1/3)(#)(( #Z 3)*sin)) is_differentiable_on Z by FDIFF_4:54; A4: sin is_differentiable_on Z by FDIFF_1:26,SIN_COS:68; now let x; assume A5: x in Z; then ((sin-((1/3)(#)(( #Z 3)*sin)))`|Z).x = diff(sin,x) - diff(((1/3)(#)(( #Z 3)*sin)),x) by A1,A3,A4,FDIFF_1:19 .=cos.x - diff(((1/3)(#)(( #Z 3)*sin)),x) by SIN_COS:64 .=cos.x -(((1/3)(#)(( #Z 3)*sin))`|Z).x by A3,A5,FDIFF_1:def 7 .=cos.x -((sin.x) #Z (3-1) *cos.x) by A2,A5,FDIFF_4:54 .=cos.x*(1-(sin.x) #Z 2) .=cos.x*(1-(sin.x) |^ |.2.| ) by PREPOWER:def 3 .=cos.x*(1-(sin.x) |^ 2 ) by ABSVALUE:def 1 .=cos.x*(1-(sin.x)*(sin.x)) by WSIERP_1:1 .=cos.x*((cos.x)*(cos.x)+(sin.x)*(sin.x)-(sin.x)*(sin.x)) by SIN_COS:28 .=cos.x*((cos.x)|^2) by WSIERP_1:1 .=((cos.x)|^(2+1)) by NEWTON:6 .=(cos.x)|^3; hence ((sin-((1/3)(#)(( #Z 3)*sin)))`|Z).x =(cos.x)|^3; end; hence thesis by A1,A3,A4,FDIFF_1:19; end; :: 49 f.x=sin(ln x) theorem Z c= dom (sin*ln) implies sin*ln is_differentiable_on Z & for x st x in Z holds ((sin*ln)`|Z).x =cos.(log(number_e,x))/x proof assume A1: Z c= dom (sin*ln); then for y being object st y in Z holds y in dom ln by FUNCT_1:11; then A2: Z c= dom ln by TARSKI:def 3; then A3: ln is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:18; A4: for x st x in Z holds sin*ln is_differentiable_in x proof let x; assume x in Z; then A5: ln is_differentiable_in x by A3,FDIFF_1:9; sin is_differentiable_in ln.x by SIN_COS:64; hence thesis by A5,FDIFF_2:13; end; then A6: sin*ln is_differentiable_on Z by A1,FDIFF_1:9; for x st x in Z holds ((sin*ln)`|Z).x =cos.(log(number_e,x))/x proof let x; A7: sin is_differentiable_in ln.x by SIN_COS:64; assume A8: x in Z; then A9: x in right_open_halfline(0) by A1,FUNCT_1:11,TAYLOR_1:18; ln is_differentiable_in x by A3,A8,FDIFF_1:9; then diff(sin*ln,x) = diff(sin,ln.x)*diff(ln,x) by A7,FDIFF_2:13 .=cos.(ln.x)*diff(ln,x) by SIN_COS:64 .=cos.(log(number_e,x))*diff(ln,x) by A9,TAYLOR_1:def 2 .=cos.(log(number_e,x))*(1/x) by A2,A8,TAYLOR_1:18 .=cos.(log(number_e,x))/x by XCMPLX_1:99; hence thesis by A6,A8,FDIFF_1:def 7; end; hence thesis by A1,A4,FDIFF_1:9; end; :: 50 f.x=-cos(ln x) theorem Z c= dom (-(cos*ln)) implies -(cos*ln) is_differentiable_on Z & for x st x in Z holds ((-(cos*ln))`|Z).x =sin.(log(number_e,x))/x proof assume A1: Z c= dom (-(cos*ln)); then A2: Z c= dom (cos*ln) by VALUED_1:8; then for y being object st y in Z holds y in dom ln by FUNCT_1:11; then A3: Z c= dom ln by TARSKI:def 3; then A4: ln is_differentiable_on Z by FDIFF_1:26,TAYLOR_1:18; for x st x in Z holds cos*ln is_differentiable_in x proof let x; assume x in Z; then A5: ln is_differentiable_in x by A4,FDIFF_1:9; cos is_differentiable_in ln.x by SIN_COS:63; hence thesis by A5,FDIFF_2:13; end; then A6: cos*ln is_differentiable_on Z by A2,FDIFF_1:9; A7: for x st x in Z holds ((-(cos*ln))`|Z).x =sin.(log(number_e,x))/x proof let x; A8: cos is_differentiable_in ln.x by SIN_COS:63; assume A9: x in Z; then A10: x in right_open_halfline(0) by A2,FUNCT_1:11,TAYLOR_1:18; A11: ln is_differentiable_in x by A4,A9,FDIFF_1:9; ((-(cos*ln))`|Z).x =(-1)*diff((cos*ln),x) by A1,A6,A9,FDIFF_1:20 .=(-1)*(diff(cos,ln.x)*diff(ln,x)) by A11,A8,FDIFF_2:13 .=(-1)*((-sin.(ln.x))*diff(ln,x)) by SIN_COS:63 .=(-1)*(-sin.(ln.x))*diff(ln,x) .=(-1)*(-sin.(log(number_e,x)))*diff(ln,x) by A10,TAYLOR_1:def 2 .=(-1)*(-sin.(log(number_e,x)))*(1/x) by A3,A9,TAYLOR_1:18 .=sin.(log(number_e,x))/x by XCMPLX_1:99; hence thesis; end; Z c= dom ((-1)(#)(cos*ln)) by A1; hence thesis by A6,A7,FDIFF_1:20; end;