:: Difference and Difference Quotient -- Part {II}
:: by Bo Li , Yanping Zhuang and Xiquan Liang
::
:: Received October 25, 2007
:: Copyright (c) 2007 Association of Mizar Users
theorem Th1: :: DIFF_2:1
theorem :: DIFF_2:2
theorem Th3: :: DIFF_2:3
theorem :: DIFF_2:4
theorem Th5: :: DIFF_2:5
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: :: DIFF_2:6
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 :: DIFF_2:7
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: :: DIFF_2:8
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: :: DIFF_2:9
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 :: DIFF_2:10
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 number ;
func [!f,x0,x1,x2,x3,x4!] -> Real equals :: DIFF_2:def 1
([!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 number holds
[!f,x0,x1,x2,x3,x4!] = ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4);
theorem Th11: :: DIFF_2:11
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: :: DIFF_2:12
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 :: DIFF_2:13
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 number ;
func [!f,x0,x1,x2,x3,x4,x5!] -> Real equals :: DIFF_2:def 2
([!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 number holds
[!f,x0,x1,x2,x3,x4,x5!] = ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5);
theorem Th14: :: DIFF_2:14
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: :: DIFF_2:15
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 :: DIFF_2:16
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 :: DIFF_2:17
theorem :: DIFF_2:18
for
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL ,
REAL st
x0,
x1,
x2,
x3 are_mutually_different holds
(
[!f,x0,x1,x2,x3!] = [!f,x1,x2,x3,x0!] &
[!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
theorem :: DIFF_2:19
for
x0,
x1,
x2,
x3 being
Real for
f being
Function of
REAL ,
REAL st
x0,
x1,
x2,
x3 are_mutually_different holds
(
[!f,x0,x1,x2,x3!] = [!f,x1,x0,x2,x3!] &
[!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] )
theorem :: DIFF_2:20
theorem Th21: :: DIFF_2:21
theorem Th22: :: DIFF_2:22
for
x0,
x1,
x2,
a,
b being
Real st
x0,
x1,
x2 are_mutually_different holds
[!(AffineMap a,b),x0,x1,x2!] = 0
theorem :: DIFF_2:23
for
x0,
x1,
x2,
x3,
a,
b being
Real st
x0,
x1,
x2,
x3 are_mutually_different holds
[!(AffineMap a,b),x0,x1,x2,x3!] = 0
theorem :: DIFF_2:24
theorem :: DIFF_2:25
theorem :: DIFF_2:26
theorem Th27: :: DIFF_2:27
theorem Th28: :: DIFF_2:28
for
a,
b,
c,
x0,
x1,
x2 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_different holds
[!f,x0,x1,x2!] = a
theorem Th29: :: DIFF_2:29
for
a,
b,
c,
x0,
x1,
x2,
x3 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_different holds
[!f,x0,x1,x2,x3!] = 0
theorem :: DIFF_2:30
for
a,
b,
c,
x0,
x1,
x2,
x3,
x4 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_different holds
[!f,x0,x1,x2,x3,x4!] = 0
theorem :: DIFF_2:31
theorem :: DIFF_2:32
theorem :: DIFF_2:33
theorem Th34: :: DIFF_2:34
theorem Th35: :: DIFF_2:35
theorem Th36: :: DIFF_2:36
for
k,
x0,
x1,
x2,
x3 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_different holds
[!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3))
theorem :: DIFF_2:37
for
k,
x0,
x1,
x2,
x3,
x4 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_different holds
[!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4)
theorem :: DIFF_2:38
theorem :: DIFF_2:39
theorem :: DIFF_2:40
theorem :: DIFF_2:41
theorem :: DIFF_2:42
theorem :: DIFF_2:43
theorem :: DIFF_2:44
theorem :: DIFF_2:45
theorem :: DIFF_2:46
theorem :: DIFF_2:47
theorem :: DIFF_2:48
theorem :: DIFF_2:49
theorem :: DIFF_2:50
theorem :: DIFF_2:51
theorem :: DIFF_2:52
theorem :: DIFF_2:53
theorem :: DIFF_2:54
theorem :: DIFF_2:55
theorem :: DIFF_2:56
theorem :: DIFF_2:57
theorem :: DIFF_2:58
theorem :: DIFF_2:59
theorem :: DIFF_2:60
theorem :: DIFF_2:61
theorem :: DIFF_2:62
theorem :: DIFF_2:63
theorem :: DIFF_2:64
theorem :: DIFF_2:65
theorem :: DIFF_2:66
theorem :: DIFF_2:67
theorem :: DIFF_2:68
theorem :: DIFF_2:69
theorem :: DIFF_2:70
theorem :: DIFF_2:71
theorem :: DIFF_2:72