:: Difference and Difference Quotient -- Part {IV}
:: by Xiquan Liang , Ling Tang and Xichun Jiang
::
:: Received July 12, 2010
:: Copyright (c) 2010-2012 Association of Mizar Users


begin

theorem Th1: :: DIFF_4:1
for x0, x1 being Real st x0 > 0 & x1 > 0 holds
(log (number_e,x0)) - (log (number_e,x1)) = log (number_e,(x0 / x1))
proofend;

theorem :: DIFF_4:2
for x0, x1 being Real st x0 > 0 & x1 > 0 holds
(log (number_e,x0)) + (log (number_e,x1)) = log (number_e,(x0 * x1))
proofend;

theorem Th3: :: DIFF_4:3
for x being Real st x > 0 holds
log (number_e,x) = ln . x
proofend;

theorem Th4: :: DIFF_4:4
for x0, x1 being Real st x0 > 0 & x1 > 0 holds
(ln . x0) - (ln . x1) = ln . (x0 / x1)
proofend;

:: f.x=k/(x^2)
theorem :: DIFF_4:5
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 ^2) ) &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 * (((1 / ((x1 * x2) * x0)) * (((1 / x0) + (1 / x2)) + (1 / x1))) - ((1 / ((x2 * x1) * x3)) * (((1 / x3) + (1 / x1)) + (1 / x2))))) / (x0 - x3)
proofend;

:: f.x=(cot(x))^2
theorem :: DIFF_4:6
for x0, x1 being Real st x0 in dom cot &amp; x1 in dom cot holds
[!(cot (#) cot),x0,x1!] = - ((((cos x1) ^2) - ((cos x0) ^2)) / ((((sin x0) * (sin x1)) ^2) * (x0 - x1)))
proofend;

theorem :: DIFF_4:7
for x, h being Real st x in dom cot &amp; x + h in dom cot holds
(fD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((sin (x + h)) * (sin x)) ^2)
proofend;

theorem :: DIFF_4:8
for x, h being Real st x in dom cot &amp; x - h in dom cot holds
(bD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((sin x) * (sin (x - h))) ^2)
proofend;

theorem :: DIFF_4:9
for x, h being Real st x + (h / 2) in dom cot &amp; x - (h / 2) in dom cot holds
(cD ((cot (#) cot),h)) . x = ((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((sin (x + (h / 2))) * (sin (x - (h / 2)))) ^2)
proofend;

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

theorem :: DIFF_4:11
for x, h being Real st x in dom cosec &amp; x + h in dom cosec holds
(fD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) - (cos h)) ^2))
proofend;

theorem :: DIFF_4:12
for x, h being Real st x in dom cosec &amp; x - h in dom cosec holds
(bD ((cosec (#) cosec),h)) . x = - (((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) - (cos h)) ^2))
proofend;

theorem :: DIFF_4:13
for x, h being Real st x + (h / 2) in dom cosec &amp; x - (h / 2) in dom cosec holds
(cD ((cosec (#) cosec),h)) . x = - (((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) - (cos h)) ^2))
proofend;

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

theorem :: DIFF_4:15
for x, h being Real st x in dom sec &amp; x + h in dom sec holds
(fD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) + h))) * (sin h)) / (((cos ((2 * x) + h)) + (cos h)) ^2)
proofend;

theorem :: DIFF_4:16
for x, h being Real st x in dom sec &amp; x - h in dom sec holds
(bD ((sec (#) sec),h)) . x = ((4 * (sin ((2 * x) - h))) * (sin h)) / (((cos ((2 * x) - h)) + (cos h)) ^2)
proofend;

theorem :: DIFF_4:17
for x, h being Real st x + (h / 2) in dom sec &amp; x - (h / 2) in dom sec holds
(cD ((sec (#) sec),h)) . x = ((4 * (sin (2 * x))) * (sin h)) / (((cos (2 * x)) + (cos h)) ^2)
proofend;

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

theorem :: DIFF_4:19
for x, h being Real st x + h in (dom cosec) /\ (dom sec) &amp; x in (dom cosec) /\ (dom sec) holds
(fD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x)))))
proofend;

theorem :: DIFF_4:20
for x, h being Real st x - h in (dom cosec) /\ (dom sec) &amp; x in (dom cosec) /\ (dom sec) holds
(bD ((cosec (#) sec),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h))))))
proofend;

theorem :: DIFF_4:21
for x, h being Real st x + (h / 2) in (dom cosec) /\ (dom sec) &amp; x - (h / 2) in (dom cosec) /\ (dom sec) holds
(cD ((cosec (#) sec),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h)))))
proofend;

:: f.x=(tan(x))^2*cos(x)
theorem :: DIFF_4:22
for x0, x1 being Real st x0 in dom tan &amp; x1 in dom tan holds
[!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),x0,x1!]
proofend;

theorem :: DIFF_4:23
for x, h being Real st x in dom tan &amp; x + h in dom tan holds
(fD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x)
proofend;

theorem :: DIFF_4:24
for x, h being Real st x in dom tan &amp; x - h in dom tan holds
(bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (x - h))
proofend;

theorem :: DIFF_4:25
for x, h being Real st x + (h / 2) in dom tan &amp; x - (h / 2) in dom tan holds
(cD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (x - (h / 2)))
proofend;

:: f.x=(cot(x))^2*sin(x)
theorem :: DIFF_4:26
for x0, x1 being Real st x0 in dom cot &amp; x1 in dom cot holds
[!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),x0,x1!]
proofend;

theorem :: DIFF_4:27
for x, h being Real st x in dom cot &amp; x + h in dom cot holds
(fD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x)
proofend;

theorem :: DIFF_4:28
for x, h being Real st x in dom cot &amp; x - h in dom cot holds
(bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (x - h))
proofend;

theorem :: DIFF_4:29
for x, h being Real st x + (h / 2) in dom cot &amp; x - (h / 2) in dom cot holds
(cD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (x - (h / 2)))
proofend;

::f.x = ln.x
theorem :: DIFF_4:30
for x0, x1 being Real st x0 > 0 &amp; x1 > 0 holds
[!ln,x0,x1!] = (ln . (x0 / x1)) / (x0 - x1) by Th4;

theorem :: DIFF_4:31
for x, h being Real st x > 0 &amp; x + h > 0 holds
(fD (ln,h)) . x = ln . (1 + (h / x))
proofend;

theorem :: DIFF_4:32
for x, h being Real st x > 0 &amp; x - h > 0 holds
(bD (ln,h)) . x = ln . (1 + (h / (x - h)))
proofend;

theorem :: DIFF_4:33
for x, h being Real st x + (h / 2) > 0 &amp; x - (h / 2) > 0 holds
(cD (ln,h)) . x = ln . (1 + (h / (x - (h / 2))))
proofend;

theorem :: DIFF_4:34
for h, k being real number holds exp_R (h - k) = (exp_R h) / (exp_R k)
proofend;

:: f.x = fD(g,h).x
theorem :: DIFF_4:35
for h, x being Real
for f being Function of REAL,REAL holds (fD (f,h)) . x = ((Shift (f,h)) . x) - (f . x)
proofend;

theorem :: DIFF_4:36
for h, x0, x1 being Real
for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (fD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + h),(x1 + h)!] - [!g,x0,x1!]
proofend;

theorem :: DIFF_4:37
for h, x being Real
for f being Function of REAL,REAL holds (fD ((fD (f,h)),h)) . x = ((fD (f,(2 * h))) . x) - (2 * ((fD (f,h)) . x))
proofend;

theorem :: DIFF_4:38
for h, x being Real
for f being Function of REAL,REAL holds (bD ((fD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
proofend;

theorem :: DIFF_4:39
for h, x being Real
for f being Function of REAL,REAL holds (cD ((fD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)
proofend;

theorem Th40: :: DIFF_4:40
for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . 1) . x = (((fdif (f,h)) . 0) . (x + h)) - (((fdif (f,h)) . 0) . x)
proofend;

theorem :: DIFF_4:41
for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((fdif (f,h)) . (n + 1)) . x = (((fdif (f,h)) . n) . (x + h)) - (((fdif (f,h)) . n) . x)
proofend;

:: f.x = bD(g,h).x
theorem :: DIFF_4:42
for h, x being Real
for f being Function of REAL,REAL holds (bD (f,h)) . x = (f . x) - ((Shift (f,(- h))) . x)
proofend;

theorem :: DIFF_4:43
for h, x0, x1 being Real
for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (bD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,x0,x1!] - [!g,(x0 - h),(x1 - h)!]
proofend;

theorem :: DIFF_4:44
for h, x being Real
for f being Function of REAL,REAL holds (fD ((bD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
proofend;

theorem :: DIFF_4:45
for h, x being Real
for f being Function of REAL,REAL holds (bD ((bD (f,h)),h)) . x = (2 * ((bD (f,h)) . x)) - ((bD (f,(2 * h))) . x)
proofend;

theorem :: DIFF_4:46
for h, x being Real
for f being Function of REAL,REAL holds (cD ((bD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2)))
proofend;

theorem Th47: :: DIFF_4:47
for h, x being Real
for f being Function of REAL,REAL holds ((bdif (f,h)) . 1) . x = (((bdif (f,h)) . 0) . x) - (((bdif (f,h)) . 0) . (x - h))
proofend;

theorem :: DIFF_4:48
for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((bdif (f,h)) . (n + 1)) . x = (((bdif (f,h)) . n) . x) - (((bdif (f,h)) . n) . (x - h))
proofend;

:: f.x = cD(g,h).x
theorem :: DIFF_4:49
for h, x being Real
for f being Function of REAL,REAL holds (cD (f,h)) . x = ((Shift (f,(h / 2))) . x) - ((Shift (f,(- (h / 2)))) . x)
proofend;

theorem :: DIFF_4:50
for h, x0, x1 being Real
for f, g being Function of REAL,REAL st ( for x being Real holds f . x = (cD (g,h)) . x ) holds
[!f,x0,x1!] = [!g,(x0 + (h / 2)),(x1 + (h / 2))!] - [!g,(x0 - (h / 2)),(x1 - (h / 2))!]
proofend;

theorem :: DIFF_4:51
for h, x being Real
for f being Function of REAL,REAL holds (fD ((cD (f,h)),h)) . x = ((fD (f,h)) . (x + (h / 2))) - ((cD (f,h)) . x)
proofend;

theorem :: DIFF_4:52
for h, x being Real
for f being Function of REAL,REAL holds (bD ((cD (f,h)),h)) . x = ((cD (f,h)) . x) - ((bD (f,h)) . (x - (h / 2)))
proofend;

theorem :: DIFF_4:53
for h, x being Real
for f being Function of REAL,REAL holds (cD ((cD (f,h)),h)) . x = ((fD (f,h)) . x) - ((bD (f,h)) . x)
proofend;

theorem Th54: :: DIFF_4:54
for h, x being Real
for f being Function of REAL,REAL holds ((cdif (f,h)) . 1) . x = (((cdif (f,h)) . 0) . (x + (h / 2))) - (((cdif (f,h)) . 0) . (x - (h / 2)))
proofend;

theorem :: DIFF_4:55
for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((cdif (f,h)) . (n + 1)) . x = (((cdif (f,h)) . n) . (x + (h / 2))) - (((cdif (f,h)) . n) . (x - (h / 2)))
proofend;

:: f.x=(tan(x))^2*sin(x)
theorem :: DIFF_4:56
for x0, x1 being Real st x0 in dom tan &amp; x1 in dom tan holds
[!((tan (#) tan) (#) sin),x0,x1!] = ((((sin x0) |^ 3) * ((cos x1) ^2)) - (((sin x1) |^ 3) * ((cos x0) ^2))) / ((((cos x0) ^2) * ((cos x1) ^2)) * (x0 - x1))
proofend;

theorem :: DIFF_4:57
for x, h being Real st x in dom tan &amp; x + h in dom tan holds
(fD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + h)) |^ 3) * (((cos . (x + h)) ") |^ 2)) - (((sin . x) |^ 3) * (((cos . x) ") |^ 2))
proofend;

theorem :: DIFF_4:58
for x, h being Real st x in dom tan &amp; x - h in dom tan holds
(bD (((tan (#) tan) (#) sin),h)) . x = (((sin . x) |^ 3) * (((cos . x) ") |^ 2)) - (((sin . (x - h)) |^ 3) * (((cos . (x - h)) ") |^ 2))
proofend;

theorem :: DIFF_4:59
for x, h being Real st x + (h / 2) in dom tan &amp; x - (h / 2) in dom tan holds
(cD (((tan (#) tan) (#) sin),h)) . x = (((sin . (x + (h / 2))) |^ 3) * (((cos . (x + (h / 2))) ") |^ 2)) - (((sin . (x - (h / 2))) |^ 3) * (((cos . (x - (h / 2))) ") |^ 2))
proofend;

:: f.x=(cot(x))^2*cos(x)
theorem :: DIFF_4:60
for x0, x1 being Real st x0 in dom cot &amp; x1 in dom cot holds
[!((cot (#) cot) (#) cos),x0,x1!] = ((((cos x0) |^ 3) * ((sin x1) ^2)) - (((cos x1) |^ 3) * ((sin x0) ^2))) / ((((sin x0) ^2) * ((sin x1) ^2)) * (x0 - x1))
proofend;

theorem :: DIFF_4:61
for x, h being Real st x in dom cot &amp; x + h in dom cot holds
(fD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + h)) |^ 3) * (((sin . (x + h)) ") |^ 2)) - (((cos . x) |^ 3) * (((sin . x) ") |^ 2))
proofend;

theorem :: DIFF_4:62
for x, h being Real st x in dom cot &amp; x - h in dom cot holds
(bD (((cot (#) cot) (#) cos),h)) . x = (((cos . x) |^ 3) * (((sin . x) ") |^ 2)) - (((cos . (x - h)) |^ 3) * (((sin . (x - h)) ") |^ 2))
proofend;

theorem :: DIFF_4:63
for x, h being Real st x + (h / 2) in dom cot &amp; x - (h / 2) in dom cot holds
(cD (((cot (#) cot) (#) cos),h)) . x = (((cos . (x + (h / 2))) |^ 3) * (((sin . (x + (h / 2))) ") |^ 2)) - (((cos . (x - (h / 2))) |^ 3) * (((sin . (x - (h / 2))) ") |^ 2))
proofend;