Copyright (c) 2002 Association of Mizar Users
environ
vocabulary FUNCT_1, BOOLE, ABSVALUE, EUCLID, PRE_TOPC, SQUARE_1, RELAT_1,
SUBSET_1, ARYTM_3, METRIC_1, RCOMP_1, FUNCT_5, TOPMETR, COMPTS_1,
JGRAPH_4, ORDINAL2, TOPS_2, ARYTM_1, COMPLEX1, MCART_1, PCOMPS_1,
JGRAPH_3, BORSUK_1, TOPREAL1, TOPREAL2, JORDAN3, PSCOMP_1, REALSET1,
JORDAN5C, JORDAN6, ARYTM, SEQ_1;
notation ORDINAL1, NUMBERS, XCMPLX_0, XREAL_0, REAL_1, XBOOLE_0, ABSVALUE,
EUCLID, TARSKI, RELAT_1, TOPS_2, FUNCT_1, FUNCT_2, NAT_1, STRUCT_0,
TOPMETR, PCOMPS_1, COMPTS_1, METRIC_1, SQUARE_1, RCOMP_1, PSCOMP_1,
BINOP_1, PRE_TOPC, JGRAPH_1, JGRAPH_3, TOPREAL1, JORDAN5C, JORDAN6,
TOPREAL2, JGRAPH_4, GRCAT_1;
constructors REAL_1, ABSVALUE, TOPREAL1, TOPS_2, RCOMP_1, PSCOMP_1, TOPREAL2,
WELLFND1, JGRAPH_3, JORDAN5C, JORDAN6, JGRAPH_4, GRCAT_1, BORSUK_3,
TOPRNS_1;
clusters XREAL_0, STRUCT_0, RELSET_1, FUNCT_1, EUCLID, PRE_TOPC, TOPMETR,
SQUARE_1, PSCOMP_1, BORSUK_1, METRIC_1, BORSUK_2, BORSUK_3, MEMBERED;
requirements REAL, NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, JORDAN6;
theorems TARSKI, XBOOLE_0, XBOOLE_1, AXIOMS, RELAT_1, FUNCT_1, FUNCT_2,
TOPS_1, TOPS_2, PRE_TOPC, TOPMETR, JORDAN6, EUCLID, REAL_1, REAL_2,
JGRAPH_1, SEQ_4, SQUARE_1, PSCOMP_1, METRIC_1, JGRAPH_2, RCOMP_1,
COMPTS_1, RFUNCT_2, SETWISEO, BORSUK_1, TOPREAL1, TOPREAL3, TOPREAL5,
JGRAPH_3, ABSVALUE, COMPLEX1, JORDAN5A, JORDAN5B, JORDAN7, HEINE,
JGRAPH_4, PCOMPS_1, JORDAN5C, JORDAN1B, XREAL_0, TREAL_1, GRCAT_1,
TSEP_1, JORDAN1A, JORDAN1, TOPRNS_1, XCMPLX_0, XCMPLX_1;
schemes FUNCT_2, JGRAPH_2;
begin :: Preliminaries
reserve x,a for real number;
theorem Th1:
a>=0 & (x-a)*(x+a)>=0 implies -a>=x or x>=a
proof assume a>=0 & (x-a)*(x+a)>=0;
then x-a>=0 & x+a>=0 or x-a<=0 & x+a<=0 by SQUARE_1:25;
then x-a+a>=0+a or x+a<=0 by REAL_1:55;
then x-(a-a)>=0+a or x+a<=0 by XCMPLX_1:37;
then x>=0+a or x+a-a<=0-a by REAL_1:49,XCMPLX_1:17;
then x>=0+a or x+(a-a)<=0-a by XCMPLX_1:29;
then x>=a or x<=0-a by XCMPLX_1:25;
hence -a>=x or x>=a by XCMPLX_1:150;
end;
theorem Th2: a<=0 & x<a implies x^2>a^2
proof assume A1: a<=0 & x<a;
then --a<=0;
then A2: -a>=0 by REAL_1:66;
-x>-a by A1,REAL_1:50;
then (-x)^2>(-a)^2 by A2,SQUARE_1:78;
then x^2>(-a)^2 by SQUARE_1:61;
hence thesis by SQUARE_1:61;
end;
theorem Th3: for p being Point of TOP-REAL 2 st |.p.|<=1
holds -1<=p`1 & p`1<=1 & -1<=p`2 & p`2<=1
proof let p be Point of TOP-REAL 2;
assume A1: |.p.|<=1;
set a=|.p.|;
A2: a>=0 by TOPRNS_1:26;
A3: (|.p.|)^2 =(p`1)^2+(p`2)^2 by JGRAPH_3:10;
then a^2-(p`1)^2=(p`2)^2 by XCMPLX_1:26;
then a^2-(p`1)^2>=0 by SQUARE_1:72;
then a^2-(p`1)^2+(p`1)^2>=0+(p`1)^2 by REAL_1:55;
then a^2>=(p`1)^2 by XCMPLX_1:27;
then A4: -a<=p`1 & p`1<=a by A2,JGRAPH_2:5;
a^2-(p`2)^2=(p`1)^2 by A3,XCMPLX_1:26;
then a^2-(p`2)^2>=0 by SQUARE_1:72;
then a^2-(p`2)^2+(p`2)^2>=0+(p`2)^2 by REAL_1:55;
then a^2>=(p`2)^2 by XCMPLX_1:27;
then A5: -a<=p`2 & p`2<=a by A2,JGRAPH_2:5;
-a>=-1 by A1,REAL_1:50;
hence thesis by A1,A4,A5,AXIOMS:22;
end;
theorem Th4: for p being Point of TOP-REAL 2 st |.p.|<=1 & p`1<>0 & p`2<>0
holds -1<p`1 & p`1<1 & -1<p`2 & p`2<1
proof let p be Point of TOP-REAL 2;
assume A1: |.p.|<=1 & p`1<>0 & p`2<>0;
set a=|.p.|;
A2: a>=0 by TOPRNS_1:26;
A3: (|.p.|)^2 =(p`1)^2+(p`2)^2 by JGRAPH_3:10;
then a^2-(p`1)^2=(p`2)^2 by XCMPLX_1:26;
then a^2-(p`1)^2>0 by A1,SQUARE_1:74;
then a^2-(p`1)^2+(p`1)^2>0+(p`1)^2 by REAL_1:67;
then a^2>(p`1)^2 by XCMPLX_1:27;
then A4: -a<p`1 & p`1<a by A2,JGRAPH_2:6;
a^2-(p`2)^2=(p`1)^2 by A3,XCMPLX_1:26;
then a^2-(p`2)^2>0 by A1,SQUARE_1:74;
then a^2-(p`2)^2+(p`2)^2>0+(p`2)^2 by REAL_1:67;
then a^2>(p`2)^2 by XCMPLX_1:27;
then A5: -a<p`2 & p`2<a by A2,JGRAPH_2:6;
-a>=-1 by A1,REAL_1:50;
hence thesis by A1,A4,A5,AXIOMS:22;
end;
theorem for a,b,d,e,r3 being Real,PM,PM2 being non empty MetrStruct,
x being Element of PM,
x2 being Element of PM2
st d<=a & a<=b & b<=e
& PM=Closed-Interval-MSpace(a,b)
& PM2=Closed-Interval-MSpace(d,e)
& x=x2 & x in the carrier of PM & x2 in the carrier of PM2
holds Ball(x,r3) c= Ball(x2,r3)
proof let a,b,d,e,r3 be Real,PM,PM2 be non empty MetrStruct,
x be Element of PM,
x2 be Element of PM2;
assume A1: d<=a & a<=b & b<=e
& PM=Closed-Interval-MSpace(a,b)
& PM2=Closed-Interval-MSpace(d,e) &
x=x2 & x in the carrier of PM & x2 in the carrier of PM2;
then A2: d<=b by AXIOMS:22;
then A3: d<=e by A1,AXIOMS:22;
A4: a<=e by A1,AXIOMS:22;
let z be set;assume z in Ball(x,r3);
then z in {y where y is Element of PM: dist(x,y) < r3 }
by METRIC_1:18;
then consider y being Element of PM such that
A5: y=z & dist(x,y)<r3;
A6: the carrier of PM=[.a,b.] by A1,TOPMETR:14;
A7: a in [.d,e.] by A1,A4,TOPREAL5:1;
b in [.d,e.] by A1,A2,TOPREAL5:1;
then A8: [.a,b.] c= [.d,e.] by A7,RCOMP_1:16;
A9: (the distance of PM).(x,y)
= real_dist.(x,y) by A1,METRIC_1:def 14,TOPMETR:def 1;
A10: dist(x,y)= (the distance of PM).(x,y) by METRIC_1:def 1;
y in [.a,b.] by A6;
then reconsider y3=y as Element of PM2 by A1,A3,A8,TOPMETR:14
;
real_dist.(x,y)=
(the distance of PM2).(x2,y3) by A1,METRIC_1:def 14,TOPMETR:def 1
.=dist(x2,y3) by METRIC_1:def 1;
then z in {y2 where y2 is Element of PM2:
dist(x2,y2)<r3} by A5,A9,A10;
hence thesis by METRIC_1:18;
end;
theorem Th6: for a,b,d,e being real number,
B being Subset of Closed-Interval-TSpace(d,e)
st d<=a & a<=b & b<=e & B=[.a,b.] holds
Closed-Interval-TSpace(a,b)=Closed-Interval-TSpace(d,e)|B
proof let a,b,d,e be real number,
B be Subset of Closed-Interval-TSpace(d,e);
assume A1: d<=a & a<=b & b<=e & B=[.a,b.];
then A2: d<=b by AXIOMS:22;
then A3: d<=e by A1,AXIOMS:22;
A4: a<=e by A1,AXIOMS:22;
reconsider A=[.d,e.] as non empty Subset of R^1
by A1,A2,TOPMETR:24,TOPREAL5:1;
reconsider B2=[.a,b.] as non empty Subset of R^1
by A1,TOPMETR:24,TOPREAL5:1;
A5: a in [.d,e.] by A1,A4,TOPREAL5:1;
b in [.d,e.] by A1,A2,TOPREAL5:1;
then A6: [.a,b.] c= [.d,e.] by A5,RCOMP_1:16;
A7: Closed-Interval-TSpace(a,b)=R^1|B2 by A1,TOPMETR:26;
Closed-Interval-TSpace(d,e)=R^1|A by A3,TOPMETR:26;
hence thesis by A1,A6,A7,JORDAN6:47;
end;
theorem for a,b being real number, B being Subset of I[01]
st 0<=a & a<=b & b<=1 & B=[.a,b.] holds
Closed-Interval-TSpace(a,b)=I[01]|B by Th6,TOPMETR:27;
theorem Th8: for X being TopStruct,
Y,Z being non empty TopStruct,f being map of X,Y,
h being map of Y,Z st h is_homeomorphism & f is continuous
holds h*f is continuous
proof let X be TopStruct,Y,Z be non empty TopStruct,f be map of X,Y,
h be map of Y,Z;
assume A1: h is_homeomorphism &
f is continuous;
then h is continuous by TOPS_2:def 5;
hence h*f is continuous by A1,TOPS_2:58;
end;
theorem Th9: for X,Y,Z being TopStruct, f being map of X,Y,
h being map of Y,Z st h is_homeomorphism & f is one-to-one
holds h*f is one-to-one
proof let X,Y,Z be TopStruct, f be map of X,Y, h be map of Y,Z;
assume A1: h is_homeomorphism & f is one-to-one;
then h is one-to-one by TOPS_2:def 5;
hence h*f is one-to-one by A1,FUNCT_1:46;
end;
theorem Th10: for X being TopStruct,S,V being non empty TopStruct,
B being non empty Subset of S,f being map of X,S|B, g being map of S,V,
h being map of X,V
st h=g*f & f is continuous & g is continuous holds h is continuous
proof let X be TopStruct,S,V be non empty TopStruct,
B be non empty Subset of S,
f be map of X,S|B, g be map of S,V,
h being map of X,V;
assume that A1: h=g*f & f is continuous and A2: g is continuous;
now let P be Subset of V;
A3: (g*f)"P = f"(g"P) by RELAT_1:181;
now assume P is closed;
then A4: g"P is closed by A2,PRE_TOPC:def 12;
A5: [#](S|B)=B by PRE_TOPC:def 10;
A6: the carrier of S|B =B by JORDAN1:1;
then B /\ g"P c= the carrier of S|B by XBOOLE_1:17;
then reconsider F=B /\ g"P as Subset of S|B;
A7: F is closed by A4,A5,PRE_TOPC:43;
A8: rng f /\ (the carrier of S|B)= rng f by XBOOLE_1:28;
h"P=f"(rng f /\ g"P) by A1,A3,RELAT_1:168
.=f"(rng f /\ ((the carrier of S|B) /\ g"P)) by A8,XBOOLE_1:16
.=f"F by A6,RELAT_1:168;
hence h"P is closed by A1,A7,PRE_TOPC:def 12;
end;
hence P is closed implies h"P is closed;
end;
hence thesis by PRE_TOPC:def 12;
end;
theorem Th11:for a,b,d,e,s1,s2,t1,t2 being Real,h being map of
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(d,e) st
h is_homeomorphism & h.s1=t1 & h.s2=t2 & h.a=d & h.b=e & d<=e &
t1<=t2 & s1 in [.a,b.] & s2 in [.a,b.] holds s1<=s2
proof let a,b,d,e,s1,s2,t1,t2 be Real,h be map of
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(d,e);
assume A1: h is_homeomorphism & h.s1=t1 & h.s2=t2 & h.a=d & h.b=e & d<=e
& t1<=t2 & s1 in [.a,b.] & s2 in [.a,b.];
then A2: h is one-to-one by TOPS_2:def 5;
A3: a<=s2 & s2<=b by A1,TOPREAL5:1;
A4: a<=s1 & s1<=b by A1,TOPREAL5:1;
then A5: a<=b by AXIOMS:22;
A6: dom h=[#](Closed-Interval-TSpace(a,b)) by A1,TOPS_2:def 5
.=the carrier of Closed-Interval-TSpace(a,b) by PRE_TOPC:12
.=[.a,b.] by A5,TOPMETR:25;
A7: h is continuous by A1,TOPS_2:def 5;
A8: the carrier of Closed-Interval-TSpace(a,b)
=[.a,b.] by A5,TOPMETR:25;
A9: the carrier of Closed-Interval-TSpace(d,e)
=[.d,e.] by A1,TOPMETR:25;
A10: h is one-to-one by A1,TOPS_2:def 5;
[.s2,s1.] c= the carrier of Closed-Interval-TSpace(a,b)
by A3,A4,A8,TREAL_1:1;
then reconsider B=[.s2,s1.] as Subset of Closed-Interval-TSpace(a,b)
;
reconsider Bb=[.s2,s1.] as Subset of
Closed-Interval-TSpace(a,b) by A3,A4,A8,TREAL_1:1;
assume A11: s1>s2;
reconsider f3=h|Bb as map of Closed-Interval-TSpace(a,b)|B,
Closed-Interval-TSpace(d,e) by JGRAPH_3:12;
A12: f3 is continuous by A7,TOPMETR:10;
reconsider C=[.d,e.] as non empty Subset of R^1
by A1,TOPMETR:24,TOPREAL5:1;
A13: R^1|C=Closed-Interval-TSpace(d,e) by A1,TOPMETR:26;
A14: Closed-Interval-TSpace(s2,s1)
=Closed-Interval-TSpace(a,b)|B by A3,A4,A11,Th6;
then f3 is map of Closed-Interval-TSpace(s2,s1),R^1
by A13,JORDAN6:4;
then reconsider f=h|B as map of Closed-Interval-TSpace(s2,s1),R^1;
dom f=the carrier of Closed-Interval-TSpace(s2,s1)
by FUNCT_2:def 1;
then A15: dom f=[.s2,s1.] by A11,TOPMETR:25;
A16: f is continuous by A12,A13,A14,JORDAN6:4;
set t=(t1+t2)/2;
s2 in B by A11,TOPREAL5:1;
then A17: f.s2=t2 by A1,FUNCT_1:72;
s1 in B by A11,TOPREAL5:1;
then A18: f.s1=t1 by A1,FUNCT_1:72;
t1<>t2 by A1,A2,A6,A11,FUNCT_1:def 8;
then A19: t1<t2 by A1,REAL_1:def 5;
then t1+t1<t1+t2 by REAL_1:67;
then (t1+t1)/2<(t1+t2)/2 by REAL_1:73;
then A20: (2*t1)/2<t by XCMPLX_1:11;
t1+t2<t2+t2 by A19,REAL_1:67;
then (t1+t2)/2<(t2+t2)/2 by REAL_1:73;
then (2*t2)/2>t by XCMPLX_1:11;
then A21: t2>t & t>t1 by A20,XCMPLX_1:90;
then consider r being Real such that
A22: f.r =t & s2<r & r <s1 by A11,A16,A17,A18,TOPREAL5:13;
A23: r<b by A4,A22,AXIOMS:22;
a<r by A3,A22,AXIOMS:22;
then A24: r in [.a,b.] by A23,TOPREAL5:1;
[.s1,b.] c= the carrier of Closed-Interval-TSpace(a,b)
by A4,A8,TREAL_1:1;
then reconsider B1=[.s1,b.] as Subset of Closed-Interval-TSpace(a,b)
;
reconsider B1b=[.s1,b.] as Subset of
Closed-Interval-TSpace(a,b) by A4,A8,TREAL_1:1;
reconsider f4=h|B1b as map of Closed-Interval-TSpace(a,b)|B1,
Closed-Interval-TSpace(d,e) by JGRAPH_3:12;
A25: Closed-Interval-TSpace(s1,b)
=Closed-Interval-TSpace(a,b)|B1 by A4,Th6;
A26: f4 is continuous by A7,TOPMETR:10;
f4 is map of Closed-Interval-TSpace(s1,b),R^1
by A13,A25,JORDAN6:4;
then reconsider f1=h|B1 as map of Closed-Interval-TSpace(s1,b),R^1;
A27: f1 is continuous by A13,A25,A26,JORDAN6:4;
s2 in dom f by A11,A15,TOPREAL5:1;
then t2 in rng f3 by A17,FUNCT_1:def 5;
then A28: d<=t2 & t2<=e by A9,TOPREAL5:1;
then A29: s1<b by A1,A4,A19,REAL_1:def 5;
A30: s1 in B1 by A4,TOPREAL5:1;
A31: b in B1 by A4,TOPREAL5:1;
A32: f1.s1= t1 by A1,A30,FUNCT_1:72;
A33: f1.b= e by A1,A31,FUNCT_1:72;
e>t & t>t1 by A21,A28,AXIOMS:22;
then consider r1 being Real such that
A34: f1.r1 =t & s1<r1 & r1 <b by A27,A29,A32,A33,TOPREAL5:12;
a<r1 by A4,A34,AXIOMS:22;
then A35: r1 in [.a,b.] by A34,TOPREAL5:1;
A36: r1 in B1 by A34,TOPREAL5:1;
r in [.s2,s1.] by A22,TOPREAL5:1;
then h.r = t by A22,FUNCT_1:72 .=h.r1 by A34,A36,FUNCT_1:72;
hence contradiction by A6,A10,A22,A24,A34,A35,FUNCT_1:def 8;
end;
theorem Th12:for a,b,d,e,s1,s2,t1,t2 being Real,h being map of
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(d,e) st
h is_homeomorphism & h.s1=t1 & h.s2=t2 & h.a=e & h.b=d & e>=d &
t1>=t2 & s1 in [.a,b.] & s2 in [.a,b.] holds s1<=s2
proof let a,b,d,e,s1,s2,t1,t2 be Real,h be map of
Closed-Interval-TSpace(a,b),Closed-Interval-TSpace(d,e);
assume A1: h is_homeomorphism & h.s1=t1 & h.s2=t2 & h.a=e & h.b=d & e>=d
& t1>=t2 & s1 in [.a,b.] & s2 in [.a,b.];
then A2: h is one-to-one by TOPS_2:def 5;
A3: a<=s2 & s2<=b by A1,TOPREAL5:1;
A4: a<=s1 & s1<=b by A1,TOPREAL5:1;
then A5: a<=b by AXIOMS:22;
A6: dom h=[#](Closed-Interval-TSpace(a,b)) by A1,TOPS_2:def 5
.=the carrier of Closed-Interval-TSpace(a,b) by PRE_TOPC:12
.=[.a,b.] by A5,TOPMETR:25;
A7: h is continuous by A1,TOPS_2:def 5;
A8: the carrier of Closed-Interval-TSpace(a,b)
=[.a,b.] by A5,TOPMETR:25;
A9: the carrier of Closed-Interval-TSpace(d,e)
=[.d,e.] by A1,TOPMETR:25;
A10: h is one-to-one by A1,TOPS_2:def 5;
[.s2,s1.] c= the carrier of Closed-Interval-TSpace(a,b)
by A3,A4,A8,TREAL_1:1;
then reconsider B=[.s2,s1.] as Subset of Closed-Interval-TSpace(a,b)
;
reconsider Bb=[.s2,s1.] as Subset of
Closed-Interval-TSpace(a,b) by A3,A4,A8,TREAL_1:1;
assume A11: s1>s2;
reconsider f3=h|Bb as map of Closed-Interval-TSpace(a,b)|B,
Closed-Interval-TSpace(d,e) by JGRAPH_3:12;
A12: f3 is continuous by A7,TOPMETR:10;
reconsider C=[.d,e.] as non empty Subset of R^1
by A1,TOPMETR:24,TOPREAL5:1;
A13: R^1|C=Closed-Interval-TSpace(d,e) by A1,TOPMETR:26;
A14: Closed-Interval-TSpace(s2,s1)
=Closed-Interval-TSpace(a,b)|B by A3,A4,A11,Th6;
then f3 is map of Closed-Interval-TSpace(s2,s1),R^1
by A13,JORDAN6:4;
then reconsider f=h|B as map of Closed-Interval-TSpace(s2,s1),R^1;
dom f=the carrier of Closed-Interval-TSpace(s2,s1)
by FUNCT_2:def 1;
then A15: dom f=[.s2,s1.] by A11,TOPMETR:25;
A16: f is continuous by A12,A13,A14,JORDAN6:4;
set t=(t1+t2)/2;
s2 in B by A11,TOPREAL5:1;
then A17: f.s2=t2 by A1,FUNCT_1:72;
s1 in B by A11,TOPREAL5:1;
then A18: f.s1=t1 by A1,FUNCT_1:72;
t1<>t2 by A1,A2,A6,A11,FUNCT_1:def 8;
then A19: t1>t2 by A1,REAL_1:def 5;
then t1+t1>t1+t2 by REAL_1:67;
then (t1+t1)/2>(t1+t2)/2 by REAL_1:73;
then A20: (2*t1)/2>t by XCMPLX_1:11;
t1+t2>t2+t2 by A19,REAL_1:67;
then (t1+t2)/2>(t2+t2)/2 by REAL_1:73;
then (2*t2)/2<t by XCMPLX_1:11;
then A21: t2<t & t<t1 by A20,XCMPLX_1:90;
then consider r being Real such that
A22: f.r =t & s2<r & r <s1 by A11,A16,A17,A18,TOPREAL5:12;
A23: r<b by A4,A22,AXIOMS:22;
a<r by A3,A22,AXIOMS:22;
then A24: r in [.a,b.] by A23,TOPREAL5:1;
[.s1,b.] c= the carrier of Closed-Interval-TSpace(a,b)
by A4,A8,TREAL_1:1;
then reconsider B1=[.s1,b.] as Subset of Closed-Interval-TSpace(a,b)
;
reconsider B1b=[.s1,b.] as Subset of
Closed-Interval-TSpace(a,b) by A4,A8,TREAL_1:1;
reconsider f4=h|B1b as map of Closed-Interval-TSpace(a,b)|B1,
Closed-Interval-TSpace(d,e) by JGRAPH_3:12;
A25: Closed-Interval-TSpace(s1,b)
=Closed-Interval-TSpace(a,b)|B1 by A4,Th6;
A26: f4 is continuous by A7,TOPMETR:10;
f4 is map of Closed-Interval-TSpace(s1,b),R^1
by A13,A25,JORDAN6:4;
then reconsider f1=h|B1 as map of Closed-Interval-TSpace(s1,b),R^1;
A27: f1 is continuous by A13,A25,A26,JORDAN6:4;
s2 in dom f by A11,A15,TOPREAL5:1;
then t2 in rng f3 by A17,FUNCT_1:def 5;
then A28: d<=t2 & t2<=e by A9,TOPREAL5:1;
then A29: s1<b by A1,A4,A19,REAL_1:def 5;
A30: s1 in B1 by A4,TOPREAL5:1;
A31: b in B1 by A4,TOPREAL5:1;
A32: f1.s1= t1 by A1,A30,FUNCT_1:72;
A33: f1.b= d by A1,A31,FUNCT_1:72;
d<t & t<t1 by A21,A28,AXIOMS:22;
then consider r1 being Real such that
A34: f1.r1 =t & s1<r1 & r1 <b by A27,A29,A32,A33,TOPREAL5:13;
a<r1 by A4,A34,AXIOMS:22;
then A35: r1 in [.a,b.] by A34,TOPREAL5:1;
A36: r1 in B1 by A34,TOPREAL5:1;
r in [.s2,s1.] by A22,TOPREAL5:1;
then h.r= t by A22,FUNCT_1:72 .=h.r1 by A34,A36,FUNCT_1:72;
hence contradiction by A6,A10,A22,A24,A34,A35,FUNCT_1:def 8;
end;
theorem for n being Nat holds
-(0.REAL n)=0.REAL n
proof let n be Nat;
0.REAL n+0.REAL n=0.REAL n by EUCLID:31;
hence thesis by EUCLID:41;
end;
begin :: Fashoda Meet Theorems for Circle in Special Case
theorem Th14:
for f,g being map of I[01],TOP-REAL 2,a,b,c,d being Real,
O,I being Point of I[01] st O=0 & I=1 &
f is continuous one-to-one &
g is continuous one-to-one & a <> b & c <> d &
(f.O)`1=a & (c <=(f.O)`2 & (f.O)`2 <=d) &
(f.I)`1=b & (c <=(f.I)`2 & (f.I)`2 <=d) &
(g.O)`2=c & (a <=(g.O)`1 & (g.O)`1 <=b) &
(g.I)`2=d & (a <=(g.I)`1 & (g.I)`1 <=b) &
(for r being Point of I[01] holds
(a >=(f.r)`1 or (f.r)`1>=b or c >=(f.r)`2 or (f.r)`2>=d) &
(a >=(g.r)`1 or (g.r)`1>=b or c >=(g.r)`2 or (g.r)`2>=d))
holds rng f meets rng g
proof let f,g be map of I[01],TOP-REAL 2,a,b,c,d be Real,
O,I be Point of I[01];
assume A1: O=0 & I=1 &
f is continuous one-to-one & g is continuous one-to-one & a <> b & c <> d &
(f.O)`1=a & (c <=(f.O)`2 & (f.O)`2 <=d) &
(f.I)`1=b & (c <=(f.I)`2 & (f.I)`2 <=d) &
(g.O)`2=c & (a <=(g.O)`1 & (g.O)`1 <=b) &
(g.I)`2=d & (a <=(g.I)`1 & (g.I)`1 <=b) &
(for r being Point of I[01] holds
(a >=(f.r)`1 or (f.r)`1>=b or c >=(f.r)`2 or (f.r)`2>=d) &
(a >=(g.r)`1 or (g.r)`1>=b or c >=(g.r)`2 or (g.r)`2>=d));
then A2: a <= b by AXIOMS:22;
c <= d by A1,AXIOMS:22;
then a < b & c < d by A1,A2,REAL_1:def 5;
hence thesis by A1,JGRAPH_2:55;
end;
Lm1: 0 in [.0,1.] & 1 in [.0,1.] by RCOMP_1:15;
theorem Th15: for f being map of I[01],TOP-REAL 2 st
f is continuous one-to-one
ex f2 being map of I[01],TOP-REAL 2 st f2.0=f.1 & f2.1=f.0 &
rng f2=rng f & f2 is continuous & f2 is one-to-one
proof let f be map of I[01],TOP-REAL 2;
assume A1: f is continuous one-to-one;
A2: I[01] is compact by HEINE:11,TOPMETR:27;
A3: dom f=the carrier of I[01] by FUNCT_2:def 1;
then A4: f.1 in rng f by Lm1,BORSUK_1:83,FUNCT_1:12;
reconsider P=rng f as non empty Subset of TOP-REAL 2 by A3,Lm1,BORSUK_1:83,
FUNCT_1:12;
consider f1 being map of I[01],(TOP-REAL 2)|P such that
A5: f1=f & f1 is_homeomorphism by A1,A2,JGRAPH_1:64;
f.0 in rng f by A3,Lm1,BORSUK_1:83,FUNCT_1:12;
then reconsider p1=f.0,p2=f.1 as Point of TOP-REAL 2 by A4;
P is_an_arc_of p1,p2 by A5,TOPREAL1:def 2;
then P is_an_arc_of p2,p1 by JORDAN5B:14;
then consider f3 being map of I[01], (TOP-REAL 2)|P such that
A6: f3 is_homeomorphism & f3.0 = p2 & f3.1 = p1 by TOPREAL1:def 2;
A7: rng f3=[#]((TOP-REAL 2)|P) by A6,TOPS_2:def 5
.=P by PRE_TOPC:def 10;
consider f4 being map of I[01], (TOP-REAL 2) such that
A8: f3=f4 & f4 is continuous & f4 is one-to-one by A6,JORDAN7:15;
thus thesis by A6,A7,A8;
end;
reserve p,q for Point of TOP-REAL 2;
theorem Th16:
for f,g being map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN being Subset of TOP-REAL 2,
O,I being Point of I[01] st O=0 & I=1 &
f is continuous one-to-one &
g is continuous one-to-one &
C0={p: |.p.|<=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXN & f.I in KXP & g.O in KYP & g.I in KYN &
rng f c= C0 & rng g c= C0 holds rng f meets rng g
proof let f,g be map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN be Subset of TOP-REAL 2,
O,I be Point of I[01];
assume A1: O=0 & I=1 &
f is continuous one-to-one &
g is continuous one-to-one &
C0={p: |.p.|<=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXN & f.I in KXP & g.O in KYP & g.I in KYN &
rng f c= C0 & rng g c= C0;
then consider g2 being map of I[01],TOP-REAL 2 such that
A2: g2.0=g.1 & g2.1=g.0 &
rng g2=rng g & g2 is continuous one-to-one by Th15;
thus thesis by A1,A2,JGRAPH_3:55;
end;
theorem Th17: for f,g being map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN being Subset of TOP-REAL 2,
O,I being Point of I[01] st O=0 & I=1 &
f is continuous one-to-one &
g is continuous one-to-one &
C0={p: |.p.|>=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXN & f.I in KXP & g.O in KYN & g.I in KYP &
rng f c= C0 & rng g c= C0 holds rng f meets rng g
proof let f,g be map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN be Subset of TOP-REAL 2,
O,I be Point of I[01];
assume A1: O=0 & I=1 &
f is continuous one-to-one & g is continuous one-to-one &
C0 = {p: |.p.|>=1}&
KXP = {q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN = {q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP = {q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN = {q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXN & f.I in KXP & g.O in KYN & g.I in KYP &
rng f c= C0 & rng g c= C0;
Sq_Circ"*f is Function of the carrier of I[01],
the carrier of TOP-REAL 2 by FUNCT_2:19,JGRAPH_3:39;
then reconsider ff=Sq_Circ"*f as map of I[01],TOP-REAL 2;
Sq_Circ"*g is Function of the carrier of I[01],
the carrier of TOP-REAL 2 by FUNCT_2:19,JGRAPH_3:39;
then reconsider gg=Sq_Circ"*g as map of I[01],TOP-REAL 2;
consider h1 being map of (TOP-REAL 2),(TOP-REAL 2)
such that A2:h1=(Sq_Circ") & h1 is continuous by JGRAPH_3:52;
A3:dom ff=the carrier of I[01] by FUNCT_2:def 1;
A4:dom gg=the carrier of I[01] by FUNCT_2:def 1;
A5:dom f=the carrier of I[01] by FUNCT_2:def 1;
A6:dom g=the carrier of I[01] by FUNCT_2:def 1;
A7:ff is continuous by A1,A2,TOPS_2:58;
A8: Sq_Circ" is one-to-one by FUNCT_1:62,JGRAPH_3:32;
then A9:ff is one-to-one by A1,FUNCT_1:46;
A10:gg is continuous by A1,A2,TOPS_2:58;
A11:gg is one-to-one by A1,A8,FUNCT_1:46;
A12: (ff.O)`1=-1 & (ff.I)`1=1 & (gg.O)`2=-1 & (gg.I)`2=1
proof
A13: (ff.O)=(Sq_Circ").(f.O) by A3,FUNCT_1:22;
consider p1 being Point of TOP-REAL 2 such that
A14: f.O=p1 &( |.p1.|=1 & p1`2>=p1`1 & p1`2<=-p1`1) by A1;
A15:p1<>0.REAL 2 &
(p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 & p1`2<=-p1`1)
by A14,TOPRNS_1:24;
then A16:Sq_Circ".p1=|[p1`1*sqrt(1+(p1`2/p1`1)^2),p1`2*sqrt(1+(p1`2/p1`1)^2
)]|
by JGRAPH_3:38;
reconsider px=ff.O as Point of TOP-REAL 2;
set q=px;
A17: px`1 = p1`1*sqrt(1+(p1`2/p1`1)^2) &
px`2 = p1`2*sqrt(1+(p1`2/p1`1)^2) by A13,A14,A16,EUCLID:56;
(p1`2/p1`1)^2 >=0 by SQUARE_1:72;
then 1+(p1`2/p1`1)^2>=1+0 by REAL_1:55;
then 1+(p1`2/p1`1)^2>0 by AXIOMS:22;
then A18:sqrt(1+(p1`2/p1`1)^2)>0 by SQUARE_1:93;
A19:now assume
A20: px`1=0 & px`2=0;
then A21:p1`1=0 by A17,A18,XCMPLX_1:6;
p1`2=0 by A17,A18,A20,XCMPLX_1:6;
hence contradiction by A15,A21,EUCLID:57,58;
end;
p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 &
p1`2*sqrt(1+(p1`2/p1`1)^2) <= (-p1`1)*sqrt(1+(p1`2/p1`1)^2)
by A14,A18,AXIOMS:25;
then p1`2<=p1`1 & (-p1`1)*sqrt(1+(p1`2/p1`1)^2) <= p1`2*sqrt(1+(p1`2/p1`1
)^2)
or px`2>=px`1 & px`2<=-px`1 by A17,A18,AXIOMS:25,XCMPLX_1:175;
then A22:px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A17,A18,AXIOMS:25,XCMPLX_1:175;
A23:p1=Sq_Circ.px by A13,A14,FUNCT_1:54,JGRAPH_3:32,54;
A24:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by A19,A22,JGRAPH_2:11,JGRAPH_3:def 1;
A25: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1
= q`1/sqrt(1+(q`2/q`1)^2) &
(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2
= q`2/sqrt(1+(q`2/q`1)^2) by EUCLID:56;
(q`2/q`1)^2 >=0 by SQUARE_1:72;
then 1+(q`2/q`1)^2>=1+0 by REAL_1:55;
then A26:1+(q`2/q`1)^2>0 by AXIOMS:22;
then A27:sqrt(1+(q`2/q`1)^2)>0 by SQUARE_1:93;
px`1<>0 by A19,A22;
then A28: (px`1)^2<>0 by SQUARE_1:73;
now
(|.p1.|)^2= (q`1/sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2
by A23,A24,A25,JGRAPH_3:10
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A26,SQUARE_1:def 4
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A26,SQUARE_1:def 4
.= ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)
by XCMPLX_1:63;
then ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)*(1+(q`2/q`1)^2)=(1)*(1+(q`2/q`1
)^2)
by A14,SQUARE_1:59;
then ((q`1)^2+(q`2)^2)=(1+(q`2/q`1)^2) by A26,XCMPLX_1:88;
then (px`1)^2+(px`2)^2=1+(px`2)^2/(px`1)^2 by SQUARE_1:69;
then (px`1)^2+(px`2)^2-1=(px`2)^2/(px`1)^2 by XCMPLX_1:26;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2=(px`2)^2 by A28,XCMPLX_1:88;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2=(px`2)^2 by XCMPLX_1:29;
then (px`1)^2*(px`1)^2+((px`2)^2-1)*(px`1)^2=(px`2)^2 by XCMPLX_1:8;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2=0 by XCMPLX_1:14
;
then (px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2=0
by XCMPLX_1:40;
then (px`1)^2*(px`1)^2+(px`1)^2*(px`2)^2-(px`1)^2*1-(px`2)^2=0
by XCMPLX_1:29;
then (px`1)^2*(px`1)^2-(px`1)^2*1+(px`1)^2*(px`2)^2-(1)*(px`2)^2=0
by XCMPLX_1:29;
then (px`1)^2*((px`1)^2-1)+(px`1)^2*(px`2)^2-(1)*(px`2)^2=0
by XCMPLX_1:40;
then (px`1)^2*((px`1)^2-1)+((px`1)^2*(px`2)^2-(1)*(px`2)^2)=0
by XCMPLX_1:29;
hence ((px`1)^2-1)*(px`1)^2+((px`1)^2-1)*(px`2)^2=0 by XCMPLX_1:40;
end;
then A29:((px`1)^2-1)*((px`1)^2+(px`2)^2)=0 by XCMPLX_1:8;
((px`1)^2+(px`2)^2)<>0 by A19,COMPLEX1:2;
then (px`1)^2-1=0 by A29,XCMPLX_1:6;
then (px`1-1)*(px`1+1)=0 by SQUARE_1:59,67;
then A30: px`1-1=0 or px`1+1=0 by XCMPLX_1:6;
A31: now assume A32: px`1=1;
then A33:p1`1>0 by A23,A24,A25,A27,REAL_2:127;
-p1`2>=--p1`1 by A14,REAL_1:50;
then -p1`2>0 by A23,A24,A25,A27,A32,REAL_2:127;
then --p1`2<-0 by REAL_1:50;
hence contradiction by A14,A33,AXIOMS:22;
end;
A34: (ff.I)=(Sq_Circ").(f.I) by A3,FUNCT_1:22;
consider p2 being Point of TOP-REAL 2 such that
A35: f.I=p2 & (|.p2.|=1 & p2`2<=p2`1 & p2`2>=-p2`1) by A1;
A36:p2<>0.REAL 2 &
(p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 & p2`2<=-p2`1)
by A35,TOPRNS_1:24;
then A37:Sq_Circ".p2=|[p2`1*sqrt(1+(p2`2/p2`1)^2),p2`2*sqrt(1+(p2`2/p2`1)^2
)]|
by JGRAPH_3:38;
reconsider py=ff.I as Point of TOP-REAL 2;
A38: py`1 = p2`1*sqrt(1+(p2`2/p2`1)^2) &
py`2 = p2`2*sqrt(1+(p2`2/p2`1)^2) by A34,A35,A37,EUCLID:56;
(p2`2/p2`1)^2 >=0 by SQUARE_1:72;
then 1+(p2`2/p2`1)^2>=1+0 by REAL_1:55;
then 1+(p2`2/p2`1)^2>0 by AXIOMS:22;
then A39:sqrt(1+(p2`2/p2`1)^2)>0 by SQUARE_1:93;
A40:now assume
A41: py`1=0 & py`2=0;
then A42:p2`1=0 by A38,A39,XCMPLX_1:6;
p2`2=0 by A38,A39,A41,XCMPLX_1:6;
hence contradiction by A36,A42,EUCLID:57,58;
end;
A43: now
p2`2<=p2`1 & (-p2`1)*sqrt(1+(p2`2/p2`1)^2) <= p2`2*sqrt(1+(p2`2/p2`1)^2)
or py`2>=py`1 & py`2<=-py`1 by A35,A39,AXIOMS:25;
hence
p2`2*sqrt(1+(p2`2/p2`1)^2) <= p2`1*sqrt(1+(p2`2/p2`1)^2) & -py`1<=py
`2
or py`2>=py`1 & py`2<=-py`1 by A38,A39,AXIOMS:25,XCMPLX_1:175;
end;
A44:p2=Sq_Circ.py by A34,A35,FUNCT_1:54,JGRAPH_3:32,54;
A45:Sq_Circ.py=|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|
by A38,A40,A43,JGRAPH_2:11,JGRAPH_3:def 1;
A46: (|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|)`1
= py`1/sqrt(1+(py`2/py`1)^2) &
(|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|)`2
= py`2/sqrt(1+(py`2/py`1)^2) by EUCLID:56;
(py`2/py`1)^2 >=0 by SQUARE_1:72;
then 1+(py`2/py`1)^2>=1+0 by REAL_1:55;
then A47:1+(py`2/py`1)^2>0 by AXIOMS:22;
then A48:sqrt(1+(py`2/py`1)^2)>0 by SQUARE_1:93;
py`1<>0 by A38,A40,A43;
then A49: (py`1)^2<>0 by SQUARE_1:73;
now
(|.p2.|)^2= (py`1/sqrt(1+(py`2/py`1)^2))^2+(py`2/sqrt(1+(py`2/py`1)^2))^2
by A44,A45,A46,JGRAPH_3:10
.= (py`1)^2/(sqrt(1+(py`2/py`1)^2))^2+(py`2/sqrt(1+(py`2/py`1)^2))^2
by SQUARE_1:69
.= (py`1)^2/(sqrt(1+(py`2/py`1)^2))^2
+(py`2)^2/(sqrt(1+(py`2/py`1)^2))^2
by SQUARE_1:69
.= (py`1)^2/(1+(py`2/py`1)^2)+(py`2)^2/(sqrt(1+(py`2/py`1)^2))^2
by A47,SQUARE_1:def 4
.= (py`1)^2/(1+(py`2/py`1)^2)+(py`2)^2/(1+(py`2/py`1)^2)
by A47,SQUARE_1:def 4
.= ((py`1)^2+(py`2)^2)/(1+(py`2/py`1)^2) by XCMPLX_1:63;
then ((py`1)^2+(py`2)^2)/(1+(py`2/py`1)^2)*(1+(py`2/py`1)^2)
=(1)*(1+(py`2/py`1)^2) by A35,SQUARE_1:59;
then ((py`1)^2+(py`2)^2)=(1+(py`2/py`1)^2)
by A47,XCMPLX_1:88;
then (py`1)^2+(py`2)^2=1+(py`2)^2/(py`1)^2 by SQUARE_1:69;
then (py`1)^2+(py`2)^2-1=(py`2)^2/(py`1)^2 by XCMPLX_1:26;
then ((py`1)^2+(py`2)^2-1)*(py`1)^2=(py`2)^2 by A49,XCMPLX_1:88;
then ((py`1)^2+((py`2)^2-1))*(py`1)^2=(py`2)^2 by XCMPLX_1:29;
then (py`1)^2*(py`1)^2+((py`2)^2-1)*(py`1)^2=(py`2)^2 by XCMPLX_1:8;
then (py`1)^2*(py`1)^2+(py`1)^2*((py`2)^2-1)-(py`2)^2=0 by XCMPLX_1:14
;
then (py`1)^2*(py`1)^2+((py`1)^2*(py`2)^2-(py`1)^2*1)-(py`2)^2=0
by XCMPLX_1:40;
then (py`1)^2*(py`1)^2+(py`1)^2*(py`2)^2-(py`1)^2*1-(py`2)^2=0
by XCMPLX_1:29;
then (py`1)^2*(py`1)^2-(py`1)^2*1+(py`1)^2*(py`2)^2-(1)*(py`2)^2=0
by XCMPLX_1:29;
then (py`1)^2*((py`1)^2-1)+(py`1)^2*(py`2)^2-(1)*(py`2)^2=0
by XCMPLX_1:40;
then (py`1)^2*((py`1)^2-1)+((py`1)^2*(py`2)^2-(1)*(py`2)^2)=0
by XCMPLX_1:29;
hence ((py`1)^2-1)*(py`1)^2+((py`1)^2-1)*(py`2)^2=0 by XCMPLX_1:40;
end;
then A50:((py`1)^2-1)*((py`1)^2+(py`2)^2)=0 by XCMPLX_1:8;
((py`1)^2+(py`2)^2)<>0 by A40,COMPLEX1:2;
then ((py`1)^2-1)=0 by A50,XCMPLX_1:6;
then (py`1-1)*(py`1+1)=0 by SQUARE_1:59,67;
then A51: py`1-1=0 or py`1+1=0 by XCMPLX_1:6;
A52: now assume A53: py`1=-1;
then A54:p2`1<0 by A44,A45,A46,A48,REAL_2:128;
-p2`2<=--p2`1 by A35,REAL_1:50;
then -p2`2<0 by A44,A45,A46,A48,A53,REAL_2:128;
then --p2`2>-0 by REAL_1:50;
hence contradiction by A35,A54,AXIOMS:22;
end;
A55: (gg.O)=(Sq_Circ").(g.O) by A4,FUNCT_1:22;
consider p3 being Point of TOP-REAL 2 such that
A56: g.O=p3 &( |.p3.|=1 & p3`2<=p3`1 & p3`2<=-p3`1) by A1;
A57: -p3`2>=--p3`1 by A56,REAL_1:50;
then A58:p3<>0.REAL 2 &
(p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
by A56,TOPRNS_1:24;
then A59:Sq_Circ".p3=|[p3`1*sqrt(1+(p3`1/p3`2)^2),p3`2*sqrt(1+(p3`1/p3`2)^2)
]|
by JGRAPH_3:40;
reconsider pz=gg.O as Point of TOP-REAL 2;
A60: pz`2 = p3`2*sqrt(1+(p3`1/p3`2)^2) &
pz`1 = p3`1*sqrt(1+(p3`1/p3`2)^2) by A55,A56,A59,EUCLID:56;
(p3`1/p3`2)^2 >=0 by SQUARE_1:72;
then 1+(p3`1/p3`2)^2>=1+0 by REAL_1:55;
then 1+(p3`1/p3`2)^2>0 by AXIOMS:22;
then A61:sqrt(1+(p3`1/p3`2)^2)>0 by SQUARE_1:93;
A62:now assume
A63: pz`2=0 & pz`1=0;
then A64:p3`2=0 by A60,A61,XCMPLX_1:6;
p3`1=0 by A60,A61,A63,XCMPLX_1:6;
hence contradiction by A58,A64,EUCLID:57,58;
end;
A65: now
p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 &
p3`1*sqrt(1+(p3`1/p3`2)^2) <= (-p3`2)*sqrt(1+(p3`1/p3`2)^2)
by A56,A57,A61,AXIOMS:25;
then p3`1<=p3`2 & (-p3`2)*sqrt(1+(p3`1/p3`2)^2) <= p3`1*sqrt(1+(p3`1/p3`2
)^2)
or pz`1>=pz`2 & pz`1<=-pz`2 by A60,A61,AXIOMS:25,XCMPLX_1:175;
hence
p3`1*sqrt(1+(p3`1/p3`2)^2) <= p3`2*sqrt(1+(p3`1/p3`2)^2) & -pz`2<=pz`1
or pz`1>=pz`2 & pz`1<=-pz`2 by A60,A61,AXIOMS:25,XCMPLX_1:175;
end;
A66:p3=Sq_Circ.pz by A55,A56,FUNCT_1:54,JGRAPH_3:32,54;
A67:Sq_Circ.pz=|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|
by A60,A62,A65,JGRAPH_2:11,JGRAPH_3:14;
A68: (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`2
= pz`2/sqrt(1+(pz`1/pz`2)^2) &
(|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`1
= pz`1/sqrt(1+(pz`1/pz`2)^2) by EUCLID:56;
(pz`1/pz`2)^2 >=0 by SQUARE_1:72;
then 1+(pz`1/pz`2)^2>=1+0 by REAL_1:55;
then A69:1+(pz`1/pz`2)^2>0 by AXIOMS:22;
then A70:sqrt(1+(pz`1/pz`2)^2)>0 by SQUARE_1:93;
pz`2<>0 by A60,A62,A65;
then A71: (pz`2)^2<>0 by SQUARE_1:73;
A72:(|.p3.|)^2= (pz`2/sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by A66,A67,A68,JGRAPH_3:10
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by SQUARE_1:69
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2
+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by SQUARE_1:69
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by A69,SQUARE_1:def 4
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(1+(pz`1/pz`2)^2)
by A69,SQUARE_1:def 4
.= ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2) by XCMPLX_1:63;
now
((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)*(1+(pz`1/pz`2)^2)=(1)*(1+(pz`1/pz`2)^2
)
by A56,A72,SQUARE_1:59;
then ((pz`2)^2+(pz`1)^2)=(1+(pz`1/pz`2)^2) by A69,XCMPLX_1:88;
then (pz`2)^2+(pz`1)^2=1+(pz`1)^2/(pz`2)^2 by SQUARE_1:69;
then (pz`2)^2+(pz`1)^2-1=(pz`1)^2/(pz`2)^2 by XCMPLX_1:26;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2=(pz`1)^2 by A71,XCMPLX_1:88;
then ((pz`2)^2+((pz`1)^2-1))*(pz`2)^2=(pz`1)^2 by XCMPLX_1:29;
then (pz`2)^2*(pz`2)^2+((pz`1)^2-1)*(pz`2)^2=(pz`1)^2 by XCMPLX_1:8;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*((pz`1)^2-1)-(pz`1)^2=0 by XCMPLX_1:14
;
then (pz`2)^2*(pz`2)^2+((pz`2)^2*(pz`1)^2-(pz`2)^2*1)-(pz`1)^2=0
by XCMPLX_1:40;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*(pz`1)^2-(pz`2)^2*1-(pz`1)^2=0
by XCMPLX_1:29;
then (pz`2)^2*(pz`2)^2-(pz`2)^2*1+(pz`2)^2*(pz`1)^2-(1)*(pz`1)^2=0
by XCMPLX_1:29;hence
(pz`2)^2*((pz`2)^2-1)+(pz`2)^2*(pz`1)^2-(1)*(pz`1)^2=0
by XCMPLX_1:40;
end;
then (pz`2)^2*((pz`2)^2-1)+((pz`2)^2*(pz`1)^2-(1)*(pz`1)^2)=0
by XCMPLX_1:29;
then (pz`2)^2*((pz`2)^2-1)+((pz`2)^2-1)*(pz`1)^2=0 by XCMPLX_1:40;
then A73:((pz`2)^2-1)*((pz`2)^2+(pz`1)^2)=0 by XCMPLX_1:8;
((pz`2)^2+(pz`1)^2)<>0 by A62,COMPLEX1:2;
then ((pz`2)^2-1)=0 by A73,XCMPLX_1:6;
then (pz`2-1)*(pz`2+1)=0 by SQUARE_1:59,67;
then pz`2-1=0 or pz`2+1=0 by XCMPLX_1:6;
then pz`2=0+1 or pz`2+1=0 by XCMPLX_1:27;
then A74: pz`2=1 or pz`2=0-1 by XCMPLX_1:26;
A75: now assume A76: pz`2=1;
then A77:p3`2>0 by A66,A67,A68,A70,REAL_2:127;
-p3`1>0 by A56,A66,A67,A68,A70,A76,REAL_2:127;
then --p3`1<-0 by REAL_1:50;
hence contradiction by A56,A77,AXIOMS:22;
end;
A78: (gg.I)=(Sq_Circ").(g.I) by A4,FUNCT_1:22;
consider p4 being Point of TOP-REAL 2 such that
A79: g.I=p4 &(
|.p4.|=1 & p4`2>=p4`1 & p4`2>=-p4`1) by A1;
A80: -p4`2<=--p4`1 by A79,REAL_1:50;
then A81:p4<>0.REAL 2 & (p4`1<=p4`2 & -p4`2<=p4`1 or p4`1>=p4`2 & p4`1<=-p4
`2)
by A79,TOPRNS_1:24;
then A82:Sq_Circ".p4=|[p4`1*sqrt(1+(p4`1/p4`2)^2),p4`2*sqrt(1+(p4`1/p4`2)^2
)]|
by JGRAPH_3:40;
reconsider pu=gg.I as Point of TOP-REAL 2;
A83: pu`2 = p4`2*sqrt(1+(p4`1/p4`2)^2) &
pu`1 = p4`1*sqrt(1+(p4`1/p4`2)^2) by A78,A79,A82,EUCLID:56;
(p4`1/p4`2)^2 >=0 by SQUARE_1:72;
then 1+(p4`1/p4`2)^2>=1+0 by REAL_1:55;
then 1+(p4`1/p4`2)^2>0 by AXIOMS:22;
then A84:sqrt(1+(p4`1/p4`2)^2)>0 by SQUARE_1:93;
A85:now assume
A86: pu`2=0 & pu`1=0;
then A87:p4`2=0 by A83,A84,XCMPLX_1:6;
p4`1=0 by A83,A84,A86,XCMPLX_1:6;
hence contradiction by A81,A87,EUCLID:57,58;
end;
A88: now
p4`1<=p4`2 & (-p4`2)*sqrt(1+(p4`1/p4`2)^2) <= p4`1*sqrt(1+(p4`1/p4`2)^2)
or pu`1>=pu`2 & pu`1<=-pu`2 by A79,A80,A84,AXIOMS:25;hence
p4`1*sqrt(1+(p4`1/p4`2)^2) <= p4`2*sqrt(1+(p4`1/p4`2)^2) & -pu`2<=pu`1
or pu`1>=pu`2 & pu`1<=-pu`2 by A83,A84,AXIOMS:25,XCMPLX_1:175;
end;
A89:p4=Sq_Circ.pu by A78,A79,FUNCT_1:54,JGRAPH_3:32,54;
A90:Sq_Circ.pu=|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|
by A83,A85,A88,JGRAPH_2:11,JGRAPH_3:14;
A91: (|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|)`2
= pu`2/sqrt(1+(pu`1/pu`2)^2) &
(|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|)`1
= pu`1/sqrt(1+(pu`1/pu`2)^2) by EUCLID:56;
(pu`1/pu`2)^2 >=0 by SQUARE_1:72;
then 1+(pu`1/pu`2)^2>=1+0 by REAL_1:55;
then A92:1+(pu`1/pu`2)^2>0 by AXIOMS:22;
then A93:sqrt(1+(pu`1/pu`2)^2)>0 by SQUARE_1:93;
pu`2<>0 by A83,A85,A88;
then A94: (pu`2)^2<>0 by SQUARE_1:73;
now
(|.p4.|)^2= (pu`2/sqrt(1+(pu`1/pu`2)^2))^2+(pu`1/sqrt(1+(pu`1/pu`2)^2))^2
by A89,A90,A91,JGRAPH_3:10
.= (pu`2)^2/(sqrt(1+(pu`1/pu`2)^2))^2+(pu`1/sqrt(1+(pu`1/pu`2)^2))^2
by SQUARE_1:69
.= (pu`2)^2/(sqrt(1+(pu`1/pu`2)^2))^2
+(pu`1)^2/(sqrt(1+(pu`1/pu`2)^2))^2
by SQUARE_1:69
.= (pu`2)^2/(1+(pu`1/pu`2)^2)+(pu`1)^2/(sqrt(1+(pu`1/pu`2)^2))^2
by A92,SQUARE_1:def 4
.= (pu`2)^2/(1+(pu`1/pu`2)^2)+(pu`1)^2/(1+(pu`1/pu`2)^2)
by A92,SQUARE_1:def 4
.= ((pu`2)^2+(pu`1)^2)/(1+(pu`1/pu`2)^2) by XCMPLX_1:63;
then ((pu`2)^2+(pu`1)^2)/(1+(pu`1/pu`2)^2)*(1+(pu`1/pu`2)^2)=(1)*(1+(pu`1/pu
`2)^2)
by A79,SQUARE_1:59;
then ((pu`2)^2+(pu`1)^2)=(1+(pu`1/pu`2)^2)
by A92,XCMPLX_1:88;
then (pu`2)^2+(pu`1)^2=1+(pu`1)^2/(pu`2)^2 by SQUARE_1:69;
then (pu`2)^2+(pu`1)^2-1=(pu`1)^2/(pu`2)^2 by XCMPLX_1:26;
then ((pu`2)^2+(pu`1)^2-1)*(pu`2)^2=(pu`1)^2
by A94,XCMPLX_1:88;
then ((pu`2)^2+((pu`1)^2-1))*(pu`2)^2=(pu`1)^2 by XCMPLX_1:29;
then (pu`2)^2*(pu`2)^2+((pu`1)^2-1)*(pu`2)^2=(pu`1)^2 by XCMPLX_1:8;
then (pu`2)^2*(pu`2)^2+(pu`2)^2*((pu`1)^2-1)-(pu`1)^2=0 by XCMPLX_1:14
;
then (pu`2)^2*(pu`2)^2+((pu`2)^2*(pu`1)^2-(pu`2)^2*1)-(pu`1)^2=0
by XCMPLX_1:40;
then (pu`2)^2*(pu`2)^2+(pu`2)^2*(pu`1)^2-(pu`2)^2*1-(pu`1)^2=0
by XCMPLX_1:29;
then (pu`2)^2*(pu`2)^2-(pu`2)^2*1+(pu`2)^2*(pu`1)^2-(1)*(pu`1)^2=0
by XCMPLX_1:29;
then (pu`2)^2*((pu`2)^2-1)+(pu`2)^2*(pu`1)^2-(1)*(pu`1)^2=0
by XCMPLX_1:40;
then (pu`2)^2*((pu`2)^2-1)+((pu`2)^2*(pu`1)^2-(1)*(pu`1)^2)=0
by XCMPLX_1:29;
hence ((pu`2)^2-1)*(pu`2)^2+((pu`2)^2-1)*(pu`1)^2=0 by XCMPLX_1:40;
end;
then A95:((pu`2)^2-1)*((pu`2)^2+(pu`1)^2)=0 by XCMPLX_1:8;
((pu`2)^2+(pu`1)^2)<>0 by A85,COMPLEX1:2;
then ((pu`2)^2-1)=0 by A95,XCMPLX_1:6;
then (pu`2-1)*(pu`2+1)=0 by SQUARE_1:59,67;
then pu`2-1=0 or pu`2+1=0 by XCMPLX_1:6;
then A96: pu`2=0+1 or pu`2+1=0 by XCMPLX_1:27;
now assume A97: pu`2=-1;
then A98:p4`2<0 by A89,A90,A91,A93,REAL_2:128;
-p4`1<0 by A79,A89,A90,A91,A93,A97,REAL_2:128;
then --p4`1>-0 by REAL_1:50;
hence contradiction by A79,A98,AXIOMS:22;
end;
hence thesis by A30,A31,A51,A52,A74,A75,A96,XCMPLX_1:26,27;
end;
A99: for r being Point of I[01] holds
(-1>=(ff.r)`1 or (ff.r)`1>=1 or -1 >=(ff.r)`2 or (ff.r)`2>=1)
& (-1>=(gg.r)`1 or (gg.r)`1>=1 or -1 >=(gg.r)`2 or (gg.r)`2>=1)
proof let r be Point of I[01];
A100: (ff.r)=(Sq_Circ").(f.r) by A3,FUNCT_1:22;
f.r in rng f by A5,FUNCT_1:12;
then f.r in C0 by A1;
then consider p1 being Point of TOP-REAL 2 such that
A101: f.r=p1 & |.p1.|>=1 by A1;
A102:now per cases;
case A103: p1=0.REAL 2;
|.0.REAL 2.|=0 by TOPRNS_1:24;
hence contradiction by A101,A103;
case
A104:p1<>0.REAL 2 &
(p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 & p1`2<=-p1`1);
then A105:Sq_Circ".p1=|[p1`1*sqrt(1+(p1`2/p1`1)^2),p1`2*sqrt(1+(p1`2/p1`1)^2
)]|
by JGRAPH_3:38;
reconsider px=ff.r as Point of TOP-REAL 2;
set q=px;
A106: px`1 = p1`1*sqrt(1+(p1`2/p1`1)^2) &
px`2 = p1`2*sqrt(1+(p1`2/p1`1)^2) by A100,A101,A105,EUCLID:56;
(p1`2/p1`1)^2 >=0 by SQUARE_1:72;
then 1+(p1`2/p1`1)^2>=1+0 by REAL_1:55;
then 1+(p1`2/p1`1)^2>0 by AXIOMS:22;
then A107:sqrt(1+(p1`2/p1`1)^2)>0 by SQUARE_1:93;
A108:now assume
A109: px`1=0 & px`2=0;
then A110:p1`1=0 by A106,A107,XCMPLX_1:6;
p1`2=0 by A106,A107,A109,XCMPLX_1:6;
hence contradiction by A104,A110,EUCLID:57,58;
end;
A111: now
p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 &
p1`2*sqrt(1+(p1`2/p1`1)^2) <= (-p1`1)*sqrt(1+(p1`2/p1`1)^2)
by A104,A107,AXIOMS:25;
then p1`2<=p1`1 & (-p1`1)*sqrt(1+(p1`2/p1`1)^2) <= p1`2*sqrt(1+(p1`2/p1`1
)^2)
or px`2>=px`1 & px`2<=-px`1 by A106,A107,AXIOMS:25,XCMPLX_1:175;
hence
p1`2*sqrt(1+(p1`2/p1`1)^2) <= p1`1*sqrt(1+(p1`2/p1`1)^2) & -px`1<=px`2
or px`2>=px`1 & px`2<=-px`1 by A106,A107,AXIOMS:25,XCMPLX_1:175;
end;
A112:p1=Sq_Circ.px by A100,A101,FUNCT_1:54,JGRAPH_3:32,54;
A113:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by A106,A108,A111,JGRAPH_2:11,JGRAPH_3:def 1;
A114: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1
= q`1/sqrt(1+(q`2/q`1)^2) &
(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2
= q`2/sqrt(1+(q`2/q`1)^2) by EUCLID:56;
A115:(px`1)^2 >=0 by SQUARE_1:72;
(q`2/q`1)^2 >=0 by SQUARE_1:72;
then 1+(q`2/q`1)^2>=1+0 by REAL_1:55;
then A116:1+(q`2/q`1)^2>0 by AXIOMS:22;
(|.p1.|)^2>=|.p1.| by A101,JGRAPH_2:2;
then A117: (|.p1.|)^2>=1 by A101,AXIOMS:22;
px`1<>0 by A106,A108,A111;
then A118: (px`1)^2<>0 by SQUARE_1:73;
now
(|.p1.|)^2= (q`1/sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2
by A112,A113,A114,JGRAPH_3:10
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A116,SQUARE_1:def 4
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A116,SQUARE_1:def 4
.= ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)
by XCMPLX_1:63;
then ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)*(1+(q`2/q`1)^2)>=(1)*(1+(q`2/q
`1)^2)
by A116,A117,AXIOMS:25;
then ((q`1)^2+(q`2)^2)>=(1+(q`2/q`1)^2)
by A116,XCMPLX_1:88;
then (px`1)^2+(px`2)^2>=1+(px`2)^2/(px`1)^2 by SQUARE_1:69;
then (px`1)^2+(px`2)^2-1>=1+(px`2)^2/(px`1)^2-1 by REAL_1:49;
then (px`1)^2+(px`2)^2-1>=(px`2)^2/(px`1)^2 by XCMPLX_1:26;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=(px`2)^2/(px`1)^2*(px`1)^2
by A115,AXIOMS:25;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=(px`2)^2
by A118,XCMPLX_1:88;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2>=(px`2)^2 by XCMPLX_1:29;
then (px`1)^2*(px`1)^2+((px`2)^2-1)*(px`1)^2>=(px`2)^2 by XCMPLX_1:8;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>=(px`2)^2-(px`2
)^2
by REAL_1:49;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>=0 by XCMPLX_1:
14
;
then (px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2>=0
by XCMPLX_1:40;
then (px`1)^2*(px`1)^2+(px`1)^2*(px`2)^2-(px`1)^2*1-(px`2)^2>=0
by XCMPLX_1:29;
then (px`1)^2*(px`1)^2-(px`1)^2*1+(px`1)^2*(px`2)^2-(1)*(px`2)^2>=0
by XCMPLX_1:29;
then (px`1)^2*((px`1)^2-1)+(px`1)^2*(px`2)^2-(1)*(px`2)^2>=0
by XCMPLX_1:40;
then (px`1)^2*((px`1)^2-1)+((px`1)^2*(px`2)^2-(1)*(px`2)^2)>=0
by XCMPLX_1:29;hence
((px`1)^2-1)*(px`1)^2+((px`1)^2-1)*(px`2)^2>=0 by XCMPLX_1:40;
end;
then A119:((px`1)^2-1)*((px`1)^2+(px`2)^2)>=0 by XCMPLX_1:8;
A120: ((px`1)^2+(px`2)^2)<>0 by A108,COMPLEX1:2;
(px`2)^2>=0 by SQUARE_1:72;
then ((px`1)^2+(px`2)^2)>=0+0 by A115,REAL_1:55;
then ((px`1)^2-1)>=0 by A119,A120,SQUARE_1:25;
then (px`1-1)*(px`1+1)>=0 by SQUARE_1:59,67;
hence -1>=(ff.r)`1 or (ff.r)`1>=1 or
-1 >=(ff.r)`2 or (ff.r)`2>=1 by Th1;
case
A121:p1<>0.REAL 2 &
not(p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 & p1`2<=-p1`1);
then A122:Sq_Circ".p1=|[p1`1*sqrt(1+(p1`1/p1`2)^2),p1`2*sqrt(1+(p1`1/p1`2)
^2)]|
by JGRAPH_3:38;
A123:p1<>0.REAL 2 &
(p1`1<=p1`2 & -p1`2<=p1`1 or p1`1>=p1`2 & p1`1<=-p1`2)
by A121,JGRAPH_2:23;
reconsider pz=ff.r as Point of TOP-REAL 2;
A124: pz`2 = p1`2*sqrt(1+(p1`1/p1`2)^2) &
pz`1 = p1`1*sqrt(1+(p1`1/p1`2)^2) by A100,A101,A122,EUCLID:56;
(p1`1/p1`2)^2 >=0 by SQUARE_1:72;
then 1+(p1`1/p1`2)^2>=1+0 by REAL_1:55;
then 1+(p1`1/p1`2)^2>0 by AXIOMS:22;
then A125:sqrt(1+(p1`1/p1`2)^2)>0 by SQUARE_1:93;
A126:now assume
A127: pz`2=0 & pz`1=0;
then p1`2=0 by A124,A125,XCMPLX_1:6;
hence contradiction by A121,A124,A125,A127,XCMPLX_1:6;
end;
A128: now
p1`1<=p1`2 & -p1`2<=p1`1 or p1`1>=p1`2 &
p1`1*sqrt(1+(p1`1/p1`2)^2) <= (-p1`2)*sqrt(1+(p1`1/p1`2)^2)
by A123,A125,AXIOMS:25;
then p1`1<=p1`2 & (-p1`2)*sqrt(1+(p1`1/p1`2)^2) <= p1`1*sqrt(1+(p1`1/p1`2
)^2)
or pz`1>=pz`2 & pz`1<=-pz`2 by A124,A125,AXIOMS:25,XCMPLX_1:175;
hence
p1`1*sqrt(1+(p1`1/p1`2)^2) <= p1`2*sqrt(1+(p1`1/p1`2)^2) & -pz`2<=pz`1
or pz`1>=pz`2 & pz`1<=-pz`2 by A124,A125,AXIOMS:25,XCMPLX_1:175;
end;
A129:p1=Sq_Circ.pz by A100,A101,FUNCT_1:54,JGRAPH_3:32,54;
A130:Sq_Circ.pz=|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|
by A124,A126,A128,JGRAPH_2:11,JGRAPH_3:14;
A131: (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`2
= pz`2/sqrt(1+(pz`1/pz`2)^2) &
(|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`1
= pz`1/sqrt(1+(pz`1/pz`2)^2) by EUCLID:56;
A132:(pz`2)^2 >=0 by SQUARE_1:72;
(pz`1/pz`2)^2 >=0 by SQUARE_1:72;
then 1+(pz`1/pz`2)^2>=1+0 by REAL_1:55;
then A133:1+(pz`1/pz`2)^2>0 by AXIOMS:22;
(|.p1.|)^2>=|.p1.| by A101,JGRAPH_2:2;
then A134: (|.p1.|)^2>=1 by A101,AXIOMS:22;
pz`2<>0 by A124,A126,A128;
then A135: (pz`2)^2<>0 by SQUARE_1:73;
A136:(|.p1.|)^2= (pz`2/sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by A129,A130,A131,JGRAPH_3:10
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by SQUARE_1:69
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2
+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by SQUARE_1:69
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by A133,SQUARE_1:def 4
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(1+(pz`1/pz`2)^2)
by A133,SQUARE_1:def 4
.= ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)
by XCMPLX_1:63;
now
((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)*(1+(pz`1/pz`2)^2)
>=(1)*(1+(pz`1/pz`2)^2)
by A133,A134,A136,AXIOMS:25;
then ((pz`2)^2+(pz`1)^2)>=(1+(pz`1/pz`2)^2)
by A133,XCMPLX_1:88;
then (pz`2)^2+(pz`1)^2>=1+(pz`1)^2/(pz`2)^2 by SQUARE_1:69;
then (pz`2)^2+(pz`1)^2-1>=1+(pz`1)^2/(pz`2)^2-1 by REAL_1:49;
then (pz`2)^2+(pz`1)^2-1>=(pz`1)^2/(pz`2)^2 by XCMPLX_1:26;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2>=(pz`1)^2/(pz`2)^2*(pz`2)^2
by A132,AXIOMS:25;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2>=(pz`1)^2
by A135,XCMPLX_1:88;
then ((pz`2)^2+((pz`1)^2-1))*(pz`2)^2>=(pz`1)^2 by XCMPLX_1:29;
then (pz`2)^2*(pz`2)^2+((pz`1)^2-1)*(pz`2)^2>=(pz`1)^2 by XCMPLX_1:8;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*((pz`1)^2-1)-(pz`1)^2
>=(pz`1)^2-(pz`1)^2 by REAL_1:49;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*((pz`1)^2-1)-(pz`1)^2>=0 by XCMPLX_1:
14
;
then (pz`2)^2*(pz`2)^2+((pz`2)^2*(pz`1)^2-(pz`2)^2*1)-(pz`1)^2>=0
by XCMPLX_1:40;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*(pz`1)^2-(pz`2)^2*1-(pz`1)^2>=0
by XCMPLX_1:29;
then (pz`2)^2*(pz`2)^2-(pz`2)^2*1+(pz`2)^2*(pz`1)^2-(1)*(pz`1)^2>=0
by XCMPLX_1:29;
hence (pz`2)^2*((pz`2)^2-1)+(pz`2)^2*(pz`1)^2-(1)*(pz`1)^2>=0
by XCMPLX_1:40;
end;
then (pz`2)^2*((pz`2)^2-1)+((pz`2)^2*(pz`1)^2-(1)*(pz`1)^2)>=0
by XCMPLX_1:29;
then (pz`2)^2*((pz`2)^2-1)+((pz`2)^2-1)*(pz`1)^2>=0
by XCMPLX_1:40;
then A137:((pz`2)^2-1)*((pz`2)^2+(pz`1)^2)>=0 by XCMPLX_1:8;
A138: ((pz`2)^2+(pz`1)^2)<>0 by A126,COMPLEX1:2;
(pz`1)^2>=0 by SQUARE_1:72;
then (pz`2)^2+(pz`1)^2>=0+0 by A132,REAL_1:55;
then (pz`2)^2-1>=0 by A137,A138,SQUARE_1:25;
then (pz`2-1)*(pz`2+1)>=0 by SQUARE_1:59,67;
hence -1>=(ff.r)`1 or (ff.r)`1>=1 or
-1 >=(ff.r)`2 or (ff.r)`2>=1 by Th1;
end;
A139: (gg.r)=(Sq_Circ").(g.r) by A4,FUNCT_1:22;
g.r in rng g by A6,FUNCT_1:12;
then g.r in C0 by A1;
then consider p2 being Point of TOP-REAL 2 such that
A140: g.r=p2 & |.p2.|>=1 by A1;
now per cases;
case A141: p2=0.REAL 2;
|.0.REAL 2.|=0 by TOPRNS_1:24;
hence contradiction by A140,A141;
case
A142:p2<>0.REAL 2 &
(p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 & p2`2<=-p2`1);
then A143:Sq_Circ".p2=|[p2`1*sqrt(1+(p2`2/p2`1)^2),p2`2*sqrt(1+(p2`2/p2`1)^2
)]|
by JGRAPH_3:38;
reconsider px=gg.r as Point of TOP-REAL 2;
set q=px;
A144:Sq_Circ".p2=q by A4,A140,FUNCT_1:22;
A145: px`1 = p2`1*sqrt(1+(p2`2/p2`1)^2) &
px`2 = p2`2*sqrt(1+(p2`2/p2`1)^2) by A139,A140,A143,EUCLID:56;
(p2`2/p2`1)^2 >=0 by SQUARE_1:72;
then 1+(p2`2/p2`1)^2>=1+0 by REAL_1:55;
then 1+(p2`2/p2`1)^2>0 by AXIOMS:22;
then A146:sqrt(1+(p2`2/p2`1)^2)>0 by SQUARE_1:93;
A147:now assume
A148: px`1=0 & px`2=0;
then A149:p2`1=0 by A145,A146,XCMPLX_1:6;
p2`2=0 by A145,A146,A148,XCMPLX_1:6;
hence contradiction by A142,A149,EUCLID:57,58;
end;
A150: now
p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 &
p2`2*sqrt(1+(p2`2/p2`1)^2) <= (-p2`1)*sqrt(1+(p2`2/p2`1)^2)
by A142,A146,AXIOMS:25;
then p2`2<=p2`1 & (-p2`1)*sqrt(1+(p2`2/p2`1)^2) <= p2`2*sqrt(1+(p2`2/p2`1
)^2)
or px`2>=px`1 & px`2<=-px`1 by A145,A146,AXIOMS:25,XCMPLX_1:175
;hence
p2`2*sqrt(1+(p2`2/p2`1)^2) <= p2`1*sqrt(1+(p2`2/p2`1)^2) & -px`1<=px
`2
or px`2>=px`1 & px`2<=-px`1 by A145,A146,AXIOMS:25,XCMPLX_1:175;
end;
A151:p2=Sq_Circ.px by A144,FUNCT_1:54,JGRAPH_3:32,54;
A152:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by A145,A147,A150,JGRAPH_2:11,JGRAPH_3:def 1;
A153: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1
= q`1/sqrt(1+(q`2/q`1)^2) &
(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2
= q`2/sqrt(1+(q`2/q`1)^2) by EUCLID:56;
A154:(px`1)^2 >=0 by SQUARE_1:72;
(q`2/q`1)^2 >=0 by SQUARE_1:72;
then 1+(q`2/q`1)^2>=1+0 by REAL_1:55;
then A155:1+(q`2/q`1)^2>0 by AXIOMS:22;
(|.p2.|)^2>=|.p2.| by A140,JGRAPH_2:2;
then A156: (|.p2.|)^2>=1 by A140,AXIOMS:22;
px`1<>0 by A145,A147,A150;
then A157: (px`1)^2<>0 by SQUARE_1:73;
now
(|.p2.|)^2= (q`1/sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2
by A151,A152,A153,JGRAPH_3:10
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A155,SQUARE_1:def 4
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A155,SQUARE_1:def 4
.= ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)
by XCMPLX_1:63;
then ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)*(1+(q`2/q`1)^2)>=(1)*(1+(q`2/q
`1)^2)
by A155,A156,AXIOMS:25;
then ((q`1)^2+(q`2)^2)>=(1+(q`2/q`1)^2)
by A155,XCMPLX_1:88;
then (px`1)^2+(px`2)^2>=1+(px`2)^2/(px`1)^2 by SQUARE_1:69;
then (px`1)^2+(px`2)^2-1>=1+(px`2)^2/(px`1)^2-1 by REAL_1:49;
then (px`1)^2+(px`2)^2-1>=(px`2)^2/(px`1)^2 by XCMPLX_1:26;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=(px`2)^2/(px`1)^2*(px`1)^2
by A154,AXIOMS:25;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2>=(px`2)^2
by A157,XCMPLX_1:88;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2>=(px`2)^2 by XCMPLX_1:29;
then (px`1)^2*(px`1)^2+((px`2)^2-1)*(px`1)^2>=(px`2)^2 by XCMPLX_1:8;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>=(px`2)^2-(px`2
)^2
by REAL_1:49;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2>=0 by XCMPLX_1:
14
;
then (px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2>=0
by XCMPLX_1:40;
then (px`1)^2*(px`1)^2+(px`1)^2*(px`2)^2-(px`1)^2*1-(px`2)^2>=0
by XCMPLX_1:29;
then (px`1)^2*(px`1)^2-(px`1)^2*1+(px`1)^2*(px`2)^2-(1)*(px`2)^2>=0
by XCMPLX_1:29;
then (px`1)^2*((px`1)^2-1)+(px`1)^2*(px`2)^2-(1)*(px`2)^2>=0
by XCMPLX_1:40;
then (px`1)^2*((px`1)^2-1)+((px`1)^2*(px`2)^2-(1)*(px`2)^2)>=0
by XCMPLX_1:29;hence
((px`1)^2-1)*(px`1)^2+((px`1)^2-1)*(px`2)^2>=0 by XCMPLX_1:40;
end;
then A158:((px`1)^2-1)*((px`1)^2+(px`2)^2)>=0 by XCMPLX_1:8;
A159: ((px`1)^2+(px`2)^2)<>0 by A147,COMPLEX1:2;
(px`2)^2>=0 by SQUARE_1:72;
then ((px`1)^2+(px`2)^2)>=0+0 by A154,REAL_1:55;
then ((px`1)^2-1)>=0 by A158,A159,SQUARE_1:25;
then (px`1-1)*(px`1+1)>=0 by SQUARE_1:59,67;
hence -1>=(gg.r)`1 or (gg.r)`1>=1 or -1 >=(gg.r)`2 or (gg.r)`2>=1
by Th1;
case
A160:p2<>0.REAL 2 &
not(p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 & p2`2<=-p2`1);
then A161:Sq_Circ".p2=|[p2`1*sqrt(1+(p2`1/p2`2)^2),p2`2*sqrt(1+(p2`1/p2`2)^2
)]|
by JGRAPH_3:38;
A162:p2<>0.REAL 2 &
(p2`1<=p2`2 & -p2`2<=p2`1 or p2`1>=p2`2 & p2`1<=-p2`2)
by A160,JGRAPH_2:23;
reconsider pz=gg.r as Point of TOP-REAL 2;
A163: pz`2 = p2`2*sqrt(1+(p2`1/p2`2)^2) &
pz`1 = p2`1*sqrt(1+(p2`1/p2`2)^2) by A139,A140,A161,EUCLID:56;
(p2`1/p2`2)^2 >=0 by SQUARE_1:72;
then 1+(p2`1/p2`2)^2>=1+0 by REAL_1:55;
then 1+(p2`1/p2`2)^2>0 by AXIOMS:22;
then A164:sqrt(1+(p2`1/p2`2)^2)>0 by SQUARE_1:93;
A165:now assume
A166: pz`2=0 & pz`1=0;
then p2`2=0 by A163,A164,XCMPLX_1:6;
hence contradiction by A160,A163,A164,A166,XCMPLX_1:6;
end;
A167: now
p2`1<=p2`2 & -p2`2<=p2`1 or p2`1>=p2`2 &
p2`1*sqrt(1+(p2`1/p2`2)^2) <= (-p2`2)*sqrt(1+(p2`1/p2`2)^2)
by A162,A164,AXIOMS:25;
then p2`1<=p2`2 & (-p2`2)*sqrt(1+(p2`1/p2`2)^2) <= p2`1*sqrt(1+(p2`1/p2`2)
^2)
or pz`1>=pz`2 & pz`1<=-pz`2 by A163,A164,AXIOMS:25,XCMPLX_1:175;
hence
p2`1*sqrt(1+(p2`1/p2`2)^2) <= p2`2*sqrt(1+(p2`1/p2`2)^2) & -pz`2<=pz`1
or pz`1>=pz`2 & pz`1<=-pz`2 by A163,A164,AXIOMS:25,XCMPLX_1:175;
end;
A168:p2=Sq_Circ.pz by A139,A140,FUNCT_1:54,JGRAPH_3:32,54;
A169:Sq_Circ.pz=|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|
by A163,A165,A167,JGRAPH_2:11,JGRAPH_3:14;
A170: (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`2
= pz`2/sqrt(1+(pz`1/pz`2)^2) &
(|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`1
= pz`1/sqrt(1+(pz`1/pz`2)^2) by EUCLID:56;
A171:(pz`2)^2 >=0 by SQUARE_1:72;
(pz`1/pz`2)^2 >=0 by SQUARE_1:72;
then 1+(pz`1/pz`2)^2>=1+0 by REAL_1:55;
then A172:1+(pz`1/pz`2)^2>0 by AXIOMS:22;
(|.p2.|)^2>=|.p2.| by A140,JGRAPH_2:2;
then A173: (|.p2.|)^2>=1 by A140,AXIOMS:22;
pz`2<>0 by A163,A165,A167;
then A174: (pz`2)^2<>0 by SQUARE_1:73;
A175:(|.p2.|)^2= (pz`2/sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by A168,A169,A170,JGRAPH_3:10
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by SQUARE_1:69
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2
+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by SQUARE_1:69
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by A172,SQUARE_1:def 4
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(1+(pz`1/pz`2)^2)
by A172,SQUARE_1:def 4
.= ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)
by XCMPLX_1:63;
now
((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)*(1+(pz`1/pz`2)^2)
>=(1)*(1+(pz`1/pz`2)^2)
by A172,A173,A175,AXIOMS:25;
then ((pz`2)^2+(pz`1)^2)>=(1+(pz`1/pz`2)^2) by A172,XCMPLX_1:88;
then (pz`2)^2+(pz`1)^2>=1+(pz`1)^2/(pz`2)^2 by SQUARE_1:69;
then (pz`2)^2+(pz`1)^2-1>=1+(pz`1)^2/(pz`2)^2-1 by REAL_1:49;
then (pz`2)^2+(pz`1)^2-1>=(pz`1)^2/(pz`2)^2 by XCMPLX_1:26;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2>=(pz`1)^2/(pz`2)^2*(pz`2)^2
by A171,AXIOMS:25;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2>=(pz`1)^2 by A174,XCMPLX_1:88;
then ((pz`2)^2+((pz`1)^2-1))*(pz`2)^2>=(pz`1)^2 by XCMPLX_1:29;
then (pz`2)^2*(pz`2)^2+((pz`1)^2-1)*(pz`2)^2>=(pz`1)^2 by XCMPLX_1:8;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*((pz`1)^2-1)-(pz`1)^2
>=(pz`1)^2-(pz`1)^2 by REAL_1:49;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*((pz`1)^2-1)-(pz`1)^2>=0 by XCMPLX_1:
14
;
then (pz`2)^2*(pz`2)^2+((pz`2)^2*(pz`1)^2-(pz`2)^2*1)-(pz`1)^2>=0
by XCMPLX_1:40;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*(pz`1)^2-(pz`2)^2*1-(pz`1)^2>=0
by XCMPLX_1:29;
then (pz`2)^2*(pz`2)^2-(pz`2)^2*1+(pz`2)^2*(pz`1)^2-(1)*(pz`1)^2>=0
by XCMPLX_1:29;hence
(pz`2)^2*((pz`2)^2-1)+(pz`2)^2*(pz`1)^2-(1)*(pz`1)^2>=0
by XCMPLX_1:40;
end;
then (pz`2)^2*((pz`2)^2-1)+((pz`2)^2*(pz`1)^2-(1)*(pz`1)^2)>=0
by XCMPLX_1:29;
then (pz`2)^2*((pz`2)^2-1)+((pz`2)^2-1)*(pz`1)^2>=0
by XCMPLX_1:40;
then A176:((pz`2)^2-1)*((pz`2)^2+(pz`1)^2)>=0 by XCMPLX_1:8;
A177: ((pz`2)^2+(pz`1)^2)<>0 by A165,COMPLEX1:2;
(pz`1)^2>=0 by SQUARE_1:72;
then ((pz`2)^2+(pz`1)^2)>=0+0 by A171,REAL_1:55;
then ((pz`2)^2-1)>=0 by A176,A177,SQUARE_1:25;
then (pz`2-1)*(pz`2+1)>=0 by SQUARE_1:59,67;
hence -1>=(gg.r)`1 or (gg.r)`1>=1 or
-1 >=(gg.r)`2 or (gg.r)`2>=1 by Th1;
end;
hence
(-1>=(ff.r)`1 or (ff.r)`1>=1 or -1 >=(ff.r)`2 or (ff.r)`2>=1)
& (-1>=(gg.r)`1 or (gg.r)`1>=1 or -1 >=(gg.r)`2 or (gg.r)`2>=1)
by A102;
end;
(-1 <=(ff.O)`2 & (ff.O)`2 <= 1) &
(-1 <=(ff.I)`2 & (ff.I)`2 <= 1) &
(-1 <=(gg.O)`1 & (gg.O)`1 <= 1) &
(-1 <=(gg.I)`1 & (gg.I)`1 <= 1)
proof
A178: (ff.O)=(Sq_Circ").(f.O) by A3,FUNCT_1:22;
consider p1 being Point of TOP-REAL 2 such that
A179: f.O=p1 &( |.p1.|=1 & p1`2>=p1`1 & p1`2<=-p1`1) by A1;
A180:p1<>0.REAL 2 &
(p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 & p1`2<=-p1`1)
by A179,TOPRNS_1:24;
then A181:Sq_Circ".p1=|[p1`1*sqrt(1+(p1`2/p1`1)^2),p1`2*sqrt(1+(p1`2/p1`1)
^2)]|
by JGRAPH_3:38;
reconsider px=ff.O as Point of TOP-REAL 2;
set q=px;
A182: px`1 = p1`1*sqrt(1+(p1`2/p1`1)^2) &
px`2 = p1`2*sqrt(1+(p1`2/p1`1)^2) by A178,A179,A181,EUCLID:56;
(p1`2/p1`1)^2 >=0 by SQUARE_1:72;
then 1+(p1`2/p1`1)^2>=1+0 by REAL_1:55;
then 1+(p1`2/p1`1)^2>0 by AXIOMS:22;
then A183:sqrt(1+(p1`2/p1`1)^2)>0 by SQUARE_1:93;
A184:now assume
A185: px`1=0 & px`2=0;
then A186:p1`1=0 by A182,A183,XCMPLX_1:6;
p1`2=0 by A182,A183,A185,XCMPLX_1:6;
hence contradiction by A180,A186,EUCLID:57,58;
end;
p1`2<=p1`1 & -p1`1<=p1`2 or p1`2>=p1`1 &
p1`2*sqrt(1+(p1`2/p1`1)^2) <= (-p1`1)*sqrt(1+(p1`2/p1`1)^2)
by A179,A183,AXIOMS:25;
then p1`2<=p1`1 & (-p1`1)*sqrt(1+(p1`2/p1`1)^2) <= p1`2*sqrt(1+(p1`2/p1`1
)^2)
or px`2>=px`1 & px`2<=-px`1 by A182,A183,AXIOMS:25,XCMPLX_1:175;
then A187:px`2<=px`1 & -px`1<=px`2 or px`2>=px`1 & px`2<=-px`1
by A182,A183,AXIOMS:25,XCMPLX_1:175;
A188:p1=Sq_Circ.px by A178,A179,FUNCT_1:54,JGRAPH_3:32,54;
A189:Sq_Circ.q=|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|
by A184,A187,JGRAPH_2:11,JGRAPH_3:def 1;
A190: (|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`1
= q`1/sqrt(1+(q`2/q`1)^2) &
(|[q`1/sqrt(1+(q`2/q`1)^2),q`2/sqrt(1+(q`2/q`1)^2)]|)`2
= q`2/sqrt(1+(q`2/q`1)^2) by EUCLID:56;
(q`2/q`1)^2 >=0 by SQUARE_1:72;
then 1+(q`2/q`1)^2>=1+0 by REAL_1:55;
then A191:1+(q`2/q`1)^2>0 by AXIOMS:22;
px`1<>0 by A184,A187;
then A192: (px`1)^2<>0 by SQUARE_1:73;
now
(|.p1.|)^2= (q`1/sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2
by A188,A189,A190,JGRAPH_3:10
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2/sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69
.= (q`1)^2/(sqrt(1+(q`2/q`1)^2))^2+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by SQUARE_1:69
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(sqrt(1+(q`2/q`1)^2))^2
by A191,SQUARE_1:def 4
.= (q`1)^2/(1+(q`2/q`1)^2)+(q`2)^2/(1+(q`2/q`1)^2)
by A191,SQUARE_1:def 4
.= ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2) by XCMPLX_1:63;
then ((q`1)^2+(q`2)^2)/(1+(q`2/q`1)^2)*(1+(q`2/q`1)^2)=(1)*(1+(q`2/q`1
)^2)
by A179,SQUARE_1:59;
then ((q`1)^2+(q`2)^2)=(1+(q`2/q`1)^2) by A191,XCMPLX_1:88;
then (px`1)^2+(px`2)^2=1+(px`2)^2/(px`1)^2 by SQUARE_1:69;
then (px`1)^2+(px`2)^2-1=(px`2)^2/(px`1)^2 by XCMPLX_1:26;
then ((px`1)^2+(px`2)^2-1)*(px`1)^2=(px`2)^2 by A192,XCMPLX_1:88;
then ((px`1)^2+((px`2)^2-1))*(px`1)^2=(px`2)^2 by XCMPLX_1:29;
then (px`1)^2*(px`1)^2+((px`2)^2-1)*(px`1)^2=(px`2)^2 by XCMPLX_1:8;
then (px`1)^2*(px`1)^2+(px`1)^2*((px`2)^2-1)-(px`2)^2=0 by XCMPLX_1:14
;
then (px`1)^2*(px`1)^2+((px`1)^2*(px`2)^2-(px`1)^2*1)-(px`2)^2=0
by XCMPLX_1:40;
then (px`1)^2*(px`1)^2+(px`1)^2*(px`2)^2-(px`1)^2*1-(px`2)^2=0
by XCMPLX_1:29;
then (px`1)^2*(px`1)^2-(px`1)^2*1+(px`1)^2*(px`2)^2-(1)*(px`2)^2=0
by XCMPLX_1:29;
then (px`1)^2*((px`1)^2-1)+(px`1)^2*(px`2)^2-(1)*(px`2)^2=0
by XCMPLX_1:40;
then (px`1)^2*((px`1)^2-1)+((px`1)^2*(px`2)^2-(1)*(px`2)^2)=0
by XCMPLX_1:29;
hence
((px`1)^2-1)*(px`1)^2+((px`1)^2-1)*(px`2)^2=0 by XCMPLX_1:40;
end;
then A193:((px`1)^2-1)*((px`1)^2+(px`2)^2)=0 by XCMPLX_1:8;
((px`1)^2+(px`2)^2)<>0 by A184,COMPLEX1:2;
then ((px`1)^2-1)=0 by A193,XCMPLX_1:6;
then (px`1-1)*(px`1+1)=0 by SQUARE_1:59,67;
then px`1-1=0 or px`1+1=0 by XCMPLX_1:6;
then px`1=0+1 or px`1+1=0 by XCMPLX_1:27;
then A194: px`1=1 or px`1=0-1 by XCMPLX_1:26;
A195: (ff.I)=(Sq_Circ").(f.I) by A3,FUNCT_1:22;
consider p2 being Point of TOP-REAL 2 such that
A196: f.I=p2 &(
|.p2.|=1 & p2`2<=p2`1 & p2`2>=-p2`1) by A1;
A197:p2<>0.REAL 2 &
(p2`2<=p2`1 & -p2`1<=p2`2 or p2`2>=p2`1 & p2`2<=-p2`1)
by A196,TOPRNS_1:24;
then A198:Sq_Circ".p2=|[p2`1*sqrt(1+(p2`2/p2`1)^2),p2`2*sqrt(1+(p2`2/p2`1)
^2)]|
by JGRAPH_3:38;
reconsider py=ff.I as Point of TOP-REAL 2;
A199: py`1 = p2`1*sqrt(1+(p2`2/p2`1)^2) &
py`2 = p2`2*sqrt(1+(p2`2/p2`1)^2) by A195,A196,A198,EUCLID:56;
(p2`2/p2`1)^2 >=0 by SQUARE_1:72;
then 1+(p2`2/p2`1)^2>=1+0 by REAL_1:55;
then 1+(p2`2/p2`1)^2>0 by AXIOMS:22;
then A200:sqrt(1+(p2`2/p2`1)^2)>0 by SQUARE_1:93;
A201:now assume
A202: py`1=0 & py`2=0;
then A203:p2`1=0 by A199,A200,XCMPLX_1:6;
p2`2=0 by A199,A200,A202,XCMPLX_1:6;
hence contradiction by A197,A203,EUCLID:57,58;
end;
A204: now
p2`2<=p2`1 & (-p2`1)*sqrt(1+(p2`2/p2`1)^2) <= p2`2*sqrt(1+(p2`2/p2`1)^2)
or py`2>=py`1 & py`2<=-py`1 by A196,A200,AXIOMS:25;
hence
p2`2*sqrt(1+(p2`2/p2`1)^2) <= p2`1*sqrt(1+(p2`2/p2`1)^2) & -py`1<=py
`2
or py`2>=py`1 & py`2<=-py`1 by A199,A200,AXIOMS:25,XCMPLX_1:175;
end;
A205:p2=Sq_Circ.py by A195,A196,FUNCT_1:54,JGRAPH_3:32,54;
A206:Sq_Circ.py=|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|
by A199,A201,A204,JGRAPH_2:11,JGRAPH_3:def 1;
A207: (|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|)`1
= py`1/sqrt(1+(py`2/py`1)^2) &
(|[py`1/sqrt(1+(py`2/py`1)^2),py`2/sqrt(1+(py`2/py`1)^2)]|)`2
= py`2/sqrt(1+(py`2/py`1)^2) by EUCLID:56;
(py`2/py`1)^2 >=0 by SQUARE_1:72;
then 1+(py`2/py`1)^2>=1+0 by REAL_1:55;
then A208:1+(py`2/py`1)^2>0 by AXIOMS:22;
py`1<>0 by A199,A201,A204;
then A209: (py`1)^2<>0 by SQUARE_1:73;
now
(|.p2.|)^2= (py`1/sqrt(1+(py`2/py`1)^2))^2+(py`2/sqrt(1+(py`2/py`1)^2))^2
by A205,A206,A207,JGRAPH_3:10
.= (py`1)^2/(sqrt(1+(py`2/py`1)^2))^2+(py`2/sqrt(1+(py`2/py`1)^2))^2
by SQUARE_1:69
.= (py`1)^2/(sqrt(1+(py`2/py`1)^2))^2
+(py`2)^2/(sqrt(1+(py`2/py`1)^2))^2
by SQUARE_1:69
.= (py`1)^2/(1+(py`2/py`1)^2)+(py`2)^2/(sqrt(1+(py`2/py`1)^2))^2
by A208,SQUARE_1:def 4
.= (py`1)^2/(1+(py`2/py`1)^2)+(py`2)^2/(1+(py`2/py`1)^2)
by A208,SQUARE_1:def 4
.= ((py`1)^2+(py`2)^2)/(1+(py`2/py`1)^2)
by XCMPLX_1:63;
then ((py`1)^2+(py`2)^2)/(1+(py`2/py`1)^2)*(1+(py`2/py`1)^2)
=(1)*(1+(py`2/py`1)^2) by A196,SQUARE_1:59;
then ((py`1)^2+(py`2)^2)=(1+(py`2/py`1)^2)
by A208,XCMPLX_1:88;
then (py`1)^2+(py`2)^2=1+(py`2)^2/(py`1)^2 by SQUARE_1:69;
then (py`1)^2+(py`2)^2-1=(py`2)^2/(py`1)^2 by XCMPLX_1:26;
then ((py`1)^2+(py`2)^2-1)*(py`1)^2=(py`2)^2
by A209,XCMPLX_1:88;
then ((py`1)^2+((py`2)^2-1))*(py`1)^2=(py`2)^2 by XCMPLX_1:29;
then (py`1)^2*(py`1)^2+((py`2)^2-1)*(py`1)^2=(py`2)^2 by XCMPLX_1:8;
then (py`1)^2*(py`1)^2+(py`1)^2*((py`2)^2-1)-(py`2)^2=0 by XCMPLX_1:14
;
then (py`1)^2*(py`1)^2+((py`1)^2*(py`2)^2-(py`1)^2*1)-(py`2)^2=0
by XCMPLX_1:40;
then (py`1)^2*(py`1)^2+(py`1)^2*(py`2)^2-(py`1)^2*1-(py`2)^2=0
by XCMPLX_1:29;
then (py`1)^2*(py`1)^2-(py`1)^2*1+(py`1)^2*(py`2)^2-(1)*(py`2)^2=0
by XCMPLX_1:29;
then (py`1)^2*((py`1)^2-1)+(py`1)^2*(py`2)^2-(1)*(py`2)^2=0
by XCMPLX_1:40;
then (py`1)^2*((py`1)^2-1)+((py`1)^2*(py`2)^2-(1)*(py`2)^2)=0
by XCMPLX_1:29;
hence ((py`1)^2-1)*(py`1)^2+((py`1)^2-1)*(py`2)^2=0 by XCMPLX_1:40;
end;
then A210:((py`1)^2-1)*((py`1)^2+(py`2)^2)=0 by XCMPLX_1:8;
((py`1)^2+(py`2)^2)<>0 by A201,COMPLEX1:2;
then ((py`1)^2-1)=0 by A210,XCMPLX_1:6;
then (py`1-1)*(py`1+1)=0 by SQUARE_1:59,67;
then py`1-1=0 or py`1+1=0 by XCMPLX_1:6;
then py`1=0+1 or py`1+1=0 by XCMPLX_1:27;
then A211: py`1=1 or py`1=0-1 by XCMPLX_1:26;
A212: gg.O=(Sq_Circ").(g.O) by A4,FUNCT_1:22;
consider p3 being Point of TOP-REAL 2 such that
A213: g.O=p3 &( |.p3.|=1 & p3`2<=p3`1 & p3`2<=-p3`1) by A1;
A214: -p3`2>=--p3`1 by A213,REAL_1:50;
then A215:p3<>0.REAL 2 &
(p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 & p3`1<=-p3`2)
by A213,TOPRNS_1:24;
then A216:Sq_Circ".p3=|[p3`1*sqrt(1+(p3`1/p3`2)^2),p3`2*sqrt(1+(p3`1/p3`2)^2
)]|
by JGRAPH_3:40;
reconsider pz=gg.O as Point of TOP-REAL 2;
A217: pz`2 = p3`2*sqrt(1+(p3`1/p3`2)^2) &
pz`1 = p3`1*sqrt(1+(p3`1/p3`2)^2) by A212,A213,A216,EUCLID:56;
(p3`1/p3`2)^2 >=0 by SQUARE_1:72;
then 1+(p3`1/p3`2)^2>=1+0 by REAL_1:55;
then 1+(p3`1/p3`2)^2>0 by AXIOMS:22;
then A218:sqrt(1+(p3`1/p3`2)^2)>0 by SQUARE_1:93;
A219:now assume
A220: pz`2=0 & pz`1=0;
then A221:p3`2=0 by A217,A218,XCMPLX_1:6;
p3`1=0 by A217,A218,A220,XCMPLX_1:6;
hence contradiction by A215,A221,EUCLID:57,58;
end;
A222: now
p3`1<=p3`2 & -p3`2<=p3`1 or p3`1>=p3`2 &
p3`1*sqrt(1+(p3`1/p3`2)^2) <= (-p3`2)*sqrt(1+(p3`1/p3`2)^2)
by A213,A214,A218,AXIOMS:25;
then p3`1<=p3`2 & (-p3`2)*sqrt(1+(p3`1/p3`2)^2) <= p3`1*sqrt(1+(p3`1/p3`2
)^2)
or pz`1>=pz`2 & pz`1<=-pz`2 by A217,A218,AXIOMS:25,XCMPLX_1:175;
hence
p3`1*sqrt(1+(p3`1/p3`2)^2) <= p3`2*sqrt(1+(p3`1/p3`2)^2) & -pz`2<=pz`1
or pz`1>=pz`2 & pz`1<=-pz`2 by A217,A218,AXIOMS:25,XCMPLX_1:175;
end;
A223:p3=Sq_Circ.pz by A212,A213,FUNCT_1:54,JGRAPH_3:32,54;
A224:Sq_Circ.pz=|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|
by A217,A219,A222,JGRAPH_2:11,JGRAPH_3:14;
A225: (|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`2
= pz`2/sqrt(1+(pz`1/pz`2)^2) &
(|[pz`1/sqrt(1+(pz`1/pz`2)^2),pz`2/sqrt(1+(pz`1/pz`2)^2)]|)`1
= pz`1/sqrt(1+(pz`1/pz`2)^2) by EUCLID:56;
(pz`1/pz`2)^2 >=0 by SQUARE_1:72;
then 1+(pz`1/pz`2)^2>=1+0 by REAL_1:55;
then A226:1+(pz`1/pz`2)^2>0 by AXIOMS:22;
pz`2<>0 by A217,A219,A222;
then A227: (pz`2)^2<>0 by SQUARE_1:73;
A228:(|.p3.|)^2= (pz`2/sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by A223,A224,A225,JGRAPH_3:10
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2+(pz`1/sqrt(1+(pz`1/pz`2)^2))^2
by SQUARE_1:69
.= (pz`2)^2/(sqrt(1+(pz`1/pz`2)^2))^2
+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by SQUARE_1:69
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(sqrt(1+(pz`1/pz`2)^2))^2
by A226,SQUARE_1:def 4
.= (pz`2)^2/(1+(pz`1/pz`2)^2)+(pz`1)^2/(1+(pz`1/pz`2)^2)
by A226,SQUARE_1:def 4
.= ((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)
by XCMPLX_1:63;
now
((pz`2)^2+(pz`1)^2)/(1+(pz`1/pz`2)^2)*(1+(pz`1/pz`2)^2)=(1)*(1+(pz`1/pz`2)^2
)
by A213,A228,SQUARE_1:59;
then ((pz`2)^2+(pz`1)^2)=(1+(pz`1/pz`2)^2)
by A226,XCMPLX_1:88;
then (pz`2)^2+(pz`1)^2=1+(pz`1)^2/(pz`2)^2 by SQUARE_1:69;
then (pz`2)^2+(pz`1)^2-1=(pz`1)^2/(pz`2)^2 by XCMPLX_1:26;
then ((pz`2)^2+(pz`1)^2-1)*(pz`2)^2=(pz`1)^2
by A227,XCMPLX_1:88;
then ((pz`2)^2+((pz`1)^2-1))*(pz`2)^2=(pz`1)^2 by XCMPLX_1:29;
then (pz`2)^2*(pz`2)^2+((pz`1)^2-1)*(pz`2)^2=(pz`1)^2 by XCMPLX_1:8;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*((pz`1)^2-1)-(pz`1)^2=0 by XCMPLX_1:14
;
then (pz`2)^2*(pz`2)^2+((pz`2)^2*(pz`1)^2-(pz`2)^2*1)-(pz`1)^2=0
by XCMPLX_1:40;
then (pz`2)^2*(pz`2)^2+(pz`2)^2*(pz`1)^2-(pz`2)^2*1-(pz`1)^2=0
by XCMPLX_1:29;
then (pz`2)^2*(pz`2)^2-(pz`2)^2*1+(pz`2)^2*(pz`1)^2-(1)*(pz`1)^2=0
by XCMPLX_1:29;hence
(pz`2)^2*((pz`2)^2-1)+(pz`2)^2*(pz`1)^2-(1)*(pz`1)^2=0
by XCMPLX_1:40;
end;
then (pz`2)^2*((pz`2)^2-1)+((pz`2)^2*(pz`1)^2-(1)*(pz`1)^2)=0
by XCMPLX_1:29;
then (pz`2)^2*((pz`2)^2-1)+((pz`2)^2-1)*(pz`1)^2=0
by XCMPLX_1:40;
then A229:((pz`2)^2-1)*((pz`2)^2+(pz`1)^2)=0 by XCMPLX_1:8;
((pz`2)^2+(pz`1)^2)<>0 by A219,COMPLEX1:2;
then ((pz`2)^2-1)=0 by A229,XCMPLX_1:6;
then (pz`2-1)*(pz`2+1)=0 by SQUARE_1:59,67;
then pz`2-1=0 or pz`2+1=0 by XCMPLX_1:6;
then pz`2=0+1 or pz`2+1=0 by XCMPLX_1:27;
then A230: pz`2=1 or pz`2=0-1 by XCMPLX_1:26;
A231: (gg.I)=(Sq_Circ").(g.I) by A4,FUNCT_1:22;
consider p4 being Point of TOP-REAL 2 such that
A232: g.I=p4 &(
|.p4.|=1 & p4`2>=p4`1 & p4`2>=-p4`1) by A1;
A233: -p4`2<=--p4`1 by A232,REAL_1:50;
then A234:p4<>0.REAL 2 &
(p4`1<=p4`2 & -p4`2<=p4`1 or p4`1>=p4`2 & p4`1<=-p4`2)
by A232,TOPRNS_1:24;
then A235:Sq_Circ".p4=|[p4`1*sqrt(1+(p4`1/p4`2)^2),p4`2*sqrt(1+(p4`1/p4`2)
^2)]|
by JGRAPH_3:40;
reconsider pu=gg.I as Point of TOP-REAL 2;
A236: pu`2 = p4`2*sqrt(1+(p4`1/p4`2)^2) &
pu`1 = p4`1*sqrt(1+(p4`1/p4`2)^2) by A231,A232,A235,EUCLID:56;
(p4`1/p4`2)^2 >=0 by SQUARE_1:72;
then 1+(p4`1/p4`2)^2>=1+0 by REAL_1:55;
then 1+(p4`1/p4`2)^2>0 by AXIOMS:22;
then A237:sqrt(1+(p4`1/p4`2)^2)>0 by SQUARE_1:93;
A238:now assume
A239: pu`2=0 & pu`1=0;
then A240:p4`2=0 by A236,A237,XCMPLX_1:6;
p4`1=0 by A236,A237,A239,XCMPLX_1:6;
hence contradiction by A234,A240,EUCLID:57,58;
end;
A241: now
p4`1<=p4`2 & (-p4`2)*sqrt(1+(p4`1/p4`2)^2) <= p4`1*sqrt(1+(p4`1/p4`2)^2)
or pu`1>=pu`2 & pu`1<=-pu`2 by A232,A233,A237,AXIOMS:25;hence
p4`1*sqrt(1+(p4`1/p4`2)^2) <= p4`2*sqrt(1+(p4`1/p4`2)^2) & -pu`2<=pu`1
or pu`1>=pu`2 & pu`1<=-pu`2 by A236,A237,AXIOMS:25,XCMPLX_1:175;
end;
A242:p4=Sq_Circ.pu by A231,A232,FUNCT_1:54,JGRAPH_3:32,54;
A243:Sq_Circ.pu=|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|
by A236,A238,A241,JGRAPH_2:11,JGRAPH_3:14;
A244: (|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|)`2
= pu`2/sqrt(1+(pu`1/pu`2)^2) &
(|[pu`1/sqrt(1+(pu`1/pu`2)^2),pu`2/sqrt(1+(pu`1/pu`2)^2)]|)`1
= pu`1/sqrt(1+(pu`1/pu`2)^2) by EUCLID:56;
(pu`1/pu`2)^2 >=0 by SQUARE_1:72;
then 1+(pu`1/pu`2)^2>=1+0 by REAL_1:55;
then A245:1+(pu`1/pu`2)^2>0 by AXIOMS:22;
pu`2<>0 by A236,A238,A241;
then A246: (pu`2)^2<>0 by SQUARE_1:73;
now
(|.p4.|)^2= (pu`2/sqrt(1+(pu`1/pu`2)^2))^2+(pu`1/sqrt(1+(pu`1/pu`2)^2))^2
by A242,A243,A244,JGRAPH_3:10
.= (pu`2)^2/(sqrt(1+(pu`1/pu`2)^2))^2+(pu`1/sqrt(1+(pu`1/pu`2)^2))^2
by SQUARE_1:69
.= (pu`2)^2/(sqrt(1+(pu`1/pu`2)^2))^2
+(pu`1)^2/(sqrt(1+(pu`1/pu`2)^2))^2
by SQUARE_1:69
.= (pu`2)^2/(1+(pu`1/pu`2)^2)+(pu`1)^2/(sqrt(1+(pu`1/pu`2)^2))^2
by A245,SQUARE_1:def 4
.= (pu`2)^2/(1+(pu`1/pu`2)^2)+(pu`1)^2/(1+(pu`1/pu`2)^2)
by A245,SQUARE_1:def 4
.= ((pu`2)^2+(pu`1)^2)/(1+(pu`1/pu`2)^2) by XCMPLX_1:63;
then ((pu`2)^2+(pu`1)^2)/(1+(pu`1/pu`2)^2)*(1+(pu`1/pu`2)^2)=(1)*(1+(pu`1/pu
`2)^2)
by A232,SQUARE_1:59;
then ((pu`2)^2+(pu`1)^2)=(1+(pu`1/pu`2)^2) by A245,XCMPLX_1:88;
then (pu`2)^2+(pu`1)^2=1+(pu`1)^2/(pu`2)^2 by SQUARE_1:69;
then (pu`2)^2+(pu`1)^2-1=(pu`1)^2/(pu`2)^2 by XCMPLX_1:26;
then ((pu`2)^2+(pu`1)^2-1)*(pu`2)^2=(pu`1)^2 by A246,XCMPLX_1:88;
then ((pu`2)^2+((pu`1)^2-1))*(pu`2)^2=(pu`1)^2 by XCMPLX_1:29;
then (pu`2)^2*(pu`2)^2+((pu`1)^2-1)*(pu`2)^2=(pu`1)^2 by XCMPLX_1:8;
then (pu`2)^2*(pu`2)^2+(pu`2)^2*((pu`1)^2-1)-(pu`1)^2=0 by XCMPLX_1:14
;
then (pu`2)^2*(pu`2)^2+((pu`2)^2*(pu`1)^2-(pu`2)^2*1)-(pu`1)^2=0
by XCMPLX_1:40;
then (pu`2)^2*(pu`2)^2+(pu`2)^2*(pu`1)^2-(pu`2)^2*1-(pu`1)^2=0
by XCMPLX_1:29;
then (pu`2)^2*(pu`2)^2-(pu`2)^2*1+(pu`2)^2*(pu`1)^2-(1)*(pu`1)^2=0
by XCMPLX_1:29;
then (pu`2)^2*((pu`2)^2-1)+(pu`2)^2*(pu`1)^2-(1)*(pu`1)^2=0
by XCMPLX_1:40;
then (pu`2)^2*((pu`2)^2-1)+((pu`2)^2*(pu`1)^2-(1)*(pu`1)^2)=0
by XCMPLX_1:29;
hence ((pu`2)^2-1)*(pu`2)^2+((pu`2)^2-1)*(pu`1)^2=0 by XCMPLX_1:40;
end;
then A247:((pu`2)^2-1)*((pu`2)^2+(pu`1)^2)=0 by XCMPLX_1:8;
((pu`2)^2+(pu`1)^2)<>0 by A238,COMPLEX1:2;
then (pu`2)^2-1=0 by A247,XCMPLX_1:6;
then (pu`2-1)*(pu`2+1)=0 by SQUARE_1:59,67;
then pu`2-1=0 or pu`2+1=0 by XCMPLX_1:6;
then pu`2=0+1 or pu`2+1=0 by XCMPLX_1:27;
then A248: pu`2=1 or pu`2=0-1 by XCMPLX_1:26;
thus -1 <=(ff.O)`2 & (ff.O)`2 <= 1 by A187,A194,AXIOMS:22;
thus -1 <=(ff.I)`2 & (ff.I)`2 <= 1 by A199,A204,A211,AXIOMS:22;
thus -1 <=(gg.O)`1 & (gg.O)`1 <= 1 by A217,A222,A230,AXIOMS:22;
thus -1 <=(gg.I)`1 & (gg.I)`1 <= 1 by A236,A241,A248,AXIOMS:22;
end;
then rng ff meets rng gg by A1,A7,A9,A10,A11,A12,A99,Th14;
then consider y being set such that
A249: y in rng ff & y in rng gg by XBOOLE_0:3;
consider x1 being set such that
A250: x1 in dom ff & y=ff.x1 by A249,FUNCT_1:def 5;
consider x2 being set such that
A251: x2 in dom gg & y=gg.x2 by A249,FUNCT_1:def 5;
A252:ff.x1=Sq_Circ".(f.x1) by A250,FUNCT_1:22;
A253:dom (Sq_Circ")=the carrier of TOP-REAL 2
by FUNCT_2:def 1,JGRAPH_3:39;
x1 in dom f by A250,FUNCT_1:21;
then A254:f.x1 in rng f by FUNCT_1:def 5;
x2 in dom g by A251,FUNCT_1:21;
then A255:g.x2 in rng g by FUNCT_1:def 5;
A256: Sq_Circ" is one-to-one by FUNCT_1:62,JGRAPH_3:32;
gg.x2=Sq_Circ".(g.x2) by A251,FUNCT_1:22;
then f.x1=g.x2 by A250,A251,A252,A253,A254,A255,A256,FUNCT_1:def 8;
hence thesis by A254,A255,XBOOLE_0:3;
end;
theorem Th18: for f,g being map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN being Subset of TOP-REAL 2,
O,I being Point of I[01] st O=0 & I=1 &
f is continuous one-to-one &
g is continuous one-to-one &
C0={p: |.p.|>=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXN & f.I in KXP &
g.O in KYP & g.I in KYN &
rng f c= C0 & rng g c= C0
holds rng f meets rng g
proof let f,g be map of I[01],TOP-REAL 2,
C0,KXP,KXN,KYP,KYN be Subset of TOP-REAL 2,
O,I be Point of I[01];
assume A1: O=0 & I=1 &
f is continuous one-to-one & g is continuous one-to-one &
C0={p: |.p.|>=1}&
KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} &
KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} &
KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} &
KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} &
f.O in KXN & f.I in KXP &
g.O in KYP & g.I in KYN &
rng f c= C0 & rng g c= C0;
then consider g2 being map of I[01],TOP-REAL 2 such that
A2: g2.0=g.1 & g2.1=g.0 &
rng g2=rng g & g2 is continuous one-to-one by Th15;
thus rng f meets rng g by A1,A2,Th17;
end;
theorem Th19:
for f,g being map of I[01],TOP-REAL 2,
C0 being Subset of TOP-REAL 2
st C0={q: |.q.|>=1} &
f is continuous one-to-one &
g is continuous one-to-one &
f.0=|[-1,0]| & f.1=|[1,0]| & g.1=|[0,1]| & g.0=|[0,-1]|
& rng f c= C0 & rng g c= C0
holds rng f meets rng g
proof let f,g be map of I[01],TOP-REAL 2,
C0 be Subset of TOP-REAL 2;
assume A1: C0={q: |.q.|>=1} &
f is continuous one-to-one & g is continuous one-to-one &
f.0=|[-1,0]| & f.1=|[1,0]| & g.1=|[0,1]| & g.0=|[0,-1]|
& rng f c= C0 & rng g c= C0;
defpred P[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2<=$1`1 & $1`2>=-$1`1;
{q1 where q1 is Point of TOP-REAL 2:P[q1] } is Subset
of TOP-REAL 2 from TopSubset;
then reconsider KXP={q1 where q1 is Point of TOP-REAL 2:
|.q1.|=1 & q1`2<=q1`1 & q1`2>=-q1`1} as Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2>=$1`1 & $1`2<=-$1`1;
{q2 where q2 is Point of TOP-REAL 2: P[q2]}
is Subset of TOP-REAL 2 from TopSubset;
then reconsider KXN={q2 where q2 is Point of TOP-REAL 2:
|.q2.|=1 & q2`2>=q2`1 & q2`2<=-q2`1} as Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2>=$1`1 & $1`2>=-$1`1;
{q3 where q3 is Point of TOP-REAL 2:P[q3]}
is Subset of TOP-REAL 2 from TopSubset;
then reconsider KYP={q3 where q3 is Point of TOP-REAL 2:
|.q3.|=1 & q3`2>=q3`1 & q3`2>=-q3`1} as Subset of TOP-REAL 2;
defpred P[Point of TOP-REAL 2] means
|.$1.|=1 & $1`2<=$1`1 & $1`2<=-$1`1;
{q4 where q4 is Point of TOP-REAL 2:P[q4]}
is Subset of TOP-REAL 2 from TopSubset;
then reconsider KYN={q4 where q4 is Point of TOP-REAL 2:
|.q4.|=1 & q4`2<=q4`1 & q4`2<=-q4`1} as Subset of TOP-REAL 2;
reconsider O=0 as Point of I[01] by BORSUK_1:83,RCOMP_1:15;
reconsider I=1 as Point of I[01] by BORSUK_1:83,RCOMP_1:15;
A2: (|[-1,0]|)`1=-1 & (|[-1,0]|)`2=0 by EUCLID:56;
then A3: |. (|[-1,0]|).|=sqrt((-1)^2+0^2) by JGRAPH_3:10
.=1 by SQUARE_1:59,60,61,83;
(|[-1,0]|)`2 <=-((|[-1,0]|)`1) by A2;
then A4: f.O in KXN by A1,A2,A3;
A5: (|[1,0]|)`1=1 & (|[1,0]|)`2=0 by EUCLID:56;
then |.(|[1,0]|).|=sqrt(1^2+0) by JGRAPH_3:10,SQUARE_1:60
.=1 by SQUARE_1:59,83;
then A6: f.I in KXP by A1,A5;
A7: (|[0,-1]|)`2=-1 & (|[0,-1]|)`1=0 by EUCLID:56;
then A8: |.(|[0,-1]|).|=sqrt(0^2+(-1)^2) by JGRAPH_3:10
.=1 by SQUARE_1:59,60,61,83;
(|[0,-1]|)`2 <=-((|[0,-1]|)`1) by A7;
then A9: g.O in KYN by A1,A7,A8;
A10: (|[0,1]|)`2=1 & (|[0,1]|)`1=0 by EUCLID:56;
then A11: |. (|[0,1]|).|=sqrt(0+1^2) by JGRAPH_3:10,SQUARE_1:60
.=1 by SQUARE_1:59,83;
(|[0,1]|)`2 >=-((|[0,1]|)`1) by A10;
then g.I in KYP by A1,A10,A11;
hence rng f meets rng g by A1,A4,A6,A9,Th17;
end;
theorem for p1,p2,p3,p4 being Point of TOP-REAL 2,
C0 being Subset of TOP-REAL 2
st C0={p: |.p.|>=1}
& |.p1.|=1 & |.p2.|=1 & |.p3.|=1 & |.p4.|=1 &
(ex h being map of TOP-REAL 2,TOP-REAL 2 st h is_homeomorphism
& h.:C0 c= C0 &
h.p1=|[-1,0]| & h.p2=|[0,1]| & h.p3=|[1,0]| & h.p4=|[0,-1]|)
holds
(for f,g being map of I[01],TOP-REAL 2 st
f is continuous one-to-one &
g is continuous one-to-one &
f.0=p1 & f.1=p3 & g.0=p4 & g.1=p2 &
rng f c= C0 & rng g c= C0
holds rng f meets rng g)
proof let p1,p2,p3,p4 be Point of TOP-REAL 2,
C0 be Subset of TOP-REAL 2;
assume A1: C0={p: |.p.|>=1}
& |.p1.|=1 & |.p2.|=1 & |.p3.|=1 & |.p4.|=1 &
(ex h being map of TOP-REAL 2,TOP-REAL 2 st h is_homeomorphism
& h.:C0 c= C0 &
h.p1=(|[-1,0]|) & h.p2=(|[0,1]|) & h.p3=(|[1,0]|) & h.p4=(|[0,-1]|));
then consider h being map of TOP-REAL 2,TOP-REAL 2 such that
A2: h is_homeomorphism
& h.:C0 c= C0 &
h.p1=(|[-1,0]|) & h.p2=(|[0,1]|) & h.p3=(|[1,0]|) & h.p4=(|[0,-1]|);
let f,g be map of I[01],TOP-REAL 2;
assume A3: f is continuous one-to-one &
g is continuous one-to-one &
f.0=p1 & f.1=p3 & g.0=p4 & g.1=p2 &
rng f c= C0 & rng g c= C0;
reconsider f2=h*f as map of I[01],TOP-REAL 2;
reconsider g2=h*g as map of I[01],TOP-REAL 2;
A4: h is continuous by A2,TOPS_2:def 5;
then A5: f2 is continuous by A3,TOPS_2:58;
A6: g2 is continuous by A3,A4,TOPS_2:58;
A7: h is one-to-one by A2,TOPS_2:def 5;
then A8: f2 is one-to-one by A3,FUNCT_1:46;
A9: g2 is one-to-one by A3,A7,FUNCT_1:46;
A10: 0 in dom f2 &1 in dom f2 by Lm1,BORSUK_1:83,FUNCT_2:def 1;
then A11: f2.0=|[-1,0]| by A2,A3,FUNCT_1:22;
A12: f2.1=|[1,0]| by A2,A3,A10,FUNCT_1:22;
A13: 0 in dom g2 &1 in dom g2 by Lm1,BORSUK_1:83,FUNCT_2:def 1;
then A14: g2.0=|[0,-1]| by A2,A3,FUNCT_1:22;
A15: g2.1=|[0,1]| by A2,A3,A13,FUNCT_1:22;
A16: rng f2 c= C0
proof let y be set;assume y in rng f2;
then consider x being set such that
A17: x in dom f2 & y=f2.x by FUNCT_1:def 5;
A18: y=h.(f.x) by A17,FUNCT_1:22;
x in dom f by A17,FUNCT_1:21;
then A19: f.x in rng f by FUNCT_1:def 5;
dom h=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then y in h.:C0 by A3,A18,A19,FUNCT_1:def 12;
hence y in C0 by A2;
end;
rng g2 c= C0
proof let y be set;assume y in rng g2;
then consider x being set such that
A20: x in dom g2 & y=g2.x by FUNCT_1:def 5;
A21: y=h.(g.x) by A20,FUNCT_1:22;
x in dom g by A20,FUNCT_1:21;
then A22: g.x in rng g by FUNCT_1:def 5;
dom h=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then y in h.:C0 by A3,A21,A22,FUNCT_1:def 12;
hence y in C0 by A2;
end;
then rng f2 meets rng g2 by A1,A5,A6,A8,A9,A11,A12,A14,A15,A16,Th19;
then consider q5 being set such that
A23: q5 in rng f2 & q5 in rng g2 by XBOOLE_0:3;
consider x being set such that
A24: x in dom f2 & q5=f2.x by A23,FUNCT_1:def 5;
A25: q5=h.(f.x) by A24,FUNCT_1:22;
consider u being set such that
A26: u in dom g2 & q5=g2.u by A23,FUNCT_1:def 5;
A27: q5=h.(g.u) by A26,FUNCT_1:22;
A28: h is one-to-one by A2,TOPS_2:def 5;
A29: f.x in dom h by A24,FUNCT_1:21;
g.u in dom h by A26,FUNCT_1:21;
then A30: f.x=g.u by A25,A27,A28,A29,FUNCT_1:def 8;
A31: x in dom f by A24,FUNCT_1:21;
A32: u in dom g by A26,FUNCT_1:21;
A33: f.x in rng f by A31,FUNCT_1:def 5;
g.u in rng g by A32,FUNCT_1:def 5;
hence thesis by A30,A33,XBOOLE_0:3;
end;
begin :: Properties of Fan Morphisms
theorem Th21:
for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>0
holds (for p being Point of TOP-REAL 2 st p=(cn-FanMorphN).q holds p`2>0)
proof let cn be Real,q be Point of TOP-REAL 2;
assume A1: -1<cn & cn<1 & q`2>0;
now per cases;
case q`1/|.q.|>=cn;
hence (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphN).q holds p`2>0) by A1,JGRAPH_4:82;
case q`1/|.q.|<cn;
hence (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphN).q holds p`2>0) by A1,JGRAPH_4:83;
end;
hence thesis;
end;
theorem
for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>=0
holds (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphN).q holds p`2>=0)
proof let cn be Real,q be Point of TOP-REAL 2;
assume A1: -1<cn & cn<1 & q`2>=0;
now per cases by A1;
case q`2>0;
hence (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphN).q holds p`2>=0) by A1,Th21;
case q`2=0;
hence (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphN).q holds p`2>=0) by JGRAPH_4:56;
end;
hence thesis;
end;
theorem Th23:
for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2>=0
& q`1/|.q.|<cn & |.q.|<>0 holds (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphN).q holds p`2>=0 & p`1<0)
proof let cn be Real,q be Point of TOP-REAL 2;
assume A1: -1<cn & cn<1 & q`2>=0
& q`1/|.q.|<cn & |.q.|<>0;
let p be Point of TOP-REAL 2;
assume A2: p=(cn-FanMorphN).q;
now per cases;
case A3: q`2=0;
then A4: q=p by A2,JGRAPH_4:56;
|.q.|^2=(q`1)^2+0 by A3,JGRAPH_3:10,SQUARE_1:60 .=(q`1)^2;
then |.q.|=q`1 or |.q.|=-(q`1) by JGRAPH_3:1;
then (-(q`1))/|.q.|=1 by A1,XCMPLX_1:60;
then -(q`1/|.q.|)=1 by XCMPLX_1:188;
then A5: q`1=(-1)*|.q.| by A1,XCMPLX_1:88;
|.q.|>=0 by TOPRNS_1:26;
hence p`2>=0 & p`1<0 by A1,A4,A5,SQUARE_1:24;
case q`2<>0;
hence p`2>=0 & p`1<0 by A1,A2,JGRAPH_4:83;
end;
hence p`2>=0 & p`1<0;
end;
theorem Th24:
for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2>=0
& q2`2>=0 & |.q1.|<>0 & |.q2.|<>0 & q1`1/|.q1.|<q2`1/|.q2.|
holds (for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2 holds p1`1/|.p1.|<p2`1/|.p2.|)
proof let cn be Real,q1,q2 be Point of TOP-REAL 2;
assume A1: -1<cn & cn<1 & q1`2>=0 & q2`2>=0 & |.q1.|<>0 & |.q2.|<>0
& q1`1/|.q1.|<q2`1/|.q2.|;
now per cases by A1;
case A2: q1`2>0;
now per cases by A1;
case q2`2>0;
hence (for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2 holds
p1`1/|.p1.|<p2`1/|.p2.|) by A1,A2,JGRAPH_4:86;
case A3: q2`2=0;
then |.q2.|^2=(q2`1)^2+0 by JGRAPH_3:10,SQUARE_1:60 .=(q2`1)^2;
then A4: |.q2.|=q2`1 or |.q2.|=-(q2`1) by JGRAPH_3:1;
now assume |.q2.|=-(q2`1);
then 1=(-(q2`1))/|.q2.| by A1,XCMPLX_1:60;
then A5: q1`1/|.q1.|< -1 by A1,XCMPLX_1:191;
A6: |.q1.|>=0 by TOPRNS_1:26;
(|.q1.|)^2=(q1`1)^2+(q1`2)^2 by JGRAPH_3:10;
then (|.q1.|)^2-(q1`1)^2=(q1`2)^2 by XCMPLX_1:26;
then (|.q1.|)^2-(q1`1)^2>=0 by SQUARE_1:72;
then (|.q1.|)^2-(q1`1)^2+(q1`1)^2>=0+(q1`1)^2 by REAL_1:55;
then (|.q1.|)^2>=(q1`1)^2 by XCMPLX_1:27;
then -|.q1.|<=q1`1 & q1`1<=|.q1.| by A6,JGRAPH_2:5;
then (-|.q1.|)/|.q1.|<=q1`1/|.q1.| by A1,A6,REAL_1:73;
hence contradiction by A1,A5,XCMPLX_1:198;
end;
then A7: q2`1/|.q2.|=1 by A1,A4,XCMPLX_1:60;
thus for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2 holds
p1`1/|.p1.|<p2`1/|.p2.|
proof let p1,p2 be Point of TOP-REAL 2;
assume A8: p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2;
then A9: p2=q2 by A3,JGRAPH_4:56;
A10: |.p1.|=|.q1.| by A8,JGRAPH_4:73;
A11: |.p1.|>=0 by TOPRNS_1:26;
(|.p1.|)^2=(p1`1)^2+(p1`2)^2 by JGRAPH_3:10;
then A12: (|.p1.|)^2-(p1`1)^2=(p1`2)^2 by XCMPLX_1:26;
then (|.p1.|)^2-(p1`1)^2>=0 by SQUARE_1:72;
then (|.p1.|)^2-(p1`1)^2+(p1`1)^2>=0+(p1`1)^2 by REAL_1:55;
then (|.p1.|)^2>=(p1`1)^2 by XCMPLX_1:27;
then -|.p1.|<=p1`1 & p1`1<=|.p1.| by A11,JGRAPH_2:5;
then (|.p1.|)/|.p1.|>=p1`1/|.p1.| by A1,A10,A11,REAL_1:73;
then A13: 1>= p1`1/|.p1.| by A1,A10,XCMPLX_1:60;
A14: p1`2>0 by A1,A2,A8,Th21;
now assume 1= p1`1/|.p1.|; then (1)*|.p1.|=p1`1 by A1,A10,XCMPLX_1:
88
;
then (|.p1.|)^2-(p1`1)^2=0 by XCMPLX_1:14;
hence contradiction by A12,A14,SQUARE_1:73;
end;
hence p1`1/|.p1.|<p2`1/|.p2.| by A7,A9,A13,REAL_1:def 5;
end;
end;
hence (for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2 holds
p1`1/|.p1.|<p2`1/|.p2.|);
case A15: q1`2=0;
then |.q1.|^2=(q1`1)^2+0 by JGRAPH_3:10,SQUARE_1:60 .=(q1`1)^2;
then A16: |.q1.|=q1`1 or |.q1.|=-(q1`1) by JGRAPH_3:1;
now assume |.q1.|=(q1`1);
then A17: q2`1/|.q2.|> 1 by A1,XCMPLX_1:60;
A18: |.q2.|>=0 by TOPRNS_1:26;
(|.q2.|)^2=(q2`1)^2+(q2`2)^2 by JGRAPH_3:10;
then (|.q2.|)^2-(q2`1)^2=(q2`2)^2 by XCMPLX_1:26;
then (|.q2.|)^2-(q2`1)^2>=0 by SQUARE_1:72;
then (|.q2.|)^2-(q2`1)^2+(q2`1)^2>=0+(q2`1)^2 by REAL_1:55;
then (|.q2.|)^2>=(q2`1)^2 by XCMPLX_1:27;
then -|.q2.|<=q2`1 & q2`1<=|.q2.| by A18,JGRAPH_2:5;
then (|.q2.|)/|.q2.|>=q2`1/|.q2.| by A1,A18,REAL_1:73;
hence contradiction by A1,A17,XCMPLX_1:60;
end;
then (-(q1`1))/|.q1.|=1 by A1,A16,XCMPLX_1:60;
then A19: -(q1`1/|.q1.|)=1 by XCMPLX_1:188;
thus (for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2
holds p1`1/|.p1.|<p2`1/|.p2.|)
proof let p1,p2 be Point of TOP-REAL 2;
assume A20: p1=(cn-FanMorphN).q1 & p2=(cn-FanMorphN).q2;
then A21: p1=q1 by A15,JGRAPH_4:56;
A22: |.p2.|=|.q2.| by A20,JGRAPH_4:73;
A23: |.p2.|>=0 by TOPRNS_1:26;
(|.p2.|)^2=(p2`1)^2+(p2`2)^2 by JGRAPH_3:10;
then A24: (|.p2.|)^2-(p2`1)^2=(p2`2)^2 by XCMPLX_1:26;
then (|.p2.|)^2-(p2`1)^2>=0 by SQUARE_1:72;
then (|.p2.|)^2-(p2`1)^2+(p2`1)^2>=0+(p2`1)^2 by REAL_1:55;
then (|.p2.|)^2>=(p2`1)^2 by XCMPLX_1:27;
then -|.p2.|<=p2`1 & p2`1<=|.p2.| by A23,JGRAPH_2:5;
then (-|.p2.|)/|.p2.|<=p2`1/|.p2.| by A1,A22,A23,REAL_1:73;
then A25: -1 <= p2`1/|.p2.| by A1,A22,XCMPLX_1:198;
now per cases;
case q2`2=0;
then p2=q2 by A20,JGRAPH_4:56;
hence p2`1/|.p2.|>-1 by A1,A19;
case q2`2<>0;
then A26: p2`2>0 by A1,A20,Th21;
now assume -1= p2`1/|.p2.|; then (-1)*|.p2.|=p2`1 by A1,A22,XCMPLX_1
:88;
then (-|.p2.|)^2=(p2`1)^2 by XCMPLX_1:180;
then (|.p2.|)^2=(p2`1)^2 by SQUARE_1:61;
then (|.p2.|)^2-(p2`1)^2=0 by XCMPLX_1:14;
hence contradiction by A24,A26,SQUARE_1:73;
end;
hence p2`1/|.p2.|>-1 by A25,REAL_1:def 5;
end;
hence p1`1/|.p1.|<p2`1/|.p2.| by A19,A21;
end;
end;
hence thesis;
end;
theorem Th25:
for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1>0
holds (for p being Point of TOP-REAL 2 st p=(sn-FanMorphE).q holds p`1>0)
proof let sn be Real,q be Point of TOP-REAL 2;
assume A1: -1<sn & sn<1 & q`1>0;
now per cases;
case q`2/|.q.|>=sn;
hence (for p being Point of TOP-REAL 2 st
p=(sn-FanMorphE).q holds p`1>0) by A1,JGRAPH_4:113;
case q`2/|.q.|<sn;
hence (for p being Point of TOP-REAL 2 st
p=(sn-FanMorphE).q holds p`1>0) by A1,JGRAPH_4:114;
end;
hence thesis;
end;
theorem
for sn being Real,q being Point of TOP-REAL 2 st -1<sn & sn<1 & q`1>=0
& q`2/|.q.|<sn & |.q.|<>0 holds (for p being Point of TOP-REAL 2 st
p=(sn-FanMorphE).q holds p`1>=0 & p`2<0)
proof let sn be Real,q be Point of TOP-REAL 2;
assume A1: -1<sn & sn<1 & q`1>=0 & q`2/|.q.|<sn & |.q.|<>0;
let p be Point of TOP-REAL 2;
assume A2: p=(sn-FanMorphE).q;
now per cases;
case A3: q`1=0;
then A4: q=p by A2,JGRAPH_4:89;
|.q.|^2=(q`2)^2+0 by A3,JGRAPH_3:10,SQUARE_1:60 .=(q`2)^2;
then |.q.|=q`2 or |.q.|=-(q`2) by JGRAPH_3:1;
then (-(q`2))/|.q.|=1 by A1,XCMPLX_1:60;
then -(q`2/|.q.|)=1 by XCMPLX_1:188;
then A5: q`2=(-1)*|.q.| by A1,XCMPLX_1:88;
|.q.|>=0 by TOPRNS_1:26;
hence p`1>=0 & p`2<0 by A1,A4,A5,SQUARE_1:24;
case q`1<>0;
hence p`1>=0 & p`2<0 by A1,A2,JGRAPH_4:114;
end;
hence p`1>=0 & p`2<0;
end;
theorem Th27:
for sn being Real,q1,q2 being Point of TOP-REAL 2 st -1<sn & sn<1 & q1`1>=0
& q2`1>=0 & |.q1.|<>0 & |.q2.|<>0 & q1`2/|.q1.|<q2`2/|.q2.|
holds (for p1,p2 being Point of TOP-REAL 2 st
p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2 holds p1`2/|.p1.|<p2`2/|.p2.|)
proof let sn be Real,q1,q2 be Point of TOP-REAL 2;
assume A1: -1<sn & sn<1 & q1`1>=0 & q2`1>=0 & |.q1.|<>0 & |.q2.|<>0
& q1`2/|.q1.|<q2`2/|.q2.|;
now per cases by A1;
case A2: q1`1>0;
now per cases by A1;
case q2`1>0;
hence (for p1,p2 being Point of TOP-REAL 2 st
p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2 holds
p1`2/|.p1.|<p2`2/|.p2.|) by A1,A2,JGRAPH_4:117;
case A3: q2`1=0;
then |.q2.|^2=(q2`2)^2+0 by JGRAPH_3:10,SQUARE_1:60 .=(q2`2)^2;
then A4: |.q2.|=q2`2 or |.q2.|=-(q2`2) by JGRAPH_3:1;
now assume |.q2.|=-(q2`2);
then 1=(-(q2`2))/|.q2.| by A1,XCMPLX_1:60;
then A5: q1`2/|.q1.|< -1 by A1,XCMPLX_1:191;
A6: |.q1.|>=0 by TOPRNS_1:26;
(|.q1.|)^2=(q1`2)^2+(q1`1)^2 by JGRAPH_3:10;
then (|.q1.|)^2-(q1`2)^2=(q1`1)^2 by XCMPLX_1:26;
then (|.q1.|)^2-(q1`2)^2>=0 by SQUARE_1:72;
then (|.q1.|)^2-(q1`2)^2+(q1`2)^2>=0+(q1`2)^2 by REAL_1:55;
then (|.q1.|)^2>=(q1`2)^2 by XCMPLX_1:27;
then -|.q1.|<=q1`2 & q1`2<=|.q1.| by A6,JGRAPH_2:5;
then (-|.q1.|)/|.q1.|<=q1`2/|.q1.| by A1,A6,REAL_1:73;
hence contradiction by A1,A5,XCMPLX_1:198;
end;
then A7: q2`2/|.q2.|=1 by A1,A4,XCMPLX_1:60;
thus for p1,p2 being Point of TOP-REAL 2 st
p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2 holds
p1`2/|.p1.|<p2`2/|.p2.|
proof let p1,p2 be Point of TOP-REAL 2;
assume A8: p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2;
then A9: p2=q2 by A3,JGRAPH_4:89;
A10: |.p1.|=|.q1.| by A8,JGRAPH_4:104;
A11: |.p1.|>=0 by TOPRNS_1:26;
(|.p1.|)^2=(p1`2)^2+(p1`1)^2 by JGRAPH_3:10;
then A12: (|.p1.|)^2-(p1`2)^2=(p1`1)^2 by XCMPLX_1:26;
then (|.p1.|)^2-(p1`2)^2>=0 by SQUARE_1:72;
then (|.p1.|)^2-(p1`2)^2+(p1`2)^2>=0+(p1`2)^2 by REAL_1:55;
then (|.p1.|)^2>=(p1`2)^2 by XCMPLX_1:27;
then -|.p1.|<=p1`2 & p1`2<=|.p1.| by A11,JGRAPH_2:5;
then (|.p1.|)/|.p1.|>=p1`2/|.p1.| by A1,A10,A11,REAL_1:73;
then A13: 1>= p1`2/|.p1.| by A1,A10,XCMPLX_1:60;
A14: p1`1>0 by A1,A2,A8,Th25;
now assume 1= p1`2/|.p1.|; then (1)*|.p1.|=p1`2 by A1,A10,XCMPLX_1:
88
;
then (|.p1.|)^2-(p1`2)^2=0 by XCMPLX_1:14;
hence contradiction by A12,A14,SQUARE_1:73;
end;
hence p1`2/|.p1.|<p2`2/|.p2.| by A7,A9,A13,REAL_1:def 5;
end;
end;
hence (for p1,p2 being Point of TOP-REAL 2 st
p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2 holds
p1`2/|.p1.|<p2`2/|.p2.|);
case A15: q1`1=0;
then |.q1.|^2=(q1`2)^2+0 by JGRAPH_3:10,SQUARE_1:60 .=(q1`2)^2;
then A16: |.q1.|=q1`2 or |.q1.|=-(q1`2) by JGRAPH_3:1;
now assume |.q1.|=(q1`2);
then A17: q2`2/|.q2.|> 1 by A1,XCMPLX_1:60;
A18: |.q2.|>=0 by TOPRNS_1:26;
(|.q2.|)^2=(q2`2)^2+(q2`1)^2 by JGRAPH_3:10;
then (|.q2.|)^2-(q2`2)^2=(q2`1)^2 by XCMPLX_1:26;
then (|.q2.|)^2-(q2`2)^2>=0 by SQUARE_1:72;
then (|.q2.|)^2-(q2`2)^2+(q2`2)^2>=0+(q2`2)^2 by REAL_1:55;
then (|.q2.|)^2>=(q2`2)^2 by XCMPLX_1:27;
then -|.q2.|<=q2`2 & q2`2<=|.q2.| by A18,JGRAPH_2:5;
then (|.q2.|)/|.q2.|>=q2`2/|.q2.| by A1,A18,REAL_1:73;
hence contradiction by A1,A17,XCMPLX_1:60;
end;
then (-(q1`2))/|.q1.|=1 by A1,A16,XCMPLX_1:60;
then A19: -(q1`2/|.q1.|)=1 by XCMPLX_1:188;
thus (for p1,p2 being Point of TOP-REAL 2 st
p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2
holds p1`2/|.p1.|<p2`2/|.p2.|)
proof let p1,p2 be Point of TOP-REAL 2;
assume A20: p1=(sn-FanMorphE).q1 & p2=(sn-FanMorphE).q2;
then A21: p1=q1 by A15,JGRAPH_4:89;
A22: |.p2.|=|.q2.| by A20,JGRAPH_4:104;
A23: |.p2.|>=0 by TOPRNS_1:26;
(|.p2.|)^2=(p2`2)^2+(p2`1)^2 by JGRAPH_3:10;
then A24: (|.p2.|)^2-(p2`2)^2=(p2`1)^2 by XCMPLX_1:26;
then (|.p2.|)^2-(p2`2)^2>=0 by SQUARE_1:72;
then (|.p2.|)^2-(p2`2)^2+(p2`2)^2>=0+(p2`2)^2 by REAL_1:55;
then (|.p2.|)^2>=(p2`2)^2 by XCMPLX_1:27;
then -|.p2.|<=p2`2 & p2`2<=|.p2.| by A23,JGRAPH_2:5;
then (-|.p2.|)/|.p2.|<=p2`2/|.p2.| by A1,A22,A23,REAL_1:73;
then A25: -1 <= p2`2/|.p2.| by A1,A22,XCMPLX_1:198;
now per cases;
case q2`1=0;
then p2=q2 by A20,JGRAPH_4:89;
hence p2`2/|.p2.|>-1 by A1,A19;
case q2`1<>0;
then A26: p2`1>0 by A1,A20,Th25;
now assume -1= p2`2/|.p2.|; then (-1)*|.p2.|=p2`2 by A1,A22,XCMPLX_1
:88;
then (-|.p2.|)^2=(p2`2)^2 by XCMPLX_1:180;
then (|.p2.|)^2=(p2`2)^2 by SQUARE_1:61;
then (|.p2.|)^2-(p2`2)^2=0 by XCMPLX_1:14;
hence contradiction by A24,A26,SQUARE_1:73;
end;
hence
p2`2/|.p2.|>-1 by A25,REAL_1:def 5;
end;
hence p1`2/|.p1.|<p2`2/|.p2.| by A19,A21;
end;
end;
hence thesis;
end;
theorem Th28:
for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2<0
holds (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphS).q holds p`2<0)
proof let cn be Real,q be Point of TOP-REAL 2;
assume A1: -1<cn & cn<1 & q`2<0;
now per cases;
case q`1/|.q.|>=cn;
hence (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphS).q holds p`2<0) by A1,JGRAPH_4:144;
case q`1/|.q.|<cn;
hence (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphS).q holds p`2<0) by A1,JGRAPH_4:145;
end;
hence thesis;
end;
theorem Th29:
for cn being Real,q being Point of TOP-REAL 2 st -1<cn & cn<1 & q`2<0
& q`1/|.q.|>cn holds (for p being Point of TOP-REAL 2 st
p=(cn-FanMorphS).q holds p`2<0 & p`1>0)
proof let cn be Real,q be Point of TOP-REAL 2;
assume A1: -1<cn & cn<1 & q`2<0 & q`1/|.q.|>cn;
let p be Point of TOP-REAL 2;
assume A2: p=(cn-FanMorphS).q;
then A3: p`2<0 & p`1>=0 by A1,JGRAPH_4:144;
now assume A4: p`1=0;
then (|.p.|)^2=(p`2)^2+0 by JGRAPH_3:10,SQUARE_1:60 .=(p`2)^2;
then A5: p`2=|.p.| or p`2= - |.p.| by JGRAPH_3:1;
then A6: |.p.| <> 0 by A1,A2,JGRAPH_4:144;
set p1=(1/|.p.|)*p;
A7: |.p.|*p1=(|.p.|*(1/|.p.|))*p by EUCLID:34
.=(1)*p by A6,XCMPLX_1:107 .=p by EUCLID:33;
A8: p1=|[(1/|.p.|)*p`1,(1/|.p.|)*p`2]| by EUCLID:61;
then p1`2=(-|.p.|)*(1/|.p.|) by A3,A5,EUCLID:56,TOPRNS_1:26 .=-(|.p.|*(1/
|.p.|)) by XCMPLX_1:175
.=-1 by A6,XCMPLX_1:107;
then A9: p=|.p.|*(|[0,-1]|) by A4,A7,A8,EUCLID:56;
set q1=(|.p.|)*|[cn,-sqrt(1-cn^2)]|;
A10:(|[cn,-sqrt(1-cn^2)]|)`1=cn by EUCLID:56;
A11:(|[cn,-sqrt(1-cn^2)]|)`2=-sqrt(1-cn^2) by EUCLID:56;
then A12: q1=|[|.p.|*cn,|.p.|*(-sqrt(1-cn^2))]| by A10,EUCLID:61;
then A13: q1`1=(|.p.|)*cn by EUCLID:56;
A14: q1`2= (-sqrt(1-cn^2))*(|.p.|) by A12,EUCLID:56
.=-(sqrt(1-cn^2)*(|.p.|)) by XCMPLX_1:175;
A15: |.p.|>=0 by TOPRNS_1:26;
1^2>cn^2 by A1,JGRAPH_2:8;
then A16: 1-cn^2>0 by SQUARE_1:11,59;
then sqrt(1-cn^2)>0 by SQUARE_1:93;
then --sqrt(1-cn^2)*(|.p.|)>0 by A6,A15,SQUARE_1:21;
then A17: q1`2<0 by A14,REAL_1:66;
A18: |.q1.|=abs(|.p.|)*|.(|[cn,-sqrt(1-cn^2)]|).|
by TOPRNS_1:8
.=abs(|.p.|)*sqrt((cn)^2+(-sqrt(1-cn^2))^2)
by A10,A11,JGRAPH_3:10
.=abs(|.p.|)*sqrt(cn^2+(sqrt(1-cn^2))^2) by SQUARE_1:61
.=abs(|.p.|)*sqrt(cn^2+(1-cn^2)) by A16,SQUARE_1:def 4
.=abs(|.p.|)*1 by SQUARE_1:83,XCMPLX_1:27
.=|.p.| by A15,ABSVALUE:def 1;
then A19: q1`1/|.q1.|=cn by A6,A13,XCMPLX_1:90;
set p2=(cn-FanMorphS).q1;
A20: p2`2<0 & p2`1=0 by A1,A17,A19,JGRAPH_4:149;
then (|.p2.|)^2=(p2`2)^2+0 by JGRAPH_3:10,SQUARE_1:60 .=(p2`2)^2;
then A21: p2`2=|.p2.| or p2`2= - |.p2.| by JGRAPH_3:1;
|.p2.|=|.p.| by A18,JGRAPH_4:135;
then A22: p2=|[0,-(|.p.|)]| by A20,A21,EUCLID:57,TOPRNS_1:26;
(|[0,-1]|)`1=0 & (|[0,-1]|)`2=-1 by EUCLID:56;
then A23: |.p.|*(|[0,-1]|)=|[|.p.|*0,|.p.|*(-1)]| by EUCLID:61
.=|[0,-(|.p.|)]| by XCMPLX_1:180;
A24: (cn-FanMorphS) is one-to-one by A1,JGRAPH_4:140;
dom (cn-FanMorphS)=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
then q1=q by A2,A9,A22,A23,A24,FUNCT_1:def 8;
hence contradiction by A1,A6,A13,A18,XCMPLX_1:90;
end;
hence p`2<0 & p`1>0 by A1,A2,JGRAPH_4:144;
end;
theorem Th30:
for cn being Real,q1,q2 being Point of TOP-REAL 2 st -1<cn & cn<1 & q1`2<=0
& q2`2<=0 & |.q1.|<>0 & |.q2.|<>0 & q1`1/|.q1.|<q2`1/|.q2.|
holds (for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2 holds p1`1/|.p1.|<p2`1/|.p2.|)
proof let cn be Real,q1,q2 be Point of TOP-REAL 2;
assume A1: -1<cn & cn<1 & q1`2<=0 & q2`2<=0 & |.q1.|<>0 & |.q2.|<>0
& q1`1/|.q1.|<q2`1/|.q2.|;
now per cases by A1;
case A2: q1`2<0;
now per cases by A1;
case q2`2<0;
hence (for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2 holds
p1`1/|.p1.|<p2`1/|.p2.|) by A1,A2,JGRAPH_4:148;
case A3: q2`2=0;
then |.q2.|^2=(q2`1)^2+0 by JGRAPH_3:10,SQUARE_1:60 .=(q2`1)^2;
then A4: |.q2.|=q2`1 or |.q2.|=-(q2`1) by JGRAPH_3:1;
now assume |.q2.|=-(q2`1);
then 1=(-(q2`1))/|.q2.| by A1,XCMPLX_1:60;
then A5: q1`1/|.q1.|< -1 by A1,XCMPLX_1:191;
A6: |.q1.|>=0 by TOPRNS_1:26;
(|.q1.|)^2=(q1`1)^2+(q1`2)^2 by JGRAPH_3:10;
then (|.q1.|)^2-(q1`1)^2=(q1`2)^2 by XCMPLX_1:26;
then (|.q1.|)^2-(q1`1)^2>=0 by SQUARE_1:72;
then (|.q1.|)^2-(q1`1)^2+(q1`1)^2>=0+(q1`1)^2 by REAL_1:55;
then (|.q1.|)^2>=(q1`1)^2 by XCMPLX_1:27;
then -|.q1.|<=q1`1 & q1`1<=|.q1.| by A6,JGRAPH_2:5;
then (-|.q1.|)/|.q1.|<=q1`1/|.q1.| by A1,A6,REAL_1:73;
hence contradiction by A1,A5,XCMPLX_1:198;
end;
then A7: q2`1/|.q2.|=1 by A1,A4,XCMPLX_1:60;
thus for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2 holds
p1`1/|.p1.|<p2`1/|.p2.|
proof let p1,p2 be Point of TOP-REAL 2;
assume A8: p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2;
then A9: p2=q2 by A3,JGRAPH_4:120;
A10: |.p1.|=|.q1.| by A8,JGRAPH_4:135;
A11: |.p1.|>=0 by TOPRNS_1:26;
(|.p1.|)^2=(p1`1)^2+(p1`2)^2 by JGRAPH_3:10;
then A12: (|.p1.|)^2-(p1`1)^2=(p1`2)^2 by XCMPLX_1:26;
then (|.p1.|)^2-(p1`1)^2>=0 by SQUARE_1:72;
then (|.p1.|)^2-(p1`1)^2+(p1`1)^2>=0+(p1`1)^2 by REAL_1:55;
then (|.p1.|)^2>=(p1`1)^2 by XCMPLX_1:27;
then -|.p1.|<=p1`1 & p1`1<=|.p1.| by A11,JGRAPH_2:5;
then (|.p1.|)/|.p1.|>=p1`1/|.p1.| by A1,A10,A11,REAL_1:73;
then A13: 1>= p1`1/|.p1.| by A1,A10,XCMPLX_1:60;
A14: p1`2<0 by A1,A2,A8,Th28;
now assume 1= p1`1/|.p1.|; then (1)*|.p1.|=p1`1 by A1,A10,XCMPLX_1:
88
;
then (|.p1.|)^2-(p1`1)^2=0 by XCMPLX_1:14;
hence contradiction by A12,A14,SQUARE_1:73;
end;
hence p1`1/|.p1.|<p2`1/|.p2.| by A7,A9,A13,REAL_1:def 5;
end;
end;
hence (for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2 holds
p1`1/|.p1.|<p2`1/|.p2.|);
case A15: q1`2=0;
then |.q1.|^2=(q1`1)^2+0 by JGRAPH_3:10,SQUARE_1:60 .=(q1`1)^2;
then A16: |.q1.|=q1`1 or |.q1.|=-(q1`1) by JGRAPH_3:1;
now assume |.q1.|=(q1`1);
then A17: q2`1/|.q2.|> 1 by A1,XCMPLX_1:60;
A18: |.q2.|>=0 by TOPRNS_1:26;
(|.q2.|)^2=(q2`1)^2+(q2`2)^2 by JGRAPH_3:10;
then (|.q2.|)^2-(q2`1)^2=(q2`2)^2 by XCMPLX_1:26;
then (|.q2.|)^2-(q2`1)^2>=0 by SQUARE_1:72;
then (|.q2.|)^2-(q2`1)^2+(q2`1)^2>=0+(q2`1)^2 by REAL_1:55;
then (|.q2.|)^2>=(q2`1)^2 by XCMPLX_1:27;
then -|.q2.|<=q2`1 & q2`1<=|.q2.| by A18,JGRAPH_2:5;
then (|.q2.|)/|.q2.|>=q2`1/|.q2.| by A1,A18,REAL_1:73;
hence contradiction by A1,A17,XCMPLX_1:60;
end;
then (-(q1`1))/|.q1.|=1 by A1,A16,XCMPLX_1:60;
then A19: -(q1`1/|.q1.|)=1 by XCMPLX_1:188;
thus (for p1,p2 being Point of TOP-REAL 2 st
p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2
holds p1`1/|.p1.|<p2`1/|.p2.|)
proof let p1,p2 be Point of TOP-REAL 2;
assume A20: p1=(cn-FanMorphS).q1 & p2=(cn-FanMorphS).q2;
then A21: p1=q1 by A15,JGRAPH_4:120;
A22: |.p2.|=|.q2.| by A20,JGRAPH_4:135;
A23: |.p2.|>=0 by TOPRNS_1:26;
(|.p2.|)^2=(p2`1)^2+(p2`2)^2 by JGRAPH_3:10;
then A24: (|.p2.|)^2-(p2`1)^2=(p2`2)^2 by XCMPLX_1:26;
then (|.p2.|)^2-(p2`1)^2>=0 by SQUARE_1:72;
then (|.p2.|)^2-(p2`1)^2+(p2`1)^2>=0+(p2`1)^2 by REAL_1:55;
then (|.p2.|)^2>=(p2`1)^2 by XCMPLX_1:27;
then -|.p2.|<=p2`1 & p2`1<=|.p2.| by A23,JGRAPH_2:5;
then (-|.p2.|)/|.p2.|<=p2`1/|.p2.| by A1,A22,A23,REAL_1:73;
then A25: -1 <= p2`1/|.p2.| by A1,A22,XCMPLX_1:198;
now per cases;
case q2`2=0;
then p2=q2 by A20,JGRAPH_4:120;
hence p2`1/|.p2.|>-1 by A1,A19;
case q2`2<>0;
then A26: p2`2<0 by A1,A20,Th28;
now assume -1= p2`1/|.p2.|; then (-1)*|.p2.|=p2`1 by A1,A22,XCMPLX_1
:88;
then (-|.p2.|)^2=(p2`1)^2 by XCMPLX_1:180;
then (|.p2.|)^2=(p2`1)^2 by SQUARE_1:61;
then (|.p2.|)^2-(p2`1)^2=0 by XCMPLX_1:14;
hence contradiction by A24,A26,SQUARE_1:73;
end;
hence
p2`1/|.p2.|>-1 by A25,REAL_1:def 5;
end;
hence p1`1/|.p1.|<p2`1/|.p2.| by A19,A21;
end;
end;
hence thesis;
end;
begin :: Order of Points on Circle
Lm2: now let P be compact non empty Subset of TOP-REAL 2;
assume A1: P={q: |.q.|=1};
A2: proj1.:P c= [.-1,1.]
proof let y be set;assume y in proj1.:P;
then consider x being set such that
A3: x in dom proj1 & x in P & y=proj1.x by FUNCT_1:def 12;
reconsider q=x as Point of TOP-REAL 2 by A3;
A4: y=q`1 by A3,PSCOMP_1:def 28;
consider q2 being Point of TOP-REAL 2 such that
A5: q2=x & |.q2.|=1 by A1,A3;
(q`1)^2+(q`2)^2=1 by A5,JGRAPH_3:10,SQUARE_1:59;
then A6: (q`2)^2=1-(q`1)^2 by XCMPLX_1:26;
0<=(q`2)^2 by SQUARE_1:72;
then 1-(q`1)^2+(q`1)^2 >=0+(q`1)^2 by A6,REAL_1:55;
then 1>=(q`1)^2 by XCMPLX_1:27;
then -1<=q`1 & q`1<=1 by JGRAPH_4:4;
hence y in [.-1,1.] by A4,TOPREAL5:1;
end;
[.-1,1.] c= proj1.:P
proof let y be set;assume
y in [.-1,1.];
then y in {r where r is Real: -1<=r & r<=1 } by RCOMP_1:def 1;
then consider r being Real such that
A7: y=r & -1<=r & r<=1;
set q=|[r,sqrt(1-r^2)]|;
A8: dom proj1=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A9: q`1=r & q`2=sqrt(1-r^2) by EUCLID:56;
1^2>=r^2 by A7,JGRAPH_2:7;
then A10: 1-r^2>=0 by SQUARE_1:12,59;
|.q.|=sqrt(r^2+(sqrt(1-r^2))^2) by A9,JGRAPH_3:10
.=sqrt(r^2+(1-r^2)) by A10,SQUARE_1:def 4
.=1 by SQUARE_1:83,XCMPLX_1:27;
then A11: q in P by A1;
proj1.q=q`1 by PSCOMP_1:def 28 .=r by EUCLID:56;
hence y in proj1.:P by A7,A8,A11,FUNCT_1:def 12;
end;
hence proj1.:P=[.-1,1.] by A2,XBOOLE_0:def 10;
A12: proj2.:P c= [.-1,1.]
proof let y be set;assume
y in proj2.:P;
then consider x being set such that
A13: x in dom proj2 & x in P & y=proj2.x by FUNCT_1:def 12;
reconsider q=x as Point of TOP-REAL 2 by A13;
A14: y=q`2 by A13,PSCOMP_1:def 29;
consider q2 being Point of TOP-REAL 2 such that
A15: q2=x & |.q2.|=1 by A1,A13;
(q`1)^2+(q`2)^2=1 by A15,JGRAPH_3:10,SQUARE_1:59;
then A16: (q`1)^2=1-(q`2)^2 by XCMPLX_1:26;
0<=(q`1)^2 by SQUARE_1:72;
then 1-(q`2)^2+(q`2)^2 >=0+(q`2)^2 by A16,REAL_1:55;
then 1>=(q`2)^2 by XCMPLX_1:27;
then -1<=q`2 & q`2<=1 by JGRAPH_4:4;
hence y in [.-1,1.] by A14,TOPREAL5:1;
end;
[.-1,1.] c= proj2.:P
proof let y be set;assume
y in [.-1,1.];
then y in {r where r is Real: -1<=r & r<=1 } by RCOMP_1:def 1;
then consider r being Real such that
A17: y=r & -1<=r & r<=1;
set q=|[sqrt(1-r^2),r]|;
A18: dom proj2=the carrier of TOP-REAL 2 by FUNCT_2:def 1;
A19: q`2=r & q`1=sqrt(1-r^2) by EUCLID:56;
1^2>=r^2 by A17,JGRAPH_2:7;
then A20: 1-r^2>=0 by SQUARE_1:12,59;
|.q.|=sqrt((sqrt(1-r^2))^2+r^2) by A19,JGRAPH_3:10
.=sqrt((1-r^2)+r^2) by A20,SQUARE_1:def 4
.=1 by SQUARE_1:83,XCMPLX_1:27;
then A21: q in P by A1;
proj2.q=q`2 by PSCOMP_1:def 29 .=r by EUCLID:56;
hence y in proj2.:P by A17,A18,A21,FUNCT_1:def 12;
end;
hence proj2.:P=[.-1,1.] by A12,XBOOLE_0:def 10;
end;
Lm3: for P being compact non empty Subset of TOP-REAL 2 st
P={q: |.q.|=1} holds W-bound(P)=-1
proof let P be compact non empty Subset of TOP-REAL 2;
assume A1: P={q: |.q.|=1};
A2: the carrier of ((TOP-REAL 2)|P) = P by JORDAN1:1;
proj1.:P=[.-1,1.] by A1,Lm2;
then (proj1|P).:P=[.-1,1.] by RFUNCT_2:5;
then (proj1||P).:P=[.-1,1.] by PSCOMP_1:def 26;
then inf ((proj1||P).:P)=-1 by JORDAN5A:20;
then inf (proj1||P)=-1 by A2,PSCOMP_1:def 20;
hence W-bound P=-1 by PSCOMP_1:def 30;
end;
theorem Th31: for P being compact non empty Subset of TOP-REAL 2 st
P={q: |.q.|=1}
holds W-bound(P)=-1 & E-bound(P)=1 & S-bound(P)=-1 & N-bound(P)=1
proof let P be compact non empty Subset of TOP-REAL 2;
assume A1: P={q: |.q.|=1};
hence W-bound(P)=-1 by Lm3;
A2: the carrier of ((TOP-REAL 2)|P) =P by JORDAN1:1;
proj1.:P=[.-1,1.] by A1,Lm2;
then (proj1|P).:P=[.-1,1.] by RFUNCT_2:5;
then (proj1||P).:P=[.-1,1.] by PSCOMP_1:def 26;
then sup ((proj1||P).:the carrier of ((TOP-REAL 2)|P))=1 by A2,JORDAN5A:20;
then sup (proj1||P)=1 by PSCOMP_1:def 21;
hence E-bound P=1 by PSCOMP_1:def 32;
proj2.:P=[.-1,1.] by A1,Lm2;
then (proj2|P).:P=[.-1,1.] by RFUNCT_2:5;
then A3: (proj2||P).:P=[.-1,1.] by PSCOMP_1:def 26;
then inf ((proj2||P).:P)=-1 by JORDAN5A:20;
then inf (proj2||P)=-1 by A2,PSCOMP_1:def 20;
hence S-bound P=-1 by PSCOMP_1:def 33;
sup ((proj2||P).:P)=1 by A3,JORDAN5A:20;
then sup (proj2||P)=1 by A2,PSCOMP_1:def 21;
hence N-bound P=1 by PSCOMP_1:def 31;
end;
theorem Th32: for P being compact non empty Subset of TOP-REAL 2 st
P={q: |.q.|=1}
holds W-min(P)=|[-1,0]|
proof let P be compact non empty Subset of TOP-REAL 2;
assume A1: P={q: |.q.|=1};
A2: the carrier of ((TOP-REAL 2)|P) = P by JORDAN1:1;
A3: W-bound P=-1 by A1,Lm3;
proj2.:P=[.-1,1.] by A1,Lm2;
then (proj2|P).:P=[.-1,1.] by RFUNCT_2:5;
then A4: (proj2||P).:P=[.-1,1.] by PSCOMP_1:def 26;
then inf ((proj2||P).:P)=-1 by JORDAN5A:20;
then inf (proj2||P)=-1 by A2,PSCOMP_1:def 20;
then S-bound P=-1 by PSCOMP_1:def 33;
then A5: SW-corner P=|[-1,-1]| by A3,PSCOMP_1:def 34;
sup ((proj2||P).:P)=1 by A4,JORDAN5A:20;
then sup (proj2||P)=1 by A2,PSCOMP_1:def 21;
then N-bound P=1 by PSCOMP_1:def 31;
then A6: NW-corner P=|[-1,1]| by A3,PSCOMP_1:def 35;
A7: {|[-1,0]|} c= LSeg(SW-corner P, NW-corner P)/\P
proof let x be set;assume
x in {|[-1,0]|};
then A8: x=|[-1,0]| by TARSKI:def 1;
set q=|[-1,0]|;
q`2=0 & q`1=-1 by EUCLID:56;
then |.q.|=sqrt((-1)^2+0^2) by JGRAPH_3:10
.=1 by SQUARE_1:59,60,61,83;
then A9: x in P by A1,A8;
q=|[(1/2)*(-1)+(1/2)*(-1),(1/2)*(-1)+(1/2)*1]|;
then q=|[(1/2)*(-1),(1/2)*(-1)]|+|[(1/2)*(-1),(1/2)*1]| by EUCLID:60;
then q=|[(1/2)*(-1),(1/2)*(-1)]|+(1/2)*|[-1,1]| by EUCLID:62;
then q=(1/2)*|[-1,-1]|+(1-(1/2))*|[-1,1]| by EUCLID:62;
then q in { (1-l)*(SW-corner P) + l*(NW-corner P) where l is Real:
0 <= l & l <= 1 } by A5,A6;
then x in LSeg(SW-corner P, NW-corner P) by A8,TOPREAL1:def 4;
hence x in LSeg(SW-corner P, NW-corner P)/\P by A9,XBOOLE_0:def 3;
end;
LSeg(SW-corner P, NW-corner P)/\P c= {|[-1,0]|}
proof let x be set;assume x in LSeg(SW-corner P, NW-corner P)/\P;
then A10: x in LSeg(SW-corner P, NW-corner P) & x in P by XBOOLE_0:def 3;
then x in { (1-l)*(SW-corner P) + l*(NW-corner P) where l is Real:
0 <= l & l