begin
theorem Th4:
theorem Th9:
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem Th18:
theorem
theorem
theorem
theorem
theorem Th23:
theorem
theorem
theorem
theorem
theorem
theorem Th29:
theorem Th30:
theorem
theorem Th32:
theorem
for
r,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL ,
REAL holds
[!((r (#) f1) + f2),x0,x1!] = (r * [!f1,x0,x1!]) + [!f2,x0,x1!]
theorem
for
r,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL ,
REAL holds
[!((r (#) f1) - f2),x0,x1!] = (r * [!f1,x0,x1!]) - [!f2,x0,x1!]
theorem
for
r,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL ,
REAL holds
[!(f1 + (r (#) f2)),x0,x1!] = [!f1,x0,x1!] + (r * [!f2,x0,x1!])
theorem
for
r,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL ,
REAL holds
[!(f1 - (r (#) f2)),x0,x1!] = [!f1,x0,x1!] - (r * [!f2,x0,x1!])
theorem
for
r1,
r2,
x0,
x1 being
Real for
f1,
f2 being
Function of
REAL ,
REAL holds
[!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!])
theorem Th38:
theorem
for
x0,
x1,
x2 being
Real for
f being
Function of
REAL ,
REAL st
x0,
x1,
x2 are_mutually_different holds
[!f,x0,x1,x2!] = [!f,x0,x2,x1!]
theorem
for
h,
x being
Real for
f1,
f2 being
Function of
REAL ,
REAL for
S being
Seq_Sequence st ( for
n,
i being
Nat st
i <= n holds
(S . n) . i = ((n choose i) * (((bdif f1,h) . i) . x)) * (((bdif f2,h) . (n -' i)) . (x - (i * h))) ) holds
(
((bdif (f1 (#) f2),h) . 1) . x = Sum (S . 1),1 &
((bdif (f1 (#) f2),h) . 2) . x = Sum (S . 2),2 )
theorem Th42:
theorem
for
h,
x being
Real for
f1,
f2 being
Function of
REAL ,
REAL for
S being
Seq_Sequence st ( for
n,
i being
Nat st
i <= n holds
(S . n) . i = ((n choose i) * (((cdif f1,h) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif f2,h) . (n -' i)) . (x - (i * (h / 2)))) ) holds
(
((cdif (f1 (#) f2),h) . 1) . x = Sum (S . 1),1 &
((cdif (f1 (#) f2),h) . 2) . x = Sum (S . 2),2 )
theorem
theorem
theorem
for
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL ,
REAL st ( for
x being
Real holds
f . x = sqrt x ) &
x0,
x1,
x2,
x3 are_mutually_different &
x0 > 0 &
x1 > 0 &
x2 > 0 &
x3 > 0 holds
[!f,x0,x1,x2,x3!] = ((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3)))
theorem
theorem
theorem
theorem
theorem
theorem
for
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL ,
REAL st ( for
x being
Real holds
f . x = x ^2 ) &
x0,
x1,
x2,
x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = 0
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem
theorem