:: Difference and Difference Quotient -- Part {III} :: by Xiquan Liang and Ling Tang :: :: Received November 17, 2009 :: Copyright (c) 2009-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 DIFF_1, ARYTM_3, ARYTM_1, FUNCT_1, SUBSET_1, NUMBERS, RELAT_1, SERIES_1, ZFMISC_1, REAL_1, NAT_1, XXREAL_0, CARD_3, SQUARE_1, SIN_COS, VALUED_1, CARD_1; notations REAL_1, ORDINAL1, NAT_1, SERIES_1, XXREAL_0, XCMPLX_0, XREAL_0, ZFMISC_1, SUBSET_1, NUMBERS, VALUED_1, NAT_D, NEWTON, FUNCT_1, FUNCT_2, RELSET_1, SEQFUNC, SQUARE_1, SIN_COS, SIN_COS4, DIFF_1; constructors REAL_1, SEQFUNC, SERIES_1, NAT_D, PARTFUN3, DIFF_1, RELSET_1, SQUARE_1, SIN_COS, SIN_COS4, NEWTON, COMSEQ_3, RCOMP_1; registrations NUMBERS, XREAL_0, MEMBERED, VALUED_0, VALUED_1, FUNCT_2, RELSET_1, SIN_COS, XCMPLX_0, ORDINAL1, NAT_1, SQUARE_1; requirements REAL, NUMERALS, SUBSET, ARITHM; begin reserve n,m for Element of NAT; reserve h,k,r,r1,r2,x,x0,x1,x2,x3 for Real; reserve f,f1,f2 for Function of REAL,REAL; theorem :: DIFF_3:1 cD(f,h).x = fD(f,h/2).x - fD(f,-h/2).x; theorem :: DIFF_3:2 fD(f,-h/2).x = -bD(f,h/2).x; theorem :: DIFF_3:3 cD(f,h).x = bD(f,h/2).x - bD(f,-h/2).x; theorem :: DIFF_3:4 fdif(r(#)f1+f2,h).(n+1).x = r* fdif(f1,h).(n+1).x + fdif(f2,h).(n+1).x; theorem :: DIFF_3:5 fdif(f1+r(#)f2,h).(n+1).x = fdif(f1,h).(n+1).x + r* fdif(f2,h).(n+1).x; theorem :: DIFF_3:6 fdif(r1(#)f1-r2(#)f2,h).(n+1).x = r1* fdif(f1,h).(n+1).x - r2* fdif(f2,h).(n+1).x; theorem :: DIFF_3:7 fdif(f,h).1 = fD(f,h); theorem :: DIFF_3:8 bdif(r(#)f1+f2,h).(n+1).x = r* bdif(f1,h).(n+1).x + bdif(f2,h).(n+1).x; theorem :: DIFF_3:9 bdif(f1+r(#)f2,h).(n+1).x = bdif(f1,h).(n+1).x + r* bdif(f2,h).(n+1).x; theorem :: DIFF_3:10 bdif(r1(#)f1-r2(#)f2,h).(n+1).x = r1* bdif(f1,h).(n+1).x - r2* bdif(f2,h).(n+1).x; theorem :: DIFF_3:11 bdif(f,h).1 = bD(f,h); theorem :: DIFF_3:12 (bdif(bdif(f,h).m,h).n).x = bdif(f,h).(m+n).x; theorem :: DIFF_3:13 cdif(r(#)f1+f2,h).(n+1).x = r* cdif(f1,h).(n+1).x + cdif(f2,h).(n+1).x; theorem :: DIFF_3:14 cdif(f1+r(#)f2,h).(n+1).x = cdif(f1,h).(n+1).x + r* cdif(f2,h).(n+1).x; theorem :: DIFF_3:15 cdif(r1(#)f1-r2(#)f2,h).(n+1).x = r1* cdif(f1,h).(n+1).x - r2* cdif(f2,h).(n+1).x; theorem :: DIFF_3:16 cdif(f,h).1 = cD(f,h); theorem :: DIFF_3:17 (cdif(cdif(f,h).m,h).n).x = cdif(f,h).(m+n).x; theorem :: DIFF_3:18 (fdif(f,h).n).x = (cdif(f,h).n).(x+(n/2)*h) implies (bdif(f,h).n).x = (cdif(f,h).n).(x-(n/2)*h); theorem :: DIFF_3:19 (fdif(f,h).n).x = (cdif(f,h).n).(x+((n-1)/2)*h+h/2) implies (bdif(f,h).n).x = (cdif(f,h).n).(x-((n-1)/2)*h-h/2); theorem :: DIFF_3:20 [!f,x,x+h!] = (fD(f,h).x)/h; theorem :: DIFF_3:21 [!f,x-h,x!] = (bD(f,h).x)/h; theorem :: DIFF_3:22 [!f,x-h/2,x+h/2!] = (cD(f,h).x)/h; theorem :: DIFF_3:23 [!f,x-h/2,x+h/2!] = (cdif(f,h).1.x)/h; theorem :: DIFF_3:24 h<>0 implies [!f,x-h,x,x+h!] = (cdif(f,h).2.x)/(2*h*h); theorem :: DIFF_3:25 [!(f1-f2),x0,x1!] = [!f1,x0,x1!] - [!f2,x0,x1!]; theorem :: DIFF_3:26 [!(r(#)f1+f2),x0,x1!] = r* [!f1,x0,x1!] + [!f2,x0,x1!]; theorem :: DIFF_3:27 [!(r(#)f1-f2),x0,x1!] = r* [!f1,x0,x1!] - [!f2,x0,x1!]; theorem :: DIFF_3:28 [!(f1+r(#)f2),x0,x1!] = [!f1,x0,x1!] + r* [!f2,x0,x1!]; theorem :: DIFF_3:29 [!(f1-r(#)f2),x0,x1!] = [!f1,x0,x1!] - r* [!f2,x0,x1!]; theorem :: DIFF_3:30 [!(r1(#)f1-r2(#)f2),x0,x1!] = r1* [!f1,x0,x1!] - r2* [!f2,x0,x1!]; theorem :: DIFF_3:31 (bdif(f1(#)f2,h).1).x = f1.x* (bdif(f2,h).1).x + f2.(x-h)* (bdif(f1,h).1).x; theorem :: DIFF_3:32 x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!] = [!f,x0,x2,x1!]; reserve S for Seq_Sequence; theorem :: DIFF_3:33 (for n, i be Nat st i<=n holds (S.n).i=(n choose i) * bdif(f1,h).i.x * bdif(f2,h).(n-'i).(x-i*h)) implies bdif(f1(#)f2,h).1.x = Sum(S.1, 1) & bdif(f1(#)f2,h).2.x = Sum(S.2, 2); theorem :: DIFF_3:34 (cdif(f1(#)f2,h).1).x = f1.(x+h/2)* (cdif(f2,h).1).x + f2.(x-h/2)* (cdif(f1,h).1).x; theorem :: DIFF_3:35 (for n,i be Nat st i<=n holds (S.n).i=(n choose i) * (cdif(f1,h).i).(x+(n-'i)*(h/2)) * (cdif(f2,h).(n-'i)).(x-i*(h/2))) implies cdif(f1(#)f2,h).1.x = Sum(S.1, 1) & cdif(f1(#)f2,h).2.x = Sum(S.2, 2); :: f.x=sqrt x theorem :: DIFF_3:36 (for x holds f.x = sqrt x) & x0<>x1 & x0>0 & x1>0 implies [!f,x0,x1!] = 1/(sqrt x0 + sqrt x1); theorem :: DIFF_3:37 (for x holds f.x = sqrt x) & x0,x1,x2 are_mutually_distinct & x0>0 & x1>0 & x2>0 implies [!f,x0,x1,x2!] = -1/((sqrt x0+sqrt x1)*(sqrt x0+sqrt x2)*(sqrt x1+sqrt x2)); theorem :: DIFF_3:38 (for x holds f.x = sqrt x) & x0,x1,x2,x3 are_mutually_distinct & x0>0 & x1>0 & x2>0 & x3>0 implies [!f,x0,x1,x2,x3!] = (sqrt x0+sqrt x1+sqrt x2+sqrt x3)/((sqrt x0+sqrt x1) *(sqrt x0+sqrt x2)*(sqrt x0+sqrt x3)*(sqrt x1+sqrt x2)*(sqrt x1+sqrt x3) *(sqrt x2+sqrt x3)); theorem :: DIFF_3:39 (for x holds f.x = sqrt x) & x>0 & x+h>0 implies fD(f,h).x = sqrt (x+h) - sqrt x; theorem :: DIFF_3:40 (for x holds f.x = sqrt x) & x>0 & x-h>0 implies bD(f,h).x = sqrt x - sqrt (x-h); theorem :: DIFF_3:41 (for x holds f.x = sqrt x) & x+h/2>0 & x-h/2>0 implies cD(f,h).x = sqrt (x+h/2) - sqrt (x-h/2); :: f.x=x^2 theorem :: DIFF_3:42 (for x holds f.x = x^2) & x0<>x1 implies [!f,x0,x1!] = x0+x1; theorem :: DIFF_3:43 (for x holds f.x = x^2) & x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!] = 1; theorem :: DIFF_3:44 (for x holds f.x = x^2) & x0,x1,x2,x3 are_mutually_distinct implies [!f,x0,x1,x2,x3!] = 0; theorem :: DIFF_3:45 (for x holds f.x = x^2) implies fD(f,h).x = 2*x*h + h^2; theorem :: DIFF_3:46 (for x holds f.x = x^2) implies bD(f,h).x = h*(2*x-h); theorem :: DIFF_3:47 (for x holds f.x = x^2) implies cD(f,h).x = 2*h*x; :: f.x=k/(x^2) theorem :: DIFF_3:48 (for x holds f.x = k/(x^2)) & x0<>x1 & x0<>0 & x1<>0 implies [!f,x0,x1!] = -(k/(x0*x1))*(1/x0+1/x1); theorem :: DIFF_3:49 (for x holds f.x = k/(x^2)) & x0<>0 & x1<>0 & x2<>0 & x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!] = (k/(x0*x1*x2))*(1/x0+1/x1+1/x2); theorem :: DIFF_3:50 (for x holds f.x = k/(x^2)) & x<>0 & x+h<>0 implies fD(f,h).x = (-k)*h*(2*x+h)/((x^2+h*x)^2); theorem :: DIFF_3:51 (for x holds f.x = k/(x^2)) & x<>0 & x-h<>0 implies bD(f,h).x = (-k)*h*(2*x-h)/((x^2-x*h)^2); theorem :: DIFF_3:52 (for x holds f.x = k/(x^2)) & x+h/2<>0 & x-h/2<>0 implies cD(f,h).x = (-2*h*k*x)/((x^2-(h/2)^2)^2); :: f.x=(sin x)^3 theorem :: DIFF_3:53 [!sin(#)sin(#)sin,x0,x1!] = (1/2)*(3*cos((x0+x1)/2)*sin((x0-x1)/2) -cos(3*(x0+x1)/2)*sin(3*(x0-x1)/2))/(x0-x1); theorem :: DIFF_3:54 fD(sin(#)sin(#)sin,h).x =(1/2)*(3*cos((2*x+h)/2)*sin(h/2)-cos(3*(2*x+h)/2)*sin(3*h/2)); theorem :: DIFF_3:55 bD(sin(#)sin(#)sin,h).x = (1/2)*(3*cos((2*x-h)/2)*sin(h/2)-cos(3*(2*x-h)/2)*sin(3*h/2)); theorem :: DIFF_3:56 cD(sin(#)sin(#)sin,h).x = (1/2)*(3*cos(x)*sin(h/2)-cos(3*x)*sin(3*h/2)); :: f.x=(cos x)^3 theorem :: DIFF_3:57 [!cos(#)cos(#)cos,x0,x1!] = -(1/2)*(3*sin((x0+x1)/2)*sin((x0-x1)/2) +sin((3*x0+3*x1)/2)*sin((3*x0-3*x1)/2))/(x0-x1); theorem :: DIFF_3:58 fD(cos(#)cos(#)cos,h).x= -(1/2)*(3*sin((2*x+h)/2)*sin(h/2) +sin((3*(2*x+h))/2)*sin(3*h/2)); theorem :: DIFF_3:59 bD(cos(#)cos(#)cos,h).x = -(1/2)*(3*sin((2*x-h)/2)*sin(h/2)+sin((3*(2*x-h))/2)*sin(3*h/2)); theorem :: DIFF_3:60 cD(cos(#)cos(#)cos,h).x = -(1/2)*(3*sin(x)*sin(h/2)+sin(3*x)*sin(3*h/2)); :: f.x=1/sin(x) theorem :: DIFF_3:61 (for x holds f.x = 1/sin(x)) & sin(x0)<>0 & sin(x1)<>0 implies [!f,x0,x1!] = -2*(sin(x1)-sin(x0))/(cos(x0+x1)-cos(x0-x1))/(x0-x1); theorem :: DIFF_3:62 (for x holds f.x = 1/sin(x)) & sin(x)<>0 & sin(x+h)<>0 implies fD(f,h).x = -2*(sin(x)-sin(x+h))/(cos(2*x+h)-cos(h)); theorem :: DIFF_3:63 (for x holds f.x = 1/sin(x)) & sin(x)<>0 & sin(x-h)<>0 implies bD(f,h).x = (-2)*(sin(x-h)-sin(x))/(cos(2*x-h)-cos(h)); theorem :: DIFF_3:64 (for x holds f.x = 1/sin(x)) & sin(x+h/2)<>0 & sin(x-h/2)<>0 implies cD(f,h).x = -2*(sin(x-h/2)-sin(x+h/2))/(cos(2*x)-cos(h)); :: f.x=1/cos(x) theorem :: DIFF_3:65 (for x holds f.x = 1/cos(x)) & x0<>x1 & cos(x0)<>0 & cos(x1)<>0 implies [!f,x0,x1!] = 2*(cos(x1)-cos(x0))/(cos(x0+x1)+cos(x0-x1))/(x0-x1); theorem :: DIFF_3:66 (for x holds f.x = 1/cos(x)) & cos(x)<>0 & cos(x+h)<>0 implies fD(f,h).x = 2*(cos(x)-cos(x+h))/(cos(2*x+h)+cos(h)); theorem :: DIFF_3:67 (for x holds f.x = 1/cos(x)) & cos(x)<>0 & cos(x-h)<>0 implies bD(f,h).x = 2*(cos(x-h)-cos(x))/(cos(2*x-h)+cos(h)); theorem :: DIFF_3:68 (for x holds f.x = 1/cos(x)) & cos(x+h/2)<>0 & cos(x-h/2)<>0 implies cD(f,h).x = 2*(cos(x-h/2)-cos(x+h/2))/(cos(2*x)+cos(h)); :: f.x=1/(sin(x))^2 theorem :: DIFF_3:69 (for x holds f.x=1/(sin(x))^2) & x0<>x1 & sin(x0)<>0 & sin(x1)<>0 implies [!f,x0,x1!] = 16*cos((x1+x0)/2)*sin((x1-x0)/2) *cos((x1-x0)/2)*sin((x1+x0)/2)/(((cos(x0+x1)-cos(x0-x1))^2)*(x0-x1)); theorem :: DIFF_3:70 (for x holds f.x=1/(sin(x))^2) & sin(x)<>0 & sin(x+h)<>0 implies fD(f,h).x = 16*cos((2*x+h)/2)*sin((-h)/2)*cos((-h)/2)*sin((2*x+h)/2) /((cos(2*x+h)-cos(h))^2); theorem :: DIFF_3:71 (for x holds f.x=1/(sin(x))^2) & sin(x)<>0 & sin(x-h)<>0 implies bD(f,h).x = 16*cos((2*x-h)/2)*sin((-h)/2)*cos((-h)/2)*sin((2*x-h)/2) /((cos(2*x-h)-cos(h))^2); theorem :: DIFF_3:72 (for x holds f.x=1/(sin(x))^2) & sin(x+h/2)<>0 & sin(x-h/2)<>0 implies cD(f,h).x = 16*cos(x)*sin((-h)/2)*cos((-h)/2)*sin(x)/((cos(2*x)-cos(h))^2); :: f.x=1/(cos(x)^2) theorem :: DIFF_3:73 (for x holds f.x=1/(cos(x))^2) & x0<>x1 & cos(x0)<>0 & cos(x1)<>0 implies [!f,x0,x1!] = (-16)*sin((x1+x0)/2)*sin((x1-x0)/2)*cos((x1+x0)/2) *cos((x1-x0)/2)/((cos(x0+x1)+cos(x0-x1))^2)/(x0-x1); theorem :: DIFF_3:74 (for x holds f.x=1/(cos(x))^2) & cos(x)<>0 & cos(x+h)<>0 implies fD(f,h).x = (-16)*sin((2*x+h)/2)*sin((-h)/2)*cos((2*x+h)/2) *cos((-h)/2)/((cos(2*x+h)+cos(h))^2); theorem :: DIFF_3:75 (for x holds f.x=1/(cos(x))^2) & cos(x)<>0 & cos(x-h)<>0 implies bD(f,h).x = (-16)*sin((2*x-h)/2)*sin((-h)/2)*cos((2*x-h)/2) *cos((-h)/2)/((cos(2*x-h)+cos(h))^2); theorem :: DIFF_3:76 (for x holds f.x=1/(cos(x))^2) & cos(x+h/2)<>0 & cos(x-h/2)<>0 implies cD(f,h).x = (-16)*sin(x)*sin((-h)/2)*cos(x)*cos((-h)/2) /((cos(2*x)+cos(h))^2); :: f.x=tan(x)*sin(x) theorem :: DIFF_3:77 x0 in dom tan & x1 in dom tan implies [!tan(#)sin,x0,x1!] = (1/cos(x0)-cos(x0)-1/cos(x1)+cos(x1))/(x0-x1); theorem :: DIFF_3:78 (for x holds f.x = (tan(#)sin).x) & x in dom tan & x+h in dom tan implies fD(f,h).x = 1/cos(x+h)-cos(x+h)-1/cos(x)+cos(x); theorem :: DIFF_3:79 (for x holds f.x = (tan(#)sin).x) & x in dom tan & x-h in dom tan implies bD(f,h).x = 1/cos(x)-cos(x)-1/cos(x-h)+cos(x-h); theorem :: DIFF_3:80 (for x holds f.x = (tan(#)sin).x) & x+h/2 in dom tan & x-h/2 in dom tan implies cD(f,h).x = 1/cos(x+h/2)-cos(x+h/2)-1/cos(x-h/2)+cos(x-h/2); :: f.x=tan(x)*cos(x) theorem :: DIFF_3:81 (for x holds f.x = (tan(#)cos).x) & x0 in dom tan & x1 in dom tan implies [!f,x0,x1!] = (sin(x0)-sin(x1))/(x0-x1); theorem :: DIFF_3:82 (for x holds f.x = (tan(#)cos).x) & x in dom tan & x+h in dom tan implies fD(f,h).x = sin(x+h)-sin(x); theorem :: DIFF_3:83 (for x holds f.x = (tan(#)cos).x) & x in dom tan & x-h in dom tan implies bD(f,h).x = sin(x)-sin(x-h); theorem :: DIFF_3:84 (for x holds f.x = (tan(#)cos).x) & x+h/2 in dom tan & x-h/2 in dom tan implies cD(f,h).x = sin(x+h/2)-sin(x-h/2); :: f.x=cot(x)*cos(x) theorem :: DIFF_3:85 (for x holds f.x = (cot(#)cos).x) & x0 in dom cot & x1 in dom cot implies [!f,x0,x1!] = (1/sin(x0)-sin(x0)-1/sin(x1)+sin(x1))/(x0-x1); theorem :: DIFF_3:86 (for x holds f.x = (cot(#)cos).x) & x in dom cot & x+h in dom cot implies fD(f,h).x = 1/sin(x+h)-sin(x+h)-1/sin(x)+sin(x); theorem :: DIFF_3:87 (for x holds f.x = (cot(#)cos).x) & x in dom cot & x-h in dom cot implies bD(f,h).x = 1/sin(x)-sin(x)-1/sin(x-h)+sin(x-h); theorem :: DIFF_3:88 (for x holds f.x = (cot(#)cos).x) & x+h/2 in dom cot & x-h/2 in dom cot implies cD(f,h).x = 1/sin(x+h/2)-sin(x+h/2)-1/sin(x-h/2)+sin(x-h/2); :: f.x=cot(x)*sin(x) theorem :: DIFF_3:89 (for x holds f.x = (cot(#)sin).x) & x0 in dom cot & x1 in dom cot implies [!f,x0,x1!] = (cos(x0)-cos(x1))/(x0-x1); theorem :: DIFF_3:90 (for x holds f.x = (cot(#)sin).x) & x in dom cot & x+h in dom cot implies fD(f,h).x = cos(x+h)-cos(x); theorem :: DIFF_3:91 (for x holds f.x = (cot(#)sin).x) & x in dom cot & x-h in dom cot implies bD(f,h).x = cos(x)-cos(x-h); theorem :: DIFF_3:92 (for x holds f.x = (cot(#)sin).x) & x+h/2 in dom cot & x-h/2 in dom cot implies cD(f,h).x = cos(x+h/2)-cos(x-h/2); :: f.x=(tan(x))^2 theorem :: DIFF_3:93 (for x holds f.x=(tan(#)tan).x) & x0 in dom tan & x1 in dom tan implies [!f,x0,x1!] = ((cos(x1))^2-(cos(x0))^2)/((cos(x0)*cos(x1))^2*(x0-x1)) ; theorem :: DIFF_3:94 (for x holds f.x=(tan(#)tan).x) & x in dom tan & x+h in dom tan implies fD(f,h).x = -(1/2)*(cos(2*(x+h))-cos(2*x))/((cos(x+h)*cos(x))^2); theorem :: DIFF_3:95 (for x holds f.x=(tan(#)tan).x) & x in dom tan & x-h in dom tan implies bD(f,h).x = -(1/2)*(cos(2*x)-cos(2*(h-x)))/((cos(x)*cos(x-h))^2); theorem :: DIFF_3:96 (for x holds f.x=(tan(#)tan).x) & x+h/2 in dom tan & x-h/2 in dom tan implies cD(f,h).x = -(1/2)*(cos(h+2*x)-cos(h-2*x))/((cos(x+h/2)*cos(x-h/2))^2);