let f be PartFunc of COMPLEX,COMPLEX; :: thesis: for x0 being Complex
for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Complex_Sequence
for c being constant Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let x0 be Complex; :: thesis: for N being Neighbourhood of x0 st f is_differentiable_in x0 & N c= dom f holds
for h being non-zero 0 -convergent Complex_Sequence
for c being constant Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let N be Neighbourhood of x0; :: thesis: ( f is_differentiable_in x0 & N c= dom f implies for h being non-zero 0 -convergent Complex_Sequence
for c being constant Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
assume that
A1: f is_differentiable_in x0 and
A2: N c= dom f ; :: thesis: for h being non-zero 0 -convergent Complex_Sequence
for c being constant Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
consider N1 being Neighbourhood of x0 such that
N1 c= dom f and
A3: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Complex st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1;
consider N2 being Neighbourhood of x0 such that
A4: N2 c= N and
A5: N2 c= N1 by Lm1;
A6: N2 c= dom f by A2, A4;
let h be non-zero 0 -convergent Complex_Sequence; :: thesis: for c being constant Complex_Sequence st rng c = {x0} & rng (h + c) c= N holds
( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
let c be constant Complex_Sequence; :: thesis: ( rng c = {x0} & rng (h + c) c= N implies ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) ) )
assume that
A7: rng c = {x0} and
A8: rng (h + c) c= N ; :: thesis: ( (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent & diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) )
consider g being Real such that
A9: 0 < g and
A10: { y where y is Complex : |.(y - x0).| < g } c= N2 by Def5;
|.(x0 - x0).| = 0 by COMPLEX1:44;
then x0 in { y where y is Complex : |.(y - x0).| < g } by A9;
then A11: x0 in N2 by A10;
A12: rng c c= dom f
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng c or y in dom f )
assume y in rng c ; :: thesis: y in dom f
then y = x0 by A7, TARSKI:def 1;
then y in N by A4, A11;
hence y in dom f by A2; :: thesis: verum
end;
ex n being Nat st
( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
proof
x0 in rng c by A7, TARSKI:def 1;
then A13: lim c = x0 by CFCONT_1:27;
A14: c is convergent by CFCONT_1:26;
then A15: h + c is convergent ;
lim h = 0 by Def1;
then lim (h + c) = 0 + x0 by A14, A13, COMSEQ_2:14
.= x0 ;
then consider n being Nat such that
A16: for m being Nat st n <= m holds
|.(((h + c) . m) - x0).| < g by A9, A15, COMSEQ_2:def 6;
take n ; :: thesis: ( rng (c ^\ n) c= N2 & rng ((h + c) ^\ n) c= N2 )
A17: rng (c ^\ n) = {x0} by A7, VALUED_0:26;
thus rng (c ^\ n) c= N2 by A11, A17, TARSKI:def 1; :: thesis: rng ((h + c) ^\ n) c= N2
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng ((h + c) ^\ n) or y in N2 )
assume y in rng ((h + c) ^\ n) ; :: thesis: y in N2
then consider m being Element of NAT such that
A18: y = ((h + c) ^\ n) . m by FUNCT_2:113;
reconsider y1 = y as Complex by A18;
n + 0 <= n + m by XREAL_1:7;
then |.(((h + c) . (n + m)) - x0).| < g by A16;
then |.((((h + c) ^\ n) . m) - x0).| < g by NAT_1:def 3;
then y1 in { z where z is Complex : |.(z - x0).| < g } by A18;
hence y in N2 by A10; :: thesis: verum
end;
then consider n being Nat such that
rng (c ^\ n) c= N2 and
A19: rng ((h + c) ^\ n) c= N2 ;
consider L being C_LinearFunc, R being C_RestFunc such that
A20: for x being Complex st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A3;
A21: rng (c ^\ n) c= dom f
proof
let y be object ; :: according to TARSKI:def 3 :: thesis: ( not y in rng (c ^\ n) or y in dom f )
assume A22: y in rng (c ^\ n) ; :: thesis: y in dom f
rng (c ^\ n) = rng c by VALUED_0:26;
then y = x0 by A7, A22, TARSKI:def 1;
then y in N by A4, A11;
hence y in dom f by A2; :: thesis: verum
end;
A23: ( ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent & lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L /. 1r )
proof
deffunc H1( Nat) -> set = (L /. 1r) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);
consider s1 being Complex_Sequence such that
A24: for k being Nat holds s1 . k = H1(k) from COMSEQ_1:sch 1();
A25: now :: thesis: for r being Real st 0 < r holds
ex n1 being Nat st
for k being Nat st n1 <= k holds
|.((s1 . k) - (L /. 1r)).| < r
A26: ( ((h ^\ n) ") (#) (R /* (h ^\ n)) is convergent & lim (((h ^\ n) ") (#) (R /* (h ^\ n))) = 0 ) by Def3;
let r be Real; :: thesis: ( 0 < r implies ex n1 being Nat st
for k being Nat st n1 <= k holds
|.((s1 . k) - (L /. 1r)).| < r )
assume 0 < r ; :: thesis: ex n1 being Nat st
for k being Nat st n1 <= k holds
|.((s1 . k) - (L /. 1r)).| < r
then consider m being Nat such that
A27: for k being Nat st m <= k holds
|.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0c).| < r by A26, COMSEQ_2:def 6;
take n1 = m; :: thesis: for k being Nat st n1 <= k holds
|.((s1 . k) - (L /. 1r)).| < r
let k be Nat; :: thesis: ( n1 <= k implies |.((s1 . k) - (L /. 1r)).| < r )
assume A28: n1 <= k ; :: thesis: |.((s1 . k) - (L /. 1r)).| < r
|.((s1 . k) - (L /. 1r)).| = |.(((L /. 1r) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L /. 1r)).| by A24
.= |.(((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0c).| ;
hence |.((s1 . k) - (L /. 1r)).| < r by A27, A28; :: thesis: verum
end;
consider x being Complex such that
A29: for b1 being Complex holds L /. b1 = x * b1 by Def4;
A30: L /. 1r = x * 1r by A29
.= x ;
now :: thesis: for m being Element of NAT holds (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m
let m be Element of NAT ; :: thesis: (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = s1 . m
A31: (h ^\ n) . m <> 0c by COMSEQ_1:4;
thus (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) . m = (((L /* (h ^\ n)) + (R /* (h ^\ n))) . m) * (((h ^\ n) ") . m) by VALUED_1:5
.= (((L /* (h ^\ n)) . m) + ((R /* (h ^\ n)) . m)) * (((h ^\ n) ") . m) by VALUED_1:1
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) . m) * (((h ^\ n) ") . m))
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) ") . m)) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:5
.= (((L /* (h ^\ n)) . m) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by VALUED_1:10
.= ((L /. ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by FUNCT_2:115
.= ((x * ((h ^\ n) . m)) * (((h ^\ n) . m) ")) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A29
.= (x * (((h ^\ n) . m) * (((h ^\ n) . m) "))) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m)
.= (x * 1r) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . m) by A31, XCMPLX_0:def 7
.= s1 . m by A24, A30 ; :: thesis: verum
end;
then A32: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = s1 ;
hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A25; :: thesis: lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L /. 1r
hence lim (((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ")) = L /. 1r by A32, A25, COMSEQ_2:def 6; :: thesis: verum
end;
A33: for k being Nat holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
proof
let k be Nat; :: thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
A34: k + n in NAT by ORDINAL1:def 12;
A35: k in NAT by ORDINAL1:def 12;
then ((h + c) ^\ n) . k in rng ((h + c) ^\ n) by FUNCT_2:112;
then A36: ((h + c) ^\ n) . k in N2 by A19;
( (c ^\ n) . k in rng (c ^\ n) & rng (c ^\ n) = rng c ) by FUNCT_2:112, VALUED_0:26, A35;
then A37: (c ^\ n) . k = x0 by A7, TARSKI:def 1;
(((h + c) ^\ n) . k) - ((c ^\ n) . k) = ((h + c) . (k + n)) - ((c ^\ n) . k) by NAT_1:def 3
.= ((h . (k + n)) + (c . (k + n))) - ((c ^\ n) . k) by VALUED_1:1, A34
.= (((h ^\ n) . k) + (c . (k + n))) - ((c ^\ n) . k) by NAT_1:def 3
.= (((h ^\ n) . k) + ((c ^\ n) . k)) - ((c ^\ n) . k) by NAT_1:def 3
.= (h ^\ n) . k ;
hence (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A20, A5, A36, A37; :: thesis: verum
end;
A38: rng (h + c) c= dom f by A8, A2;
A39: rng ((h + c) ^\ n) c= dom f by A19, A4, A2;
now :: thesis: for k being Element of NAT holds ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
let k be Element of NAT ; :: thesis: ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k
thus ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) . k = ((f /* ((h + c) ^\ n)) . k) - ((f /* (c ^\ n)) . k) by CFCONT_1:1
.= (f /. (((h + c) ^\ n) . k)) - ((f /* (c ^\ n)) . k) by A39, FUNCT_2:109
.= (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) by A21, FUNCT_2:109
.= (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k)) by A33
.= ((L /* (h ^\ n)) . k) + (R /. ((h ^\ n) . k)) by FUNCT_2:115
.= ((L /* (h ^\ n)) . k) + ((R /* (h ^\ n)) . k) by FUNCT_2:115
.= ((L /* (h ^\ n)) + (R /* (h ^\ n))) . k by VALUED_1:1 ; :: thesis: verum
end;
then A40: ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") = ((f /* ((h + c) ^\ n)) - (f /* (c ^\ n))) (#) ((h ^\ n) ") by FUNCT_2:def 7
.= (((f /* (h + c)) ^\ n) - (f /* (c ^\ n))) (#) ((h ^\ n) ") by A38, VALUED_0:27
.= (((f /* (h + c)) ^\ n) - ((f /* c) ^\ n)) (#) ((h ^\ n) ") by A12, VALUED_0:27
.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ^\ n) ") by Th19
.= (((f /* (h + c)) - (f /* c)) ^\ n) (#) ((h ") ^\ n) by Th20
.= (((f /* (h + c)) - (f /* c)) (#) (h ")) ^\ n by Th21 ;
then A41: L /. 1r = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A23, CFCONT_1:23;
thus (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A23, A40, CFCONT_1:22; :: thesis: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
for x being Complex st x in N2 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A20, A5;
hence diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c))) by A1, A6, A41, Def7; :: thesis: verum