:: Cauchy-Riemann Differential Equations of Complex Functions
:: by Hiroshi Yamazaki , Yasunari Shidama , Chanapat Pacharapokin and Yatsuka Nakamura
::
:: Received April 7, 2009
:: Copyright (c) 2009-2021 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, PARTFUN1, REAL_1, SEQ_1, COMSEQ_1, SEQ_2,
CARD_1, FUNCT_1, COMPLEX1, RELAT_1, NAT_1, ORDINAL2, ARYTM_3, XXREAL_0,
ARYTM_1, FDIFF_1, VALUED_0, XCMPLX_0, VALUED_1, FINSEQ_1, PDIFF_1,
AFINSQ_1, CARD_3, RCOMP_1, TARSKI, CFDIFF_1, FUNCT_2, XXREAL_1, PRE_TOPC,
REAL_NS1, BINOP_2, NORMSP_1, EUCLID, MCART_1, RVSUM_1, SQUARE_1,
SUPINF_2, STRUCT_0, LOPBAN_1, FUNCT_7;
notations TARSKI, SUBSET_1, RELAT_1, FUNCT_1, FUNCT_2, RELSET_1, PARTFUN1,
BINOP_1, ORDINAL1, NUMBERS, XXREAL_0, XCMPLX_0, BINOP_2, XREAL_0,
COMPLEX1, REAL_1, VALUED_1, SEQ_1, SEQ_2, RLVECT_1, COMSEQ_1, COMSEQ_2,
COMSEQ_3, PRE_TOPC, STRUCT_0, RVSUM_1, FINSEQ_1, FINSEQ_2, FINSEQ_7,
SQUARE_1, EUCLID, NORMSP_0, NORMSP_1, REAL_NS1, LOPBAN_1, NFCONT_1,
FDIFF_1, NDIFF_1, PDIFF_1, CFDIFF_1, RCOMP_1;
constructors REAL_1, SQUARE_1, RSSPACE3, SEQ_2, BINOP_2, FINSEQ_7, NFCONT_1,
RCOMP_1, FDIFF_1, NDIFF_1, PDIFF_1, CFDIFF_1, COMSEQ_2, COMSEQ_3,
RVSUM_1, RELSET_1, BINOP_1, NUMBERS, EXTREAL1, FINSEQ_4;
registrations RELSET_1, STRUCT_0, ORDINAL1, MEMBERED, NUMBERS, XBOOLE_0,
XREAL_0, XXREAL_0, XCMPLX_0, FUNCT_2, REAL_NS1, COMSEQ_3, VALUED_0,
VALUED_1, SEQ_4, FDIFF_1, CFDIFF_1, EUCLID, COMSEQ_2, SQUARE_1, RVSUM_1,
CFUNCT_1;
requirements SUBSET, REAL, BOOLE, NUMERALS, ARITHM;
equalities LOPBAN_1, EUCLID, COMPLEX1, PDIFF_1, VALUED_1, RVSUM_1, XCMPLX_0;
expansions COMPLEX1, PDIFF_1;
theorems TARSKI, ABSVALUE, XBOOLE_1, XREAL_0, EUCLID, XREAL_1, XXREAL_0,
RCOMP_1, RLVECT_1, SEQ_4, COMPLEX1, SEQ_1, SEQ_2, FINSEQ_1, XCMPLX_1,
VALUED_1, BINOP_2, FINSEQ_2, FINSEQ_7, RVSUM_1, RELAT_1, FUNCT_1,
FUNCT_2, NORMSP_1, LOPBAN_1, PARTFUN1, NFCONT_1, FDIFF_1, NDIFF_1,
REAL_NS1, NUMBERS, FUNCT_3, SQUARE_1, CFUNCT_1, CFDIFF_1, PDIFF_1,
XCMPLX_0, COMSEQ_1, COMSEQ_2, COMSEQ_3, JGRAPH_1, VECTSP_1, NORMSP_0,
CARD_1, ORDINAL1;
schemes FUNCT_2;
begin
reserve n, m for Element of NAT;
reserve z for Complex;
Lm1: for seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real
st seq=cseq & seq is convergent & lim seq = rlim holds lim cseq = rlim
proof
let seq be Real_Sequence, cseq be Complex_Sequence, rlim be Real such
that
A1: seq = cseq & seq is convergent & lim seq = rlim;
reconsider clim = rlim as Element of COMPLEX by XCMPLX_0:def 2;
cseq is convergent & for p be Real st 0
(#) seq holds seq is
non-zero iff cseq is non-zero
proof
let seq, cseq be Complex_Sequence such that
A1: cseq = (#) seq;
thus seq is non-zero implies cseq is non-zero by A1,COMSEQ_1:38;
A2: (#) seq is non-zero implies seq is non-zero
proof
assume
A3: (#) seq is non-zero;
now
let n;
( (#) seq).n <> 0c by A3,COMSEQ_1:4;
then * seq.n <> 0c by VALUED_1:6;
hence seq.n <> 0c;
end;
hence thesis by COMSEQ_1:4;
end;
assume cseq is non-zero;
hence seq is non-zero by A1,A2;
end;
Lm5: for seq, cseq be Complex_Sequence st cseq = (#) seq holds seq is
0-convergent non-zero iff cseq is 0-convergent non-zero
proof
let seq, cseq be Complex_Sequence such that
A1: cseq = (#) seq;
thus seq is 0-convergent non-zero implies cseq is 0-convergent non-zero
proof
assume
A2: seq is 0-convergent non-zero;
then lim seq = 0 by CFDIFF_1:def 1;
then
A3: lim ( (#) seq) = * 0 by A2,COMSEQ_2:18
.= 0;
(#) seq is non-zero & (#) seq is convergent by A2,COMSEQ_1:38;
hence cseq is 0-convergent non-zero by A1,A3,CFDIFF_1:def 1;
end;
assume
A4: cseq is 0-convergent non-zero;
then
A5: seq is non-zero by A1,Lm4;
(-) (#) ( (#) seq ) is convergent by A1,A4;
then ((-) * ) (#) seq is convergent by CFUNCT_1:22;
then
A6: seq is convergent by CFUNCT_1:26;
lim ( (#) seq) = 0 by A1,A4,CFDIFF_1:def 1;
then * lim seq = 0 by A6,COMSEQ_2:18;
hence seq is 0-convergent non-zero by A6,A5,CFDIFF_1:def 1;
end;
:: Cauchy-Riemann
theorem Th2:
for f be PartFunc of COMPLEX, COMPLEX, u,v be PartFunc of REAL 2,
REAL, z0 be Complex, x0, y0 be Real,
xy0 be Element of REAL 2 st (for x, y be
Real st x+y* in dom f holds <*x,y*> in dom u & u.<*x,y*> = (Re f).(x+y*))
& (for x,y be Real st x+y* in dom f holds <*x,y*> in dom v & v.<*x,y*> = (Im
f).(x+y*)) & z0 = x0+y0* & xy0 = <*x0,y0*> & f is_differentiable_in z0
holds 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)
proof
let f be PartFunc of COMPLEX,COMPLEX, u,v be PartFunc of REAL 2,REAL, z0 be
Complex, x00,y00 be Real ,xy0 be Element of REAL 2 such that
A1: for x,y be Real st x+y* in dom f holds <*x,y*> in dom u & u.<*x,y
*> = (Re f).(x+y*) and
A2: for x,y be Real st x+y* in dom f holds <*x,y*> in dom v & v.<*x,y
*> = (Im f).(x+y*) and
A3: z0 = x00+y00* and
A4: xy0 = <*x00,y00*> and
A5: f is_differentiable_in z0;
reconsider x0 = x00, y0 = y00 as Element of REAL by XREAL_0:def 1;
A6: z0 = x0+y0* by A3;
A7: xy0 = <*x0,y0*> by A4;
deffunc LDF2(Real) = In((Im diff(f,z0))* $1,REAL);
consider LD2 be Function of REAL, REAL such that
A8: for x be Element of REAL holds LD2.x = LDF2(x) from FUNCT_2:sch 4;
A9: for x be Real holds LD2.x = (Im diff(f,z0))* x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD2.x = LDF2(x) by A8;
hence thesis;
end;
reconsider LD2 as LinearFunc by A9,FDIFF_1:def 3;
deffunc LDF1(Real) = In((Re diff(f,z0)) * $1,REAL);
consider LD1 be Function of REAL, REAL such that
A10: for x be Element of REAL holds LD1.x = LDF1(x) from FUNCT_2:sch 4;
A11: for x be Real holds LD1.x = (Re diff(f,z0)) * x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD1.x = LDF1(x) by A10;
hence thesis;
end;
A12: for y be Real holds (v*reproj(2,xy0)).y = v.<*x0,y*>
proof
let y be Real;
reconsider yy=y, dwa=2 as Element of REAL by XREAL_0:def 1;
yy in REAL;
then yy in dom (reproj(2,xy0)) by PDIFF_1:def 5;
hence (v*reproj(2,xy0)).y = v.((reproj(2,xy0)).y) by FUNCT_1:13
.=v.(Replace(xy0,2,yy)) by PDIFF_1:def 5
.=v.<*x0,yy*> by A7,FINSEQ_7:14
.=v.<*x0,y*>;
end;
A13: for y be Real holds (u*reproj(2,xy0)).y=u.<*x0,y*>
proof
let y be Real;
reconsider yy=y as Element of REAL by XREAL_0:def 1;
y in REAL by XREAL_0:def 1;
then y in dom (reproj(2,xy0)) by PDIFF_1:def 5;
hence (u*reproj(2,xy0)).y = u.((reproj(2,xy0)).y) by FUNCT_1:13
.= u.(Replace(xy0,2,yy)) by PDIFF_1:def 5
.= u.<*x0,y*> by A7,FINSEQ_7:14;
end;
A14: proj(2,2).xy0 = xy0.2 by PDIFF_1:def 1
.= y0 by A7,FINSEQ_1:44;
reconsider LD1 as LinearFunc by A11,FDIFF_1:def 3;
deffunc LDF3(Real) = In(-(Im diff(f,z0)) * $1,REAL);
consider LD3 be Function of REAL,REAL such that
A15: for x be Element of REAL holds LD3.x = LDF3(x) from FUNCT_2:sch 4;
A16: for x be Real holds LD3.x = -(Im diff(f,z0)) * x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD3.x = LDF3(x) by A15;
hence thesis;
end;
for x be Real holds LD3.x = (-(Im diff(f,z0)))* x
proof
let x be Real;
thus LD3.x = -(Im diff(f,z0)) * x by A16
.= (-(Im diff(f,z0)))* x;
end;
then reconsider LD3 as LinearFunc by FDIFF_1:def 3;
reconsider z0 as Element of COMPLEX by XCMPLX_0:def 2;
consider N being Neighbourhood of z0 such that
A17: N c= dom f and
A18: ex L be C_LinearFunc, R be C_RestFunc st diff(f,z0) = L/.1r &
for z being Complex
st z in N holds f/.z-f/.z0 = L/.(z-z0)+R/.(z-z0) by A5,CFDIFF_1:def 7;
consider L be C_LinearFunc, R be C_RestFunc such that
A19: diff(f,z0) = L/.1r & for z be Complex st
z in N holds f/.z-f/.z0 = L/.(z-z0) +R/.(z-z0) by A18;
deffunc RF4(Real) = In((Im R).($1*),REAL);
consider R4 be Function of REAL, REAL such that
A20: for y be Element of REAL holds R4.y =RF4(y) from FUNCT_2:sch 4;
A21: for z be Complex st z in N holds f/.z-f/.z0 = diff(f,z0)*(z-z0)+R/.(z-z0)
proof
let z be Complex;
assume
A22: z in N;
reconsider z as Element of COMPLEX by XCMPLX_0:def 2;
consider a0 be Complex such that
A23: for w be Complex holds L/.w = a0*w by CFDIFF_1:def 4;
L/.(1r*(z-z0)) = a0*1r*(z-z0) by A23
.= (L/.1r)*(z-z0) by A23;
hence thesis by A19,A22;
end;
A24: for x,y be Real st x+y* in N & x0+y0* in N holds
f.(x+y*)-f.(x0+y0*) =
diff(f,z0)*((x+y*)-(x0+y0*)) + R/.((x+y*)-(x0+y0*))
proof
let x,y be Real;
assume
A25: x+y* in N & x0+y0* in N;
then f.(x+y*) = f/.(x+y*) & f.(x0+y0*) = f/.(x0+y0*)
by A17,PARTFUN1:def 6;
hence thesis by A21,A25,A6;
end;
A26: dom R = COMPLEX by PARTFUN1:def 2;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R4/*h) is
convergent & lim ((h")(#)(R4/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz0 =h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 as 0-convergent non-zero Complex_Sequence by Lm3;
set hz=(#)hz0;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm5;
now
A27: rng hz c= dom R by A26;
dom R4=REAL by PARTFUN1:def 2;
then
A28: rng h c= dom R4;
let n be Nat;
A29: n in NAT by ORDINAL1:def 12;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A30: Im ((h.nn)" ) = 0 & Re ((h.nn)") = (h.nn)" by COMPLEX1:def 1,def 2;
A31: hz.n = (h.n)* by VALUED_1:6;
reconsider hn = h.n as Real;
(h.n)* in COMPLEX by XCMPLX_0:def 2;
then
A32: (h.n)* in dom Im R by Th1;
thus ((h")(#)(R4/*h)).n = (h").n*((R4/*h).n) by SEQ_1:8
.= (h.n)"*((R4/*h).n) by VALUED_1:10
.= (h.n)"*(R4.hn) by A28,FUNCT_2:108,A29
.= (h.nn)"*RF4(hn) by A20
.= (h.n)"* (Im R).((h.n)*)
.= Re ((h.n)" )* Im (R.((h.n)*)) + Re (R.((h.n)*)) * Im ((h.
n)") by A32,A30,COMSEQ_3:def 4
.= Im (((hz.n)/) "* (R.(hz.n))) by A31,COMPLEX1:9
.= Im (( /(hz.n)) * (R.(hz.n))) by XCMPLX_1:213
.= Im ( *(hz").n * (R.(hz.n))) by VALUED_1:10
.= Im ( *((hz").n * (R.(hz.n))))
.= Re ( ) * Im ((hz").n * (R/.(hz.n))) + Re ((hz").n * (R/.(hz.n
)))*Im ( ) by COMPLEX1:9
.= Re ((hz").n * (R/*hz).n ) by A27,COMPLEX1:7,FUNCT_2:109,A29
.= Re (( (hz")(#)(R/*hz)).n ) by VALUED_1:5;
end;
then
A33: (h")(#)(R4/*h) = Re ((hz")(#)(R/*hz)) by COMSEQ_3:def 5;
(hz")(#)(R/*hz) is convergent & lim ((hz")(#)(R/*hz)) = 0 by CFDIFF_1:def 3
;
hence thesis by A33,COMPLEX1:4,COMSEQ_3:41;
end;
then reconsider R4 as RestFunc by FDIFF_1:def 2;
deffunc RF2(Real) = In((Re R).($1*),REAL);
A34: dom R = COMPLEX by PARTFUN1:def 2;
consider R2 be Function of REAL,REAL such that
A35: for y be Element of REAL holds R2.y =RF2(y) from FUNCT_2:sch 4;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R2/*h) is
convergent & lim ((h")(#)(R2/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz0 =h as Complex_Sequence by FUNCT_2:6;
reconsider hz0 as 0-convergent non-zero Complex_Sequence by Lm3;
set hz=(#)hz0;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm5;
A36: (hz")(#)(R/*hz) is convergent by CFDIFF_1:def 3;
dom R= COMPLEX by PARTFUN1:def 2;
then
A37: rng hz c= dom R;
now
dom R2=REAL by PARTFUN1:def 2;
then
A38: rng h c= dom R2;
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A39: Im ((h.nn)" ) = 0 & Re ((h.nn)") = (h.nn)" by COMPLEX1:def 1,def 2;
A40: hz.n=(h.n)* by VALUED_1:6;
dom Re R = COMPLEX by Th1;
then
A41: (h.n)* in dom Re R by XCMPLX_0:def 2;
A42: R.(hz.n) = R/.(hz.n);
reconsider hn = h.n as Real;
thus ((h")(#)(R2/*h)).n = (h").n*((R2/*h).n) by SEQ_1:8
.= (h.n)"*((R2/*h).n) by VALUED_1:10
.= (h.nn)"*(R2.(h.n)) by A38,FUNCT_2:108
.= (h.nn)"*(RF2(hn)) by A35
.= (h.n)"* (Re R).((h.n)*)
.= Re ((h.n)" )* Re (R.((h.n)*)) -Im ((h.n)") *Im (R.((h.n)*
)) by A41,A39,COMSEQ_3:def 3
.= Re (((hz.n)/) "* (R.(hz.n))) by A40,COMPLEX1:9
.= Re (( /(hz.n)) * (R.(hz.n))) by XCMPLX_1:213
.= Re ( *(hz").n * (R.(hz.n))) by VALUED_1:10
.= Re ( *((hz").n * (R.(hz.n))))
.= Re * Re ((hz").n * (R.(hz.n))) -
Im * Im ((hz").n * (R.(hz.n))) by COMPLEX1:9
.= -Im ((hz").nn * (R/*hz).nn ) by A42,A37,COMPLEX1:7,FUNCT_2:109
.= -Im (( (hz")(#)(R/*hz)).n ) by VALUED_1:5
.= - (Im ((hz")(#)(R/*hz))).n by COMSEQ_3:def 6;
end;
then
A43: (h")(#)(R2/*h) = - Im ((hz")(#)(R/*hz)) by SEQ_1:10;
lim ((hz")(#)(R/*hz)) = 0 by CFDIFF_1:def 3;
then lim Im ((hz")(#)(R/*hz)) = Im 0 by A36,COMSEQ_3:41;
then lim ((h")(#)(R2/*h)) = -Im 0 by A43,A36,SEQ_2:10
.= 0 by COMPLEX1:4;
hence thesis by A43,A36,SEQ_2:9;
end;
then reconsider R2 as RestFunc by FDIFF_1:def 2;
consider r0 be Real such that
A44: 0 in N
proof
let y be Real;
|. (x0+y*) - z0 .| = |.(y-y0)*.| by A6;
then
A47: |. (x0+y*) - z0 .| = |.(y-y0).|*|..| by COMPLEX1:65;
assume y in Ny0;
then x0+y* is Complex & |. (x0+y*) - z0 .| < r0 by A47,COMPLEX1:49
,RCOMP_1:1;
then (x0+y*) in {w where w is Complex : |.w-z0.| < r0};
hence (x0+y*) in N by A45;
end;
A48: for x, y be Real holds diff(f,z0)*((x+y*)-(x0+y0*)) = ((Re diff(f
,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0)) + ((Im diff(f,z0)) * (x-x0)+(Re diff(f,
z0))*(y-y0))*
proof
let x, y be Real;
thus diff(f,z0)*((x+y*)-(x0+y0*)) = ( Re ( diff(f,z0)) + (Im diff(f,
z0)) * )*((x-x0)+(y-y0)*) by COMPLEX1:13
.= ((Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0)) + ((Im diff(f,z0)
) * (x-x0)+(Re diff(f,z0))*(y-y0))*;
end;
A49: for x,y be Real holds Re (diff(f,z0)*((x+y*)-(x0+y0*))) = (Re
diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0)
proof
let x, y be Real;
thus Re (diff(f,z0)*((x+y*)-(x0+y0*))) = Re (((Re diff(f,z0)) * (x-
x0)-(Im diff(f,z0))*(y-y0)) + ((Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0))
* ) by A48
.= (Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y-y0) by COMPLEX1:12;
end;
A50: for y be Real st y in Ny0 holds u.<*x0,y*> - u.<*x0,y0*> = -(Im diff(f,
z0))*(y-y0) + (Re R).((x0-x0)+ (y-y0)*)
proof
let y be Real;
(x0+y*)-(x0+y0*) in dom R by A34,XCMPLX_0:def 2;
then
A51: (y-y0)* in dom Re R by COMSEQ_3:def 3;
assume y in Ny0;
then
A52: x0+y* in N by A46;
then x0+y* in dom f by A17;
then
A53: x0+y* in dom Re f by COMSEQ_3:def 3;
A54: x0+y0* in N by A6,CFDIFF_1:7;
then x0+y0* in dom f by A17;
then
A55: x0+y0* in dom Re f by COMSEQ_3:def 3;
u.<*x0,y*> - u.<*x0,y0*> = (Re f).(x0+y*) - u.<*x0,y0*> by A1,A17,A52
.=(Re f).(x0+y*) - (Re f).(x0+y0*) by A1,A17,A54
.= Re (f.(x0+y*)) -(Re f).(x0+y0*) by A53,COMSEQ_3:def 3
.= Re (f.(x0+y*)) -Re (f.(x0+y0*)) by A55,COMSEQ_3:def 3
.= Re (f.(x0+y*)-f.(x0+y0*)) by COMPLEX1:19
.= Re ( diff(f,z0)*((x0+y*)-(x0+y0*)) +R/.((x0+y*)-(x0+y0*
))) by A24,A52,A54
.= Re ( diff(f,z0)*((x0+y*)-(x0+y0*))) +Re (R/.((x0+y*)-(x0+
y0*))) by COMPLEX1:8
.= (Re diff(f,z0))*(x0-x0)-(Im diff(f,z0))*(y-y0) +Re (R/.((x0+y*)-
(x0+y0*))) by A49
.= (Re diff(f,z0))*0-(Im diff(f,z0))*(y-y0) +Re (R/.((x0+y*)-
(x0+y0*)))
.= -(Im diff(f,z0))*(y-y0) +Re (R/.((x0+y*)-(x0+y0*)))
.= -(Im diff(f,z0))*(y-y0) +Re (R.((x0+y*)-(x0+y0*)))
.= -(Im diff(f,z0))*(y-y0) + (Re R).((x0-x0)+ (y-y0)*)
by A51,COMSEQ_3:def 3;
hence thesis;
end;
A56: for y be Real
st y in Ny0 holds (u*reproj(2,xy0)).y - (u*reproj(2,xy0)
).y0 = LD3.(y-y0) + R2.(y-y0)
proof
let y be Real;
assume
A57: y in Ny0;
reconsider yy0 = y-y0 as Element of REAL by XREAL_0:def 1;
thus (u*reproj(2,xy0)).y - (u*reproj(2,xy0)).y0
= u.<*x0,y*> - (u*reproj(2,xy0)).y0 by A13
.= u.<*x0,y*> - u.<*x0,y0*> by A13
.= -(Im diff(f,z0))*(y-y0) + (Re R).((x0-x0)+(y-y0)*) by A50,A57
.= LD3.(y-y0) + (Re R).((x0-x0)+ (y-y0)*) by A16
.= LD3.(y-y0) + RF2(yy0)
.= LD3.(y-y0) + R2.(y-y0) by A35;
end;
A58: for x,y be Real holds Im (diff(f,z0)*((x+y*)-(x0+y0*))) = (Im
diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0)
proof
let x, y be Real;
thus Im (diff(f,z0)*((x+y*)-(x0+y0*))) = Im (((Re diff(f,z0)) * (x-
x0)-(Im diff(f,z0))*(y-y0)) + ((Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0))
* ) by A48
.= (Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y-y0) by COMPLEX1:12;
end;
A59: for y be Real st y in Ny0 holds v.<*x0,y*> - v.<*x0,y0*> = (Re diff(f,
z0))*(y-y0) + (Im R).((x0-x0)+(y-y0)*)
proof
let y be Real;
(x0+y*)-(x0+y0*) in dom R by A34,XCMPLX_0:def 2;
then
A60: (y-y0)* in dom Im R by COMSEQ_3:def 4;
assume y in Ny0;
then
A61: x0+y* in N by A46;
then x0+y* in dom f by A17;
then
A62: x0+y* in dom Im f by COMSEQ_3:def 4;
A63: x0+y0* in N by A6,CFDIFF_1:7;
then x0+y0* in dom f by A17;
then
A64: x0+y0* in dom Im f by COMSEQ_3:def 4;
v.<*x0,y*> - v.<*x0,y0*> = (Im f).(x0+y*) - v.<*x0,y0*> by A2,A17,A61
.=(Im f).(x0+y*) - (Im f).(x0+y0*) by A2,A17,A63
.= Im (f.(x0+y*)) -(Im f).(x0+y0*) by A62,COMSEQ_3:def 4
.= Im (f.(x0+y*)) -Im (f.(x0+y0*)) by A64,COMSEQ_3:def 4
.= Im (f.(x0+y*)-f.(x0+y0*)) by COMPLEX1:19
.= Im ( diff(f,z0)*((x0+y*)-(x0+y0*)) +R/.((x0+y*)-(x0+y0*
))) by A24,A61,A63
.= Im ( diff(f,z0)*((x0+y*)-(x0+y0*))) + Im (R/.((x0+y*)-(x0+
y0*))) by COMPLEX1:8
.= (Im diff(f,z0)) * (x0-x0)+(Re diff(f,z0))*(y-y0) + Im (R/.((x0+y*
)-(x0+y0*))) by A58
.= (Im diff(f,z0)) * (x0-x0)+(Re diff(f,z0))*(y-y0) + Im (R.((x0+y*
)-(x0+y0*)))
.= (Re diff(f,z0))*(y-y0) + (Im R).((x0-x0)+(y-y0)*)
by A60,COMSEQ_3:def 4;
hence thesis;
end;
A65: for y be Real
st y in Ny0 holds (v*reproj(2,xy0)).y - (v*reproj(2,xy0)
).y0 = LD1.(y-y0) + R4.(y-y0)
proof
let y be Real;
assume
A66: y in Ny0;
reconsider yy0 = y-y0 as Element of REAL by XREAL_0:def 1;
thus (v*reproj(2,xy0)).y - (v*reproj(2,xy0)).y0 = v.<*x0,y*> - (v*reproj(2
,xy0)).y0 by A12
.= v.<*x0,y*> - v.<*x0,y0*> by A12
.= (Re diff(f,z0))*(y-y0) + (Im R).((x0-x0)+(y-y0)*) by A59,A66
.= LD1.(y-y0) + (Im R).((x0-x0)+(y-y0) *) by A11
.= LD1.(y-y0) + RF4(yy0)
.= LD1.(y-y0) + R4.(y-y0) by A20;
end;
now
let s be object;
assume s in (reproj(2,xy0)).:Ny0;
then consider y being Element of REAL such that
A67: y in Ny0 and
A68: s = (reproj(2,xy0)).y by FUNCT_2:65;
A69: x0+y* in N by A46,A67;
s=Replace(xy0,2,y) by A68,PDIFF_1:def 5
.= <* x0, y *> by A7,FINSEQ_7:14;
hence s in dom v by A2,A17,A69;
end;
then dom (reproj(2,xy0)) = REAL & (reproj(2,xy0)).:Ny0 c= dom v by
FUNCT_2:def 1,TARSKI:def 3;
then
A70: Ny0 c= dom (v*reproj(2,xy0)) by FUNCT_3:3;
then
A71: v*reproj(2,xy0) is_differentiable_in proj(2,2).xy0 by A14,A65,
FDIFF_1:def 4;
A72: for x be Element of REAL holds (v*reproj(1,xy0)).x=v.<*x,y0*>
proof
let x be Element of REAL;
x in REAL;
then x in dom (reproj(1,xy0)) by PDIFF_1:def 5;
hence (v*reproj(1,xy0)).x = v.((reproj(1,xy0)).x) by FUNCT_1:13
.= v.(Replace(xy0,1,x)) by PDIFF_1:def 5
.= v.<*x,y0*> by A7,FINSEQ_7:13;
end;
now
let s be object;
assume s in (reproj(2,xy0)).:Ny0;
then consider y being Element of REAL such that
A73: y in Ny0 and
A74: s = (reproj(2,xy0)).y by FUNCT_2:65;
A75: x0+y* in N by A46,A73;
s=Replace(xy0,2,y) by A74,PDIFF_1:def 5
.= <* x0, y *> by A7,FINSEQ_7:14;
hence s in dom u by A1,A17,A75;
end;
then dom (reproj(2,xy0)) = REAL & (reproj(2,xy0)).:Ny0 c= dom u by
FUNCT_2:def 1,TARSKI:def 3;
then
A76: Ny0 c= dom (u*reproj(2,xy0)) by FUNCT_3:3;
then
A77: u*reproj(2,xy0) is_differentiable_in proj(2,2).xy0 by A14,A56,
FDIFF_1:def 4;
LD3.1 = - (Im diff(f,z0))*1 by A16
.= - (Im diff(f,z0));
then
A78: partdiff(u,xy0,2) = -Im diff(f,z0) by A14,A56,A76,A77,FDIFF_1:def 5;
A79: LD1.1 = (Re diff(f,z0))*1 by A11
.= Re diff(f,z0);
A80: proj(1,2).xy0 = xy0.1 by PDIFF_1:def 1
.= x0 by A7,FINSEQ_1:44;
set Nx0 = ].x0-r0,x0+r0.[;
reconsider Nx0 as Neighbourhood of x0 by A44,RCOMP_1:def 6;
deffunc RF3(Real) = In((Im R).$1,REAL);
consider R3 be Function of REAL, REAL such that
A81: for y be Element of REAL holds R3.y =RF3(y) from FUNCT_2:sch 4;
A82: for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R3/*h) is
convergent & lim ((h")(#)(R3/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz =h as Complex_Sequence by FUNCT_2:6;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm3;
now
dom R = COMPLEX by PARTFUN1:def 2;
then
A83: rng hz c= dom R;
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A84: Im ((h.nn)") = 0 & Re ((h.nn)") = (h.nn)" by COMPLEX1:def 1,def 2;
A85: dom R3=REAL by PARTFUN1:def 2;
then
A86: rng h c= dom R3;
dom R3 c= dom Im R by A85,Th1,NUMBERS:11;
then
A87: h.nn in dom Im R by A85,TARSKI:def 3;
thus ((h")(#)(R3/*h)).n = (h").n*((R3/*h).n) by SEQ_1:8
.= (h.n)"*((R3/*h).n) by VALUED_1:10
.= (h.nn)"*(R3.(h.nn)) by A86,FUNCT_2:108
.= (h.nn)"*(RF3(h.nn)) by A81
.= (h.n)"* (Im R).(h.n)
.= Re ((h.n)")*Im (R/.(h.n)) + Re (R/.(h.n))*Im ((h.n)")
by A87,A84,COMSEQ_3:def 4
.= Im ((h.n)"* (R/.(h.n))) by COMPLEX1:9
.= Im ((hz").n * (R/.(hz.n))) by VALUED_1:10
.= Im ((hz").nn * (R/*hz).nn) by A83,FUNCT_2:109
.= Im (((hz")(#)(R/*hz)).n) by VALUED_1:5;
end;
then
A88: (h")(#)(R3/*h) = Im ((hz")(#)(R/*hz)) by COMSEQ_3:def 6;
(hz")(#)(R/*hz) is convergent & lim ((hz")(#)(R/*hz)) = 0
by CFDIFF_1:def 3;
hence thesis by A88,COMPLEX1:4,COMSEQ_3:41;
end;
deffunc RF1(Real) = In((Re R).$1,REAL);
consider R1 be Function of REAL,REAL such that
A89: for x be Element of REAL holds R1.x = RF1(x) from FUNCT_2:sch 4;
reconsider R3 as RestFunc by A82,FDIFF_1:def 2;
A90: for x be Real st x in Nx0 holds x+y0* in N
proof
let x be Real;
assume x in Nx0;
then |.x-x0.| < r0 by RCOMP_1:1;
then x+y0* is Complex & |. (x+y0*) - z0 .| < r0 by A6;
then (x+y0*) in {y where y is Complex : |.y-z0.| < r0};
hence (x+y0*) in N by A45;
end;
A91: for x be Real st x in Nx0 holds v.<*x,y0*> - v.<*x0,y0*> = (Im diff(f,
z0)) * (x-x0)+ (Im R).((x-x0) + 0 *)
proof
let x be Real;
(x+y0*)-(x0+y0*) in dom R by A34,XCMPLX_0:def 2;
then
A92: x-x0 in dom Im R by COMSEQ_3:def 4;
assume x in Nx0;
then
A93: x+y0* in N by A90;
then x+y0* in dom f by A17;
then
A94: x+y0* in dom Im f by COMSEQ_3:def 4;
A95: x0+y0* in N by A6,CFDIFF_1:7;
then x0+y0* in dom f by A17;
then
A96: x0+y0* in dom Im f by COMSEQ_3:def 4;
v.<*x,y0*> - v.<*x0,y0*> = (Im f).(x+y0*) - v.<*x0,y0*> by A2,A17,A93
.=(Im f).(x+y0*) - (Im f).(x0+y0*) by A2,A17,A95
.= Im (f.(x+y0*)) -(Im f).(x0+y0*) by A94,COMSEQ_3:def 4
.= Im (f.(x+y0*)) -Im (f.(x0+y0*)) by A96,COMSEQ_3:def 4
.= Im (f.(x+y0*)-f.(x0+y0*)) by COMPLEX1:19
.= Im ( diff(f,z0)*((x+y0*)-(x0+y0*)) +R/.((x+y0*)-(x0+y0*
))) by A24,A93,A95
.= Im ( diff(f,z0)*((x+y0*)-(x0+y0*))) + Im (R/.((x+y0*)-(x0+
y0*))) by COMPLEX1:8
.= (Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y0-y0) + Im (R/.((x+y0*
)-(x0+y0*))) by A58
.= (Im diff(f,z0)) * (x-x0)+(Re diff(f,z0))*(y0-y0) + Im (R.((x+y0*
)-(x0+y0*)))
.= (Im diff(f,z0)) * (x-x0)+ (Im R).((x-x0) + 0 *)
by A92,COMSEQ_3:def 4;
hence thesis;
end;
A97: for x be Real
st x in Nx0 holds (v*reproj(1,xy0)).x - (v*reproj(1,xy0)
).x0 = LD2.(x-x0)+ R3.(x-x0)
proof
let x be Real;
assume
A98: x in Nx0;
reconsider xx0 = x-x0 as Element of REAL by XREAL_0:def 1;
x in REAL by XREAL_0:def 1;
hence (v*reproj(1,xy0)).x - (v*reproj(1,xy0)).x0
= v.<*x,y0*> - (v*reproj(1,xy0)).x0 by A72
.= v.<*x,y0*> - v.<*x0,y0*> by A72
.= (Im diff(f,z0))*(x-x0) + (Im R).((x-x0)+ 0 *) by A91,A98
.= LD2.(x-x0) + (Im R).((x-x0)+ 0 *) by A9
.= LD2.(x-x0) + RF3(xx0)
.= LD2.(x-x0) + R3.(xx0) by A81
.= LD2.(x-x0) + R3.(x-x0);
end;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R1/*h) is
convergent & lim ((h")(#)(R1/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
rng h c= COMPLEX by NUMBERS:11,XBOOLE_1:1;
then reconsider hz = h as Complex_Sequence by FUNCT_2:6;
reconsider hz as 0-convergent non-zero Complex_Sequence by Lm3;
now
dom R= COMPLEX by PARTFUN1:def 2;
then
A99: rng hz c= dom R;
let n be Nat;
reconsider nn=n as Element of NAT by ORDINAL1:def 12;
A100: Im ((h.nn)") = 0 & Re ((h.nn)") = (h.nn)" by COMPLEX1:def 1,def 2;
A101: dom R1=REAL by PARTFUN1:def 2;
then
A102: rng h c= dom R1;
dom R1 c= dom Re R by A101,Th1,NUMBERS:11;
then
A103: h.nn in dom Re R by A101,TARSKI:def 3;
thus ((h")(#)(R1/*h)).n = (h").n*((R1/*h).n) by SEQ_1:8
.= (h.n)"*((R1/*h).n) by VALUED_1:10
.= (h.nn)"*(R1/.(h.nn)) by A102,FUNCT_2:109
.= (h.nn)"* RF1(h.nn) by A89
.= (h.n)"* (Re R).(h.n)
.= Re ((h.n)")* Re (R.(h.n)) - Im ((h.n)")* Im (R.(h.n)) by A103,A100,
COMSEQ_3:def 3
.= Re ((h.n)"* (R.(h.n))) by COMPLEX1:9
.= Re ((hz").n * (R/.(hz.n))) by VALUED_1:10
.= Re ((hz").nn * (R/*hz).nn) by A99,FUNCT_2:109
.= Re (( (hz")(#)(R/*hz) ).n ) by VALUED_1:5;
end;
then
A104: (h")(#)(R1/*h) = Re ((hz")(#)(R/*hz)) by COMSEQ_3:def 5;
(hz")(#)(R/*hz) is convergent & lim ((hz")(#)(R/*hz)) = 0
by CFDIFF_1:def 3;
hence thesis by A104,COMPLEX1:4,COMSEQ_3:41;
end;
then reconsider R1 as RestFunc by FDIFF_1:def 2;
A105: LD2.1 = (Im diff(f,z0))*1 by A9
.= Im diff(f,z0);
A106: for x be Element of REAL holds (u*reproj(1,xy0)).x=u.<*x,y0*>
proof
let x be Element of REAL;
x in REAL;
then x in dom (reproj(1,xy0)) by PDIFF_1:def 5;
hence (u*reproj(1,xy0)).x = u.((reproj(1,xy0)).x) by FUNCT_1:13
.= u.(Replace(xy0,1,x)) by PDIFF_1:def 5
.= u.<*x,y0*> by A7,FINSEQ_7:13;
end;
A107: for x be Real st x in Nx0 holds u.<*x,y0*> - u.<*x0,y0*> = (Re diff(f,
z0)) * (x-x0) + (Re R).((x-x0)+0 *)
proof
let x be Real;
(x+y0*)-(x0+y0*) in dom R by A34, XCMPLX_0:def 2;
then
A108: (x-x0) in dom Re R by COMSEQ_3:def 3;
assume x in Nx0;
then
A109: x+y0* in N by A90;
then x+y0* in dom f by A17;
then
A110: x+y0* in dom Re f by COMSEQ_3:def 3;
A111: x0+y0* in N by A6,CFDIFF_1:7;
then x0+y0* in dom f by A17;
then
A112: x0+y0* in dom Re f by COMSEQ_3:def 3;
u.<*x,y0*> - u.<*x0,y0*> = (Re f).(x+y0*) - u.<*x0,y0*> by A1,A17,A109
.=(Re f).(x+y0*) - (Re f).(x0+y0*) by A1,A17,A111
.= Re (f.(x+y0*)) -(Re f).(x0+y0*) by A110,COMSEQ_3:def 3
.= Re (f.(x+y0*)) -Re (f.(x0+y0*)) by A112,COMSEQ_3:def 3
.= Re (f.(x+y0*)-f.(x0+y0*)) by COMPLEX1:19
.= Re ( diff(f,z0)*((x+y0*)-(x0+y0*)) + R/.((x+y0*)-(x0+y0*
))) by A24,A109,A111
.= Re ( diff(f,z0)*((x+y0*)-(x0+y0*))) + Re (R/.((x+y0*)-(x0+
y0*))) by COMPLEX1:8
.= (Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y0-y0) + Re (R/.((x+y0*
)-(x0+y0*))) by A49
.= (Re diff(f,z0)) * (x-x0)-(Im diff(f,z0))*(y0-y0) + Re (R.((x+y0*
)-(x0+y0*)))
.= (Re diff(f,z0)) * (x-x0) + (Re R).((x-x0)+0 *)
by A108,COMSEQ_3:def 3;
hence thesis;
end;
A113: for x be Real
st x in Nx0 holds (u*reproj(1,xy0)).x - (u*reproj(1,xy0)
).x0 = LD1.(x-x0) + R1.(x-x0)
proof
let x be Real;
assume
A114: x in Nx0;
reconsider xx0 = x-x0 as Element of REAL by XREAL_0:def 1;
x in REAL by XREAL_0:def 1;
hence (u*reproj(1,xy0)).x - (u*reproj(1,xy0)).x0
= u.<*x,y0*> - (u*reproj(1
,xy0)).x0 by A106
.= u.<*x,y0*> - u.<*x0,y0*> by A106
.= (Re diff(f,z0)) * (x-x0) + (Re R).((x-x0)+0 *) by A107,A114
.= LD1.(x-x0) + (Re R).((x-x0)+0 *) by A11
.= LD1.(x-x0) + RF1(xx0)
.= LD1.(x-x0) + R1.(xx0) by A89
.= LD1.(x-x0) + R1.(x-x0);
end;
now
let s be object;
assume s in (reproj(1,xy0)).:Nx0;
then consider x being Element of REAL such that
A115: x in Nx0 and
A116: s = (reproj(1,xy0)).x by FUNCT_2:65;
A117: x+y0* in N by A90,A115;
s=Replace(xy0,1,x) by A116,PDIFF_1:def 5
.= <* x, y0 *> by A7,FINSEQ_7:13;
hence s in dom v by A2,A17,A117;
end;
then dom (reproj(1,xy0)) = REAL & (reproj(1,xy0)).:Nx0 c= dom v by
FUNCT_2:def 1,TARSKI:def 3;
then
A118: Nx0 c= dom (v*reproj(1,xy0)) by FUNCT_3:3;
then
A119: v*reproj(1,xy0) is_differentiable_in proj(1,2).xy0 by A80,A97,
FDIFF_1:def 4;
now
let s be object;
assume s in (reproj(1,xy0)).:Nx0;
then consider x being Element of REAL such that
A120: x in Nx0 and
A121: s = (reproj(1,xy0)).x by FUNCT_2:65;
A122: x+y0* in N by A90,A120;
s=Replace(xy0,1,x) by A121,PDIFF_1:def 5
.= <* x, y0 *> by A7,FINSEQ_7:13;
hence s in dom u by A1,A17,A122;
end;
then dom (reproj(1,xy0)) = REAL & (reproj(1,xy0)).:Nx0 c= dom u by
FUNCT_2:def 1,TARSKI:def 3;
then
A123: Nx0 c= dom (u*reproj(1,xy0)) by FUNCT_3:3;
then u*reproj(1,xy0) is_differentiable_in proj(1,2).xy0 by A80,A113,
FDIFF_1:def 4;
hence thesis by A80,A14,A113,A97,A65,A123,A77,A78,A105,A118,A119,A79,A70,A71,
FDIFF_1:def 5;
end;
Lm6: for x,y be Real,
vx, vy be Point of REAL-NS 1 st vx=<*x*> & vy=<*y*> holds
vx+vy=<*x+y*> & vx-vy = <*x-y*>
proof
let x, y be Real,vx, vy be Point of REAL-NS 1;
assume
A1: vx=<*x*> & vy=<*y*>;
reconsider vx1= vx, vy1 =vy as Element of REAL 1 by REAL_NS1:def 4;
thus vx+vy = vx1+vy1 by REAL_NS1:2
.= <*x+y*> by A1,RVSUM_1:13;
thus vx-vy = vx1-vy1 by REAL_NS1:5
.= <*x-y*> by A1,RVSUM_1:29;
end;
Lm7: for x, y, z, w be Real, vx, vy be Element of REAL 2 st vx = <*x,y*> & vy
= <*z,w*> holds vx+vy = <*x+z,y+w*> & vx-vy = <*x-z,y-w*>
proof
let x, y, z, w be Real, vx, vy be Element of REAL 2;
reconsider x1=x,y1=y,z1=z,w1=w as Element of REAL by XREAL_0:def 1;
assume
A1: vx = <*x,y*> & vy = <*z,w*>;
hence vx + vy = <* addreal.(x1,z1), addreal.(y1,w1) *> by FINSEQ_2:75
.= <*x1+z1,addreal.(y1,w1) *> by BINOP_2:def 9
.= <*x+z,y+w*> by BINOP_2:def 9;
thus vx - vy = <* diffreal.(x1,z1), diffreal.(y1,w1) *> by A1,FINSEQ_2:75
.= <*x1-z1,diffreal.(y1,w1) *> by BINOP_2:def 10
.= <*x-z,y-w*> by BINOP_2:def 10;
end;
Lm8: for x, y, a be Real,
vx be Element of REAL 2 st vx=<*x,y*> holds a*vx=<*
a*x,a*y *>
proof
let x, y, a be Real, vx be Element of REAL 2;
reconsider x1=x,y1=y as Element of REAL by XREAL_0:def 1;
assume vx = <*x,y*>;
hence a*vx = <* (a multreal).x1, (a multreal).y1 *> by FINSEQ_2:36
.= <*a*x1,(a multreal).y1 *> by RVSUM_1:5
.= <*a*x,a*y*> by RVSUM_1:5;
end;
Lm9: for x,y be Real holds <*x,y*> is Point of REAL-NS 2
proof
let x, y be Real;
reconsider x1=x, y1=y as Element of REAL by XREAL_0:def 1;
<*x1,y1*> in REAL 2 by FINSEQ_2:101;
hence thesis by REAL_NS1:def 4;
end;
Lm10: for x, y, z, w be Real, vx, vy be Point of REAL-NS 2 st vx = <*x,y*> &
vy = <*z,w*> holds vx+vy = <*x+z,y+w*> & vx-vy = <*x-z,y-w*>
proof
let x, y, z, w be Real, vx, vy be Point of REAL-NS 2;
assume
A1: vx = <*x,y*> & vy = <*z,w*>;
reconsider vx1 = vx, vy1 = vy as Element of REAL 2 by REAL_NS1:def 4;
thus vx+vy = vx1+vy1 by REAL_NS1:2
.= <*x+z,y+w*> by A1,Lm7;
thus vx-vy = vx1-vy1 by REAL_NS1:5
.= <*x-z,y-w*> by A1,Lm7;
end;
Lm11: for x,y,a be Real,
vx be Point of REAL-NS 2 st vx=<*x,y*> holds a*vx = <*
a*x,a*y *>
proof
let x, y, a be Real, vx be Point of REAL-NS 2;
assume
A1: vx = <*x,y*>;
reconsider vx1 = vx as Element of REAL 2 by REAL_NS1:def 4;
thus a*vx = a*vx1 by REAL_NS1:3
.= <*a*x, a*y *> by A1,Lm8;
end;
Lm12: for u be PartFunc of REAL 2, REAL, xy be Element of REAL 2 st xy in dom
u holds (<>*u).xy = <*u.xy*>
proof
let u be PartFunc of REAL 2, REAL, xy be Element of REAL 2;
assume xy in dom u;
hence (<>*u).xy = (proj(1,1) qua Function" ).(u.xy) by FUNCT_1:13
.= <*u.xy*> by PDIFF_1:1;
end;
Lm13: for u be PartFunc of REAL 2, REAL, x, y be Real st <*x,y*> in dom u
holds (<>*u)/.(<*x,y*>) =<*u/.(<*x,y*>)*>
proof
set W = proj(1,1)qua Function";
let u be PartFunc of REAL 2, REAL;
let x, y be Real;
assume
A1: <*x,y*> in dom u;
rng u c= dom W by PDIFF_1:2;
then dom <>*u = dom u by RELAT_1:27;
hence (<>*u)/.(<*x,y*>) = (<>*u).(<*x,y*>) by A1,PARTFUN1:def 6
.= (proj(1,1) qua Function" ).(u.(<*x,y*>)) by A1,FUNCT_1:13
.= <*u.(<*x,y*>)*> by PDIFF_1:1
.= <*u/.(<*x,y*>)*> by A1,PARTFUN1:def 6;
end;
Lm14: for x,y be Real,z be Complex,v be Element of REAL-NS 2
st z=x+y* & v=<* x,y *> holds |.z.|= ||.v.||
proof
let x, y be Real,z be Complex,v be Element of REAL-NS 2;
assume that
A1: z=x+y* and
A2: v = <* x,y *>;
A3: Im z = y by A1,COMPLEX1:12;
x in REAL & y in REAL by XREAL_0:def 1;
then reconsider xx = <* x,y *> as Element of REAL 2 by FINSEQ_2:101;
A4: |.xx.| = ||.v.|| & Re z = x by A1,A2,COMPLEX1:12,REAL_NS1:1;
reconsider xx1 = xx as Point of TOP-REAL 2 by EUCLID:22;
xx1`2 = y by FINSEQ_1:44;
then
A5: (sqr xx).2 = y^2 by VALUED_1:11;
xx1`1 = x by FINSEQ_1:44;
then len sqr xx = 2 & (sqr xx).1 = x^2 by CARD_1:def 7,VALUED_1:11;
then sqr xx = <*x^2,y^2*> by A5,FINSEQ_1:44;
hence thesis by A4,A3,RVSUM_1:77;
end;
Lm15: for x,y be Real,z be Complex st z=x+y*
holds |.z.| <= |.x.|+|.y.|
proof
let x, y be Real,z be Complex;
assume z = x+y*;
then Re z = x & Im z = y by COMPLEX1:12;
hence thesis by COMPLEX1:78;
end;
Lm16: for x, y be Real holds |.x.| <= |.x+y*.| & |.y.| <= |.x+y*.|
proof
let x, y be Real;
set z = x+y*;
Re z = x & Im z = y by COMPLEX1:12;
hence thesis by COMPLEX1:79;
end;
Lm17: for x,y be Real,v be Element of REAL-NS 2 st v=<* x,y *> holds ||.v.||
<= |.x.|+|.y.|
proof
let x, y be Real,v be Element of REAL-NS 2;
reconsider z = x+y* as Complex;
assume v = <* x,y *>;
then |.z.|= ||.v.|| by Lm14;
hence thesis by Lm15;
end;
theorem Th3:
for seq be Real_Sequence holds seq is convergent & lim seq = 0
iff abs seq is convergent & lim abs seq = 0
proof
let seq be Real_Sequence;
thus seq is convergent & lim seq = 0 implies abs seq is convergent & lim abs
seq = 0
proof
assume that
A1: seq is convergent and
A2: lim seq = 0;
lim abs seq = |.0 .| by A1,A2,SEQ_4:14
.= 0 by ABSVALUE:2;
hence thesis by A1;
end;
thus thesis by SEQ_4:15;
end;
theorem Th4:
for X be RealNormSpace, seq be sequence of X holds seq is
convergent & lim seq = 0.X iff ||. seq .|| is convergent & lim ||. seq .|| = 0
proof
let X be RealNormSpace, seq be sequence of X;
thus seq is convergent & lim seq = 0.X implies ||. seq .|| is convergent &
lim ||. seq .|| = 0
proof
assume
A1: seq is convergent & lim seq = 0.X;
then lim ||. seq .|| = ||.0.X.|| by LOPBAN_1:20;
hence thesis by A1,LOPBAN_1:20,NORMSP_1:1;
end;
assume
A2: ||. seq .|| is convergent & lim ||. seq .|| = 0;
A3: now
let p be Real;
assume 0 < p;
then consider m be Nat such that
A4: for n be Nat st m <= n holds |.||. seq .||.n - 0 .| < p
by A2,SEQ_2:def 7;
take m;
hereby
let n be Nat;
assume m <= n;
then |.||. seq .||.n - 0 .| < p by A4;
then
A5: |. ||. seq.n .|| .| < p by NORMSP_0:def 4;
0 <= ||. seq.n .|| by NORMSP_1:4;
then ||. seq.n .|| < p by A5,ABSVALUE:def 1;
hence ||.seq.n-0.X.|| < p by RLVECT_1:13;
end;
end;
then seq is convergent by NORMSP_1:def 6;
hence thesis by A3,NORMSP_1:def 7;
end;
Lm18: for x be Real, vx be Element of REAL-NS 2 st vx = <* x,0 *> holds ||.vx
.|| = |.x.|
proof
let x be Real, vx be Element of REAL-NS 2;
x in REAL & 0 in REAL by XREAL_0:def 1;
then reconsider xx = <* x,0 *> as Element of REAL 2 by FINSEQ_2:101;
reconsider xx1 = xx as Point of TOP-REAL 2 by EUCLID:22;
assume vx = <* x,0 *>;
then
A1: ||.vx.|| = |.xx.| by REAL_NS1:1;
xx1`2 = 0 by FINSEQ_1:44;
then
A2: (sqr xx).2 = 0^2 by VALUED_1:11;
xx1`1 = x by FINSEQ_1:44;
then len sqr xx = 2 & (sqr xx).1 = x^2 by CARD_1:def 7,VALUED_1:11;
then sqr xx = <*x^2,0^2*> by A2,FINSEQ_1:44;
then sqrt Sum sqr xx = sqrt ( x^2+0^2 ) by RVSUM_1:77
.= sqrt ( x^2+0 * 0) by SQUARE_1:def 1;
hence ||.vx.|| = |.x.| by A1,COMPLEX1:72;
end;
Lm19: for x be Real,vx be Element of REAL-NS 2 st vx = <* 0,x*> holds ||.vx.||
= |.x.|
proof
let x be Real, vx be Element of REAL-NS 2;
x in REAL & 0 in REAL by XREAL_0:def 1;
then reconsider xx = <* 0,x *> as Element of REAL 2 by FINSEQ_2:101;
reconsider xx1 = xx as Point of TOP-REAL 2 by EUCLID:22;
assume vx = <* 0,x *>;
then
A1: ||.vx.|| = |.xx.| by REAL_NS1:1;
xx1`2 = x by FINSEQ_1:44;
then
A2: (sqr xx).2 = x^2 by VALUED_1:11;
xx1`1 = 0 by FINSEQ_1:44;
then len sqr xx = 2 & (sqr xx).1 = 0^2 by CARD_1:def 7,VALUED_1:11;
then sqr xx = <*0^2,x^2*> by A2,FINSEQ_1:44;
then sqrt Sum sqr xx = sqrt ( 0^2+x^2 ) by RVSUM_1:77
.= sqrt ( (0 * 0)+x^2 ) by SQUARE_1:def 1
.= sqrt ( x^2 );
hence ||.vx.|| = |.x.| by A1,COMPLEX1:72;
end;
Lm20: for x be Real,vx be Element of REAL-NS 1 st vx = <* x *> holds ||.vx.||
= |.x.|
proof
let x be Real, vx be Element of REAL-NS 1;
reconsider xx = vx as Element of REAL 1 by REAL_NS1:def 4;
reconsider x2 = x^2 as Element of REAL by XREAL_0:def 1;
assume vx = <* x *>;
then sqrt Sum sqr xx = sqrt Sum <*x2*> by RVSUM_1:55;
then
A1: sqrt Sum sqr xx = sqrt (x^2) by RVSUM_1:73;
||.vx.|| = |.xx.| by REAL_NS1:1;
hence ||.vx.|| = |.x.| by A1,COMPLEX1:72;
end;
Lm21: for v be Element of REAL-NS 1 holds |. proj(1,1).v .| = ||.v.||
proof
let v be Element of REAL-NS 1;
reconsider x=proj(1,1).v as Real;
reconsider w=v as Element of REAL 1 by REAL_NS1:def 4;
len w = 1 & w.1 = x by CARD_1:def 7,PDIFF_1:def 1;
then <* x *> = w by FINSEQ_1:40;
hence thesis by Lm20;
end;
theorem Th5:
for u be PartFunc of REAL 2, REAL, x0, y0 be Real,
xy0 be Element
of REAL 2 st xy0 = <*x0,y0*> & <>*u is_differentiable_in xy0 holds 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 *>)
proof
reconsider ey0 = <* 0, 1 *> as Point of REAL-NS 2 by Lm9;
reconsider ex0 = <* 1, 0 *> as Point of REAL-NS 2 by Lm9;
let u be PartFunc of REAL 2,REAL, x00, y00 be Real,
xy0 be Element of REAL 2
such that
A1: xy0 = <*x00,y00*> and
A2: <>*u is_differentiable_in xy0;
reconsider x0=x00, y0 = y00 as Element of REAL by XREAL_0:def 1;
A3: xy0 = <*x0,y0*> by A1;
set W = proj(1,1)qua Function";
consider g be PartFunc of REAL-NS 2,REAL-NS 1, gxy0 be Point of REAL-NS 2
such that
A4: <>*u=g and
A5: xy0=gxy0 and
A6: g is_differentiable_in gxy0 by A2;
consider N being Neighbourhood of gxy0 such that
A7: N c= dom g and
A8: ex R be RestFunc of REAL-NS 2,REAL-NS 1 st for xy be Point of REAL-NS 2
st xy in N holds g/.xy-g/.gxy0 = diff(g,gxy0).(xy-gxy0) + R/.(xy-gxy0) by A6,
NDIFF_1:def 7;
consider R be RestFunc of REAL-NS 2,REAL-NS 1 such that
A9: for xy be Point of REAL-NS 2 st xy in N holds g/.xy-g/.gxy0 = diff(
g,gxy0).(xy-gxy0) + R/.(xy-gxy0) by A8;
consider r0 be Real such that
A10: 0 < r0 and
A11: {xy where xy is Point of REAL-NS 2: ||.xy-gxy0.|| < r0} c= N by
NFCONT_1:def 1;
consider f be PartFunc of REAL-NS 2,REAL-NS 1, fxy0 be Point of REAL-NS 2
such that
A12: <>*u=f & xy0=fxy0 and
A13: diff(<>*u,xy0)=diff(f,fxy0) by A2,PDIFF_1:def 8;
rng u c= dom W by PDIFF_1:2;
then
A14: dom <>*u = dom u by RELAT_1:27;
A15: for xy be Element of REAL 2,
L1, R1 be Real, z be Element of REAL 2 st
xy in N & z=xy-xy0 & <*L1*>=diff(<>*u,xy0).z & <*R1*>=R.z holds u.xy-u.xy0 = L1
+R1
proof
let xy be Element of REAL 2, L1, R1 be Real, z be Element of REAL 2;
assume that
A16: xy in N and
A17: z=xy-xy0 and
A18: <*L1*>=diff(<>*u,xy0).z and
A19: <*R1*>=R.z;
reconsider zxy=xy as Point of REAL-NS 2 by REAL_NS1:def 4;
A20: zxy-gxy0 = z by A5,A17,REAL_NS1:5;
R is total by NDIFF_1:def 5;
then dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
then R/.(zxy-gxy0) = <*R1*> by A19,A20,PARTFUN1:def 6;
then
A21: diff(g,gxy0).(zxy-gxy0) + R/.(zxy-gxy0) = <*L1+R1*> by A4,A5,A12,A13,A18
,A20,Lm6;
A22: xy0 in N by A5,NFCONT_1:4;
then
A23: g/.gxy0 = g.xy0 by A5,A7,PARTFUN1:def 6
.=(<>*u)/.xy0 by A4,A7,A22,PARTFUN1:def 6;
A24: g/.zxy = g.xy by A7,A16,PARTFUN1:def 6
.=(<>*u)/.xy by A4,A7,A16,PARTFUN1:def 6;
A25: g/.zxy-g/.gxy0 = diff(g,gxy0).(zxy-gxy0) + R/.(zxy-gxy0) by A9,A16;
A26: (<>*u)/.xy0 = (<>*u).xy0 by A4,A7,A22,PARTFUN1:def 6
.= <*u.xy0*> by A4,A7,A14,A22,Lm12;
(<>*u)/.xy = (<>*u).xy by A4,A7,A16,PARTFUN1:def 6
.= <*u.xy*> by A4,A7,A14,A16,Lm12;
then g/.zxy-g/.gxy0 = <*u.xy*> -<*u.xy0*> by A24,A23,A26,REAL_NS1:5
.= <*u.xy*> +<*-u.xy0*> by RVSUM_1:20
.= <* u.xy-u.xy0 *> by RVSUM_1:13;
hence u.xy - u.xy0 = (<*L1+R1*>).1 by A25,A21,FINSEQ_1:def 8
.= L1+R1 by FINSEQ_1:def 8;
end;
set Nx0 = ].x0-r0,x0+r0.[;
reconsider Nx0 as Neighbourhood of x0 by A10,RCOMP_1:def 6;
A27: for x be Real st x in Nx0 holds <*x,y0*> in N
proof
let x be Real;
reconsider xy=<*x,y0*> as Point of REAL-NS 2 by Lm9;
x-x0 in REAL & 0 in REAL by XREAL_0:def 1;
then reconsider xx=<* x-x0,0 *> as Element of REAL 2 by FINSEQ_2:101;
reconsider xx1 =xx as Point of TOP-REAL 2 by EUCLID:22;
assume x in Nx0;
then
A28: |.x-x0.| < r0 by RCOMP_1:1;
xx1`2 = 0 by FINSEQ_1:44;
then
A29: |.xx1`2.| = 0 by ABSVALUE:2;
xy-gxy0 =<*x-x0,y0-y0*> by A3,A5,Lm10
.=<* x-x0,0 *>;
then
A30: ||. xy-gxy0 .|| = |.xx.| by REAL_NS1:1;
|.xx1`1.| = |.x-x0.| & |. xx .| <= |.xx1`1.|+|.xx1`2.| by FINSEQ_1:44
,JGRAPH_1:31;
then ||. xy-gxy0 .|| < r0 by A28,A29,A30,XXREAL_0:2;
then xy in {z where z is Point of REAL-NS 2: ||.z-gxy0.|| < r0};
hence thesis by A11;
end;
now
let s be object;
assume s in (reproj(1,xy0)).:Nx0;
then consider x being Element of REAL such that
A31: x in Nx0 and
A32: s = (reproj(1,xy0)).x by FUNCT_2:65;
A33: <* x,y0 *> in N by A27,A31;
s=Replace(xy0,1,x) by A32,PDIFF_1:def 5
.= <* x, y0 *> by A3,FINSEQ_7:13;
hence s in dom u by A4,A7,A14,A33;
end;
then dom (reproj(1,xy0)) = REAL & (reproj(1,xy0)).:Nx0 c= dom u by
FUNCT_2:def 1,TARSKI:def 3;
then
A34: Nx0 c= dom (u*reproj(1,xy0)) by FUNCT_3:3;
defpred P1[Element of REAL,Element of REAL] means ex vx be Element of REAL 2
st vx=<*$1,0 *> & <*$2*> = R.vx;
A35: now
let x be Element of REAL;
reconsider vx = <*x,In(0,REAL) *> as Element of REAL 2 by FINSEQ_2:101;
R is total by NDIFF_1:def 5;
then
A36: dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
vx is Element of REAL-NS 2 by REAL_NS1:def 4;
then R.vx in the carrier of REAL-NS 1 by A36,PARTFUN1:4;
then R.vx is Element of REAL 1 by REAL_NS1:def 4;
then consider y being Element of REAL such that
A37: <*y*> = R.vx by FINSEQ_2:97;
take y;
thus P1[x,y] by A37;
end;
consider R1 be Function of REAL,REAL such that
A38: for x being Element of REAL holds P1[x, R1.x] from FUNCT_2:sch 3(
A35);
A39: now
let x be Real, vx be Element of REAL 2;
assume
A40: vx=<*x,0 *>;
x in REAL by XREAL_0:def 1;
then
ex vx1 be Element of REAL 2 st vx1=<*x,0 *> & <*R1.x*> = R.vx1 by A38;
hence <*R1.x*> = R.vx by A40;
end;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R1/*h) is
convergent & lim ((h")(#)(R1/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
defpred H1[Nat,Element of REAL-NS 2] means $2 = <* h.$1,0 *>;
A41: now
let n be Element of NAT;
<* h.n,In(0,REAL) *> in REAL 2 by FINSEQ_2:101;
then reconsider y = <* h.n, In(0,REAL) *> as Element of REAL-NS 2 by
REAL_NS1:def 4;
take y;
thus H1[n,y];
end;
consider h1 be sequence of REAL-NS 2 such that
A42: for n being Element of NAT holds H1[n, h1.n] from FUNCT_2:sch 3(A41);
A43: for n being Nat holds H1[n, h1.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A42;
end;
reconsider h1 as sequence of REAL-NS 2;
now
let n be Element of NAT;
A44: h1.n =<*h.n,0 *> by A43;
thus ||.h1.|| .n = ||. h1.n .|| by NORMSP_0:def 4
.= |.h.n.| by A44,Lm18
.= (abs(h)).n by VALUED_1:18;
end;
then
A45: ||.h1.|| = abs h by FUNCT_2:63;
set g = (||.h1.||")(#)(R/*h1);
now
let n be Element of NAT;
reconsider v = h1.n as Element of REAL 2 by REAL_NS1:def 4;
dom R1 = REAL by PARTFUN1:def 2;
then
A46: rng h c= dom R1;
A47: h1.n= <* h.n, 0 *> by A43;
R is total by NDIFF_1:def 5;
then
A48: dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
then
A49: rng h1 c= dom R;
A50: h1.n =<*h.n,0 *> by A43;
A51: R/.(h1.n) = R.v by A48,PARTFUN1:def 6
.= <* R1.(h.n) *> by A39,A47;
thus ||.g.||.n = ||. g.n .|| by NORMSP_0:def 4
.= ||. (||.h1.||").n *(R/*h1) .n .|| by NDIFF_1:def 2
.= ||. ((||.h1.||).n)" *(R/*h1) .n .|| by VALUED_1:10
.= ||. (||.h1.n.||)" *(R/*h1) .n .|| by NORMSP_0:def 4
.= ||. (|.h.n.|)" *(R/*h1) .n .|| by A50,Lm18
.= ||. (|.h.n.|)" *(R/.(h1.n)) .|| by A49,FUNCT_2:109
.= ||. |.(h.n)" .| *(R/.(h1.n)) .|| by COMPLEX1:66
.= |.|.(h.n)" .|.| *||. (R/.(h1.n)) .|| by NORMSP_1:def 1
.= |.(h.n)".|*|.R1.(h.n).| by A51,Lm20
.= |.(h.n)" * (R1.(h.n)) .| by COMPLEX1:65
.= |.(h.n)" * ((R1/*h).n).| by A46,FUNCT_2:108
.= |.(h".n) * (R1/*h).n.| by VALUED_1:10
.= |.(h"(#)(R1/*h)) .n.| by VALUED_1:5
.= abs (h"(#)(R1/*h)) .n by VALUED_1:18;
end;
then
A52: abs ((h")(#)(R1/*h)) = ||.g.|| by FUNCT_2:63;
now
let n be Nat;
A53: h.n <> 0 by SEQ_1:5;
A54: h1.n = <*h.n,0 *> by A43;
now
assume h1.n = 0.(REAL-NS 2);
then h1.n = 0*2 by REAL_NS1:def 4
.= <* 0,0 *> by EUCLID:54,70;
hence contradiction by A54,A53,FINSEQ_1:77;
end;
hence h1.n <> 0.(REAL-NS 2);
end;
then
A55: h1 is non-zero by NDIFF_1:7;
h is convergent & lim h = 0;
then abs h is convergent & lim abs h = 0 by Th3;
then h1 is convergent & lim h1 = 0.(REAL-NS 2) by A45,Th4;
then h1 is (0.(REAL-NS 2))-convergent non-zero by A55,NDIFF_1:def 4;
then (||.h1.||")(#)(R/*h1) is convergent & lim ((||.h1.||")(#)(R/*h1)) =
0.( REAL-NS 1) by NDIFF_1:def 5;
then ||.g.|| is convergent & lim ||.g.|| = 0 by Th4;
hence (h")(#)(R1/*h) is convergent & lim ((h")(#)(R1/*h)) = 0 by A52,Th3;
end;
then reconsider R1 as RestFunc by FDIFF_1:def 2;
ex0 is Element of REAL 2 by REAL_NS1:def 4;
then diff(<>*u,xy0).ex0 is Element of REAL 1 by FUNCT_2:5;
then consider Dux be Element of REAL such that
A56: <*Dux*> = diff(<>*u,xy0).ex0 by FINSEQ_2:97;
deffunc LDF1(Real) = In(Dux* $1,REAL);
consider LD1 be Function of REAL,REAL such that
A57: for x be Element of REAL holds LD1.x = LDF1(x) from FUNCT_2:sch 4;
A58: for x be Real holds LD1.x = Dux* x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD1.x = LDF1(x) by A57;
hence thesis;
end;
set Ny0 = ].y0-r0,y0+r0.[;
reconsider Ny0 as Neighbourhood of y0 by A10,RCOMP_1:def 6;
A59: for y be Real st y in Ny0 holds <*x0,y*> in N
proof
let y be Real;
reconsider xy=<*x0,y*> as Point of REAL-NS 2 by Lm9;
0 in REAL & y-y0 in REAL by XREAL_0:def 1;
then reconsider xx=<* 0,y-y0 *> as Element of REAL 2 by FINSEQ_2:101;
reconsider xx1 = xx as Point of TOP-REAL 2 by EUCLID:22;
assume y in Ny0;
then
A60: |.y-y0.| < r0 by RCOMP_1:1;
xx1`1 = 0 by FINSEQ_1:44;
then
A61: |.xx1`1.| = 0 by ABSVALUE:2;
|. xx .| <= |.xx1`1.|+|.xx1`2.| by JGRAPH_1:31;
then
A62: |.xx.| <= |.y-y0.| by A61,FINSEQ_1:44;
xy-gxy0 =<*x0-x0,y-y0*> by A3,A5,Lm10
.=<* 0,y-y0 *>;
then ||. xy-gxy0 .|| = |.xx.| by REAL_NS1:1;
then ||. xy-gxy0 .|| < r0 by A60,A62,XXREAL_0:2;
then xy in {z where z is Point of REAL-NS 2: ||.z-gxy0.|| < r0};
hence thesis by A11;
end;
now
let s be object;
assume s in (reproj(2,xy0)).:Ny0;
then consider y being Element of REAL such that
A63: y in Ny0 and
A64: s = (reproj(2,xy0)).y by FUNCT_2:65;
A65: <* x0,y *> in N by A59,A63;
s=Replace(xy0,2,y) by A64,PDIFF_1:def 5
.= <* x0, y *> by A3,FINSEQ_7:14;
hence s in dom u by A4,A7,A14,A65;
end;
then dom (reproj(2,xy0)) = REAL & (reproj(2,xy0)).:Ny0 c= dom u by
FUNCT_2:def 1,TARSKI:def 3;
then
A66: Ny0 c= dom (u*reproj(2,xy0)) by FUNCT_3:3;
defpred P2[Element of REAL,Element of REAL] means ex vy be Element of REAL 2
st vy=<* 0,$1 *> & <*$2*> = R.vy;
A67: now
let x be Element of REAL;
reconsider vx = <*In(0,REAL),x *> as Element of REAL 2 by FINSEQ_2:101;
R is total by NDIFF_1:def 5;
then
A68: dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
vx is Element of REAL-NS 2 by REAL_NS1:def 4;
then R.vx in the carrier of REAL-NS 1 by A68,PARTFUN1:4;
then R.vx is Element of REAL 1 by REAL_NS1:def 4;
then consider y being Element of REAL such that
A69: <*y*> = R.vx by FINSEQ_2:97;
take y;
thus P2[x,y] by A69;
end;
consider R3 be Function of REAL,REAL such that
A70: for x being Element of REAL holds P2[x, R3.x] from FUNCT_2:sch 3(
A67);
A71: now
let y be Real, vy be Element of REAL 2;
reconsider yy=y as Element of REAL by XREAL_0:def 1;
assume
A72: vy=<* 0,y *>;
ex vy1 be Element of REAL 2 st vy1=<* 0,y *> & <*R3.yy*> = R.vy1 by A70;
hence <*R3.y*> = R.vy by A72;
end;
for h be 0-convergent non-zero Real_Sequence holds (h")(#)(R3/*h) is
convergent & lim ((h")(#)(R3/*h)) = 0
proof
let h be 0-convergent non-zero Real_Sequence;
defpred H1[Nat,Element of REAL-NS 2] means $2= <* 0,h.$1 *>;
A73: now
let n be Element of NAT;
<* In(0,REAL),h.n *> in REAL 2 by FINSEQ_2:101;
then reconsider y = <* 0,h.n *> as Element of REAL-NS 2 by REAL_NS1:def 4
;
take y;
thus H1[n,y];
end;
consider h1 be sequence of REAL-NS 2 such that
A74: for n being Element of NAT holds H1[n, h1.n] from FUNCT_2:sch 3(A73);
A75: for n being Nat holds H1[n, h1.n]
proof let n be Nat;
n in NAT by ORDINAL1:def 12;
hence thesis by A74;
end;
reconsider h1 as sequence of REAL-NS 2;
now
let n be Element of NAT;
A76: h1.n = <* 0,h.n *> by A75;
thus ||.h1.||.n = ||. h1.n .|| by NORMSP_0:def 4
.= |.h.n.| by A76,Lm19
.= (abs(h)).n by VALUED_1:18;
end;
then
A77: ||.h1.|| = abs h by FUNCT_2:63;
set g=(||.h1.||")(#)(R/*h1);
now
let n be Element of NAT;
reconsider v = h1.n as Element of REAL 2 by REAL_NS1:def 4;
dom R3 = REAL by PARTFUN1:def 2;
then
A78: rng h c= dom R3;
A79: h1.n= <* 0, h.n *> by A75;
R is total by NDIFF_1:def 5;
then
A80: dom R = the carrier of REAL-NS 2 by PARTFUN1:def 2;
then
A81: rng h1 c= dom R;
A82: h1.n =<* 0,h.n *> by A75;
A83: R/.(h1.n) = R.v by A80,PARTFUN1:def 6
.= <* R3.(h.n) *> by A71,A79;
thus ||.g.||.n = ||. g.n .|| by NORMSP_0:def 4
.= ||. (||.h1.||").n *(R/*h1) .n .|| by NDIFF_1:def 2
.= ||. ((||.h1.||).n)" *(R/*h1) .n .|| by VALUED_1:10
.= ||. (||.h1.n.||)" *(R/*h1) .n .|| by NORMSP_0:def 4
.= ||. (|.h.n.|)" *(R/*h1) .n .|| by A82,Lm19
.= ||. (|.h.n.|)" *(R/.(h1.n)) .|| by A81,FUNCT_2:109
.= ||. |.(h.n)" .| *(R/.(h1.n)) .|| by COMPLEX1:66
.= |.|.(h.n)" .|.| *||. (R/.(h1.n)) .|| by NORMSP_1:def 1
.= |.(h.n)".|*|.R3.(h.n).| by A83,Lm20
.= |.(h.n)" * (R3.(h.n)).| by COMPLEX1:65
.= |.(h.n)" * ((R3/*h).n).| by A78,FUNCT_2:108
.= |.(h".n) * (R3/*h).n.| by VALUED_1:10
.= |.(h"(#)(R3/*h)).n.| by VALUED_1:5
.= abs(h"(#)(R3/*h)).n by VALUED_1:18;
end;
then
A84: abs ((h")(#)(R3/*h)) = ||.g.|| by FUNCT_2:63;
now
let n be Nat;
A85: h.n <> 0 by SEQ_1:5;
A86: h1.n = <* 0,h.n *> by A75;
now
assume h1.n = 0.(REAL-NS 2);
then h1.n = 0*2 by REAL_NS1:def 4
.= <* 0,0 *> by EUCLID:54,70;
hence contradiction by A86,A85,FINSEQ_1:77;
end;
hence h1.n <> 0.(REAL-NS 2);
end;
then
A87: h1 is non-zero by NDIFF_1:7;
h is convergent & lim h = 0;
then abs h is convergent & lim abs h = 0 by Th3;
then h1 is convergent & lim h1 = 0.(REAL-NS 2) by A77,Th4;
then h1 is (0.(REAL-NS 2))-convergent non-zero by A87,NDIFF_1:def 4;
then (||.h1.||")(#)(R/*h1) is convergent & lim ((||.h1.||")(#)(R/*h1)) =
0.( REAL-NS 1) by NDIFF_1:def 5;
then ||.g.|| is convergent & lim ||.g.|| = 0 by Th4;
hence (h")(#)(R3/*h) is convergent & lim ((h")(#)(R3/*h)) = 0 by A84,Th3;
end;
then reconsider R3 as RestFunc by FDIFF_1:def 2;
ey0 is Element of REAL 2 by REAL_NS1:def 4;
then diff(<>*u,xy0).ey0 is Element of REAL 1 by FUNCT_2:5;
then consider Duy be Element of REAL such that
A88: <*Duy*> = diff(<>*u,xy0).ey0 by FINSEQ_2:97;
deffunc LDF3(Real) = In(Duy* $1,REAL);
consider LD3 be Function of REAL, REAL such that
A89: for x be Element of REAL holds LD3.x = LDF3(x) from FUNCT_2:sch 4;
A90: for x be Real holds LD3.x = Duy*x
proof let x be Real;
reconsider x as Element of REAL by XREAL_0:def 1;
LD3.x = LDF3(x) by A89;
hence thesis;
end;
reconsider LD3 as LinearFunc by A90,FDIFF_1:def 3;
A91: LD3.1 = Duy *1 by A90
.=Duy;
A92: for y be Element of REAL holds (u*reproj(2,xy0)).y=u.<*x0,y*>
proof
let y be Element of REAL;
y in REAL;
then y in dom (reproj(2,xy0)) by PDIFF_1:def 5;
hence (u*reproj(2,xy0)).y = u.((reproj(2,xy0)).y) by FUNCT_1:13
.=u.(Replace(xy0,2,y)) by PDIFF_1:def 5
.=u.<*x0,y*> by A3,FINSEQ_7:14;
end;
A93: for y be Real
st y in Ny0 holds (u*reproj(2,xy0)).y - (u*reproj(2,xy0)
).y0 = LD3.(y-y0) + R3.(y-y0)
proof
ey0 is Element of REAL 2 by REAL_NS1:def 4;
then reconsider D1=diff(<>*u,xy0).ey0 as Element of REAL 1 by FUNCT_2:5;
let y be Real;
assume
A94: y in Ny0;
reconsider yy=y as Element of REAL by XREAL_0:def 1;
reconsider xy =<*x0,yy*> as Element of REAL 2 by FINSEQ_2:101;
A95: LD3.(y-y0)= Duy*(y-y0) by A90;
A96: xy-xy0 = <* x0-x0,y-y0 *> by A3,Lm7
.= <* (y-y0)*0,(y-y0)*1 *>
.= (y-y0)* ey0 by Lm11;
A97: diff(f,fxy0) is LinearOperator of REAL-NS 2,REAL-NS 1 by LOPBAN_1:def 9;
(y-y0)*D1 = (y-y0)*(diff(f,fxy0).ey0) by A13,REAL_NS1:3
.= (diff(<>*u,xy0)).(xy-xy0) by A13,A96,A97,LOPBAN_1:def 5;
then
A98: <*LD3.(y-y0)*> = (diff(<>*u,xy0)).(xy-xy0) by A88,A95,RVSUM_1:47;
<* 0, y-y0 *> = <* x0-x0, y-y0 *> .= xy - xy0 by A3,Lm7;
then
A99: <*R3.(y-y0) *> = R.(xy-xy0) by A71;
thus (u*reproj(2,xy0)).y - (u*reproj(2,xy0)).y0
= u.<*x0,yy*> - (u*reproj(2,xy0)).y0 by A92
.= u.xy - u.xy0 by A3,A92
.= LD3. (y-y0) + R3.(y-y0) by A15,A59,A94,A98,A99;
end;
reconsider LD1 as LinearFunc by A58,FDIFF_1:def 3;
A100: LD1.1 = Dux*1 by A58
.= Dux;
A101: for x be Element of REAL holds (u*reproj(1,xy0)).x=u.<*x,y0*>
proof
let x be Element of REAL;
x in REAL;
then x in dom (reproj(1,xy0)) by PDIFF_1:def 5;
hence (u*reproj(1,xy0)).x = u.((reproj(1,xy0)).x) by FUNCT_1:13
.=u.(Replace(xy0,1,x)) by PDIFF_1:def 5
.=u.<*x,y0*> by A3,FINSEQ_7:13;
end;
A102: for x be Real
st x in Nx0 holds (u*reproj(1,xy0)).x - (u*reproj(1,xy0)
).x0 = LD1.(x-x0) + R1.(x-x0)
proof
ex0 is Element of REAL 2 by REAL_NS1:def 4;
then reconsider D1=diff(<>*u,xy0).ex0 as Element of REAL 1 by FUNCT_2:5;
let x be Real;
assume
A103: x in Nx0;
reconsider xx=x as Element of REAL by XREAL_0:def 1;
reconsider xy =<*xx,y0*> as Element of REAL 2 by FINSEQ_2:101;
A104: LD1. (x-x0)= Dux*(x-x0) by A58;
A105: xy-xy0 = <* x-x0, y0-y0 *> by A3,Lm7
.= <* (x-x0)*1, (x-x0)*0 *>
.= (x-x0)* ex0 by Lm11;
A106: diff(f,fxy0) is LinearOperator of REAL-NS 2,REAL-NS 1 by LOPBAN_1:def 9;
(x-x0)*D1 = (x-x0)*(diff(f,fxy0).ex0) by A13,REAL_NS1:3
.= (diff(<>*u,xy0)).(xy-xy0) by A13,A105,A106,LOPBAN_1:def 5;
then
A107: <*LD1. (x-x0)*> = (diff(<>*u,xy0)).(xy-xy0) by A56,A104,RVSUM_1:47;
<*x-x0,0 *> = <*x-x0,y0-y0 *> .= xy-xy0 by A3,Lm7;
then
A108: <*R1.(x-x0) *> = R.(xy-xy0) by A39;
thus (u*reproj(1,xy0)).x - (u*reproj(1,xy0)).x0
= u.<*xx,y0*> - (u*reproj(1
,xy0)).x0 by A101
.= u.xy - u.xy0 by A3,A101
.= LD1.(x-x0) + R1.(x-x0) by A15,A27,A103,A107,A108;
end;
A109: proj(2,2).xy0=xy0.2 by PDIFF_1:def 1
.= y0 by A3,FINSEQ_1:44;
then
A110: u*reproj(2,xy0) is_differentiable_in proj(2,2).xy0 by A93,A66,
FDIFF_1:def 4;
A111: proj(1,2).xy0=xy0.1 by PDIFF_1:def 1
.= x0 by A3,FINSEQ_1:44;
then u*reproj(1,xy0) is_differentiable_in proj(1,2).xy0 by A102,A34,
FDIFF_1:def 4;
hence thesis by A111,A109,A56,A88,A102,A93,A100,A34,A91,A66,A110,FDIFF_1:def
5;
end;
reconsider jj=1 as Element of REAL by XREAL_0:def 1;
theorem
for f be PartFunc of COMPLEX, COMPLEX, u,v be PartFunc of REAL 2, REAL
, z0 be Complex, x0, y0 be Real, xy0 be Element of REAL 2 st (for x,y be Real
st <*x,y*> in dom v holds x+y* in dom f) & (for x,y be Real st x+y*