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

begin

theorem Th4: :: 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 Th9: :: 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 r, h, 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 r, h, 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 r1, r2, h, 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 r, h, 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 r, h, 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 r1, r2, h, 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 Th18: :: 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 m, n 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 r, h, 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 r, h, 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 r1, r2, h, 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 Th23: :: 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 m, n 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 x, h 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 x, h being Real
for f being Function of REAL ,REAL holds [!f,(x - h),x!] = ((bD f,h) . x) / h

proof end;

theorem Th29: :: DIFF_3:22

for x, h 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 Th30: :: DIFF_3:23

for x, h 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 Th32: :: 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 Th38: :: 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_different 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 Th42: :: 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;

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_different & 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_different & 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 x, h 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 x, h 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 x, h 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;

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

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

proof end;

theorem :: DIFF_3:50

for k, x, h 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 k, x, h 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 k, x, h 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;

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;

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;

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 x, h 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 x, h 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 x, h 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;

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 x, h 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 x, h 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 x, h 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;

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 x, h 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 x, h 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 x, h 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;

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 x, h 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 x, h 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 x, h 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;

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 x, h 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 x, h 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 x, h 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;

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 x, h 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 x, h 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 x, h 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;

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 x, h 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 x, h 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 x, h 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;

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 x, h 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 x, h 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 x, h 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;

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 x, h 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 x, h 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 x, h 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;