:: Difference and Difference Quotient -- Part {IV}
:: by Xiquan Liang , Ling Tang and Xichun Jiang
::
:: Received July 12, 2010
:: 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
[!(cot (#) cot),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 ((cot (#) cot),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 ((cot (#) cot),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 ((cot (#) cot),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
[!(cosec (#) cosec),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 ((cosec (#) cosec),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 ((cosec (#) cosec),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 ((cosec (#) cosec),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
[!(sec (#) sec),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 ((sec (#) sec),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 ((sec (#) sec),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 ((sec (#) sec),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 (dom cosec) /\ (dom sec) & 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)

proof end;

theorem :: DIFF_4:19

for h, x being Real st x + h in (dom cosec) /\ (dom sec) & 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)))))

proof end;

theorem :: DIFF_4:20

for h, x being Real st x - h in (dom cosec) /\ (dom sec) & 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))))))

proof end;

theorem :: DIFF_4:21

for h, x being Real st x + (h / 2) in (dom cosec) /\ (dom sec) & 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)))))

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
[!((tan (#) tan) (#) cos),x0,x1!] = [!(tan (#) sin),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 (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + h)) - ((tan (#) sin) . x)

proof end;

theorem :: DIFF_4:24

for h, x being Real st x in dom tan & x - h in dom tan holds
(bD (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . x) - ((tan (#) sin) . (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 (((tan (#) tan) (#) cos),h)) . x = ((tan (#) sin) . (x + (h / 2))) - ((tan (#) sin) . (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
[!((cot (#) cot) (#) sin),x0,x1!] = [!(cot (#) cos),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 (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + h)) - ((cot (#) cos) . x)

proof end;

theorem :: DIFF_4:28

for h, x being Real st x in dom cot & x - h in dom cot holds
(bD (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . x) - ((cot (#) cos) . (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 (((cot (#) cot) (#) sin),h)) . x = ((cot (#) cos) . (x + (h / 2))) - ((cot (#) cos) . (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) = (exp_R h) / (exp_R 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
[!((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))

proof end;

theorem :: DIFF_4:57

for h, x being Real st x in dom tan & 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))

proof end;

theorem :: DIFF_4:58

for h, x being Real st x in dom tan & 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))

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 (((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))

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
[!((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))

proof end;

theorem :: DIFF_4:61

for h, x being Real st x in dom cot & 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))

proof end;

theorem :: DIFF_4:62

for h, x being Real st x in dom cot & 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))

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 (((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))

proof end;