:: by Chanapat Pacharapokin , Hiroshi Yamazaki , Yasunari Shidama and Yatsuka Nakamura

::

:: Received November 4, 2008

:: Copyright (c) 2008-2017 Association of Mizar Users

:: deftheorem Def1 defines -convergent CFDIFF_1:def 1 :

for x being Real

for IT being Complex_Sequence holds

( IT is x -convergent iff ( IT is convergent & lim IT = x ) );

for x being Real

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 ;

for cs being Complex_Sequence st rs = cs & rs is convergent holds

cs is convergent ;

definition

let r be Real;

ex b_{1} being Complex_Sequence st

for n being Nat holds b_{1} . n = 1 / (n + r)

for b_{1}, b_{2} being Complex_Sequence st ( for n being Nat holds b_{1} . n = 1 / (n + r) ) & ( for n being Nat holds b_{2} . n = 1 / (n + r) ) holds

b_{1} = b_{2}

end;
func InvShift r -> Complex_Sequence means :Def2: :: CFDIFF_1:def 2

for n being Nat holds it . n = 1 / (n + r);

existence for n being Nat holds it . n = 1 / (n + r);

ex b

for n being Nat holds b

proof end;

uniqueness for b

b

proof end;

:: deftheorem Def2 defines InvShift CFDIFF_1:def 2 :

for r being Real

for b_{2} being Complex_Sequence holds

( b_{2} = InvShift r iff for n being Nat holds b_{2} . n = 1 / (n + r) );

for r being Real

for b

( b

registration

let r be positive Real;

coherence

( InvShift r is non-zero & InvShift r is 0 -convergent )

end;
coherence

( InvShift r is non-zero & InvShift r is 0 -convergent )

proof end;

registration

ex b_{1} being Complex_Sequence st

( b_{1} is 0 -convergent & b_{1} is non-zero )
end;

cluster V1() V4( NAT ) V5( COMPLEX ) Function-like V11() total non-zero quasi_total complex-valued 0 -convergent for Element of K19(K20(NAT,COMPLEX));

existence ex b

( b

proof end;

registration

for b_{1} being Complex_Sequence st b_{1} is 0 -convergent & b_{1} is non-zero holds

b_{1} is convergent
;

end;

cluster Function-like non-zero quasi_total 0 -convergent -> convergent for Element of K19(K20(NAT,COMPLEX));

coherence for b

b

reconsider cs = NAT --> 0c as Complex_Sequence ;

registration

ex b_{1} being Complex_Sequence st b_{1} is constant
end;

cluster V1() V4( NAT ) V5( COMPLEX ) Function-like constant V11() total quasi_total complex-valued for Element of K19(K20(NAT,COMPLEX));

existence ex b

proof end;

theorem :: CFDIFF_1:4

for seq being Complex_Sequence holds

( seq is constant iff for n, m being Nat holds seq . n = seq . m )

( seq is constant iff for n, m being Nat holds seq . n = seq . m )

proof end;

theorem :: CFDIFF_1:5

for seq being Complex_Sequence

for Nseq being V42() sequence of NAT

for n being Nat holds (seq * Nseq) . n = seq . (Nseq . n)

for Nseq being V42() sequence of NAT

for n being Nat holds (seq * Nseq) . n = seq . (Nseq . n)

proof end;

definition

let IT be PartFunc of COMPLEX,COMPLEX;

end;
attr IT 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 );

for h being non-zero 0 -convergent Complex_Sequence holds

( (h ") (#) (IT /* h) is convergent & lim ((h ") (#) (IT /* h)) = 0 );

:: 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 ) );

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

ex b_{1} being PartFunc of COMPLEX,COMPLEX st

( b_{1} is total & b_{1} is RestFunc-like )
end;

cluster V1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued RestFunc-like for Element of K19(K20(COMPLEX,COMPLEX));

existence ex b

( b

proof end;

:: deftheorem Def4 defines linear CFDIFF_1:def 4 :

for IT being PartFunc of COMPLEX,COMPLEX holds

( IT is linear iff ex a being Complex st

for z being Complex holds IT /. z = a * z );

for IT being PartFunc of COMPLEX,COMPLEX holds

( IT is linear iff ex a being Complex st

for z being Complex holds IT /. z = a * z );

registration

ex b_{1} being PartFunc of COMPLEX,COMPLEX st

( b_{1} is total & b_{1} is linear )
end;

cluster V1() V4( COMPLEX ) V5( COMPLEX ) Function-like total complex-valued linear for Element of K19(K20(COMPLEX,COMPLEX));

existence ex b

( b

proof end;

registration

let L1, L2 be C_LinearFunc;

coherence

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = L1 + L2 holds

( b_{1} is total & b_{1} is linear )

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = L1 - L2 holds

( b_{1} is total & b_{1} is linear )

end;
coherence

for b

( b

proof end;

coherence for b

( b

proof end;

registration

let a be Complex;

let L be C_LinearFunc;

coherence

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = a (#) L holds

( b_{1} is total & b_{1} is linear )

end;
let L be C_LinearFunc;

coherence

for b

( b

proof end;

registration

let R1, R2 be C_RestFunc;

coherence

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = R1 + R2 holds

( b_{1} is total & b_{1} is RestFunc-like )

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = R1 - R2 holds

( b_{1} is total & b_{1} is RestFunc-like )

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = R1 (#) R2 holds

( b_{1} is total & b_{1} is RestFunc-like )

end;
coherence

for b

( b

proof end;

coherence for b

( b

proof end;

coherence for b

( b

proof end;

registration

let a be Complex;

let R be C_RestFunc;

coherence

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = a (#) R holds

( b_{1} is total & b_{1} is RestFunc-like )

end;
let R be C_RestFunc;

coherence

for b

( b

proof end;

registration

let L1, L2 be C_LinearFunc;

coherence

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = L1 (#) L2 holds

( b_{1} is total & b_{1} is RestFunc-like )

end;
coherence

for b

( b

proof end;

registration

let R be C_RestFunc;

let L be C_LinearFunc;

coherence

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = R (#) L holds

( b_{1} is total & b_{1} is RestFunc-like )

for b_{1} being PartFunc of COMPLEX,COMPLEX st b_{1} = L (#) R holds

( b_{1} is total & b_{1} is RestFunc-like )
;

end;
let L be C_LinearFunc;

coherence

for b

( b

proof end;

coherence for b

( b

definition

let z0 be Complex;

ex b_{1} being Subset of COMPLEX ex g being Real st

( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b_{1} )

end;
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 g being Real st

( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= it );

ex b

( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b

proof end;

:: deftheorem Def5 defines Neighbourhood CFDIFF_1:def 5 :

for z0 being Complex

for b_{2} being Subset of COMPLEX holds

( b_{2} is Neighbourhood of z0 iff ex g being Real st

( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b_{2} ) );

for z0 being Complex

for b

( b

( 0 < g & { y where y is Complex : |.(y - z0).| < g } c= b

theorem Th6: :: CFDIFF_1:6

for z0 being Complex

for g being Real st 0 < g holds

{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0

for g being Real st 0 < g holds

{ y where y is Complex : |.(y - z0).| < g } is Neighbourhood of z0

proof 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 end;

definition

let f be PartFunc of COMPLEX,COMPLEX;

let z0 be Complex;

end;
let z0 be Complex;

pred f is_differentiable_in z0 means :: 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 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

for z being Complex st z in N holds

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) );

:: deftheorem 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 Complex st z in N holds

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) );

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

ex b_{1} 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

( b_{1} = L /. 1r & ( for z being Complex st z in N holds

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) )

for b_{1}, b_{2} 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

( b_{1} = L /. 1r & ( for z being 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_{2} = L /. 1r & ( for z being Complex st z in N holds

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) holds

b_{1} = b_{2}

end;
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 Complex st z in N holds

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) );

existence 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 Complex st z in N holds

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) );

ex b

( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st

( b

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) )

proof end;

uniqueness for b

( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st

( b

(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

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) holds

b

proof 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 b_{3} being Element of COMPLEX holds

( b_{3} = 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

( b_{3} = L /. 1r & ( for z being Complex st z in N holds

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) );

for f being PartFunc of COMPLEX,COMPLEX

for z0 being Complex st f is_differentiable_in z0 holds

for b

( b

( N c= dom f & ex L being C_LinearFunc ex R being C_RestFunc st

( b

(f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) ) ) ) );

definition

let f be PartFunc of COMPLEX,COMPLEX;

end;
attr f is differentiable means :: CFDIFF_1:def 8

for x being Complex st x in dom f holds

f is_differentiable_in x;

for x being Complex st x in dom f holds

f is_differentiable_in x;

:: deftheorem defines differentiable CFDIFF_1:def 8 :

for f being PartFunc of COMPLEX,COMPLEX holds

( f is differentiable iff for x being Complex st x in dom f holds

f is_differentiable_in x );

for f being PartFunc of COMPLEX,COMPLEX holds

( f is differentiable iff for x being Complex st x in dom f holds

f is_differentiable_in x );

:: deftheorem 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 ) );

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 by XBOOLE_1:1;

for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds

X is Subset of COMPLEX by XBOOLE_1:1;

definition

let X be Subset of COMPLEX;

end;
attr X is closed means :: CFDIFF_1:def 10

for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds

lim s1 in X;

for s1 being Complex_Sequence st rng s1 c= X & s1 is convergent holds

lim s1 in X;

:: deftheorem 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 );

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

:: deftheorem defines open CFDIFF_1:def 11 :

for X being Subset of COMPLEX holds

( X is open iff X ` is closed );

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

for z0 being Complex st z0 in X holds

ex N being Neighbourhood of z0 st N c= X

proof 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

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

ex N being Neighbourhood of z0 st N c= X ) holds

X is open

proof end;

theorem :: CFDIFF_1:12

theorem Th13: :: CFDIFF_1:13

for X being Subset of COMPLEX

for z0 being Element of COMPLEX

for r being Real st X = { y where y is Complex : |.(y - z0).| < r } holds

X is open

for z0 being Element of COMPLEX

for r being Real st X = { y where y is Complex : |.(y - z0).| < r } holds

X is open

proof end;

theorem :: CFDIFF_1:14

for X being Subset of COMPLEX

for z0 being Element of COMPLEX

for r being Real st X = { y where y is Complex : |.(y - z0).| <= r } holds

X is closed

for z0 being Element of COMPLEX

for r being Real st X = { y where y is Complex : |.(y - z0).| <= r } holds

X is closed

proof 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 Complex st x in Z holds

f is_differentiable_in x ) ) )

for Z being open Subset of COMPLEX holds

( f is_differentiable_on Z iff ( Z c= dom f & ( for x being Complex st x in Z holds

f is_differentiable_in x ) ) )

proof 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

for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on Y holds

Y is open

proof end;

definition

let f be PartFunc of COMPLEX,COMPLEX;

let X be set ;

assume A1: f is_differentiable_on X ;

ex b_{1} being PartFunc of COMPLEX,COMPLEX st

( dom b_{1} = X & ( for x being Complex st x in X holds

b_{1} /. x = diff (f,x) ) )

for b_{1}, b_{2} being PartFunc of COMPLEX,COMPLEX st dom b_{1} = X & ( for x being Complex st x in X holds

b_{1} /. x = diff (f,x) ) & dom b_{2} = X & ( for x being Complex st x in X holds

b_{2} /. x = diff (f,x) ) holds

b_{1} = b_{2}

end;
let X be set ;

assume A1: f is_differentiable_on X ;

func f `| X -> PartFunc of COMPLEX,COMPLEX means :Def12: :: CFDIFF_1:def 12

( dom it = X & ( for x being Complex st x in X holds

it /. x = diff (f,x) ) );

existence ( dom it = X & ( for x being Complex st x in X holds

it /. x = diff (f,x) ) );

ex b

( dom b

b

proof end;

uniqueness for b

b

b

b

proof 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 b_{3} being PartFunc of COMPLEX,COMPLEX holds

( b_{3} = f `| X iff ( dom b_{3} = X & ( for x being Complex st x in X holds

b_{3} /. x = diff (f,x) ) ) );

for f being PartFunc of COMPLEX,COMPLEX

for X being set st f is_differentiable_on X holds

for b

( b

b

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 Complex st rng f = {a1} holds

( f is_differentiable_on Z & ( for x being Complex st x in Z holds

(f `| Z) /. x = 0c ) )

for Z being open Subset of COMPLEX st Z c= dom f & ex a1 being Complex st rng f = {a1} holds

( f is_differentiable_on Z & ( for x being Complex st x in Z holds

(f `| Z) /. x = 0c ) )

proof end;

registration
end;

registration

let h be non-zero 0 -convergent Complex_Sequence;

let n be Nat;

coherence

for b_{1} being Complex_Sequence st b_{1} = h ^\ n holds

b_{1} is 0 -convergent

end;
let n be Nat;

coherence

for b

b

proof end;

theorem Th18: :: CFDIFF_1:18

for k being Nat

for seq, seq1 being Complex_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

for seq, seq1 being Complex_Sequence holds (seq + seq1) ^\ k = (seq ^\ k) + (seq1 ^\ k)

proof end;

theorem Th19: :: CFDIFF_1:19

for k being Nat

for seq, seq1 being Complex_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)

for seq, seq1 being Complex_Sequence holds (seq - seq1) ^\ k = (seq ^\ k) - (seq1 ^\ k)

proof end;

theorem Th21: :: CFDIFF_1:21

for k being Nat

for seq, seq1 being Complex_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)

for seq, seq1 being Complex_Sequence holds (seq (#) seq1) ^\ k = (seq ^\ k) (#) (seq1 ^\ k)

proof 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))) )

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

theorem Th23: :: CFDIFF_1:23

for f1, f2 being PartFunc of COMPLEX,COMPLEX

for x0 being 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)) )

for x0 being 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 end;

theorem Th24: :: CFDIFF_1:24

for f1, f2 being PartFunc of COMPLEX,COMPLEX

for x0 being 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)) )

for x0 being 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 end;

theorem Th25: :: CFDIFF_1:25

for a being Complex

for f being PartFunc of COMPLEX,COMPLEX

for x0 being Complex st f is_differentiable_in x0 holds

( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) )

for f being PartFunc of COMPLEX,COMPLEX

for x0 being Complex st f is_differentiable_in x0 holds

( a (#) f is_differentiable_in x0 & diff ((a (#) f),x0) = a * (diff (f,x0)) )

proof end;

theorem Th26: :: CFDIFF_1:26

for f1, f2 being PartFunc of COMPLEX,COMPLEX

for x0 being 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))) )

for x0 being 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 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 Complex st x in Z holds

(f `| Z) /. x = 1r ) )

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 Complex st x in Z holds

(f `| Z) /. x = 1r ) )

proof 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 Complex st x in Z holds

((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )

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 Complex st x in Z holds

((f1 + f2) `| Z) /. x = (diff (f1,x)) + (diff (f2,x)) ) )

proof 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 Complex st x in Z holds

((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )

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 Complex st x in Z holds

((f1 - f2) `| Z) /. x = (diff (f1,x)) - (diff (f2,x)) ) )

proof end;

theorem :: CFDIFF_1:30

for a being 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 Complex st x in Z holds

((a (#) f) `| Z) /. x = a * (diff (f,x)) ) )

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 Complex st x in Z holds

((a (#) f) `| Z) /. x = a * (diff (f,x)) ) )

proof 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 Complex st x in Z holds

((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) )

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 Complex st x in Z holds

((f1 (#) f2) `| Z) /. x = ((f2 /. x) * (diff (f1,x))) + ((f1 /. x) * (diff (f2,x))) ) )

proof 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 Complex st x in Z holds

(f `| Z) /. x = 0c ) )

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 Complex st x in Z holds

(f `| Z) /. x = 0c ) )

proof end;

theorem :: CFDIFF_1:33

for a, b being Complex

for f being PartFunc of COMPLEX,COMPLEX

for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Complex st x in Z holds

f /. x = (a * x) + b ) holds

( f is_differentiable_on Z & ( for x being Complex st x in Z holds

(f `| Z) /. x = a ) )

for f being PartFunc of COMPLEX,COMPLEX

for Z being open Subset of COMPLEX st Z c= dom f & ( for x being Complex st x in Z holds

f /. x = (a * x) + b ) holds

( f is_differentiable_on Z & ( for x being Complex st x in Z holds

(f `| Z) /. x = a ) )

proof end;

theorem Th34: :: CFDIFF_1:34

for f being PartFunc of COMPLEX,COMPLEX

for x0 being Complex st f is_differentiable_in x0 holds

f is_continuous_in x0

for x0 being Complex st f is_differentiable_in x0 holds

f is_continuous_in x0

proof 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

for f being PartFunc of COMPLEX,COMPLEX st f is_differentiable_on X holds

f is_continuous_on X

proof 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

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

::$CT

theorem :: CFDIFF_1:38

for x0 being 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 )

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