let C be Simple_closed_curve; for p being Point of (TOP-REAL 2) st W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C holds
not p in South_Arc C
let p be Point of (TOP-REAL 2); ( W-bound C < p `1 & p `1 < E-bound C & p in North_Arc C implies not p in South_Arc C )
reconsider p9 = p as Point of (Euclid 2) by EUCLID:22;
assume that
A1:
W-bound C < p `1
and
A2:
p `1 < E-bound C
and
A3:
p in North_Arc C
and
A4:
p in South_Arc C
; contradiction
set s = min (((p `1) - (W-bound C)),((E-bound C) - (p `1)));
A5:
W-bound C = (W-bound C) + 0
;
A6:
p `1 = (p `1) + 0
;
A7:
(p `1) - (W-bound C) > 0
by A1, A5, XREAL_1:20;
(E-bound C) - (p `1) > 0
by A2, A6, XREAL_1:20;
then A8:
min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) > 0
by A7, XXREAL_0:15;
now for r being Real st 0 < r & r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) holds
Ball (p9,r) meets Upper_Arc Clet r be
Real;
( 0 < r & r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) implies Ball (p9,r) meets Upper_Arc C )reconsider rr =
r as
Real ;
assume that A9:
0 < r
and A10:
r < min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
;
Ball (p9,r) meets Upper_Arc CA11:
r / 8
> 0
by A9, XREAL_1:139;
reconsider G =
Ball (
p9,
(r / 8)) as
a_neighborhood of
p by A9, GOBOARD6:2, XREAL_1:139;
consider k1 being
Nat such that A12:
for
m being
Nat st
m > k1 holds
(Upper_Appr C) . m meets G
by A3, KURATO_2:def 1;
consider k2 being
Nat such that A13:
for
m being
Nat st
m > k2 holds
(Lower_Appr C) . m meets G
by A4, KURATO_2:def 1;
reconsider k =
max (
k1,
k2) as
Nat by TARSKI:1;
A14:
k >= k1
by XXREAL_0:25;
set z9 =
max (
((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C)));
set z =
max (
(max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),
(r / 8));
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8) >= 1
by A11, XREAL_1:181, XXREAL_0:25;
then
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
>= log (2,1)
by PRE_FF:10;
then
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
>= 0
by POWER:51;
then reconsider m9 =
[\(log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))))/] as
Nat by INT_1:53;
A15:
2
to_power (m9 + 1) > 0
by POWER:34;
set N = 2
to_power (m9 + 1);
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
< (m9 + 1) * 1
by INT_1:29;
then
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
< (m9 + 1) * (log (2,2))
by POWER:52;
then
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
< log (2,
(2 to_power (m9 + 1)))
by POWER:55;
then
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8) < 2
to_power (m9 + 1)
by A15, PRE_FF:10;
then
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)) * (r / 8) < (2 to_power (m9 + 1)) * (r / 8)
by A11, XREAL_1:68;
then
max (
(max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),
(r / 8))
< (2 to_power (m9 + 1)) * (r / 8)
by A11, XCMPLX_1:87;
then
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < ((2 to_power (m9 + 1)) * (r / 8)) / (2 to_power (m9 + 1))
by A15, XREAL_1:74;
then
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < ((r / 8) / (2 to_power (m9 + 1))) * (2 to_power (m9 + 1))
;
then A16:
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < r / 8
by A15, XCMPLX_1:87;
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) >= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A15, XREAL_1:72, XXREAL_0:25;
then A17:
(max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) < r / 8
by A16, XXREAL_0:2;
reconsider W =
max (
k,
m9) as
Nat by TARSKI:1;
set m =
W + 1;
A18:
len (Gauge (C,(W + 1))) = width (Gauge (C,(W + 1)))
by JORDAN8:def 1;
max (
k,
m9)
>= k
by XXREAL_0:25;
then
max (
k,
m9)
>= k1
by A14, XXREAL_0:2;
then
W + 1
> k1
by NAT_1:13;
then
(Upper_Appr C) . (W + 1) meets G
by A12;
then
Upper_Arc (L~ (Cage (C,(W + 1)))) meets G
by Def1;
then consider p1 being
object such that A19:
p1 in Upper_Arc (L~ (Cage (C,(W + 1))))
and A20:
p1 in G
by XBOOLE_0:3;
reconsider p1 =
p1 as
Point of
(TOP-REAL 2) by A19;
reconsider p19 =
p1 as
Point of
(Euclid 2) by EUCLID:22;
set f =
Upper_Seq (
C,
(W + 1));
A21:
Upper_Arc (L~ (Cage (C,(W + 1)))) = L~ (Upper_Seq (C,(W + 1)))
by JORDAN1G:55;
then consider i1 being
Nat such that A22:
1
<= i1
and A23:
i1 + 1
<= len (Upper_Seq (C,(W + 1)))
and A24:
p1 in LSeg (
((Upper_Seq (C,(W + 1))) /. i1),
((Upper_Seq (C,(W + 1))) /. (i1 + 1)))
by A19, SPPOL_2:14;
reconsider c1 =
(Upper_Seq (C,(W + 1))) /. i1 as
Point of
(Euclid 2) by EUCLID:22;
reconsider c2 =
(Upper_Seq (C,(W + 1))) /. (i1 + 1) as
Point of
(Euclid 2) by EUCLID:22;
A25:
Upper_Seq (
C,
(W + 1))
is_sequence_on Gauge (
C,
(W + 1))
by JORDAN1G:4;
i1 < len (Upper_Seq (C,(W + 1)))
by A23, NAT_1:13;
then
i1 in Seg (len (Upper_Seq (C,(W + 1))))
by A22, FINSEQ_1:1;
then A26:
i1 in dom (Upper_Seq (C,(W + 1)))
by FINSEQ_1:def 3;
then consider ii1,
jj1 being
Nat such that A27:
[ii1,jj1] in Indices (Gauge (C,(W + 1)))
and A28:
(Upper_Seq (C,(W + 1))) /. i1 = (Gauge (C,(W + 1))) * (
ii1,
jj1)
by A25, GOBOARD1:def 9;
A29:
N-bound C > (S-bound C) + 0
by TOPREAL5:16;
A30:
E-bound C > (W-bound C) + 0
by TOPREAL5:17;
A31:
(N-bound C) - (S-bound C) > 0
by A29, XREAL_1:20;
A32:
(E-bound C) - (W-bound C) > 0
by A30, XREAL_1:20;
A33:
2
|^ (m9 + 1) > 0
by A15, POWER:41;
max (
k,
m9)
>= m9
by XXREAL_0:25;
then
W + 1
> m9
by NAT_1:13;
then
W + 1
>= m9 + 1
by NAT_1:13;
then A34:
2
|^ (W + 1) >= 2
|^ (m9 + 1)
by PREPOWER:93;
then A35:
((N-bound C) - (S-bound C)) / (2 |^ (W + 1)) <= ((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1))
by A31, A33, XREAL_1:118;
A36:
((E-bound C) - (W-bound C)) / (2 |^ (W + 1)) <= ((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1))
by A32, A33, A34, XREAL_1:118;
A37:
((N-bound C) - (S-bound C)) / (2 to_power (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A15, XREAL_1:72, XXREAL_0:25;
A38:
((E-bound C) - (W-bound C)) / (2 to_power (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A15, XREAL_1:72, XXREAL_0:25;
A39:
((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A37, POWER:41;
A40:
((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A38, POWER:41;
A41:
((N-bound C) - (S-bound C)) / (2 |^ (W + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A35, A39, XXREAL_0:2;
A42:
((E-bound C) - (W-bound C)) / (2 |^ (W + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A36, A40, XXREAL_0:2;
then
dist (
((Upper_Seq (C,(W + 1))) /. i1),
((Upper_Seq (C,(W + 1))) /. (i1 + 1)))
<= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A22, A23, A25, A41, Th6;
then
dist (
((Upper_Seq (C,(W + 1))) /. i1),
((Upper_Seq (C,(W + 1))) /. (i1 + 1)))
< r / 8
by A17, XXREAL_0:2;
then
dist (
c1,
c2)
< r / 8
by TOPREAL6:def 1;
then A43:
|.(((Upper_Seq (C,(W + 1))) /. i1) - ((Upper_Seq (C,(W + 1))) /. (i1 + 1))).| < r / 8
by SPPOL_1:39;
|.(p1 - ((Upper_Seq (C,(W + 1))) /. i1)).| <= |.(((Upper_Seq (C,(W + 1))) /. i1) - ((Upper_Seq (C,(W + 1))) /. (i1 + 1))).|
by A24, JGRAPH_1:36;
then A44:
|.(p1 - ((Upper_Seq (C,(W + 1))) /. i1)).| < r / 8
by A43, XXREAL_0:2;
dist (
p19,
p9)
< r / 8
by A20, METRIC_1:11;
then
|.(p - p1).| < r / 8
by SPPOL_1:39;
then A45:
|.(p - p1).| + |.(p1 - ((Upper_Seq (C,(W + 1))) /. i1)).| < (r / (2 * 4)) + (r / (2 * 4))
by A44, XREAL_1:8;
|.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| <= |.(p - p1).| + |.(p1 - ((Upper_Seq (C,(W + 1))) /. i1)).|
by TOPRNS_1:34;
then A46:
|.(p - ((Upper_Seq (C,(W + 1))) /. i1)).| < r / 4
by A45, XXREAL_0:2;
then A47:
dist (
p9,
c1)
< r / 4
by SPPOL_1:39;
then A48:
(Upper_Seq (C,(W + 1))) /. i1 in Ball (
p9,
(r / 4))
by METRIC_1:11;
A49:
(Upper_Seq (C,(W + 1))) /. i1 in Upper_Arc (L~ (Cage (C,(W + 1))))
by A21, A26, SPPOL_2:44;
A50:
k >= k2
by XXREAL_0:25;
max (
k,
m9)
>= k
by XXREAL_0:25;
then
max (
k,
m9)
>= k2
by A50, XXREAL_0:2;
then
W + 1
> k2
by NAT_1:13;
then
(Lower_Appr C) . (W + 1) meets G
by A13;
then
Lower_Arc (L~ (Cage (C,(W + 1)))) meets G
by Def2;
then consider p2 being
object such that A51:
p2 in Lower_Arc (L~ (Cage (C,(W + 1))))
and A52:
p2 in G
by XBOOLE_0:3;
reconsider p2 =
p2 as
Point of
(TOP-REAL 2) by A51;
reconsider p29 =
p2 as
Point of
(Euclid 2) by EUCLID:22;
set g =
Lower_Seq (
C,
(W + 1));
A53:
Lower_Arc (L~ (Cage (C,(W + 1)))) = L~ (Lower_Seq (C,(W + 1)))
by JORDAN1G:56;
then consider i2 being
Nat such that A54:
1
<= i2
and A55:
i2 + 1
<= len (Lower_Seq (C,(W + 1)))
and A56:
p2 in LSeg (
((Lower_Seq (C,(W + 1))) /. i2),
((Lower_Seq (C,(W + 1))) /. (i2 + 1)))
by A51, SPPOL_2:14;
reconsider d1 =
(Lower_Seq (C,(W + 1))) /. i2 as
Point of
(Euclid 2) by EUCLID:22;
reconsider d2 =
(Lower_Seq (C,(W + 1))) /. (i2 + 1) as
Point of
(Euclid 2) by EUCLID:22;
A57:
Lower_Seq (
C,
(W + 1))
is_sequence_on Gauge (
C,
(W + 1))
by JORDAN1G:5;
i2 < len (Lower_Seq (C,(W + 1)))
by A55, NAT_1:13;
then
i2 in Seg (len (Lower_Seq (C,(W + 1))))
by A54, FINSEQ_1:1;
then A58:
i2 in dom (Lower_Seq (C,(W + 1)))
by FINSEQ_1:def 3;
then consider ii2,
jj2 being
Nat such that A59:
[ii2,jj2] in Indices (Gauge (C,(W + 1)))
and A60:
(Lower_Seq (C,(W + 1))) /. i2 = (Gauge (C,(W + 1))) * (
ii2,
jj2)
by A57, GOBOARD1:def 9;
dist (
((Lower_Seq (C,(W + 1))) /. i2),
((Lower_Seq (C,(W + 1))) /. (i2 + 1)))
<= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A41, A42, A54, A55, A57, Th6;
then
dist (
((Lower_Seq (C,(W + 1))) /. i2),
((Lower_Seq (C,(W + 1))) /. (i2 + 1)))
< r / 8
by A17, XXREAL_0:2;
then
dist (
d1,
d2)
< r / 8
by TOPREAL6:def 1;
then A61:
|.(((Lower_Seq (C,(W + 1))) /. i2) - ((Lower_Seq (C,(W + 1))) /. (i2 + 1))).| < r / 8
by SPPOL_1:39;
|.(p2 - ((Lower_Seq (C,(W + 1))) /. i2)).| <= |.(((Lower_Seq (C,(W + 1))) /. i2) - ((Lower_Seq (C,(W + 1))) /. (i2 + 1))).|
by A56, JGRAPH_1:36;
then A62:
|.(p2 - ((Lower_Seq (C,(W + 1))) /. i2)).| < r / 8
by A61, XXREAL_0:2;
dist (
p29,
p9)
< r / 8
by A52, METRIC_1:11;
then
|.(p - p2).| < r / 8
by SPPOL_1:39;
then A63:
|.(p - p2).| + |.(p2 - ((Lower_Seq (C,(W + 1))) /. i2)).| < (r / (2 * 4)) + (r / (2 * 4))
by A62, XREAL_1:8;
|.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| <= |.(p - p2).| + |.(p2 - ((Lower_Seq (C,(W + 1))) /. i2)).|
by TOPRNS_1:34;
then A64:
|.(p - ((Lower_Seq (C,(W + 1))) /. i2)).| < r / 4
by A63, XXREAL_0:2;
then A65:
dist (
p9,
d1)
< r / 4
by SPPOL_1:39;
then A66:
(Lower_Seq (C,(W + 1))) /. i2 in Ball (
p9,
(r / 4))
by METRIC_1:11;
A67:
(Lower_Seq (C,(W + 1))) /. i2 in Lower_Arc (L~ (Cage (C,(W + 1))))
by A53, A58, SPPOL_2:44;
set Gij =
(Gauge (C,(W + 1))) * (
ii2,
jj1);
set Gji =
(Gauge (C,(W + 1))) * (
ii1,
jj2);
reconsider Gij9 =
(Gauge (C,(W + 1))) * (
ii2,
jj1),
Gji9 =
(Gauge (C,(W + 1))) * (
ii1,
jj2) as
Point of
(Euclid 2) by EUCLID:22;
A68:
1
<= ii1
by A27, MATRIX_0:32;
A69:
ii1 <= len (Gauge (C,(W + 1)))
by A27, MATRIX_0:32;
A70:
1
<= jj1
by A27, MATRIX_0:32;
A71:
jj1 <= width (Gauge (C,(W + 1)))
by A27, MATRIX_0:32;
A72:
1
<= ii2
by A59, MATRIX_0:32;
A73:
ii2 <= len (Gauge (C,(W + 1)))
by A59, MATRIX_0:32;
A74:
1
<= jj2
by A59, MATRIX_0:32;
A75:
jj2 <= width (Gauge (C,(W + 1)))
by A59, MATRIX_0:32;
A76:
len (Upper_Seq (C,(W + 1))) >= 3
by JORDAN1E:15;
A77:
len (Lower_Seq (C,(W + 1))) >= 3
by JORDAN1E:15;
A78:
len (Upper_Seq (C,(W + 1))) >= 1
by A76, XXREAL_0:2;
A79:
len (Lower_Seq (C,(W + 1))) >= 1
by A77, XXREAL_0:2;
A80:
len (Upper_Seq (C,(W + 1))) in Seg (len (Upper_Seq (C,(W + 1))))
by A78, FINSEQ_1:1;
A81:
len (Lower_Seq (C,(W + 1))) in Seg (len (Lower_Seq (C,(W + 1))))
by A79, FINSEQ_1:1;
A82:
len (Upper_Seq (C,(W + 1))) in dom (Upper_Seq (C,(W + 1)))
by A80, FINSEQ_1:def 3;
A83:
len (Lower_Seq (C,(W + 1))) in dom (Lower_Seq (C,(W + 1)))
by A81, FINSEQ_1:def 3;
A84:
r / 4
< r
by A9, XREAL_1:223;
A85:
r / 2
< r
by A9, XREAL_1:216;
A86:
min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
<= (p `1) - (W-bound C)
by XXREAL_0:17;
A87:
min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
<= (E-bound C) - (p `1)
by XXREAL_0:17;
A88:
now not 1 >= ii1assume
1
>= ii1
;
contradictionthen A89:
ii1 = 1
by A68, XXREAL_0:1;
dist (
p9,
c1)
< r
by A47, A84, XXREAL_0:2;
then
dist (
p9,
c1)
< min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
by A10, XXREAL_0:2;
then A90:
dist (
p9,
c1)
< (p `1) - (W-bound C)
by A86, XXREAL_0:2;
A91:
(p `1) - (((Upper_Seq (C,(W + 1))) /. i1) `1) <= |.((p `1) - (((Upper_Seq (C,(W + 1))) /. i1) `1)).|
by ABSVALUE:4;
|.((p `1) - (((Upper_Seq (C,(W + 1))) /. i1) `1)).| <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).|
by JGRAPH_1:34;
then
(p `1) - (((Upper_Seq (C,(W + 1))) /. i1) `1) <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).|
by A91, XXREAL_0:2;
then
(p `1) - (W-bound (L~ (Cage (C,(W + 1))))) <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).|
by A18, A28, A70, A71, A89, JORDAN1A:73;
then
(p `1) - (W-bound (L~ (Cage (C,(W + 1))))) <= dist (
p9,
c1)
by SPPOL_1:39;
then
(p `1) - (W-bound (L~ (Cage (C,(W + 1))))) < (p `1) - (W-bound C)
by A90, XXREAL_0:2;
then
W-bound (L~ (Cage (C,(W + 1)))) > W-bound C
by XREAL_1:13;
hence
contradiction
by Th11;
verum end; A92:
now not ii1 >= len (Gauge (C,(W + 1)))assume
ii1 >= len (Gauge (C,(W + 1)))
;
contradictionthen A93:
ii1 = len (Gauge (C,(W + 1)))
by A69, XXREAL_0:1;
((Gauge (C,(W + 1))) * ((len (Gauge (C,(W + 1)))),jj1)) `1 = E-bound (L~ (Cage (C,(W + 1))))
by A18, A70, A71, JORDAN1A:71;
then (Upper_Seq (C,(W + 1))) /. i1 =
E-max (L~ (Cage (C,(W + 1))))
by A21, A26, A28, A93, JORDAN1J:46, SPPOL_2:44
.=
(Upper_Seq (C,(W + 1))) /. (len (Upper_Seq (C,(W + 1))))
by JORDAN1F:7
;
then
i1 = len (Upper_Seq (C,(W + 1)))
by A26, A82, PARTFUN2:10;
hence
contradiction
by A23, NAT_1:13;
verum end; A94:
now not ii2 <= 1assume
ii2 <= 1
;
contradictionthen A95:
ii2 = 1
by A72, XXREAL_0:1;
((Gauge (C,(W + 1))) * (1,jj2)) `1 = W-bound (L~ (Cage (C,(W + 1))))
by A18, A74, A75, JORDAN1A:73;
then (Lower_Seq (C,(W + 1))) /. i2 =
W-min (L~ (Cage (C,(W + 1))))
by A53, A58, A60, A95, JORDAN1J:47, SPPOL_2:44
.=
(Lower_Seq (C,(W + 1))) /. (len (Lower_Seq (C,(W + 1))))
by JORDAN1F:8
;
then
i2 = len (Lower_Seq (C,(W + 1)))
by A58, A83, PARTFUN2:10;
hence
contradiction
by A55, NAT_1:13;
verum end; A96:
now not ii2 >= len (Gauge (C,(W + 1)))assume
ii2 >= len (Gauge (C,(W + 1)))
;
contradictionthen A97:
ii2 = len (Gauge (C,(W + 1)))
by A73, XXREAL_0:1;
dist (
p9,
d1)
< r
by A65, A84, XXREAL_0:2;
then
dist (
p9,
d1)
< min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
by A10, XXREAL_0:2;
then A98:
dist (
p9,
d1)
< (E-bound C) - (p `1)
by A87, XXREAL_0:2;
A99:
(((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1) <= |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).|
by ABSVALUE:4;
|.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= |.(((Lower_Seq (C,(W + 1))) /. i2) - p).|
by JGRAPH_1:34;
then
|.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).|
by TOPRNS_1:27;
then
(((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1) <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).|
by A99, XXREAL_0:2;
then
(E-bound (L~ (Cage (C,(W + 1))))) - (p `1) <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).|
by A18, A60, A74, A75, A97, JORDAN1A:71;
then
(E-bound (L~ (Cage (C,(W + 1))))) - (p `1) <= dist (
p9,
d1)
by SPPOL_1:39;
then
(E-bound (L~ (Cage (C,(W + 1))))) - (p `1) < (E-bound C) - (p `1)
by A98, XXREAL_0:2;
then
E-bound (L~ (Cage (C,(W + 1)))) < E-bound C
by XREAL_1:13;
hence
contradiction
by Th9;
verum end; A100:
Ball (
p9,
(rr / 4))
c= Ball (
p9,
rr)
by A84, PCOMPS_1:1;
A101:
((Gauge (C,(W + 1))) * (ii2,jj1)) `1 =
((Gauge (C,(W + 1))) * (ii2,1)) `1
by A70, A71, A72, A73, GOBOARD5:2
.=
((Lower_Seq (C,(W + 1))) /. i2) `1
by A60, A72, A73, A74, A75, GOBOARD5:2
;
A102:
((Gauge (C,(W + 1))) * (ii2,jj1)) `2 =
((Gauge (C,(W + 1))) * (1,jj1)) `2
by A70, A71, A72, A73, GOBOARD5:1
.=
((Upper_Seq (C,(W + 1))) /. i1) `2
by A28, A68, A69, A70, A71, GOBOARD5:1
;
A103:
((Gauge (C,(W + 1))) * (ii1,jj2)) `1 =
((Gauge (C,(W + 1))) * (ii1,1)) `1
by A68, A69, A74, A75, GOBOARD5:2
.=
((Upper_Seq (C,(W + 1))) /. i1) `1
by A28, A68, A69, A70, A71, GOBOARD5:2
;
A104:
((Gauge (C,(W + 1))) * (ii1,jj2)) `2 =
((Gauge (C,(W + 1))) * (1,jj2)) `2
by A68, A69, A74, A75, GOBOARD5:1
.=
((Lower_Seq (C,(W + 1))) /. i2) `2
by A60, A72, A73, A74, A75, GOBOARD5:1
;
A105:
|.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= |.(((Lower_Seq (C,(W + 1))) /. i2) - p).|
by JGRAPH_1:34;
A106:
|.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| <= |.(((Upper_Seq (C,(W + 1))) /. i1) - p).|
by JGRAPH_1:34;
A107:
|.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).|
by A105, TOPRNS_1:27;
A108:
|.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).|
by A106, TOPRNS_1:27;
A109:
|.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| <= r / 4
by A64, A107, XXREAL_0:2;
|.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| <= r / 4
by A46, A108, XXREAL_0:2;
then
|.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| <= (r / (2 * 2)) + (r / (2 * 2))
by A109, XREAL_1:7;
then A110:
|.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).| < r
by A85, XXREAL_0:2;
A111:
|.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| <= |.(((Upper_Seq (C,(W + 1))) /. i1) - p).|
by JGRAPH_1:34;
A112:
|.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| <= |.(((Lower_Seq (C,(W + 1))) /. i2) - p).|
by JGRAPH_1:34;
A113:
|.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| <= |.(p - ((Upper_Seq (C,(W + 1))) /. i1)).|
by A111, TOPRNS_1:27;
A114:
|.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| <= |.(p - ((Lower_Seq (C,(W + 1))) /. i2)).|
by A112, TOPRNS_1:27;
A115:
|.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| <= r / 4
by A46, A113, XXREAL_0:2;
|.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| <= r / 4
by A64, A114, XXREAL_0:2;
then
|.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| <= (r / (2 * 2)) + (r / (2 * 2))
by A115, XREAL_1:7;
then A116:
|.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).| < r
by A85, XXREAL_0:2;
|.(((Gauge (C,(W + 1))) * (ii2,jj1)) - p).| <= |.((((Lower_Seq (C,(W + 1))) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,(W + 1))) /. i1) `2) - (p `2)).|
by A101, A102, JGRAPH_1:32;
then
|.(((Gauge (C,(W + 1))) * (ii2,jj1)) - p).| < r
by A110, XXREAL_0:2;
then
dist (
Gij9,
p9)
< r
by SPPOL_1:39;
then A117:
(Gauge (C,(W + 1))) * (
ii2,
jj1)
in Ball (
p9,
r)
by METRIC_1:11;
|.(((Gauge (C,(W + 1))) * (ii1,jj2)) - p).| <= |.((((Upper_Seq (C,(W + 1))) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,(W + 1))) /. i2) `2) - (p `2)).|
by A103, A104, JGRAPH_1:32;
then
|.(((Gauge (C,(W + 1))) * (ii1,jj2)) - p).| < r
by A116, XXREAL_0:2;
then
dist (
Gji9,
p9)
< r
by SPPOL_1:39;
then A118:
(Gauge (C,(W + 1))) * (
ii1,
jj2)
in Ball (
p9,
r)
by METRIC_1:11;
A119:
LSeg (
((Lower_Seq (C,(W + 1))) /. i2),
((Gauge (C,(W + 1))) * (ii2,jj1)))
c= Ball (
p9,
rr)
by A66, A100, A117, TOPREAL3:21;
A120:
LSeg (
((Gauge (C,(W + 1))) * (ii2,jj1)),
((Upper_Seq (C,(W + 1))) /. i1))
c= Ball (
p9,
rr)
by A48, A100, A117, TOPREAL3:21;
A121:
LSeg (
((Lower_Seq (C,(W + 1))) /. i2),
((Gauge (C,(W + 1))) * (ii1,jj2)))
c= Ball (
p9,
rr)
by A66, A100, A118, TOPREAL3:21;
A122:
LSeg (
((Gauge (C,(W + 1))) * (ii1,jj2)),
((Upper_Seq (C,(W + 1))) /. i1))
c= Ball (
p9,
rr)
by A48, A100, A118, TOPREAL3:21;
now Ball (p9,r) meets Upper_Arc Cper cases
( jj2 <= jj1 or jj1 < jj2 )
;
suppose A123:
jj2 <= jj1
;
Ball (p9,r) meets Upper_Arc C
(LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1))) c= Ball (
p9,
r)
proof
let x be
object ;
TARSKI:def 3 ( not x in (LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1))) or x in Ball (p9,r) )
assume A124:
x in (LSeg (((Lower_Seq (C,(W + 1))) /. i2),((Gauge (C,(W + 1))) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii2,jj1)),((Upper_Seq (C,(W + 1))) /. i1)))
;
x in Ball (p9,r)
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
hence
x in Ball (
p9,
r)
;
verum
end; hence
Ball (
p9,
r)
meets Upper_Arc C
by A28, A49, A60, A67, A71, A74, A88, A92, A94, A96, A123, JORDAN15:48, XBOOLE_1:63;
verum end; suppose A125:
jj1 < jj2
;
Ball (p9,r) meets Upper_Arc C
(LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Gauge (C,(W + 1))) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Lower_Seq (C,(W + 1))) /. i2))) c= Ball (
p9,
r)
proof
let x be
object ;
TARSKI:def 3 ( not x in (LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Gauge (C,(W + 1))) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Lower_Seq (C,(W + 1))) /. i2))) or x in Ball (p9,r) )
assume A126:
x in (LSeg (((Upper_Seq (C,(W + 1))) /. i1),((Gauge (C,(W + 1))) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,(W + 1))) * (ii1,jj2)),((Lower_Seq (C,(W + 1))) /. i2)))
;
x in Ball (p9,r)
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
hence
x in Ball (
p9,
r)
;
verum
end; hence
Ball (
p9,
r)
meets Upper_Arc C
by A28, A49, A60, A67, A70, A75, A88, A92, A94, A96, A125, Th25, XBOOLE_1:63;
verum end; hence
Ball (
p9,
r)
meets Upper_Arc C
;
verum end;
then
p in Cl (Upper_Arc C)
by A8, GOBOARD6:93;
then A127:
p in Upper_Arc C
by PRE_TOPC:22;
now for r being Real st 0 < r & r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) holds
Ball (p9,r) meets Lower_Arc Clet r be
Real;
( 0 < r & r < min (((p `1) - (W-bound C)),((E-bound C) - (p `1))) implies Ball (p9,r) meets Lower_Arc C )reconsider rr =
r as
Real ;
assume that A128:
0 < r
and A129:
r < min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
;
Ball (p9,r) meets Lower_Arc CA130:
r / 8
> 0
by A128, XREAL_1:139;
reconsider G =
Ball (
p9,
(r / 8)) as
a_neighborhood of
p by A128, GOBOARD6:2, XREAL_1:139;
consider k1 being
Nat such that A131:
for
m being
Nat st
m > k1 holds
(Upper_Appr C) . m meets G
by A3, KURATO_2:def 1;
consider k2 being
Nat such that A132:
for
m being
Nat st
m > k2 holds
(Lower_Appr C) . m meets G
by A4, KURATO_2:def 1;
set k =
max (
k1,
k2);
A133:
max (
k1,
k2)
>= k1
by XXREAL_0:25;
set z9 =
max (
((N-bound C) - (S-bound C)),
((E-bound C) - (W-bound C)));
set z =
max (
(max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),
(r / 8));
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8) >= 1
by A130, XREAL_1:181, XXREAL_0:25;
then
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
>= log (2,1)
by PRE_FF:10;
then
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
>= 0
by POWER:51;
then reconsider m9 =
[\(log (2,((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8))))/] as
Nat by INT_1:53;
A134:
2
to_power (m9 + 1) > 0
by POWER:34;
set N = 2
to_power (m9 + 1);
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
< (m9 + 1) * 1
by INT_1:29;
then
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
< (m9 + 1) * (log (2,2))
by POWER:52;
then
log (2,
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)))
< log (2,
(2 to_power (m9 + 1)))
by POWER:55;
then
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8) < 2
to_power (m9 + 1)
by A134, PRE_FF:10;
then
((max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (r / 8)) * (r / 8) < (2 to_power (m9 + 1)) * (r / 8)
by A130, XREAL_1:68;
then
max (
(max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),
(r / 8))
< (2 to_power (m9 + 1)) * (r / 8)
by A130, XCMPLX_1:87;
then
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < ((2 to_power (m9 + 1)) * (r / 8)) / (2 to_power (m9 + 1))
by A134, XREAL_1:74;
then
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < ((r / 8) / (2 to_power (m9 + 1))) * (2 to_power (m9 + 1))
;
then A135:
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) < r / 8
by A134, XCMPLX_1:87;
(max ((max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))),(r / 8))) / (2 to_power (m9 + 1)) >= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A134, XREAL_1:72, XXREAL_0:25;
then A136:
(max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1)) < r / 8
by A135, XXREAL_0:2;
reconsider W =
max (
(max (k1,k2)),
m9) as
Nat by TARSKI:1;
set m =
W + 1;
reconsider m =
W + 1 as
Nat ;
A137:
len (Gauge (C,m)) = width (Gauge (C,m))
by JORDAN8:def 1;
max (
(max (k1,k2)),
m9)
>= max (
k1,
k2)
by XXREAL_0:25;
then
max (
(max (k1,k2)),
m9)
>= k1
by A133, XXREAL_0:2;
then
m > k1
by NAT_1:13;
then
(Upper_Appr C) . m meets G
by A131;
then
Upper_Arc (L~ (Cage (C,m))) meets G
by Def1;
then consider p1 being
object such that A138:
p1 in Upper_Arc (L~ (Cage (C,m)))
and A139:
p1 in G
by XBOOLE_0:3;
reconsider p1 =
p1 as
Point of
(TOP-REAL 2) by A138;
reconsider p19 =
p1 as
Point of
(Euclid 2) by EUCLID:22;
set f =
Upper_Seq (
C,
m);
A140:
Upper_Arc (L~ (Cage (C,m))) = L~ (Upper_Seq (C,m))
by JORDAN1G:55;
then consider i1 being
Nat such that A141:
1
<= i1
and A142:
i1 + 1
<= len (Upper_Seq (C,m))
and A143:
p1 in LSeg (
((Upper_Seq (C,m)) /. i1),
((Upper_Seq (C,m)) /. (i1 + 1)))
by A138, SPPOL_2:14;
reconsider c1 =
(Upper_Seq (C,m)) /. i1 as
Point of
(Euclid 2) by EUCLID:22;
reconsider c2 =
(Upper_Seq (C,m)) /. (i1 + 1) as
Point of
(Euclid 2) by EUCLID:22;
A144:
Upper_Seq (
C,
m)
is_sequence_on Gauge (
C,
m)
by JORDAN1G:4;
i1 < len (Upper_Seq (C,m))
by A142, NAT_1:13;
then
i1 in Seg (len (Upper_Seq (C,m)))
by A141, FINSEQ_1:1;
then A145:
i1 in dom (Upper_Seq (C,m))
by FINSEQ_1:def 3;
then consider ii1,
jj1 being
Nat such that A146:
[ii1,jj1] in Indices (Gauge (C,m))
and A147:
(Upper_Seq (C,m)) /. i1 = (Gauge (C,m)) * (
ii1,
jj1)
by A144, GOBOARD1:def 9;
A148:
N-bound C > (S-bound C) + 0
by TOPREAL5:16;
A149:
E-bound C > (W-bound C) + 0
by TOPREAL5:17;
A150:
(N-bound C) - (S-bound C) > 0
by A148, XREAL_1:20;
A151:
(E-bound C) - (W-bound C) > 0
by A149, XREAL_1:20;
A152:
2
|^ (m9 + 1) > 0
by A134, POWER:41;
max (
(max (k1,k2)),
m9)
>= m9
by XXREAL_0:25;
then
m > m9
by NAT_1:13;
then
m >= m9 + 1
by NAT_1:13;
then A153:
2
|^ m >= 2
|^ (m9 + 1)
by PREPOWER:93;
then A154:
((N-bound C) - (S-bound C)) / (2 |^ m) <= ((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1))
by A150, A152, XREAL_1:118;
A155:
((E-bound C) - (W-bound C)) / (2 |^ m) <= ((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1))
by A151, A152, A153, XREAL_1:118;
A156:
((N-bound C) - (S-bound C)) / (2 to_power (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A134, XREAL_1:72, XXREAL_0:25;
A157:
((E-bound C) - (W-bound C)) / (2 to_power (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A134, XREAL_1:72, XXREAL_0:25;
A158:
((N-bound C) - (S-bound C)) / (2 |^ (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A156, POWER:41;
A159:
((E-bound C) - (W-bound C)) / (2 |^ (m9 + 1)) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A157, POWER:41;
A160:
((N-bound C) - (S-bound C)) / (2 |^ m) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A154, A158, XXREAL_0:2;
A161:
((E-bound C) - (W-bound C)) / (2 |^ m) <= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A155, A159, XXREAL_0:2;
then
dist (
((Upper_Seq (C,m)) /. i1),
((Upper_Seq (C,m)) /. (i1 + 1)))
<= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A141, A142, A144, A160, Th6;
then
dist (
((Upper_Seq (C,m)) /. i1),
((Upper_Seq (C,m)) /. (i1 + 1)))
< r / 8
by A136, XXREAL_0:2;
then
dist (
c1,
c2)
< r / 8
by TOPREAL6:def 1;
then A162:
|.(((Upper_Seq (C,m)) /. i1) - ((Upper_Seq (C,m)) /. (i1 + 1))).| < r / 8
by SPPOL_1:39;
|.(p1 - ((Upper_Seq (C,m)) /. i1)).| <= |.(((Upper_Seq (C,m)) /. i1) - ((Upper_Seq (C,m)) /. (i1 + 1))).|
by A143, JGRAPH_1:36;
then A163:
|.(p1 - ((Upper_Seq (C,m)) /. i1)).| < r / 8
by A162, XXREAL_0:2;
dist (
p19,
p9)
< r / 8
by A139, METRIC_1:11;
then
|.(p - p1).| < r / 8
by SPPOL_1:39;
then A164:
|.(p - p1).| + |.(p1 - ((Upper_Seq (C,m)) /. i1)).| < (r / (2 * 4)) + (r / (2 * 4))
by A163, XREAL_1:8;
|.(p - ((Upper_Seq (C,m)) /. i1)).| <= |.(p - p1).| + |.(p1 - ((Upper_Seq (C,m)) /. i1)).|
by TOPRNS_1:34;
then A165:
|.(p - ((Upper_Seq (C,m)) /. i1)).| < r / 4
by A164, XXREAL_0:2;
then A166:
dist (
p9,
c1)
< r / 4
by SPPOL_1:39;
then A167:
(Upper_Seq (C,m)) /. i1 in Ball (
p9,
(r / 4))
by METRIC_1:11;
A168:
(Upper_Seq (C,m)) /. i1 in Upper_Arc (L~ (Cage (C,m)))
by A140, A145, SPPOL_2:44;
A169:
max (
k1,
k2)
>= k2
by XXREAL_0:25;
max (
(max (k1,k2)),
m9)
>= max (
k1,
k2)
by XXREAL_0:25;
then
max (
(max (k1,k2)),
m9)
>= k2
by A169, XXREAL_0:2;
then
m > k2
by NAT_1:13;
then
(Lower_Appr C) . m meets G
by A132;
then
Lower_Arc (L~ (Cage (C,m))) meets G
by Def2;
then consider p2 being
object such that A170:
p2 in Lower_Arc (L~ (Cage (C,m)))
and A171:
p2 in G
by XBOOLE_0:3;
reconsider p2 =
p2 as
Point of
(TOP-REAL 2) by A170;
reconsider p29 =
p2 as
Point of
(Euclid 2) by EUCLID:22;
set g =
Lower_Seq (
C,
m);
A172:
Lower_Arc (L~ (Cage (C,m))) = L~ (Lower_Seq (C,m))
by JORDAN1G:56;
then consider i2 being
Nat such that A173:
1
<= i2
and A174:
i2 + 1
<= len (Lower_Seq (C,m))
and A175:
p2 in LSeg (
((Lower_Seq (C,m)) /. i2),
((Lower_Seq (C,m)) /. (i2 + 1)))
by A170, SPPOL_2:14;
reconsider d1 =
(Lower_Seq (C,m)) /. i2 as
Point of
(Euclid 2) by EUCLID:22;
reconsider d2 =
(Lower_Seq (C,m)) /. (i2 + 1) as
Point of
(Euclid 2) by EUCLID:22;
A176:
Lower_Seq (
C,
m)
is_sequence_on Gauge (
C,
m)
by JORDAN1G:5;
i2 < len (Lower_Seq (C,m))
by A174, NAT_1:13;
then
i2 in Seg (len (Lower_Seq (C,m)))
by A173, FINSEQ_1:1;
then A177:
i2 in dom (Lower_Seq (C,m))
by FINSEQ_1:def 3;
then consider ii2,
jj2 being
Nat such that A178:
[ii2,jj2] in Indices (Gauge (C,m))
and A179:
(Lower_Seq (C,m)) /. i2 = (Gauge (C,m)) * (
ii2,
jj2)
by A176, GOBOARD1:def 9;
dist (
((Lower_Seq (C,m)) /. i2),
((Lower_Seq (C,m)) /. (i2 + 1)))
<= (max (((N-bound C) - (S-bound C)),((E-bound C) - (W-bound C)))) / (2 to_power (m9 + 1))
by A160, A161, A173, A174, A176, Th6;
then
dist (
((Lower_Seq (C,m)) /. i2),
((Lower_Seq (C,m)) /. (i2 + 1)))
< r / 8
by A136, XXREAL_0:2;
then
dist (
d1,
d2)
< r / 8
by TOPREAL6:def 1;
then A180:
|.(((Lower_Seq (C,m)) /. i2) - ((Lower_Seq (C,m)) /. (i2 + 1))).| < r / 8
by SPPOL_1:39;
|.(p2 - ((Lower_Seq (C,m)) /. i2)).| <= |.(((Lower_Seq (C,m)) /. i2) - ((Lower_Seq (C,m)) /. (i2 + 1))).|
by A175, JGRAPH_1:36;
then A181:
|.(p2 - ((Lower_Seq (C,m)) /. i2)).| < r / 8
by A180, XXREAL_0:2;
dist (
p29,
p9)
< r / 8
by A171, METRIC_1:11;
then
|.(p - p2).| < r / 8
by SPPOL_1:39;
then A182:
|.(p - p2).| + |.(p2 - ((Lower_Seq (C,m)) /. i2)).| < (r / (2 * 4)) + (r / (2 * 4))
by A181, XREAL_1:8;
|.(p - ((Lower_Seq (C,m)) /. i2)).| <= |.(p - p2).| + |.(p2 - ((Lower_Seq (C,m)) /. i2)).|
by TOPRNS_1:34;
then A183:
|.(p - ((Lower_Seq (C,m)) /. i2)).| < r / 4
by A182, XXREAL_0:2;
then A184:
dist (
p9,
d1)
< r / 4
by SPPOL_1:39;
then A185:
(Lower_Seq (C,m)) /. i2 in Ball (
p9,
(r / 4))
by METRIC_1:11;
A186:
(Lower_Seq (C,m)) /. i2 in Lower_Arc (L~ (Cage (C,m)))
by A172, A177, SPPOL_2:44;
set Gij =
(Gauge (C,m)) * (
ii2,
jj1);
set Gji =
(Gauge (C,m)) * (
ii1,
jj2);
reconsider Gij9 =
(Gauge (C,m)) * (
ii2,
jj1),
Gji9 =
(Gauge (C,m)) * (
ii1,
jj2) as
Point of
(Euclid 2) by EUCLID:22;
A187:
1
<= ii1
by A146, MATRIX_0:32;
A188:
ii1 <= len (Gauge (C,m))
by A146, MATRIX_0:32;
A189:
1
<= jj1
by A146, MATRIX_0:32;
A190:
jj1 <= width (Gauge (C,m))
by A146, MATRIX_0:32;
A191:
1
<= ii2
by A178, MATRIX_0:32;
A192:
ii2 <= len (Gauge (C,m))
by A178, MATRIX_0:32;
A193:
1
<= jj2
by A178, MATRIX_0:32;
A194:
jj2 <= width (Gauge (C,m))
by A178, MATRIX_0:32;
A195:
len (Upper_Seq (C,m)) >= 3
by JORDAN1E:15;
A196:
len (Lower_Seq (C,m)) >= 3
by JORDAN1E:15;
A197:
len (Upper_Seq (C,m)) >= 1
by A195, XXREAL_0:2;
A198:
len (Lower_Seq (C,m)) >= 1
by A196, XXREAL_0:2;
A199:
len (Upper_Seq (C,m)) in Seg (len (Upper_Seq (C,m)))
by A197, FINSEQ_1:1;
A200:
len (Lower_Seq (C,m)) in Seg (len (Lower_Seq (C,m)))
by A198, FINSEQ_1:1;
A201:
len (Upper_Seq (C,m)) in dom (Upper_Seq (C,m))
by A199, FINSEQ_1:def 3;
A202:
len (Lower_Seq (C,m)) in dom (Lower_Seq (C,m))
by A200, FINSEQ_1:def 3;
A203:
r / 4
< r
by A128, XREAL_1:223;
A204:
r / 2
< r
by A128, XREAL_1:216;
A205:
min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
<= (p `1) - (W-bound C)
by XXREAL_0:17;
A206:
min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
<= (E-bound C) - (p `1)
by XXREAL_0:17;
A207:
now not 1 >= ii1assume
1
>= ii1
;
contradictionthen A208:
ii1 = 1
by A187, XXREAL_0:1;
dist (
p9,
c1)
< r
by A166, A203, XXREAL_0:2;
then
dist (
p9,
c1)
< min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
by A129, XXREAL_0:2;
then A209:
dist (
p9,
c1)
< (p `1) - (W-bound C)
by A205, XXREAL_0:2;
A210:
(p `1) - (((Upper_Seq (C,m)) /. i1) `1) <= |.((p `1) - (((Upper_Seq (C,m)) /. i1) `1)).|
by ABSVALUE:4;
|.((p `1) - (((Upper_Seq (C,m)) /. i1) `1)).| <= |.(p - ((Upper_Seq (C,m)) /. i1)).|
by JGRAPH_1:34;
then
(p `1) - (((Upper_Seq (C,m)) /. i1) `1) <= |.(p - ((Upper_Seq (C,m)) /. i1)).|
by A210, XXREAL_0:2;
then
(p `1) - (W-bound (L~ (Cage (C,m)))) <= |.(p - ((Upper_Seq (C,m)) /. i1)).|
by A137, A147, A189, A190, A208, JORDAN1A:73;
then
(p `1) - (W-bound (L~ (Cage (C,m)))) <= dist (
p9,
c1)
by SPPOL_1:39;
then
(p `1) - (W-bound (L~ (Cage (C,m)))) < (p `1) - (W-bound C)
by A209, XXREAL_0:2;
then
W-bound (L~ (Cage (C,m))) > W-bound C
by XREAL_1:13;
hence
contradiction
by Th11;
verum end; A211:
now not ii1 >= len (Gauge (C,m))assume
ii1 >= len (Gauge (C,m))
;
contradictionthen A212:
ii1 = len (Gauge (C,m))
by A188, XXREAL_0:1;
((Gauge (C,m)) * ((len (Gauge (C,m))),jj1)) `1 = E-bound (L~ (Cage (C,m)))
by A137, A189, A190, JORDAN1A:71;
then (Upper_Seq (C,m)) /. i1 =
E-max (L~ (Cage (C,m)))
by A140, A145, A147, A212, JORDAN1J:46, SPPOL_2:44
.=
(Upper_Seq (C,m)) /. (len (Upper_Seq (C,m)))
by JORDAN1F:7
;
then
i1 = len (Upper_Seq (C,m))
by A145, A201, PARTFUN2:10;
hence
contradiction
by A142, NAT_1:13;
verum end; A213:
now not ii2 <= 1assume
ii2 <= 1
;
contradictionthen A214:
ii2 = 1
by A191, XXREAL_0:1;
((Gauge (C,m)) * (1,jj2)) `1 = W-bound (L~ (Cage (C,m)))
by A137, A193, A194, JORDAN1A:73;
then (Lower_Seq (C,m)) /. i2 =
W-min (L~ (Cage (C,m)))
by A172, A177, A179, A214, JORDAN1J:47, SPPOL_2:44
.=
(Lower_Seq (C,m)) /. (len (Lower_Seq (C,m)))
by JORDAN1F:8
;
then
i2 = len (Lower_Seq (C,m))
by A177, A202, PARTFUN2:10;
hence
contradiction
by A174, NAT_1:13;
verum end; A215:
now not ii2 >= len (Gauge (C,m))assume
ii2 >= len (Gauge (C,m))
;
contradictionthen A216:
ii2 = len (Gauge (C,m))
by A192, XXREAL_0:1;
dist (
p9,
d1)
< r
by A184, A203, XXREAL_0:2;
then
dist (
p9,
d1)
< min (
((p `1) - (W-bound C)),
((E-bound C) - (p `1)))
by A129, XXREAL_0:2;
then A217:
dist (
p9,
d1)
< (E-bound C) - (p `1)
by A206, XXREAL_0:2;
A218:
(((Lower_Seq (C,m)) /. i2) `1) - (p `1) <= |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).|
by ABSVALUE:4;
|.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= |.(((Lower_Seq (C,m)) /. i2) - p).|
by JGRAPH_1:34;
then
|.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= |.(p - ((Lower_Seq (C,m)) /. i2)).|
by TOPRNS_1:27;
then
(((Lower_Seq (C,m)) /. i2) `1) - (p `1) <= |.(p - ((Lower_Seq (C,m)) /. i2)).|
by A218, XXREAL_0:2;
then
(E-bound (L~ (Cage (C,m)))) - (p `1) <= |.(p - ((Lower_Seq (C,m)) /. i2)).|
by A137, A179, A193, A194, A216, JORDAN1A:71;
then
(E-bound (L~ (Cage (C,m)))) - (p `1) <= dist (
p9,
d1)
by SPPOL_1:39;
then
(E-bound (L~ (Cage (C,m)))) - (p `1) < (E-bound C) - (p `1)
by A217, XXREAL_0:2;
then
E-bound (L~ (Cage (C,m))) < E-bound C
by XREAL_1:13;
hence
contradiction
by Th9;
verum end; A219:
Ball (
p9,
(rr / 4))
c= Ball (
p9,
rr)
by A203, PCOMPS_1:1;
A220:
((Gauge (C,m)) * (ii2,jj1)) `1 =
((Gauge (C,m)) * (ii2,1)) `1
by A189, A190, A191, A192, GOBOARD5:2
.=
((Lower_Seq (C,m)) /. i2) `1
by A179, A191, A192, A193, A194, GOBOARD5:2
;
A221:
((Gauge (C,m)) * (ii2,jj1)) `2 =
((Gauge (C,m)) * (1,jj1)) `2
by A189, A190, A191, A192, GOBOARD5:1
.=
((Upper_Seq (C,m)) /. i1) `2
by A147, A187, A188, A189, A190, GOBOARD5:1
;
A222:
((Gauge (C,m)) * (ii1,jj2)) `1 =
((Gauge (C,m)) * (ii1,1)) `1
by A187, A188, A193, A194, GOBOARD5:2
.=
((Upper_Seq (C,m)) /. i1) `1
by A147, A187, A188, A189, A190, GOBOARD5:2
;
A223:
((Gauge (C,m)) * (ii1,jj2)) `2 =
((Gauge (C,m)) * (1,jj2)) `2
by A187, A188, A193, A194, GOBOARD5:1
.=
((Lower_Seq (C,m)) /. i2) `2
by A179, A191, A192, A193, A194, GOBOARD5:1
;
A224:
|.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= |.(((Lower_Seq (C,m)) /. i2) - p).|
by JGRAPH_1:34;
A225:
|.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| <= |.(((Upper_Seq (C,m)) /. i1) - p).|
by JGRAPH_1:34;
A226:
|.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= |.(p - ((Lower_Seq (C,m)) /. i2)).|
by A224, TOPRNS_1:27;
A227:
|.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| <= |.(p - ((Upper_Seq (C,m)) /. i1)).|
by A225, TOPRNS_1:27;
A228:
|.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| <= r / 4
by A183, A226, XXREAL_0:2;
|.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| <= r / 4
by A165, A227, XXREAL_0:2;
then
|.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| <= (r / (2 * 2)) + (r / (2 * 2))
by A228, XREAL_1:7;
then A229:
|.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).| < r
by A204, XXREAL_0:2;
A230:
|.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| <= |.(((Upper_Seq (C,m)) /. i1) - p).|
by JGRAPH_1:34;
A231:
|.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| <= |.(((Lower_Seq (C,m)) /. i2) - p).|
by JGRAPH_1:34;
A232:
|.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| <= |.(p - ((Upper_Seq (C,m)) /. i1)).|
by A230, TOPRNS_1:27;
A233:
|.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| <= |.(p - ((Lower_Seq (C,m)) /. i2)).|
by A231, TOPRNS_1:27;
A234:
|.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| <= r / 4
by A165, A232, XXREAL_0:2;
|.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| <= r / 4
by A183, A233, XXREAL_0:2;
then
|.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| <= (r / (2 * 2)) + (r / (2 * 2))
by A234, XREAL_1:7;
then A235:
|.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).| < r
by A204, XXREAL_0:2;
|.(((Gauge (C,m)) * (ii2,jj1)) - p).| <= |.((((Lower_Seq (C,m)) /. i2) `1) - (p `1)).| + |.((((Upper_Seq (C,m)) /. i1) `2) - (p `2)).|
by A220, A221, JGRAPH_1:32;
then
|.(((Gauge (C,m)) * (ii2,jj1)) - p).| < r
by A229, XXREAL_0:2;
then
dist (
Gij9,
p9)
< r
by SPPOL_1:39;
then A236:
(Gauge (C,m)) * (
ii2,
jj1)
in Ball (
p9,
r)
by METRIC_1:11;
|.(((Gauge (C,m)) * (ii1,jj2)) - p).| <= |.((((Upper_Seq (C,m)) /. i1) `1) - (p `1)).| + |.((((Lower_Seq (C,m)) /. i2) `2) - (p `2)).|
by A222, A223, JGRAPH_1:32;
then
|.(((Gauge (C,m)) * (ii1,jj2)) - p).| < r
by A235, XXREAL_0:2;
then
dist (
Gji9,
p9)
< r
by SPPOL_1:39;
then A237:
(Gauge (C,m)) * (
ii1,
jj2)
in Ball (
p9,
r)
by METRIC_1:11;
A238:
LSeg (
((Lower_Seq (C,m)) /. i2),
((Gauge (C,m)) * (ii2,jj1)))
c= Ball (
p9,
rr)
by A185, A219, A236, TOPREAL3:21;
A239:
LSeg (
((Gauge (C,m)) * (ii2,jj1)),
((Upper_Seq (C,m)) /. i1))
c= Ball (
p9,
rr)
by A167, A219, A236, TOPREAL3:21;
A240:
LSeg (
((Lower_Seq (C,m)) /. i2),
((Gauge (C,m)) * (ii1,jj2)))
c= Ball (
p9,
rr)
by A185, A219, A237, TOPREAL3:21;
A241:
LSeg (
((Gauge (C,m)) * (ii1,jj2)),
((Upper_Seq (C,m)) /. i1))
c= Ball (
p9,
rr)
by A167, A219, A237, TOPREAL3:21;
now Ball (p9,r) meets Lower_Arc Cper cases
( jj2 <= jj1 or jj1 < jj2 )
;
suppose A242:
jj2 <= jj1
;
Ball (p9,r) meets Lower_Arc C
(LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1))) c= Ball (
p9,
r)
proof
let x be
object ;
TARSKI:def 3 ( not x in (LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1))) or x in Ball (p9,r) )
assume A243:
x in (LSeg (((Lower_Seq (C,m)) /. i2),((Gauge (C,m)) * (ii2,jj1)))) \/ (LSeg (((Gauge (C,m)) * (ii2,jj1)),((Upper_Seq (C,m)) /. i1)))
;
x in Ball (p9,r)
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
hence
x in Ball (
p9,
r)
;
verum
end; hence
Ball (
p9,
r)
meets Lower_Arc C
by A147, A168, A179, A186, A190, A193, A207, A211, A213, A215, A242, JORDAN15:49, XBOOLE_1:63;
verum end; suppose A244:
jj1 < jj2
;
Ball (p9,r) meets Lower_Arc C
(LSeg (((Upper_Seq (C,m)) /. i1),((Gauge (C,m)) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,m)) * (ii1,jj2)),((Lower_Seq (C,m)) /. i2))) c= Ball (
p9,
r)
proof
let x be
object ;
TARSKI:def 3 ( not x in (LSeg (((Upper_Seq (C,m)) /. i1),((Gauge (C,m)) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,m)) * (ii1,jj2)),((Lower_Seq (C,m)) /. i2))) or x in Ball (p9,r) )
assume A245:
x in (LSeg (((Upper_Seq (C,m)) /. i1),((Gauge (C,m)) * (ii1,jj2)))) \/ (LSeg (((Gauge (C,m)) * (ii1,jj2)),((Lower_Seq (C,m)) /. i2)))
;
x in Ball (p9,r)
then reconsider x9 =
x as
Point of
(TOP-REAL 2) ;
hence
x in Ball (
p9,
r)
;
verum
end; hence
Ball (
p9,
r)
meets Lower_Arc C
by A147, A168, A179, A186, A189, A194, A207, A211, A213, A215, A244, Th24, XBOOLE_1:63;
verum end; hence
Ball (
p9,
r)
meets Lower_Arc C
;
verum end;
then
p in Cl (Lower_Arc C)
by A8, GOBOARD6:93;
then
p in Lower_Arc C
by PRE_TOPC:22;
then
p in (Upper_Arc C) /\ (Lower_Arc C)
by A127, XBOOLE_0:def 4;
then
p in {(W-min C),(E-max C)}
by JORDAN6:50;
then
( p = W-min C or p = E-max C )
by TARSKI:def 2;
hence
contradiction
by A1, A2, EUCLID:52; verum