let x0 be Real; for f being PartFunc of REAL,REAL st f is_differentiable_in x0 holds
for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f holds
( ((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h)))) = diff (f,x0) )
let f be PartFunc of REAL,REAL; ( f is_differentiable_in x0 implies for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f holds
( ((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h)))) = diff (f,x0) ) )
assume A1:
f is_differentiable_in x0
; for h being non-zero 0 -convergent Real_Sequence
for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f holds
( ((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h)))) = diff (f,x0) )
let h be non-zero 0 -convergent Real_Sequence; for c being V8() Real_Sequence st rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f holds
( ((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h)))) = diff (f,x0) )
let c be V8() Real_Sequence; ( rng c = {x0} & rng (h + c) c= dom f & rng ((- h) + c) c= dom f implies ( ((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h)))) = diff (f,x0) ) )
assume that
A2:
rng c = {x0}
and
A3:
rng (h + c) c= dom f
and
A4:
rng ((- h) + c) c= dom f
; ( ((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h)))) = diff (f,x0) )
set fm = ((- h) ") (#) ((f /* ((- h) + c)) - (f /* c));
lim (- h) = - (lim h)
by SEQ_2:10;
then A5:
- h is 0 -convergent
;
A6:
lim (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c))) = diff (f,x0)
by A1, A2, A4, Th12, A5;
set fp = (h ") (#) ((f /* (h + c)) - (f /* c));
A7:
diff (f,x0) = diff (f,x0)
;
then A8:
((- h) ") (#) ((f /* ((- h) + c)) - (f /* c)) is convergent
by A1, A2, A4, Th12, A5;
A9:
(h ") (#) ((f /* (h + c)) - (f /* c)) is convergent
by A1, A2, A3, A7, Th12;
then A10:
((h ") (#) ((f /* (h + c)) - (f /* c))) + (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c))) is convergent
by A8;
A12: (2 ") (#) (((h ") (#) ((f /* (h + c)) - (f /* c))) + (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c)))) =
(2 ") (#) (((h ") (#) ((f /* (c + h)) - (f /* c))) + (((- 1) (#) (h ")) (#) ((f /* (c + (- h))) - (f /* c))))
by SEQ_1:47
.=
(2 ") (#) (((h ") (#) ((f /* (c + h)) - (f /* c))) + ((- 1) (#) ((h ") (#) ((f /* (c + (- h))) - (f /* c)))))
by SEQ_1:18
.=
(2 ") (#) (((h ") (#) ((f /* (c + h)) - (f /* c))) + ((h ") (#) ((- 1) (#) ((f /* (c + (- h))) - (f /* c)))))
by SEQ_1:19
.=
(2 ") (#) ((h ") (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c)))))
by SEQ_1:16
.=
((2 ") (#) (h ")) (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c))))
by SEQ_1:18
.=
((2 (#) h) ") (#) (((f /* (c + h)) - (f /* c)) + ((- 1) (#) ((f /* (c + (- h))) - (f /* c))))
by SEQ_1:46
.=
((2 (#) h) ") (#) ((f /* (c + h)) - ((f /* c) - (- ((f /* (c + (- h))) - (f /* c)))))
by SEQ_1:30
.=
((2 (#) h) ") (#) ((f /* (c + h)) - ((f /* (c + (- h))) - ((f /* c) - (f /* c))))
by SEQ_1:30
.=
((2 (#) h) ") (#) (((f /* (c + h)) - (f /* (c - h))) + ((f /* c) - (f /* c)))
by SEQ_1:30
;
lim ((h ") (#) ((f /* (h + c)) - (f /* c))) = diff (f,x0)
by A1, A2, A3, Th12;
then lim (((h ") (#) ((f /* (h + c)) - (f /* c))) + (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c)))) =
(1 * (diff (f,x0))) + (diff (f,x0))
by A9, A8, A6, SEQ_2:6
.=
2 * (diff (f,x0))
;
then A13: lim ((2 ") (#) (((h ") (#) ((f /* (h + c)) - (f /* c))) + (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c))))) =
(2 ") * (2 * (diff (f,x0)))
by A10, SEQ_2:8
.=
diff (f,x0)
;
(2 ") (#) (((h ") (#) ((f /* (h + c)) - (f /* c))) + (((- h) ") (#) ((f /* ((- h) + c)) - (f /* c)))) is convergent
by A10;
hence
( ((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h))) is convergent & lim (((2 (#) h) ") (#) ((f /* (c + h)) - (f /* (c - h)))) = diff (f,x0) )
by A13, A12, A11, FUNCT_2:63; verum