let C be Simple_closed_curve; for p being Point of (TOP-REAL 2) st p in BDD C holds
ex n, i, j being Element of NAT st
( 1 < i & i < len (Gauge C,n) & 1 < j & j < width (Gauge C,n) & p `1 <> ((Gauge C,n) * i,j) `1 & p in cell (Gauge C,n),i,j & cell (Gauge C,n),i,j c= BDD C )
let p be Point of (TOP-REAL 2); ( p in BDD C implies ex n, i, j being Element of NAT st
( 1 < i & i < len (Gauge C,n) & 1 < j & j < width (Gauge C,n) & p `1 <> ((Gauge C,n) * i,j) `1 & p in cell (Gauge C,n),i,j & cell (Gauge C,n),i,j c= BDD C ) )
reconsider P = p as Point of (Euclid 2) by Lm3;
set W = W-bound C;
set E = E-bound C;
set S = S-bound C;
set N = N-bound C;
set EW = (E-bound C) - (W-bound C);
set NS = (N-bound C) - (S-bound C);
assume A1:
p in BDD C
; ex n, i, j being Element of NAT st
( 1 < i & i < len (Gauge C,n) & 1 < j & j < width (Gauge C,n) & p `1 <> ((Gauge C,n) * i,j) `1 & p in cell (Gauge C,n),i,j & cell (Gauge C,n),i,j c= BDD C )
then consider r being Real such that
A2:
r > 0
and
A3:
Ball P,r c= BDD C
by Th29;
set l = r / 4;
r / 4 > 0
by A2, XREAL_1:141;
then consider n being Element of NAT such that
1 < n
and
A4:
dist ((Gauge C,n) * 1,1),((Gauge C,n) * 1,2) < r / 4
and
A5:
dist ((Gauge C,n) * 1,1),((Gauge C,n) * 2,1) < r / 4
by GOBRD14:21;
set I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/];
set J = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/];
A6:
1 < [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/]
by A1, Th24;
set G = Gauge C,n;
A7:
[\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] + 1 <= len (Gauge C,n)
by A1, Th23;
A8:
[\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] + 1 <= width (Gauge C,n)
by A1, Th24;
take
n
; ex i, j being Element of NAT st
( 1 < i & i < len (Gauge C,n) & 1 < j & j < width (Gauge C,n) & p `1 <> ((Gauge C,n) * i,j) `1 & p in cell (Gauge C,n),i,j & cell (Gauge C,n),i,j c= BDD C )
A9:
1 < [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/]
by A1, Th22;
then reconsider I = [\(((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/], J = [\(((((p `2 ) - (S-bound C)) / ((N-bound C) - (S-bound C))) * (2 |^ n)) + 2)/] as Element of NAT by A6, INT_1:16;
A10:
I < I + 1
by XREAL_1:31;
then A11:
I <= len (Gauge C,n)
by A7, XXREAL_0:2;
reconsider GIJ = (Gauge C,n) * I,J as Point of (Euclid 2) by Lm3;
reconsider GIJ = (Gauge C,n) * (I + 1),J as Point of (Euclid 2) by Lm3;
reconsider GIJ = (Gauge C,n) * (I + 1),(J + 1) as Point of (Euclid 2) by Lm5;
reconsider GIJ = (Gauge C,n) * I,(J + 1) as Point of (Euclid 2) by Lm5;
1 <= J + 1
by NAT_1:11;
then
[I,(J + 1)] in Indices (Gauge C,n)
by A9, A8, A11, MATRIX_1:37;
then
(Gauge C,n) * I,(J + 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((J + 1) - 2)))]|
by JORDAN8:def 1;
then A12:
((Gauge C,n) * I,(J + 1)) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1))
by EUCLID:56;
then A13:
p `2 < ((Gauge C,n) * I,(J + 1)) `2
by Th28;
A14:
J < J + 1
by XREAL_1:31;
then A15:
J <= width (Gauge C,n)
by A8, XXREAL_0:2;
then
[I,J] in Indices (Gauge C,n)
by A9, A6, A11, MATRIX_1:37;
then A16:
(Gauge C,n) * I,J = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)))]|
by JORDAN8:def 1;
then
((Gauge C,n) * I,J) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 2))
by EUCLID:56;
then A17:
((Gauge C,n) * I,J) `1 <= p `1
by Th25;
1 <= I + 1
by NAT_1:11;
then
[(I + 1),J] in Indices (Gauge C,n)
by A7, A6, A15, MATRIX_1:37;
then
(Gauge C,n) * (I + 1),J = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((I + 1) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2)))]|
by JORDAN8:def 1;
then
((Gauge C,n) * (I + 1),J) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (I - 1))
by EUCLID:56;
then A18:
p `1 < ((Gauge C,n) * (I + 1),J) `1
by Th26;
((Gauge C,n) * I,J) `2 = (S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 2))
by A16, EUCLID:56;
then A19:
((Gauge C,n) * I,J) `2 <= p `2
by Th27;
A20:
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (J - 1)) > p `2
by Th28;
then A21:
p in cell (Gauge C,n),I,J
by A9, A7, A6, A8, A17, A19, A18, A12, JORDAN9:19;
per cases
( p `1 <> ((Gauge C,n) * I,J) `1 or p `1 = ((Gauge C,n) * I,J) `1 )
;
suppose A22:
p `1 <> ((Gauge C,n) * I,J) `1
;
ex i, j being Element of NAT st
( 1 < i & i < len (Gauge C,n) & 1 < j & j < width (Gauge C,n) & p `1 <> ((Gauge C,n) * i,j) `1 & p in cell (Gauge C,n),i,j & cell (Gauge C,n),i,j c= BDD C )take
I
;
ex j being Element of NAT st
( 1 < I & I < len (Gauge C,n) & 1 < j & j < width (Gauge C,n) & p `1 <> ((Gauge C,n) * I,j) `1 & p in cell (Gauge C,n),I,j & cell (Gauge C,n),I,j c= BDD C )take
J
;
( 1 < I & I < len (Gauge C,n) & 1 < J & J < width (Gauge C,n) & p `1 <> ((Gauge C,n) * I,J) `1 & p in cell (Gauge C,n),I,J & cell (Gauge C,n),I,J c= BDD C )thus
( 1
< I &
I < len (Gauge C,n) & 1
< J &
J < width (Gauge C,n) )
by A1, A7, A8, A10, A14, Th22, Th24, XXREAL_0:2;
( p `1 <> ((Gauge C,n) * I,J) `1 & p in cell (Gauge C,n),I,J & cell (Gauge C,n),I,J c= BDD C )
cell (Gauge C,n),
I,
J c= Ball P,
r
by A2, A4, A5, A9, A7, A6, A8, A21, Lm6;
hence
(
p `1 <> ((Gauge C,n) * I,J) `1 &
p in cell (Gauge C,n),
I,
J &
cell (Gauge C,n),
I,
J c= BDD C )
by A3, A9, A7, A6, A8, A20, A17, A19, A18, A12, A22, JORDAN9:19, XBOOLE_1:1;
verum end; suppose A23:
p `1 = ((Gauge C,n) * I,J) `1
;
ex i, j being Element of NAT st
( 1 < i & i < len (Gauge C,n) & 1 < j & j < width (Gauge C,n) & p `1 <> ((Gauge C,n) * i,j) `1 & p in cell (Gauge C,n),i,j & cell (Gauge C,n),i,j c= BDD C )then A24:
p `1 <= ((Gauge C,n) * ((I -' 1) + 1),J) `1
by A9, XREAL_1:237;
A25:
(I -' 1) + 1
<= len (Gauge C,n)
by A9, A11, XREAL_1:237;
A26:
1
<= J
by A1, Th24;
A27:
1
<= I -' 1
by A1, Th22, NAT_D:49;
then
I -' 1
< I
by NAT_D:51;
then A28:
p `1 > ((Gauge C,n) * (I -' 1),J) `1
by A11, A15, A23, A27, A26, GOBOARD5:4;
take
I -' 1
;
ex j being Element of NAT st
( 1 < I -' 1 & I -' 1 < len (Gauge C,n) & 1 < j & j < width (Gauge C,n) & p `1 <> ((Gauge C,n) * (I -' 1),j) `1 & p in cell (Gauge C,n),(I -' 1),j & cell (Gauge C,n),(I -' 1),j c= BDD C )take
J
;
( 1 < I -' 1 & I -' 1 < len (Gauge C,n) & 1 < J & J < width (Gauge C,n) & p `1 <> ((Gauge C,n) * (I -' 1),J) `1 & p in cell (Gauge C,n),(I -' 1),J & cell (Gauge C,n),(I -' 1),J c= BDD C )A29:
J + 1
<= width (Gauge C,n)
by A1, Th24;
A30:
1
<= I -' 1
by A1, Th22, NAT_D:49;
then A31:
I -' 1
< I
by NAT_D:51;
len (Gauge C,n) = width (Gauge C,n)
by JORDAN8:def 1;
then A32:
J <= len (Gauge C,n)
by A8, A14, XXREAL_0:2;
I -' 1
<> 1
proof
assume
I -' 1
= 1
;
contradiction
then
1
= I - 1
by NAT_D:39;
then
((Gauge C,n) * I,J) `1 = W-bound C
by A6, A32, JORDAN8:14;
then
p `1 <= W-bound (BDD C)
by A1, A23, Th18;
then A33:
p `1 < W-bound (BDD C)
by A1, Th34, XXREAL_0:1;
BDD C is
Bounded
by JORDAN2C:114;
hence
contradiction
by A1, A33, Th6;
verum
end; hence
( 1
< I -' 1 &
I -' 1
< len (Gauge C,n) & 1
< J &
J < width (Gauge C,n) )
by A1, A14, A11, A30, A29, A31, Th24, XXREAL_0:1, XXREAL_0:2;
( p `1 <> ((Gauge C,n) * (I -' 1),J) `1 & p in cell (Gauge C,n),(I -' 1),J & cell (Gauge C,n),(I -' 1),J c= BDD C )A34:
(I -' 1) + 1
<= len (Gauge C,n)
by A9, A11, XREAL_1:237;
A35:
J + 1
<= width (Gauge C,n)
by A1, Th24;
A36:
p `1 <= ((Gauge C,n) * ((I -' 1) + 1),J) `1
by A9, A23, XREAL_1:237;
A37:
1
<= J
by A1, Th24;
A38:
(I -' 1) + 1
= I
by A9, XREAL_1:237;
then A39:
((Gauge C,n) * (I -' 1),J) `2 = ((Gauge C,n) * I,J) `2
by A11, A30, A37, A29, JORDAN9:18;
A40:
((Gauge C,n) * (I -' 1),(J + 1)) `2 = ((Gauge C,n) * I,(J + 1)) `2
by A11, A38, A30, A37, A29, JORDAN9:18;
p `1 > ((Gauge C,n) * (I -' 1),J) `1
by A11, A15, A23, A30, A37, A31, GOBOARD5:4;
then
p in cell (Gauge C,n),
(I -' 1),
J
by A19, A13, A30, A34, A37, A29, A36, A39, A40, JORDAN9:19;
then
cell (Gauge C,n),
(I -' 1),
J c= Ball P,
r
by A2, A4, A5, A27, A25, A26, A35, Lm6;
hence
(
p `1 <> ((Gauge C,n) * (I -' 1),J) `1 &
p in cell (Gauge C,n),
(I -' 1),
J &
cell (Gauge C,n),
(I -' 1),
J c= BDD C )
by A3, A19, A13, A39, A40, A27, A25, A26, A35, A24, A28, JORDAN9:19, XBOOLE_1:1;
verumreconsider GIJ =
(Gauge C,n) * (I -' 1),
J as
Point of
(Euclid 2) by Lm3;
set q =
(Gauge C,n) * (I -' 1),
J;
set q =
(Gauge C,n) * (I -' 1),
(J + 1);
reconsider GIJ =
(Gauge C,n) * (I -' 1),
(J + 1) as
Point of
(Euclid 2) by Lm3;
end;