let f, g be Function of I[01],(TOP-REAL 2); for C0, KXP, KXN, KYP, KYN being Subset of (TOP-REAL 2)
for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.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
let C0, KXP, KXN, KYP, KYN be Subset of (TOP-REAL 2); for O, I being Point of I[01] st O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.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
let O, I be Point of I[01]; ( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.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 implies rng f meets rng g )
assume A1:
( O = 0 & I = 1 & f is continuous & f is one-to-one & g is continuous & g is one-to-one & C0 = { p where p is Point of (TOP-REAL 2) : |.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 )
; rng f meets rng g
A2:
dom g = the carrier of I[01]
by FUNCT_2:def 1;
reconsider gg = (Sq_Circ ") * g as Function of I[01],(TOP-REAL 2) by FUNCT_2:13, JGRAPH_3:29;
reconsider ff = (Sq_Circ ") * f as Function of I[01],(TOP-REAL 2) by FUNCT_2:13, JGRAPH_3:29;
A3:
dom gg = the carrier of I[01]
by FUNCT_2:def 1;
A4:
dom ff = the carrier of I[01]
by FUNCT_2:def 1;
A5:
( (ff . O) `1 = - 1 & (ff . I) `1 = 1 & (gg . O) `2 = - 1 & (gg . I) `2 = 1 )
proof
reconsider pz =
gg . O as
Point of
(TOP-REAL 2) ;
reconsider py =
ff . I as
Point of
(TOP-REAL 2) ;
reconsider px =
ff . O as
Point of
(TOP-REAL 2) ;
set q =
px;
A6:
|[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `1 = (px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))
by EUCLID:52;
reconsider pu =
gg . I as
Point of
(TOP-REAL 2) ;
A7:
|[((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)))
by EUCLID:52;
consider p2 being
Point of
(TOP-REAL 2) such that A8:
f . I = p2
and A9:
|.p2.| = 1
and A10:
p2 `2 <= p2 `1
and A11:
p2 `2 >= - (p2 `1)
by A1;
A12:
ff . I = (Sq_Circ ") . (f . I)
by A4, FUNCT_1:12;
then A13:
p2 = Sq_Circ . py
by A8, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A14:
p2 <> 0. (TOP-REAL 2)
by A9, TOPRNS_1:23;
then A15:
(Sq_Circ ") . p2 = |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]|
by A10, A11, JGRAPH_3:28;
then A16:
py `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by A12, A8, EUCLID:52;
((p2 `2) / (p2 `1)) ^2 >= 0
by XREAL_1:63;
then A17:
sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0
by SQUARE_1:25;
A18:
py `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by A12, A8, A15, EUCLID:52;
A20:
( (
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 A10, A11, A17, XREAL_1:64;
then
( (
(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 A12, A8, A15, A16, A17, EUCLID:52, XREAL_1:64;
then A21:
Sq_Circ . py = |[((py `1) / (sqrt (1 + (((py `2) / (py `1)) ^2)))),((py `2) / (sqrt (1 + (((py `2) / (py `1)) ^2))))]|
by A16, A18, A19, JGRAPH_2:3, JGRAPH_3:def 1;
A22:
((py `2) / (py `1)) ^2 >= 0
by XREAL_1:63;
then A23:
sqrt (1 + (((py `2) / (py `1)) ^2)) > 0
by SQUARE_1:25;
A24:
now not py `1 = - 1assume A25:
py `1 = - 1
;
contradiction
- (p2 `2) <= - (- (p2 `1))
by A11, XREAL_1:24;
then
- (p2 `2) < 0
by A13, A21, A7, A22, A25, SQUARE_1:25, XREAL_1:141;
then
- (- (p2 `2)) > - 0
;
hence
contradiction
by A10, A13, A21, A23, A25, EUCLID:52;
verum end;
|[((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:52;
then |.p2.| ^2 =
(((py `1) / (sqrt (1 + (((py `2) / (py `1)) ^2)))) ^2) + (((py `2) / (sqrt (1 + (((py `2) / (py `1)) ^2)))) ^2)
by A13, A21, A7, JGRAPH_3:1
.=
(((py `1) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2)) + (((py `2) / (sqrt (1 + (((py `2) / (py `1)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((py `1) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2)) + (((py `2) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2))
by XCMPLX_1:76
.=
(((py `1) ^2) / (1 + (((py `2) / (py `1)) ^2))) + (((py `2) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2))
by A22, SQUARE_1:def 2
.=
(((py `1) ^2) / (1 + (((py `2) / (py `1)) ^2))) + (((py `2) ^2) / (1 + (((py `2) / (py `1)) ^2)))
by A22, SQUARE_1:def 2
.=
(((py `1) ^2) + ((py `2) ^2)) / (1 + (((py `2) / (py `1)) ^2))
by XCMPLX_1:62
;
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 A9;
then
((py `1) ^2) + ((py `2) ^2) = 1
+ (((py `2) / (py `1)) ^2)
by A22, XCMPLX_1:87;
then A26:
(((py `1) ^2) + ((py `2) ^2)) - 1
= ((py `2) ^2) / ((py `1) ^2)
by XCMPLX_1:76;
py `1 <> 0
by A16, A18, A17, A19, A20, XREAL_1:64;
then
((((py `1) ^2) + ((py `2) ^2)) - 1) * ((py `1) ^2) = (py `2) ^2
by A26, XCMPLX_1:6, XCMPLX_1:87;
then A27:
(((py `1) ^2) - 1) * (((py `1) ^2) + ((py `2) ^2)) = 0
;
((py `1) ^2) + ((py `2) ^2) <> 0
by A19, COMPLEX1:1;
then
((py `1) - 1) * ((py `1) + 1) = 0
by A27, XCMPLX_1:6;
then A28:
(
(py `1) - 1
= 0 or
(py `1) + 1
= 0 )
by XCMPLX_1:6;
A29:
|[((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)))
by EUCLID:52;
consider p1 being
Point of
(TOP-REAL 2) such that A30:
f . O = p1
and A31:
|.p1.| = 1
and A32:
p1 `2 >= p1 `1
and A33:
p1 `2 <= - (p1 `1)
by A1;
((p1 `2) / (p1 `1)) ^2 >= 0
by XREAL_1:63;
then A34:
sqrt (1 + (((p1 `2) / (p1 `1)) ^2)) > 0
by SQUARE_1:25;
A35:
ff . O = (Sq_Circ ") . (f . O)
by A4, FUNCT_1:12;
then A36:
p1 = Sq_Circ . px
by A30, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A37:
p1 <> 0. (TOP-REAL 2)
by A31, TOPRNS_1:23;
then
(Sq_Circ ") . p1 = |[((p1 `1) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))),((p1 `2) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))))]|
by A32, A33, JGRAPH_3:28;
then A38:
(
px `1 = (p1 `1) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) &
px `2 = (p1 `2) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) )
by A35, A30, EUCLID:52;
( (
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 A32, A33, A34, XREAL_1:64;
then A40:
( (
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 A38, A34, XREAL_1:64;
then
( (
px `2 <= px `1 &
- (px `1) <= px `2 ) or (
px `2 >= px `1 &
px `2 <= - (px `1) ) )
by A38, A34, XREAL_1:64;
then A41:
Sq_Circ . px = |[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]|
by A39, JGRAPH_2:3, JGRAPH_3:def 1;
A42:
((px `2) / (px `1)) ^2 >= 0
by XREAL_1:63;
then A43:
sqrt (1 + (((px `2) / (px `1)) ^2)) > 0
by SQUARE_1:25;
A44:
now not px `1 = 1assume A45:
px `1 = 1
;
contradiction
- (p1 `2) >= - (- (p1 `1))
by A33, XREAL_1:24;
then
- (p1 `2) > 0
by A36, A41, A6, A43, A45, XREAL_1:139;
then
- (- (p1 `2)) < - 0
;
hence
contradiction
by A32, A36, A41, A43, A45, EUCLID:52;
verum end;
|[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `2 = (px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))
by EUCLID:52;
then |.p1.| ^2 =
(((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2)
by A36, A41, A6, JGRAPH_3:1
.=
(((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2))
by XCMPLX_1:76
.=
(((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2))
by A42, SQUARE_1:def 2
.=
(((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2)))
by A42, SQUARE_1:def 2
.=
(((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))
by XCMPLX_1:62
;
then
((((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))) * (1 + (((px `2) / (px `1)) ^2)) = 1
* (1 + (((px `2) / (px `1)) ^2))
by A31;
then
((px `1) ^2) + ((px `2) ^2) = 1
+ (((px `2) / (px `1)) ^2)
by A42, XCMPLX_1:87;
then A46:
(((px `1) ^2) + ((px `2) ^2)) - 1
= ((px `2) ^2) / ((px `1) ^2)
by XCMPLX_1:76;
px `1 <> 0
by A38, A34, A39, A40, XREAL_1:64;
then
((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) = (px `2) ^2
by A46, XCMPLX_1:6, XCMPLX_1:87;
then A47:
(((px `1) ^2) - 1) * (((px `1) ^2) + ((px `2) ^2)) = 0
;
A48:
|[((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)))
by EUCLID:52;
consider p4 being
Point of
(TOP-REAL 2) such that A49:
g . I = p4
and A50:
|.p4.| = 1
and A51:
p4 `2 >= p4 `1
and A52:
p4 `2 >= - (p4 `1)
by A1;
((p4 `1) / (p4 `2)) ^2 >= 0
by XREAL_1:63;
then A53:
sqrt (1 + (((p4 `1) / (p4 `2)) ^2)) > 0
by SQUARE_1:25;
A54:
- (p4 `2) <= - (- (p4 `1))
by A52, XREAL_1:24;
then A55:
( (
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 A51, A53, XREAL_1:64;
A56:
gg . I = (Sq_Circ ") . (g . I)
by A3, FUNCT_1:12;
then A57:
p4 = Sq_Circ . pu
by A49, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A58:
p4 <> 0. (TOP-REAL 2)
by A50, TOPRNS_1:23;
then A59:
(Sq_Circ ") . p4 = |[((p4 `1) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2)))),((p4 `2) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2))))]|
by A51, A54, JGRAPH_3:30;
then A60:
pu `2 = (p4 `2) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2)))
by A56, A49, EUCLID:52;
A61:
pu `1 = (p4 `1) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2)))
by A56, A49, A59, EUCLID:52;
( (
(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 A56, A49, A59, A60, A53, A55, EUCLID:52, XREAL_1:64;
then A63:
Sq_Circ . pu = |[((pu `1) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))),((pu `2) / (sqrt (1 + (((pu `1) / (pu `2)) ^2))))]|
by A60, A61, A62, JGRAPH_2:3, JGRAPH_3:4;
A64:
((pu `1) / (pu `2)) ^2 >= 0
by XREAL_1:63;
then A65:
sqrt (1 + (((pu `1) / (pu `2)) ^2)) > 0
by SQUARE_1:25;
A66:
now not pu `2 = - 1assume A67:
pu `2 = - 1
;
contradictionthen
- (p4 `1) < 0
by A52, A57, A63, A48, A64, SQUARE_1:25, XREAL_1:141;
then
- (- (p4 `1)) > - 0
;
hence
contradiction
by A51, A57, A63, A65, A67, EUCLID:52;
verum end;
|[((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:52;
then |.p4.| ^2 =
(((pu `2) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))) ^2) + (((pu `1) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))) ^2)
by A57, A63, A48, JGRAPH_3:1
.=
(((pu `2) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2)) + (((pu `1) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((pu `2) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2)) + (((pu `1) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2))
by XCMPLX_1:76
.=
(((pu `2) ^2) / (1 + (((pu `1) / (pu `2)) ^2))) + (((pu `1) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2))
by A64, SQUARE_1:def 2
.=
(((pu `2) ^2) / (1 + (((pu `1) / (pu `2)) ^2))) + (((pu `1) ^2) / (1 + (((pu `1) / (pu `2)) ^2)))
by A64, SQUARE_1:def 2
.=
(((pu `2) ^2) + ((pu `1) ^2)) / (1 + (((pu `1) / (pu `2)) ^2))
by XCMPLX_1:62
;
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 A50;
then
((pu `2) ^2) + ((pu `1) ^2) = 1
+ (((pu `1) / (pu `2)) ^2)
by A64, XCMPLX_1:87;
then A68:
(((pu `2) ^2) + ((pu `1) ^2)) - 1
= ((pu `1) ^2) / ((pu `2) ^2)
by XCMPLX_1:76;
pu `2 <> 0
by A60, A61, A53, A62, A55, XREAL_1:64;
then
((((pu `2) ^2) + ((pu `1) ^2)) - 1) * ((pu `2) ^2) = (pu `1) ^2
by A68, XCMPLX_1:6, XCMPLX_1:87;
then A69:
(((pu `2) ^2) - 1) * (((pu `2) ^2) + ((pu `1) ^2)) = 0
;
((pu `2) ^2) + ((pu `1) ^2) <> 0
by A62, COMPLEX1:1;
then
((pu `2) - 1) * ((pu `2) + 1) = 0
by A69, XCMPLX_1:6;
then A70:
(
(pu `2) - 1
= 0 or
(pu `2) + 1
= 0 )
by XCMPLX_1:6;
consider p3 being
Point of
(TOP-REAL 2) such that A71:
g . O = p3
and A72:
|.p3.| = 1
and A73:
p3 `2 <= p3 `1
and A74:
p3 `2 <= - (p3 `1)
by A1;
A75:
p3 <> 0. (TOP-REAL 2)
by A72, TOPRNS_1:23;
A76:
gg . O = (Sq_Circ ") . (g . O)
by A3, FUNCT_1:12;
then A77:
p3 = Sq_Circ . pz
by A71, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A78:
- (p3 `2) >= - (- (p3 `1))
by A74, XREAL_1:24;
then A79:
(Sq_Circ ") . p3 = |[((p3 `1) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))),((p3 `2) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))))]|
by A73, A75, JGRAPH_3:30;
then A80:
pz `2 = (p3 `2) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))
by A76, A71, EUCLID:52;
((p3 `1) / (p3 `2)) ^2 >= 0
by XREAL_1:63;
then A81:
sqrt (1 + (((p3 `1) / (p3 `2)) ^2)) > 0
by SQUARE_1:25;
A82:
pz `1 = (p3 `1) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))
by A76, A71, A79, EUCLID:52;
( (
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 A73, A78, A81, XREAL_1:64;
then A84:
( (
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 A80, A82, A81, XREAL_1:64;
then
( (
(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 A76, A71, A79, A80, A81, EUCLID:52, XREAL_1:64;
then A85:
Sq_Circ . pz = |[((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))),((pz `2) / (sqrt (1 + (((pz `1) / (pz `2)) ^2))))]|
by A80, A82, A83, JGRAPH_2:3, JGRAPH_3:4;
A86:
((pz `1) / (pz `2)) ^2 >= 0
by XREAL_1:63;
then A87:
sqrt (1 + (((pz `1) / (pz `2)) ^2)) > 0
by SQUARE_1:25;
A88:
now not pz `2 = 1assume A89:
pz `2 = 1
;
contradictionthen
- (p3 `1) > 0
by A74, A77, A85, A29, A87, XREAL_1:139;
then
- (- (p3 `1)) < - 0
;
hence
contradiction
by A73, A77, A85, A87, A89, EUCLID:52;
verum end;
|[((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:52;
then |.p3.| ^2 =
(((pz `2) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2)
by A77, A85, A29, JGRAPH_3:1
.=
(((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2))
by XCMPLX_1:76
.=
(((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2))
by A86, SQUARE_1:def 2
.=
(((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / (1 + (((pz `1) / (pz `2)) ^2)))
by A86, SQUARE_1:def 2
.=
(((pz `2) ^2) + ((pz `1) ^2)) / (1 + (((pz `1) / (pz `2)) ^2))
by XCMPLX_1:62
;
then
((((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 A72;
then
((pz `2) ^2) + ((pz `1) ^2) = 1
+ (((pz `1) / (pz `2)) ^2)
by A86, XCMPLX_1:87;
then A90:
(((pz `2) ^2) + ((pz `1) ^2)) - 1
= ((pz `1) ^2) / ((pz `2) ^2)
by XCMPLX_1:76;
pz `2 <> 0
by A80, A82, A81, A83, A84, XREAL_1:64;
then
((((pz `2) ^2) + ((pz `1) ^2)) - 1) * ((pz `2) ^2) = (pz `1) ^2
by A90, XCMPLX_1:6, XCMPLX_1:87;
then A91:
(((pz `2) ^2) - 1) * (((pz `2) ^2) + ((pz `1) ^2)) = 0
;
((pz `2) ^2) + ((pz `1) ^2) <> 0
by A83, COMPLEX1:1;
then
((pz `2) - 1) * ((pz `2) + 1) = 0
by A91, XCMPLX_1:6;
then A92:
(
(pz `2) - 1
= 0 or
(pz `2) + 1
= 0 )
by XCMPLX_1:6;
((px `1) ^2) + ((px `2) ^2) <> 0
by A39, COMPLEX1:1;
then
((px `1) - 1) * ((px `1) + 1) = 0
by A47, XCMPLX_1:6;
then
(
(px `1) - 1
= 0 or
(px `1) + 1
= 0 )
by XCMPLX_1:6;
hence
(
(ff . O) `1 = - 1 &
(ff . I) `1 = 1 &
(gg . O) `2 = - 1 &
(gg . I) `2 = 1 )
by A44, A28, A24, A92, A88, A70, A66;
verum
end;
A93:
dom f = the carrier of I[01]
by FUNCT_2:def 1;
A94:
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];
( ( - 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 ) )
f . r in rng f
by A93, FUNCT_1:3;
then
f . r in C0
by A1;
then consider p1 being
Point of
(TOP-REAL 2) such that A95:
f . r = p1
and A96:
|.p1.| >= 1
by A1;
g . r in rng g
by A2, FUNCT_1:3;
then
g . r in C0
by A1;
then consider p2 being
Point of
(TOP-REAL 2) such that A97:
g . r = p2
and A98:
|.p2.| >= 1
by A1;
A99:
gg . r = (Sq_Circ ") . (g . r)
by A3, FUNCT_1:12;
A100:
now ( ( p2 = 0. (TOP-REAL 2) & contradiction ) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) & ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) & ( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 ) ) )per cases
( p2 = 0. (TOP-REAL 2) or ( p2 <> 0. (TOP-REAL 2) & ( ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) or ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) ) or ( p2 <> 0. (TOP-REAL 2) & not ( p2 `2 <= p2 `1 & - (p2 `1) <= p2 `2 ) & not ( p2 `2 >= p2 `1 & p2 `2 <= - (p2 `1) ) ) )
;
case A101:
(
p2 <> 0. (TOP-REAL 2) & ( (
p2 `2 <= p2 `1 &
- (p2 `1) <= p2 `2 ) or (
p2 `2 >= p2 `1 &
p2 `2 <= - (p2 `1) ) ) )
;
( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 )reconsider px =
gg . r as
Point of
(TOP-REAL 2) ;
A102:
(Sq_Circ ") . p2 = |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]|
by A101, JGRAPH_3:28;
then A103:
px `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by A99, A97, EUCLID:52;
set q =
px;
A104:
(px `1) ^2 >= 0
by XREAL_1:63;
|.p2.| ^2 >= |.p2.|
by A98, XREAL_1:151;
then A105:
|.p2.| ^2 >= 1
by A98, XXREAL_0:2;
A106:
(px `2) ^2 >= 0
by XREAL_1:63;
((p2 `2) / (p2 `1)) ^2 >= 0
by XREAL_1:63;
then A107:
sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0
by SQUARE_1:25;
A108:
px `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by A99, A97, A102, EUCLID:52;
( (
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 A101, A107, XREAL_1:64;
then A110:
( (
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 A103, A108, A107, XREAL_1:64;
then A111:
px `1 <> 0
by A103, A108, A107, A109, XREAL_1:64;
( (
(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 A99, A97, A102, A103, A107, A110, EUCLID:52, XREAL_1:64;
then A112:
Sq_Circ . px = |[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]|
by A103, A108, A109, JGRAPH_2:3, JGRAPH_3:def 1;
(Sq_Circ ") . p2 = px
by A3, A97, FUNCT_1:12;
then A113:
p2 = Sq_Circ . px
by FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A114:
((px `2) / (px `1)) ^2 >= 0
by XREAL_1:63;
(
|[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `1 = (px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2))) &
|[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `2 = (px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))) )
by EUCLID:52;
then |.p2.| ^2 =
(((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2)
by A113, A112, JGRAPH_3:1
.=
(((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2))
by XCMPLX_1:76
.=
(((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2))
by A114, SQUARE_1:def 2
.=
(((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2)))
by A114, SQUARE_1:def 2
.=
(((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))
by XCMPLX_1:62
;
then
((((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))) * (1 + (((px `2) / (px `1)) ^2)) >= 1
* (1 + (((px `2) / (px `1)) ^2))
by A114, A105, XREAL_1:64;
then
((px `1) ^2) + ((px `2) ^2) >= 1
+ (((px `2) / (px `1)) ^2)
by A114, XCMPLX_1:87;
then
((px `1) ^2) + ((px `2) ^2) >= 1
+ (((px `2) ^2) / ((px `1) ^2))
by XCMPLX_1:76;
then
(((px `1) ^2) + ((px `2) ^2)) - 1
>= (1 + (((px `2) ^2) / ((px `1) ^2))) - 1
by XREAL_1:9;
then
((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) >= (((px `2) ^2) / ((px `1) ^2)) * ((px `1) ^2)
by A104, XREAL_1:64;
then
(((px `1) ^2) + (((px `2) ^2) - 1)) * ((px `1) ^2) >= (px `2) ^2
by A111, XCMPLX_1:6, XCMPLX_1:87;
then
((((px `1) ^2) * ((px `1) ^2)) + (((px `1) ^2) * (((px `2) ^2) - 1))) - ((px `2) ^2) >= ((px `2) ^2) - ((px `2) ^2)
by XREAL_1:9;
then A115:
(((px `1) ^2) - 1) * (((px `1) ^2) + ((px `2) ^2)) >= 0
;
((px `1) ^2) + ((px `2) ^2) <> 0
by A109, COMPLEX1:1;
then
((px `1) - 1) * ((px `1) + 1) >= 0
by A104, A115, A106, XREAL_1:132;
hence
(
- 1
>= (gg . r) `1 or
(gg . r) `1 >= 1 or
- 1
>= (gg . r) `2 or
(gg . r) `2 >= 1 )
by XREAL_1:95;
verum end; case A116:
(
p2 <> 0. (TOP-REAL 2) & not (
p2 `2 <= p2 `1 &
- (p2 `1) <= p2 `2 ) & not (
p2 `2 >= p2 `1 &
p2 `2 <= - (p2 `1) ) )
;
( - 1 >= (gg . r) `1 or (gg . r) `1 >= 1 or - 1 >= (gg . r) `2 or (gg . r) `2 >= 1 )reconsider pz =
gg . r as
Point of
(TOP-REAL 2) ;
A117:
(Sq_Circ ") . p2 = |[((p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2))))]|
by A116, JGRAPH_3:28;
then A118:
pz `2 = (p2 `2) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))
by A99, A97, EUCLID:52;
((p2 `1) / (p2 `2)) ^2 >= 0
by XREAL_1:63;
then A119:
sqrt (1 + (((p2 `1) / (p2 `2)) ^2)) > 0
by SQUARE_1:25;
A122:
pz `1 = (p2 `1) * (sqrt (1 + (((p2 `1) / (p2 `2)) ^2)))
by A99, A97, A117, EUCLID:52;
( (
p2 `1 <= p2 `2 &
- (p2 `2) <= p2 `1 ) or (
p2 `1 >= p2 `2 &
p2 `1 <= - (p2 `2) ) )
by A116, JGRAPH_2:13;
then
( (
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 A119, XREAL_1:64;
then A123:
( (
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 A118, A122, A119, XREAL_1:64;
then A124:
pz `2 <> 0
by A118, A122, A119, A120, XREAL_1:64;
( (
(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 A99, A97, A117, A118, A119, A123, EUCLID:52, XREAL_1:64;
then A125:
Sq_Circ . pz = |[((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))),((pz `2) / (sqrt (1 + (((pz `1) / (pz `2)) ^2))))]|
by A118, A122, A120, JGRAPH_2:3, JGRAPH_3:4;
A126:
((pz `1) / (pz `2)) ^2 >= 0
by XREAL_1:63;
|.p2.| ^2 >= |.p2.|
by A98, XREAL_1:151;
then A127:
|.p2.| ^2 >= 1
by A98, XXREAL_0:2;
A128:
|[((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:52;
A129:
(pz `1) ^2 >= 0
by XREAL_1:63;
A130:
(pz `2) ^2 >= 0
by XREAL_1:63;
(
p2 = Sq_Circ . pz &
|[((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))) )
by A99, A97, EUCLID:52, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
then |.p2.| ^2 =
(((pz `2) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2)
by A125, A128, JGRAPH_3:1
.=
(((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2))
by XCMPLX_1:76
.=
(((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2))
by A126, SQUARE_1:def 2
.=
(((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / (1 + (((pz `1) / (pz `2)) ^2)))
by A126, SQUARE_1:def 2
.=
(((pz `2) ^2) + ((pz `1) ^2)) / (1 + (((pz `1) / (pz `2)) ^2))
by XCMPLX_1:62
;
then
((((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 A126, A127, XREAL_1:64;
then
((pz `2) ^2) + ((pz `1) ^2) >= 1
+ (((pz `1) / (pz `2)) ^2)
by A126, XCMPLX_1:87;
then
((pz `2) ^2) + ((pz `1) ^2) >= 1
+ (((pz `1) ^2) / ((pz `2) ^2))
by XCMPLX_1:76;
then
(((pz `2) ^2) + ((pz `1) ^2)) - 1
>= (1 + (((pz `1) ^2) / ((pz `2) ^2))) - 1
by XREAL_1:9;
then
((((pz `2) ^2) + ((pz `1) ^2)) - 1) * ((pz `2) ^2) >= (((pz `1) ^2) / ((pz `2) ^2)) * ((pz `2) ^2)
by A130, XREAL_1:64;
then
(((pz `2) ^2) + (((pz `1) ^2) - 1)) * ((pz `2) ^2) >= (pz `1) ^2
by A124, XCMPLX_1:6, XCMPLX_1:87;
then
((((pz `2) ^2) * ((pz `2) ^2)) + (((pz `2) ^2) * (((pz `1) ^2) - 1))) - ((pz `1) ^2) >= ((pz `1) ^2) - ((pz `1) ^2)
by XREAL_1:9;
then A131:
(((pz `2) ^2) - 1) * (((pz `2) ^2) + ((pz `1) ^2)) >= 0
;
((pz `2) ^2) + ((pz `1) ^2) <> 0
by A120, COMPLEX1:1;
then
((pz `2) - 1) * ((pz `2) + 1) >= 0
by A130, A131, A129, XREAL_1:132;
hence
(
- 1
>= (gg . r) `1 or
(gg . r) `1 >= 1 or
- 1
>= (gg . r) `2 or
(gg . r) `2 >= 1 )
by XREAL_1:95;
verum end; end; end;
A132:
ff . r = (Sq_Circ ") . (f . r)
by A4, FUNCT_1:12;
now ( ( p1 = 0. (TOP-REAL 2) & contradiction ) or ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) ) & ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) ) or ( p1 <> 0. (TOP-REAL 2) & not ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) & not ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) & ( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 ) ) )per cases
( p1 = 0. (TOP-REAL 2) or ( p1 <> 0. (TOP-REAL 2) & ( ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) or ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) ) ) or ( p1 <> 0. (TOP-REAL 2) & not ( p1 `2 <= p1 `1 & - (p1 `1) <= p1 `2 ) & not ( p1 `2 >= p1 `1 & p1 `2 <= - (p1 `1) ) ) )
;
case A133:
(
p1 <> 0. (TOP-REAL 2) & ( (
p1 `2 <= p1 `1 &
- (p1 `1) <= p1 `2 ) or (
p1 `2 >= p1 `1 &
p1 `2 <= - (p1 `1) ) ) )
;
( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 )reconsider px =
ff . r as
Point of
(TOP-REAL 2) ;
A134:
(Sq_Circ ") . p1 = |[((p1 `1) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))),((p1 `2) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))))]|
by A133, JGRAPH_3:28;
then A135:
px `1 = (p1 `1) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))
by A132, A95, EUCLID:52;
((p1 `2) / (p1 `1)) ^2 >= 0
by XREAL_1:63;
then A136:
sqrt (1 + (((p1 `2) / (p1 `1)) ^2)) > 0
by SQUARE_1:25;
A137:
px `2 = (p1 `2) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))
by A132, A95, A134, EUCLID:52;
( (
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 A133, A136, XREAL_1:64;
then A139:
( (
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 A135, A137, A136, XREAL_1:64;
then A140:
px `1 <> 0
by A135, A137, A136, A138, XREAL_1:64;
|.p1.| ^2 >= |.p1.|
by A96, XREAL_1:151;
then A141:
|.p1.| ^2 >= 1
by A96, XXREAL_0:2;
A142:
(px `1) ^2 >= 0
by XREAL_1:63;
set q =
px;
A143:
|[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `2 = (px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))
by EUCLID:52;
A144:
(px `2) ^2 >= 0
by XREAL_1:63;
A145:
((px `2) / (px `1)) ^2 >= 0
by XREAL_1:63;
( (
(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 A132, A95, A134, A135, A136, A139, EUCLID:52, XREAL_1:64;
then A146:
Sq_Circ . px = |[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]|
by A135, A137, A138, JGRAPH_2:3, JGRAPH_3:def 1;
(
p1 = Sq_Circ . px &
|[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `1 = (px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2))) )
by A132, A95, EUCLID:52, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
then |.p1.| ^2 =
(((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2)
by A146, A143, JGRAPH_3:1
.=
(((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2))
by XCMPLX_1:76
.=
(((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2))
by A145, SQUARE_1:def 2
.=
(((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2)))
by A145, SQUARE_1:def 2
.=
(((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))
by XCMPLX_1:62
;
then
((((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))) * (1 + (((px `2) / (px `1)) ^2)) >= 1
* (1 + (((px `2) / (px `1)) ^2))
by A145, A141, XREAL_1:64;
then
((px `1) ^2) + ((px `2) ^2) >= 1
+ (((px `2) / (px `1)) ^2)
by A145, XCMPLX_1:87;
then
((px `1) ^2) + ((px `2) ^2) >= 1
+ (((px `2) ^2) / ((px `1) ^2))
by XCMPLX_1:76;
then
(((px `1) ^2) + ((px `2) ^2)) - 1
>= (1 + (((px `2) ^2) / ((px `1) ^2))) - 1
by XREAL_1:9;
then
((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) >= (((px `2) ^2) / ((px `1) ^2)) * ((px `1) ^2)
by A142, XREAL_1:64;
then
(((px `1) ^2) + (((px `2) ^2) - 1)) * ((px `1) ^2) >= (px `2) ^2
by A140, XCMPLX_1:6, XCMPLX_1:87;
then
((((px `1) ^2) * ((px `1) ^2)) + (((px `1) ^2) * (((px `2) ^2) - 1))) - ((px `2) ^2) >= ((px `2) ^2) - ((px `2) ^2)
by XREAL_1:9;
then A147:
(((px `1) ^2) - 1) * (((px `1) ^2) + ((px `2) ^2)) >= 0
;
((px `1) ^2) + ((px `2) ^2) <> 0
by A138, COMPLEX1:1;
then
((px `1) - 1) * ((px `1) + 1) >= 0
by A142, A147, A144, XREAL_1:132;
hence
(
- 1
>= (ff . r) `1 or
(ff . r) `1 >= 1 or
- 1
>= (ff . r) `2 or
(ff . r) `2 >= 1 )
by XREAL_1:95;
verum end; case A148:
(
p1 <> 0. (TOP-REAL 2) & not (
p1 `2 <= p1 `1 &
- (p1 `1) <= p1 `2 ) & not (
p1 `2 >= p1 `1 &
p1 `2 <= - (p1 `1) ) )
;
( - 1 >= (ff . r) `1 or (ff . r) `1 >= 1 or - 1 >= (ff . r) `2 or (ff . r) `2 >= 1 )reconsider pz =
ff . r as
Point of
(TOP-REAL 2) ;
A149:
(Sq_Circ ") . p1 = |[((p1 `1) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2)))),((p1 `2) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2))))]|
by A148, JGRAPH_3:28;
then A150:
pz `2 = (p1 `2) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2)))
by A132, A95, EUCLID:52;
((p1 `1) / (p1 `2)) ^2 >= 0
by XREAL_1:63;
then A151:
sqrt (1 + (((p1 `1) / (p1 `2)) ^2)) > 0
by SQUARE_1:25;
A154:
pz `1 = (p1 `1) * (sqrt (1 + (((p1 `1) / (p1 `2)) ^2)))
by A132, A95, A149, EUCLID:52;
( (
p1 `1 <= p1 `2 &
- (p1 `2) <= p1 `1 ) or (
p1 `1 >= p1 `2 &
p1 `1 <= - (p1 `2) ) )
by A148, JGRAPH_2:13;
then
( (
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 A151, XREAL_1:64;
then A155:
( (
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 A150, A154, A151, XREAL_1:64;
then A156:
pz `2 <> 0
by A150, A154, A151, A152, XREAL_1:64;
( (
(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 A132, A95, A149, A150, A151, A155, EUCLID:52, XREAL_1:64;
then A157:
Sq_Circ . pz = |[((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))),((pz `2) / (sqrt (1 + (((pz `1) / (pz `2)) ^2))))]|
by A150, A154, A152, JGRAPH_2:3, JGRAPH_3:4;
A158:
((pz `1) / (pz `2)) ^2 >= 0
by XREAL_1:63;
|.p1.| ^2 >= |.p1.|
by A96, XREAL_1:151;
then A159:
|.p1.| ^2 >= 1
by A96, XXREAL_0:2;
A160:
|[((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:52;
A161:
(pz `1) ^2 >= 0
by XREAL_1:63;
A162:
(pz `2) ^2 >= 0
by XREAL_1:63;
(
p1 = Sq_Circ . pz &
|[((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))) )
by A132, A95, EUCLID:52, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
then |.p1.| ^2 =
(((pz `2) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2)
by A157, A160, JGRAPH_3:1
.=
(((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2))
by XCMPLX_1:76
.=
(((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2))
by A158, SQUARE_1:def 2
.=
(((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / (1 + (((pz `1) / (pz `2)) ^2)))
by A158, SQUARE_1:def 2
.=
(((pz `2) ^2) + ((pz `1) ^2)) / (1 + (((pz `1) / (pz `2)) ^2))
by XCMPLX_1:62
;
then
((((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 A158, A159, XREAL_1:64;
then
((pz `2) ^2) + ((pz `1) ^2) >= 1
+ (((pz `1) / (pz `2)) ^2)
by A158, XCMPLX_1:87;
then
((pz `2) ^2) + ((pz `1) ^2) >= 1
+ (((pz `1) ^2) / ((pz `2) ^2))
by XCMPLX_1:76;
then
(((pz `2) ^2) + ((pz `1) ^2)) - 1
>= (1 + (((pz `1) ^2) / ((pz `2) ^2))) - 1
by XREAL_1:9;
then
((((pz `2) ^2) + ((pz `1) ^2)) - 1) * ((pz `2) ^2) >= (((pz `1) ^2) / ((pz `2) ^2)) * ((pz `2) ^2)
by A162, XREAL_1:64;
then
(((pz `2) ^2) + (((pz `1) ^2) - 1)) * ((pz `2) ^2) >= (pz `1) ^2
by A156, XCMPLX_1:6, XCMPLX_1:87;
then
((((pz `2) ^2) * ((pz `2) ^2)) + (((pz `2) ^2) * (((pz `1) ^2) - 1))) - ((pz `1) ^2) >= ((pz `1) ^2) - ((pz `1) ^2)
by XREAL_1:9;
then A163:
(((pz `2) ^2) - 1) * (((pz `2) ^2) + ((pz `1) ^2)) >= 0
;
((pz `2) ^2) + ((pz `1) ^2) <> 0
by A152, COMPLEX1:1;
then
((pz `2) - 1) * ((pz `2) + 1) >= 0
by A162, A163, A161, XREAL_1:132;
hence
(
- 1
>= (ff . r) `1 or
(ff . r) `1 >= 1 or
- 1
>= (ff . r) `2 or
(ff . r) `2 >= 1 )
by XREAL_1:95;
verum end; end; 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 A100;
verum
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
reconsider pz =
gg . O as
Point of
(TOP-REAL 2) ;
reconsider py =
ff . I as
Point of
(TOP-REAL 2) ;
reconsider px =
ff . O as
Point of
(TOP-REAL 2) ;
set q =
px;
A164:
(
|[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `1 = (px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2))) &
|[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]| `2 = (px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))) )
by EUCLID:52;
A165:
((px `2) / (px `1)) ^2 >= 0
by XREAL_1:63;
consider p1 being
Point of
(TOP-REAL 2) such that A166:
f . O = p1
and A167:
|.p1.| = 1
and A168:
(
p1 `2 >= p1 `1 &
p1 `2 <= - (p1 `1) )
by A1;
A169:
ff . O = (Sq_Circ ") . (f . O)
by A4, FUNCT_1:12;
then A170:
p1 = Sq_Circ . px
by A166, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
((p1 `2) / (p1 `1)) ^2 >= 0
by XREAL_1:63;
then A171:
sqrt (1 + (((p1 `2) / (p1 `1)) ^2)) > 0
by SQUARE_1:25;
A172:
p1 <> 0. (TOP-REAL 2)
by A167, TOPRNS_1:23;
then
(Sq_Circ ") . p1 = |[((p1 `1) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2)))),((p1 `2) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))))]|
by A168, JGRAPH_3:28;
then A173:
(
px `1 = (p1 `1) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) &
px `2 = (p1 `2) * (sqrt (1 + (((p1 `2) / (p1 `1)) ^2))) )
by A169, A166, EUCLID:52;
( (
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 A168, A171, XREAL_1:64;
then A175:
( (
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 A173, A171, XREAL_1:64;
then
( (
px `2 <= px `1 &
- (px `1) <= px `2 ) or (
px `2 >= px `1 &
px `2 <= - (px `1) ) )
by A173, A171, XREAL_1:64;
then
Sq_Circ . px = |[((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))),((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2))))]|
by A174, JGRAPH_2:3, JGRAPH_3:def 1;
then |.p1.| ^2 =
(((px `1) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2)
by A170, A164, JGRAPH_3:1
.=
(((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) / (sqrt (1 + (((px `2) / (px `1)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((px `1) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2)) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2))
by XCMPLX_1:76
.=
(((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / ((sqrt (1 + (((px `2) / (px `1)) ^2))) ^2))
by A165, SQUARE_1:def 2
.=
(((px `1) ^2) / (1 + (((px `2) / (px `1)) ^2))) + (((px `2) ^2) / (1 + (((px `2) / (px `1)) ^2)))
by A165, SQUARE_1:def 2
.=
(((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))
by XCMPLX_1:62
;
then
((((px `1) ^2) + ((px `2) ^2)) / (1 + (((px `2) / (px `1)) ^2))) * (1 + (((px `2) / (px `1)) ^2)) = 1
* (1 + (((px `2) / (px `1)) ^2))
by A167;
then
((px `1) ^2) + ((px `2) ^2) = 1
+ (((px `2) / (px `1)) ^2)
by A165, XCMPLX_1:87;
then A176:
(((px `1) ^2) + ((px `2) ^2)) - 1
= ((px `2) ^2) / ((px `1) ^2)
by XCMPLX_1:76;
px `1 <> 0
by A173, A171, A174, A175, XREAL_1:64;
then
((((px `1) ^2) + ((px `2) ^2)) - 1) * ((px `1) ^2) = (px `2) ^2
by A176, XCMPLX_1:6, XCMPLX_1:87;
then A177:
(((px `1) ^2) - 1) * (((px `1) ^2) + ((px `2) ^2)) = 0
;
((px `1) ^2) + ((px `2) ^2) <> 0
by A174, COMPLEX1:1;
then
((px `1) - 1) * ((px `1) + 1) = 0
by A177, XCMPLX_1:6;
then
(
(px `1) - 1
= 0 or
(px `1) + 1
= 0 )
by XCMPLX_1:6;
then
(
px `1 = 1 or
px `1 = 0 - 1 )
;
hence
(
- 1
<= (ff . O) `2 &
(ff . O) `2 <= 1 )
by A173, A171, A175, XREAL_1:64;
( - 1 <= (ff . I) `2 & (ff . I) `2 <= 1 & - 1 <= (gg . O) `1 & (gg . O) `1 <= 1 & - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )
A178:
((py `2) / (py `1)) ^2 >= 0
by XREAL_1:63;
reconsider pu =
gg . I as
Point of
(TOP-REAL 2) ;
A179:
(
|[((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:52;
A180:
((pz `1) / (pz `2)) ^2 >= 0
by XREAL_1:63;
consider p2 being
Point of
(TOP-REAL 2) such that A181:
f . I = p2
and A182:
|.p2.| = 1
and A183:
(
p2 `2 <= p2 `1 &
p2 `2 >= - (p2 `1) )
by A1;
A184:
ff . I = (Sq_Circ ") . (f . I)
by A4, FUNCT_1:12;
then A185:
p2 = Sq_Circ . py
by A181, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A186:
p2 <> 0. (TOP-REAL 2)
by A182, TOPRNS_1:23;
then A187:
(Sq_Circ ") . p2 = |[((p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))),((p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2))))]|
by A183, JGRAPH_3:28;
then A188:
py `1 = (p2 `1) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by A184, A181, EUCLID:52;
A189:
py `2 = (p2 `2) * (sqrt (1 + (((p2 `2) / (p2 `1)) ^2)))
by A184, A181, A187, EUCLID:52;
((p2 `2) / (p2 `1)) ^2 >= 0
by XREAL_1:63;
then A190:
sqrt (1 + (((p2 `2) / (p2 `1)) ^2)) > 0
by SQUARE_1:25;
A192:
( (
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 A183, A190, XREAL_1:64;
then A193:
( (
(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 A184, A181, A187, A188, A190, EUCLID:52, XREAL_1:64;
then
Sq_Circ . py = |[((py `1) / (sqrt (1 + (((py `2) / (py `1)) ^2)))),((py `2) / (sqrt (1 + (((py `2) / (py `1)) ^2))))]|
by A188, A189, A191, JGRAPH_2:3, JGRAPH_3:def 1;
then |.p2.| ^2 =
(((py `1) / (sqrt (1 + (((py `2) / (py `1)) ^2)))) ^2) + (((py `2) / (sqrt (1 + (((py `2) / (py `1)) ^2)))) ^2)
by A185, A179, JGRAPH_3:1
.=
(((py `1) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2)) + (((py `2) / (sqrt (1 + (((py `2) / (py `1)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((py `1) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2)) + (((py `2) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2))
by XCMPLX_1:76
.=
(((py `1) ^2) / (1 + (((py `2) / (py `1)) ^2))) + (((py `2) ^2) / ((sqrt (1 + (((py `2) / (py `1)) ^2))) ^2))
by A178, SQUARE_1:def 2
.=
(((py `1) ^2) / (1 + (((py `2) / (py `1)) ^2))) + (((py `2) ^2) / (1 + (((py `2) / (py `1)) ^2)))
by A178, SQUARE_1:def 2
.=
(((py `1) ^2) + ((py `2) ^2)) / (1 + (((py `2) / (py `1)) ^2))
by XCMPLX_1:62
;
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 A182;
then
((py `1) ^2) + ((py `2) ^2) = 1
+ (((py `2) / (py `1)) ^2)
by A178, XCMPLX_1:87;
then A194:
(((py `1) ^2) + ((py `2) ^2)) - 1
= ((py `2) ^2) / ((py `1) ^2)
by XCMPLX_1:76;
py `1 <> 0
by A188, A189, A190, A191, A192, XREAL_1:64;
then
((((py `1) ^2) + ((py `2) ^2)) - 1) * ((py `1) ^2) = (py `2) ^2
by A194, XCMPLX_1:6, XCMPLX_1:87;
then A195:
(((py `1) ^2) - 1) * (((py `1) ^2) + ((py `2) ^2)) = 0
;
((py `1) ^2) + ((py `2) ^2) <> 0
by A191, COMPLEX1:1;
then
((py `1) - 1) * ((py `1) + 1) = 0
by A195, XCMPLX_1:6;
then
(
(py `1) - 1
= 0 or
(py `1) + 1
= 0 )
by XCMPLX_1:6;
hence
(
- 1
<= (ff . I) `2 &
(ff . I) `2 <= 1 )
by A188, A189, A193;
( - 1 <= (gg . O) `1 & (gg . O) `1 <= 1 & - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )
A196:
(
|[((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:52;
consider p3 being
Point of
(TOP-REAL 2) such that A197:
g . O = p3
and A198:
|.p3.| = 1
and A199:
p3 `2 <= p3 `1
and A200:
p3 `2 <= - (p3 `1)
by A1;
A201:
p3 <> 0. (TOP-REAL 2)
by A198, TOPRNS_1:23;
A202:
gg . O = (Sq_Circ ") . (g . O)
by A3, FUNCT_1:12;
then A203:
p3 = Sq_Circ . pz
by A197, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A204:
- (p3 `2) >= - (- (p3 `1))
by A200, XREAL_1:24;
then A205:
(Sq_Circ ") . p3 = |[((p3 `1) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))),((p3 `2) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2))))]|
by A199, A201, JGRAPH_3:30;
then A206:
pz `2 = (p3 `2) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))
by A202, A197, EUCLID:52;
A207:
pz `1 = (p3 `1) * (sqrt (1 + (((p3 `1) / (p3 `2)) ^2)))
by A202, A197, A205, EUCLID:52;
((p3 `1) / (p3 `2)) ^2 >= 0
by XREAL_1:63;
then A208:
sqrt (1 + (((p3 `1) / (p3 `2)) ^2)) > 0
by SQUARE_1:25;
( (
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 A199, A204, A208, XREAL_1:64;
then A210:
( (
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 A206, A207, A208, XREAL_1:64;
then A211:
( (
(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 A202, A197, A205, A206, A208, EUCLID:52, XREAL_1:64;
then
Sq_Circ . pz = |[((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))),((pz `2) / (sqrt (1 + (((pz `1) / (pz `2)) ^2))))]|
by A206, A207, A209, JGRAPH_2:3, JGRAPH_3:4;
then |.p3.| ^2 =
(((pz `2) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2)
by A203, A196, JGRAPH_3:1
.=
(((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) / (sqrt (1 + (((pz `1) / (pz `2)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((pz `2) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2)) + (((pz `1) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2))
by XCMPLX_1:76
.=
(((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / ((sqrt (1 + (((pz `1) / (pz `2)) ^2))) ^2))
by A180, SQUARE_1:def 2
.=
(((pz `2) ^2) / (1 + (((pz `1) / (pz `2)) ^2))) + (((pz `1) ^2) / (1 + (((pz `1) / (pz `2)) ^2)))
by A180, SQUARE_1:def 2
.=
(((pz `2) ^2) + ((pz `1) ^2)) / (1 + (((pz `1) / (pz `2)) ^2))
by XCMPLX_1:62
;
then
((((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 A198;
then
((pz `2) ^2) + ((pz `1) ^2) = 1
+ (((pz `1) / (pz `2)) ^2)
by A180, XCMPLX_1:87;
then A212:
(((pz `2) ^2) + ((pz `1) ^2)) - 1
= ((pz `1) ^2) / ((pz `2) ^2)
by XCMPLX_1:76;
pz `2 <> 0
by A206, A207, A208, A209, A210, XREAL_1:64;
then
((((pz `2) ^2) + ((pz `1) ^2)) - 1) * ((pz `2) ^2) = (pz `1) ^2
by A212, XCMPLX_1:6, XCMPLX_1:87;
then A213:
(((pz `2) ^2) - 1) * (((pz `2) ^2) + ((pz `1) ^2)) = 0
;
((pz `2) ^2) + ((pz `1) ^2) <> 0
by A209, COMPLEX1:1;
then
((pz `2) - 1) * ((pz `2) + 1) = 0
by A213, XCMPLX_1:6;
then
(
(pz `2) - 1
= 0 or
(pz `2) + 1
= 0 )
by XCMPLX_1:6;
hence
(
- 1
<= (gg . O) `1 &
(gg . O) `1 <= 1 )
by A206, A207, A211;
( - 1 <= (gg . I) `1 & (gg . I) `1 <= 1 )
A214:
(
|[((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:52;
A215:
((pu `1) / (pu `2)) ^2 >= 0
by XREAL_1:63;
consider p4 being
Point of
(TOP-REAL 2) such that A216:
g . I = p4
and A217:
|.p4.| = 1
and A218:
p4 `2 >= p4 `1
and A219:
p4 `2 >= - (p4 `1)
by A1;
A220:
- (p4 `2) <= - (- (p4 `1))
by A219, XREAL_1:24;
A221:
gg . I = (Sq_Circ ") . (g . I)
by A3, FUNCT_1:12;
then A222:
p4 = Sq_Circ . pu
by A216, FUNCT_1:32, JGRAPH_3:22, JGRAPH_3:43;
A223:
p4 <> 0. (TOP-REAL 2)
by A217, TOPRNS_1:23;
then A224:
(Sq_Circ ") . p4 = |[((p4 `1) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2)))),((p4 `2) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2))))]|
by A218, A220, JGRAPH_3:30;
then A225:
pu `2 = (p4 `2) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2)))
by A221, A216, EUCLID:52;
A226:
pu `1 = (p4 `1) * (sqrt (1 + (((p4 `1) / (p4 `2)) ^2)))
by A221, A216, A224, EUCLID:52;
((p4 `1) / (p4 `2)) ^2 >= 0
by XREAL_1:63;
then A227:
sqrt (1 + (((p4 `1) / (p4 `2)) ^2)) > 0
by SQUARE_1:25;
A229:
( (
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 A218, A220, A227, XREAL_1:64;
then A230:
( (
(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 A221, A216, A224, A225, A227, EUCLID:52, XREAL_1:64;
then
Sq_Circ . pu = |[((pu `1) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))),((pu `2) / (sqrt (1 + (((pu `1) / (pu `2)) ^2))))]|
by A225, A226, A228, JGRAPH_2:3, JGRAPH_3:4;
then |.p4.| ^2 =
(((pu `2) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))) ^2) + (((pu `1) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))) ^2)
by A222, A214, JGRAPH_3:1
.=
(((pu `2) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2)) + (((pu `1) / (sqrt (1 + (((pu `1) / (pu `2)) ^2)))) ^2)
by XCMPLX_1:76
.=
(((pu `2) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2)) + (((pu `1) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2))
by XCMPLX_1:76
.=
(((pu `2) ^2) / (1 + (((pu `1) / (pu `2)) ^2))) + (((pu `1) ^2) / ((sqrt (1 + (((pu `1) / (pu `2)) ^2))) ^2))
by A215, SQUARE_1:def 2
.=
(((pu `2) ^2) / (1 + (((pu `1) / (pu `2)) ^2))) + (((pu `1) ^2) / (1 + (((pu `1) / (pu `2)) ^2)))
by A215, SQUARE_1:def 2
.=
(((pu `2) ^2) + ((pu `1) ^2)) / (1 + (((pu `1) / (pu `2)) ^2))
by XCMPLX_1:62
;
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 A217;
then
((pu `2) ^2) + ((pu `1) ^2) = 1
+ (((pu `1) / (pu `2)) ^2)
by A215, XCMPLX_1:87;
then A231:
(((pu `2) ^2) + ((pu `1) ^2)) - 1
= ((pu `1) ^2) / ((pu `2) ^2)
by XCMPLX_1:76;
pu `2 <> 0
by A225, A226, A227, A228, A229, XREAL_1:64;
then
((((pu `2) ^2) + ((pu `1) ^2)) - 1) * ((pu `2) ^2) = (pu `1) ^2
by A231, XCMPLX_1:6, XCMPLX_1:87;
then A232:
(((pu `2) ^2) - 1) * (((pu `2) ^2) + ((pu `1) ^2)) = 0
;
((pu `2) ^2) + ((pu `1) ^2) <> 0
by A228, COMPLEX1:1;
then
((pu `2) - 1) * ((pu `2) + 1) = 0
by A232, XCMPLX_1:6;
then
(
(pu `2) - 1
= 0 or
(pu `2) + 1
= 0 )
by XCMPLX_1:6;
hence
(
- 1
<= (gg . I) `1 &
(gg . I) `1 <= 1 )
by A225, A226, A230;
verum
end;
then
rng ff meets rng gg
by A1, A5, A94, Th11, JGRAPH_3:22, JGRAPH_3:42;
then consider y being object such that
A233:
y in rng ff
and
A234:
y in rng gg
by XBOOLE_0:3;
consider x1 being object such that
A235:
x1 in dom ff
and
A236:
y = ff . x1
by A233, FUNCT_1:def 3;
consider x2 being object such that
A237:
x2 in dom gg
and
A238:
y = gg . x2
by A234, FUNCT_1:def 3;
A239:
( dom (Sq_Circ ") = the carrier of (TOP-REAL 2) & gg . x2 = (Sq_Circ ") . (g . x2) )
by A237, FUNCT_1:12, FUNCT_2:def 1, JGRAPH_3:29;
x1 in dom f
by A235, FUNCT_1:11;
then A240:
f . x1 in rng f
by FUNCT_1:def 3;
x2 in dom g
by A237, FUNCT_1:11;
then A241:
g . x2 in rng g
by FUNCT_1:def 3;
ff . x1 = (Sq_Circ ") . (f . x1)
by A235, FUNCT_1:12;
then
f . x1 = g . x2
by A236, A238, A240, A241, A239, FUNCT_1:def 4, JGRAPH_3:22;
hence
rng f meets rng g
by A240, A241, XBOOLE_0:3; verum