:: Difference and Difference Quotient -- Part {II}
:: by Bo Li , Yanping Zhuang and Xiquan Liang
::
:: Received October 25, 2007
:: Copyright (c) 2007-2021 Association of Mizar Users

theorem Th1: :: DIFF_2:1

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

proof end;

theorem :: DIFF_2:2

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

proof end;

theorem Th3: :: DIFF_2:3

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

proof end;

theorem :: DIFF_2:4

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

proof end;

theorem Th5: :: DIFF_2:5

for r, x0, x1, x2 being Real
for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2!] = r * [!f,x0,x1,x2!]

proof end;

theorem Th6: :: DIFF_2:6

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

proof end;

theorem :: DIFF_2:7

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

proof end;

theorem Th8: :: DIFF_2:8

for r, x0, x1, x2, x3 being Real
for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3!] = r * [!f,x0,x1,x2,x3!]

proof end;

theorem Th9: :: DIFF_2:9

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

proof end;

theorem :: DIFF_2:10

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

proof end;

definition

let f be real-valued Function;
let x0, x1, x2, x3, x4 be Real;

func [!f,x0,x1,x2,x3,x4!] -> Real equals :: DIFF_2:def 1
([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4);

correctness
coherence
([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4) is Real;
;

end;

:: deftheorem defines [! DIFF_2:def 1 :
for f being real-valued Function
for x0, x1, x2, x3, x4 being Real holds [!f,x0,x1,x2,x3,x4!] = ([!f,x0,x1,x2,x3!] - [!f,x1,x2,x3,x4!]) / (x0 - x4);

theorem Th11: :: DIFF_2:11

for r, x0, x1, x2, x3, x4 being Real
for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4!] = r * [!f,x0,x1,x2,x3,x4!]

proof end;

theorem Th12: :: DIFF_2:12

for x0, x1, x2, x3, x4 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4!] = [!f1,x0,x1,x2,x3,x4!] + [!f2,x0,x1,x2,x3,x4!]

proof end;

theorem :: DIFF_2:13

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

proof end;

definition

let f be real-valued Function;
let x0, x1, x2, x3, x4, x5 be Real;

func [!f,x0,x1,x2,x3,x4,x5!] -> Real equals :: DIFF_2:def 2
([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5);

correctness
coherence
([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5) is Real;
;

end;

:: deftheorem defines [! DIFF_2:def 2 :
for f being real-valued Function
for x0, x1, x2, x3, x4, x5 being Real holds [!f,x0,x1,x2,x3,x4,x5!] = ([!f,x0,x1,x2,x3,x4!] - [!f,x1,x2,x3,x4,x5!]) / (x0 - x5);

theorem Th14: :: DIFF_2:14

for r, x0, x1, x2, x3, x4, x5 being Real
for f being Function of REAL,REAL holds [!(r (#) f),x0,x1,x2,x3,x4,x5!] = r * [!f,x0,x1,x2,x3,x4,x5!]

proof end;

theorem Th15: :: DIFF_2:15

for x0, x1, x2, x3, x4, x5 being Real
for f1, f2 being Function of REAL,REAL holds [!(f1 + f2),x0,x1,x2,x3,x4,x5!] = [!f1,x0,x1,x2,x3,x4,x5!] + [!f2,x0,x1,x2,x3,x4,x5!]

proof end;

theorem :: DIFF_2:16

for r1, r2, x0, x1, x2, x3, x4, x5 being Real
for f1, f2 being Function of REAL,REAL holds [!((r1 (#) f1) + (r2 (#) f2)),x0,x1,x2,x3,x4,x5!] = (r1 * [!f1,x0,x1,x2,x3,x4,x5!]) + (r2 * [!f2,x0,x1,x2,x3,x4,x5!])

proof end;

theorem :: DIFF_2:17

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) / ((x0 - x1) * (x0 - x2))) + ((f . x1) / ((x1 - x0) * (x1 - x2)))) + ((f . x2) / ((x2 - x0) * (x2 - x1)))

proof end;

theorem :: DIFF_2:18

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

proof end;

theorem :: DIFF_2:19

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

proof end;

theorem :: DIFF_2:20

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

proof end;

:: f.x=a*x+b

theorem Th21: :: DIFF_2:21

for x0, x1, a, b being Real st x0 <> x1 holds
[!(AffineMap (a,b)),x0,x1!] = a

proof end;

theorem Th22: :: DIFF_2:22

for x0, x1, x2, a, b being Real st x0,x1,x2 are_mutually_distinct holds
[!(AffineMap (a,b)),x0,x1,x2!] = 0

proof end;

theorem :: DIFF_2:23

for x0, x1, x2, x3, a, b being Real st x0,x1,x2,x3 are_mutually_distinct holds
[!(AffineMap (a,b)),x0,x1,x2,x3!] = 0

proof end;

theorem :: DIFF_2:24

for h, a, b, x being Real holds (fD ((AffineMap (a,b)),h)) . x = a * h

proof end;

theorem :: DIFF_2:25

for h, a, b, x being Real holds (bD ((AffineMap (a,b)),h)) . x = a * h

proof end;

theorem :: DIFF_2:26

for h, a, b, x being Real holds (cD ((AffineMap (a,b)),h)) . x = a * h

proof end;

:: f.x=a*x^2+b*x+c

theorem Th27: :: DIFF_2:27

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

proof end;

theorem Th28: :: DIFF_2:28

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

proof end;

theorem Th29: :: DIFF_2:29

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

proof end;

theorem :: DIFF_2:30

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

proof end;

theorem :: DIFF_2:31

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

proof end;

theorem :: DIFF_2:32

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

proof end;

theorem :: DIFF_2:33

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

proof end;

:: f.x=k/x

theorem Th34: :: DIFF_2:34

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

proof end;

theorem Th35: :: DIFF_2:35

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

proof end;

theorem Th36: :: DIFF_2:36

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

proof end;

theorem :: DIFF_2:37

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

proof end;

theorem :: DIFF_2:38

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

theorem :: DIFF_2:39

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

theorem :: DIFF_2:40

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

proof end;

:: f.x = sin(x)

theorem :: DIFF_2:41

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

proof end;

theorem :: DIFF_2:42

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

proof end;

theorem :: DIFF_2:43

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

proof end;

theorem :: DIFF_2:44

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

proof end;

:: f.x = cos(x)

theorem :: DIFF_2:45

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

proof end;

theorem :: DIFF_2:46

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

proof end;

theorem :: DIFF_2:47

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

proof end;

theorem :: DIFF_2:48

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

proof end;

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

theorem :: DIFF_2:49

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

proof end;

theorem :: DIFF_2:50

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

proof end;

theorem :: DIFF_2:51

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

proof end;

theorem :: DIFF_2:52

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

proof end;

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

theorem :: DIFF_2:53

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

proof end;

theorem :: DIFF_2:54

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

proof end;

theorem :: DIFF_2:55

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

proof end;

theorem :: DIFF_2:56

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

proof end;

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

theorem :: DIFF_2:57

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

proof end;

theorem :: DIFF_2:58

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

proof end;

theorem :: DIFF_2:59

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

proof end;

theorem :: DIFF_2:60

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

proof end;

:: f.x = (sin(x))^2*cos(x)

theorem :: DIFF_2:61

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

proof end;

theorem :: DIFF_2:62

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

proof end;

theorem :: DIFF_2:63

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

proof end;

theorem :: DIFF_2:64

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

proof end;

:: f.x = sin(x)*(cos(x))^2

theorem :: DIFF_2:65

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

proof end;

theorem :: DIFF_2:66

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

proof end;

theorem :: DIFF_2:67

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

proof end;

theorem :: DIFF_2:68

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

proof end;

:: f.x = tan(x)

theorem :: DIFF_2:69

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

proof end;

:: f.x = cot(x)

theorem :: DIFF_2:70

for x0, x1 being Real st x0 in dom cot & x1 in dom cot holds
[!cot,x0,x1!] = - ((sin (x0 - x1)) / (((sin x0) * (sin x1)) * (x0 - x1)))

proof end;

:: f.x = cosec(x)

theorem :: DIFF_2:71

for x0, x1 being Real st x0 in dom cosec & x1 in dom cosec holds
[!cosec,x0,x1!] = ((2 * (cos ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((sin x1) * (sin x0)) * (x0 - x1))

proof end;

:: f.x = sec(x)

theorem :: DIFF_2:72

for x0, x1 being Real st x0 in dom sec & x1 in dom sec holds
[!sec,x0,x1!] = - (((2 * (sin ((x1 + x0) / 2))) * (sin ((x1 - x0) / 2))) / (((cos x1) * (cos x0)) * (x0 - x1)))

proof end;