let f be PartFunc of COMPLEX ,COMPLEX ; :: thesis: for u, v being PartFunc of (REAL 2),REAL
for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st <*x,y*> in dom v holds
x + (y * <i> ) in dom f ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) ) ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) ) ) & z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff u,xy0,1 = partdiff v,xy0,2 & partdiff u,xy0,2 = - (partdiff v,xy0,1) holds
( f is_differentiable_in z0 & u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 )
let u, v be PartFunc of (REAL 2),REAL ; :: thesis: for z0 being Complex
for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st <*x,y*> in dom v holds
x + (y * <i> ) in dom f ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) ) ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) ) ) & z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff u,xy0,1 = partdiff v,xy0,2 & partdiff u,xy0,2 = - (partdiff v,xy0,1) holds
( f is_differentiable_in z0 & u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 )
let z0 be Complex; :: thesis: for x0, y0 being Real
for xy0 being Element of REAL 2 st ( for x, y being Real st <*x,y*> in dom v holds
x + (y * <i> ) in dom f ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) ) ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) ) ) & z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff u,xy0,1 = partdiff v,xy0,2 & partdiff u,xy0,2 = - (partdiff v,xy0,1) holds
( f is_differentiable_in z0 & u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 )
let x0, y0 be Real; :: thesis: for xy0 being Element of REAL 2 st ( for x, y being Real st <*x,y*> in dom v holds
x + (y * <i> ) in dom f ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) ) ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) ) ) & z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff u,xy0,1 = partdiff v,xy0,2 & partdiff u,xy0,2 = - (partdiff v,xy0,1) holds
( f is_differentiable_in z0 & u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 )
let xy0 be Element of REAL 2; :: thesis: ( ( for x, y being Real st <*x,y*> in dom v holds
x + (y * <i> ) in dom f ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) ) ) & ( for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) ) ) & z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> & <>* u is_differentiable_in xy0 & <>* v is_differentiable_in xy0 & partdiff u,xy0,1 = partdiff v,xy0,2 & partdiff u,xy0,2 = - (partdiff v,xy0,1) implies ( f is_differentiable_in z0 & u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 ) )
assume that
AG2:
for x, y being Real st <*x,y*> in dom v holds
x + (y * <i> ) in dom f
and
A2:
for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom u & u . <*x,y*> = (Re f) . (x + (y * <i> )) )
and
A3:
for x, y being Real st x + (y * <i> ) in dom f holds
( <*x,y*> in dom v & v . <*x,y*> = (Im f) . (x + (y * <i> )) )
and
A4:
( z0 = x0 + (y0 * <i> ) & xy0 = <*x0,y0*> )
and
AG5:
<>* u is_differentiable_in xy0
and
AG6:
<>* v is_differentiable_in xy0
and
AG7:
partdiff u,xy0,1 = partdiff v,xy0,2
and
AG8:
partdiff u,xy0,2 = - (partdiff v,xy0,1)
; :: thesis: ( f is_differentiable_in z0 & u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 )
P1:
( u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & <*(partdiff u,xy0,1)*> = (diff (<>* u),xy0) . <*1,0 *> & <*(partdiff u,xy0,2)*> = (diff (<>* u),xy0) . <*0 ,1*> )
by Th02, A4, AG5;
P2:
( v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & <*(partdiff v,xy0,1)*> = (diff (<>* v),xy0) . <*1,0 *> & <*(partdiff v,xy0,2)*> = (diff (<>* v),xy0) . <*0 ,1*> )
by Th02, A4, AG6;
consider gu being PartFunc of (REAL-NS 2),(REAL-NS 1), guxy0 being Point of (REAL-NS 2) such that
X1:
( <>* u = gu & xy0 = guxy0 & gu is_differentiable_in guxy0 )
by AG5, PDIFF_1:def 7;
consider hu being PartFunc of (REAL-NS 2),(REAL-NS 1), huxy0 being Point of (REAL-NS 2) such that
X2:
( <>* u = hu & xy0 = huxy0 & diff (<>* u),xy0 = diff hu,huxy0 )
by AG5, PDIFF_1:def 8;
consider Nu being Neighbourhood of guxy0 such that
X3:
( Nu c= dom gu & ex Ru being REST of (REAL-NS 2),(REAL-NS 1) st
for xy being Point of (REAL-NS 2) st xy in Nu holds
(gu /. xy) - (gu /. guxy0) = ((diff gu,guxy0) . (xy - guxy0)) + (Ru /. (xy - guxy0)) )
by NDIFF_1:def 7, X1;
consider Ru being REST of (REAL-NS 2),(REAL-NS 1) such that
X4:
for xy being Point of (REAL-NS 2) st xy in Nu holds
(gu /. xy) - (gu /. guxy0) = ((diff gu,guxy0) . (xy - guxy0)) + (Ru /. (xy - guxy0))
by X3;
consider r1 being Real such that
X5:
( 0 < r1 & { xy where xy is Point of (REAL-NS 2) : ||.(xy - guxy0).|| < r1 } c= Nu )
by NFCONT_1:def 3;
Z5:
for x, y being Element of REAL st <*x,y*> in Nu holds
(u . <*x,y*>) - (u . <*x0,y0*>) = (((partdiff u,xy0,1) * (x - x0)) + ((partdiff u,xy0,2) * (y - y0))) + ((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>))
proof
let x,
y be
Element of
REAL ;
:: thesis: ( <*x,y*> in Nu implies (u . <*x,y*>) - (u . <*x0,y0*>) = (((partdiff u,xy0,1) * (x - x0)) + ((partdiff u,xy0,2) * (y - y0))) + ((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>)) )
assume Z510:
<*x,y*> in Nu
;
:: thesis: (u . <*x,y*>) - (u . <*x0,y0*>) = (((partdiff u,xy0,1) * (x - x0)) + ((partdiff u,xy0,2) * (y - y0))) + ((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>))
<*x,y*> in REAL 2
by FINSEQ_2:121;
then reconsider xy =
<*x,y*> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
<*1,0 *> in REAL 2
by FINSEQ_2:121;
then reconsider e1 =
<*1,0 *> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
<*0 ,1*> in REAL 2
by FINSEQ_2:121;
then reconsider e2 =
<*0 ,1*> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
rng u c= dom ((proj 1,1) " )
by PDIFF_1:2;
then Z514:
dom (<>* u) = dom u
by RELAT_1:46;
gu /. xy =
gu . xy
by X3, Z510, PARTFUN1:def 8
.=
(<>* u) /. <*x,y*>
by X1, X3, Z510, PARTFUN1:def 8
.=
<*(u /. <*x,y*>)*>
by X1, X3, Z510, Z514, Lm023
.=
<*(u . <*x,y*>)*>
by X1, X3, Z510, Z514, PARTFUN1:def 8
;
then Z513:
(proj 1,1) . (gu /. xy) = u . <*x,y*>
by PDIFF_1:1;
||.(guxy0 - guxy0).|| < r1
by NORMSP_1:10, X5;
then
guxy0 in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - guxy0).|| < r1 }
;
then W0511:
<*x0,y0*> in Nu
by X1, A4, X5;
gu /. guxy0 =
gu . guxy0
by A4, X1, X3, W0511, PARTFUN1:def 8
.=
(<>* u) /. <*x0,y0*>
by A4, X1, X3, W0511, PARTFUN1:def 8
.=
<*(u /. <*x0,y0*>)*>
by X1, X3, W0511, Z514, Lm023
.=
<*(u . <*x0,y0*>)*>
by W0511, X1, X3, Z514, PARTFUN1:def 8
;
then W513:
(proj 1,1) . (gu /. guxy0) = u . <*x0,y0*>
by PDIFF_1:1;
W600:
(u . <*x,y*>) - (u . <*x0,y0*>) =
(proj 1,1) . ((gu /. xy) - (gu /. guxy0))
by PDIFF_1:4, Z513, W513
.=
(proj 1,1) . (((diff gu,guxy0) . (xy - guxy0)) + (Ru /. (xy - guxy0)))
by X4, Z510
.=
((proj 1,1) . ((diff gu,guxy0) . (xy - guxy0))) + ((proj 1,1) . (Ru /. (xy - guxy0)))
by PDIFF_1:4
;
E0:
xy - guxy0 = <*(x - x0),(y - y0)*>
by Lm212, X1, A4;
E1:
(x - x0) * e1 =
<*((x - x0) * 1),((x - x0) * 0 )*>
by Lm213
.=
<*(x - x0),0 *>
;
E2:
(y - y0) * e2 =
<*((y - y0) * 0 ),((y - y0) * 1)*>
by Lm213
.=
<*0 ,(y - y0)*>
;
((x - x0) * e1) + ((y - y0) * e2) =
<*((x - x0) + 0 ),(0 + (y - y0))*>
by Lm212, E1, E2
.=
<*(x - x0),(y - y0)*>
;
then E4:
xy - guxy0 = ((x - x0) * e1) + ((y - y0) * e2)
by Lm212, X1, A4;
L0:
diff gu,
guxy0 is
LinearOperator of
(REAL-NS 2),
(REAL-NS 1)
by LOPBAN_1:def 10;
W610:
(diff gu,guxy0) . (xy - guxy0) =
((diff gu,guxy0) . ((x - x0) * e1)) + ((diff gu,guxy0) . ((y - y0) * e2))
by E4, L0, LOPBAN_1:def 5
.=
((x - x0) * ((diff gu,guxy0) . e1)) + ((diff gu,guxy0) . ((y - y0) * e2))
by L0, LOPBAN_1:def 6
.=
((x - x0) * ((diff gu,guxy0) . e1)) + ((y - y0) * ((diff gu,guxy0) . e2))
by L0, LOPBAN_1:def 6
;
Ru is
total
by NDIFF_1:def 5;
then W0700:
dom Ru = the
carrier of
(REAL-NS 2)
by PARTFUN1:def 4;
thus (u . <*x,y*>) - (u . <*x0,y0*>) =
(((proj 1,1) . ((x - x0) * ((diff gu,guxy0) . e1))) + ((proj 1,1) . ((y - y0) * ((diff gu,guxy0) . e2)))) + ((proj 1,1) . (Ru /. (xy - guxy0)))
by W600, W610, PDIFF_1:4
.=
(((x - x0) * ((proj 1,1) . ((diff gu,guxy0) . e1))) + ((proj 1,1) . ((y - y0) * ((diff gu,guxy0) . e2)))) + ((proj 1,1) . (Ru /. (xy - guxy0)))
by PDIFF_1:4
.=
(((x - x0) * ((proj 1,1) . <*(partdiff u,xy0,1)*>)) + ((y - y0) * ((proj 1,1) . <*(partdiff u,xy0,2)*>))) + ((proj 1,1) . (Ru /. (xy - guxy0)))
by PDIFF_1:4, X1, X2, P1
.=
(((x - x0) * (partdiff u,xy0,1)) + ((y - y0) * ((proj 1,1) . <*(partdiff u,xy0,2)*>))) + ((proj 1,1) . (Ru /. (xy - guxy0)))
by PDIFF_1:1
.=
(((x - x0) * (partdiff u,xy0,1)) + ((y - y0) * (partdiff u,xy0,2))) + ((proj 1,1) . (Ru /. (xy - guxy0)))
by PDIFF_1:1
.=
(((partdiff u,xy0,1) * (x - x0)) + ((partdiff u,xy0,2) * (y - y0))) + ((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>))
by W0700, PARTFUN1:def 8, E0
;
:: thesis: verum
end;
consider gv being PartFunc of (REAL-NS 2),(REAL-NS 1), gvxy0 being Point of (REAL-NS 2) such that
Y1:
( <>* v = gv & xy0 = gvxy0 & gv is_differentiable_in gvxy0 )
by AG6, PDIFF_1:def 7;
consider hv being PartFunc of (REAL-NS 2),(REAL-NS 1), hvxy0 being Point of (REAL-NS 2) such that
Y2:
( <>* v = hv & xy0 = hvxy0 & diff (<>* v),xy0 = diff hv,hvxy0 )
by AG6, PDIFF_1:def 8;
consider Nv being Neighbourhood of gvxy0 such that
Y3:
( Nv c= dom gv & ex Rv being REST of (REAL-NS 2),(REAL-NS 1) st
for xy being Point of (REAL-NS 2) st xy in Nv holds
(gv /. xy) - (gv /. gvxy0) = ((diff gv,gvxy0) . (xy - gvxy0)) + (Rv /. (xy - gvxy0)) )
by NDIFF_1:def 7, Y1;
consider Rv being REST of (REAL-NS 2),(REAL-NS 1) such that
Y4:
for xy being Point of (REAL-NS 2) st xy in Nv holds
(gv /. xy) - (gv /. gvxy0) = ((diff gv,gvxy0) . (xy - gvxy0)) + (Rv /. (xy - gvxy0))
by Y3;
consider r2 being Real such that
Y5:
( 0 < r2 & { xy where xy is Point of (REAL-NS 2) : ||.(xy - gvxy0).|| < r2 } c= Nv )
by NFCONT_1:def 3;
W5:
for x, y being Element of REAL st <*x,y*> in Nv holds
(v . <*x,y*>) - (v . <*x0,y0*>) = (((partdiff v,xy0,1) * (x - x0)) + ((partdiff v,xy0,2) * (y - y0))) + ((proj 1,1) . (Rv . <*(x - x0),(y - y0)*>))
proof
let x,
y be
Element of
REAL ;
:: thesis: ( <*x,y*> in Nv implies (v . <*x,y*>) - (v . <*x0,y0*>) = (((partdiff v,xy0,1) * (x - x0)) + ((partdiff v,xy0,2) * (y - y0))) + ((proj 1,1) . (Rv . <*(x - x0),(y - y0)*>)) )
assume Z510:
<*x,y*> in Nv
;
:: thesis: (v . <*x,y*>) - (v . <*x0,y0*>) = (((partdiff v,xy0,1) * (x - x0)) + ((partdiff v,xy0,2) * (y - y0))) + ((proj 1,1) . (Rv . <*(x - x0),(y - y0)*>))
<*x,y*> in REAL 2
by FINSEQ_2:121;
then reconsider xy =
<*x,y*> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
<*1,0 *> in REAL 2
by FINSEQ_2:121;
then reconsider e1 =
<*1,0 *> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
<*0 ,1*> in REAL 2
by FINSEQ_2:121;
then reconsider e2 =
<*0 ,1*> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
rng v c= dom ((proj 1,1) " )
by PDIFF_1:2;
then Z514:
dom (<>* v) = dom v
by RELAT_1:46;
gv /. xy =
gv . xy
by Y3, Z510, PARTFUN1:def 8
.=
(<>* v) /. <*x,y*>
by Y1, Y3, Z510, PARTFUN1:def 8
.=
<*(v /. <*x,y*>)*>
by Z510, Y3, Y1, Z514, Lm023
.=
<*(v . <*x,y*>)*>
by Z510, Y3, Y1, Z514, PARTFUN1:def 8
;
then Z513:
(proj 1,1) . (gv /. xy) = v . <*x,y*>
by PDIFF_1:1;
||.(gvxy0 - gvxy0).|| < r2
by NORMSP_1:10, Y5;
then
gvxy0 in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 }
;
then W0511:
<*x0,y0*> in Nv
by Y1, A4, Y5;
gv /. gvxy0 =
gv . gvxy0
by A4, Y1, Y3, W0511, PARTFUN1:def 8
.=
(<>* v) /. <*x0,y0*>
by A4, Y1, Y3, W0511, PARTFUN1:def 8
.=
<*(v /. <*x0,y0*>)*>
by Y1, Y3, W0511, Z514, Lm023
.=
<*(v . <*x0,y0*>)*>
by Y1, Y3, W0511, Z514, PARTFUN1:def 8
;
then W513:
(proj 1,1) . (gv /. gvxy0) = v . <*x0,y0*>
by PDIFF_1:1;
W600:
(v . <*x,y*>) - (v . <*x0,y0*>) =
(proj 1,1) . ((gv /. xy) - (gv /. gvxy0))
by PDIFF_1:4, Z513, W513
.=
(proj 1,1) . (((diff gv,gvxy0) . (xy - gvxy0)) + (Rv /. (xy - gvxy0)))
by Y4, Z510
.=
((proj 1,1) . ((diff gv,gvxy0) . (xy - gvxy0))) + ((proj 1,1) . (Rv /. (xy - gvxy0)))
by PDIFF_1:4
;
E0:
xy - gvxy0 = <*(x - x0),(y - y0)*>
by Lm212, Y1, A4;
E1:
(x - x0) * e1 =
<*((x - x0) * 1),((x - x0) * 0 )*>
by Lm213
.=
<*(x - x0),0 *>
;
E2:
(y - y0) * e2 =
<*((y - y0) * 0 ),((y - y0) * 1)*>
by Lm213
.=
<*0 ,(y - y0)*>
;
E3:
((x - x0) * e1) + ((y - y0) * e2) =
<*((x - x0) + 0 ),(0 + (y - y0))*>
by Lm212, E1, E2
.=
<*(x - x0),(y - y0)*>
;
L0:
diff gv,
gvxy0 is
LinearOperator of
(REAL-NS 2),
(REAL-NS 1)
by LOPBAN_1:def 10;
W610:
(diff gv,gvxy0) . (xy - gvxy0) =
((diff gv,gvxy0) . ((x - x0) * e1)) + ((diff gv,gvxy0) . ((y - y0) * e2))
by E0, E3, L0, LOPBAN_1:def 5
.=
((x - x0) * ((diff gv,gvxy0) . e1)) + ((diff gv,gvxy0) . ((y - y0) * e2))
by L0, LOPBAN_1:def 6
.=
((x - x0) * ((diff gv,gvxy0) . e1)) + ((y - y0) * ((diff gv,gvxy0) . e2))
by L0, LOPBAN_1:def 6
;
Rv is
total
by NDIFF_1:def 5;
then W0700:
dom Rv = the
carrier of
(REAL-NS 2)
by PARTFUN1:def 4;
thus (v . <*x,y*>) - (v . <*x0,y0*>) =
(((proj 1,1) . ((x - x0) * ((diff gv,gvxy0) . e1))) + ((proj 1,1) . ((y - y0) * ((diff gv,gvxy0) . e2)))) + ((proj 1,1) . (Rv /. (xy - gvxy0)))
by W600, W610, PDIFF_1:4
.=
(((x - x0) * ((proj 1,1) . ((diff gv,gvxy0) . e1))) + ((proj 1,1) . ((y - y0) * ((diff gv,gvxy0) . e2)))) + ((proj 1,1) . (Rv /. (xy - gvxy0)))
by PDIFF_1:4
.=
(((x - x0) * ((proj 1,1) . ((diff gv,gvxy0) . e1))) + ((y - y0) * ((proj 1,1) . ((diff gv,gvxy0) . e2)))) + ((proj 1,1) . (Rv /. (xy - gvxy0)))
by PDIFF_1:4
.=
(((x - x0) * (partdiff v,xy0,1)) + ((y - y0) * ((proj 1,1) . <*(partdiff v,xy0,2)*>))) + ((proj 1,1) . (Rv /. (xy - gvxy0)))
by Y1, Y2, P2, PDIFF_1:1
.=
(((x - x0) * (partdiff v,xy0,1)) + ((y - y0) * (partdiff v,xy0,2))) + ((proj 1,1) . (Rv /. (xy - gvxy0)))
by PDIFF_1:1
.=
(((partdiff v,xy0,1) * (x - x0)) + ((partdiff v,xy0,2) * (y - y0))) + ((proj 1,1) . (Rv . <*(x - x0),(y - y0)*>))
by W0700, PARTFUN1:def 8, E0
;
:: thesis: verum
end;
set r0 = min (r1 / 2),(r2 / 2);
set N = { y where y is Complex : |.(y - z0).| < min (r1 / 2),(r2 / 2) } ;
LmZ0:
for x, y being Element of REAL st x + (y * <i> ) in { y where y is Complex : |.(y - z0).| < min (r1 / 2),(r2 / 2) } holds
( abs (x - x0) < r1 / 2 & abs (y - y0) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 )
proof
let x,
y be
Element of
REAL ;
:: thesis: ( x + (y * <i> ) in { y where y is Complex : |.(y - z0).| < min (r1 / 2),(r2 / 2) } implies ( abs (x - x0) < r1 / 2 & abs (y - y0) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 ) )
assume Z1:
x + (y * <i> ) in { y where y is Complex : |.(y - z0).| < min (r1 / 2),(r2 / 2) }
;
:: thesis: ( abs (x - x0) < r1 / 2 & abs (y - y0) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 )
Q0:
(
min (r1 / 2),
(r2 / 2) <= r1 / 2 &
min (r1 / 2),
(r2 / 2) <= r2 / 2 )
by XXREAL_0:17;
Q01:
ex
w being
Complex st
(
w = x + (y * <i> ) &
|.(w - z0).| < min (r1 / 2),
(r2 / 2) )
by Z1;
abs (x - x0) <= |.((x - x0) + ((y - y0) * <i> )).|
by Lm038;
then Z01:
abs (x - x0) < min (r1 / 2),
(r2 / 2)
by Q01, A4, XXREAL_0:2;
abs (y - y0) <= |.((x - x0) + ((y - y0) * <i> )).|
by Lm038;
then Z02:
abs (y - y0) < min (r1 / 2),
(r2 / 2)
by Q01, A4, XXREAL_0:2;
<*x,y*> in REAL 2
by FINSEQ_2:121;
then reconsider xy =
<*x,y*> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
thus
abs (x - x0) < r1 / 2
by Q0, XXREAL_0:2, Z01;
:: thesis: ( abs (y - y0) < r1 / 2 & abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 )
thus
abs (y - y0) < r1 / 2
by Q0, XXREAL_0:2, Z02;
:: thesis: ( abs (x - x0) < r2 / 2 & abs (y - y0) < r2 / 2 )
thus
abs (x - x0) < r2 / 2
by Q0, XXREAL_0:2, Z01;
:: thesis: abs (y - y0) < r2 / 2
thus
abs (y - y0) < r2 / 2
by Q0, XXREAL_0:2, Z02;
:: thesis: verum
end;
Z0:
now let x,
y be
Element of
REAL ;
:: thesis: ( x + (y * <i> ) in { y where y is Complex : |.(y - z0).| < min (r1 / 2),(r2 / 2) } implies (f /. (x + (y * <i> ))) - (f /. (x0 + (y0 * <i> ))) = (((partdiff u,xy0,1) + (<i> * (partdiff v,xy0,1))) * ((x - x0) + ((y - y0) * <i> ))) + (((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj 1,1) . (Rv . <*(x - x0),(y - y0)*>)) * <i> )) )assume Z1:
x + (y * <i> ) in { y where y is Complex : |.(y - z0).| < min (r1 / 2),(r2 / 2) }
;
:: thesis: (f /. (x + (y * <i> ))) - (f /. (x0 + (y0 * <i> ))) = (((partdiff u,xy0,1) + (<i> * (partdiff v,xy0,1))) * ((x - x0) + ((y - y0) * <i> ))) + (((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj 1,1) . (Rv . <*(x - x0),(y - y0)*>)) * <i> ))
rng v c= dom ((proj 1,1) " )
by PDIFF_1:2;
then ZZZ:
dom (<>* v) = dom v
by RELAT_1:46;
Q0:
(
min (r1 / 2),
(r2 / 2) <= r1 / 2 &
min (r1 / 2),
(r2 / 2) <= r2 / 2 )
by XXREAL_0:17;
Q01:
ex
w being
Complex st
(
w = x + (y * <i> ) &
|.(w - z0).| < min (r1 / 2),
(r2 / 2) )
by Z1;
abs (x - x0) <= |.((x - x0) + ((y - y0) * <i> )).|
by Lm038;
then Z01:
abs (x - x0) < min (r1 / 2),
(r2 / 2)
by Q01, A4, XXREAL_0:2;
abs (y - y0) <= |.((x - x0) + ((y - y0) * <i> )).|
by Lm038;
then Z02:
abs (y - y0) < min (r1 / 2),
(r2 / 2)
by Q01, A4, XXREAL_0:2;
<*x,y*> in REAL 2
by FINSEQ_2:121;
then reconsider xy =
<*x,y*> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
ZX1:
xy - guxy0 = <*(x - x0),(y - y0)*>
by X1, A4, Lm212;
Z03:
abs (x - x0) < r1 / 2
by Q0, XXREAL_0:2, Z01;
Z04:
abs (y - y0) < r1 / 2
by Q0, XXREAL_0:2, Z02;
Z41:
||.(xy - guxy0).|| <= (abs (x - x0)) + (abs (y - y0))
by ZX1, Lm036;
(abs (x - x0)) + (abs (y - y0)) < (r1 / 2) + (r1 / 2)
by Z03, Z04, XREAL_1:10;
then
||.(xy - guxy0).|| < r1
by Z41, XXREAL_0:2;
then Z0031:
xy in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - guxy0).|| < r1 }
;
ZY1:
xy - gvxy0 = <*(x - x0),(y - y0)*>
by Y1, A4, Lm212;
Z05:
abs (x - x0) < r2 / 2
by Q0, XXREAL_0:2, Z01;
Z06:
abs (y - y0) < r2 / 2
by Q0, XXREAL_0:2, Z02;
Z61:
||.(xy - gvxy0).|| <= (abs (x - x0)) + (abs (y - y0))
by ZY1, Lm036;
(abs (x - x0)) + (abs (y - y0)) < (r2 / 2) + (r2 / 2)
by Z05, Z06, XREAL_1:10;
then
||.(xy - gvxy0).|| < r2
by Z61, XXREAL_0:2;
then Z0041:
xy in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 }
;
then
<*x,y*> in Nv
by Y5;
then Z02:
x + (y * <i> ) in dom f
by ZZZ, Y1, Y3, AG2;
then Z02R:
x + (y * <i> ) in dom (Re f)
by Def2;
Z02I:
x + (y * <i> ) in dom (Im f)
by Def3, Z02;
||.(gvxy0 - gvxy0).|| < r2
by NORMSP_1:10, Y5;
then
gvxy0 in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 }
;
then
<*x0,y0*> in Nv
by A4, Y1, Y5;
then Z021:
x0 + (y0 * <i> ) in dom f
by ZZZ, Y1, Y3, AG2;
then Z021R:
x0 + (y0 * <i> ) in dom (Re f)
by Def2;
Z021I:
x0 + (y0 * <i> ) in dom (Im f)
by Z021, Def3;
Z05:
f /. (x + (y * <i> )) =
(Re (f /. (x + (y * <i> )))) + ((Im (f /. (x + (y * <i> )))) * <i> )
by COMPLEX1:29
.=
((Re f) . (x + (y * <i> ))) + ((Im (f /. (x + (y * <i> )))) * <i> )
by Z02R, Def2
.=
((Re f) . (x + (y * <i> ))) + (((Im f) . (x + (y * <i> ))) * <i> )
by Z02I, Def3
;
Z06:
f /. (x0 + (y0 * <i> )) =
(Re (f /. (x0 + (y0 * <i> )))) + ((Im (f /. (x0 + (y0 * <i> )))) * <i> )
by COMPLEX1:29
.=
((Re f) . (x0 + (y0 * <i> ))) + ((Im (f /. (x0 + (y0 * <i> )))) * <i> )
by Z021R, Def2
.=
((Re f) . (x0 + (y0 * <i> ))) + (((Im f) . (x0 + (y0 * <i> ))) * <i> )
by Z021I, Def3
;
Z07:
(f /. (x + (y * <i> ))) - (f /. (x0 + (y0 * <i> ))) =
((u . <*x,y*>) + (((Im f) . (x + (y * <i> ))) * <i> )) - (((Re f) . (x0 + (y0 * <i> ))) + (((Im f) . (x0 + (y0 * <i> ))) * <i> ))
by Z05, Z06, A2, Z02
.=
((u . <*x,y*>) + ((v . <*x,y*>) * <i> )) - (((Re f) . (x0 + (y0 * <i> ))) + (((Im f) . (x0 + (y0 * <i> ))) * <i> ))
by A3, Z02
.=
((u . <*x,y*>) + ((v . <*x,y*>) * <i> )) - ((u . <*x0,y0*>) + (((Im f) . (x0 + (y0 * <i> ))) * <i> ))
by A2, Z021
.=
((u . <*x,y*>) + ((v . <*x,y*>) * <i> )) - ((u . <*x0,y0*>) + ((v . <*x0,y0*>) * <i> ))
by A3, Z021
.=
((u . <*x,y*>) - (u . <*x0,y0*>)) + (((v . <*x,y*>) - (v . <*x0,y0*>)) * <i> )
;
Z08:
(u . <*x,y*>) - (u . <*x0,y0*>) =
(((partdiff u,xy0,1) * (x - x0)) + ((partdiff u,xy0,2) * (y - y0))) + ((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>))
by Z5, Z0031, X5
.=
(((partdiff u,xy0,1) * (x - x0)) + (((<i> * (partdiff v,xy0,1)) * (y - y0)) * <i> )) + ((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>))
by AG8
;
Z09:
((v . <*x,y*>) - (v . <*x0,y0*>)) * <i> = ((((partdiff v,xy0,1) * (x - x0)) + ((partdiff u,xy0,1) * (y - y0))) + ((proj 1,1) . (Rv . <*(x - x0),(y - y0)*>))) * <i>
by W5, Z0041, Y5, AG7;
thus
(f /. (x + (y * <i> ))) - (f /. (x0 + (y0 * <i> ))) = (((partdiff u,xy0,1) + (<i> * (partdiff v,xy0,1))) * ((x - x0) + ((y - y0) * <i> ))) + (((proj 1,1) . (Ru . <*(x - x0),(y - y0)*>)) + (((proj 1,1) . (Rv . <*(x - x0),(y - y0)*>)) * <i> ))
by Z07, Z08, Z09;
:: thesis: verum end;
reconsider a = (partdiff u,xy0,1) + (<i> * (partdiff v,xy0,1)) as Complex by XCMPLX_0:def 2;
deffunc H1( Element of COMPLEX ) -> Element of COMPLEX = a * $1;
consider L being Function of COMPLEX ,COMPLEX such that
Z20:
for x being Element of COMPLEX holds L . x = H1(x)
from FUNCT_2:sch 4();
for z being Complex holds L /. z = a * z
by Z20;
then reconsider L = L as C_LINEAR by CFDIFF_1:def 4;
defpred S1[ Element of COMPLEX , Element of COMPLEX ] means $2 = ((proj 1,1) . (Ru . <*(Re $1),(Im $1)*>)) + (((proj 1,1) . (Rv . <*(Re $1),(Im $1)*>)) * <i> );
consider R being Function of COMPLEX ,COMPLEX such that
Z30:
for z being Element of COMPLEX holds S1[z,R . z]
from FUNCT_2:sch 10(S1);
for h being convergent_to_0 Complex_Sequence holds
( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 )
proof
let h be
convergent_to_0 Complex_Sequence;
:: thesis: ( (h " ) (#) (R /* h) is convergent & lim ((h " ) (#) (R /* h)) = 0 )
V1:
now let r be
Real;
:: thesis: ( 0 < r implies ex M being Element of NAT st
for n being Element of NAT st M <= n holds
|.((((h " ) (#) (R /* h)) . n) - 0c ).| < r )assume AZ01:
0 < r
;
:: thesis: ex M being Element of NAT st
for n being Element of NAT st M <= n holds
|.((((h " ) (#) (R /* h)) . n) - 0c ).| < r
Ru is
total
by NDIFF_1:def 5;
then consider d1 being
Real such that AZ2:
(
d1 > 0 & ( for
z being
Point of
(REAL-NS 2) st
z <> 0. (REAL-NS 2) &
||.z.|| < d1 holds
(||.z.|| " ) * ||.(Ru /. z).|| < r / 2 ) )
by NDIFF_1:26, AZ01;
Rv is
total
by NDIFF_1:def 5;
then consider d2 being
Real such that AZ3:
(
d2 > 0 & ( for
z being
Point of
(REAL-NS 2) st
z <> 0. (REAL-NS 2) &
||.z.|| < d2 holds
(||.z.|| " ) * ||.(Rv /. z).|| < r / 2 ) )
by NDIFF_1:26, AZ01;
AZ31:
(
h is
convergent &
lim h = 0 )
by CFDIFF_1:def 1;
set d =
min d1,
d2;
0 < min d1,
d2
by AZ2, AZ3, XXREAL_0:21;
then consider M being
Element of
NAT such that AZ4:
for
n being
Element of
NAT st
M <= n holds
|.((h . n) - 0 ).| < min d1,
d2
by AZ31, COMSEQ_2:def 5;
XXX:
(
min d1,
d2 <= d1 &
min d1,
d2 <= d2 )
by XXREAL_0:17;
now let n be
Element of
NAT ;
:: thesis: ( M <= n implies |.((((h " ) (#) (R /* h)) . n) - 0 ).| < r )assume AZ0:
M <= n
;
:: thesis: |.((((h " ) (#) (R /* h)) . n) - 0 ).| < rset x =
Re (h . n);
set y =
Im (h . n);
<*(Re (h . n)),(Im (h . n))*> in REAL 2
by FINSEQ_2:121;
then reconsider z =
<*(Re (h . n)),(Im (h . n))*> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
Ru is
total
by NDIFF_1:def 5;
then W0700:
dom Ru = the
carrier of
(REAL-NS 2)
by PARTFUN1:def 4;
Rv is
total
by NDIFF_1:def 5;
then V0700:
dom Rv = the
carrier of
(REAL-NS 2)
by PARTFUN1:def 4;
AZ5:
z <> 0. (REAL-NS 2)
YYY0:
|.((h . n) - 0 ).| < min d1,
d2
by AZ4, AZ0;
h . n = (Re (h . n)) + ((Im (h . n)) * <i> )
by COMPLEX1:29;
then AZ6:
||.z.|| = |.(h . n).|
by Lm034;
AZ7:
||.z.|| < d1
by AZ6, YYY0, XXX, XXREAL_0:2;
AZ8:
||.z.|| < d2
by AZ6, YYY0, XXX, XXREAL_0:2;
AZ9:
(||.z.|| " ) * ||.(Ru /. z).|| < r / 2
by AZ5, AZ7, AZ2;
AZ10:
(||.z.|| " ) * ||.(Rv /. z).|| < r / 2
by AZ5, AZ8, AZ3;
AZ11:
R /. (h . n) = ((proj 1,1) . (Ru . <*(Re (h . n)),(Im (h . n))*>)) + (((proj 1,1) . (Rv . <*(Re (h . n)),(Im (h . n))*>)) * <i> )
by Z30;
h . n <> 0
by COMSEQ_1:4;
then
0 < |.(h . n).|
by COMPLEX1:133;
then AZS1:
(|.(h . n).| " ) * |.(R /. (h . n)).| <= (|.(h . n).| " ) * ((abs ((proj 1,1) . (Ru . <*(Re (h . n)),(Im (h . n))*>))) + (abs ((proj 1,1) . (Rv . <*(Re (h . n)),(Im (h . n))*>))))
by AZ11, Lm035, XREAL_1:66;
AZ013:
abs ((proj 1,1) . (Ru . <*(Re (h . n)),(Im (h . n))*>)) =
abs ((proj 1,1) . (Ru /. z))
by PARTFUN1:def 8, W0700
.=
||.(Ru /. z).||
by Lm037
;
AZ014:
abs ((proj 1,1) . (Rv . <*(Re (h . n)),(Im (h . n))*>)) =
abs ((proj 1,1) . (Rv /. z))
by PARTFUN1:def 8, V0700
.=
||.(Rv /. z).||
by Lm037
;
((|.(h . n).| " ) * (abs ((proj 1,1) . (Ru . <*(Re (h . n)),(Im (h . n))*>)))) + ((|.(h . n).| " ) * (abs ((proj 1,1) . (Rv . <*(Re (h . n)),(Im (h . n))*>)))) < (r / 2) + (r / 2)
by XREAL_1:10, AZ014, AZ10, AZ013, AZ6, AZ9;
then
(|.(h . n).| " ) * |.(R /. (h . n)).| < r
by AZS1, XXREAL_0:2;
then
|.((h . n) " ).| * |.(R /. (h . n)).| < r
by COMPLEX1:152;
then AZ141:
|.(((h . n) " ) * (R /. (h . n))).| < r
by COMPLEX1:151;
dom R = COMPLEX
by FUNCT_2:def 1;
then
rng h c= dom R
;
then
|.(((h . n) " ) * ((R /* h) . n)).| < r
by AZ141, FUNCT_2:186;
then
|.(((h " ) . n) * ((R /* h) . n)).| < r
by VALUED_1:10;
hence
|.((((h " ) (#) (R /* h)) . n) - 0 ).| < r
by VALUED_1:5;
:: thesis: verum end; hence
ex
M being
Element of
NAT st
for
n being
Element of
NAT st
M <= n holds
|.((((h " ) (#) (R /* h)) . n) - 0c ).| < r
;
:: thesis: verum end;
then
(h " ) (#) (R /* h) is
convergent
by COMSEQ_2:def 4;
hence
(
(h " ) (#) (R /* h) is
convergent &
lim ((h " ) (#) (R /* h)) = 0 )
by COMSEQ_2:def 5, V1;
:: thesis: verum
end;
then reconsider R = R as C_REST by CFDIFF_1:def 3;
reconsider N = { y where y is Complex : |.(y - z0).| < min (r1 / 2),(r2 / 2) } as Neighbourhood of z0 by X5, Y5, XXREAL_0:21, CFDIFF_1:6;
now let z be
set ;
:: thesis: ( z in N implies z in dom f )assume AZ1:
z in N
;
:: thesis: z in dom fthen reconsider zz =
z as
Complex ;
set x =
Re zz;
set y =
Im zz;
AZ2:
z = (Re zz) + ((Im zz) * <i> )
by COMPLEX1:29;
Z1:
(Re zz) + ((Im zz) * <i> ) in N
by AZ1, COMPLEX1:29;
rng v c= dom ((proj 1,1) " )
by PDIFF_1:2;
then ZZZ:
dom (<>* v) = dom v
by RELAT_1:46;
<*(Re zz),(Im zz)*> in REAL 2
by FINSEQ_2:121;
then reconsider xy =
<*(Re zz),(Im zz)*> as
Point of
(REAL-NS 2) by REAL_NS1:def 4;
ZY1:
xy - gvxy0 = <*((Re zz) - x0),((Im zz) - y0)*>
by Y1, A4, Lm212;
Z05:
abs ((Re zz) - x0) < r2 / 2
by Z1, LmZ0;
Z06:
abs ((Im zz) - y0) < r2 / 2
by Z1, LmZ0;
Z61:
||.(xy - gvxy0).|| <= (abs ((Re zz) - x0)) + (abs ((Im zz) - y0))
by ZY1, Lm036;
(abs ((Re zz) - x0)) + (abs ((Im zz) - y0)) < (r2 / 2) + (r2 / 2)
by Z05, Z06, XREAL_1:10;
then
||.(xy - gvxy0).|| < r2
by Z61, XXREAL_0:2;
then
xy in { wxy where wxy is Point of (REAL-NS 2) : ||.(wxy - gvxy0).|| < r2 }
;
then
<*(Re zz),(Im zz)*> in Nv
by Y5;
hence
z in dom f
by AZ2, ZZZ, Y1, Y3, AG2;
:: thesis: verum end;
then Z50:
N c= dom f
by TARSKI:def 3;
now let z be
Complex;
:: thesis: ( z in N implies (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0)) )assume Z51:
z in N
;
:: thesis: (f /. z) - (f /. z0) = (L /. (z - z0)) + (R /. (z - z0))set x =
Re z;
set y =
Im z;
Z53:
z = (Re z) + ((Im z) * <i> )
by COMPLEX1:29;
Z55:
z - z0 = ((Re z) - x0) + (((Im z) - y0) * <i> )
by A4, Z53;
Re (z - z0) = (Re z) - x0
by Z55, COMPLEX1:28;
then Z57:
<*(Re (z - z0)),(Im (z - z0))*> = <*((Re z) - x0),((Im z) - y0)*>
by Z55, COMPLEX1:28;
thus (f /. z) - (f /. z0) =
(((partdiff u,xy0,1) + (<i> * (partdiff v,xy0,1))) * (((Re z) - x0) + (((Im z) - y0) * <i> ))) + (((proj 1,1) . (Ru . <*((Re z) - x0),((Im z) - y0)*>)) + (((proj 1,1) . (Rv . <*((Re z) - x0),((Im z) - y0)*>)) * <i> ))
by A4, Z53, Z0, Z51
.=
(L /. (z - z0)) + (((proj 1,1) . (Ru . <*((Re z) - x0),((Im z) - y0)*>)) + (((proj 1,1) . (Rv . <*((Re z) - x0),((Im z) - y0)*>)) * <i> ))
by Z20, A4, Z53
.=
(L /. (z - z0)) + (R /. (z - z0))
by Z30, Z57
;
:: thesis: verum end;
then
f is_differentiable_in z0
by CFDIFF_1:def 6, Z50;
hence
( f is_differentiable_in z0 & u is_partial_differentiable_in xy0,1 & u is_partial_differentiable_in xy0,2 & v is_partial_differentiable_in xy0,1 & v is_partial_differentiable_in xy0,2 & Re (diff f,z0) = partdiff u,xy0,1 & Re (diff f,z0) = partdiff v,xy0,2 & Im (diff f,z0) = - (partdiff u,xy0,2) & Im (diff f,z0) = partdiff v,xy0,1 )
by A2, A3, A4, Th01; :: thesis: verum