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

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))
proof end;

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))
proof end;

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

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

:: 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) ) & x0 <> 0 & x1 <> 0 & x2 <> 0 & x3 <> 0 & x0,x1,x2,x3 are_mutually_distinct 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)
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: DIFF_4:19
for h, x being Real st x + h in () /\ () & x in () /\ () holds
(fD ((),h)) . x = - (4 * (((cos ((2 * x) + h)) * (sin h)) / ((sin (2 * (x + h))) * (sin (2 * x)))))
proof end;

theorem :: DIFF_4:20
for h, x being Real st x - h in () /\ () & x in () /\ () holds
(bD ((),h)) . x = - (4 * (((cos ((2 * x) - h)) * (sin h)) / ((sin (2 * x)) * (sin (2 * (x - h))))))
proof end;

theorem :: DIFF_4:21
for h, x being Real st x + (h / 2) in () /\ () & x - (h / 2) in () /\ () holds
(cD ((),h)) . x = - (4 * (((cos (2 * x)) * (sin h)) / ((sin ((2 * x) + h)) * (sin ((2 * x) - h)))))
proof end;

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

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

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

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

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

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

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

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

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

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

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

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

theorem :: DIFF_4:34
for h, k being Real holds exp_R (h - k) = () / ()
proof end;

:: 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)
proof end;

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!]
proof end;

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))
proof end;

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)
proof end;

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)
proof end;

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)
proof end;

theorem :: DIFF_4:41
for n being 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)
proof end;

:: 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)
proof end;

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

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)
proof end;

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)
proof end;

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)))
proof end;

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))
proof end;

theorem :: DIFF_4:48
for n being 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))
proof end;

:: 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)
proof end;

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

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)
proof end;

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)))
proof end;

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)
proof end;

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)))
proof end;

theorem :: DIFF_4:55
for n being 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)))
proof end;

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

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

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

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

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

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

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

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