:: Difference and Difference Quotient -- Part {II}
:: by Bo Li , Yanping Zhuang and Xiquan Liang
::
:: Received October 25, 2007
:: Copyright (c) 2007-2026 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;