:: Difference and Difference Quotient -- Part {III}
:: by Xiquan Liang and Ling Tang
::
:: Received November 17, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users

theorem Th1: :: DIFF_3:1

for h, x being Real
for f being Function of REAL,REAL holds (cD (f,h)) . x = ((fD (f,(h / 2))) . x) - ((fD (f,(- (h / 2)))) . x)

proof end;

theorem Th2: :: DIFF_3:2

for h, x being Real
for f being Function of REAL,REAL holds (fD (f,(- (h / 2)))) . x = - ((bD (f,(h / 2))) . x)

proof end;

theorem :: DIFF_3:3

for h, x being Real
for f being Function of REAL,REAL holds (cD (f,h)) . x = ((bD (f,(h / 2))) . x) - ((bD (f,(- (h / 2)))) . x)

proof end;

theorem :: DIFF_3:4

for n being Element of NAT
for h, r, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((fdif (f1,h)) . (n + 1)) . x)) + (((fdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_3:5

for n being Element of NAT
for h, r, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x = (((fdif (f1,h)) . (n + 1)) . x) + (r * (((fdif (f2,h)) . (n + 1)) . x))

proof end;

theorem :: DIFF_3:6

for n being Element of NAT
for h, r1, r2, x being Real
for f1, f2 being Function of REAL,REAL holds ((fdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((fdif (f1,h)) . (n + 1)) . x)) - (r2 * (((fdif (f2,h)) . (n + 1)) . x))

proof end;

theorem :: DIFF_3:7

for h being Real
for f being Function of REAL,REAL holds (fdif (f,h)) . 1 = fD (f,h)

proof end;

theorem :: DIFF_3:8

for n being Element of NAT
for h, r, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((bdif (f1,h)) . (n + 1)) . x)) + (((bdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_3:9

for n being Element of NAT
for h, r, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x = (((bdif (f1,h)) . (n + 1)) . x) + (r * (((bdif (f2,h)) . (n + 1)) . x))

proof end;

theorem :: DIFF_3:10

for n being Element of NAT
for h, r1, r2, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((bdif (f1,h)) . (n + 1)) . x)) - (r2 * (((bdif (f2,h)) . (n + 1)) . x))

proof end;

theorem Th11: :: DIFF_3:11

for h being Real
for f being Function of REAL,REAL holds (bdif (f,h)) . 1 = bD (f,h)

proof end;

theorem :: DIFF_3:12

for n, m being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((bdif (((bdif (f,h)) . m),h)) . n) . x = ((bdif (f,h)) . (m + n)) . x

proof end;

theorem :: DIFF_3:13

for n being Element of NAT
for h, r, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif (((r (#) f1) + f2),h)) . (n + 1)) . x = (r * (((cdif (f1,h)) . (n + 1)) . x)) + (((cdif (f2,h)) . (n + 1)) . x)

proof end;

theorem :: DIFF_3:14

for n being Element of NAT
for h, r, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 + (r (#) f2)),h)) . (n + 1)) . x = (((cdif (f1,h)) . (n + 1)) . x) + (r * (((cdif (f2,h)) . (n + 1)) . x))

proof end;

theorem :: DIFF_3:15

for n being Element of NAT
for h, r1, r2, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif (((r1 (#) f1) - (r2 (#) f2)),h)) . (n + 1)) . x = (r1 * (((cdif (f1,h)) . (n + 1)) . x)) - (r2 * (((cdif (f2,h)) . (n + 1)) . x))

proof end;

theorem Th16: :: DIFF_3:16

for h being Real
for f being Function of REAL,REAL holds (cdif (f,h)) . 1 = cD (f,h)

proof end;

theorem :: DIFF_3:17

for n, m being Element of NAT
for h, x being Real
for f being Function of REAL,REAL holds ((cdif (((cdif (f,h)) . m),h)) . n) . x = ((cdif (f,h)) . (m + n)) . x

proof end;

theorem :: DIFF_3:18

for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL st ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . (x + ((n / 2) * h)) holds
((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . (x - ((n / 2) * h))

proof end;

theorem :: DIFF_3:19

for n being Element of NAT
for h, x being Real
for f being Function of REAL,REAL st ((fdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x + (((n - 1) / 2) * h)) + (h / 2)) holds
((bdif (f,h)) . n) . x = ((cdif (f,h)) . n) . ((x - (((n - 1) / 2) * h)) - (h / 2))

proof end;

theorem :: DIFF_3:20

for h, x being Real
for f being Function of REAL,REAL holds [!f,x,(x + h)!] = ((fD (f,h)) . x) / h

proof end;

theorem :: DIFF_3:21

for h, x being Real
for f being Function of REAL,REAL holds [!f,(x - h),x!] = ((bD (f,h)) . x) / h

proof end;

theorem Th22: :: DIFF_3:22

for h, x being Real
for f being Function of REAL,REAL holds [!f,(x - (h / 2)),(x + (h / 2))!] = ((cD (f,h)) . x) / h

proof end;

theorem Th23: :: DIFF_3:23

for h, x being Real
for f being Function of REAL,REAL holds [!f,(x - (h / 2)),(x + (h / 2))!] = (((cdif (f,h)) . 1) . x) / h

proof end;

theorem :: DIFF_3:24

for h, x being Real
for f being Function of REAL,REAL st h <> 0 holds
[!f,(x - h),x,(x + h)!] = (((cdif (f,h)) . 2) . x) / ((2 * h) * h)

proof end;

theorem Th25: :: DIFF_3:25

for x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 - f2),x0,x1!] = [!f1,x0,x1!] - [!f2,x0,x1!]

proof end;

theorem :: DIFF_3:26

for r, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!((r (#) f1) + f2),x0,x1!] = (r * [!f1,x0,x1!]) + [!f2,x0,x1!]

proof end;

theorem :: DIFF_3:27

for r, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!((r (#) f1) - f2),x0,x1!] = (r * [!f1,x0,x1!]) - [!f2,x0,x1!]

proof end;

theorem :: DIFF_3:28

for r, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 + (r (#) f2)),x0,x1!] = [!f1,x0,x1!] + (r * [!f2,x0,x1!])

proof end;

theorem :: DIFF_3:29

for r, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 - (r (#) f2)),x0,x1!] = [!f1,x0,x1!] - (r * [!f2,x0,x1!])

proof end;

theorem :: DIFF_3:30

for r1, r2, x0, x1 being Real
for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) - (r2 (#) f2)),x0,x1!] = (r1 * [!f1,x0,x1!]) - (r2 * [!f2,x0,x1!])

proof end;

theorem Th31: :: DIFF_3:31

for h, x being Real
for f1, f2 being Function of REAL,REAL holds ((bdif ((f1 (#) f2),h)) . 1) . x = ((f1 . x) * (((bdif (f2,h)) . 1) . x)) + ((f2 . (x - h)) * (((bdif (f1,h)) . 1) . x))

proof end;

theorem :: DIFF_3:32

for x0, x1, x2 being Real
for f being Function of REAL,REAL st x0,x1,x2 are_mutually_distinct holds
[!f,x0,x1,x2!] = [!f,x0,x2,x1!]

proof end;

theorem :: DIFF_3:33

for h, x being Real
for f1, f2 being Function of REAL,REAL
for S being Seq_Sequence st ( for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((bdif (f1,h)) . i) . x)) * (((bdif (f2,h)) . (n -' i)) . (x - (i * h))) ) holds
( ((bdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((bdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )

proof end;

theorem Th34: :: DIFF_3:34

for h, x being Real
for f1, f2 being Function of REAL,REAL holds ((cdif ((f1 (#) f2),h)) . 1) . x = ((f1 . (x + (h / 2))) * (((cdif (f2,h)) . 1) . x)) + ((f2 . (x - (h / 2))) * (((cdif (f1,h)) . 1) . x))

proof end;

theorem :: DIFF_3:35

for h, x being Real
for f1, f2 being Function of REAL,REAL
for S being Seq_Sequence st ( for n, i being Nat st i <= n holds
(S . n) . i = ((n choose i) * (((cdif (f1,h)) . i) . (x + ((n -' i) * (h / 2))))) * (((cdif (f2,h)) . (n -' i)) . (x - (i * (h / 2)))) ) holds
( ((cdif ((f1 (#) f2),h)) . 1) . x = Sum ((S . 1),1) & ((cdif ((f1 (#) f2),h)) . 2) . x = Sum ((S . 2),2) )

proof end;

:: f.x=sqrt x

theorem :: DIFF_3:36

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x0 <> x1 & x0 > 0 & x1 > 0 holds
[!f,x0,x1!] = 1 / ((sqrt x0) + (sqrt x1))

proof end;

theorem :: DIFF_3:37

for x0, x1, x2 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x0,x1,x2 are_mutually_distinct & x0 > 0 & x1 > 0 & x2 > 0 holds
[!f,x0,x1,x2!] = - (1 / ((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x1) + (sqrt x2))))

proof end;

theorem :: DIFF_3:38

for x0, x1, x2, x3 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x0,x1,x2,x3 are_mutually_distinct & x0 > 0 & x1 > 0 & x2 > 0 & x3 > 0 holds
[!f,x0,x1,x2,x3!] = ((((sqrt x0) + (sqrt x1)) + (sqrt x2)) + (sqrt x3)) / (((((((sqrt x0) + (sqrt x1)) * ((sqrt x0) + (sqrt x2))) * ((sqrt x0) + (sqrt x3))) * ((sqrt x1) + (sqrt x2))) * ((sqrt x1) + (sqrt x3))) * ((sqrt x2) + (sqrt x3)))

proof end;

theorem :: DIFF_3:39

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x > 0 & x + h > 0 holds
(fD (f,h)) . x = (sqrt (x + h)) - (sqrt x)

proof end;

theorem :: DIFF_3:40

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x > 0 & x - h > 0 holds
(bD (f,h)) . x = (sqrt x) - (sqrt (x - h))

proof end;

theorem :: DIFF_3:41

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = sqrt x ) & x + (h / 2) > 0 & x - (h / 2) > 0 holds
(cD (f,h)) . x = (sqrt (x + (h / 2))) - (sqrt (x - (h / 2)))

proof end;

:: f.x=x^2

theorem :: DIFF_3:42

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) & x0 <> x1 holds
[!f,x0,x1!] = x0 + x1

proof end;

theorem :: DIFF_3:43

for x0, x1, x2 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) & x0,x1,x2 are_mutually_distinct holds
[!f,x0,x1,x2!] = 1

proof end;

theorem :: DIFF_3:44

for x0, x1, x2, x3 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) & x0,x1,x2,x3 are_mutually_distinct holds
[!f,x0,x1,x2,x3!] = 0

proof end;

theorem :: DIFF_3:45

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) holds
(fD (f,h)) . x = ((2 * x) * h) + (h ^2)

proof end;

theorem :: DIFF_3:46

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) holds
(bD (f,h)) . x = h * ((2 * x) - h)

proof end;

theorem :: DIFF_3:47

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = x ^2 ) holds
(cD (f,h)) . x = (2 * h) * x

proof end;

:: f.x=k/(x^2)

theorem :: DIFF_3:48

for k, x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) & x0 <> x1 & x0 <> 0 & x1 <> 0 holds
[!f,x0,x1!] = - ((k / (x0 * x1)) * ((1 / x0) + (1 / x1)))

proof end;

theorem :: DIFF_3:49

for k, x0, x1, x2 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 & x0,x1,x2 are_mutually_distinct holds
[!f,x0,x1,x2!] = (k / ((x0 * x1) * x2)) * (((1 / x0) + (1 / x1)) + (1 / x2))

proof end;

theorem :: DIFF_3:50

for h, k, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) & x <> 0 & x + h <> 0 holds
(fD (f,h)) . x = (((- k) * h) * ((2 * x) + h)) / (((x ^2) + (h * x)) ^2)

proof end;

theorem :: DIFF_3:51

for h, k, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) & x <> 0 & x - h <> 0 holds
(bD (f,h)) . x = (((- k) * h) * ((2 * x) - h)) / (((x ^2) - (x * h)) ^2)

proof end;

theorem :: DIFF_3:52

for h, k, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = k / (x ^2) ) & x + (h / 2) <> 0 & x - (h / 2) <> 0 holds
(cD (f,h)) . x = (- (((2 * h) * k) * x)) / (((x ^2) - ((h / 2) ^2)) ^2)

proof end;

:: f.x=(sin x)^3

theorem :: DIFF_3:53

for x0, x1 being Real holds [!((sin (#) sin) (#) sin),x0,x1!] = ((1 / 2) * (((3 * (cos ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) - ((cos ((3 * (x0 + x1)) / 2)) * (sin ((3 * (x0 - x1)) / 2))))) / (x0 - x1)

proof end;

theorem :: DIFF_3:54

for h, x being Real holds (fD (((sin (#) sin) (#) sin),h)) . x = (1 / 2) * (((3 * (cos (((2 * x) + h) / 2))) * (sin (h / 2))) - ((cos ((3 * ((2 * x) + h)) / 2)) * (sin ((3 * h) / 2))))

proof end;

theorem :: DIFF_3:55

for h, x being Real holds (bD (((sin (#) sin) (#) sin),h)) . x = (1 / 2) * (((3 * (cos (((2 * x) - h) / 2))) * (sin (h / 2))) - ((cos ((3 * ((2 * x) - h)) / 2)) * (sin ((3 * h) / 2))))

proof end;

theorem :: DIFF_3:56

for h, x being Real holds (cD (((sin (#) sin) (#) sin),h)) . x = (1 / 2) * (((3 * (cos x)) * (sin (h / 2))) - ((cos (3 * x)) * (sin ((3 * h) / 2))))

proof end;

:: f.x=(cos x)^3

theorem :: DIFF_3:57

for x0, x1 being Real holds [!((cos (#) cos) (#) cos),x0,x1!] = - (((1 / 2) * (((3 * (sin ((x0 + x1) / 2))) * (sin ((x0 - x1) / 2))) + ((sin (((3 * x0) + (3 * x1)) / 2)) * (sin (((3 * x0) - (3 * x1)) / 2))))) / (x0 - x1))

proof end;

theorem :: DIFF_3:58

for h, x being Real holds (fD (((cos (#) cos) (#) cos),h)) . x = - ((1 / 2) * (((3 * (sin (((2 * x) + h) / 2))) * (sin (h / 2))) + ((sin ((3 * ((2 * x) + h)) / 2)) * (sin ((3 * h) / 2)))))

proof end;

theorem :: DIFF_3:59

for h, x being Real holds (bD (((cos (#) cos) (#) cos),h)) . x = - ((1 / 2) * (((3 * (sin (((2 * x) - h) / 2))) * (sin (h / 2))) + ((sin ((3 * ((2 * x) - h)) / 2)) * (sin ((3 * h) / 2)))))

proof end;

theorem :: DIFF_3:60

for h, x being Real holds (cD (((cos (#) cos) (#) cos),h)) . x = - ((1 / 2) * (((3 * (sin x)) * (sin (h / 2))) + ((sin (3 * x)) * (sin ((3 * h) / 2)))))

proof end;

:: f.x=1/sin(x)

theorem :: DIFF_3:61

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) & sin x0 <> 0 & sin x1 <> 0 holds
[!f,x0,x1!] = - (((2 * ((sin x1) - (sin x0))) / ((cos (x0 + x1)) - (cos (x0 - x1)))) / (x0 - x1))

proof end;

theorem :: DIFF_3:62

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) & sin x <> 0 & sin (x + h) <> 0 holds
(fD (f,h)) . x = - ((2 * ((sin x) - (sin (x + h)))) / ((cos ((2 * x) + h)) - (cos h)))

proof end;

theorem :: DIFF_3:63

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) & sin x <> 0 & sin (x - h) <> 0 holds
(bD (f,h)) . x = ((- 2) * ((sin (x - h)) - (sin x))) / ((cos ((2 * x) - h)) - (cos h))

proof end;

theorem :: DIFF_3:64

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (sin x) ) & sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = - ((2 * ((sin (x - (h / 2))) - (sin (x + (h / 2))))) / ((cos (2 * x)) - (cos h)))

proof end;

:: f.x=1/cos(x)

theorem :: DIFF_3:65

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (cos x) ) & x0 <> x1 & cos x0 <> 0 & cos x1 <> 0 holds
[!f,x0,x1!] = ((2 * ((cos x1) - (cos x0))) / ((cos (x0 + x1)) + (cos (x0 - x1)))) / (x0 - x1)

proof end;

theorem :: DIFF_3:66

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (cos x) ) & cos x <> 0 & cos (x + h) <> 0 holds
(fD (f,h)) . x = (2 * ((cos x) - (cos (x + h)))) / ((cos ((2 * x) + h)) + (cos h))

proof end;

theorem :: DIFF_3:67

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (cos x) ) & cos x <> 0 & cos (x - h) <> 0 holds
(bD (f,h)) . x = (2 * ((cos (x - h)) - (cos x))) / ((cos ((2 * x) - h)) + (cos h))

proof end;

theorem :: DIFF_3:68

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / (cos x) ) & cos (x + (h / 2)) <> 0 & cos (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = (2 * ((cos (x - (h / 2))) - (cos (x + (h / 2))))) / ((cos (2 * x)) + (cos h))

proof end;

:: f.x=1/(sin(x))^2

theorem :: DIFF_3:69

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) & x0 <> x1 & sin x0 <> 0 & sin x1 <> 0 holds
[!f,x0,x1!] = ((((16 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) * (cos ((x1 - x0) / 2))) * (sin ((x1 + x0) / 2))) / ((((cos (x0 + x1)) - (cos (x0 - x1))) ^2) * (x0 - x1))

proof end;

theorem :: DIFF_3:70

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) & sin x <> 0 & sin (x + h) <> 0 holds
(fD (f,h)) . x = ((((16 * (cos (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin (((2 * x) + h) / 2))) / (((cos ((2 * x) + h)) - (cos h)) ^2)

proof end;

theorem :: DIFF_3:71

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) & sin x <> 0 & sin (x - h) <> 0 holds
(bD (f,h)) . x = ((((16 * (cos (((2 * x) - h) / 2))) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin (((2 * x) - h) / 2))) / (((cos ((2 * x) - h)) - (cos h)) ^2)

proof end;

theorem :: DIFF_3:72

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((sin x) ^2) ) & sin (x + (h / 2)) <> 0 & sin (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = ((((16 * (cos x)) * (sin ((- h) / 2))) * (cos ((- h) / 2))) * (sin x)) / (((cos (2 * x)) - (cos h)) ^2)

proof end;

:: f.x=1/(cos(x)^2)

theorem :: DIFF_3:73

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) & x0 <> x1 & cos x0 <> 0 & cos x1 <> 0 holds
[!f,x0,x1!] = ((((((- 16) * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) * (cos ((x1 + x0) / 2))) * (cos ((x1 - x0) / 2))) / (((cos (x0 + x1)) + (cos (x0 - x1))) ^2)) / (x0 - x1)

proof end;

theorem :: DIFF_3:74

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) & cos x <> 0 & cos (x + h) <> 0 holds
(fD (f,h)) . x = (((((- 16) * (sin (((2 * x) + h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) + h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) + h)) + (cos h)) ^2)

proof end;

theorem :: DIFF_3:75

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) & cos x <> 0 & cos (x - h) <> 0 holds
(bD (f,h)) . x = (((((- 16) * (sin (((2 * x) - h) / 2))) * (sin ((- h) / 2))) * (cos (((2 * x) - h) / 2))) * (cos ((- h) / 2))) / (((cos ((2 * x) - h)) + (cos h)) ^2)

proof end;

theorem :: DIFF_3:76

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = 1 / ((cos x) ^2) ) & cos (x + (h / 2)) <> 0 & cos (x - (h / 2)) <> 0 holds
(cD (f,h)) . x = (((((- 16) * (sin x)) * (sin ((- h) / 2))) * (cos x)) * (cos ((- h) / 2))) / (((cos (2 * x)) + (cos h)) ^2)

proof end;

:: f.x=tan(x)*sin(x)

theorem :: DIFF_3:77

for x0, x1 being Real st x0 in dom tan & x1 in dom tan holds
[!(tan (#) sin),x0,x1!] = ((((1 / (cos x0)) - (cos x0)) - (1 / (cos x1))) + (cos x1)) / (x0 - x1)

proof end;

theorem :: DIFF_3:78

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) sin) . x ) & x in dom tan & x + h in dom tan holds
(fD (f,h)) . x = (((1 / (cos (x + h))) - (cos (x + h))) - (1 / (cos x))) + (cos x)

proof end;

theorem :: DIFF_3:79

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) sin) . x ) & x in dom tan & x - h in dom tan holds
(bD (f,h)) . x = (((1 / (cos x)) - (cos x)) - (1 / (cos (x - h)))) + (cos (x - h))

proof end;

theorem :: DIFF_3:80

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) sin) . x ) & x + (h / 2) in dom tan & x - (h / 2) in dom tan holds
(cD (f,h)) . x = (((1 / (cos (x + (h / 2)))) - (cos (x + (h / 2)))) - (1 / (cos (x - (h / 2))))) + (cos (x - (h / 2)))

proof end;

:: f.x=tan(x)*cos(x)

theorem :: DIFF_3:81

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) cos) . x ) & x0 in dom tan & x1 in dom tan holds
[!f,x0,x1!] = ((sin x0) - (sin x1)) / (x0 - x1)

proof end;

theorem :: DIFF_3:82

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) cos) . x ) & x in dom tan & x + h in dom tan holds
(fD (f,h)) . x = (sin (x + h)) - (sin x)

proof end;

theorem :: DIFF_3:83

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) cos) . x ) & x in dom tan & x - h in dom tan holds
(bD (f,h)) . x = (sin x) - (sin (x - h))

proof end;

theorem :: DIFF_3:84

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) cos) . x ) & x + (h / 2) in dom tan & x - (h / 2) in dom tan holds
(cD (f,h)) . x = (sin (x + (h / 2))) - (sin (x - (h / 2)))

proof end;

:: f.x=cot(x)*cos(x)

theorem :: DIFF_3:85

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) & x0 in dom cot & x1 in dom cot holds
[!f,x0,x1!] = ((((1 / (sin x0)) - (sin x0)) - (1 / (sin x1))) + (sin x1)) / (x0 - x1)

proof end;

theorem :: DIFF_3:86

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) & x in dom cot & x + h in dom cot holds
(fD (f,h)) . x = (((1 / (sin (x + h))) - (sin (x + h))) - (1 / (sin x))) + (sin x)

proof end;

theorem :: DIFF_3:87

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) & x in dom cot & x - h in dom cot holds
(bD (f,h)) . x = (((1 / (sin x)) - (sin x)) - (1 / (sin (x - h)))) + (sin (x - h))

proof end;

theorem :: DIFF_3:88

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) cos) . x ) & x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD (f,h)) . x = (((1 / (sin (x + (h / 2)))) - (sin (x + (h / 2)))) - (1 / (sin (x - (h / 2))))) + (sin (x - (h / 2)))

proof end;

:: f.x=cot(x)*sin(x)

theorem :: DIFF_3:89

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) sin) . x ) & x0 in dom cot & x1 in dom cot holds
[!f,x0,x1!] = ((cos x0) - (cos x1)) / (x0 - x1)

proof end;

theorem :: DIFF_3:90

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) sin) . x ) & x in dom cot & x + h in dom cot holds
(fD (f,h)) . x = (cos (x + h)) - (cos x)

proof end;

theorem :: DIFF_3:91

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) sin) . x ) & x in dom cot & x - h in dom cot holds
(bD (f,h)) . x = (cos x) - (cos (x - h))

proof end;

theorem :: DIFF_3:92

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (cot (#) sin) . x ) & x + (h / 2) in dom cot & x - (h / 2) in dom cot holds
(cD (f,h)) . x = (cos (x + (h / 2))) - (cos (x - (h / 2)))

proof end;

:: f.x=(tan(x))^2

theorem :: DIFF_3:93

for x0, x1 being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) tan) . x ) & x0 in dom tan & x1 in dom tan holds
[!f,x0,x1!] = (((cos x1) ^2) - ((cos x0) ^2)) / ((((cos x0) * (cos x1)) ^2) * (x0 - x1))

proof end;

theorem :: DIFF_3:94

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) tan) . x ) & x in dom tan & x + h in dom tan holds
(fD (f,h)) . x = - (((1 / 2) * ((cos (2 * (x + h))) - (cos (2 * x)))) / (((cos (x + h)) * (cos x)) ^2))

proof end;

theorem :: DIFF_3:95

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) tan) . x ) & x in dom tan & x - h in dom tan holds
(bD (f,h)) . x = - (((1 / 2) * ((cos (2 * x)) - (cos (2 * (h - x))))) / (((cos x) * (cos (x - h))) ^2))

proof end;

theorem :: DIFF_3:96

for h, x being Real
for f being Function of REAL,REAL st ( for x being Real holds f . x = (tan (#) tan) . x ) & x + (h / 2) in dom tan & x - (h / 2) in dom tan holds
(cD (f,h)) . x = - (((1 / 2) * ((cos (h + (2 * x))) - (cos (h - (2 * x))))) / (((cos (x + (h / 2))) * (cos (x - (h / 2)))) ^2))

proof end;