environ
vocabularies HIDDEN, 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 HIDDEN, 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;
definitions ;
theorems DIFF_1, XCMPLX_1, SIN_COS4, ZFMISC_1, RFUNCT_1, FCONT_1, FDIFF_8, VALUED_1;
schemes ;
registrations XREAL_0, RELSET_1, MEMBERED, FUNCT_2, VALUED_0, VALUED_1, SQUARE_1, SIN_COS;
constructors HIDDEN, SQUARE_1, REAL_1, DIFF_1, PARTFUN3, SIN_COS, SIN_COS4, FCONT_1, FDIFF_9, SEQFUNC, RELSET_1, VALUED_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM;
equalities DIFF_1, SIN_COS4, SQUARE_1, SIN_COS, FDIFF_9;
expansions ;
theorem Th5:
for
r,
x0,
x1,
x2 being
Real for
f being
Function of
REAL,
REAL holds
[!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!]
theorem Th6:
for
x0,
x1,
x2 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!(f1 + f2),x0,x1,x2!] = [!f1,x0,x1,x2!] + [!f2,x0,x1,x2!]
theorem
for
r1,
r2,
x0,
x1,
x2 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2!] = (r1 * [!f1,x0,x1,x2!]) + (r2 * [!f2,x0,x1,x2!])
theorem Th8:
for
r,
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL,
REAL holds
[!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!]
theorem Th9:
for
x0,
x1,
x2,
x3 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!(f1 + f2),x0,x1,x2,x3!] = [!f1,x0,x1,x2,x3!] + [!f2,x0,x1,x2,x3!]
theorem
for
r1,
r2,
x0,
x1,
x2,
x3 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3!] = (r1 * [!f1,x0,x1,x2,x3!]) + (r2 * [!f2,x0,x1,x2,x3!])
definition
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
coherence
([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4) is Real;
;
end;
::
deftheorem defines
[! DIFF_2:def 1 :
for f being real-valued Function
for x0, x1, x2, x3, x4 being Real holds [!f,x0,x1,x2,x3,x4!] = ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4);
theorem Th11:
for
r,
x0,
x1,
x2,
x3,
x4 being
Real for
f being
Function of
REAL,
REAL holds
[!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!]
theorem Th12:
for
x0,
x1,
x2,
x3,
x4 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]
theorem
for
r1,
r2,
x0,
x1,
x2,
x3,
x4 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4!] = (r1 * [!f1,x0,x1,x2,x3,x4!]) + (r2 * [!f2,x0,x1,x2,x3,x4!])
definition
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
coherence
([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5) is Real;
;
end;
::
deftheorem defines
[! DIFF_2:def 2 :
for f being real-valued Function
for x0, x1, x2, x3, x4, x5 being Real holds [!f,x0,x1,x2,x3,x4,x5!] = ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5);
theorem Th14:
for
r,
x0,
x1,
x2,
x3,
x4,
x5 being
Real for
f being
Function of
REAL,
REAL holds
[!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!]
theorem Th15:
for
x0,
x1,
x2,
x3,
x4,
x5 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!]
theorem
for
r1,
r2,
x0,
x1,
x2,
x3,
x4,
x5 being
Real for
f1,
f2 being
Function of
REAL,
REAL holds
[!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!])
theorem
for
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL,
REAL st
x0,
x1,
x2,
x3 are_mutually_distinct holds
(
[!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] &
[!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
theorem
for
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL,
REAL st
x0,
x1,
x2,
x3 are_mutually_distinct holds
(
[!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] &
[!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] )
theorem Th22:
for
x0,
x1,
x2,
a,
b being
Real st
x0,
x1,
x2 are_mutually_distinct holds
[!(AffineMap (a,b)),x0,x1,x2!] = 0
theorem
for
x0,
x1,
x2,
x3,
a,
b being
Real st
x0,
x1,
x2,
x3 are_mutually_distinct holds
[!(AffineMap (a,b)),x0,x1,x2,x3!] = 0
theorem Th28:
for
x0,
x1,
x2,
a,
b,
c being
Real for
f being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = ((a * (x ^2)) + (b * x)) + c ) &
x0,
x1,
x2 are_mutually_distinct holds
[!f,x0,x1,x2!] = a
theorem Th29:
for
x0,
x1,
x2,
x3,
a,
b,
c being
Real for
f being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = ((a * (x ^2)) + (b * x)) + c ) &
x0,
x1,
x2,
x3 are_mutually_distinct holds
[!f,x0,x1,x2,x3!] = 0
theorem
for
x0,
x1,
x2,
x3,
x4,
a,
b,
c being
Real for
f being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = ((a * (x ^2)) + (b * x)) + c ) &
x0,
x1,
x2,
x3,
x4 are_mutually_distinct holds
[!f,x0,x1,x2,x3,x4!] = 0
theorem Th36:
for
x0,
x1,
x2,
x3,
k being
Real for
f being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = k / x ) &
x0 <> 0 &
x1 <> 0 &
x2 <> 0 &
x3 <> 0 &
x0,
x1,
x2,
x3 are_mutually_distinct holds
[!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3))
theorem
for
x0,
x1,
x2,
x3,
x4,
k being
Real for
f being
Function of
REAL,
REAL st ( for
x being
Real holds
f . x = k / x ) &
x0 <> 0 &
x1 <> 0 &
x2 <> 0 &
x3 <> 0 &
x4 <> 0 &
x0,
x1,
x2,
x3,
x4 are_mutually_distinct holds
[!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4)