:: Difference and Difference Quotient -- Part {II} :: by Bo Li , Yanping Zhuang and Xiquan Liang :: :: Received October 25, 2007 :: Copyright (c) 2007-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 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; equalities DIFF_1, SIN_COS4, SQUARE_1, SIN_COS, FDIFF_9; theorems DIFF_1, XCMPLX_1, SIN_COS4, ZFMISC_1, RFUNCT_1, FCONT_1, FDIFF_8, VALUED_1; 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 Th1: [!f,x,x+h!] = (fdif(f,h).1.x)/h proof [!f,x,x+h!] = [!f,x+h,x!] by DIFF_1:29 .= (fD(f,h).x)/h by DIFF_1:3 .= (fD(fdif(f,h).0,h).x)/h by DIFF_1:def 6 .= (fdif(f,h).(0 qua Nat+1).x)/h by DIFF_1:def 6; hence thesis; end; theorem h<>0 implies [!f,x,x+h,x+2*h!] = (fdif(f,h).2.x)/(2*h^2) proof A1: fdif(f,h).1 is Function of REAL,REAL by DIFF_1:2; assume A2: h<>0; then A3: x+h<>x+2*h; x<>x+h & x<>x+2*h by A2; then x, x+h, x+2*h are_mutually_distinct by A3,ZFMISC_1:def 5; then [!f,x,x+h,x+2*h!] = [!f,x+2*h,x+h,x!] by DIFF_1:34 .= ([!f,x+h,x+2*h!]-[!f,x+h,x!])/((x+2*h)-x) by DIFF_1:29 .= ([!f,x+h,(x+h)+h!]-[!f,x,x+h!])/((x+2*h)-x) by DIFF_1:29 .= ((fdif(f,h).1.(x+h))/h-[!f,x,x+h!])/((x+2*h)-x) by Th1 .= ((fdif(f,h).1.(x+h))/h -(fdif(f,h).1.x)/h)/((x+2*h)-x) by Th1 .= (fdif(f,h).1.(x+h)-(fdif(f,h).1.x)) /h/((x+2*h)-x) by XCMPLX_1:120 .= (fD(fdif(f,h).1,h).x/h)/(2*h) by A1,DIFF_1:3 .= ((fdif(f,h).(1+1).x)/h)/(2*h) by DIFF_1:def 6 .= (fdif(f,h).2.x)/(h*(2*h)) by XCMPLX_1:78 .= (fdif(f,h).2.x)/(2*(h^2)); hence thesis; end; theorem Th3: [!f,x-h,x!] = (bdif(f,h).1.x)/h proof [!f,x-h,x!] = [!f,x,x-h!] by DIFF_1:29 .= (bD(f,h).x)/h by DIFF_1:4 .= (bD(bdif(f,h).0,h).x)/h by DIFF_1:def 7 .= (bdif(f,h).(0 qua Nat+1).x)/h by DIFF_1:def 7; hence thesis; end; theorem h<>0 implies [!f,x-2*h,x-h,x!] = (bdif(f,h).2.x)/(2*h^2) proof set y=x-h; A1: bdif(f,h).1 is Function of REAL,REAL by DIFF_1:12; assume A2: h<>0; then A3: x-h<>x-2*h; x<>x-h & x<>x-2*h by A2; then x,x-h,x-2*h are_mutually_distinct by A3,ZFMISC_1:def 5; then [!f,x-2*h,x-h,x!] = [!f,x,x-h,x-2*h!] by DIFF_1:34 .= ([!f,x-h,x!]-[!f,x-h,x-2*h!])/(x-(x-2*h)) by DIFF_1:29 .= ((bdif(f,h).1.x)/h-[!f,x-h,x-2*h!])/(x-(x-2*h)) by Th3 .= ((bdif(f,h).1.x)/h-[!f,y-h,y!])/(x-(x-2*h)) by DIFF_1:29 .= ((bdif(f,h).1.x)/h-(bdif(f,h).1.(x-h))/h)/(x-(x-2*h)) by Th3 .= ((bdif(f,h).1.x-bdif(f,h).1.(x-h))/h) /(x-(x-2*h)) by XCMPLX_1:120 .= (bD(bdif(f,h).1,h).x/h)/(2*h) by A1,DIFF_1:4 .= ((bdif(f,h).(1+1).x)/h)/(2*h) by DIFF_1:def 7 .= (bdif(f,h).2.x)/(h*(2*h)) by XCMPLX_1:78 .= (bdif(f,h).2.x)/(2*(h^2)); hence thesis; end; theorem Th5: [!(r(#)f),x0,x1,x2!] = r*[!f,x0,x1,x2!] proof [!(r(#)f),x0,x1,x2!] = (r*[!f,x0,x1!]-[!(r(#)f),x1,x2!]) /(x0-x2) by DIFF_1:31 .= (r*[!f,x0,x1!]-r*[!f,x1,x2!])/(x0-x2) by DIFF_1:31 .= (r*([!f,x0,x1!]-[!f,x1,x2!]))/(x0-x2); hence thesis by XCMPLX_1:74; end; theorem Th6: [!(f1+f2),x0,x1,x2!] = [!f1,x0,x1,x2!]+[!f2,x0,x1,x2!] proof [!(f1+f2),x0,x1,x2!] = ([!f1,x0,x1!]+[!f2,x0,x1!]-[!(f1+f2),x1,x2!])/(x0 -x2) by DIFF_1:32 .= ([!f1,x0,x1!]+[!f2,x0,x1!] -([!f1,x1,x2!]+[!f2,x1,x2!]))/(x0-x2) by DIFF_1:32 .= (([!f1,x0,x1!]-[!f1,x1,x2!]) +([!f2,x0,x1!]-[!f2,x1,x2!]))/(x0-x2); hence thesis by XCMPLX_1:62; end; theorem [!(r1(#)f1+r2(#)f2),x0,x1,x2!] = r1*[!f1,x0,x1,x2!]+r2*[!f2,x0,x1,x2!] proof [!(r1(#)f1+r2(#)f2),x0,x1,x2!] = [!(r1(#)f1),x0,x1,x2!]+[!(r2(#)f2),x0, x1,x2!] by Th6 .= r1*[!f1,x0,x1,x2!]+[!(r2(#)f2),x0,x1,x2!] by Th5; hence thesis by Th5; end; theorem Th8: [!(r(#)f),x0,x1,x2,x3!] = r*[!f,x0,x1,x2,x3!] proof [!(r(#)f),x0,x1,x2,x3!] = (r*[!f,x0,x1,x2!]-[!(r(#)f),x1,x2,x3!]) /(x0- x3) by Th5 .= (r*[!f,x0,x1,x2!]-r*[!f,x1,x2,x3!])/(x0-x3) by Th5 .= (r*([!f,x0,x1,x2!]-[!f,x1,x2,x3!]))/(x0-x3); hence thesis by XCMPLX_1:74; end; theorem Th9: [!(f1+f2),x0,x1,x2,x3!]=[!f1,x0,x1,x2,x3!]+[!f2,x0,x1,x2,x3!] proof [!(f1+f2),x0,x1,x2,x3!] = ([!f1,x0,x1,x2!]+[!f2,x0,x1,x2!] - [!(f1+f2), x1,x2,x3!])/(x0-x3) by Th6 .= ([!f1,x0,x1,x2!]+[!f2,x0,x1,x2!] - ([!f1,x1,x2,x3!]+[!f2,x1,x2,x3!])) /(x0-x3) by Th6 .= (([!f1,x0,x1,x2!] - [!f1,x1,x2,x3!]) + ([!f2,x0,x1,x2!] - [!f2,x1,x2, x3!]))/(x0-x3); hence thesis by XCMPLX_1:62; end; theorem [!(r1(#)f1+r2(#)f2),x0,x1,x2,x3!] = r1*[!f1,x0,x1,x2,x3!]+r2*[!f2,x0, x1,x2,x3!] proof [!(r1(#)f1+r2(#)f2),x0,x1,x2,x3!] = [!(r1(#)f1),x0,x1,x2,x3!] +[!(r2(#) f2),x0,x1,x2,x3!] by Th9 .= r1*[!f1,x0,x1,x2,x3!]+[!(r2(#)f2),x0,x1,x2,x3!] by Th8; hence thesis by Th8; end; 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 ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3, x4!])/(x0-x4); correctness; end; theorem Th11: [!(r(#)f),x0,x1,x2,x3,x4!] = r*[!f,x0,x1,x2,x3,x4!] proof [!(r(#)f),x0,x1,x2,x3,x4!] = (r*[!f,x0,x1,x2,x3!] -[!(r(#)f),x1,x2,x3,x4 !])/(x0-x4) by Th8 .= (r*[!f,x0,x1,x2,x3!]-r*[!f,x1,x2,x3,x4!])/(x0-x4) by Th8 .= (r*([!f,x0,x1,x2,x3!]-[!f,x1,x2,x3,x4!]))/(x0-x4); hence thesis by XCMPLX_1:74; end; theorem Th12: [!(f1+f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!]+[!f2,x0,x1,x2 ,x3,x4!] proof [!(f1+f2),x0,x1,x2,x3,x4!] = ([!f1,x0,x1,x2,x3!]+[!f2,x0,x1,x2,x3!] - [! (f1+f2),x1,x2,x3,x4!])/(x0-x4) by Th9 .= ([!f1,x0,x1,x2,x3!]+[!f2,x0,x1,x2,x3!] - ([!f1,x1,x2,x3,x4!]+[!f2,x1, x2,x3,x4!]))/(x0-x4) by Th9 .= (([!f1,x0,x1,x2,x3!] - [!f1,x1,x2,x3,x4!]) + ([!f2,x0,x1,x2,x3!] - [! f2,x1,x2,x3,x4!]))/(x0-x4); hence thesis by XCMPLX_1:62; end; theorem [!(r1(#)f1+r2(#)f2),x0,x1,x2,x3,x4!] = r1*[!f1,x0,x1,x2,x3,x4!]+r2*[! f2,x0,x1,x2,x3,x4!] proof [!(r1(#)f1+r2(#)f2),x0,x1,x2,x3,x4!] = [!(r1(#)f1),x0,x1,x2,x3,x4!] +[!( r2(#)f2),x0,x1,x2,x3,x4!] by Th12 .= r1*[!f1,x0,x1,x2,x3,x4!] +[!(r2(#)f2),x0,x1,x2,x3,x4!] by Th11; hence thesis by Th11; end; 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 ([!f,x0,x1,x2,x3,x4!] - [!f,x1, x2,x3,x4,x5!])/(x0-x5); correctness; end; theorem Th14: [!(r(#)f),x0,x1,x2,x3,x4,x5!] = r*[!f,x0,x1,x2,x3,x4,x5!] proof [!(r(#)f),x0,x1,x2,x3,x4,x5!] = (r*[!f,x0,x1,x2,x3,x4!] -[!(r(#)f),x1,x2 ,x3,x4,x5!])/(x0-x5) by Th11 .= (r*[!f,x0,x1,x2,x3,x4!] -r*[!f,x1,x2,x3,x4,x5!])/(x0-x5) by Th11 .= (r*([!f,x0,x1,x2,x3,x4!]-[!f,x1,x2,x3,x4,x5!]))/(x0-x5); hence thesis by XCMPLX_1:74; end; theorem Th15: [!(f1+f2),x0,x1,x2,x3,x4,x5!] =[!f1,x0,x1,x2,x3,x4,x5!]+[!f2,x0, x1,x2,x3,x4,x5!] proof [!(f1+f2),x0,x1,x2,x3,x4,x5!] = ([!f1,x0,x1,x2,x3,x4!]+[!f2,x0,x1,x2,x3, x4!] - [!(f1+f2),x1,x2,x3,x4,x5!])/(x0-x5) by Th12 .= ([!f1,x0,x1,x2,x3,x4!]+[!f2,x0,x1,x2,x3,x4!] - ([!f1,x1,x2,x3,x4,x5!] +[!f2,x1,x2,x3,x4,x5!]))/(x0-x5) by Th12 .= (([!f1,x0,x1,x2,x3,x4!] - [!f1,x1,x2,x3,x4,x5!]) + ([!f2,x0,x1,x2,x3, x4!] - [!f2,x1,x2,x3,x4,x5!]))/(x0-x5); hence thesis by XCMPLX_1:62; end; theorem [!(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!] proof [!(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!] by Th15 .= r1*[!f1,x0,x1,x2,x3,x4,x5!] +[!(r2(#)f2),x0,x1,x2,x3,x4,x5!] by Th14; hence thesis by Th14; end; theorem 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)) proof assume A1: x0,x1,x2 are_mutually_distinct; then A2: x1-x2<>0 by ZFMISC_1:def 5; A3: x0-x1<>0 by A1,ZFMISC_1:def 5; A4: x0-x2<>0 by A1,ZFMISC_1:def 5; [!f,x0,x1,x2!] = (f.x0-f.x1)/(x0-x1)/(x0-x2) - (f.x1-f.x2)/(x1-x2)/(x0- x2) by XCMPLX_1:120 .= (f.x0-f.x1)/((x0-x1)*(x0-x2)) - (f.x1-f.x2)/(x1-x2)/(x0-x2) by XCMPLX_1:78 .= (f.x0-f.x1)/((x0-x1)*(x0-x2)) - (f.x1-f.x2)/((x1-x2)*(x0-x2)) by XCMPLX_1:78 .= f.x0/((x0-x1)*(x0-x2)) - f.x1/((x0-x1)*(x0-x2)) - (f.x1-f.x2)/((x1-x2 )*(x0-x2)) by XCMPLX_1:120 .= f.x0/((x0-x1)*(x0-x2)) - f.x1/((x0-x1)*(x0-x2)) - (f.x1/((x1-x2)*(x0- x2)) - f.x2/((x1-x2)*(x0-x2))) by XCMPLX_1:120 .= f.x0/((x0-x1)*(x0-x2))-(f.x1/((x0-x1)*(x0-x2)) + f.x1/((x1-x2)*(x0-x2 )))+ f.x2/((x1-x2)*(x0-x2)) .= f.x0/((x0-x1)*(x0-x2)) - (f.x1*(x1-x2)/((x0-x1) *(x0-x2)*(x1-x2)) + f .x1/((x1-x2)*(x0-x2))) + f.x2/((x1-x2)*(x0-x2)) by A2,XCMPLX_1:91 .= f.x0/((x0-x1)*(x0-x2)) - (f.x1*(x1-x2)/((x0-x1)*(x0-x2) *(x1-x2)) + f .x1*(x0-x1)/((x1-x2)*(x0-x2)*(x0-x1))) + f.x2/((x1-x2)*(x0-x2)) by A3, XCMPLX_1:91 .= f.x0/((x0-x1)*(x0-x2)) - (f.x1*(x1-x2) + f.x1*(x0-x1))/((x0-x1)*(x0- x2)*(x1-x2)) + f.x2/((x1-x2)*(x0-x2)) by XCMPLX_1:62 .= f.x0/((x0-x1)*(x0-x2)) - f.x1*(x0-x2)/((x0-x1) *(x1-x2)*(x0-x2)) + f. x2/((x1-x2)*(x0-x2)) .= f.x0/((x0-x1)*(x0-x2)) - f.x1/(-(x1-x0)*(x1-x2)) + f.x2/(-(x2-x1)*(x0 -x2)) by A4,XCMPLX_1:91 .= f.x0/((x0-x1)*(x0-x2)) + - f.x1/(-((x1-x0)*(x1-x2))) + f.x2/((-(x2-x1 ))*(-(x2-x0))); hence thesis by XCMPLX_1:189; end; theorem 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!] proof set x10 = x1-x0; set x20 = x2-x0; set x30 = x3-x0; set x12 = x1-x2; set x13 = x1-x3; set x23 = x2-x3; assume A1: x0,x1,x2,x3 are_mutually_distinct; then A2: x2-x3<>0 by ZFMISC_1:def 6; A3: x3-x0<>0 by A1,ZFMISC_1:def 6; A4: x1-x3<>0 by A1,ZFMISC_1:def 6; A5: x1-x0<>0 by A1,ZFMISC_1:def 6; A6: x2-x0<>0 by A1,ZFMISC_1:def 6; A7: x1-x2<>0 by A1,ZFMISC_1:def 6; A8: [!f,x0,x1,x2,x3!] = (((f.x0-f.x1)/(-(x1-x0))-(f.x1-f.x2)/(x1-x2)) /(-(x2 -x0))-((f.x1-f.x2)/(x1-x2)-(f.x2-f.x3) /(x2-x3))/(x1-x3))/(x0-x3) .= ((-(f.x0-f.x1)/(x1-x0)-(f.x1-f.x2)/(x1-x2)) /(-(x2-x0))-((f.x1-f.x2)/ (x1-x2)-(f.x2-f.x3) /(x2-x3))/(x1-x3))/(x0-x3) by XCMPLX_1:188 .= ((-((f.x0-f.x1)/(x1-x0)+(f.x1-f.x2)/(x1-x2))) /(-(x2-x0))-((f.x1-f.x2 )/(x1-x2)-(f.x2-f.x3) /(x2-x3))/(x1-x3))/(x0-x3) .= (((f.x0-f.x1)/(x1-x0)+(f.x1-f.x2)/(x1-x2))/(x2-x0) -((f.x1-f.x2)/(x1- x2)-(f.x2-f.x3) /(x2-x3))/(x1-x3))/(x0-x3) by XCMPLX_1:191 .= (((f.x0-f.x1)*x12+(f.x1-f.x2)*x10) /(x10*x12)/x20-((f.x1-f.x2)/(x1-x2 ) -(f.x2-f.x3)/(x2-x3))/(x1-x3))/(x0-x3) by A7,A5,XCMPLX_1:116 .= (((f.x0-f.x1)*x12+(f.x1-f.x2)*x10)/(x10*x12)/x20 -((f.x1-f.x2)*x23-(f .x2-f.x3)*x12) /(x12*x23)/x13)/(x0-x3) by A2,A7,XCMPLX_1:130 .= (((f.x0-f.x1)*x12+(f.x1-f.x2)*x10)/(x10*x12*x20) -((f.x1-f.x2)*x23-(f .x2-f.x3)*x12) /(x12*x23)/x13)/(x0-x3) by XCMPLX_1:78 .= (((f.x0-f.x1)*x12+(f.x1-f.x2)*x10)/(x10*x12*x20) -((f.x1-f.x2)*x23-(f .x2-f.x3)*x12) /(x12*x23*x13))/(x0-x3) by XCMPLX_1:78 .= (-(((f.x0-f.x1)*x12+(f.x1-f.x2)*x10)/(x10*x12*x20) -((f.x1-f.x2)*x23- (f.x2-f.x3)*x12) /(x12*x23*x13)))/(-(x0-x3)) by XCMPLX_1:191 .= (((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13) -((f.x0-f.x1)*x12+(f .x1-f.x2)*x10)/(x10*x12*x20))/(x3-x0) .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13)/x30 -((f.x0-f.x1)*x12 +(f.x1-f.x2)*x10) /(x10*x12*x20)/x30 by XCMPLX_1:120 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13*x30) -((f.x0-f.x1)*x12 +(f.x1-f.x2)*x10) /(x10*x12*x20)/x30 by XCMPLX_1:78 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13*x30) -((f.x0-f.x1)*x12 +(f.x1-f.x2)*x10) /(x10*x12*x20*x30) by XCMPLX_1:78 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)*x20 /(x12*x23*x13*x30*x20)-((f.x0-f .x1)*x12+(f.x1-f.x2)*x10) /(x10*x12*x20*x30) by A6,XCMPLX_1:91 .= ((f.x1-f.x2)*x23*x20-(f.x2-f.x3)*x12*x20)*x10 /(x12*x20*x30*x23*x13* x10)-((f.x0-f.x1)*x12 +(f.x1-f.x2)*x10)/(x10*x12*x20*x30) by A5,XCMPLX_1:91 .= ((f.x1-f.x2)*x23*x20*x10-(f.x2-f.x3)*x12*x20*x10) /(x12*x20*x30*x23* x13*x10)-((f.x0-f.x1)*x12+(f.x1-f.x2)*x10) *(x23*x13)/((x12*x20*x30)*x10*(x23* x13)) by A2,A4,XCMPLX_1:6,91 .= (((f.x1-f.x2)*x23*x20*x10-(f.x2-f.x3)*x12*x20*x10) -((f.x0-f.x1)*x12* x23*x13+(f.x1-f.x2)*x10*x23*x13)) /(x12*x20*x30*x23*x13*x10) by XCMPLX_1:120 .= (-f.x0*x12*x23*x13+f.x1*x20*x23*x30-f.x2*x13*x10*x30 +f.x3*x12*x20* x10)/(x12*x20*x30*x23*x13*x10); A9: [!f,x3,x2,x1,x0!] = (((f.x3-f.x2)/(-(x2-x3))-(f.x2-f.x1)/(-(x1-x2))) /( -(x1-x3))-((f.x2-f.x1)/(-(x1-x2))-(f.x1-f.x0) /(x1-x0))/(x2-x0))/(x3-x0) .= ((-(f.x3-f.x2)/(x2-x3)-(f.x2-f.x1)/(-(x1-x2))) /(-(x1-x3))-((f.x2-f. x1)/(-(x1-x2))-(f.x1-f.x0) /(x1-x0))/(x2-x0))/(x3-x0) by XCMPLX_1:188 .= ((-(f.x3-f.x2)/(x2-x3)-(-(f.x2-f.x1)/(x1-x2))) /(-(x1-x3))-((f.x2-f. x1)/(-(x1-x2))-(f.x1-f.x0) /(x1-x0))/(x2-x0))/(x3-x0) by XCMPLX_1:188 .= ((-((f.x3-f.x2)/(x2-x3)-(f.x2-f.x1)/(x1-x2))) /(-(x1-x3))-((f.x2-f.x1 )/(-(x1-x2))-(f.x1-f.x0) /(x1-x0))/(x2-x0))/(x3-x0) .= (((f.x3-f.x2)/(x2-x3)-(f.x2-f.x1)/(x1-x2))/(x1-x3) -((f.x2-f.x1)/(-( x1-x2))-(f.x1-f.x0)/(x1-x0)) /(x2-x0))/(x3-x0) by XCMPLX_1:191 .= (((f.x3-f.x2)/(x2-x3)-(f.x2-f.x1)/(x1-x2))/(x1-x3) -(-(f.x2-f.x1)/(x1 -x2)-(f.x1-f.x0)/(x1-x0)) /(x2-x0))/(x3-x0) by XCMPLX_1:188 .= (((f.x3-f.x2)/x23-(f.x2-f.x1)/x12)/x13+ -((-((f.x1-f.x0)/x10+(f.x2-f. x1)/x12)))/x20)/x30 .= (((f.x3-f.x2)/x23-(f.x2-f.x1)/x12)/x13+((f.x1-f.x0)/x10 +(f.x2-f.x1)/ x12)/x20)/x30 by XCMPLX_1:190 .= (((f.x3-f.x2)*x12-(f.x2-f.x1)*x23)/(x23*x12)/x13 +((f.x1-f.x0)/x10+(f .x2-f.x1) /x12)/x20)/x30 by A2,A7,XCMPLX_1:130 .= (((f.x3-f.x2)*x12-(f.x2-f.x1)*x23)/(x23*x12)/x13 +((f.x1-f.x0)*x12+(f .x2-f.x1)*x10) /(x10*x12)/x20)/x30 by A7,A5,XCMPLX_1:116 .= (((f.x3-f.x2)*x12-(f.x2-f.x1)*x23)/(x23*x12*x13) +((f.x1-f.x0)*x12+(f .x2-f.x1)*x10) /(x10*x12)/x20)/x30 by XCMPLX_1:78 .= (((f.x3-f.x2)*x12-(f.x2-f.x1)*x23)/(x23*x12*x13) +((f.x1-f.x0)*x12+(f .x2-f.x1)*x10) /(x10*x12*x20))/x30 by XCMPLX_1:78 .= (((f.x3-f.x2)*x12-(f.x2-f.x1)*x23)/(x23*x12*x13) +((f.x1-f.x0)*x12+(f .x2-f.x1)*x10)*x13 /(x10*x12*x20*x13))/x30 by A4,XCMPLX_1:91 .= (((f.x3-f.x2)*x12-(f.x2-f.x1)*x23)/(x23*x12*x13) +((f.x1-f.x0)*x12* x13+(f.x2-f.x1)*x10*x13)*x23 /(x10*x12*x13*x20*x23))/x30 by A2,XCMPLX_1:91 .= (((f.x3-f.x2)*x12-(f.x2-f.x1)*x23)*x20/(x23*x12*x13*x20) +((f.x1-f.x0 )*x12*x13*x23+(f.x2-f.x1)*x10*x13*x23)/ (x10*x12*x13*x20*x23))/x30 by A6, XCMPLX_1:91 .= (((f.x3-f.x2)*x12*x20-(f.x2-f.x1)*x23*x20)*x10/(x12*x13*x20*x23*x10) +((f.x1-f.x0)*x12*x13*x23+(f.x2-f.x1)*x10*x13*x23)/ (x10*x12*x13*x20*x23))/x30 by A5,XCMPLX_1:91 .= ((f.x3-f.x2)*x12*x20*x10-(f.x2-f.x1)*x23*x20*x10) /(x10*x12*x13*x20* x23)/x30+((f.x1-f.x0)*x12*x13*x23 +(f.x2-f.x1)*x10*x13*x23)/(x10*x12*x13*x20* x23)/x30 by XCMPLX_1:62 .= ((f.x3-f.x2)*x12*x20*x10-(f.x2-f.x1)*x23*x20*x10) /(x10*x12*x13*x20* x23*x30)+((f.x1-f.x0)*x12*x13*x23 +(f.x2-f.x1)*x10*x13*x23)/(x10*x12*x13*x20* x23) /x30 by XCMPLX_1:78 .= ((f.x3-f.x2)*x12*x20*x10-(f.x2-f.x1)*x23*x20*x10) /(x10*x12*x13*x20* x23*x30)+((f.x1-f.x0)*x12*x13*x23 +(f.x2-f.x1)*x10*x13*x23)/ (x10*x12*x13*x20* x23*x30) by XCMPLX_1:78 .= ((f.x3-f.x2)*x12*x20*x10-(f.x2-f.x1)*x23*x20*x10 +((f.x1-f.x0)*x12* x13*x23+(f.x2-f.x1)*x10*x13*x23)) /(x10*x12*x13*x20*x23*x30) by XCMPLX_1:62 .= [!f,x0,x1,x2,x3!] by A8; [!f,x1,x2,x3,x0!] = (((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23)/x13 -(( f.x2-f.x3)/(x2-x3)-(f.x3-f.x0)/(x3-x0)) /(x2-x0))/(x1-x0) by A2,A7,XCMPLX_1:130 .= (((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23)/x13- ((f.x2-f.x3)*x30-(f .x3-f.x0)*x23) /(x23*x30)/x20)/x10 by A2,A3,XCMPLX_1:130 .= (((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13) -((f.x2-f.x3)*x30-(f .x3-f.x0)*x23) /(x23*x30)/x20)/x10 by XCMPLX_1:78 .= (((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13) -((f.x2-f.x3)*x30-(f .x3-f.x0)*x23) /(x23*x30*x20))/x10 by XCMPLX_1:78 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13) /x10-((f.x2-f.x3)*x30 -(f.x3-f.x0)*x23) /(x23*x30*x20)/x10 by XCMPLX_1:120 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13*x10) -((f.x2-f.x3)*x30 -(f.x3-f.x0)*x23) /(x23*x30*x20)/x10 by XCMPLX_1:78 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13*x10) -((f.x2-f.x3)*x30 -(f.x3-f.x0)*x23) /(x23*x30*x20*x10) by XCMPLX_1:78 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)*x30 /(x12*x23*x13*x10*x30)-((f.x2-f .x3)*x30 -(f.x3-f.x0)*x23)/(x23*x30*x20*x10) by A3,XCMPLX_1:91 .= ((f.x1-f.x2)*x23*x30-(f.x2-f.x3)*x12*x30)*x20 /(x12*x23*x13*x10*x30* x20)-((f.x2-f.x3)*x30 -(f.x3-f.x0)*x23)/(x23*x30*x20*x10) by A6,XCMPLX_1:91 .=((f.x1-f.x2)*x23*x30*x20-(f.x2-f.x3)*x12*x30*x20) /(x12*x23*x13*x10* x30*x20)-((f.x2-f.x3)*x30 -(f.x3-f.x0)*x23)*x13/ ((x10*x30*x20)*x23*x13) by A4, XCMPLX_1:91 .=((f.x1-f.x2)*x23*x30*x20 -(f.x2-f.x3)*x12*x30*x20)/(x12*x23*x13*x10* x30*x20) -((f.x2-f.x3)*x30*x13-(f.x3-f.x0)*x23*x13)*x12 /((x23*x13*x10*x30*x20) *x12) by A7,XCMPLX_1:91 .=(((f.x1-f.x2)*x23*x30*x20-(f.x2-f.x3)*x12*x30*x20)- ((f.x2-f.x3)*x30* x13*x12-(f.x3-f.x0)*x23*x13*x12)) /(x12*x23*x13*x10*x30*x20) by XCMPLX_1:120 .= [!f,x0,x1,x2,x3!] by A8; hence thesis by A9; end; theorem 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!] proof set x10 = x1-x0; set x20 = x2-x0; set x30 = x3-x0; set x12 = x1-x2; set x13 = x1-x3; set x23 = x2-x3; assume A1: x0,x1,x2,x3 are_mutually_distinct; then A2: x2-x3<>0 by ZFMISC_1:def 6; A3: x1-x3<>0 by A1,ZFMISC_1:def 6; A4: x1-x2<>0 by A1,ZFMISC_1:def 6; A5: x3-x0<>0 by A1,ZFMISC_1:def 6; A6: x2-x0<>0 by A1,ZFMISC_1:def 6; A7: x1-x0<>0 by A1,ZFMISC_1:def 6; A8: [!f,x0,x1,x2,x3!] = (((f.x0-f.x1)/(-(x1-x0))-(f.x1-f.x2)/(x1-x2)) /(-(x2 -x0))-((f.x1-f.x2)/(x1-x2)-(f.x2-f.x3) /(x2-x3))/(x1-x3))/(x0-x3) .= ((-(f.x0-f.x1)/(x1-x0)-(f.x1-f.x2)/(x1-x2)) /(-(x2-x0))-((f.x1-f.x2)/ (x1-x2)-(f.x2-f.x3) /(x2-x3))/(x1-x3))/(x0-x3) by XCMPLX_1:188 .= ((-((f.x0-f.x1)/(x1-x0)+(f.x1-f.x2)/(x1-x2))) /(-(x2-x0))-((f.x1-f.x2 )/(x1-x2)-(f.x2-f.x3) /(x2-x3))/(x1-x3))/(x0-x3) .= (((f.x0-f.x1)/(x1-x0)+(f.x1-f.x2)/(x1-x2))/(x2-x0) -((f.x1-f.x2)/(x1- x2)-(f.x2-f.x3) /(x2-x3))/(x1-x3))/(x0-x3) by XCMPLX_1:191 .= (((f.x0-f.x1)*x12+(f.x1-f.x2)*x10) /(x10*x12)/x20-((f.x1-f.x2)/(x1-x2 ) -(f.x2-f.x3)/(x2-x3))/(x1-x3))/(x0-x3) by A4,A7,XCMPLX_1:116 .= (((f.x0-f.x1)*x12+(f.x1-f.x2)*x10)/(x10*x12)/x20 -((f.x1-f.x2)*x23-(f .x2-f.x3)*x12) /(x12*x23)/x13)/(x0-x3) by A2,A4,XCMPLX_1:130 .= (((f.x0-f.x1)*x12+(f.x1-f.x2)*x10)/(x10*x12*x20) -((f.x1-f.x2)*x23-(f .x2-f.x3)*x12) /(x12*x23)/x13)/(x0-x3) by XCMPLX_1:78 .= (((f.x0-f.x1)*x12+(f.x1-f.x2)*x10)/(x10*x12*x20) -((f.x1-f.x2)*x23-(f .x2-f.x3)*x12) /(x12*x23*x13))/(x0-x3) by XCMPLX_1:78 .= (-(((f.x0-f.x1)*x12+(f.x1-f.x2)*x10)/(x10*x12*x20) -((f.x1-f.x2)*x23- (f.x2-f.x3)*x12) /(x12*x23*x13)))/(-(x0-x3)) by XCMPLX_1:191 .= (((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13) -((f.x0-f.x1)*x12+(f .x1-f.x2)*x10)/(x10*x12*x20))/(x3-x0) .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13)/x30 -((f.x0-f.x1)*x12 +(f.x1-f.x2)*x10) /(x10*x12*x20)/x30 by XCMPLX_1:120 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13*x30) -((f.x0-f.x1)*x12 +(f.x1-f.x2)*x10) /(x10*x12*x20)/x30 by XCMPLX_1:78 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)/(x12*x23*x13*x30) -((f.x0-f.x1)*x12 +(f.x1-f.x2)*x10) /(x10*x12*x20*x30) by XCMPLX_1:78 .= ((f.x1-f.x2)*x23-(f.x2-f.x3)*x12)*x20 /(x12*x23*x13*x30*x20)-((f.x0-f .x1)*x12+(f.x1-f.x2)*x10) /(x10*x12*x20*x30) by A6,XCMPLX_1:91 .= ((f.x1-f.x2)*x23*x20-(f.x2-f.x3)*x12*x20)*x10 /(x12*x20*x30*x23*x13* x10)-((f.x0-f.x1)*x12 +(f.x1-f.x2)*x10)/(x10*x12*x20*x30) by A7,XCMPLX_1:91 .= ((f.x1-f.x2)*x23*x20*x10-(f.x2-f.x3)*x12*x20*x10) /(x12*x20*x30*x23* x13*x10)-((f.x0-f.x1)*x12+(f.x1-f.x2)*x10) *(x23*x13)/((x12*x20*x30)*x10*(x23* x13)) by A2,A3,XCMPLX_1:6,91 .= (((f.x1-f.x2)*x23*x20*x10-(f.x2-f.x3)*x12*x20*x10) -((f.x0-f.x1)*x12* x23*x13+(f.x1-f.x2)*x10*x23*x13)) /(x12*x20*x30*x23*x13*x10) by XCMPLX_1:120 .= (-f.x0*x12*x23*x13+f.x1*x20*x23*x30-f.x2*x13*x10*x30 +f.x3*x12*x20* x10)/(x12*x20*x30*x23*x13*x10); A9: [!f,x1,x2,x0,x3!] = (((f.x1-f.x2)/(x1-x2)-(f.x2-f.x0)/(x2-x0)) /(x1-x0) -((f.x2-f.x0)/(x2-x0)-(f.x0-f.x3) /(-(x3-x0)))/(x2-x3))/(x1-x3) .= (((f.x1-f.x2)/(x1-x2)-(f.x2-f.x0)/(x2-x0)) /(x1-x0)-((f.x2-f.x0)/(x2- x0)--(f.x0-f.x3) /(x3-x0))/(x2-x3))/(x1-x3) by XCMPLX_1:188 .= (((f.x1-f.x2)*x20-(f.x2-f.x0)*x12)/(x12*x20) /x10-((f.x2-f.x0)/x20+(f .x0-f.x3) /x30)/x23)/x13 by A4,A6,XCMPLX_1:130 .= (((f.x1-f.x2)*x20-(f.x2-f.x0)*x12)/(x12*x20) /x10-((f.x2-f.x0)*x30+(f .x0-f.x3) *x20)/(x30*x20)/x23)/x13 by A5,A6,XCMPLX_1:116 .= (((f.x1-f.x2)*x20-(f.x2-f.x0)*x12)/(x12*x20*x10) -((f.x2-f.x0)*x30+(f .x0-f.x3) *x20)/(x30*x20)/x23)/x13 by XCMPLX_1:78 .= (((f.x1-f.x2)*x20-(f.x2-f.x0)*x12)/(x12*x20*x10) -((f.x2-f.x0)*x30+(f .x0-f.x3) *x20)/(x30*x20*x23))/x13 by XCMPLX_1:78 .= ((f.x1-f.x2)*x20-(f.x2-f.x0)*x12)/(x12*x20*x10) /x13-((f.x2-f.x0)*x30 +(f.x0-f.x3) *x20)/(x30*x20*x23)/x13 by XCMPLX_1:120 .= ((f.x1-f.x2)*x20-(f.x2-f.x0)*x12)/(x12*x20*x10 *x13)-((f.x2-f.x0)*x30 +(f.x0-f.x3) *x20)/(x30*x20*x23)/x13 by XCMPLX_1:78 .= ((f.x1-f.x2)*x20-(f.x2-f.x0)*x12)/(x12*x20*x10 *x13)-((f.x2-f.x0)*x30 +(f.x0-f.x3) *x20)/(x30*x20*x23*x13) by XCMPLX_1:78 .= ((f.x1-f.x2)*x20-(f.x2-f.x0)*x12)*x30/(x12*x20*x10 *x13*x30)-((f.x2-f .x0)*x30+(f.x0-f.x3) *x20)/(x30*x20*x23*x13) by A5,XCMPLX_1:91 .= ((f.x1-f.x2)*x20*x30-(f.x2-f.x0)*x12*x30)*x23 /(x12*x20*x10*x13*x30* x23)-((f.x2-f.x0)*x30 +(f.x0-f.x3)*x20)/(x30*x20*x23*x13) by A2,XCMPLX_1:91 .= ((f.x1-f.x2)*x20*x30*x23-(f.x2-f.x0)*x12*x30*x23) /(x12*x20*x10*x13* x30*x23)-((f.x2-f.x0)*x30+(f.x0-f.x3) *x20)*x12/(x30*x20*x23*x13*x12) by A4, XCMPLX_1:91 .= ((f.x1-f.x2)*x20*x30*x23-(f.x2-f.x0)*x12*x30*x23) /(x12*x20*x10*x13* x30*x23)-((f.x2-f.x0)*x30*x12+(f.x0-f.x3) *x20*x12)*x10/(x30*x20*x23*x13*x12* x10) by A7,XCMPLX_1:91 .= (((f.x1-f.x2)*x20*x30*x23-(f.x2-f.x0)*x12*x30*x23) -((f.x2-f.x0)*x30* x12*x10+(f.x0-f.x3)*x20*x12*x10)) /(x30*x20*x23*x13*x12*x10) by XCMPLX_1:120 .= [!f,x0,x1,x2,x3!] by A8; [!f,x1,x0,x2,x3!] = (((f.x1-f.x0)/(x1-x0)--(f.x0-f.x2)/(x2-x0)) /(x1-x2) -((f.x0-f.x2)/(-(x2-x0))-(f.x2-f.x3) /(x2-x3))/(x0-x3))/(x1-x3) by XCMPLX_1:188 .= (((f.x1-f.x0)/(x1-x0)+(f.x0-f.x2)/(x2-x0)) /(x1-x2)-(-(f.x0-f.x2)/(x2 -x0)-(f.x2-f.x3) /(x2-x3))/(-(x3-x0)))/(x1-x3) by XCMPLX_1:188 .= (((f.x1-f.x0)/(x1-x0)+(f.x0-f.x2)/(x2-x0)) /(x1-x2)- (-((f.x0-f.x2)/( x2-x0)+(f.x2-f.x3) /(x2-x3)))/(-(x3-x0)))/(x1-x3) .= (((f.x1-f.x0)/(x1-x0)+(f.x0-f.x2)/(x2-x0)) /(x1-x2)- ((f.x0-f.x2)/(x2 -x0)+(f.x2-f.x3) /(x2-x3))/(x3-x0))/(x1-x3) by XCMPLX_1:191 .= (((f.x1-f.x0)*x20+(f.x0-f.x2)*x10)/(x20*x10) /x12 - ((f.x0-f.x2)/x20+ (f.x2-f.x3) /x23)/x30)/x13 by A6,A7,XCMPLX_1:116 .= (((f.x1-f.x0)*x20+(f.x0-f.x2)*x10)/(x10*x20) /x12 - ((f.x0-f.x2)*x23+ (f.x2-f.x3) *x20)/(x23*x20)/x30)/x13 by A2,A6,XCMPLX_1:116 .= (((f.x1-f.x0)*x20+(f.x0-f.x2)*x10)/(x10*x20*x12) - ((f.x0-f.x2)*x23+( f.x2-f.x3) *x20)/(x23*x20)/x30)/x13 by XCMPLX_1:78 .= (((f.x1-f.x0)*x20+(f.x0-f.x2)*x10)/(x10*x20*x12) - ((f.x0-f.x2)*x23+( f.x2-f.x3)*x20) /(x23*x20*x30))/x13 by XCMPLX_1:78 .= ((f.x1-f.x0)*x20+(f.x0-f.x2)*x10)/(x10*x20*x12)/x13 - ((f.x0-f.x2)* x23+(f.x2-f.x3)*x20) /(x23*x20*x30)/x13 by XCMPLX_1:120 .= ((f.x1-f.x0)*x20+(f.x0-f.x2)*x10)/(x10*x20*x12*x13) - ((f.x0-f.x2)* x23+(f.x2-f.x3)*x20) /(x23*x20*x30)/x13 by XCMPLX_1:78 .= ((f.x1-f.x0)*x20+(f.x0-f.x2)*x10)/(x10*x20*x12*x13) - ((f.x0-f.x2)* x23+(f.x2-f.x3)*x20) /(x23*x20*x30*x13) by XCMPLX_1:78 .= ((f.x1-f.x0)*x20+(f.x0-f.x2)*x10)*x23 /(x10*x20*x12*x13*x23)- ((f.x0- f.x2)*x23 +(f.x2-f.x3)*x20)/(x23*x20*x30*x13) by A2,XCMPLX_1:91 .= ((f.x1-f.x0)*x20*x23+(f.x0-f.x2)*x10*x23)*x30 /(x10*x20*x12*x13*x23* x30)- ((f.x0-f.x2)*x23 +(f.x2-f.x3)*x20)/(x23*x20*x30*x13) by A5,XCMPLX_1:91 .= ((f.x1-f.x0)*x20*x23*x30+(f.x0-f.x2)*x10*x23*x30) /(x10*x20*x12*x13* x23*x30)- ((f.x0-f.x2)*x23 +(f.x2-f.x3)*x20)*x10/(x23*x20*x30*x13*x10) by A7, XCMPLX_1:91 .= ((f.x1-f.x0)*x20*x23*x30+(f.x0-f.x2)*x10*x23*x30) /(x10*x20*x12*x13* x23*x30) - ((f.x0-f.x2)*x23*x10 +(f.x2-f.x3)*x20*x10)*x12/ (x23*x20*x30*x13*x10 *x12) by A4,XCMPLX_1:91 .= (((f.x1-f.x0)*x20*x23*x30+(f.x0-f.x2)*x10*x23*x30) - ((f.x0-f.x2)*x23 *x10*x12+(f.x2-f.x3)*x20*x10*x12)) /(x23*x20*x30*x13*x10*x12) by XCMPLX_1:120 .= [!f,x0,x1,x2,x3!] by A8; hence thesis by A9; end; theorem f is constant implies [!f,x0,x1,x2!] = 0 proof assume A1: f is constant; then [!f,x0,x1,x2!] = (0 qua Nat-[!f,x1,x2!])/(x0-x2) by DIFF_1:30 .= (0 qua Nat-(0 qua Nat))/(x0-x2) by A1,DIFF_1:30; hence thesis; end; :: f.x=a*x+b theorem Th21: x0<>x1 implies [!AffineMap(a,b),x0,x1!] = a proof assume x0<>x1; then A1: x0-x1<>0; [!AffineMap(a,b),x0,x1!] = (a*x0+b-AffineMap(a,b).x1)/(x0-x1) by FCONT_1:def 4 .= (a*x0+b-(a*x1+b))/(x0-x1) by FCONT_1:def 4 .= a*(x0-x1)/(x0-x1); hence thesis by A1,XCMPLX_1:89; end; theorem Th22: x0,x1,x2 are_mutually_distinct implies [!AffineMap(a,b),x0,x1, x2!]=0 proof assume A1: x0,x1,x2 are_mutually_distinct; then A2: x1<>x2 by ZFMISC_1:def 5; x0<>x1 by A1,ZFMISC_1:def 5; then [!AffineMap(a,b),x0,x1,x2!] = (a-[!AffineMap(a,b),x1,x2!])/(x0-x2) by Th21 .= (a-a)/(x0-x2) by A2,Th21; hence thesis; end; theorem x0,x1,x2,x3 are_mutually_distinct implies [!AffineMap(a,b),x0,x1,x2, x3!]=0 proof assume A1: x0,x1,x2,x3 are_mutually_distinct; then A2: x1<>x2 by ZFMISC_1:def 6; x1<>x3 & x2<>x3 by A1,ZFMISC_1:def 6; then A3: x1,x2,x3 are_mutually_distinct by A2,ZFMISC_1:def 5; x0<>x1 & x0<>x2 by A1,ZFMISC_1:def 6; then x0,x1,x2 are_mutually_distinct by A2,ZFMISC_1:def 5; then [!AffineMap(a,b),x0,x1,x2,x3!] = (0 qua Nat-[!AffineMap(a,b),x1,x2,x3!]) /(x0-x3) by Th22 .= (0 qua Nat-(0 qua Nat))/(x0-x3) by A3,Th22; hence thesis; end; theorem for x holds fD(AffineMap(a,b),h).x = a*h proof let x; fD(AffineMap(a,b),h).x = AffineMap(a,b).(x+h)-AffineMap(a,b).x by DIFF_1:3 .= a*(x+h)+b-AffineMap(a,b).x by FCONT_1:def 4 .= a*x+a*h+b-(a*x+b) by FCONT_1:def 4; hence thesis; end; theorem for x holds bD(AffineMap(a,b),h).x = a*h proof let x; bD(AffineMap(a,b),h).x = AffineMap(a,b).x-AffineMap(a,b).(x-h) by DIFF_1:4 .= a*x+b-AffineMap(a,b).(x-h) by FCONT_1:def 4 .= a*x+b-(a*(x-h)+b) by FCONT_1:def 4; hence thesis; end; theorem for x holds cD(AffineMap(a,b),h).x = a*h proof let x; cD(AffineMap(a,b),h).x = AffineMap(a,b).(x+h/2) - AffineMap(a,b).(x-h/2) by DIFF_1:5 .= a*(x+h/2)+b - AffineMap(a,b).(x-h/2) by FCONT_1:def 4 .= a*(x+h/2)+b - (a*(x-h/2)+b) by FCONT_1:def 4; hence thesis; end; :: f.x=a*x^2+b*x+c theorem Th27: (for x holds f.x = a*x^2+b*x+c) & x0<>x1 implies [!f,x0,x1!]=a*( x0+x1)+b proof assume that A1: for x holds f.x = a*x^2+b*x+c and A2: x0<>x1; A3: x0-x1<>0 by A2; [!f,x0,x1!] = (a*x0^2+b*x0+c-f.x1)/(x0-x1) by A1 .= (a*x0^2+b*x0+c-(a*x1^2+b*x1+c))/(x0-x1) by A1 .= (a*(x0+x1)+b)*(x0-x1)/(x0-x1); hence thesis by A3,XCMPLX_1:89; end; theorem Th28: (for x holds f.x = a*x^2+b*x+c) & x0,x1,x2 are_mutually_distinct implies [!f,x0,x1,x2!]=a proof assume A1: for x holds f.x = a*x^2+b*x+c; assume A2: x0,x1,x2 are_mutually_distinct; then A3: x1<>x2 by ZFMISC_1:def 5; A4: x0-x2<>0 by A2,ZFMISC_1:def 5; x0<>x1 by A2,ZFMISC_1:def 5; then [!f,x0,x1,x2!] = (a*(x0+x1)+b-[!f,x1,x2!])/(x0-x2) by A1,Th27 .= (a*(x0+x1)+b-(a*(x1+x2)+b))/(x0-x2) by A1,A3,Th27 .= a*(x0-x2)/(x0-x2); hence thesis by A4,XCMPLX_1:89; end; theorem Th29: (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 proof assume A1: for x holds f.x = a*x^2+b*x+c; assume A2: x0,x1,x2,x3 are_mutually_distinct; then A3: x1<>x2 by ZFMISC_1:def 6; x1<>x3 & x2<>x3 by A2,ZFMISC_1:def 6; then A4: x1,x2,x3 are_mutually_distinct by A3,ZFMISC_1:def 5; x0<>x1 & x0<>x2 by A2,ZFMISC_1:def 6; then x0,x1,x2 are_mutually_distinct by A3,ZFMISC_1:def 5; then [!f,x0,x1,x2,x3!] = (a-[!f,x1,x2,x3!])/(x0-x3) by A1,Th28 .= (a-a)/(x0-x3) by A1,A4,Th28; hence thesis; end; theorem (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 proof assume A1: for x holds f.x = a*x^2+b*x+c; assume A2: x0,x1,x2,x3,x4 are_mutually_distinct; then A3: x1<>x2 & x1<>x3 by ZFMISC_1:def 7; A4: x0<>x3 by A2,ZFMISC_1:def 7; A5: x2<>x3 by A2,ZFMISC_1:def 7; A6: x3<>x4 by A2,ZFMISC_1:def 7; x1<>x4 & x2<>x4 by A2,ZFMISC_1:def 7; then A7: x1,x2,x3,x4 are_mutually_distinct by A3,A5,A6,ZFMISC_1:def 6; x0<>x1 & x0<>x2 by A2,ZFMISC_1:def 7; then x0,x1,x2,x3 are_mutually_distinct by A4,A3,A5,ZFMISC_1:def 6; then [!f,x0,x1,x2,x3,x4!] = (0 qua Nat- [!f,x1,x2,x3,x4!])/(x0-x4) by A1,Th29 .= (0 qua Nat-(0 qua Nat))/(x0-x4) by A1,A7,Th29; hence thesis; end; theorem (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 proof assume A1: for x holds f.x = a*x^2+b*x+c; let x; fD(f,h).x = f.(x+h)-f.x by DIFF_1:3 .= a*(x+h)^2+b*(x+h)+c-f.x by A1 .= a*(x+h)^2+b*(x+h)+c-(a*x^2+b*x+c) by A1 .= 2*a*h*x+a*h^2+b*h; hence thesis; end; theorem (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 proof assume A1: for x holds f.x = a*x^2+b*x+c; let x; bD(f,h).x = f.x-f.(x-h) by DIFF_1:4 .= a*x^2+b*x+c-f.(x-h) by A1 .= a*x^2+b*x+c-(a*(x-h)^2+b*(x-h)+c) by A1 .= 2*a*h*x-a*h^2+b*h; hence thesis; end; theorem (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 proof assume A1: for x holds f.x = a*x^2+b*x+c; let x; cD(f,h).x = f.(x+h/2) - f.(x-h/2) by DIFF_1:5 .= a*(x+h/2)^2+b*(x+h/2)+c - f.(x-h/2) by A1 .= a*(x+h/2)^2+b*(x+h/2)+c -(a*(x-h/2)^2+b*(x-h/2)+c) by A1 .= 2*a*h*x+b*h; hence thesis; end; :: f.x=k/x theorem Th34: (for x holds f.x = k/x) & x0<>x1 & x0<>0 & x1<>0 implies [!f,x0, x1!] = - k/(x0*x1) proof assume that A1: for x holds f.x = k/x and A2: x0<>x1 and A3: x0<>0 and A4: x1<>0; A5: x1-x0<>0 by A2; [!f,x0,x1!] = (k/x0-f.x1)/(x0-x1) by A1 .= (k/x0-k/x1)/(x0-x1) by A1 .= ((k*x1)/(x0*x1)-k/x1)/(x0-x1) by A4,XCMPLX_1:91 .= ((k*x1)/(x0*x1)-(k*x0)/(x0*x1))/(x0-x1) by A3,XCMPLX_1:91 .= ((k*x1-k*x0)/(x0*x1))/(x0-x1) by XCMPLX_1:120 .= ((k*(x1-x0))/(x0*x1))/(-(x1-x0)) .= -((k*(x1-x0))/(x0*x1))/(x1-x0) by XCMPLX_1:188 .= -k*(x1-x0)/(x1-x0)/(x0*x1) by XCMPLX_1:48; hence thesis by A5,XCMPLX_1:89; end; theorem Th35: (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) proof assume that A1: for x holds f.x = k/x and A2: x0<>0 and A3: x1<>0 and A4: x2<>0; assume A5: x0,x1,x2 are_mutually_distinct; then A6: x1<>x2 by ZFMISC_1:def 5; A7: x0-x2<>0 by A5,ZFMISC_1:def 5; x0<>x1 by A5,ZFMISC_1:def 5; then [!f,x0,x1,x2!] = (-k/(x0*x1)-[!f,x1,x2!])/(x0-x2) by A1,A2,A3,Th34 .= (-k/(x0*x1)- -k/(x1*x2))/(x0-x2) by A1,A3,A4,A6,Th34 .= (-k/(x0*x1)+k/(x1*x2))/(x0-x2) .= (-k*x2/(x0*x1*x2)+k/(x1*x2))/(x0-x2) by A4,XCMPLX_1:91 .= (-k*x2/(x0*x1*x2)+k*x0/(x0*(x1*x2))) /(x0-x2) by A2,XCMPLX_1:91 .= (-(k*x2/(x0*x1*x2)-k*x0/(x0*x1*x2)))/(x0-x2) .= (-(k*x2-k*x0)/(x0*x1*x2))/(x0-x2) by XCMPLX_1:120 .= (-k*(x2-x0))/(x0*x1*x2)/(x0-x2) by XCMPLX_1:187 .= k*(x0-x2)/((x0*x1*x2)*(x0-x2)) by XCMPLX_1:78; hence thesis by A7,XCMPLX_1:91; end; theorem Th36: (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) proof assume that A1: for x holds f.x = k/x and A2: x0<>0 and A3: x1<>0 & x2<>0 and A4: x3<>0; assume A5: x0,x1,x2,x3 are_mutually_distinct; then A6: x1<>x2 by ZFMISC_1:def 6; x1<>x3 & x2<>x3 by A5,ZFMISC_1:def 6; then A7: x1,x2,x3 are_mutually_distinct by A6,ZFMISC_1:def 5; A8: x0-x3<>0 by A5,ZFMISC_1:def 6; x0<>x1 & x0<>x2 by A5,ZFMISC_1:def 6; then x0,x1,x2 are_mutually_distinct by A6,ZFMISC_1:def 5; then [!f,x0,x1,x2,x3!] = (k/(x0*x1*x2)-[!f,x1,x2,x3!])/(x0-x3) by A1,A2,A3 ,Th35 .= (k/(x0*x1*x2)-k/(x1*x2*x3))/(x0-x3) by A1,A3,A4,A7,Th35 .= (k*x3/(x0*x1*x2*x3)-k/(x1*x2*x3)) /(x0-x3) by A4,XCMPLX_1:91 .= (k*x3/(x0*x1*x2*x3)-k*x0/(x0*(x1*x2*x3))) /(x0-x3) by A2,XCMPLX_1:91 .= ((k*x3-k*x0)/(x0*x1*x2*x3))/(x0-x3) by XCMPLX_1:120 .= (-k)*(x0-x3)/((x0*x1*x2*x3)*(x0-x3)) by XCMPLX_1:78 .= (-k)/(x0*x1*x2*x3) by A8,XCMPLX_1:91; hence thesis by XCMPLX_1:187; end; theorem (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) proof assume that A1: for x holds f.x = k/x and A2: x0<>0 and A3: x1<>0 & x2<>0 & x3<>0 and A4: x4<>0; assume A5: x0,x1,x2,x3,x4 are_mutually_distinct; then A6: x1<>x2 & x1<>x3 by ZFMISC_1:def 7; A7: x3<>x4 by A5,ZFMISC_1:def 7; A8: x2<>x3 by A5,ZFMISC_1:def 7; A9: x0-x4<>0 by A5,ZFMISC_1:def 7; A10: x0<>x3 by A5,ZFMISC_1:def 7; x1<>x4 & x2<>x4 by A5,ZFMISC_1:def 7; then A11: x1,x2,x3,x4 are_mutually_distinct by A6,A8,A7,ZFMISC_1:def 6; x0<>x1 & x0<>x2 by A5,ZFMISC_1:def 7; then x0,x1,x2,x3 are_mutually_distinct by A10,A6,A8,ZFMISC_1:def 6; then [!f,x0,x1,x2,x3,x4!] = (-k/(x0*x1*x2*x3) - [!f,x1,x2,x3,x4!])/(x0-x4) by A1,A2,A3,Th36 .= (-k/(x0*x1*x2*x3) - -k/(x1*x2*x3*x4)) /(x0-x4) by A1,A3,A4,A11,Th36 .= (-k/(x0*x1*x2*x3) + k/(x1*x2*x3*x4))/(x0-x4) .= (-k*x4/(x0*x1*x2*x3*x4) + k/(x1*x2*x3*x4))/(x0-x4) by A4,XCMPLX_1:91 .= (-k*x4/(x0*x1*x2*x3*x4)+k*x0/(x0*(x1*x2*x3*x4))) /(x0-x4) by A2, XCMPLX_1:91 .= (k*x0/(x0*x1*x2*x3*x4)-k*x4/(x0*x1*x2*x3*x4))/(x0-x4) .= ((k*x0-k*x4)/(x0*x1*x2*x3*x4))/(x0-x4) by XCMPLX_1:120 .= k*(x0-x4)/((x0*x1*x2*x3*x4)*(x0-x4)) by XCMPLX_1:78; hence thesis by A9,XCMPLX_1:91; end; theorem (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 (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 (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)) proof assume A1: for x holds f.x = k/x & x+h/2<>0 & x-h/2<>0; let x; A2: x+h/2<>0 by A1; A3: x-h/2<>0 by A1; cD(f,h).x = f.(x+h/2) - f.(x-h/2) by DIFF_1:5 .= k/(x+h/2)- f.(x-h/2) by A1 .= k/(x+h/2)-k/(x-h/2) by A1 .= k*(x-h/2)/((x-h/2)*(x+h/2))-k/(x-h/2) by A3,XCMPLX_1:91 .= k*(x-h/2)/((x-h/2)*(x+h/2))-k*(x+h/2) /((x-h/2)*(x+h/2)) by A2, XCMPLX_1:91 .= (k*x-k*(h/2)-k*(x+h/2))/((x-h/2)*(x+h/2)) by XCMPLX_1:120; hence thesis; end; :: f.x = sin(x) theorem [!sin,x0,x1!] = 2*cos((x0+x1)/2)*sin((x0-x1)/2)/(x0-x1) proof [!sin,x0,x1!] = (sin(x0)-sin(x1))/(x0-x1) .= 2*(cos((x0+x1)/2)*sin((x0-x1)/2))/(x0-x1) by SIN_COS4:16; hence thesis; end; theorem for x holds fD(sin,h).x = 2*(cos((2*x+h)/2)*sin(h/2)) proof let x; fD(sin,h).x = sin(x+h)-sin(x) by DIFF_1:3 .= 2*(cos((x+(h+x))/2)*sin((x+h-x)/2)) by SIN_COS4:16; hence thesis; end; theorem for x holds bD(sin,h).x = 2*(cos((2*x-h)/2)*sin(h/2)) proof let x; bD(sin,h).x = sin(x)-sin(x-h) by DIFF_1:4 .= 2*(cos((x+(x-h))/2)*sin((x-(x-h))/2)) by SIN_COS4:16; hence thesis; end; theorem for x holds cD(sin,h).x = 2*(cos(x)*sin(h/2)) proof let x; cD(sin,h).x = sin(x+h/2)-sin(x-h/2) by DIFF_1:5 .= 2*(cos((x+h/2+(x-h/2))/2) *sin((x+h/2-(x-h/2))/2)) by SIN_COS4:16; hence thesis; end; :: f.x = cos(x) theorem [!cos,x0,x1!] = -2*sin((x0+x1)/2)*sin((x0-x1)/2)/(x0-x1) proof [!cos,x0,x1!] = (cos(x0)-cos(x1))/(x0-x1) .= (-2*(sin((x0+x1)/2)*sin((x0-x1)/2))) /(x0-x1) by SIN_COS4:18; hence thesis by XCMPLX_1:187; end; theorem for x holds fD(cos,h).x = -2*(sin((2*x+h)/2)*sin(h/2)) proof let x; fD(cos,h).x = cos(x+h)-cos(x) by DIFF_1:3 .= -2*(sin((x+(x+h))/2)*sin((x+h-x)/2)) by SIN_COS4:18; hence thesis; end; theorem for x holds bD(cos,h).x = -2*(sin((2*x-h)/2)*sin(h/2)) proof let x; bD(cos,h).x = cos(x)-cos(x-h) by DIFF_1:4 .= -2*(sin((x+(x-h))/2)*sin((x-(x-h))/2)) by SIN_COS4:18; hence thesis; end; theorem for x holds cD(cos,h).x = -2*(sin(x)*sin(h/2)) proof let x; cD(cos,h).x = cos(x+h/2)-cos(x-h/2) by DIFF_1:5 .= -2*(sin((x+h/2+(x-h/2))/2) *sin((x+h/2-(x-h/2))/2)) by SIN_COS4:18; hence thesis; end; :: f.x = (sin x)^2 theorem [!sin(#)sin,x0,x1!] = (1/2)*(cos(2*x1)-cos(2*x0))/(x0-x1) proof [!sin(#)sin,x0,x1!] = ((sin.x0)*(sin.x0)-(sin(#)sin).x1) /(x0-x1) by VALUED_1:5 .= (sin(x0)*sin(x0)-sin(x1)*sin(x1))/(x0-x1) by VALUED_1:5 .= (-(1/2)*(cos(x0+x0)-cos(x0-x0)) -sin(x1)*sin(x1))/(x0-x1) by SIN_COS4:29 .= (-(1/2)*(cos(x0+x0)-cos(x0-x0))- -(1/2)*(cos(x1+x1)-cos(x1-x1)))/(x0- x1) by SIN_COS4:29 .= (1/2)*(cos(2*x1)-cos(2*x0))/(x0-x1); hence thesis; end; theorem for x holds fD(sin(#)sin,h).x = (1/2)*(cos(2*x)-cos(2*(x+h))) proof let x; fD(sin(#)sin,h).x = (sin(#)sin).(x+h)-(sin(#)sin).x by DIFF_1:3 .= (sin.(x+h))*(sin.(x+h))-(sin(#)sin).x by VALUED_1:5 .= sin(x+h)*sin(x+h)-sin(x)*sin(x) by VALUED_1:5 .= -(1/2)*(cos((x+h)+(x+h))-cos((x+h)-(x+h))) -sin(x)*sin(x) by SIN_COS4:29 .= -(1/2)*(cos(2*(x+h))-cos(0)) -(-(1/2)*(cos(x+x)-cos(x-x))) by SIN_COS4:29; hence thesis; end; theorem for x holds bD(sin(#)sin,h).x = (1/2)*(cos(2*(x-h))-cos(2*x)) proof let x; bD(sin(#)sin,h).x = (sin(#)sin).x-(sin(#)sin).(x-h) by DIFF_1:4 .= (sin.x)*(sin.x)-(sin(#)sin).(x-h) by VALUED_1:5 .= sin(x)*sin(x)-sin(x-h)*sin(x-h) by VALUED_1:5 .= -(1/2)*(cos(x+x)-cos(x-x))-sin(x-h)*sin(x-h) by SIN_COS4:29 .= -(1/2)*(cos(2*x)-cos(0))-(-(1/2) *(cos((x-h)+(x-h))-cos((x-h)-(x-h))) ) by SIN_COS4:29; hence thesis; end; theorem for x holds cD(sin(#)sin,h).x = (1/2)*(cos(2*x-h)-cos(2*x+h)) proof let x; cD(sin(#)sin,h).x = (sin(#)sin).(x+h/2) - (sin(#)sin).(x-h/2) by DIFF_1:5 .= (sin.(x+h/2))*(sin.(x+h/2)) -(sin(#)sin).(x-h/2) by VALUED_1:5 .= sin(x+h/2)*sin(x+h/2) -sin(x-h/2)*sin(x-h/2) by VALUED_1:5 .= -(1/2)*(cos((x+h/2)+(x+h/2))-cos((x+h/2)-(x+h/2))) -sin(x-h/2)*sin(x- h/2) by SIN_COS4:29 .= -(1/2)*(cos(2*(x+h/2))-cos(0)) -(-(1/2)*(cos((x-h/2)+(x-h/2)) -cos((x -h/2)-(x-h/2)))) by SIN_COS4:29; hence thesis; end; :: f.x = sin(x)*cos(x) theorem [!sin(#)cos,x0,x1!] = (1/2)*(sin(2*x0)-sin(2*x1))/(x0-x1) proof [!sin(#)cos,x0,x1!] = ((sin.x0)*(cos.x0)-(sin(#)cos).x1) /(x0-x1) by VALUED_1:5 .= (sin(x0)*cos(x0)-sin(x1)*cos(x1))/(x0-x1) by VALUED_1:5 .= ((1/2)*(sin(x0+x0)+sin(x0-x0)) -sin(x1)*cos(x1))/(x0-x1) by SIN_COS4:30 .= ((1/2)*(sin(x0+x0)+sin(x0-x0)) -(1/2)*(sin(x1+x1)+sin(x1-x1)))/(x0-x1 ) by SIN_COS4:30 .= (1/2)*(sin(2*x0)-sin(2*x1))/(x0-x1); hence thesis; end; theorem for x holds fD(sin(#)cos,h).x = (1/2)*(sin(2*(x+h))-sin(2*x)) proof let x; fD(sin(#)cos,h).x = (sin(#)cos).(x+h)-(sin(#)cos).x by DIFF_1:3 .= (sin.(x+h))*(cos.(x+h))-(sin(#)cos).x by VALUED_1:5 .= sin(x+h)*cos(x+h)-sin(x)*cos(x) by VALUED_1:5 .= (1/2)*(sin((x+h)+(x+h))+sin((x+h)-(x+h))) -sin(x)*cos(x) by SIN_COS4:30 .= (1/2)*(sin(2*(x+h))+sin(0)) -(1/2)*(sin(x+x)+sin(x-x)) by SIN_COS4:30 .= (1/2)*sin(2*(x+h))-(1/2)*sin(2*x); hence thesis; end; theorem for x holds bD(sin(#)cos,h).x = (1/2)*(sin(2*x)-sin(2*(x-h))) proof let x; bD(sin(#)cos,h).x = (sin(#)cos).x-(sin(#)cos).(x-h) by DIFF_1:4 .= (sin.x)*(cos.x)-(sin(#)cos).(x-h) by VALUED_1:5 .= sin(x)*cos(x)-sin(x-h)*cos(x-h) by VALUED_1:5 .= (1/2)*(sin(x+x)+sin(x-x))-sin(x-h)*cos(x-h) by SIN_COS4:30 .= (1/2)*(sin(x+x)+sin(0)) -(1/2)*(sin((x-h)+(x-h))+sin((x-h)-(x-h))) by SIN_COS4:30 .= (1/2)*sin(2*x)-(1/2)*sin(2*(x-h)); hence thesis; end; theorem for x holds cD(sin(#)cos,h).x = (1/2)*(sin(2*x+h)-sin(2*x-h)) proof let x; cD(sin(#)cos,h).x = (sin(#)cos).(x+h/2) - (sin(#)cos).(x-h/2) by DIFF_1:5 .= (sin.(x+h/2))*(cos.(x+h/2)) -(sin(#)cos).(x-h/2) by VALUED_1:5 .= sin(x+h/2)*cos(x+h/2) -sin(x-h/2)*cos(x-h/2) by VALUED_1:5 .= (1/2)*(sin((x+h/2)+(x+h/2))+sin((x+h/2)-(x+h/2))) -sin(x-h/2)*cos(x-h /2) by SIN_COS4:30 .= (1/2)*(sin((x+h/2)+(x+h/2))+sin((x+h/2)-(x+h/2))) -(1/2)*(sin((x-h/2) +(x-h/2)) +sin((x-h/2)-(x-h/2))) by SIN_COS4:30 .= (1/2)*sin(2*(x+h/2))-(1/2)*sin(2*(x-h/2)); hence thesis; end; :: f.x = (cos(x))^2 theorem [!cos(#)cos,x0,x1!] = (1/2)*(cos(2*x0)-cos(2*x1))/(x0-x1) proof [!cos(#)cos,x0,x1!] = ((cos.x0)*(cos.x0) -(cos(#)cos).x1)/(x0-x1) by VALUED_1:5 .= (cos(x0)*cos(x0) -cos(x1)*cos(x1))/(x0-x1) by VALUED_1:5 .= ((1/2)*(cos(x0+x0)+cos(x0-x0)) -cos(x1)*cos(x1))/(x0-x1) by SIN_COS4:32 .= ((1/2)*(cos(x0+x0)+cos(x0-x0)) -(1/2)*(cos(x1+x1)+cos(x1-x1)))/(x0-x1 ) by SIN_COS4:32 .= ((1/2)*cos(2*x0)-(1/2)*cos(2*x1))/(x0-x1); hence thesis; end; theorem for x holds fD(cos(#)cos,h).x = (1/2)*(cos(2*(x+h))-cos(2*x)) proof let x; fD(cos(#)cos,h).x = (cos(#)cos).(x+h) -(cos(#)cos).x by DIFF_1:3 .= (cos.(x+h))*(cos.(x+h))-(cos(#)cos).x by VALUED_1:5 .= cos(x+h)*cos(x+h)-cos(x)*cos(x) by VALUED_1:5 .= (1/2)*(cos((x+h)+(x+h))+cos((x+h)-(x+h))) -cos(x)*cos(x) by SIN_COS4:32 .= (1/2)*(cos(2*(x+h))+cos(0)) -(1/2)*(cos(x+x)+cos(x-x)) by SIN_COS4:32 .= (1/2)*cos(2*(x+h))-(1/2)*cos(2*x); hence thesis; end; theorem for x holds bD(cos(#)cos,h).x = (1/2)*(cos(2*x)-cos(2*(x-h))) proof let x; bD(cos(#)cos,h).x = (cos(#)cos).x -(cos(#)cos).(x-h) by DIFF_1:4 .= (cos.x)*(cos.x)-(cos(#)cos).(x-h) by VALUED_1:5 .= cos(x)*cos(x) -cos(x-h)*cos(x-h) by VALUED_1:5 .= (1/2)*(cos(x+x)+cos(x-x))-cos(x-h)*cos(x-h) by SIN_COS4:32 .= (1/2)*(cos(x+x)+cos(x-x)) -(1/2)*(cos((x-h)+(x-h))+cos((x-h)-(x-h))) by SIN_COS4:32 .= (1/2)*cos(2*x)-(1/2)*cos(2*(x-h)); hence thesis; end; theorem for x holds cD(cos(#)cos,h).x = (1/2)*(cos(2*x+h)-cos(2*x-h)) proof let x; cD(cos(#)cos,h).x = (cos(#)cos).(x+h/2) - (cos(#)cos).(x-h/2) by DIFF_1:5 .= (cos.(x+h/2))*(cos.(x+h/2)) -(cos(#)cos).(x-h/2) by VALUED_1:5 .= cos(x+h/2)*cos(x+h/2) -cos(x-h/2)*cos(x-h/2) by VALUED_1:5 .= (1/2)*(cos((x+h/2)+(x+h/2))+cos((x+h/2)-(x+h/2))) -cos(x-h/2)*cos(x-h /2) by SIN_COS4:32 .= (1/2)*(cos((x+h/2)+(x+h/2))+cos((x+h/2)-(x+h/2))) -(1/2)*(cos((x-h/2) +(x-h/2)) +cos((x-h/2)-(x-h/2))) by SIN_COS4:32 .= (1/2)*cos(2*(x+h/2))-(1/2)*cos(2*(x-h/2)); hence thesis; end; :: f.x = (sin(x))^2*cos(x) theorem [!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) proof set y = 3*x0; set z = 3*x1; [!sin(#)sin(#)cos,x0,x1!] = (((sin(#)sin).x0)*(cos.x0) -(sin(#)sin(#)cos ).x1)/(x0-x1) by VALUED_1:5 .= ((sin.x0)*(sin.x0)*(cos.x0) -(sin(#)sin(#)cos).x1)/(x0-x1) by VALUED_1:5 .= ((sin.x0)*(sin.x0)*(cos.x0) -((sin(#)sin).x1)*(cos.x1))/(x0-x1) by VALUED_1:5 .= (sin(x0)*sin(x0)*cos(x0) -sin(x1)*sin(x1)*cos(x1))/(x0-x1) by VALUED_1:5 .= ((1/4)*(-cos(x0+x0-x0)+cos(x0+x0-x0) +cos(x0+x0-x0)-cos(x0+x0+x0)) - sin(x1)*sin(x1)*cos(x1))/(x0-x1) by SIN_COS4:34 .= ((1/4)*(cos(x0)-cos(3*x0))-(1/4) *(-cos(x1+x1-x1)+cos(x1+x1-x1)+cos( x1+x1-x1) -cos(x1+x1+x1)))/(x0-x1) by SIN_COS4:34 .= ((1/4)*(cos(x0)-cos(x1))+(1/4)*(cos(z)-cos(y)))/(x0-x1) .= ((1/4)*(-2*(sin((x0+x1)/2)*sin((x0-x1)/2))) +(1/4)*(cos(z)-cos(y)))/( x0-x1) by SIN_COS4:18 .= ((1/4)*(-2*(sin((x0+x1)/2)*sin((x0-x1)/2)))+(1/4) *(-2*(sin((z+y)/2)* sin((z-y)/2))))/(x0-x1) by SIN_COS4:18 .= (-(1/2)*(sin(3*(x1+x0)/2)*sin(3*(x1-x0)/2) +sin((x0+x1)/2)*sin((x0-x1 )/2)))/(x0-x1); hence thesis by XCMPLX_1:187; end; theorem 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)) proof let x; set y=3*x; set z=3*h; fD(sin(#)sin(#)cos,h).x = (sin(#)sin(#)cos).(x+h) -(sin(#)sin(#)cos).x by DIFF_1:3 .= ((sin(#)sin).(x+h))*(cos.(x+h)) -(sin(#)sin(#)cos).x by VALUED_1:5 .= (sin.(x+h))*(sin.(x+h))*(cos.(x+h)) -(sin(#)sin(#)cos).x by VALUED_1:5 .= (sin.(x+h))*(sin.(x+h))*(cos.(x+h)) -((sin(#)sin).x)*(cos.x) by VALUED_1:5 .= sin(x+h)*sin(x+h)*cos(x+h) -sin(x)*sin(x)*cos(x) by VALUED_1:5 .= (1/4)*(-cos((x+h)+(x+h)-(x+h))+cos((x+h)+(x+h)-(x+h)) +cos((x+h)+(x+h )-(x+h))-cos((x+h)+(x+h)+(x+h))) -sin(x)*sin(x)*cos(x) by SIN_COS4:34 .= (1/4)*(cos(x+h)-cos(3*(x+h)))-(1/4)*(-cos(x+x-x) +cos(x+x-x)+cos(x+x- x)-cos(x+x+x)) by SIN_COS4:34 .= (1/4)*(cos(x+h)-cos(x))-(1/4)*(cos(3*(x+h))-cos(3*x)) .= (1/4)*(-2*(sin((x+h+x)/2)*sin((x+h-x)/2))) -(1/4)*(cos(3*(x+h))-cos(3 *x)) by SIN_COS4:18 .= (1/4)*(-2*(sin((2*x+h)/2)*sin(h/2))) -(1/4)*(-2*(sin((y+z+y)/2)*sin(( y+z-y)/2))) by SIN_COS4:18 .= (1/2)*(sin((6*x+3*h)/2)*sin(3*h/2)) -(1/2)*((sin((2*x+h)/2)*sin(h/2)) ); hence thesis; end; theorem 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)) proof let x; set y=3*x; set z=3*h; bD(sin(#)sin(#)cos,h).x = (sin(#)sin(#)cos).x -(sin(#)sin(#)cos).(x-h) by DIFF_1:4 .= ((sin(#)sin).x)*(cos.x) -(sin(#)sin(#)cos).(x-h) by VALUED_1:5 .= (sin.x)*(sin.x)*(cos.x) -(sin(#)sin(#)cos).(x-h) by VALUED_1:5 .= (sin.x)*(sin.x)*(cos.x) -((sin(#)sin).(x-h))*(cos.(x-h)) by VALUED_1:5 .= sin(x)*sin(x)*cos(x) -sin(x-h)*sin(x-h)*cos(x-h) by VALUED_1:5 .= (1/4)*(-cos(x+x-x)+cos(x+x-x)+cos(x+x-x)-cos(x+x+x)) -sin(x-h)*sin(x- h)*cos(x-h) by SIN_COS4:34 .= (1/4)*(cos(x)-cos(3*x))-(1/4)*(-cos((x-h)+(x-h)-(x-h)) +cos((x-h)+(x- h)-(x-h))+cos((x-h)+(x-h)-(x-h)) -cos((x-h)+(x-h)+(x-h))) by SIN_COS4:34 .= (1/4)*(cos(x)-cos(x-h))-(1/4)*(cos(3*x)-cos(3*(x-h))) .= (1/4)*(-2*(sin((x+(x-h))/2)*sin((x-(x-h))/2))) -(1/4)*(cos(3*x)-cos(3 *(x-h))) by SIN_COS4:18 .= (1/4)*(-2*(sin((2*x-h)/2)*sin(h/2))) -(1/4)*(-2*(sin((y+(y-z))/2)* sin((y-(y-z))/2))) by SIN_COS4:18 .= (1/2)*(sin((6*x-3*h)/2)*sin(3*h/2)) -(1/2)*(sin((2*x-h)/2)*sin(h/2)); hence thesis; end; theorem 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)) proof let x; set y=3*x; set z=3*h; cD(sin(#)sin(#)cos,h).x = (sin(#)sin(#)cos).(x+h/2) - (sin(#)sin(#)cos). (x-h/2) by DIFF_1:5 .= ((sin(#)sin).(x+h/2))*(cos.(x+h/2)) -(sin(#)sin(#)cos).(x-h/2) by VALUED_1:5 .= (sin.(x+h/2))*(sin.(x+h/2))*(cos.(x+h/2)) -(sin(#)sin(#)cos).(x-h/2) by VALUED_1:5 .= (sin.(x+h/2))*(sin.(x+h/2))*(cos.(x+h/2)) -((sin(#)sin).(x-h/2))*(cos .(x-h/2)) by VALUED_1:5 .= sin(x+h/2)*sin(x+h/2)*cos(x+h/2) -sin(x-h/2)*sin(x-h/2)*cos(x-h/2) by VALUED_1:5 .= (1/4)*(-cos((x+h/2)+(x+h/2)-(x+h/2))+cos((x+h/2)+(x+h/2)-(x+h/2)) + cos((x+h/2)+(x+h/2)-(x+h/2))-cos((x+h/2)+(x+h/2)+(x+h/2))) -sin(x-h/2)*sin(x-h/ 2)*cos(x-h/2) by SIN_COS4:34 .= (1/4)*(cos(x+h/2)-cos(3*(x+h/2))) -(1/4)*(-cos((x-h/2)+(x-h/2)-(x-h/2 ))+cos((x-h/2)+(x-h/2) -(x-h/2))+cos((x-h/2)+(x-h/2)-(x-h/2)) -cos((x-h/2)+(x-h /2)+(x-h/2))) by SIN_COS4:34 .= (1/4)*(cos(x+h/2)-cos(x-h/2))-(1/4)*(cos(3*(x+h/2))-cos(3*(x-h/2))) .= (1/4)*(-2*(sin(((x+h/2)+(x-h/2))/2)*sin(((x+h/2)-(x-h/2))/2))) -(1/4) *(cos(3*(x+h/2))-cos(3*(x-h/2))) by SIN_COS4:18 .= (1/4)*(-2*(sin(x)*sin(h/2))) -(1/4)*(-2*(sin(((y+z/2)+(y-z/2))/2) * sin(((y+z/2)-(y-z/2))/2))) by SIN_COS4:18 .= -(1/2)*(sin(x)*sin(h/2))+(1/2)*(sin(3*x)*sin(3*h/2)); hence thesis; end; :: f.x = sin(x)*(cos(x))^2 theorem [!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) proof set y = 3*x0; set z = 3*x1; [!sin(#)cos(#)cos,x0,x1!] = (((sin(#)cos).x0)*(cos.x0) -(sin(#)cos(#)cos ).x1)/(x0-x1) by VALUED_1:5 .= ((sin.x0)*(cos.x0)*(cos.x0) -(sin(#)cos(#)cos).x1)/(x0-x1) by VALUED_1:5 .= ((sin.x0)*(cos.x0)*(cos.x0) -((sin(#)cos).x1)*(cos.x1))/(x0-x1) by VALUED_1:5 .= (sin(x0)*cos(x0)*cos(x0) -sin(x1)*cos(x1)*cos(x1))/(x0-x1) by VALUED_1:5 .= ((1/4)*(sin(x0+x0-x0)-sin(x0+x0-x0)+sin(x0+x0-x0) +sin(x0+x0+x0))-sin (x1)*cos(x1)*cos(x1))/(x0-x1) by SIN_COS4:35 .= ((1/4)*(sin(x0)+sin(3*x0)) -(1/4)*(sin(x1+x1-x1)-sin(x1+x1-x1) +sin( x1+x1-x1)+sin(x1+x1+x1)))/(x0-x1) by SIN_COS4:35 .= ((1/4)*(sin(x0)-sin(x1))+(1/4)*(sin(3*x0)-sin(3*x1)))/(x0-x1) .= ((1/4)*(2*(cos((x0+x1)/2)*sin((x0-x1)/2))) +(1/4)*(sin(y)-sin(z)))/( x0-x1) by SIN_COS4:16 .= ((1/2)*(cos((x0+x1)/2)*sin((x0-x1)/2))+(1/4) *(2*(cos((y+z)/2)*sin((y -z)/2))))/(x0-x1) by SIN_COS4:16 .= (1/2)*(cos((x0+x1)/2)*sin((x0-x1)/2) +cos(3*(x0+x1)/2)*sin(3*(x0-x1)/ 2))/(x0-x1); hence thesis; end; theorem 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)) proof let x; set y=3*x; set z=3*h; fD(sin(#)cos(#)cos,h).x = (sin(#)cos(#)cos).(x+h) -(sin(#)cos(#)cos).x by DIFF_1:3 .= ((sin(#)cos).(x+h))*(cos.(x+h)) -(sin(#)cos(#)cos).x by VALUED_1:5 .= (sin.(x+h))*(cos.(x+h))*(cos.(x+h)) -(sin(#)cos(#)cos).x by VALUED_1:5 .= (sin.(x+h))*(cos.(x+h))*(cos.(x+h)) -((sin(#)cos).x)*(cos.x) by VALUED_1:5 .= sin(x+h)*cos(x+h)*cos(x+h) -sin(x)*cos(x)*cos(x) by VALUED_1:5 .= (1/4)*(sin((x+h)+(x+h)-(x+h)) -sin((x+h)+(x+h)-(x+h))+sin((x+h)+(x+h) -(x+h)) +sin((x+h)+(x+h)+(x+h)))-sin(x)*cos(x)*cos(x) by SIN_COS4:35 .= (1/4)*(sin(x+h)+sin(3*(x+h)))-(1/4) *(sin(x+x-x)-sin(x+x-x)+sin(x+x-x )+sin(x+x+x)) by SIN_COS4:35 .= (1/4)*(sin(x+h)-sin(x))+(1/4)*(sin(3*(x+h))-sin(3*x)) .= (1/4)*(2*(cos((x+h+x)/2)*sin((x+h-x)/2))) +(1/4)*(sin(3*(x+h))-sin(3* x)) by SIN_COS4:16 .= (1/4)*(2*(cos((2*x+h)/2)*sin(h/2))) +(1/4)*(2*(cos((y+z+y)/2)*sin((y+ z-y)/2))) by SIN_COS4:16 .= (1/2)*(cos((2*x+h)/2)*sin(h/2)) +(1/2)*(cos((6*x+3*h)/2)*sin(3*h/2)); hence thesis; end; theorem 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)) proof let x; set y=3*x; set z=3*h; bD(sin(#)cos(#)cos,h).x = (sin(#)cos(#)cos).x -(sin(#)cos(#)cos).(x-h) by DIFF_1:4 .= ((sin(#)cos).x)*(cos.x) -(sin(#)cos(#)cos).(x-h) by VALUED_1:5 .= (sin.x)*(cos.x)*(cos.x) -(sin(#)cos(#)cos).(x-h) by VALUED_1:5 .= (sin.x)*(cos.x)*(cos.x) -((sin(#)cos).(x-h))*(cos.(x-h)) by VALUED_1:5 .= sin(x)*cos(x)*cos(x) -sin(x-h)*cos(x-h)*cos(x-h) by VALUED_1:5 .= (1/4)*(sin(x+x-x)-sin(x+x-x)+sin(x+x-x)+sin(x+x+x)) -sin(x-h)*cos(x-h )*cos(x-h) by SIN_COS4:35 .= (1/4)*(sin(x)+sin(3*x))-(1/4)*(sin((x-h)+(x-h)-(x-h)) -sin((x-h)+(x-h )-(x-h))+sin((x-h)+(x-h)-(x-h)) +sin((x-h)+(x-h)+(x-h))) by SIN_COS4:35 .= (1/4)*(sin(x)-sin(x-h))+(1/4)*(sin(3*x)-sin(3*(x-h))) .= (1/4)*(2*(cos((x+(x-h))/2)*sin((x-(x-h))/2))) +(1/4)*(sin(3*x)-sin(3* (x-h))) by SIN_COS4:16 .= (1/4)*(2*(cos((2*x-h)/2)*sin(h/2)))+(1/4) *(2*(cos((y+(y-z))/2)*sin(( y-(y-z))/2))) by SIN_COS4:16 .= (1/2)*(cos((2*x-h)/2)*sin(h/2)) +(1/2)*((cos((6*x-3*h)/2)*sin(3*h/2)) ); hence thesis; end; theorem for x holds cD(sin(#)cos(#)cos,h).x = (1/2)*(cos(x)*sin(h/2)+cos(3*x)* sin(3*h/2)) proof let x; set y=3*x; set z=3*h; cD(sin(#)cos(#)cos,h).x = (sin(#)cos(#)cos).(x+h/2) - (sin(#)cos(#)cos). (x-h/2) by DIFF_1:5 .= ((sin(#)cos).(x+h/2))*(cos.(x+h/2)) -(sin(#)cos(#)cos).(x-h/2) by VALUED_1:5 .= (sin.(x+h/2))*(cos.(x+h/2))*(cos.(x+h/2)) -(sin(#)cos(#)cos).(x-h/2) by VALUED_1:5 .= (sin.(x+h/2))*(cos.(x+h/2))*(cos.(x+h/2)) -((sin(#)cos).(x-h/2))*(cos .(x-h/2)) by VALUED_1:5 .= sin(x+h/2)*cos(x+h/2)*cos(x+h/2) -sin(x-h/2)*cos(x-h/2)*cos(x-h/2) by VALUED_1:5 .= (1/4)*(sin((x+h/2)+(x+h/2)-(x+h/2)) -sin((x+h/2)+(x+h/2)-(x+h/2))+sin ((x+h/2)+(x+h/2) -(x+h/2))+sin((x+h/2)+(x+h/2)+(x+h/2)))-sin(x-h/2) *cos(x-h/2) *cos(x-h/2) by SIN_COS4:35 .= (1/4)*(sin(x+h/2)+sin(3*(x+h/2)))-(1/4) *(sin((x-h/2)+(x-h/2)-(x-h/2) )-sin((x-h/2)+(x-h/2) -(x-h/2))+sin((x-h/2)+(x-h/2)-(x-h/2))+sin((x-h/2) +(x-h/ 2)+(x-h/2))) by SIN_COS4:35 .= (1/4)*(sin(x+h/2)-sin(x-h/2)) +(1/4)*(sin(3*(x+h/2))-sin(3*(x-h/2))) .= (1/4)*(2*(cos(((x+h/2)+(x-h/2))/2) *sin(((x+h/2)-(x-h/2))/2)))+(1/4) *(sin(3*(x+h/2))-sin(3*(x-h/2))) by SIN_COS4:16 .= (1/4)*(2*(cos(x)*sin(h/2))) +(1/4)*(2*(cos(((y+z/2)+(y-z/2))/2) *sin( ((y+z/2)-(y-z/2))/2))) by SIN_COS4:16 .= (1/2)*(cos(x)*sin(h/2))+(1/2)*(cos(3*x)*sin(3*h/2)); hence thesis; end; :: f.x = tan(x) theorem x0 in dom tan & x1 in dom tan implies [!tan,x0,x1!]=sin(x0-x1)/(cos(x0 )*cos(x1)*(x0-x1)) proof assume that A1: x0 in dom tan and A2: x1 in dom tan; A3: tan.x0 = sin.x0*(cos.x0)" by A1,RFUNCT_1:def 1 .= sin.x0*(1/(cos.x0)) by XCMPLX_1:215 .= tan(x0) by XCMPLX_1:99; A4: tan.x1 = sin.x1*(cos.x1)" by A2,RFUNCT_1:def 1 .= sin.x1*(1/(cos.x1)) by XCMPLX_1:215 .= tan(x1) by XCMPLX_1:99; cos(x0)<>0 & cos(x1)<>0 by A1,A2,FDIFF_8:1; then [!tan,x0,x1!] = sin(x0-x1)/(cos(x0)*cos(x1)) /(x0-x1) by A3,A4, SIN_COS4:20 .= sin(x0-x1)/(cos(x0)*cos(x1)*(x0-x1)) by XCMPLX_1:78; hence thesis; end; :: f.x = cot(x) theorem x0 in dom cot & x1 in dom cot implies [!cot,x0,x1!] = - sin(x0-x1)/( sin(x0)*sin(x1)*(x0-x1)) proof assume that A1: x0 in dom cot and A2: x1 in dom cot; A3: cot.x0 = cos.x0*(sin.x0)" by A1,RFUNCT_1:def 1 .= cos.x0*(1/(sin.x0)) by XCMPLX_1:215 .= cot(x0) by XCMPLX_1:99; A4: cot.x1 = cos.x1*(sin.x1)" by A2,RFUNCT_1:def 1 .= cos.x1*(1/(sin.x1)) by XCMPLX_1:215 .= cot(x1) by XCMPLX_1:99; sin(x0)<>0 & sin(x1)<>0 by A1,A2,FDIFF_8:2; then [!cot,x0,x1!] = (-sin(x0-x1)/(sin(x0)*sin(x1))) /(x0-x1) by A3,A4, SIN_COS4:24 .= -sin(x0-x1)/(sin(x0)*sin(x1))/(x0-x1) by XCMPLX_1:187; hence thesis by XCMPLX_1:78; end; :: f.x = cosec(x) theorem 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)) proof assume that A1: x0 in dom cosec and A2: x1 in dom cosec; A3: cosec.x1 = (sin.x1)" by A2,RFUNCT_1:def 2 .= cosec(x1) by XCMPLX_1:215; cosec.x0 = (sin.x0)" by A1,RFUNCT_1:def 2 .= cosec(x0) by XCMPLX_1:215; then [!cosec,x0,x1!] = (1*sin(x1)/(sin(x0)*sin(x1)) -1/sin(x1))/(x0-x1) by A2,A3, RFUNCT_1:3,XCMPLX_1:91 .= (1*sin(x1)/(sin(x0)*sin(x1)) -1*sin(x0)/(sin(x1)*sin(x0)))/(x0-x1) by A1 ,RFUNCT_1:3,XCMPLX_1:91 .= (sin(x1)-sin(x0))/(sin(x1)*sin(x0))/(x0-x1) by XCMPLX_1:120 .= (sin(x1)-sin(x0))/(sin(x1)*sin(x0)*(x0-x1)) by XCMPLX_1:78 .= 2*(cos((x1+x0)/2)*sin((x1-x0)/2)) /(sin(x1)*sin(x0)*(x0-x1)) by SIN_COS4:16; hence thesis; end; :: f.x = sec(x) theorem 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)) proof assume that A1: x0 in dom sec and A2: x1 in dom sec; A3: sec.x1 = (cos.x1)" by A2,RFUNCT_1:def 2 .= sec(x1) by XCMPLX_1:215; sec.x0 = (cos.x0)" by A1,RFUNCT_1:def 2 .= sec(x0) by XCMPLX_1:215; then [!sec,x0,x1!] = (1*cos(x1)/(cos(x0)*cos(x1)) -1/cos(x1))/(x0-x1) by A2,A3, RFUNCT_1:3,XCMPLX_1:91 .= (1*cos(x1)/(cos(x0)*cos(x1)) -1*cos(x0)/(cos(x1)*cos(x0)))/(x0-x1) by A1 ,RFUNCT_1:3,XCMPLX_1:91 .= (cos(x1)-cos(x0))/(cos(x1)*cos(x0))/(x0-x1) by XCMPLX_1:120 .= (cos(x1)-cos(x0))/(cos(x1)*cos(x0)*(x0-x1)) by XCMPLX_1:78 .= (-2*(sin((x1+x0)/2)*sin((x1-x0)/2))) /(cos(x1)*cos(x0)*(x0-x1)) by SIN_COS4:18 .= -2*(sin((x1+x0)/2)*sin((x1-x0)/2)) /(cos(x1)*cos(x0)*(x0-x1)) by XCMPLX_1:187; hence thesis; end;