:: Difference and Difference Quotient -- Part {II} :: by Bo Li , Yanping Zhuang and Xiquan Liang :: :: Received October 25, 2007 :: Copyright (c) 2007-2021 Association of Mizar Users :: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland). :: This code can be distributed under the GNU General Public Licence :: version 3.0 or later, or the Creative Commons Attribution-ShareAlike :: License version 3.0 or later, subject to the binding interpretation :: detailed in file COPYING.interpretation. :: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these :: licenses, or see http://www.gnu.org/licenses/gpl.html and :: http://creativecommons.org/licenses/by-sa/3.0/. environ vocabularies REAL_1, FUNCT_1, NUMBERS, DIFF_1, ARYTM_3, CARD_1, NAT_1, RELAT_1, SQUARE_1, ZFMISC_1, ARYTM_1, VALUED_1, VALUED_0, JGRAPH_2, SIN_COS, SIN_COS4; notations SQUARE_1, ORDINAL1, XCMPLX_0, ZFMISC_1, RELAT_1, REAL_1, NAT_1, NUMBERS, FUNCT_1, FUNCT_2, VALUED_1, SEQFUNC, SIN_COS, DIFF_1, XREAL_0, VALUED_0, FCONT_1, SIN_COS4, FDIFF_9; constructors SQUARE_1, REAL_1, DIFF_1, PARTFUN3, SIN_COS, SIN_COS4, FCONT_1, FDIFF_9, SEQFUNC, RELSET_1, VALUED_1; registrations XREAL_0, RELSET_1, MEMBERED, FUNCT_2, VALUED_0, VALUED_1, SQUARE_1, SIN_COS; requirements NUMERALS, SUBSET, BOOLE, ARITHM; begin reserve h,r,r1,r2,x0,x1,x2,x3,x4,x5,x,a,b,c,k for Real, f,f1,f2 for Function of REAL,REAL; theorem :: DIFF_2:1 [!f,x,x+h!] = (fdif(f,h).1.x)/h; theorem :: DIFF_2:2 h<>0 implies [!f,x,x+h,x+2*h!] = (fdif(f,h).2.x)/(2*h^2); theorem :: DIFF_2:3 [!f,x-h,x!] = (bdif(f,h).1.x)/h; theorem :: DIFF_2:4 h<>0 implies [!f,x-2*h,x-h,x!] = (bdif(f,h).2.x)/(2*h^2); theorem :: DIFF_2:5 [!(r(#)f),x0,x1,x2!] = r*[!f,x0,x1,x2!]; theorem :: DIFF_2:6 [!(f1+f2),x0,x1,x2!] = [!f1,x0,x1,x2!]+[!f2,x0,x1,x2!]; theorem :: DIFF_2:7 [!(r1(#)f1+r2(#)f2),x0,x1,x2!] = r1*[!f1,x0,x1,x2!]+r2*[!f2,x0,x1,x2!]; theorem :: DIFF_2:8 [!(r(#)f),x0,x1,x2,x3!] = r*[!f,x0,x1,x2,x3!]; theorem :: DIFF_2:9 [!(f1+f2),x0,x1,x2,x3!]=[!f1,x0,x1,x2,x3!]+[!f2,x0,x1,x2,x3!]; theorem :: DIFF_2:10 [!(r1(#)f1+r2(#)f2),x0,x1,x2,x3!] = r1*[!f1,x0,x1,x2,x3!]+r2*[!f2,x0, x1,x2,x3!]; definition :: Forward difference quotient of the fourth order let f be real-valued Function; let x0,x1,x2,x3,x4 be Real; func [!f,x0,x1,x2,x3,x4!] -> Real equals :: DIFF_2:def 1 ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3, x4!])/(x0-x4); end; theorem :: DIFF_2:11 [!(r(#)f),x0,x1,x2,x3,x4!] = r*[!f,x0,x1,x2,x3,x4!]; theorem :: DIFF_2:12 [!(f1+f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!]+[!f2,x0,x1,x2 ,x3,x4!]; theorem :: DIFF_2:13 [!(r1(#)f1+r2(#)f2),x0,x1,x2,x3,x4!] = r1*[!f1,x0,x1,x2,x3,x4!]+r2*[! f2,x0,x1,x2,x3,x4!]; definition :: Forward difference quotient of the fifth order let f be real-valued Function; let x0,x1,x2,x3,x4,x5 be Real; func [!f,x0,x1,x2,x3,x4,x5!] -> Real equals :: DIFF_2:def 2 ([!f,x0,x1,x2,x3,x4!] - [!f,x1, x2,x3,x4,x5!])/(x0-x5); end; theorem :: DIFF_2:14 [!(r(#)f),x0,x1,x2,x3,x4,x5!] = r*[!f,x0,x1,x2,x3,x4,x5!]; theorem :: DIFF_2:15 [!(f1+f2),x0,x1,x2,x3,x4,x5!] =[!f1,x0,x1,x2,x3,x4,x5!]+[!f2,x0, x1,x2,x3,x4,x5!]; theorem :: DIFF_2:16 [!(r1(#)f1+r2(#)f2),x0,x1,x2,x3,x4,x5!] = r1*[!f1,x0,x1,x2,x3,x4,x5!]+ r2*[!f2,x0,x1,x2,x3,x4,x5!]; theorem :: DIFF_2:17 x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!] = f.x0/((x0-x1) *(x0-x2))+f.x1/((x1-x0)*(x1-x2))+f.x2/((x2-x0)*(x2-x1)); theorem :: DIFF_2:18 x0,x1,x2,x3 are_mutually_distinct implies [!f,x0,x1,x2,x3!] = [!f,x1, x2,x3,x0!] & [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!]; theorem :: DIFF_2:19 x0,x1,x2,x3 are_mutually_distinct implies [!f,x0,x1,x2,x3!] = [!f,x1, x0,x2,x3!] & [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!]; theorem :: DIFF_2:20 f is constant implies [!f,x0,x1,x2!] = 0; :: f.x=a*x+b theorem :: DIFF_2:21 x0<>x1 implies [!AffineMap(a,b),x0,x1!] = a; theorem :: DIFF_2:22 x0,x1,x2 are_mutually_distinct implies [!AffineMap(a,b),x0,x1, x2!]=0; theorem :: DIFF_2:23 x0,x1,x2,x3 are_mutually_distinct implies [!AffineMap(a,b),x0,x1,x2, x3!]=0; theorem :: DIFF_2:24 for x holds fD(AffineMap(a,b),h).x = a*h; theorem :: DIFF_2:25 for x holds bD(AffineMap(a,b),h).x = a*h; theorem :: DIFF_2:26 for x holds cD(AffineMap(a,b),h).x = a*h; :: f.x=a*x^2+b*x+c theorem :: DIFF_2:27 (for x holds f.x = a*x^2+b*x+c) & x0<>x1 implies [!f,x0,x1!]=a*( x0+x1)+b; theorem :: DIFF_2:28 (for x holds f.x = a*x^2+b*x+c) & x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!]=a; theorem :: DIFF_2:29 (for x holds f.x = a*x^2+b*x+c) & x0,x1,x2,x3 are_mutually_distinct implies [!f,x0,x1,x2,x3!]=0; theorem :: DIFF_2:30 (for x holds f.x = a*x^2+b*x+c) & x0,x1,x2,x3,x4 are_mutually_distinct implies [!f,x0,x1,x2,x3,x4!] = 0; theorem :: DIFF_2:31 (for x holds f.x = a*x^2+b*x+c) implies for x holds fD(f,h).x = 2*a*h* x+a*h^2+b*h; theorem :: DIFF_2:32 (for x holds f.x = a*x^2+b*x+c) implies for x holds bD(f,h).x = 2*a*h* x-a*h^2+b*h; theorem :: DIFF_2:33 (for x holds f.x = a*x^2+b*x+c) implies for x holds cD(f,h).x = 2*a*h* x+b*h; :: f.x=k/x theorem :: DIFF_2:34 (for x holds f.x = k/x) & x0<>x1 & x0<>0 & x1<>0 implies [!f,x0, x1!] = - k/(x0*x1); theorem :: DIFF_2:35 (for x holds f.x = k/x) & x0<>0 & x1<>0 & x2<>0 & x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!] = k/(x0*x1*x2); theorem :: DIFF_2:36 (for x holds f.x = k/x) & x0<>0 & x1<>0 & x2<>0 & x3<>0 & x0,x1, x2,x3 are_mutually_distinct implies [!f,x0,x1,x2,x3!]=-k/(x0*x1*x2*x3); theorem :: DIFF_2:37 (for x holds f.x = k/x) & x0<>0 & x1<>0 & x2<>0 & x3<>0 & x4<>0 & x0, x1,x2,x3,x4 are_mutually_distinct implies [!f,x0,x1,x2,x3,x4!] = k/(x0*x1*x2* x3*x4); theorem :: DIFF_2:38 (for x holds f.x = k/x & x<>0 & x+h<>0) implies for x holds fD(f,h).x = (-k*h)/((x+h)*x); theorem :: DIFF_2:39 (for x holds f.x = k/x & x<>0 & x-h<>0) implies for x holds bD(f,h).x = (-k*h)/((x-h)*x); theorem :: DIFF_2:40 (for x holds f.x = k/x & x+h/2<>0 & x-h/2<>0) implies for x holds cD(f ,h).x = (-k*h)/((x-h/2)*(x+h/2)); :: f.x = sin(x) theorem :: DIFF_2:41 [!sin,x0,x1!] = 2*cos((x0+x1)/2)*sin((x0-x1)/2)/(x0-x1); theorem :: DIFF_2:42 for x holds fD(sin,h).x = 2*(cos((2*x+h)/2)*sin(h/2)); theorem :: DIFF_2:43 for x holds bD(sin,h).x = 2*(cos((2*x-h)/2)*sin(h/2)); theorem :: DIFF_2:44 for x holds cD(sin,h).x = 2*(cos(x)*sin(h/2)); :: f.x = cos(x) theorem :: DIFF_2:45 [!cos,x0,x1!] = -2*sin((x0+x1)/2)*sin((x0-x1)/2)/(x0-x1); theorem :: DIFF_2:46 for x holds fD(cos,h).x = -2*(sin((2*x+h)/2)*sin(h/2)); theorem :: DIFF_2:47 for x holds bD(cos,h).x = -2*(sin((2*x-h)/2)*sin(h/2)); theorem :: DIFF_2:48 for x holds cD(cos,h).x = -2*(sin(x)*sin(h/2)); :: f.x = (sin x)^2 theorem :: DIFF_2:49 [!sin(#)sin,x0,x1!] = (1/2)*(cos(2*x1)-cos(2*x0))/(x0-x1); theorem :: DIFF_2:50 for x holds fD(sin(#)sin,h).x = (1/2)*(cos(2*x)-cos(2*(x+h))); theorem :: DIFF_2:51 for x holds bD(sin(#)sin,h).x = (1/2)*(cos(2*(x-h))-cos(2*x)); theorem :: DIFF_2:52 for x holds cD(sin(#)sin,h).x = (1/2)*(cos(2*x-h)-cos(2*x+h)); :: f.x = sin(x)*cos(x) theorem :: DIFF_2:53 [!sin(#)cos,x0,x1!] = (1/2)*(sin(2*x0)-sin(2*x1))/(x0-x1); theorem :: DIFF_2:54 for x holds fD(sin(#)cos,h).x = (1/2)*(sin(2*(x+h))-sin(2*x)); theorem :: DIFF_2:55 for x holds bD(sin(#)cos,h).x = (1/2)*(sin(2*x)-sin(2*(x-h))); theorem :: DIFF_2:56 for x holds cD(sin(#)cos,h).x = (1/2)*(sin(2*x+h)-sin(2*x-h)); :: f.x = (cos(x))^2 theorem :: DIFF_2:57 [!cos(#)cos,x0,x1!] = (1/2)*(cos(2*x0)-cos(2*x1))/(x0-x1); theorem :: DIFF_2:58 for x holds fD(cos(#)cos,h).x = (1/2)*(cos(2*(x+h))-cos(2*x)); theorem :: DIFF_2:59 for x holds bD(cos(#)cos,h).x = (1/2)*(cos(2*x)-cos(2*(x-h))); theorem :: DIFF_2:60 for x holds cD(cos(#)cos,h).x = (1/2)*(cos(2*x+h)-cos(2*x-h)); :: f.x = (sin(x))^2*cos(x) theorem :: DIFF_2:61 [!sin(#)sin(#)cos,x0,x1!] = -(1/2)*(sin(3*(x1+x0)/2)*sin(3*(x1-x0)/2) +sin((x0+x1)/2)*sin((x0-x1)/2))/(x0-x1); theorem :: DIFF_2:62 for x holds fD(sin(#)sin(#)cos,h).x =(1/2)*(sin((6*x+3*h)/2)*sin(3*h/2 )-sin((2*x+h)/2)*sin(h/2)); theorem :: DIFF_2:63 for x holds bD(sin(#)sin(#)cos,h).x = (1/2)*(sin((6*x-3*h)/2)*sin(3*h/ 2))-(1/2)*(sin((2*x-h)/2)*sin(h/2)); theorem :: DIFF_2:64 for x holds cD(sin(#)sin(#)cos,h).x = -(1/2)*(sin(x)*sin(h/2))+(1/2)*( sin(3*x)*sin(3*h/2)); :: f.x = sin(x)*(cos(x))^2 theorem :: DIFF_2:65 [!sin(#)cos(#)cos,x0,x1!] = (1/2)*(cos((x0+x1)/2)*sin((x0-x1)/2) +cos( 3*(x0+x1)/2)*sin(3*(x0-x1)/2))/(x0-x1); theorem :: DIFF_2:66 for x holds fD(sin(#)cos(#)cos,h).x = (1/2)*(cos((2*x+h)/2)*sin(h/2)+ cos((6*x+3*h)/2)*sin(3*h/2)); theorem :: DIFF_2:67 for x holds bD(sin(#)cos(#)cos,h).x = (1/2)*(cos((2*x-h)/2)*sin(h/2)+ cos((6*x-3*h)/2)*sin(3*h/2)); theorem :: DIFF_2:68 for x holds cD(sin(#)cos(#)cos,h).x = (1/2)*(cos(x)*sin(h/2)+cos(3*x)* sin(3*h/2)); :: f.x = tan(x) theorem :: DIFF_2:69 x0 in dom tan & x1 in dom tan implies [!tan,x0,x1!]=sin(x0-x1)/(cos(x0 )*cos(x1)*(x0-x1)); :: f.x = cot(x) theorem :: DIFF_2:70 x0 in dom cot & x1 in dom cot implies [!cot,x0,x1!] = - sin(x0-x1)/( sin(x0)*sin(x1)*(x0-x1)); :: f.x = cosec(x) theorem :: DIFF_2:71 x0 in dom cosec & x1 in dom cosec implies [!cosec,x0,x1!] = 2*cos((x1+ x0)/2)*sin((x1-x0)/2) /(sin(x1)*sin(x0)*(x0-x1)); :: f.x = sec(x) theorem :: DIFF_2:72 x0 in dom sec & x1 in dom sec implies [!sec,x0,x1!] = -2*sin((x1+x0)/2 ) *sin((x1-x0)/2)/(cos(x1)*cos(x0)*(x0-x1));