:: Difference and Difference Quotient -- Part {II}
:: by Bo Li , Yanping Zhuang and Xiquan Liang
::
:: Received October 25, 2007
:: Copyright (c) 2007-2012 Association of Mizar Users


begin

theorem Th1: :: DIFF_2:1
for x, h being Real
for f being Function of REAL,REAL holds [!f,x,(x + h)!] = (((fdif (f,h)) . 1) . x) / h
proofend;

theorem :: DIFF_2:2
for h, x being Real
for f being Function of REAL,REAL st h <> 0 holds
[!f,x,(x + h),(x + (2 * h))!] = (((fdif (f,h)) . 2) . x) / (2 * (h ^2))
proofend;

theorem Th3: :: DIFF_2:3
for x, h being Real
for f being Function of REAL,REAL holds [!f,(x - h),x!] = (((bdif (f,h)) . 1) . x) / h
proofend;

theorem :: DIFF_2:4
for h, x being Real
for f being Function of REAL,REAL st h <> 0 holds
[!f,(x - (2 * h)),(x - h),x!] = (((bdif (f,h)) . 2) . x) / (2 * (h ^2))
proofend;

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!]
proofend;

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!]
proofend;

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!])
proofend;

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!]
proofend;

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!]
proofend;

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!])
proofend;

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!]
proofend;

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!]
proofend;

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!])
proofend;

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!]
proofend;

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!]
proofend;

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!])
proofend;

theorem :: DIFF_2:17
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) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1)))
proofend;

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!] &amp; [!f,x0,x1,x2,x3!] = [!f,x3,x2,x1,x0!] )
proofend;

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!] &amp; [!f,x0,x1,x2,x3!] = [!f,x1,x2,x0,x3!] )
proofend;

theorem :: DIFF_2:20
for x0, x1, x2 being Real
for f being Function of REAL,REAL st f is constant holds
[!f,x0,x1,x2!] = 0
proofend;

:: f.x=a*x+b
theorem Th21: :: DIFF_2:21
for x0, x1, a, b being Real st x0 <> x1 holds
[!(AffineMap (a,b)),x0,x1!] = a
proofend;

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
proofend;

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
proofend;

theorem :: DIFF_2:24
for a, b, h, x being Real holds (fD ((AffineMap (a,b)),h)) . x = a * h
proofend;

theorem :: DIFF_2:25
for a, b, h, x being Real holds (bD ((AffineMap (a,b)),h)) . x = a * h
proofend;

theorem :: DIFF_2:26
for a, b, h, x being Real holds (cD ((AffineMap (a,b)),h)) . x = a * h
proofend;

:: f.x=a*x^2+b*x+c
theorem Th27: :: DIFF_2:27
for a, b, c, x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) &amp; x0 <> x1 holds
[!f,x0,x1!] = (a * (x0 + x1)) + b
proofend;

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 ) &amp; x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = a
proofend;

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 ) &amp; x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = 0
proofend;

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 ) &amp; x0,x1,x2,x3,x4 are_mutually_different holds
[!f,x0,x1,x2,x3,x4!] = 0
proofend;

theorem :: DIFF_2:31
for a, b, c, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (fD (f,h)) . x = ((((2 * a) * h) * x) + (a * (h ^2))) + (b * h)
proofend;

theorem :: DIFF_2:32
for a, b, c, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (bD (f,h)) . x = ((((2 * a) * h) * x) - (a * (h ^2))) + (b * h)
proofend;

theorem :: DIFF_2:33
for a, b, c, h being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = ((a * (x ^2)) + (b * x)) + c ) holds
for x being Real holds (cD (f,h)) . x = (((2 * a) * h) * x) + (b * h)
proofend;

:: f.x=k/x
theorem Th34: :: DIFF_2:34
for k, x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) &amp; x0 <> x1 &amp; x0 <> 0 &amp; x1 <> 0 holds
[!f,x0,x1!] = - (k / (x0 * x1))
proofend;

theorem Th35: :: DIFF_2:35
for k, x0, x1, x2 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / x ) &amp; x0 <> 0 &amp; x1 <> 0 &amp; x2 <> 0 &amp; x0,x1,x2 are_mutually_different holds
[!f,x0,x1,x2!] = k / ((x0 * x1) * x2)
proofend;

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 ) &amp; x0 <> 0 &amp; x1 <> 0 &amp; x2 <> 0 &amp; x3 <> 0 &amp; x0,x1,x2,x3 are_mutually_different holds
[!f,x0,x1,x2,x3!] = - (k / (((x0 * x1) * x2) * x3))
proofend;

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 ) &amp; x0 <> 0 &amp; x1 <> 0 &amp; x2 <> 0 &amp; x3 <> 0 &amp; x4 <> 0 &amp; x0,x1,x2,x3,x4 are_mutually_different holds
[!f,x0,x1,x2,x3,x4!] = k / ((((x0 * x1) * x2) * x3) * x4)
proofend;

theorem :: DIFF_2:38
for k, h being Real
for f being Function of REAL,REAL st ( for x being Real holds
( f . x = k / x &amp; x <> 0 &amp; x + h <> 0 ) ) holds
for x being Real holds (fD (f,h)) . x = (- (k * h)) / ((x + h) * x) ;

theorem :: DIFF_2:39
for k, h being Real
for f being Function of REAL,REAL st ( for x being Real holds
( f . x = k / x &amp; x <> 0 &amp; x - h <> 0 ) ) holds
for x being Real holds (bD (f,h)) . x = (- (k * h)) / ((x - h) * x) ;

theorem :: DIFF_2:40
for k, h being Real
for f being Function of REAL,REAL st ( for x being Real holds
( f . x = k / x &amp; x + (h / 2) <> 0 &amp; x - (h / 2) <> 0 ) ) holds
for x being Real holds (cD (f,h)) . x = (- (k * h)) / ((x - (h / 2)) * (x + (h / 2)))
proofend;

:: f.x = sin(x)
theorem :: DIFF_2:41
for x0, x1 being Real holds [!sin,x0,x1!] = ((2 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1)
proofend;

theorem :: DIFF_2:42
for h, x being Real holds (fD (sin,h)) . x = 2 * ((cos (((2 * x) + h) / 2)) * (sin (h / 2)))
proofend;

theorem :: DIFF_2:43
for h, x being Real holds (bD (sin,h)) . x = 2 * ((cos (((2 * x) - h) / 2)) * (sin (h / 2)))
proofend;

theorem :: DIFF_2:44
for h, x being Real holds (cD (sin,h)) . x = 2 * ((cos x) * (sin (h / 2)))
proofend;

:: f.x = cos(x)
theorem :: DIFF_2:45
for x0, x1 being Real holds [!cos,x0,x1!] = - (((2 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) / (x0 - x1))
proofend;

theorem :: DIFF_2:46
for h, x being Real holds (fD (cos,h)) . x = - (2 * ((sin (((2 * x) + h) / 2)) * (sin (h / 2))))
proofend;

theorem :: DIFF_2:47
for h, x being Real holds (bD (cos,h)) . x = - (2 * ((sin (((2 * x) - h) / 2)) * (sin (h / 2))))
proofend;

theorem :: DIFF_2:48
for h, x being Real holds (cD (cos,h)) . x = - (2 * ((sin x) * (sin (h / 2))))
proofend;

:: f.x = (sin x)^2
theorem :: DIFF_2:49
for x0, x1 being Real holds [!(sin (#) sin),x0,x1!] = ((1 / 2) * ((cos (2 * x1)) - (cos (2 * x0)))) / (x0 - x1)
proofend;

theorem :: DIFF_2:50
for h, x being Real holds (fD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x + h))))
proofend;

theorem :: DIFF_2:51
for h, x being Real holds (bD ((sin (#) sin),h)) . x = (1 / 2) * ((cos (2 * (x - h))) - (cos (2 * x)))
proofend;

theorem :: DIFF_2:52
for h, x being Real holds (cD ((sin (#) sin),h)) . x = (1 / 2) * ((cos ((2 * x) - h)) - (cos ((2 * x) + h)))
proofend;

:: f.x = sin(x)*cos(x)
theorem :: DIFF_2:53
for x0, x1 being Real holds [!(sin (#) cos),x0,x1!] = ((1 / 2) * ((sin (2 * x0)) - (sin (2 * x1)))) / (x0 - x1)
proofend;

theorem :: DIFF_2:54
for h, x being Real holds (fD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * (x + h))) - (sin (2 * x)))
proofend;

theorem :: DIFF_2:55
for h, x being Real holds (bD ((sin (#) cos),h)) . x = (1 / 2) * ((sin (2 * x)) - (sin (2 * (x - h))))
proofend;

theorem :: DIFF_2:56
for h, x being Real holds (cD ((sin (#) cos),h)) . x = (1 / 2) * ((sin ((2 * x) + h)) - (sin ((2 * x) - h)))
proofend;

:: f.x = (cos(x))^2
theorem :: DIFF_2:57
for x0, x1 being Real holds [!(cos (#) cos),x0,x1!] = ((1 / 2) * ((cos (2 * x0)) - (cos (2 * x1)))) / (x0 - x1)
proofend;

theorem :: DIFF_2:58
for h, x being Real holds (fD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))
proofend;

theorem :: DIFF_2:59
for h, x being Real holds (bD ((cos (#) cos),h)) . x = (1 / 2) * ((cos (2 * x)) - (cos (2 * (x - h))))
proofend;

theorem :: DIFF_2:60
for h, x being Real holds (cD ((cos (#) cos),h)) . x = (1 / 2) * ((cos ((2 * x) + h)) - (cos ((2 * x) - h)))
proofend;

:: f.x = (sin(x))^2*cos(x)
theorem :: DIFF_2:61
for x0, x1 being Real holds [!((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))
proofend;

theorem :: DIFF_2:62
for h, x being Real 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))))
proofend;

theorem :: DIFF_2:63
for h, x being Real 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))))
proofend;

theorem :: DIFF_2:64
for h, x being Real holds (cD (((sin (#) sin) (#) cos),h)) . x = (- ((1 / 2) * ((sin x) * (sin (h / 2))))) + ((1 / 2) * ((sin (3 * x)) * (sin ((3 * h) / 2))))
proofend;

:: f.x = sin(x)*(cos(x))^2
theorem :: DIFF_2:65
for x0, x1 being Real holds [!((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)
proofend;

theorem :: DIFF_2:66
for h, x being Real 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))))
proofend;

theorem :: DIFF_2:67
for h, x being Real 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))))
proofend;

theorem :: DIFF_2:68
for h, x being Real holds (cD (((sin (#) cos) (#) cos),h)) . x = (1 / 2) * (((cos x) * (sin (h / 2))) + ((cos (3 * x)) * (sin ((3 * h) / 2))))
proofend;

:: f.x = tan(x)
theorem :: DIFF_2:69
for x0, x1 being Real st x0 in dom tan &amp; x1 in dom tan holds
[!tan,x0,x1!] = (sin (x0 - x1)) / (((cos x0) * (cos x1)) * (x0 - x1))
proofend;

:: f.x = cot(x)
theorem :: DIFF_2:70
for x0, x1 being Real st x0 in dom cot &amp; x1 in dom cot holds
[!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1)))
proofend;

:: f.x = cosec(x)
theorem :: DIFF_2:71
for x0, x1 being Real st x0 in dom cosec &amp; x1 in dom cosec holds
[!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1))
proofend;

:: f.x = sec(x)
theorem :: DIFF_2:72
for x0, x1 being Real st x0 in dom sec &amp; x1 in dom sec holds
[!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1)))
proofend;