:: CFDIFF_1 semantic presentation
begin
definition
let x be real number ;
let IT be Complex_Sequence;
attrIT is x -convergent means :Def1: :: CFDIFF_1:def 1
( IT is convergent & lim IT = x );
end;
:: deftheorem Def1 defines -convergent CFDIFF_1:def_1_:_
for x being real number
for IT being Complex_Sequence holds
( IT is x -convergent iff ( IT is convergent & lim IT = x ) );
theorem :: CFDIFF_1:1
for rs being Real_Sequence
for cs being Complex_Sequence st rs = cs & rs is convergent holds
cs is convergent ;
definition
let r be real number ;
func InvShift r -> Complex_Sequence means :Def2: :: CFDIFF_1:def 2
for n being Element of NAT holds it . n = 1 / (n + r);
existence
ex b1 being Complex_Sequence st
for n being Element of NAT holds b1 . n = 1 / (n + r)
proof
deffunc H1( real number ) -> Element of REAL = 1 / ($1 + r);
ex seq being Complex_Sequence st
for n being Element of NAT holds seq . n = H1(n) from COMSEQ_1:sch_1();
hence ex b1 being Complex_Sequence st
for n being Element of NAT holds b1 . n = 1 / (n + r) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being Complex_Sequence st ( for n being Element of NAT holds b1 . n = 1 / (n + r) ) & ( for n being Element of NAT holds b2 . n = 1 / (n + r) ) holds
b1 = b2
proof
let f, g be Complex_Sequence; ::_thesis: ( ( for n being Element of NAT holds f . n = 1 / (n + r) ) & ( for n being Element of NAT holds g . n = 1 / (n + r) ) implies f = g )
assume that
A1: for n being Element of NAT holds f . n = 1 / (n + r) and
A2: for n being Element of NAT holds g . n = 1 / (n + r) ; ::_thesis: f = g
let n be Element of NAT ; :: according to FUNCT_2:def_8 ::_thesis: f . n = g . n
thus f . n = 1 / (n + r) by A1
.= g . n by A2 ; ::_thesis: verum
end;
end;
:: deftheorem Def2 defines InvShift CFDIFF_1:def_2_:_
for r being real number
for b2 being Complex_Sequence holds
( b2 = InvShift r iff for n being Element of NAT holds b2 . n = 1 / (n + r) );
theorem Th2: :: CFDIFF_1:2
for r being real number st 0 < r holds
InvShift r is convergent
proof
let r be real number ; ::_thesis: ( 0 < r implies InvShift r is convergent )
assume A1: 0 < r ; ::_thesis: InvShift r is convergent
set seq = InvShift r;
take g = 0c ; :: according to COMSEQ_2:def_5 ::_thesis: for b1 being Element of REAL holds
( b1 <= 0 or ex b2 being Element of NAT st
for b3 being Element of NAT holds
( not b2 <= b3 or not b1 <= |.(((InvShift r) . b3) - g).| ) )
let p be Real; ::_thesis: ( p <= 0 or ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.(((InvShift r) . b2) - g).| ) )
assume A2: 0 < p ; ::_thesis: ex b1 being Element of NAT st
for b2 being Element of NAT holds
( not b1 <= b2 or not p <= |.(((InvShift r) . b2) - g).| )
consider k1 being Element of NAT such that
A3: p " < k1 by SEQ_4:3;
take n = k1; ::_thesis: for b1 being Element of NAT holds
( not n <= b1 or not p <= |.(((InvShift r) . b1) - g).| )
let m be Element of NAT ; ::_thesis: ( not n <= m or not p <= |.(((InvShift r) . m) - g).| )
assume n <= m ; ::_thesis: not p <= |.(((InvShift r) . m) - g).|
then n + r <= m + r by XREAL_1:6;
then A4: 1 / (m + r) <= 1 / (n + r) by A1, XREAL_1:118;
A5: (InvShift r) . m = 1 / (m + r) by Def2;
(p ") + 0 < k1 + r by A1, A3, XREAL_1:8;
then 1 / (k1 + r) < 1 / (p ") by A2, XREAL_1:76;
then 1 / (m + r) < p by A4, XXREAL_0:2;
hence abs (((InvShift r) . m) - g) < p by A1, A5, ABSVALUE:def_1; ::_thesis: verum
end;
registration
let r be real positive number ;
cluster InvShift r -> convergent ;
coherence
InvShift r is convergent by Th2;
end;
theorem Th3: :: CFDIFF_1:3
for r being real number st 0 < r holds
lim (InvShift r) = 0
proof
let r be real number ; ::_thesis: ( 0 < r implies lim (InvShift r) = 0 )
set seq = InvShift r;
assume A1: 0 < r ; ::_thesis: lim (InvShift r) = 0
now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
abs_(((InvShift_r)_._m)_-_0c)_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((InvShift r) . m) - 0c) < p )
assume A2: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
abs (((InvShift r) . m) - 0c) < p
consider k1 being Element of NAT such that
A3: p " < k1 by SEQ_4:3;
take n = k1; ::_thesis: for m being Element of NAT st n <= m holds
abs (((InvShift r) . m) - 0c) < p
let m be Element of NAT ; ::_thesis: ( n <= m implies abs (((InvShift r) . m) - 0c) < p )
assume n <= m ; ::_thesis: abs (((InvShift r) . m) - 0c) < p
then n + r <= m + r by XREAL_1:6;
then A4: 1 / (m + r) <= 1 / (n + r) by A1, XREAL_1:118;
A5: (InvShift r) . m = 1 / (m + r) by Def2;
(p ") + 0 < k1 + r by A1, A3, XREAL_1:8;
then 1 / (k1 + r) < 1 / (p ") by A2, XREAL_1:76;
then 1 / (m + r) < p by A4, XXREAL_0:2;
hence abs (((InvShift r) . m) - 0c) < p by A1, A5, ABSVALUE:def_1; ::_thesis: verum
end;
hence lim (InvShift r) = 0 by A1, COMSEQ_2:def_6; ::_thesis: verum
end;
registration
let r be real positive number ;
cluster InvShift r -> non-zero 0 -convergent ;
coherence
( InvShift r is non-empty & InvShift r is 0 -convergent )
proof
set s = InvShift r;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(InvShift_r)_._n_<>_0c
let n be Element of NAT ; ::_thesis: (InvShift r) . n <> 0c
1 / (n + r) <> 0 ;
hence (InvShift r) . n <> 0c by Def2; ::_thesis: verum
end;
hence InvShift r is non-zero by COMSEQ_1:4; ::_thesis: InvShift r is 0 -convergent
lim (InvShift r) = 0 by Th3;
hence InvShift r is 0 -convergent by Def1; ::_thesis: verum
end;
end;
registration
clusterV1() non-zero V4( NAT ) V5( COMPLEX ) Function-like V11() total quasi_total complex-valued 0 -convergent for Element of K19(K20(NAT,COMPLEX));
existence
ex b1 being Complex_Sequence st
( b1 is 0 -convergent & b1 is non-zero )
proof
take InvShift 1 ; ::_thesis: ( InvShift 1 is 0 -convergent & InvShift 1 is non-zero )
thus ( InvShift 1 is 0 -convergent & InvShift 1 is non-zero ) ; ::_thesis: verum
end;
end;
registration
cluster non-zero Function-like quasi_total 0 -convergent -> convergent for Element of K19(K20(NAT,COMPLEX));
coherence
for b1 being Complex_Sequence st b1 is 0 -convergent & b1 is non-zero holds
b1 is convergent by Def1;
end;
reconsider cs = NAT --> 0c as Complex_Sequence ;
registration
clusterV1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued for Element of K19(K20(NAT,COMPLEX));
existence
ex b1 being Complex_Sequence st b1 is constant
proof
take cs ; ::_thesis: cs is constant
thus cs is constant ; ::_thesis: verum
end;
end;
theorem :: CFDIFF_1:4
for seq being Complex_Sequence holds
( seq is constant iff for n, m being Element of NAT holds seq . n = seq . m )
proof
let seq be Complex_Sequence; ::_thesis: ( seq is constant iff for n, m being Element of NAT holds seq . n = seq . m )
thus ( seq is constant implies for n, m being Element of NAT holds seq . n = seq . m ) by VALUED_0:23; ::_thesis: ( ( for n, m being Element of NAT holds seq . n = seq . m ) implies seq is constant )
assume that
A1: for n, m being Element of NAT holds seq . n = seq . m and
A2: not seq is constant ; ::_thesis: contradiction
now__::_thesis:_for_n_being_Nat_holds_contradiction
let n be Nat; ::_thesis: contradiction
consider n1 being Nat such that
A3: seq . n1 <> seq . n by A2, VALUED_0:def_18;
( n1 in NAT & n in NAT ) by ORDINAL1:def_12;
hence contradiction by A1, A3; ::_thesis: verum
end;
hence contradiction ; ::_thesis: verum
end;
theorem :: CFDIFF_1:5
for seq being Complex_Sequence
for Nseq being V37() sequence of NAT
for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n)
proof
let seq be Complex_Sequence; ::_thesis: for Nseq being V37() sequence of NAT
for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n)
let Nseq be V37() sequence of NAT; ::_thesis: for n being Element of NAT holds (seq * Nseq) . n = seq . (Nseq . n)
let n be Element of NAT ; ::_thesis: (seq * Nseq) . n = seq . (Nseq . n)
dom (seq * Nseq) = NAT by FUNCT_2:def_1;
hence (seq * Nseq) . n = seq . (Nseq . n) by FUNCT_1:12; ::_thesis: verum
end;
definition
let IT be PartFunc of COMPLEX,COMPLEX;
attrIT is RestFunc-like means :Def3: :: CFDIFF_1:def 3
for h being non-zero 0 -convergent Complex_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 );
end;
:: deftheorem Def3 defines RestFunc-like CFDIFF_1:def_3_:_
for IT being PartFunc of COMPLEX,COMPLEX holds
( IT is RestFunc-like iff for h being non-zero 0 -convergent Complex_Sequence holds
( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 ) );
reconsider cf = COMPLEX --> 0c as Function of COMPLEX,COMPLEX ;
registration
clusterV1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued RestFunc-like for Element of K19(K20(COMPLEX,COMPLEX));
existence
ex b1 being PartFunc of COMPLEX,COMPLEX st
( b1 is total & b1 is RestFunc-like )
proof
take f = cf; ::_thesis: ( f is total & f is RestFunc-like )
thus f is total ; ::_thesis: f is RestFunc-like
let h be non-zero 0 -convergent Complex_Sequence; :: according to CFDIFF_1:def_3 ::_thesis: ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0 )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(f_/*_h))_._n_=_0c
let n be Nat; ::_thesis: ((h ") (#) (f /* h)) . n = 0c
dom f = COMPLEX by PARTFUN1:def_2;
then A1: ( n in NAT & rng h c= dom f ) by ORDINAL1:def_12;
thus ((h ") (#) (f /* h)) . n = ((h ") . n) * ((f /* h) . n) by VALUED_1:5
.= ((h ") . n) * (f /. (h . n)) by A1, FUNCT_2:108
.= ((h ") . n) * 0c by FUNCOP_1:7
.= 0c ; ::_thesis: verum
end;
then ( (h ") (#) (f /* h) is constant & ((h ") (#) (f /* h)) . 0 = 0c ) by VALUED_0:def_18;
hence ( (h ") (#) (f /* h) is convergent & lim ((h ") (#) (f /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum
end;
end;
definition
mode C_RestFunc is total RestFunc-like PartFunc of COMPLEX,COMPLEX;
end;
definition
let IT be PartFunc of COMPLEX,COMPLEX;
attrIT is linear means :Def4: :: CFDIFF_1:def 4
ex a being Element of COMPLEX st
for z being Element of COMPLEX holds IT /. z = a * z;
end;
:: deftheorem Def4 defines linear CFDIFF_1:def_4_:_
for IT being PartFunc of COMPLEX,COMPLEX holds
( IT is linear iff ex a being Element of COMPLEX st
for z being Element of COMPLEX holds IT /. z = a * z );
registration
clusterV1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued linear for Element of K19(K20(COMPLEX,COMPLEX));
existence
ex b1 being PartFunc of COMPLEX,COMPLEX st
( b1 is total & b1 is linear )
proof
deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = 1r * c1;
defpred S1[ set ] means c1 in COMPLEX ;
consider f being PartFunc of COMPLEX,COMPLEX such that
A1: ( ( for a being Element of COMPLEX holds
( a in dom f iff S1[a] ) ) & ( for a being Element of COMPLEX st a in dom f holds
f . a = H1(a) ) ) from SEQ_1:sch_3();
take f ; ::_thesis: ( f is total & f is linear )
for y being set st y in COMPLEX holds
y in dom f by A1;
then COMPLEX c= dom f by TARSKI:def_3;
then A2: dom f = COMPLEX by XBOOLE_0:def_10;
hence f is total by PARTFUN1:def_2; ::_thesis: f is linear
take 1r ; :: according to CFDIFF_1:def_4 ::_thesis: for z being Element of COMPLEX holds f /. z = 1r * z
let z be Element of COMPLEX ; ::_thesis: f /. z = 1r * z
thus f /. z = f . z by A2, PARTFUN1:def_6
.= 1r * z by A1 ; ::_thesis: verum
end;
end;
definition
mode C_LinearFunc is total linear PartFunc of COMPLEX,COMPLEX;
end;
registration
let L1, L2 be C_LinearFunc;
clusterL1 + L2 -> total linear for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 + L2 holds
( b1 is total & b1 is linear )
proof
consider a2 being Element of COMPLEX such that
A1: for z being Element of COMPLEX holds L2 /. z = a2 * z by Def4;
consider a1 being Element of COMPLEX such that
A2: for z being Element of COMPLEX holds L1 /. z = a1 * z by Def4;
now__::_thesis:_for_z_being_Element_of_COMPLEX_holds_(L1_+_L2)_/._z_=_(a1_+_a2)_*_z
let z be Element of COMPLEX ; ::_thesis: (L1 + L2) /. z = (a1 + a2) * z
thus (L1 + L2) /. z = (L1 /. z) + (L2 /. z) by CFUNCT_1:64
.= (a1 * z) + (L2 /. z) by A2
.= (a1 * z) + (a2 * z) by A1
.= (a1 + a2) * z ; ::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 + L2 holds
( b1 is total & b1 is linear ) by Def4; ::_thesis: verum
end;
clusterL1 - L2 -> total linear for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 - L2 holds
( b1 is total & b1 is linear )
proof
consider a2 being Element of COMPLEX such that
A3: for z being Element of COMPLEX holds L2 /. z = a2 * z by Def4;
consider a1 being Element of COMPLEX such that
A4: for z being Element of COMPLEX holds L1 /. z = a1 * z by Def4;
now__::_thesis:_for_z_being_Element_of_COMPLEX_holds_(L1_-_L2)_/._z_=_(a1_-_a2)_*_z
let z be Element of COMPLEX ; ::_thesis: (L1 - L2) /. z = (a1 - a2) * z
thus (L1 - L2) /. z = (L1 /. z) - (L2 /. z) by CFUNCT_1:64
.= (a1 * z) - (L2 /. z) by A4
.= (a1 * z) - (a2 * z) by A3
.= (a1 - a2) * z ; ::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 - L2 holds
( b1 is total & b1 is linear ) by Def4; ::_thesis: verum
end;
end;
registration
let a be Element of COMPLEX ;
let L be C_LinearFunc;
clustera (#) L -> total linear for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) L holds
( b1 is total & b1 is linear )
proof
consider b being Element of COMPLEX such that
A1: for z being Element of COMPLEX holds L /. z = b * z by Def4;
now__::_thesis:_for_z_being_Element_of_COMPLEX_holds_(a_(#)_L)_/._z_=_(a_*_b)_*_z
let z be Element of COMPLEX ; ::_thesis: (a (#) L) /. z = (a * b) * z
thus (a (#) L) /. z = a * (L /. z) by CFUNCT_1:65
.= a * (b * z) by A1
.= (a * b) * z ; ::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) L holds
( b1 is total & b1 is linear ) by Def4; ::_thesis: verum
end;
end;
registration
let R1, R2 be C_RestFunc;
clusterR1 + R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 + R2 holds
( b1 is total & b1 is RestFunc-like )
proof
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_((R1_+_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_+_R2)_/*_h))_=_0_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((R1 + R2) /* h) is convergent & lim ((h ") (#) ((R1 + R2) /* h)) = 0 )
A1: (h ") (#) ((R1 + R2) /* h) = (h ") (#) ((R1 /* h) + (R2 /* h)) by CFCONT_1:14
.= ((h ") (#) (R1 /* h)) + ((h ") (#) (R2 /* h)) by COMSEQ_1:10 ;
A2: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def3;
hence (h ") (#) ((R1 + R2) /* h) is convergent by A1; ::_thesis: lim ((h ") (#) ((R1 + R2) /* h)) = 0
A3: lim ((h ") (#) (R1 /* h)) = 0 by Def3;
thus lim ((h ") (#) ((R1 + R2) /* h)) = (lim ((h ") (#) (R1 /* h))) + (lim ((h ") (#) (R2 /* h))) by A2, A1, COMSEQ_2:14
.= 0 by A3, Def3 ; ::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 + R2 holds
( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum
end;
clusterR1 - R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 - R2 holds
( b1 is total & b1 is RestFunc-like )
proof
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_((R1_-_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_-_R2)_/*_h))_=_0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((R1 - R2) /* h) is convergent & lim ((h ") (#) ((R1 - R2) /* h)) = 0c )
A4: (h ") (#) ((R1 - R2) /* h) = (h ") (#) ((R1 /* h) - (R2 /* h)) by CFCONT_1:14
.= ((h ") (#) (R1 /* h)) - ((h ") (#) (R2 /* h)) by COMSEQ_1:15 ;
A5: ( (h ") (#) (R1 /* h) is convergent & (h ") (#) (R2 /* h) is convergent ) by Def3;
hence (h ") (#) ((R1 - R2) /* h) is convergent by A4; ::_thesis: lim ((h ") (#) ((R1 - R2) /* h)) = 0c
( lim ((h ") (#) (R1 /* h)) = 0c & lim ((h ") (#) (R2 /* h)) = 0c ) by Def3;
hence lim ((h ") (#) ((R1 - R2) /* h)) = 0c - 0c by A5, A4, COMSEQ_2:26
.= 0c ;
::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 - R2 holds
( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum
end;
clusterR1 (#) R2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 (#) R2 holds
( b1 is total & b1 is RestFunc-like )
proof
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_((R1_(#)_R2)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R1_(#)_R2)_/*_h))_=_0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((R1 (#) R2) /* h) is convergent & lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c )
for seq being Complex_Sequence st seq is non-zero holds
seq " is non-zero
proof
let seq be Complex_Sequence; ::_thesis: ( seq is non-zero implies seq " is non-zero )
assume that
A6: seq is non-zero and
A7: not seq " is non-zero ; ::_thesis: contradiction
consider n1 being Element of NAT such that
A8: (seq ") . n1 = 0c by A7, COMSEQ_1:4;
(seq . n1) " = (seq ") . n1 by VALUED_1:10;
hence contradiction by A6, A8, COMSEQ_1:4, XCMPLX_1:202; ::_thesis: verum
end;
then A9: h " is non-zero ;
A10: (h ") (#) ((R1 (#) R2) /* h) = ((R1 /* h) (#) (R2 /* h)) /" h by CFCONT_1:14
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) /" (h (#) (h ")) by A9, COMSEQ_1:37
.= (((R1 /* h) (#) (R2 /* h)) (#) (h ")) (#) (((h ") ") (#) (h ")) by COMSEQ_1:30
.= (h (#) (h ")) (#) ((R1 /* h) (#) ((h ") (#) (R2 /* h))) by COMSEQ_1:8
.= ((h (#) (h ")) (#) (R1 /* h)) (#) ((h ") (#) (R2 /* h)) by COMSEQ_1:8
.= (h (#) ((h ") (#) (R1 /* h))) (#) ((h ") (#) (R2 /* h)) by COMSEQ_1:8 ;
A11: (h ") (#) (R1 /* h) is convergent by Def3;
then A12: h (#) ((h ") (#) (R1 /* h)) is convergent ;
( lim ((h ") (#) (R1 /* h)) = 0c & lim h = 0c ) by Def1, Def3;
then A13: lim (h (#) ((h ") (#) (R1 /* h))) = 0 * 0 by A11, COMSEQ_2:30
.= 0c ;
A14: (h ") (#) (R2 /* h) is convergent by Def3;
hence (h ") (#) ((R1 (#) R2) /* h) is convergent by A12, A10; ::_thesis: lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c
lim ((h ") (#) (R2 /* h)) = 0c by Def3;
hence lim ((h ") (#) ((R1 (#) R2) /* h)) = 0c * 0c by A14, A12, A13, A10, COMSEQ_2:30
.= 0c ;
::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R1 (#) R2 holds
( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum
end;
end;
registration
let a be Element of COMPLEX ;
let R be C_RestFunc;
clustera (#) R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) R holds
( b1 is total & b1 is RestFunc-like )
proof
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_((a_(#)_R)_/*_h)_is_convergent_&_lim_((h_")_(#)_((a_(#)_R)_/*_h))_=_0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((a (#) R) /* h) is convergent & lim ((h ") (#) ((a (#) R) /* h)) = 0c )
A1: (h ") (#) ((a (#) R) /* h) = (h ") (#) (a (#) (R /* h)) by CFCONT_1:15
.= a (#) ((h ") (#) (R /* h)) by COMSEQ_1:13 ;
A2: (h ") (#) (R /* h) is convergent by Def3;
hence (h ") (#) ((a (#) R) /* h) is convergent by A1; ::_thesis: lim ((h ") (#) ((a (#) R) /* h)) = 0c
lim ((h ") (#) (R /* h)) = 0c by Def3;
hence lim ((h ") (#) ((a (#) R) /* h)) = a * 0c by A2, A1, COMSEQ_2:18
.= 0c ;
::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = a (#) R holds
( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum
end;
end;
registration
let L1, L2 be C_LinearFunc;
clusterL1 (#) L2 -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 (#) L2 holds
( b1 is total & b1 is RestFunc-like )
proof
reconsider LL = L1 (#) L2 as PartFunc of COMPLEX,COMPLEX ;
LL is RestFunc-like
proof
let h be non-zero 0 -convergent Complex_Sequence; :: according to CFDIFF_1:def_3 ::_thesis: ( (h ") (#) (LL /* h) is convergent & lim ((h ") (#) (LL /* h)) = 0 )
consider b1 being Element of COMPLEX such that
A1: for z being Element of COMPLEX holds L1 /. z = b1 * z by Def4;
consider b2 being Element of COMPLEX such that
A2: for z being Element of COMPLEX holds L2 /. z = b2 * z by Def4;
A3: now__::_thesis:_for_n_being_Element_of_NAT_holds_((h_")_(#)_((L1_(#)_L2)_/*_h))_._n_=_((b1_*_b2)_(#)_h)_._n
let n be Element of NAT ; ::_thesis: ((h ") (#) ((L1 (#) L2) /* h)) . n = ((b1 * b2) (#) h) . n
A4: h . n <> 0c by COMSEQ_1:4;
thus ((h ") (#) ((L1 (#) L2) /* h)) . n = ((h ") . n) * (((L1 (#) L2) /* h) . n) by VALUED_1:5
.= ((h ") . n) * ((L1 (#) L2) /. (h . n)) by FUNCT_2:115
.= ((h ") . n) * ((L1 /. (h . n)) * (L2 /. (h . n))) by CFUNCT_1:64
.= (((h ") . n) * (L1 /. (h . n))) * (L2 /. (h . n))
.= (((h . n) ") * (L1 /. (h . n))) * (L2 /. (h . n)) by VALUED_1:10
.= (((h . n) ") * ((h . n) * b1)) * (L2 /. (h . n)) by A1
.= ((((h . n) ") * (h . n)) * b1) * (L2 /. (h . n))
.= (1r * b1) * (L2 /. (h . n)) by A4, XCMPLX_0:def_7
.= b1 * (b2 * (h . n)) by A2
.= (b1 * b2) * (h . n)
.= ((b1 * b2) (#) h) . n by VALUED_1:6 ; ::_thesis: verum
end;
then A5: (h ") (#) ((L1 (#) L2) /* h) = (b1 * b2) (#) h by FUNCT_2:63;
thus (h ") (#) (LL /* h) is convergent by A3, FUNCT_2:63; ::_thesis: lim ((h ") (#) (LL /* h)) = 0
lim h = 0c by Def1;
hence lim ((h ") (#) (LL /* h)) = (b1 * b2) * 0c by A5, COMSEQ_2:18
.= 0c ;
::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L1 (#) L2 holds
( b1 is total & b1 is RestFunc-like ) ; ::_thesis: verum
end;
end;
registration
let R be C_RestFunc;
let L be C_LinearFunc;
clusterR (#) L -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R (#) L holds
( b1 is total & b1 is RestFunc-like )
proof
consider b1 being Element of COMPLEX such that
A1: for z being Element of COMPLEX holds L /. z = b1 * z by Def4;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_((R_(#)_L)_/*_h)_is_convergent_&_lim_((h_")_(#)_((R_(#)_L)_/*_h))_=_0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) ((R (#) L) /* h) is convergent & lim ((h ") (#) ((R (#) L) /* h)) = 0c )
A2: (h ") (#) ((R (#) L) /* h) = (h ") (#) ((R /* h) (#) (L /* h)) by CFCONT_1:14
.= ((h ") (#) (R /* h)) (#) (L /* h) by COMSEQ_1:8 ;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(L_/*_h)_._n_=_(b1_(#)_h)_._n
let n be Element of NAT ; ::_thesis: (L /* h) . n = (b1 (#) h) . n
thus (L /* h) . n = L /. (h . n) by FUNCT_2:115
.= b1 * (h . n) by A1
.= (b1 (#) h) . n by VALUED_1:6 ; ::_thesis: verum
end;
then A3: L /* h = b1 (#) h by FUNCT_2:63;
lim h = 0c by Def1;
then A4: lim (L /* h) = b1 * 0c by A3, COMSEQ_2:18
.= 0c ;
A5: (h ") (#) (R /* h) is convergent by Def3;
hence (h ") (#) ((R (#) L) /* h) is convergent by A2, A3; ::_thesis: lim ((h ") (#) ((R (#) L) /* h)) = 0c
lim ((h ") (#) (R /* h)) = 0c by Def3;
hence lim ((h ") (#) ((R (#) L) /* h)) = 0c * 0c by A2, A3, A4, A5, COMSEQ_2:30
.= 0c ;
::_thesis: verum
end;
hence for b1 being PartFunc of COMPLEX,COMPLEX st b1 = R (#) L holds
( b1 is total & b1 is RestFunc-like ) by Def3; ::_thesis: verum
end;
clusterL (#) R -> total RestFunc-like for PartFunc of COMPLEX,COMPLEX;
coherence
for b1 being PartFunc of COMPLEX,COMPLEX st b1 = L (#) R holds
( b1 is total & b1 is RestFunc-like ) ;
end;
definition
let z0 be Complex;
mode Neighbourhood of z0 -> Subset of COMPLEX means :Def5: :: CFDIFF_1:def 5
ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= it );
existence
ex b1 being Subset of COMPLEX ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b1 )
proof
set N = { y where y is Complex : |.(y - z0).| < 1 } ;
take { y where y is Complex : |.(y - z0).| < 1 } ; ::_thesis: ( { y where y is Complex : |.(y - z0).| < 1 } is Subset of COMPLEX & ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= { y where y is Complex : |.(y - z0).| < 1 } ) )
{ y where y is Complex : |.(y - z0).| < 1 } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < 1 } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z0).| < 1 } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z0).| < 1 ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
hence ( { y where y is Complex : |.(y - z0).| < 1 } is Subset of COMPLEX & ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= { y where y is Complex : |.(y - z0).| < 1 } ) ) ; ::_thesis: verum
end;
end;
:: deftheorem Def5 defines Neighbourhood CFDIFF_1:def_5_:_
for z0 being Complex
for b2 being Subset of COMPLEX holds
( b2 is Neighbourhood of z0 iff ex g being Real st
( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b2 ) );
theorem Th6: :: CFDIFF_1:6
for z0 being Element of COMPLEX
for g being real number st 0 < g holds
{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0
proof
let z0 be Element of COMPLEX ; ::_thesis: for g being real number st 0 < g holds
{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0
let g be real number ; ::_thesis: ( 0 < g implies { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 )
assume A1: g > 0 ; ::_thesis: { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0
set N = { y where y is Complex : |.(y - z0).| < g } ;
A2: { y where y is Complex : |.(y - z0).| < g } c= COMPLEX
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < g } or z in COMPLEX )
assume z in { y where y is Complex : |.(y - z0).| < g } ; ::_thesis: z in COMPLEX
then ex y being Complex st
( z = y & |.(y - z0).| < g ) ;
hence z in COMPLEX by XCMPLX_0:def_2; ::_thesis: verum
end;
g in REAL by XREAL_0:def_1;
hence { y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A1, A2, Def5; ::_thesis: verum
end;
theorem Th7: :: CFDIFF_1:7
for z0 being Element of COMPLEX
for N being Neighbourhood of z0 holds z0 in N
proof
let z0 be Element of COMPLEX ; ::_thesis: for N being Neighbourhood of z0 holds z0 in N
let N be Neighbourhood of z0; ::_thesis: z0 in N
consider g being Real such that
A1: 0 < g and
A2: { z where z is Complex : |.(z - z0).| < g } c= N by Def5;
|.(z0 - z0).| = 0 by COMPLEX1:44;
then z0 in { z where z is Complex : |.(z - z0).| < g } by A1;
hence z0 in N by A2; ::_thesis: verum
end;
Lm1: for z0 being Complex
for N1, N2 being Neighbourhood of z0 ex N being Neighbourhood of z0 st
( N c= N1 & N c= N2 )
proof
let z0 be Complex; ::_thesis: for N1, N2 being Neighbourhood of z0 ex N being Neighbourhood of z0 st
( N c= N1 & N c= N2 )
A1: z0 in COMPLEX by XCMPLX_0:def_2;
let N1, N2 be Neighbourhood of z0; ::_thesis: ex N being Neighbourhood of z0 st
( N c= N1 & N c= N2 )
consider a1 being Real such that
A2: 0 < a1 and
A3: { y where y is Complex : |.(y - z0).| < a1 } c= N1 by Def5;
consider a2 being Real such that
A4: 0 < a2 and
A5: { y where y is Complex : |.(y - z0).| < a2 } c= N2 by Def5;
set g = min (a1,a2);
take { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; ::_thesis: ( { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Subset of COMPLEX & { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Neighbourhood of z0 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N1 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N2 )
A6: min (a1,a2) <= a2 by XXREAL_0:17;
A7: { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= { y where y is Complex : |.(y - z0).| < a2 }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } or z in { y where y is Complex : |.(y - z0).| < a2 } )
assume z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; ::_thesis: z in { y where y is Complex : |.(y - z0).| < a2 }
then consider y being Complex such that
A8: z = y and
A9: |.(y - z0).| < min (a1,a2) ;
|.(y - z0).| < a2 by A6, A9, XXREAL_0:2;
hence z in { y where y is Complex : |.(y - z0).| < a2 } by A8; ::_thesis: verum
end;
A10: min (a1,a2) <= a1 by XXREAL_0:17;
A11: { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= { y where y is Complex : |.(y - z0).| < a1 }
proof
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } or z in { y where y is Complex : |.(y - z0).| < a1 } )
assume z in { y where y is Complex : |.(y - z0).| < min (a1,a2) } ; ::_thesis: z in { y where y is Complex : |.(y - z0).| < a1 }
then consider y being Complex such that
A12: z = y and
A13: |.(y - z0).| < min (a1,a2) ;
|.(y - z0).| < a1 by A10, A13, XXREAL_0:2;
hence z in { y where y is Complex : |.(y - z0).| < a1 } by A12; ::_thesis: verum
end;
0 < min (a1,a2) by A2, A4, XXREAL_0:15;
hence ( { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Subset of COMPLEX & { y where y is Complex : |.(y - z0).| < min (a1,a2) } is Neighbourhood of z0 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N1 & { y where y is Complex : |.(y - z0).| < min (a1,a2) } c= N2 ) by A1, A3, A5, A11, A7, Th6, XBOOLE_1:1; ::_thesis: verum
end;
definition
let f be PartFunc of COMPLEX,COMPLEX;
let z0 be Complex;
predf is_differentiable_in z0 means :Def6: :: CFDIFF_1:def 6
ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) );
end;
:: deftheorem Def6 defines is_differentiable_in CFDIFF_1:def_6_:_
for f being PartFunc of COMPLEX,COMPLEX
for z0 being Complex holds
( f is_differentiable_in z0 iff ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) );
definition
let f be PartFunc of COMPLEX,COMPLEX;
let z0 be Complex;
assume A1: f is_differentiable_in z0 ;
func diff (f,z0) -> Element of COMPLEX means :Def7: :: CFDIFF_1:def 7
ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( it = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) );
existence
ex b1 being Element of COMPLEX ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( b1 = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) )
proof
consider N being Neighbourhood of z0 such that
A2: N c= dom f and
A3: ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A1, Def6;
consider L being C_LinearFunc, R being C_RestFunc such that
A4: for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A3;
consider a being Element of COMPLEX such that
A5: for d being Element of COMPLEX holds L /. d = a * d by Def4;
take a ; ::_thesis: ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) )
L /. 1r = a * 1r by A5
.= a ;
hence ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) by A2, A4; ::_thesis: verum
end;
uniqueness
for b1, b2 being Element of COMPLEX st ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( b1 = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) & ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( b2 = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) holds
b1 = b2
proof
set s0 = InvShift 2;
let a, b be Element of COMPLEX ; ::_thesis: ( ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) & ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( b = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) implies a = b )
assume that
A6: ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) and
A7: ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( b = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) ; ::_thesis: a = b
consider N being Neighbourhood of z0 such that
N c= dom f and
A8: ex L being C_LinearFunc ex R being C_RestFunc st
( a = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) by A6;
consider L being C_LinearFunc, R being C_RestFunc such that
A9: a = L /. 1r and
A10: for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A8;
consider a1 being Element of COMPLEX such that
A11: for b being Element of COMPLEX holds L /. b = a1 * b by Def4;
consider N1 being Neighbourhood of z0 such that
N1 c= dom f and
A12: ex L being C_LinearFunc ex R being C_RestFunc st
( b = L /. 1r & ( for z being Element of COMPLEX st z in N1 holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) by A7;
consider L1 being C_LinearFunc, R1 being C_RestFunc such that
A13: b = L1 /. 1r and
A14: for z being Element of COMPLEX st z in N1 holds
(f /. z) - (f /. z0) = (L1 /. (z - z0)) + (R1 /. (z - z0)) by A12;
consider b1 being Element of COMPLEX such that
A15: for b being Element of COMPLEX holds L1 /. b = b1 * b by Def4;
reconsider s0 = InvShift 2 as Complex_Sequence ;
consider N0 being Neighbourhood of z0 such that
A16: ( N0 c= N & N0 c= N1 ) by Lm1;
consider g being Real such that
A17: 0 < g and
A18: { y where y is Complex : |.(y - z0).| < g } c= N0 by Def5;
set s1 = g (#) s0;
A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_(g_(#)_s0)_._n_=_g_/_(n_+_2)
let n be Element of NAT ; ::_thesis: (g (#) s0) . n = g / (n + 2)
thus (g (#) s0) . n = g * (s0 . n) by VALUED_1:6
.= g * (1 / (n + 2)) by Def2
.= g / (n + 2) ; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Element_of_NAT_holds_0_<>_(g_(#)_s0)_._n
let n be Element of NAT ; ::_thesis: 0 <> (g (#) s0) . n
(g (#) s0) . n = g / (n + 2) by A19;
hence 0 <> (g (#) s0) . n by A17; ::_thesis: verum
end;
then A20: g (#) s0 is non-zero by COMSEQ_1:4;
lim s0 = 0 by Th3;
then lim (g (#) s0) = g * 0 by COMSEQ_2:18;
then reconsider h = g (#) s0 as non-zero 0 -convergent Complex_Sequence by A20, Def1;
A21: for n being Element of NAT ex x being Complex st
( x in N & x in N1 & h . n = x - z0 )
proof
let n be Element of NAT ; ::_thesis: ex x being Complex st
( x in N & x in N1 & h . n = x - z0 )
reconsider g0 = g / (n + 2) as Complex ;
take x = z0 + g0; ::_thesis: ( x in N & x in N1 & h . n = x - z0 )
0 + 1 < (n + 1) + 1 by XREAL_1:6;
then A22: g / (n + 2) < g / 1 by A17, XREAL_1:76;
|.((z0 + g0) - z0).| = g / (n + 2) by A17, ABSVALUE:def_1;
then x in { y where y is Complex : |.(y - z0).| < g } by A22;
then x in N0 by A18;
hence ( x in N & x in N1 & h . n = x - z0 ) by A16, A19; ::_thesis: verum
end;
A23: a = a1 * 1r by A9, A11;
A24: now__::_thesis:_for_z_being_Complex_st_z_in_N_&_z_in_N1_holds_
(a_*_(z_-_z0))_+_(R_/._(z_-_z0))_=_(b_*_(z_-_z0))_+_(R1_/._(z_-_z0))
let z be Complex; ::_thesis: ( z in N & z in N1 implies (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0)) )
assume that
A25: z in N and
A26: z in N1 ; ::_thesis: (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0))
reconsider t0 = z0, t = z as Element of COMPLEX by XCMPLX_0:def_2;
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) by A10, A25;
then (L /. (z - z0)) + (R /. (z - z0)) = (L1 /. (z - z0)) + (R1 /. (z - z0)) by A14, A26;
then (a1 * (t - t0)) + (R /. (t - t0)) = (L1 /. (t - t0)) + (R1 /. (t - t0)) by A11;
then ((a1 * 1r) * (z - z0)) + (R /. (z - z0)) = ((b1 * 1r) * (z - z0)) + (R1 /. (z - z0)) by A15;
hence (a * (z - z0)) + (R /. (z - z0)) = (b * (z - z0)) + (R1 /. (z - z0)) by A13, A15, A23; ::_thesis: verum
end;
now__::_thesis:_for_n_being_Nat_holds_a_-_b_=_(((h_")_(#)_(R1_/*_h))_+_(-_((h_")_(#)_(R_/*_h))))_._n
dom R1 = COMPLEX by PARTFUN1:def_2;
then A27: rng h c= dom R1 ;
dom R = COMPLEX by PARTFUN1:def_2;
then A28: rng h c= dom R ;
let n be Nat; ::_thesis: a - b = (((h ") (#) (R1 /* h)) + (- ((h ") (#) (R /* h)))) . n
A29: n in NAT by ORDINAL1:def_12;
then A30: h . n <> 0c by COMSEQ_1:4;
ex x being Complex st
( x in N & x in N1 & h . n = x - z0 ) by A21, A29;
then (a * (h . n)) + (R /. (h . n)) = (b * (h . n)) + (R1 /. (h . n)) by A24;
then A31: ((a * (h . n)) / (h . n)) + ((R /. (h . n)) / (h . n)) = ((b * (h . n)) + (R1 /. (h . n))) / (h . n) by XCMPLX_1:62;
A32: (b * (h . n)) / (h . n) = b * ((h . n) / (h . n))
.= b * 1 by A30, XCMPLX_1:60
.= b ;
A33: (R1 /. (h . n)) / (h . n) = (R1 /. (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R1 /* h) . n) * ((h ") . n) by A29, A27, FUNCT_2:108
.= ((h ") (#) (R1 /* h)) . n by VALUED_1:5 ;
A34: (a * (h . n)) / (h . n) = a * ((h . n) / (h . n))
.= a * 1 by A30, XCMPLX_1:60
.= a ;
(R /. (h . n)) / (h . n) = (R /. (h . n)) * ((h ") . n) by VALUED_1:10
.= ((R /* h) . n) * ((h ") . n) by A29, A28, FUNCT_2:109
.= ((h ") (#) (R /* h)) . n by VALUED_1:5 ;
hence a - b = (((h ") (#) (R1 /* h)) . n) + (- (((h ") (#) (R /* h)) . n)) by A31, A34, A32, A33
.= (((h ") (#) (R1 /* h)) . n) + ((- ((h ") (#) (R /* h))) . n) by VALUED_1:8
.= (((h ") (#) (R1 /* h)) + (- ((h ") (#) (R /* h)))) . n by A29, VALUED_1:1 ;
::_thesis: verum
end;
then ( ((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h)) is constant & (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) . 1 = a - b ) by VALUED_0:def_18;
then A35: lim (((h ") (#) (R1 /* h)) - ((h ") (#) (R /* h))) = a - b by CFCONT_1:28;
A36: ( (h ") (#) (R1 /* h) is convergent & lim ((h ") (#) (R1 /* h)) = 0 ) by Def3;
( (h ") (#) (R /* h) is convergent & lim ((h ") (#) (R /* h)) = 0 ) by Def3;
then a - b = 0 - 0 by A35, A36, COMSEQ_2:26;
hence a = b ; ::_thesis: verum
end;
end;
:: deftheorem Def7 defines diff CFDIFF_1:def_7_:_
for f being PartFunc of COMPLEX,COMPLEX
for z0 being Complex st f is_differentiable_in z0 holds
for b3 being Element of COMPLEX holds
( b3 = diff (f,z0) iff ex N being Neighbourhood of z0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
( b3 = L /. 1r & ( for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) );
definition
let f be PartFunc of COMPLEX,COMPLEX;
attrf is differentiable means :Def8: :: CFDIFF_1:def 8
for x being Element of COMPLEX st x in dom f holds
f is_differentiable_in x;
end;
:: deftheorem Def8 defines differentiable CFDIFF_1:def_8_:_
for f being PartFunc of COMPLEX,COMPLEX holds
( f is differentiable iff for x being Element of COMPLEX st x in dom f holds
f is_differentiable_in x );
definition
let f be PartFunc of COMPLEX,COMPLEX;
let X be set ;
predf is_differentiable_on X means :Def9: :: CFDIFF_1:def 9
( X c= dom f & f | X is differentiable );
end;
:: deftheorem Def9 defines is_differentiable_on CFDIFF_1:def_9_:_
for f being PartFunc of COMPLEX,COMPLEX
for X being set holds
( f is_differentiable_on X iff ( X c= dom f & f | X is differentiable ) );
theorem Th8: :: CFDIFF_1:8
for X being set
for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds
X is Subset of COMPLEX
proof
let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds
X is Subset of COMPLEX
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_differentiable_on X implies X is Subset of COMPLEX )
assume f is_differentiable_on X ; ::_thesis: X is Subset of COMPLEX
then X c= dom f by Def9;
hence X is Subset of COMPLEX by XBOOLE_1:1; ::_thesis: verum
end;
definition
let X be Subset of COMPLEX;
attrX is closed means :Def10: :: CFDIFF_1:def 10
for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds
lim s1 in X;
end;
:: deftheorem Def10 defines closed CFDIFF_1:def_10_:_
for X being Subset of COMPLEX holds
( X is closed iff for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds
lim s1 in X );
definition
let X be Subset of COMPLEX;
attrX is open means :Def11: :: CFDIFF_1:def 11
X ` is closed ;
end;
:: deftheorem Def11 defines open CFDIFF_1:def_11_:_
for X being Subset of COMPLEX holds
( X is open iff X ` is closed );
theorem Th9: :: CFDIFF_1:9
for X being Subset of COMPLEX st X is open holds
for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X
proof
let X be Subset of COMPLEX; ::_thesis: ( X is open implies for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X )
assume X is open ; ::_thesis: for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X
then A1: X ` is closed by Def11;
let z0 be Complex; ::_thesis: ( z0 in X implies ex N being Neighbourhood of z0 st N c= X )
assume that
A2: z0 in X and
A3: for N being Neighbourhood of z0 holds not N c= X ; ::_thesis: contradiction
defpred S1[ Element of NAT , Complex] means ( $2 in { y where y is Complex : |.(y - z0).| < 1 / ($1 + 1) } & $2 in X ` );
A4: z0 in COMPLEX by XCMPLX_0:def_2;
now__::_thesis:_for_g_being_Real_st_0_<_g_holds_
ex_s_being_Element_of_COMPLEX_st_
(_s_in__{__y_where_y_is_Complex_:_|.(y_-_z0).|_<_g__}__&_s_in_X_`_)
let g be Real; ::_thesis: ( 0 < g implies ex s being Element of COMPLEX st
( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` ) )
assume A5: 0 < g ; ::_thesis: ex s being Element of COMPLEX st
( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` )
set N = { y where y is Complex : |.(y - z0).| < g } ;
{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0 by A4, A5, Th6;
then not { y where y is Complex : |.(y - z0).| < g } c= X by A3;
then consider x being set such that
A6: x in { y where y is Complex : |.(y - z0).| < g } and
A7: not x in X by TARSKI:def_3;
consider s being Complex such that
A8: x = s and
A9: |.(s - z0).| < g by A6;
reconsider s = s as Element of COMPLEX by XCMPLX_0:def_2;
take s = s; ::_thesis: ( s in { y where y is Complex : |.(y - z0).| < g } & s in X ` )
thus s in { y where y is Complex : |.(y - z0).| < g } by A9; ::_thesis: s in X `
thus s in X ` by A7, A8, XBOOLE_0:def_5; ::_thesis: verum
end;
then A10: for n being Element of NAT ex s being Element of COMPLEX st S1[n,s] ;
consider s1 being Function of NAT,COMPLEX such that
A11: for n being Element of NAT holds S1[n,s1 . n] from FUNCT_2:sch_3(A10);
A12: rng s1 c= X `
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng s1 or y in X ` )
assume y in rng s1 ; ::_thesis: y in X `
then consider y1 being set such that
A13: y1 in dom s1 and
A14: s1 . y1 = y by FUNCT_1:def_3;
reconsider y1 = y1 as Element of NAT by A13;
s1 . y1 in X ` by A11;
hence y in X ` by A14; ::_thesis: verum
end;
A15: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.((s1_._m)_-_z0).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s1 . m) - z0).| < p )
assume A16: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.((s1 . m) - z0).| < p
consider n being Element of NAT such that
A17: p " < n by SEQ_4:3;
take n = n; ::_thesis: for m being Element of NAT st n <= m holds
|.((s1 . m) - z0).| < p
let m be Element of NAT ; ::_thesis: ( n <= m implies |.((s1 . m) - z0).| < p )
assume n <= m ; ::_thesis: |.((s1 . m) - z0).| < p
then n + 1 <= m + 1 by XREAL_1:6;
then A18: 1 / (m + 1) <= 1 / (n + 1) by XREAL_1:118;
s1 . m in { y where y is Complex : |.(y - z0).| < 1 / (m + 1) } by A11;
then ex y being Complex st
( s1 . m = y & |.(y - z0).| < 1 / (m + 1) ) ;
then A19: |.((s1 . m) - z0).| < 1 / (n + 1) by A18, XXREAL_0:2;
(p ") + 0 < n + 1 by A17, XREAL_1:8;
then 1 / (n + 1) < 1 / (p ") by A16, XREAL_1:76;
hence |.((s1 . m) - z0).| < p by A19, XXREAL_0:2; ::_thesis: verum
end;
then A20: s1 is convergent by A4, COMSEQ_2:def_5;
then lim s1 = z0 by A4, A15, COMSEQ_2:def_6;
then z0 in COMPLEX \ X by A20, A12, A1, Def10;
hence contradiction by A2, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: CFDIFF_1:10
for X being Subset of COMPLEX st X is open holds
for z0 being Complex st z0 in X holds
ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X
proof
let X be Subset of COMPLEX; ::_thesis: ( X is open implies for z0 being Complex st z0 in X holds
ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X )
assume A1: X is open ; ::_thesis: for z0 being Complex st z0 in X holds
ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X
let z0 be Complex; ::_thesis: ( z0 in X implies ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X )
assume z0 in X ; ::_thesis: ex g being Real st { y where y is Complex : |.(y - z0).| < g } c= X
then consider N being Neighbourhood of z0 such that
A2: N c= X by A1, Th9;
consider g being Real such that
0 < g and
A3: { y where y is Complex : |.(y - z0).| < g } c= N by Def5;
take g ; ::_thesis: { y where y is Complex : |.(y - z0).| < g } c= X
thus { y where y is Complex : |.(y - z0).| < g } c= X by A2, A3, XBOOLE_1:1; ::_thesis: verum
end;
theorem Th11: :: CFDIFF_1:11
for X being Subset of COMPLEX st ( for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X ) holds
X is open
proof
let X be Subset of COMPLEX; ::_thesis: ( ( for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X ) implies X is open )
assume that
A1: for z0 being Complex st z0 in X holds
ex N being Neighbourhood of z0 st N c= X and
A2: not X is open ; ::_thesis: contradiction
not X ` is closed by A2, Def11;
then consider s1 being Function of NAT,COMPLEX such that
A3: rng s1 c= X ` and
A4: s1 is convergent and
A5: not lim s1 in X ` by Def10;
consider N being Neighbourhood of lim s1 such that
A6: N c= X by A1, A5, SUBSET_1:29;
consider g being Real such that
A7: 0 < g and
A8: { y where y is Complex : |.(y - (lim s1)).| < g } c= N by Def5;
consider n being Element of NAT such that
A9: for m being Element of NAT st n <= m holds
|.((s1 . m) - (lim s1)).| < g by A4, A7, COMSEQ_2:def_6;
n in NAT ;
then n in dom s1 by FUNCT_2:def_1;
then A10: s1 . n in rng s1 by FUNCT_1:def_3;
|.((s1 . n) - (lim s1)).| < g by A9;
then s1 . n in { y where y is Complex : |.(y - (lim s1)).| < g } ;
then s1 . n in N by A8;
hence contradiction by A3, A6, A10, XBOOLE_0:def_5; ::_thesis: verum
end;
theorem :: CFDIFF_1:12
for X being Subset of COMPLEX holds
( X is open iff for x being Complex st x in X holds
ex N being Neighbourhood of x st N c= X ) by Th9, Th11;
theorem Th13: :: CFDIFF_1:13
for X being Subset of COMPLEX
for z0 being Element of COMPLEX
for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds
X is open
proof
let X be Subset of COMPLEX; ::_thesis: for z0 being Element of COMPLEX
for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds
X is open
let z0 be Element of COMPLEX ; ::_thesis: for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| < r } holds
X is open
let r be Element of REAL ; ::_thesis: ( X = { y where y is Complex : |.(y - z0).| < r } implies X is open )
reconsider X0 = X as Subset of COMPLEX ;
assume A1: X = { y where y is Complex : |.(y - z0).| < r } ; ::_thesis: X is open
for x being Complex st x in X0 holds
ex N being Neighbourhood of x st N c= X0
proof
let x be Complex; ::_thesis: ( x in X0 implies ex N being Neighbourhood of x st N c= X0 )
A2: x in COMPLEX by XCMPLX_0:def_2;
reconsider r1 = (r - |.(x - z0).|) / 2 as Real ;
set N = { y where y is Complex : |.(y - x).| < r1 } ;
assume x in X0 ; ::_thesis: ex N being Neighbourhood of x st N c= X0
then ex y being Complex st
( x = y & |.(y - z0).| < r ) by A1;
then A3: r - |.(x - z0).| > 0 by XREAL_1:50;
then reconsider N = { y where y is Complex : |.(y - x).| < r1 } as Neighbourhood of x by A2, Th6;
r1 < r - |.(x - z0).| by A3, XREAL_1:216;
then A4: r1 + |.(x - z0).| < (r - |.(x - z0).|) + |.(x - z0).| by XREAL_1:8;
take N ; ::_thesis: N c= X0
let z be set ; :: according to TARSKI:def_3 ::_thesis: ( not z in N or z in X0 )
assume z in N ; ::_thesis: z in X0
then consider y1 being Complex such that
A5: z = y1 and
A6: |.(y1 - x).| < r1 ;
|.(y1 - x).| + |.(x - z0).| < r1 + |.(x - z0).| by A6, XREAL_1:8;
then ( |.(y1 - z0).| <= |.(y1 - x).| + |.(x - z0).| & |.(y1 - x).| + |.(x - z0).| < r ) by A4, COMPLEX1:63, XXREAL_0:2;
then |.(y1 - z0).| < r by XXREAL_0:2;
hence z in X0 by A1, A5; ::_thesis: verum
end;
hence X is open by Th11; ::_thesis: verum
end;
theorem :: CFDIFF_1:14
for X being Subset of COMPLEX
for z0 being Element of COMPLEX
for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| <= r } holds
X is closed
proof
let X be Subset of COMPLEX; ::_thesis: for z0 being Element of COMPLEX
for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| <= r } holds
X is closed
let z0 be Element of COMPLEX ; ::_thesis: for r being Element of REAL st X = { y where y is Complex : |.(y - z0).| <= r } holds
X is closed
let r be Element of REAL ; ::_thesis: ( X = { y where y is Complex : |.(y - z0).| <= r } implies X is closed )
reconsider X0 = X as Subset of COMPLEX ;
assume A1: X = { y where y is Complex : |.(y - z0).| <= r } ; ::_thesis: X is closed
for s1 being Complex_Sequence st rng s1 c= X0 & s1 is convergent holds
lim s1 in X0
proof
reconsider s4 = NAT --> r as Real_Sequence ;
reconsider s2 = NAT --> z0 as Complex_Sequence ;
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= X0 & s1 is convergent implies lim s1 in X0 )
assume that
A2: rng s1 c= X0 and
A3: s1 is convergent ; ::_thesis: lim s1 in X0
set s3 = s1 - s2;
A4: s2 is convergent by CFCONT_1:26;
then A5: lim (s1 - s2) = (lim s1) - (lim s2) by A3, COMSEQ_2:26;
A6: for n being Element of NAT holds |.(s1 - s2).| . n <= r
proof
let n be Element of NAT ; ::_thesis: |.(s1 - s2).| . n <= r
now__::_thesis:_for_n_being_Element_of_NAT_holds_(s1_-_s2)_._n_=_(s1_._n)_-_z0
let n be Element of NAT ; ::_thesis: (s1 - s2) . n = (s1 . n) - z0
(s1 - s2) . n = (s1 . n) + ((- s2) . n) by VALUED_1:1
.= (s1 . n) - (s2 . n) by VALUED_1:8 ;
hence (s1 - s2) . n = (s1 . n) - z0 by FUNCOP_1:7; ::_thesis: verum
end;
then A7: (s1 - s2) . n = (s1 . n) - z0 ;
dom s1 = NAT by FUNCT_2:def_1;
then s1 . n in rng s1 by FUNCT_1:def_3;
then s1 . n in X0 by A2;
then ex y being Complex st
( y = s1 . n & |.(y - z0).| <= r ) by A1;
hence |.(s1 - s2).| . n <= r by A7, VALUED_1:18; ::_thesis: verum
end;
s1 - s2 is convergent by A3, A4;
then A8: lim |.(s1 - s2).| = |.(lim (s1 - s2)).| by SEQ_2:27;
reconsider s3 = s1 - s2 as convergent Complex_Sequence by A3, A4;
A9: for n being Element of NAT holds |.s3.| . n <= s4 . n
proof
let n be Element of NAT ; ::_thesis: |.s3.| . n <= s4 . n
|.s3.| . n <= r by A6;
hence |.s3.| . n <= s4 . n by FUNCOP_1:7; ::_thesis: verum
end;
A10: for n being Element of NAT holds lim s2 = z0
proof
let n be Element of NAT ; ::_thesis: lim s2 = z0
lim s2 = s2 . n by CFCONT_1:28
.= z0 by FUNCOP_1:7 ;
hence lim s2 = z0 ; ::_thesis: verum
end;
lim s4 = s4 . 0 by SEQ_4:26
.= r by FUNCOP_1:7 ;
then lim |.s3.| <= r by A9, SEQ_2:18;
then |.((lim s1) - z0).| <= r by A10, A5, A8;
hence lim s1 in X0 by A1; ::_thesis: verum
end;
hence X is closed by Def10; ::_thesis: verum
end;
registration
clusterV45() open for Element of K19(COMPLEX);
existence
ex b1 being Subset of COMPLEX st b1 is open
proof
reconsider X = { y where y is Complex : |.(y - 0c).| < 1 } as Subset of COMPLEX by Th6;
X is open by Th13;
hence ex b1 being Subset of COMPLEX st b1 is open ; ::_thesis: verum
end;
end;
theorem Th15: :: CFDIFF_1:15
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f is_differentiable_in x ) ) )
proof
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX holds
( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f is_differentiable_in x ) ) )
let Z be open Subset of COMPLEX; ::_thesis: ( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f is_differentiable_in x ) ) )
thus ( f is_differentiable_on Z implies ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f is_differentiable_in x ) ) ) ::_thesis: ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f is_differentiable_in x ) implies f is_differentiable_on Z )
proof
assume A1: f is_differentiable_on Z ; ::_thesis: ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f is_differentiable_in x ) )
hence A2: Z c= dom f by Def9; ::_thesis: for x being Element of COMPLEX st x in Z holds
f is_differentiable_in x
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
A3: f | Z is differentiable by A1, Def9;
assume A4: x0 in Z ; ::_thesis: f is_differentiable_in x0
then x0 in dom (f | Z) by A2, RELAT_1:57;
then f | Z is_differentiable_in x0 by A3, Def8;
then consider N being Neighbourhood of x0 such that
A5: N c= dom (f | Z) and
A6: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
take N ; :: according to CFDIFF_1:def_6 ::_thesis: ( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0)) )
dom (f | Z) = (dom f) /\ Z by RELAT_1:61;
then dom (f | Z) c= dom f by XBOOLE_1:17;
hence N c= dom f by A5, XBOOLE_1:1; ::_thesis: ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0))
consider L being C_LinearFunc, R being C_RestFunc such that
A7: for x being Element of COMPLEX st x in N holds
((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A6;
take L ; ::_thesis: ex R being C_RestFunc st
for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0))
take R ; ::_thesis: for z being Element of COMPLEX st z in N holds
(f /. z) - (f /. x0) = (L /. (z - x0)) + (R /. (z - x0))
let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A8: x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A7;
then A9: (f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A5, A8, PARTFUN2:15;
x0 in (dom f) /\ Z by A2, A4, XBOOLE_0:def_4;
hence (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A9, PARTFUN2:16; ::_thesis: verum
end;
assume that
A10: Z c= dom f and
A11: for x being Element of COMPLEX st x in Z holds
f is_differentiable_in x ; ::_thesis: f is_differentiable_on Z
thus Z c= dom f by A10; :: according to CFDIFF_1:def_9 ::_thesis: f | Z is differentiable
let x0 be Element of COMPLEX ; :: according to CFDIFF_1:def_8 ::_thesis: ( x0 in dom (f | Z) implies f | Z is_differentiable_in x0 )
assume x0 in dom (f | Z) ; ::_thesis: f | Z is_differentiable_in x0
then A12: x0 in Z by RELAT_1:57;
then consider N1 being Neighbourhood of x0 such that
A13: N1 c= Z by Th9;
f is_differentiable_in x0 by A11, A12;
then consider N being Neighbourhood of x0 such that
A14: N c= dom f and
A15: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
consider N2 being Neighbourhood of x0 such that
A16: N2 c= N1 and
A17: N2 c= N by Lm1;
A18: N2 c= Z by A13, A16, XBOOLE_1:1;
take N2 ; :: according to CFDIFF_1:def_6 ::_thesis: ( N2 c= dom (f | Z) & ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) )
N2 c= dom f by A14, A17, XBOOLE_1:1;
then N2 c= (dom f) /\ Z by A18, XBOOLE_1:19;
hence A19: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
consider L being C_LinearFunc, R being C_RestFunc such that
A20: for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A15;
A21: x0 in N2 by Th7;
take L ; ::_thesis: ex R being C_RestFunc st
for z being Element of COMPLEX st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
take R ; ::_thesis: for z being Element of COMPLEX st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
let x be Element of COMPLEX ; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A22: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A17, A20;
then ((f | Z) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A19, A22, PARTFUN2:15;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A19, A21, PARTFUN2:15; ::_thesis: verum
end;
theorem :: CFDIFF_1:16
for Y being Subset of COMPLEX
for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on Y holds
Y is open
proof
let Y be Subset of COMPLEX; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on Y holds
Y is open
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_differentiable_on Y implies Y is open )
assume A1: f is_differentiable_on Y ; ::_thesis: Y is open
then A2: Y c= dom f by Def9;
now__::_thesis:_for_x0_being_Complex_st_x0_in_Y_holds_
ex_N_being_Neighbourhood_of_x0_st_N_c=_Y
let x0 be Complex; ::_thesis: ( x0 in Y implies ex N being Neighbourhood of x0 st N c= Y )
assume x0 in Y ; ::_thesis: ex N being Neighbourhood of x0 st N c= Y
then A3: x0 in dom (f | Y) by A2, RELAT_1:57;
f | Y is differentiable by A1, Def9;
then f | Y is_differentiable_in x0 by A3, Def8;
then consider N being Neighbourhood of x0 such that
A4: N c= dom (f | Y) and
ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N holds
((f | Y) /. x) - ((f | Y) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
take N = N; ::_thesis: N c= Y
dom (f | Y) = (dom f) /\ Y by RELAT_1:61;
then dom (f | Y) c= Y by XBOOLE_1:17;
hence N c= Y by A4, XBOOLE_1:1; ::_thesis: verum
end;
hence Y is open by Th11; ::_thesis: verum
end;
definition
let f be PartFunc of COMPLEX,COMPLEX;
let X be set ;
assume A1: f is_differentiable_on X ;
funcf `| X -> PartFunc of COMPLEX,COMPLEX means :Def12: :: CFDIFF_1:def 12
( dom it = X & ( for x being Element of COMPLEX st x in X holds
it /. x = diff (f,x) ) );
existence
ex b1 being PartFunc of COMPLEX,COMPLEX st
( dom b1 = X & ( for x being Element of COMPLEX st x in X holds
b1 /. x = diff (f,x) ) )
proof
deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = diff (f,$1);
defpred S1[ set ] means $1 in X;
consider F being PartFunc of COMPLEX,COMPLEX such that
A2: ( ( for x being Element of COMPLEX holds
( x in dom F iff S1[x] ) ) & ( for x being Element of COMPLEX st x in dom F holds
F . x = H1(x) ) ) from SEQ_1:sch_3();
take F ; ::_thesis: ( dom F = X & ( for x being Element of COMPLEX st x in X holds
F /. x = diff (f,x) ) )
now__::_thesis:_for_y_being_set_st_y_in_X_holds_
y_in_dom_F
A3: X is Subset of COMPLEX by A1, Th8;
let y be set ; ::_thesis: ( y in X implies y in dom F )
assume y in X ; ::_thesis: y in dom F
hence y in dom F by A2, A3; ::_thesis: verum
end;
then A4: X c= dom F by TARSKI:def_3;
for y being set st y in dom F holds
y in X by A2;
then dom F c= X by TARSKI:def_3;
hence dom F = X by A4, XBOOLE_0:def_10; ::_thesis: for x being Element of COMPLEX st x in X holds
F /. x = diff (f,x)
now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_X_holds_
F_/._x_=_diff_(f,x)
let x be Element of COMPLEX ; ::_thesis: ( x in X implies F /. x = diff (f,x) )
assume x in X ; ::_thesis: F /. x = diff (f,x)
then A5: x in dom F by A2;
then F . x = diff (f,x) by A2;
hence F /. x = diff (f,x) by A5, PARTFUN1:def_6; ::_thesis: verum
end;
hence for x being Element of COMPLEX st x in X holds
F /. x = diff (f,x) ; ::_thesis: verum
end;
uniqueness
for b1, b2 being PartFunc of COMPLEX,COMPLEX st dom b1 = X & ( for x being Element of COMPLEX st x in X holds
b1 /. x = diff (f,x) ) & dom b2 = X & ( for x being Element of COMPLEX st x in X holds
b2 /. x = diff (f,x) ) holds
b1 = b2
proof
let F, G be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( dom F = X & ( for x being Element of COMPLEX st x in X holds
F /. x = diff (f,x) ) & dom G = X & ( for x being Element of COMPLEX st x in X holds
G /. x = diff (f,x) ) implies F = G )
assume that
A6: dom F = X and
A7: for x being Element of COMPLEX st x in X holds
F /. x = diff (f,x) and
A8: dom G = X and
A9: for x being Element of COMPLEX st x in X holds
G /. x = diff (f,x) ; ::_thesis: F = G
now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_dom_F_holds_
F_/._x_=_G_/._x
let x be Element of COMPLEX ; ::_thesis: ( x in dom F implies F /. x = G /. x )
assume A10: x in dom F ; ::_thesis: F /. x = G /. x
then F /. x = diff (f,x) by A6, A7;
hence F /. x = G /. x by A6, A9, A10; ::_thesis: verum
end;
hence F = G by A6, A8, PARTFUN2:1; ::_thesis: verum
end;
end;
:: deftheorem Def12 defines `| CFDIFF_1:def_12_:_
for f being PartFunc of COMPLEX,COMPLEX
for X being set st f is_differentiable_on X holds
for b3 being PartFunc of COMPLEX,COMPLEX holds
( b3 = f `| X iff ( dom b3 = X & ( for x being Element of COMPLEX st x in X holds
b3 /. x = diff (f,x) ) ) );
theorem :: CFDIFF_1:17
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & ex a1 being Element of COMPLEX st rng f = {a1} holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) )
proof
set R = cf;
A1: dom cf = COMPLEX by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0c
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0c
A2: ( rng h c= dom cf & n in NAT ) by A1, ORDINAL1:def_12;
thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5
.= ((h ") . n) * (cf /. (h . n)) by A2, FUNCT_2:109
.= ((h ") . n) * 0c by FUNCOP_1:7
.= 0c ; ::_thesis: verum
end;
then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def_18;
hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum
end;
then reconsider R = cf as C_RestFunc by Def3;
set L = cf;
for z being Element of COMPLEX holds cf /. z = 0c * z by FUNCOP_1:7;
then reconsider L = cf as C_LinearFunc by Def4;
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom f & ex a1 being Element of COMPLEX st rng f = {a1} holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) )
let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom f & ex a1 being Element of COMPLEX st rng f = {a1} implies ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) ) )
assume A3: Z c= dom f ; ::_thesis: ( for a1 being Element of COMPLEX holds not rng f = {a1} or ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) ) )
given a1 being Element of COMPLEX such that A4: rng f = {a1} ; ::_thesis: ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) )
A5: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_dom_f_holds_
f_/._x0_=_a1
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in dom f implies f /. x0 = a1 )
assume A6: x0 in dom f ; ::_thesis: f /. x0 = a1
then f . x0 in {a1} by A4, FUNCT_1:def_3;
then f /. x0 in {a1} by A6, PARTFUN1:def_6;
hence f /. x0 = a1 by TARSKI:def_1; ::_thesis: verum
end;
A7: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A8: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A9: N c= Z by Th9;
A10: N c= dom f by A3, A9, XBOOLE_1:1;
for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5, A10
.= a1 - a1 by A3, A5, A8
.= (L /. (x - x0)) + 0c by FUNCOP_1:7
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
hence f is_differentiable_in x0 by A10, Def6; ::_thesis: verum
end;
hence A11: f is_differentiable_on Z by A3, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0c )
assume A12: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0c
then A13: f is_differentiable_in x0 by A7;
then ex N being Neighbourhood of x0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by Def6;
then consider N being Neighbourhood of x0 such that
A14: N c= dom f ;
A15: for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5, A14
.= a1 - a1 by A3, A5, A12
.= (L /. (x - x0)) + 0c by FUNCOP_1:7
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
thus (f `| Z) /. x0 = diff (f,x0) by A11, A12, Def12
.= L /. 1r by A13, A14, A15, Def7
.= 0c by FUNCOP_1:7 ; ::_thesis: verum
end;
registration
let seq be non-zero Complex_Sequence;
let k be Nat;
clusterseq ^\ k -> non-zero ;
coherence
seq ^\ k is non-empty
proof
now__::_thesis:_for_n_being_Element_of_NAT_holds_(seq_^\_k)_._n_<>_0c
let n be Element of NAT ; ::_thesis: (seq ^\ k) . n <> 0c
(seq ^\ k) . n = seq . (n + k) by NAT_1:def_3;
hence (seq ^\ k) . n <> 0c by COMSEQ_1:4; ::_thesis: verum
end;
hence seq ^\ k is non-empty by COMSEQ_1:4; ::_thesis: verum
end;
end;
registration
let h be non-zero 0 -convergent Complex_Sequence;
let n be Element of NAT ;
clusterh ^\ n -> 0 -convergent for Complex_Sequence;
coherence
for b1 being Complex_Sequence st b1 = h ^\ n holds
b1 is 0 -convergent
proof
lim h = 0 by Def1;
then A1: lim (h ^\ n) = 0 by CFCONT_1:21;
h ^\ n is convergent by CFCONT_1:21;
hence for b1 being Complex_Sequence st b1 = h ^\ n holds
b1 is 0 -convergent by A1, Def1; ::_thesis: verum
end;
end;
theorem Th18: :: CFDIFF_1:18
for k being Element of NAT
for seq, seq1 being Complex_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq, seq1 being Complex_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
let seq, seq1 be Complex_Sequence; ::_thesis: (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_+_seq1)_^\_k)_._n_=_((seq_^\_k)_+_(seq1_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((seq + seq1) ^\ k) . n = ((seq ^\ k) + (seq1 ^\ k)) . n
thus ((seq + seq1) ^\ k) . n = (seq + seq1) . (n + k) by NAT_1:def_3
.= (seq . (n + k)) + (seq1 . (n + k)) by VALUED_1:1
.= ((seq ^\ k) . n) + (seq1 . (n + k)) by NAT_1:def_3
.= ((seq ^\ k) . n) + ((seq1 ^\ k) . n) by NAT_1:def_3
.= ((seq ^\ k) + (seq1 ^\ k)) . n by VALUED_1:1 ; ::_thesis: verum
end;
hence (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th19: :: CFDIFF_1:19
for k being Element of NAT
for seq, seq1 being Complex_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq, seq1 being Complex_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
let seq, seq1 be Complex_Sequence; ::_thesis: (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_-_seq1)_^\_k)_._n_=_((seq_^\_k)_-_(seq1_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((seq - seq1) ^\ k) . n = ((seq ^\ k) - (seq1 ^\ k)) . n
thus ((seq - seq1) ^\ k) . n = (seq + (- seq1)) . (n + k) by NAT_1:def_3
.= (seq . (n + k)) + ((- seq1) . (n + k)) by VALUED_1:1
.= (seq . (n + k)) + (- (seq1 . (n + k))) by VALUED_1:8
.= ((seq ^\ k) . n) - (seq1 . (n + k)) by NAT_1:def_3
.= ((seq ^\ k) . n) + (- ((seq1 ^\ k) . n)) by NAT_1:def_3
.= ((seq ^\ k) . n) + ((- (seq1 ^\ k)) . n) by VALUED_1:8
.= ((seq ^\ k) - (seq1 ^\ k)) . n by VALUED_1:1 ; ::_thesis: verum
end;
hence (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th20: :: CFDIFF_1:20
for k being Element of NAT
for seq being Complex_Sequence holds (seq ") ^\ k = (seq ^\ k) "
proof
let k be Element of NAT ; ::_thesis: for seq being Complex_Sequence holds (seq ") ^\ k = (seq ^\ k) "
let seq be Complex_Sequence; ::_thesis: (seq ") ^\ k = (seq ^\ k) "
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_")_^\_k)_._n_=_((seq_^\_k)_")_._n
let n be Element of NAT ; ::_thesis: ((seq ") ^\ k) . n = ((seq ^\ k) ") . n
thus ((seq ") ^\ k) . n = (seq ") . (n + k) by NAT_1:def_3
.= (seq . (n + k)) " by VALUED_1:10
.= ((seq ^\ k) . n) " by NAT_1:def_3
.= ((seq ^\ k) ") . n by VALUED_1:10 ; ::_thesis: verum
end;
hence (seq ") ^\ k = (seq ^\ k) " by FUNCT_2:63; ::_thesis: verum
end;
theorem Th21: :: CFDIFF_1:21
for k being Element of NAT
for seq, seq1 being Complex_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)
proof
let k be Element of NAT ; ::_thesis: for seq, seq1 being Complex_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)
let seq, seq1 be Complex_Sequence; ::_thesis: (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)
now__::_thesis:_for_n_being_Element_of_NAT_holds_((seq_(#)_seq1)_^\_k)_._n_=_((seq_^\_k)_(#)_(seq1_^\_k))_._n
let n be Element of NAT ; ::_thesis: ((seq (#) seq1) ^\ k) . n = ((seq ^\ k) (#) (seq1 ^\ k)) . n
thus ((seq (#) seq1) ^\ k) . n = (seq (#) seq1) . (n + k) by NAT_1:def_3
.= (seq . (n + k)) * (seq1 . (n + k)) by VALUED_1:5
.= ((seq ^\ k) . n) * (seq1 . (n + k)) by NAT_1:def_3
.= ((seq ^\ k) . n) * ((seq1 ^\ k) . n) by NAT_1:def_3
.= ((seq ^\ k) (#) (seq1 ^\ k)) . n by VALUED_1:5 ; ::_thesis: verum
end;
hence (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k) by FUNCT_2:63; ::_thesis: verum
end;
theorem Th22: :: CFDIFF_1:22
for f being PartFunc of COMPLEX,COMPLEX
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))) )
proof
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 Element of COMPLEX st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6;
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, XBOOLE_1:1;
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 set ; :: 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 Element of 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 Element of NAT such that
A16: for m being Element of 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 ::_thesis: rng ((h + c) ^\ n) c= N2
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (c ^\ n) or y in N2 )
assume y in rng (c ^\ n) ; ::_thesis: y in N2
hence y in N2 by A11, A17, TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: 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 Element of 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 Element of 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 set ; :: 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( Element of NAT ) -> Element of COMPLEX = (L /. 1r) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . $1);
consider s1 being Complex_Sequence such that
A24: for k being Element of 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_Element_of_NAT_st_
for_k_being_Element_of_NAT_st_n1_<=_k_holds_
abs_((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 Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L /. 1r)) < r )
assume 0 < r ; ::_thesis: ex n1 being Element of NAT st
for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L /. 1r)) < r
then consider m being Element of NAT such that
A27: for k being Element of NAT st m <= k holds
abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0c) < r by A26, COMSEQ_2:def_6;
take n1 = m; ::_thesis: for k being Element of NAT st n1 <= k holds
abs ((s1 . k) - (L /. 1r)) < r
let k be Element of NAT ; ::_thesis: ( n1 <= k implies abs ((s1 . k) - (L /. 1r)) < r )
assume A28: n1 <= k ; ::_thesis: abs ((s1 . k) - (L /. 1r)) < r
abs ((s1 . k) - (L /. 1r)) = abs (((L /. 1r) + (((R /* (h ^\ n)) (#) ((h ^\ n) ")) . k)) - (L /. 1r)) by A24
.= abs (((((h ^\ n) ") (#) (R /* (h ^\ n))) . k) - 0c) ;
hence abs ((s1 . k) - (L /. 1r)) < r by A27, A28; ::_thesis: verum
end;
consider x being Element of COMPLEX such that
A29: for b1 being Element of 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 by FUNCT_2:63;
hence ((L /* (h ^\ n)) + (R /* (h ^\ n))) (#) ((h ^\ n) ") is convergent by A25, COMSEQ_2:def_5; ::_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 Element of NAT holds (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
proof
let k be Element of NAT ; ::_thesis: (f /. (((h + c) ^\ n) . k)) - (f /. ((c ^\ n) . k)) = (L /. ((h ^\ n) . k)) + (R /. ((h ^\ n) . k))
((h + c) ^\ n) . k in rng ((h + c) ^\ n) by FUNCT_2:112;
then A34: ((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;
then A35: (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
.= (((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, A34, A35; ::_thesis: verum
end;
A36: rng (h + c) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in dom f )
assume y in rng (h + c) ; ::_thesis: y in dom f
then y in N by A8;
hence y in dom f by A2; ::_thesis: verum
end;
A37: rng ((h + c) ^\ n) c= dom f
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng ((h + c) ^\ n) or y in dom f )
assume y in rng ((h + c) ^\ n) ; ::_thesis: y in dom f
then y in N2 by A19;
then y in N by A4;
hence y in dom f by A2; ::_thesis: verum
end;
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 A37, 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 A38: ((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 A36, 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 A39: 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, A38, CFCONT_1:22; ::_thesis: diff (f,x0) = lim ((h ") (#) ((f /* (h + c)) - (f /* c)))
for x being Element of 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, A39, Def7; ::_thesis: verum
end;
theorem Th23: :: CFDIFF_1:23
for f1, f2 being PartFunc of COMPLEX,COMPLEX
for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
proof
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
let x0 be Element of COMPLEX ; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) ) )
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 + f2 is_differentiable_in x0 & diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0)) )
consider N1 being Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider L1 being C_LinearFunc, R1 being C_RestFunc such that
A5: for x being Element of COMPLEX st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A4;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, Def6;
consider L2 being C_LinearFunc, R2 being C_RestFunc such that
A8: for x being Element of COMPLEX st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 /. (x - x0)) + (R2 /. (x - x0)) by A7;
reconsider R = R1 + R2 as C_RestFunc ;
reconsider L = L1 + L2 as C_LinearFunc ;
consider N being Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Lm1;
A11: N c= dom f2 by A6, A10, XBOOLE_1:1;
N c= dom f1 by A3, A9, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27;
then A12: N c= dom (f1 + f2) by VALUED_1:def_1;
A13: now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_N_holds_
((f1_+_f2)_/._x)_-_((f1_+_f2)_/._x0)_=_(L_/._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Element of COMPLEX ; ::_thesis: ( x in N implies ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A14: x0 in N by Th7;
assume A15: x in N ; ::_thesis: ((f1 + f2) /. x) - ((f1 + f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence ((f1 + f2) /. x) - ((f1 + f2) /. x0) = ((f1 /. x) + (f2 /. x)) - ((f1 + f2) /. x0) by A12, CFUNCT_1:1
.= ((f1 /. x) + (f2 /. x)) - ((f1 /. x0) + (f2 /. x0)) by A12, A14, CFUNCT_1:1
.= ((f1 /. x) - (f1 /. x0)) + ((f2 /. x) - (f2 /. x0))
.= ((L1 /. (x - x0)) + (R1 /. (x - x0))) + ((f2 /. x) - (f2 /. x0)) by A5, A9, A15
.= ((L1 /. (x - x0)) + (R1 /. (x - x0))) + ((L2 /. (x - x0)) + (R2 /. (x - x0))) by A8, A10, A15
.= ((L1 /. (x - x0)) + (L2 /. (x - x0))) + ((R1 /. (x - x0)) + (R2 /. (x - x0)))
.= (L /. (x - x0)) + ((R1 /. (x - x0)) + (R2 /. (x - x0))) by CFUNCT_1:64
.= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:64 ;
::_thesis: verum
end;
hence f1 + f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 + f2),x0) = (diff (f1,x0)) + (diff (f2,x0))
hence diff ((f1 + f2),x0) = L /. 1r by A12, A13, Def7
.= (L1 /. 1r) + (L2 /. 1r) by CFUNCT_1:64
.= (diff (f1,x0)) + (L2 /. 1r) by A1, A3, A5, Def7
.= (diff (f1,x0)) + (diff (f2,x0)) by A2, A6, A8, Def7 ;
::_thesis: verum
end;
theorem Th24: :: CFDIFF_1:24
for f1, f2 being PartFunc of COMPLEX,COMPLEX
for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
proof
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
let x0 be Element of COMPLEX ; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) ) )
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 - f2 is_differentiable_in x0 & diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0)) )
consider N1 being Neighbourhood of x0 such that
A3: N1 c= dom f1 and
A4: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider L1 being C_LinearFunc, R1 being C_RestFunc such that
A5: for x being Element of COMPLEX st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A4;
consider N2 being Neighbourhood of x0 such that
A6: N2 c= dom f2 and
A7: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, Def6;
consider L2 being C_LinearFunc, R2 being C_RestFunc such that
A8: for x being Element of COMPLEX st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 /. (x - x0)) + (R2 /. (x - x0)) by A7;
reconsider R = R1 - R2 as C_RestFunc ;
reconsider L = L1 - L2 as C_LinearFunc ;
consider N being Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Lm1;
A11: N c= dom f2 by A6, A10, XBOOLE_1:1;
N c= dom f1 by A3, A9, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27;
then A12: N c= dom (f1 - f2) by CFUNCT_1:2;
A13: now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_N_holds_
((f1_-_f2)_/._x)_-_((f1_-_f2)_/._x0)_=_(L_/._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Element of COMPLEX ; ::_thesis: ( x in N implies ((f1 - f2) /. x) - ((f1 - f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A14: x0 in N by Th7;
assume A15: x in N ; ::_thesis: ((f1 - f2) /. x) - ((f1 - f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence ((f1 - f2) /. x) - ((f1 - f2) /. x0) = ((f1 /. x) - (f2 /. x)) - ((f1 - f2) /. x0) by A12, CFUNCT_1:2
.= ((f1 /. x) - (f2 /. x)) - ((f1 /. x0) - (f2 /. x0)) by A12, A14, CFUNCT_1:2
.= ((f1 /. x) - (f1 /. x0)) - ((f2 /. x) - (f2 /. x0))
.= ((L1 /. (x - x0)) + (R1 /. (x - x0))) - ((f2 /. x) - (f2 /. x0)) by A5, A9, A15
.= ((L1 /. (x - x0)) + (R1 /. (x - x0))) - ((L2 /. (x - x0)) + (R2 /. (x - x0))) by A8, A10, A15
.= ((L1 /. (x - x0)) - (L2 /. (x - x0))) + ((R1 /. (x - x0)) - (R2 /. (x - x0)))
.= (L /. (x - x0)) + ((R1 /. (x - x0)) - (R2 /. (x - x0))) by CFUNCT_1:64
.= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:64 ;
::_thesis: verum
end;
hence f1 - f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 - f2),x0) = (diff (f1,x0)) - (diff (f2,x0))
hence diff ((f1 - f2),x0) = L /. 1r by A12, A13, Def7
.= (L1 /. 1r) - (L2 /. 1r) by CFUNCT_1:64
.= (diff (f1,x0)) - (L2 /. 1r) by A1, A3, A5, Def7
.= (diff (f1,x0)) - (diff (f2,x0)) by A2, A6, A8, Def7 ;
::_thesis: verum
end;
theorem Th25: :: CFDIFF_1:25
for a being Element of COMPLEX
for f being PartFunc of COMPLEX,COMPLEX
for x0 being Element of COMPLEX st f is_differentiable_in x0 holds
( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) )
proof
let a be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX
for x0 being Element of COMPLEX st f is_differentiable_in x0 holds
( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX st f is_differentiable_in x0 holds
( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) )
let x0 be Element of COMPLEX ; ::_thesis: ( f is_differentiable_in x0 implies ( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) ) )
assume A1: f is_differentiable_in x0 ; ::_thesis: ( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) )
then consider N1 being Neighbourhood of x0 such that
A2: N1 c= dom f and
A3: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N1 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
consider L1 being C_LinearFunc, R1 being C_RestFunc such that
A4: for x being Element of COMPLEX st x in N1 holds
(f /. x) - (f /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A3;
reconsider R = a (#) R1 as C_RestFunc ;
reconsider L = a (#) L1 as C_LinearFunc ;
A5: N1 c= dom (a (#) f) by A2, VALUED_1:def_5;
A6: now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_N1_holds_
((a_(#)_f)_/._x)_-_((a_(#)_f)_/._x0)_=_(L_/._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Element of COMPLEX ; ::_thesis: ( x in N1 implies ((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A7: x0 in N1 by Th7;
assume A8: x in N1 ; ::_thesis: ((a (#) f) /. x) - ((a (#) f) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence ((a (#) f) /. x) - ((a (#) f) /. x0) = (a * (f /. x)) - ((a (#) f) /. x0) by A5, CFUNCT_1:4
.= (a * (f /. x)) - (a * (f /. x0)) by A5, A7, CFUNCT_1:4
.= a * ((f /. x) - (f /. x0))
.= a * ((L1 /. (x - x0)) + (R1 /. (x - x0))) by A4, A8
.= (a * (L1 /. (x - x0))) + (a * (R1 /. (x - x0)))
.= (L /. (x - x0)) + (a * (R1 /. (x - x0))) by CFUNCT_1:65
.= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:65 ;
::_thesis: verum
end;
hence a (#) f is_differentiable_in x0 by A5, Def6; ::_thesis: diff ((a (#) f),x0) = a * (diff (f,x0))
hence diff ((a (#) f),x0) = L /. 1r by A5, A6, Def7
.= a * (L1 /. 1r) by CFUNCT_1:65
.= a * (diff (f,x0)) by A1, A2, A4, Def7 ;
::_thesis: verum
end;
theorem Th26: :: CFDIFF_1:26
for f1, f2 being PartFunc of COMPLEX,COMPLEX
for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) )
proof
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX st f1 is_differentiable_in x0 & f2 is_differentiable_in x0 holds
( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) )
let x0 be Element of COMPLEX ; ::_thesis: ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 implies ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) ) )
assume that
A1: f1 is_differentiable_in x0 and
A2: f2 is_differentiable_in x0 ; ::_thesis: ( f1 (#) f2 is_differentiable_in x0 & diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) )
consider N2 being Neighbourhood of x0 such that
A3: N2 c= dom f2 and
A4: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, Def6;
consider L2 being C_LinearFunc, R2 being C_RestFunc such that
A5: for x being Element of COMPLEX st x in N2 holds
(f2 /. x) - (f2 /. x0) = (L2 /. (x - x0)) + (R2 /. (x - x0)) by A4;
reconsider R12 = (f1 /. x0) (#) R2 as C_RestFunc ;
reconsider L12 = (f1 /. x0) (#) L2 as C_LinearFunc ;
consider N1 being Neighbourhood of x0 such that
A6: N1 c= dom f1 and
A7: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1, Def6;
consider L1 being C_LinearFunc, R1 being C_RestFunc such that
A8: for x being Element of COMPLEX st x in N1 holds
(f1 /. x) - (f1 /. x0) = (L1 /. (x - x0)) + (R1 /. (x - x0)) by A7;
reconsider R11 = (f2 /. x0) (#) R1 as C_RestFunc ;
reconsider L11 = (f2 /. x0) (#) L1 as C_LinearFunc ;
reconsider R18 = R2 (#) L1 as C_RestFunc ;
reconsider R17 = R1 (#) R2 as C_RestFunc ;
reconsider R16 = R1 (#) L2 as C_RestFunc ;
reconsider R14 = L1 (#) L2 as C_RestFunc ;
reconsider R13 = R11 + R12 as C_RestFunc ;
reconsider L = L11 + L12 as C_LinearFunc ;
reconsider R15 = R13 + R14 as C_RestFunc ;
reconsider R19 = R16 + R17 as C_RestFunc ;
reconsider R20 = R19 + R18 as C_RestFunc ;
reconsider R = R15 + R20 as C_RestFunc ;
consider N being Neighbourhood of x0 such that
A9: N c= N1 and
A10: N c= N2 by Lm1;
A11: N c= dom f2 by A3, A10, XBOOLE_1:1;
N c= dom f1 by A6, A9, XBOOLE_1:1;
then N /\ N c= (dom f1) /\ (dom f2) by A11, XBOOLE_1:27;
then A12: N c= dom (f1 (#) f2) by VALUED_1:def_4;
A13: now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_N_holds_
((f1_(#)_f2)_/._x)_-_((f1_(#)_f2)_/._x0)_=_(L_/._(x_-_x0))_+_(R_/._(x_-_x0))
let x be Element of COMPLEX ; ::_thesis: ( x in N implies ((f1 (#) f2) /. x) - ((f1 (#) f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
A14: x0 in N by Th7;
assume A15: x in N ; ::_thesis: ((f1 (#) f2) /. x) - ((f1 (#) f2) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then A16: ((f1 /. x) - (f1 /. x0)) + (f1 /. x0) = ((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0) by A8, A9;
thus ((f1 (#) f2) /. x) - ((f1 (#) f2) /. x0) = ((f1 /. x) * (f2 /. x)) - ((f1 (#) f2) /. x0) by A12, A15, CFUNCT_1:3
.= ((((f1 /. x) * (f2 /. x)) + (- ((f1 /. x) * (f2 /. x0)))) + ((f1 /. x) * (f2 /. x0))) - ((f1 /. x0) * (f2 /. x0)) by A12, A14, CFUNCT_1:3
.= ((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((f1 /. x) - (f1 /. x0)) * (f2 /. x0))
.= ((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((L1 /. (x - x0)) + (R1 /. (x - x0))) * (f2 /. x0)) by A8, A9, A15
.= ((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + (((f2 /. x0) * (L1 /. (x - x0))) + ((R1 /. (x - x0)) * (f2 /. x0)))
.= ((f1 /. x) * ((f2 /. x) - (f2 /. x0))) + ((L11 /. (x - x0)) + ((f2 /. x0) * (R1 /. (x - x0)))) by CFUNCT_1:65
.= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) * ((f2 /. x) - (f2 /. x0))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by A16, CFUNCT_1:65
.= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) + (f1 /. x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by A5, A10, A15
.= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + (((f1 /. x0) * (L2 /. (x - x0))) + ((f1 /. x0) * (R2 /. (x - x0))))) + ((L11 /. (x - x0)) + (R11 /. (x - x0)))
.= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((f1 /. x0) * (R2 /. (x - x0))))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by CFUNCT_1:65
.= ((((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + (R12 /. (x - x0)))) + ((L11 /. (x - x0)) + (R11 /. (x - x0))) by CFUNCT_1:65
.= (((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((L11 /. (x - x0)) + ((R11 /. (x - x0)) + (R12 /. (x - x0)))))
.= (((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + ((L12 /. (x - x0)) + ((L11 /. (x - x0)) + (R13 /. (x - x0)))) by CFUNCT_1:64
.= (((L1 /. (x - x0)) + (R1 /. (x - x0))) * ((L2 /. (x - x0)) + (R2 /. (x - x0)))) + (((L11 /. (x - x0)) + (L12 /. (x - x0))) + (R13 /. (x - x0)))
.= ((((L1 /. (x - x0)) * (L2 /. (x - x0))) + ((L1 /. (x - x0)) * (R2 /. (x - x0)))) + ((R1 /. (x - x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64
.= (((R14 /. (x - x0)) + ((R2 /. (x - x0)) * (L1 /. (x - x0)))) + ((R1 /. (x - x0)) * ((L2 /. (x - x0)) + (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64
.= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + (((R1 /. (x - x0)) * (L2 /. (x - x0))) + ((R1 /. (x - x0)) * (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64
.= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + ((R16 /. (x - x0)) + ((R1 /. (x - x0)) * (R2 /. (x - x0))))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64
.= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + ((R16 /. (x - x0)) + (R17 /. (x - x0)))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64
.= (((R14 /. (x - x0)) + (R18 /. (x - x0))) + (R19 /. (x - x0))) + ((L /. (x - x0)) + (R13 /. (x - x0))) by CFUNCT_1:64
.= ((R14 /. (x - x0)) + ((R19 /. (x - x0)) + (R18 /. (x - x0)))) + ((L /. (x - x0)) + (R13 /. (x - x0)))
.= ((L /. (x - x0)) + (R13 /. (x - x0))) + ((R14 /. (x - x0)) + (R20 /. (x - x0))) by CFUNCT_1:64
.= (L /. (x - x0)) + (((R13 /. (x - x0)) + (R14 /. (x - x0))) + (R20 /. (x - x0)))
.= (L /. (x - x0)) + ((R15 /. (x - x0)) + (R20 /. (x - x0))) by CFUNCT_1:64
.= (L /. (x - x0)) + (R /. (x - x0)) by CFUNCT_1:64 ; ::_thesis: verum
end;
hence f1 (#) f2 is_differentiable_in x0 by A12, Def6; ::_thesis: diff ((f1 (#) f2),x0) = ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0)))
hence diff ((f1 (#) f2),x0) = L /. 1r by A12, A13, Def7
.= (L11 /. 1r) + (L12 /. 1r) by CFUNCT_1:64
.= ((f2 /. x0) * (L1 /. 1r)) + (L12 /. 1r) by CFUNCT_1:65
.= ((f2 /. x0) * (L1 /. 1r)) + ((f1 /. x0) * (L2 /. 1r)) by CFUNCT_1:65
.= ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (L2 /. 1r)) by A1, A6, A8, Def7
.= ((f2 /. x0) * (diff (f1,x0))) + ((f1 /. x0) * (diff (f2,x0))) by A2, A3, A5, Def7 ;
::_thesis: verum
end;
theorem :: CFDIFF_1:27
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 1r ) )
proof
set R = cf;
reconsider L = id COMPLEX as PartFunc of COMPLEX,COMPLEX ;
A1: COMPLEX c= COMPLEX ;
then for b being Element of COMPLEX holds L /. b = 1r * b by PARTFUN2:6;
then reconsider L = L as C_LinearFunc by Def4;
A2: dom cf = COMPLEX by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0c
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0c
A3: ( n in NAT & rng h c= dom cf ) by A2, ORDINAL1:def_12;
thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5
.= ((h ") . n) * (cf /. (h . n)) by A3, FUNCT_2:109
.= ((h ") . n) * 0c by FUNCOP_1:7
.= 0c ; ::_thesis: verum
end;
then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def_18;
hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum
end;
then reconsider R = cf as C_RestFunc by Def3;
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom f & f | Z = id Z holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 1r ) )
let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom f & f | Z = id Z implies ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 1r ) ) )
assume that
A4: Z c= dom f and
A5: f | Z = id Z ; ::_thesis: ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 1r ) )
A6: now__::_thesis:_for_x_being_Complex_st_x_in_Z_holds_
f_/._x_=_x
let x be Complex; ::_thesis: ( x in Z implies f /. x = x )
assume A7: x in Z ; ::_thesis: f /. x = x
then (f | Z) . x = x by A5, FUNCT_1:18;
then f . x = x by A7, FUNCT_1:49;
hence f /. x = x by A4, A7, PARTFUN1:def_6; ::_thesis: verum
end;
A8: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A9: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A10: N c= Z by Th9;
A11: for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = x - (f /. x0) by A6, A10
.= x - x0 by A6, A9
.= (L /. (x - x0)) + 0c by A1, PARTFUN2:6
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
N c= dom f by A4, A10, XBOOLE_1:1;
hence f is_differentiable_in x0 by A11, Def6; ::_thesis: verum
end;
hence A12: f is_differentiable_on Z by A4, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 1r
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 1r )
assume A13: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 1r
then consider N1 being Neighbourhood of x0 such that
A14: N1 c= Z by Th9;
A15: f is_differentiable_in x0 by A8, A13;
then ex N being Neighbourhood of x0 st
( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) ) by Def6;
then consider N being Neighbourhood of x0 such that
A16: N c= dom f ;
consider N2 being Neighbourhood of x0 such that
A17: N2 c= N1 and
A18: N2 c= N by Lm1;
A19: N2 c= dom f by A16, A18, XBOOLE_1:1;
A20: for x being Element of COMPLEX st x in N2 holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Element of COMPLEX ; ::_thesis: ( x in N2 implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N2 ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then x in N1 by A17;
hence (f /. x) - (f /. x0) = x - (f /. x0) by A6, A14
.= x - x0 by A6, A13
.= (L /. (x - x0)) + 0c by A1, PARTFUN2:6
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
thus (f `| Z) /. x0 = diff (f,x0) by A12, A13, Def12
.= L /. 1r by A15, A19, A20, Def7
.= 1r by A1, PARTFUN2:6 ; ::_thesis: verum
end;
theorem :: CFDIFF_1:28
for f1, f2 being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )
proof
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 + f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )
let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom (f1 + f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 + f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) ) )
assume that
A1: Z c= dom (f1 + f2) and
A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 + f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )
now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_
f1_+_f2_is_differentiable_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f1 + f2 is_differentiable_in x0 )
assume x0 in Z ; ::_thesis: f1 + f2 is_differentiable_in x0
then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th15;
hence f1 + f2 is_differentiable_in x0 by Th23; ::_thesis: verum
end;
hence A3: f1 + f2 is_differentiable_on Z by A1, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x))
now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_Z_holds_
((f1_+_f2)_`|_Z)_/._x_=_(diff_(f1,x))_+_(diff_(f2,x))
let x be Element of COMPLEX ; ::_thesis: ( x in Z implies ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) )
assume A4: x in Z ; ::_thesis: ((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x))
then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th15;
thus ((f1 + f2) `| Z) /. x = diff ((f1 + f2),x) by A3, A4, Def12
.= (diff (f1,x)) + (diff (f2,x)) by A5, Th23 ; ::_thesis: verum
end;
hence for x being Element of COMPLEX st x in Z holds
((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ; ::_thesis: verum
end;
theorem :: CFDIFF_1:29
for f1, f2 being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
proof
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 - f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom (f1 - f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 - f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) ) )
assume that
A1: Z c= dom (f1 - f2) and
A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 - f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )
now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_
f1_-_f2_is_differentiable_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f1 - f2 is_differentiable_in x0 )
assume x0 in Z ; ::_thesis: f1 - f2 is_differentiable_in x0
then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th15;
hence f1 - f2 is_differentiable_in x0 by Th24; ::_thesis: verum
end;
hence A3: f1 - f2 is_differentiable_on Z by A1, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))
now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_Z_holds_
((f1_-_f2)_`|_Z)_/._x_=_(diff_(f1,x))_-_(diff_(f2,x))
let x be Element of COMPLEX ; ::_thesis: ( x in Z implies ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) )
assume A4: x in Z ; ::_thesis: ((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x))
then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th15;
thus ((f1 - f2) `| Z) /. x = diff ((f1 - f2),x) by A3, A4, Def12
.= (diff (f1,x)) - (diff (f2,x)) by A5, Th24 ; ::_thesis: verum
end;
hence for x being Element of COMPLEX st x in Z holds
((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ; ::_thesis: verum
end;
theorem :: CFDIFF_1:30
for a being Element of COMPLEX
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom (a (#) f) & f is_differentiable_on Z holds
( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x)) ) )
proof
let a be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom (a (#) f) & f is_differentiable_on Z holds
( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x)) ) )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom (a (#) f) & f is_differentiable_on Z holds
( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x)) ) )
let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom (a (#) f) & f is_differentiable_on Z implies ( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x)) ) ) )
assume that
A1: Z c= dom (a (#) f) and
A2: f is_differentiable_on Z ; ::_thesis: ( a (#) f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x)) ) )
now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_
a_(#)_f_is_differentiable_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies a (#) f is_differentiable_in x0 )
assume x0 in Z ; ::_thesis: a (#) f is_differentiable_in x0
then f is_differentiable_in x0 by A2, Th15;
hence a (#) f is_differentiable_in x0 by Th25; ::_thesis: verum
end;
hence A3: a (#) f is_differentiable_on Z by A1, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x))
now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_Z_holds_
((a_(#)_f)_`|_Z)_/._x_=_a_*_(diff_(f,x))
let x be Element of COMPLEX ; ::_thesis: ( x in Z implies ((a (#) f) `| Z) /. x = a * (diff (f,x)) )
assume A4: x in Z ; ::_thesis: ((a (#) f) `| Z) /. x = a * (diff (f,x))
then A5: f is_differentiable_in x by A2, Th15;
thus ((a (#) f) `| Z) /. x = diff ((a (#) f),x) by A3, A4, Def12
.= a * (diff (f,x)) by A5, Th25 ; ::_thesis: verum
end;
hence for x being Element of COMPLEX st x in Z holds
((a (#) f) `| Z) /. x = a * (diff (f,x)) ; ::_thesis: verum
end;
theorem :: CFDIFF_1:31
for f1, f2 being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 (#) f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) )
proof
let f1, f2 be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z holds
( f1 (#) f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) )
let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom (f1 (#) f2) & f1 is_differentiable_on Z & f2 is_differentiable_on Z implies ( f1 (#) f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) ) )
assume that
A1: Z c= dom (f1 (#) f2) and
A2: ( f1 is_differentiable_on Z & f2 is_differentiable_on Z ) ; ::_thesis: ( f1 (#) f2 is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) )
now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_
f1_(#)_f2_is_differentiable_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f1 (#) f2 is_differentiable_in x0 )
assume x0 in Z ; ::_thesis: f1 (#) f2 is_differentiable_in x0
then ( f1 is_differentiable_in x0 & f2 is_differentiable_in x0 ) by A2, Th15;
hence f1 (#) f2 is_differentiable_in x0 by Th26; ::_thesis: verum
end;
hence A3: f1 (#) f2 is_differentiable_on Z by A1, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x)))
now__::_thesis:_for_x_being_Element_of_COMPLEX_st_x_in_Z_holds_
((f1_(#)_f2)_`|_Z)_/._x_=_((f2_/._x)_*_(diff_(f1,x)))_+_((f1_/._x)_*_(diff_(f2,x)))
let x be Element of COMPLEX ; ::_thesis: ( x in Z implies ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) )
assume A4: x in Z ; ::_thesis: ((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x)))
then A5: ( f1 is_differentiable_in x & f2 is_differentiable_in x ) by A2, Th15;
thus ((f1 (#) f2) `| Z) /. x = diff ((f1 (#) f2),x) by A3, A4, Def12
.= ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) by A5, Th26 ; ::_thesis: verum
end;
hence for x being Element of COMPLEX st x in Z holds
((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ; ::_thesis: verum
end;
theorem :: CFDIFF_1:32
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & f | Z is constant holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) )
proof
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom f & f | Z is constant holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) )
let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom f & f | Z is constant implies ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) ) )
set R = cf;
A1: dom cf = COMPLEX by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0c
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0c
A2: ( n in NAT & rng h c= dom cf ) by A1, ORDINAL1:def_12;
thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5
.= ((h ") . n) * (cf /. (h . n)) by A2, FUNCT_2:109
.= ((h ") . n) * 0c by FUNCOP_1:7
.= 0c ; ::_thesis: verum
end;
then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def_18;
hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum
end;
then reconsider R = cf as C_RestFunc by Def3;
set L = cf;
for x being Element of COMPLEX holds cf /. x = 0c * x by FUNCOP_1:7;
then reconsider L = cf as C_LinearFunc by Def4;
assume that
A3: Z c= dom f and
A4: f | Z is constant ; ::_thesis: ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c ) )
consider a1 being Element of COMPLEX such that
A5: for x being Element of COMPLEX st x in Z /\ (dom f) holds
f /. x = a1 by A4, PARTFUN2:35;
A6: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A7: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A8: N c= Z by Th9;
A9: N c= dom f by A3, A8, XBOOLE_1:1;
A10: x0 in Z /\ (dom f) by A3, A7, XBOOLE_0:def_4;
for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by A8, A9, XBOOLE_0:def_4;
hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5
.= a1 - a1 by A5, A10
.= (L /. (x - x0)) + 0c by FUNCOP_1:7
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
hence f is_differentiable_in x0 by A9, Def6; ::_thesis: verum
end;
hence A11: f is_differentiable_on Z by A3, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = 0c
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = 0c )
assume A12: x0 in Z ; ::_thesis: (f `| Z) /. x0 = 0c
then consider N being Neighbourhood of x0 such that
A13: N c= Z by Th9;
A14: N c= dom f by A3, A13, XBOOLE_1:1;
A15: x0 in Z /\ (dom f) by A3, A12, XBOOLE_0:def_4;
A16: for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then x in Z /\ (dom f) by A13, A14, XBOOLE_0:def_4;
hence (f /. x) - (f /. x0) = a1 - (f /. x0) by A5
.= a1 - a1 by A5, A15
.= (L /. (x - x0)) + 0c by FUNCOP_1:7
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
A17: f is_differentiable_in x0 by A6, A12;
thus (f `| Z) /. x0 = diff (f,x0) by A11, A12, Def12
.= L /. 1r by A17, A14, A16, Def7
.= 0c by FUNCOP_1:7 ; ::_thesis: verum
end;
theorem :: CFDIFF_1:33
for a, b being Element of COMPLEX
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f /. x = (a * x) + b ) holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = a ) )
proof
let a, b be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f /. x = (a * x) + b ) holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = a ) )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f /. x = (a * x) + b ) holds
( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = a ) )
let Z be open Subset of COMPLEX; ::_thesis: ( Z c= dom f & ( for x being Element of COMPLEX st x in Z holds
f /. x = (a * x) + b ) implies ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = a ) ) )
set R = cf;
A1: dom cf = COMPLEX by FUNCOP_1:13;
now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_(h_")_(#)_(cf_/*_h)_is_convergent_&_lim_((h_")_(#)_(cf_/*_h))_=_0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c )
now__::_thesis:_for_n_being_Nat_holds_((h_")_(#)_(cf_/*_h))_._n_=_0c
let n be Nat; ::_thesis: ((h ") (#) (cf /* h)) . n = 0c
A2: ( n in NAT & rng h c= dom cf ) by A1, ORDINAL1:def_12;
thus ((h ") (#) (cf /* h)) . n = ((h ") . n) * ((cf /* h) . n) by VALUED_1:5
.= ((h ") . n) * (cf /. (h . n)) by A2, FUNCT_2:109
.= ((h ") . n) * 0c by FUNCOP_1:7
.= 0c ; ::_thesis: verum
end;
then ( (h ") (#) (cf /* h) is constant & ((h ") (#) (cf /* h)) . 0 = 0c ) by VALUED_0:def_18;
hence ( (h ") (#) (cf /* h) is convergent & lim ((h ") (#) (cf /* h)) = 0c ) by CFCONT_1:26, CFCONT_1:27; ::_thesis: verum
end;
then reconsider R = cf as C_RestFunc by Def3;
assume that
A3: Z c= dom f and
A4: for x being Element of COMPLEX st x in Z holds
f /. x = (a * x) + b ; ::_thesis: ( f is_differentiable_on Z & ( for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = a ) )
deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = a * $1;
consider L being Function of COMPLEX,COMPLEX such that
A5: for x being Element of COMPLEX holds L . x = H1(x) from FUNCT_2:sch_4();
for z being Element of COMPLEX holds L /. z = a * z by A5;
then reconsider L = L as C_LinearFunc by Def4;
A6: now__::_thesis:_for_x0_being_Element_of_COMPLEX_st_x0_in_Z_holds_
f_is_differentiable_in_x0
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies f is_differentiable_in x0 )
assume A7: x0 in Z ; ::_thesis: f is_differentiable_in x0
then consider N being Neighbourhood of x0 such that
A8: N c= Z by Th9;
A9: for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((a * x) + b) - (f /. x0) by A4, A8
.= ((a * x) + b) - ((a * x0) + b) by A4, A7
.= (a * (x - x0)) + 0c
.= (L /. (x - x0)) + 0c by A5
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
N c= dom f by A3, A8, XBOOLE_1:1;
hence f is_differentiable_in x0 by A9, Def6; ::_thesis: verum
end;
hence A10: f is_differentiable_on Z by A3, Th15; ::_thesis: for x being Element of COMPLEX st x in Z holds
(f `| Z) /. x = a
let x0 be Element of COMPLEX ; ::_thesis: ( x0 in Z implies (f `| Z) /. x0 = a )
assume A11: x0 in Z ; ::_thesis: (f `| Z) /. x0 = a
then consider N being Neighbourhood of x0 such that
A12: N c= Z by Th9;
A13: for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
proof
let x be Element of COMPLEX ; ::_thesis: ( x in N implies (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume x in N ; ::_thesis: (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0))
hence (f /. x) - (f /. x0) = ((a * x) + b) - (f /. x0) by A4, A12
.= ((a * x) + b) - ((a * x0) + b) by A4, A11
.= (a * (x - x0)) + 0c
.= (L /. (x - x0)) + 0c by A5
.= (L /. (x - x0)) + (R /. (x - x0)) by FUNCOP_1:7 ;
::_thesis: verum
end;
A14: N c= dom f by A3, A12, XBOOLE_1:1;
A15: f is_differentiable_in x0 by A6, A11;
thus (f `| Z) /. x0 = diff (f,x0) by A10, A11, Def12
.= L /. 1r by A15, A14, A13, Def7
.= a * 1r by A5
.= a ; ::_thesis: verum
end;
theorem Th34: :: CFDIFF_1:34
for f being PartFunc of COMPLEX,COMPLEX
for x0 being Element of COMPLEX st f is_differentiable_in x0 holds
f is_continuous_in x0
proof
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for x0 being Element of COMPLEX st f is_differentiable_in x0 holds
f is_continuous_in x0
let x0 be Element of COMPLEX ; ::_thesis: ( f is_differentiable_in x0 implies f is_continuous_in x0 )
assume A1: f is_differentiable_in x0 ; ::_thesis: f is_continuous_in x0
then consider N being Neighbourhood of x0 such that
A2: N c= dom f and
ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
A3: x0 in N by Th7;
now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_f_&_s1_is_convergent_&_lim_s1_=_x0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_x0_)_holds_
(_f_/*_s1_is_convergent_&_f_/._x0_=_lim_(f_/*_s1)_)
consider g being Real such that
A4: 0 < g and
A5: { y where y is Complex : |.(y - x0).| < g } c= N by Def5;
reconsider s2 = NAT --> x0 as Complex_Sequence ;
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom f & s1 is convergent & lim s1 = x0 & ( for n being Element of NAT holds s1 . n <> x0 ) implies ( f /* s1 is convergent & f /. x0 = lim (f /* s1) ) )
assume that
A6: rng s1 c= dom f and
A7: s1 is convergent and
A8: lim s1 = x0 and
A9: for n being Element of NAT holds s1 . n <> x0 ; ::_thesis: ( f /* s1 is convergent & f /. x0 = lim (f /* s1) )
consider l being Element of NAT such that
A10: for m being Element of NAT st l <= m holds
|.((s1 . m) - x0).| < g by A7, A8, A4, COMSEQ_2:def_6;
A11: lim s2 = s2 . 0 by CFCONT_1:28
.= x0 by FUNCOP_1:7 ;
deffunc H1( Element of NAT ) -> Element of COMPLEX = (s1 . $1) - (s2 . $1);
consider s3 being Complex_Sequence such that
A12: for n being Element of NAT holds s3 . n = H1(n) from FUNCT_2:sch_4();
A13: s3 = s1 - s2 by A12, CFCONT_1:1;
A14: s2 is convergent by CFCONT_1:26;
then A15: s3 is convergent by A7, A13;
lim s3 = lim (s1 - s2) by A12, CFCONT_1:1
.= x0 - x0 by A7, A8, A14, A11, COMSEQ_2:26
.= 0c ;
then A16: lim (s3 ^\ l) = 0c by A15, CFCONT_1:21;
reconsider c = s2 ^\ l as constant Complex_Sequence ;
A17: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_s3_._n_=_0c
given n being Element of NAT such that A18: s3 . n = 0c ; ::_thesis: contradiction
(s1 . n) - (s2 . n) = 0c by A12, A18;
hence contradiction by A9, FUNCOP_1:7; ::_thesis: verum
end;
A19: now__::_thesis:_for_n_being_Element_of_NAT_holds_not_(s3_^\_l)_._n_=_0c
given n being Element of NAT such that A20: (s3 ^\ l) . n = 0c ; ::_thesis: contradiction
s3 . (n + l) = 0c by A20, NAT_1:def_3;
hence contradiction by A17; ::_thesis: verum
end;
then A21: s3 ^\ l is non-zero by COMSEQ_1:4;
s3 ^\ l is convergent by A15, CFCONT_1:21;
then reconsider h = s3 ^\ l as non-zero 0 -convergent Complex_Sequence by A16, A21, Def1;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(((f_/*_(h_+_c))_-_(f_/*_c))_+_(f_/*_c))_._n_=_(f_/*_(h_+_c))_._n
let n be Element of NAT ; ::_thesis: (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (f /* (h + c)) . n
thus (((f /* (h + c)) - (f /* c)) + (f /* c)) . n = (((f /* (h + c)) - (f /* c)) . n) + ((f /* c) . n) by VALUED_1:1
.= (((f /* (h + c)) . n) - ((f /* c) . n)) + ((f /* c) . n) by CFCONT_1:1
.= (f /* (h + c)) . n ; ::_thesis: verum
end;
then A22: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (h + c) by FUNCT_2:63;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(h_+_c)_._n_=_(s1_^\_l)_._n
let n be Element of NAT ; ::_thesis: (h + c) . n = (s1 ^\ l) . n
thus (h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A13, Th18
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by VALUED_1:1
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by CFCONT_1:1
.= (s1 ^\ l) . n by NAT_1:def_3 ; ::_thesis: verum
end;
then A23: ((f /* (h + c)) - (f /* c)) + (f /* c) = f /* (s1 ^\ l) by A22, FUNCT_2:63
.= (f /* s1) ^\ l by A6, VALUED_0:27 ;
A24: rng c = {x0}
proof
thus rng c c= {x0} :: according to XBOOLE_0:def_10 ::_thesis: {x0} c= rng c
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng c or y in {x0} )
assume y in rng c ; ::_thesis: y in {x0}
then consider n being Element of NAT such that
A25: y = (s2 ^\ l) . n by FUNCT_2:113;
y = s2 . (n + l) by A25, NAT_1:def_3;
then y = x0 by FUNCOP_1:7;
hence y in {x0} by TARSKI:def_1; ::_thesis: verum
end;
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in {x0} or y in rng c )
assume y in {x0} ; ::_thesis: y in rng c
then A26: y = x0 by TARSKI:def_1;
c . 0 = s2 . (0 + l) by NAT_1:def_3
.= y by A26, FUNCOP_1:7 ;
hence y in rng c by FUNCT_2:4; ::_thesis: verum
end;
A27: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_n_being_Element_of_NAT_st_
for_m_being_Element_of_NAT_st_n_<=_m_holds_
|.(((f_/*_c)_._m)_-_(f_/._x0)).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p )
assume A28: 0 < p ; ::_thesis: ex n being Element of NAT st
for m being Element of NAT st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p
take n = 0 ; ::_thesis: for m being Element of NAT st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p
thus for m being Element of NAT st n <= m holds
|.(((f /* c) . m) - (f /. x0)).| < p ::_thesis: verum
proof
let m be Element of NAT ; ::_thesis: ( n <= m implies |.(((f /* c) . m) - (f /. x0)).| < p )
assume n <= m ; ::_thesis: |.(((f /* c) . m) - (f /. x0)).| < p
{x0} c= dom f by A2, A3, ZFMISC_1:31;
then |.(((f /* c) . m) - (f /. x0)).| = |.((f /. (c . m)) - (f /. x0)).| by A24, FUNCT_2:109
.= |.((f /. (s2 . (m + l))) - (f /. x0)).| by NAT_1:def_3
.= |.((f /. x0) - (f /. x0)).| by FUNCOP_1:7
.= 0 by ABSVALUE:2 ;
hence |.(((f /* c) . m) - (f /. x0)).| < p by A28; ::_thesis: verum
end;
end;
then A29: f /* c is convergent by COMSEQ_2:def_5;
now__::_thesis:_for_n_being_Element_of_NAT_holds_(h_(#)_((h_")_(#)_((f_/*_(h_+_c))_-_(f_/*_c))))_._n_=_((f_/*_(h_+_c))_-_(f_/*_c))_._n
let n be Element of NAT ; ::_thesis: (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = ((f /* (h + c)) - (f /* c)) . n
A30: h . n <> 0 by A19;
thus (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) . n = (h . n) * (((h ") (#) ((f /* (h + c)) - (f /* c))) . n) by VALUED_1:5
.= (h . n) * (((h ") . n) * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:5
.= (h . n) * (((h . n) ") * (((f /* (h + c)) - (f /* c)) . n)) by VALUED_1:10
.= ((h . n) * ((h . n) ")) * (((f /* (h + c)) - (f /* c)) . n)
.= 1 * (((f /* (h + c)) - (f /* c)) . n) by A30, XCMPLX_0:def_7
.= ((f /* (h + c)) - (f /* c)) . n ; ::_thesis: verum
end;
then A31: h (#) ((h ") (#) ((f /* (h + c)) - (f /* c))) = (f /* (h + c)) - (f /* c) by FUNCT_2:63;
rng (h + c) c= N
proof
let y be set ; :: according to TARSKI:def_3 ::_thesis: ( not y in rng (h + c) or y in N )
assume A32: y in rng (h + c) ; ::_thesis: y in N
then consider n being Element of NAT such that
A33: y = (h + c) . n by FUNCT_2:113;
reconsider y1 = y as Complex by A32;
(h + c) . n = (((s1 - s2) + s2) ^\ l) . n by A13, Th18
.= ((s1 - s2) + s2) . (n + l) by NAT_1:def_3
.= ((s1 - s2) . (n + l)) + (s2 . (n + l)) by VALUED_1:1
.= ((s1 . (n + l)) - (s2 . (n + l))) + (s2 . (n + l)) by CFCONT_1:1
.= s1 . (l + n) ;
then |.(((h + c) . n) - x0).| < g by A10, NAT_1:12;
then y1 in { z where z is Complex : |.(z - x0).| < g } by A33;
hence y in N by A5; ::_thesis: verum
end;
then A34: (h ") (#) ((f /* (h + c)) - (f /* c)) is convergent by A1, A2, A24, Th22;
then A35: (f /* (h + c)) - (f /* c) is convergent by A31;
then A36: ((f /* (h + c)) - (f /* c)) + (f /* c) is convergent by A29;
hence f /* s1 is convergent by A23, CFCONT_1:22; ::_thesis: f /. x0 = lim (f /* s1)
lim (h (#) ((h ") (#) ((f /* (h + c)) - (f /* c)))) = 0c * (lim ((h ") (#) ((f /* (h + c)) - (f /* c)))) by A16, A34, COMSEQ_2:30
.= 0 ;
then lim (((f /* (h + c)) - (f /* c)) + (f /* c)) = 0c + (lim (f /* c)) by A31, A35, A29, COMSEQ_2:14
.= f /. x0 by A27, A29, COMSEQ_2:def_6 ;
hence f /. x0 = lim (f /* s1) by A36, A23, CFCONT_1:23; ::_thesis: verum
end;
hence f is_continuous_in x0 by A2, A3, CFCONT_1:31; ::_thesis: verum
end;
theorem :: CFDIFF_1:35
for X being set
for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds
f is_continuous_on X
proof
let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds
f is_continuous_on X
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_differentiable_on X implies f is_continuous_on X )
assume A1: f is_differentiable_on X ; ::_thesis: f is_continuous_on X
hence A2: X c= dom f by Def9; :: according to CFCONT_1:def_2 ::_thesis: for b1 being Element of COMPLEX holds
( not b1 in X or f | X is_continuous_in b1 )
let x be Element of COMPLEX ; ::_thesis: ( not x in X or f | X is_continuous_in x )
assume x in X ; ::_thesis: f | X is_continuous_in x
then A3: x in dom (f | X) by A2, RELAT_1:57;
f | X is differentiable by A1, Def9;
then f | X is_differentiable_in x by A3, Def8;
hence f | X is_continuous_in x by Th34; ::_thesis: verum
end;
theorem :: CFDIFF_1:36
for X being set
for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
proof
let X be set ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX
for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: for Z being open Subset of COMPLEX st f is_differentiable_on X & Z c= X holds
f is_differentiable_on Z
let Z be open Subset of COMPLEX; ::_thesis: ( f is_differentiable_on X & Z c= X implies f is_differentiable_on Z )
assume that
A1: f is_differentiable_on X and
A2: Z c= X ; ::_thesis: f is_differentiable_on Z
A3: f | X is differentiable by A1, Def9;
X c= dom f by A1, Def9;
hence Z c= dom f by A2, XBOOLE_1:1; :: according to CFDIFF_1:def_9 ::_thesis: f | Z is differentiable
let x0 be Element of COMPLEX ; :: according to CFDIFF_1:def_8 ::_thesis: ( x0 in dom (f | Z) implies f | Z is_differentiable_in x0 )
assume A4: x0 in dom (f | Z) ; ::_thesis: f | Z is_differentiable_in x0
then A5: x0 in dom f by RELAT_1:57;
A6: x0 in Z by A4, RELAT_1:57;
then consider N1 being Neighbourhood of x0 such that
A7: N1 c= Z by Th9;
x0 in dom (f | X) by A2, A5, A6, RELAT_1:57;
then f | X is_differentiable_in x0 by A3, Def8;
then consider N being Neighbourhood of x0 such that
A8: N c= dom (f | X) and
A9: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
consider N2 being Neighbourhood of x0 such that
A10: N2 c= N and
A11: N2 c= N1 by Lm1;
A12: N2 c= Z by A7, A11, XBOOLE_1:1;
take N2 ; :: according to CFDIFF_1:def_6 ::_thesis: ( N2 c= dom (f | Z) & ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0)) )
dom (f | X) = (dom f) /\ X by RELAT_1:61;
then dom (f | X) c= dom f by XBOOLE_1:17;
then N c= dom f by A8, XBOOLE_1:1;
then N2 c= dom f by A10, XBOOLE_1:1;
then N2 c= (dom f) /\ Z by A12, XBOOLE_1:19;
hence A13: N2 c= dom (f | Z) by RELAT_1:61; ::_thesis: ex L being C_LinearFunc ex R being C_RestFunc st
for z being Element of COMPLEX st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
consider L being C_LinearFunc, R being C_RestFunc such that
A14: for x being Element of COMPLEX st x in N holds
((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A9;
take L ; ::_thesis: ex R being C_RestFunc st
for z being Element of COMPLEX st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
take R ; ::_thesis: for z being Element of COMPLEX st z in N2 holds
((f | Z) /. z) - ((f | Z) /. x0) = (L /. (z - x0)) + (R /. (z - x0))
let x be Element of COMPLEX ; ::_thesis: ( x in N2 implies ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) )
assume A15: x in N2 ; ::_thesis: ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0))
then ((f | X) /. x) - ((f | X) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A10, A14;
then A16: ((f | X) /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A2, A5, A6, PARTFUN2:17;
x in N by A10, A15;
then (f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A8, A16, PARTFUN2:15;
then (f /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A5, A6, PARTFUN2:17;
hence ((f | Z) /. x) - ((f | Z) /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A13, A15, PARTFUN2:15; ::_thesis: verum
end;
theorem :: CFDIFF_1:37
canceled;
theorem :: CFDIFF_1:38
for x0 being Element of COMPLEX
for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_in x0 holds
ex R being C_RestFunc st
( R /. 0c = 0c & R is_continuous_in 0c )
proof
let x0 be Element of COMPLEX ; ::_thesis: for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_in x0 holds
ex R being C_RestFunc st
( R /. 0c = 0c & R is_continuous_in 0c )
let f be PartFunc of COMPLEX,COMPLEX; ::_thesis: ( f is_differentiable_in x0 implies ex R being C_RestFunc st
( R /. 0c = 0c & R is_continuous_in 0c ) )
assume f is_differentiable_in x0 ; ::_thesis: ex R being C_RestFunc st
( R /. 0c = 0c & R is_continuous_in 0c )
then consider N being Neighbourhood of x0 such that
N c= dom f and
A1: ex L being C_LinearFunc ex R being C_RestFunc st
for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by Def6;
consider L being C_LinearFunc, R being C_RestFunc such that
A2: for x being Element of COMPLEX st x in N holds
(f /. x) - (f /. x0) = (L /. (x - x0)) + (R /. (x - x0)) by A1;
take R ; ::_thesis: ( R /. 0c = 0c & R is_continuous_in 0c )
consider a being Element of COMPLEX such that
A3: for z being Element of COMPLEX holds L /. z = a * z by Def4;
(f /. x0) - (f /. x0) = (L /. (x0 - x0)) + (R /. (x0 - x0)) by A2, Th7;
then A4: 0c = (a * 0c) + (R /. 0c) by A3;
hence R /. 0c = 0c ; ::_thesis: R is_continuous_in 0c
A5: now__::_thesis:_for_h_being_non-zero_0_-convergent_Complex_Sequence_holds_
(_R_/*_h_is_convergent_&_lim_(R_/*_h)_=_R_/._0c_)
let h be non-zero 0 -convergent Complex_Sequence; ::_thesis: ( R /* h is convergent & lim (R /* h) = R /. 0c )
(h ") (#) (R /* h) is bounded by Def3;
then consider M being Real such that
M > 0 and
A6: for n being Element of NAT holds |.(((h ") (#) (R /* h)) . n).| < M by COMSEQ_2:8;
lim h = 0 by Def1;
then lim |.h.| = |.0.| by SEQ_2:27;
then A7: lim (M (#) |.h.|) = M * |.0.| by SEQ_2:8
.= M * 0 by ABSVALUE:2
.= 0 ;
A8: now__::_thesis:_for_p_being_Real_st_0_<_p_holds_
ex_m_being_Element_of_NAT_st_
for_n_being_Element_of_NAT_st_m_<=_n_holds_
|.(((R_/*_h)_._n)_-_0c).|_<_p
let p be Real; ::_thesis: ( 0 < p implies ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(((R /* h) . n) - 0c).| < p )
assume 0 < p ; ::_thesis: ex m being Element of NAT st
for n being Element of NAT st m <= n holds
|.(((R /* h) . n) - 0c).| < p
then consider m being Element of NAT such that
A9: for n being Element of NAT st m <= n holds
abs (((M (#) |.h.|) . n) - 0) < p by A7, SEQ_2:def_7;
take m = m; ::_thesis: for n being Element of NAT st m <= n holds
|.(((R /* h) . n) - 0c).| < p
now__::_thesis:_for_n_being_Element_of_NAT_st_m_<=_n_holds_
|.(((R_/*_h)_._n)_-_0c).|_<_p
let n be Element of NAT ; ::_thesis: ( m <= n implies |.(((R /* h) . n) - 0c).| < p )
assume m <= n ; ::_thesis: |.(((R /* h) . n) - 0c).| < p
then A10: abs (((M (#) |.h.|) . n) - 0) < p by A9;
|.(((h ") (#) (R /* h)) . n).| = |.(((h ") . n) * ((R /* h) . n)).| by VALUED_1:5
.= |.(((h . n) ") * ((R /* h) . n)).| by VALUED_1:10 ;
then A11: |.(((h . n) ") * ((R /* h) . n)).| <= M by A6;
|.(h . n).| >= 0 by COMPLEX1:46;
then |.(h . n).| * |.(((h . n) ") * ((R /* h) . n)).| <= M * |.(h . n).| by A11, XREAL_1:64;
then |.((h . n) * (((h . n) ") * ((R /* h) . n))).| <= M * |.(h . n).| by COMPLEX1:65;
then ( h . n <> 0c & |.(((h . n) * ((h . n) ")) * ((R /* h) . n)).| <= M * |.(h . n).| ) by COMSEQ_1:4;
then |.(1r * ((R /* h) . n)).| <= M * |.(h . n).| by XCMPLX_0:def_7;
then |.((R /* h) . n).| <= M * (|.h.| . n) by VALUED_1:18;
then A12: |.((R /* h) . n).| <= (M (#) |.h.|) . n by SEQ_1:9;
then 0 <= (M (#) |.h.|) . n by COMPLEX1:46;
then (M (#) |.h.|) . n < p by A10, ABSVALUE:def_1;
hence |.(((R /* h) . n) - 0c).| < p by A12, XXREAL_0:2; ::_thesis: verum
end;
hence for n being Element of NAT st m <= n holds
|.(((R /* h) . n) - 0c).| < p ; ::_thesis: verum
end;
hence R /* h is convergent by COMSEQ_2:def_5; ::_thesis: lim (R /* h) = R /. 0c
hence lim (R /* h) = R /. 0c by A4, A8, COMSEQ_2:def_6; ::_thesis: verum
end;
A13: now__::_thesis:_for_s1_being_Complex_Sequence_st_rng_s1_c=_dom_R_&_s1_is_convergent_&_lim_s1_=_0_&_(_for_n_being_Element_of_NAT_holds_s1_._n_<>_0_)_holds_
(_R_/*_s1_is_convergent_&_lim_(R_/*_s1)_=_R_/._0c_)
let s1 be Complex_Sequence; ::_thesis: ( rng s1 c= dom R & s1 is convergent & lim s1 = 0 & ( for n being Element of NAT holds s1 . n <> 0 ) implies ( R /* s1 is convergent & lim (R /* s1) = R /. 0c ) )
assume that
rng s1 c= dom R and
A14: ( s1 is convergent & lim s1 = 0 ) and
A15: for n being Element of NAT holds s1 . n <> 0 ; ::_thesis: ( R /* s1 is convergent & lim (R /* s1) = R /. 0c )
s1 is non-zero by A15, COMSEQ_1:4;
then s1 is non-zero 0 -convergent Complex_Sequence by A14, Def1;
hence ( R /* s1 is convergent & lim (R /* s1) = R /. 0c ) by A5; ::_thesis: verum
end;
dom R = COMPLEX by PARTFUN1:def_2;
hence R is_continuous_in 0c by A13, CFCONT_1:31; ::_thesis: verum
end;