:: Gauges and Cages. { P } art { II }
:: by Artur Korni{\l}owicz and Robert Milewski
::
:: Received November 6, 2000
:: Copyright (c) 2000-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, XBOOLE_0, EUCLID, RCOMP_1, RELAT_2, SPPOL_1,
RELAT_1, CARD_1, ARYTM_3, INT_1, TARSKI, NEWTON, ABIAN, NAT_1, XXREAL_0,
ARYTM_1, FINSEQ_1, JORDAN8, MCART_1, PSCOMP_1, TREES_1, MATRIX_1,
GOBOARD5, REAL_1, SETFAM_1, JORDAN9, PRE_TOPC, TOPREAL1, RLTOPSP1,
PARTFUN1, GOBOARD1, FUNCT_1, XCMPLX_0;
notations TARSKI, XBOOLE_0, ENUMSET1, SETFAM_1, SUBSET_1, ORDINAL1, NUMBERS,
XCMPLX_0, XXREAL_0, XREAL_0, REAL_1, NAT_1, NAT_D, FUNCT_1, PARTFUN1,
STRUCT_0, FINSEQ_1, NEWTON, PRE_TOPC, COMPTS_1, CONNSP_1, MATRIX_0,
RLTOPSP1, EUCLID, GOBOARD1, TOPREAL1, GOBOARD5, PSCOMP_1, SPPOL_1, ABIAN,
GOBRD13, JORDAN8, JORDAN9;
constructors SETFAM_1, REAL_1, NAT_D, NEWTON, REALSET1, ABIAN, CONNSP_1,
PSCOMP_1, JORDAN8, GOBRD13, JORDAN9, SEQ_4, RELSET_1;
registrations RELSET_1, XREAL_0, NAT_1, INT_1, MEMBERED, NEWTON, ABIAN,
GRAPH_3, TOPREAL6, JORDAN8, JORDAN10, FUNCT_1, EUCLID;
requirements NUMERALS, SUBSET, REAL, ARITHM;
definitions TARSKI, SETFAM_1, XBOOLE_0;
equalities XBOOLE_0, PSCOMP_1, ORDINAL1;
expansions TARSKI;
theorems EUCLID, GOBRD11, JORDAN8, PSCOMP_1, JORDAN1A, NAT_1, GOBOARD5,
FINSEQ_2, SPRECT_2, SPPOL_2, TOPREAL1, SPRECT_3, GOBRD13, JORDAN9,
GOBOARD1, TARSKI, JORDAN10, ENUMSET1, NEWTON, NAT_2, INT_1, SPRECT_1,
SPPOL_1, ZFMISC_1, ABIAN, SETFAM_1, XBOOLE_0, XBOOLE_1, XCMPLX_1,
XREAL_1, XXREAL_0, NAT_D, PARTFUN1, MATRIX_0, XREAL_0;
schemes NAT_1;
begin :: Preliminaries
reserve a, b, i, k, m, n for Nat,
r for Real,
D for non empty Subset of TOP-REAL 2,
C for compact connected non vertical non horizontal Subset of TOP-REAL 2;
1 = 2 * 0 + 1;
then
Lm1: 1 div 2 = 0 by NAT_D:def 1;
2 = 2 * 1 + 0;
then
Lm2: 2 div 2 = 1;
Lm3: for x, A, B, C, D being set holds x in A \/ B \/ C \/ D iff x in A or x
in B or x in C or x in D
proof
let x, A, B, C, D be set;
hereby
assume x in A \/ B \/ C \/ D;
then x in A \/ B \/ C or x in D by XBOOLE_0:def 3;
then x in A \/ B or x in C or x in D by XBOOLE_0:def 3;
hence x in A or x in B or x in C or x in D by XBOOLE_0:def 3;
end;
assume x in A or x in B or x in C or x in D;
then x in A \/ B or x in C or x in D by XBOOLE_0:def 3;
then x in A \/ B \/ C or x in D by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
Lm4: for A, B, C, D being set holds union {A,B,C,D} = A \/ B \/ C \/ D
proof
let A, B, C, D be set;
A1: B in {A,B,C,D} by ENUMSET1:def 2;
A2: D in {A,B,C,D} by ENUMSET1:def 2;
hereby
let x be object;
assume x in union {A,B,C,D};
then consider Z being set such that
A3: x in Z and
A4: Z in {A,B,C,D} by TARSKI:def 4;
Z = A or Z = B or Z = C or Z = D by A4,ENUMSET1:def 2;
hence x in A \/ B \/ C \/ D by A3,Lm3;
end;
let x be object;
A5: C in {A,B,C,D} by ENUMSET1:def 2;
assume x in A \/ B \/ C \/ D;
then
A6: x in A or x in B or x in C or x in D by Lm3;
A in {A,B,C,D} by ENUMSET1:def 2;
hence thesis by A6,A1,A5,A2,TARSKI:def 4;
end;
theorem Th1:
for A, B being set st for x being set st x in A ex K being set st
K c= B & x c= union K holds union A c= union B
proof
let A, B be set such that
A1: for x being set st x in A ex K being set st K c= B & x c= union K;
let a be object;
assume a in union A;
then consider Z being set such that
A2: a in Z and
A3: Z in A by TARSKI:def 4;
consider K being set such that
A4: K c= B and
A5: Z c= union K by A1,A3;
ex S being set st a in S & S in K by A2,A5,TARSKI:def 4;
hence thesis by A4,TARSKI:def 4;
end;
registration
let m be non zero Nat;
cluster 2|^m -> even;
coherence
proof
defpred P[Nat] means $1 is non empty implies 2|^$1 is even;
A1: for k be Nat holds P[k] implies P[k+1]
proof
let k be Nat;
assume that
P[k] and
k+1 is non empty;
2|^(k+1) = 2*2|^k by NEWTON:6;
hence thesis;
end;
A2: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
end;
registration
let n be even Nat, m be non zero Nat;
cluster n|^m -> even;
coherence
proof
defpred P[Nat] means $1 is non empty implies n|^$1 is even;
A1: P[k] implies P[k+1]
proof
assume that
P[k] and
k+1 is non empty;
n|^(k+1) = n*n|^k by NEWTON:6;
hence thesis;
end;
A2: P[0];
P[k] from NAT_1:sch 2(A2,A1);
hence thesis;
end;
end;
theorem Th2:
r <> 0 implies 1/r * r|^(i+1) = r|^i
proof
assume
A1: r <> 0;
thus 1/r * r|^(i+1) = 1/r * (r|^i * r) by NEWTON:6
.= 1/r * r * r|^i
.= 1*r|^i by A1,XCMPLX_1:106
.= r|^i;
end;
Lm5: now
let m be Real;
assume 2 <= m;
then 2*m >= 2*2 by XREAL_1:66;
then 2*m - 2 >= 4 - 2 by XREAL_1:9;
hence 2*m - 2 >= 0;
end;
Lm6: now
let m be Real;
assume 1 <= m;
then 2*m >= 2*1 by XREAL_1:66;
then 2*m - 1 >= 2 - 1 by XREAL_1:9;
hence 2*m - 1 >= 0;
end;
Lm7: for m st 2 <= m holds 2*m-2 = 2*m-'2 by Lm5,XREAL_0:def 2;
Lm8: for m st 1 <= m holds 2*m-1 = 2*m-'1 by Lm6,XREAL_0:def 2;
Lm9: now
let m;
assume
A1: m >= 1;
then 2*m >= 2*1 by XREAL_1:64;
then 2*m-1 >= 2-1 by XREAL_1:9;
then
A2: 2*m-'1 >= 1 by A1,Lm8;
thus 2*m-'2+1 = 2*m-'1-'1+1 by NAT_D:45
.= 2*m-'1 by A2,XREAL_1:235;
end;
Lm10: for x being Real st 2 <= m holds x/(2|^i)*(m-2) = x/(2|^(i+1))*(2
*m-'2-2)
proof
let x be Real;
assume 2 <= m;
then
A1: 2*m - 2 >= 0 by Lm5;
thus x/(2|^i)*(m-2) = x/((2|^i)/(m-2)) by XCMPLX_1:81
.= x/((2|^i)*2/((m-2)*2)) by XCMPLX_1:91
.= x/((2|^i)*2)*((m-2)*2) by XCMPLX_1:81
.= x/(2|^(i+1))*(2*m-2-2) by NEWTON:6
.= x/(2|^(i+1))*(2*m-'2-2) by A1,XREAL_0:def 2;
end;
Lm11: 2 <= m implies 1 <= 2*m-'2
proof
assume
A1: 2 <= m;
then 2*2 <= 2*m by XREAL_1:66;
then
A2: 4-2 <= 2*m-2 by XREAL_1:9;
2*m-'2 = 2*m-2 by A1,Lm7;
hence thesis by A2,XXREAL_0:2;
end;
Lm12: 1 <= m implies 1 <= 2*m-'1
proof
assume
A1: 1 <= m;
then 2*1 <= 2*m by XREAL_1:66;
then 2-1 <= 2*m-1 by XREAL_1:9;
hence thesis by A1,Lm8;
end;
Lm13: m < 2|^i+3 implies 2*m-'2 < 2|^(i+1) + 3
proof
per cases by NAT_1:25;
suppose
m = 0 or m = 1;
hence thesis by NAT_2:8;
end;
suppose 1 < m;
then
A1: 1+1 <= m by NAT_1:13;
assume m < 2|^i+3;
then m+1 <= 2|^i + 3 by NAT_1:13;
then 2*(m+1) <= 2*(2|^i + 3) by XREAL_1:64;
then 2*m+2*1 <= 2*(2|^i) + 2*3;
then 2*m+2*1 <= 2|^(i+1) + 6 by NEWTON:6;
then 2*m+2-4 <= 2|^(i+1) + 6 - 4 by XREAL_1:9;
then 2*m-2 <= 2|^(i+1) + 2;
then
A2: 2*m-'2 <= 2|^(i+1) + 2 by A1,Lm7;
2|^(i+1) + 2 < 2|^(i+1) + 3 by XREAL_1:6;
hence thesis by A2,XXREAL_0:2;
end;
end;
Lm14: now
let m;
assume 2 <= m;
hence 2*m-'2+1-2 = 2*m-2+1-2 by Lm7
.= 2*m-3;
end;
begin :: Gauges and Cages
theorem Th3:
2 <= m & m < len Gauge(D,i) & 1 <= a & a <= len Gauge(D,i) & 1 <=
b & b <= len Gauge(D,i+1) implies Gauge(D,i)*(m,a)`1 = Gauge(D,i+1)*(2*m-'2,b)
`1
proof
set I = Gauge(D,i), J = Gauge(D,i+1), z = N-bound D, e = E-bound D, s =
S-bound D, w = W-bound D;
assume that
A1: 2 <= m and
A2: m < len I and
A3: 1 <= a and
A4: a <= len I and
A5: 1 <= b and
A6: b <= len J;
m < 2|^i + 3 by A2,JORDAN8:def 1;
then 2*m-'2 <= 2|^(i+1) + 3 by Lm13;
then
A7: 2*m-'2 <= len J by JORDAN8:def 1;
A8: len J = width J by JORDAN8:def 1;
1 <= 2*m-'2 by A1,Lm11;
then
A9: [2*m-'2,b] in Indices J by A5,A6,A8,A7,MATRIX_0:30;
A10: len I = width I by JORDAN8:def 1;
1 <= m by A1,XXREAL_0:2;
then [m,a] in Indices I by A2,A3,A4,A10,MATRIX_0:30;
hence I*(m,a)`1 = |[w+((e-w)/(2|^i))*(m-2),s+((z-s)/(2|^i))*(a-2)]|`1 by
JORDAN8:def 1
.= w+((e-w)/(2|^i))*(m-2) by EUCLID:52
.= w+((e-w)/(2|^(i+1)))*(2*m-'2-2) by A1,Lm10
.= |[w+((e-w)/(2|^(i+1)))*(2*m-'2-2),s+((z-s)/(2|^(i+1)))*(b-2)]|`1 by
EUCLID:52
.= J*(2*m-'2,b)`1 by A9,JORDAN8:def 1;
end;
theorem Th4:
2 <= n & n < len Gauge(D,i) & 1 <= a & a <= len Gauge(D,i) & 1 <=
b & b <= len Gauge(D,i+1) implies Gauge(D,i)*(a,n)`2 = Gauge(D,i+1)*(b,2*n-'2)
`2
proof
set I = Gauge(D,i), J = Gauge(D,i+1), z = N-bound D, e = E-bound D, s =
S-bound D, w = W-bound D;
assume that
A1: 2 <= n and
A2: n < len I and
A3: 1 <= a and
A4: a <= len I and
A5: 1 <= b and
A6: b <= len J;
n < 2|^i + 3 by A2,JORDAN8:def 1;
then 2*n-'2 <= 2|^(i+1) + 3 by Lm13;
then
A7: 2*n-'2 <= len J by JORDAN8:def 1;
A8: len J = width J by JORDAN8:def 1;
1 <= 2*n-'2 by A1,Lm11;
then
A9: [b,2*n-'2] in Indices J by A5,A6,A8,A7,MATRIX_0:30;
A10: len I = width I by JORDAN8:def 1;
1 <= n by A1,XXREAL_0:2;
then [a,n] in Indices I by A2,A3,A4,A10,MATRIX_0:30;
hence I*(a,n)`2 = |[w+((e-w)/(2|^i))*(a-2),s+((z-s)/(2|^i))*(n-2)]|`2 by
JORDAN8:def 1
.= s+((z-s)/(2|^i))*(n-2) by EUCLID:52
.= s+((z-s)/(2|^(i+1)))*(2*n-'2-2) by A1,Lm10
.= |[w+((e-w)/(2|^(i+1)))*(b-2),s+((z-s)/(2|^(i+1)))*(2*n-'2-2)]|`2 by
EUCLID:52
.= J*(b,2*n-'2)`2 by A9,JORDAN8:def 1;
end;
Lm15: m+1 < len Gauge(D,i) implies 2*m-'1 < len Gauge(D,i+1)
proof
assume m+1 < len Gauge(D,i);
then m+1 < 2|^i + 3 by JORDAN8:def 1;
then 2*(m+1)-'2 < 2|^(i+1) + 3 by Lm13;
then 2*m+2*1-'2 < 2|^(i+1) + 3;
then
A1: 2*m < 2|^(i+1) + 3 by NAT_D:34;
2*m-'1 <= 2*m by NAT_D:44;
then 2*m-'1 < 2|^(i+1) + 3 by A1,XXREAL_0:2;
hence thesis by JORDAN8:def 1;
end;
theorem Th5:
for D being compact non vertical non horizontal Subset of
TOP-REAL 2 holds 2 <= m & m+1 < len Gauge(D,i) & 2 <= n & n+1 < len Gauge(D,i)
implies cell(Gauge(D,i),m,n) = cell(Gauge(D,i+1),2*m-'2,2*n-'2) \/ cell(Gauge(D
,i+1),2*m-'1,2*n-'2) \/ cell(Gauge(D,i+1),2*m-'2,2*n-'1) \/ cell(Gauge(D,i+1),2
*m-'1,2*n-'1)
proof
let D be compact non vertical non horizontal Subset of TOP-REAL 2;
set I = Gauge(D,i), J = Gauge(D,i+1), z = N-bound D, e = E-bound D, s =
S-bound D, w = W-bound D;
assume that
A1: 2 <= m and
A2: m+1 < len I and
A3: 2 <= n and
A4: n+1 < len I;
A5: len J = width J by JORDAN8:def 1;
A6: 2*n-3 < 2*n-2 by XREAL_1:15;
z-s >= 0 by SPRECT_1:22,XREAL_1:48;
then (z-s)/(2|^(i+1))*(2*n-3) <= (z-s)/(2|^(i+1))*(2*n-2) by A6,XREAL_1:64;
then
A7: s+(z-s)/(2|^(i+1))*(2*n-3) <= s+(z-s)/(2|^(i+1))*(2*n-2) by XREAL_1:6;
A8: m <= m+1 by NAT_1:11;
A9: 2*(n+1)-'2-2 = 2*n+2*1-'2-2 .= 2*n-2 by NAT_D:34;
A10: 1 <= 2*m-'2+1 by NAT_1:11;
A11: 1 <= len J by GOBRD11:34;
A12: 1 <= n by A3,XXREAL_0:2;
then
A13: 1 <= 2*n-'1 by Lm12;
2*n-'1 <= 2*n by NAT_D:35;
then
A14: 1 <= 2*n by A13,XXREAL_0:2;
A15: 2*n-'1+1 = 2*n by A12,Lm12,NAT_D:43;
A16: 2*n-'1 < len J by A4,Lm15;
then 2*n-'1+1 <= len J by NAT_1:13;
then [1,2*n] in Indices J by A5,A15,A11,A14,MATRIX_0:30;
then
A17: J*(1,2*n)`2 = |[w+(e-w)/(2|^(i+1))*(1-2),s+(z-s)/(2|^(i+1))*(2*n-2) ]|
`2 by JORDAN8:def 1
.= s+(z-s)/(2|^(i+1))*(2*n-2) by EUCLID:52;
A18: 2*m-'1 = 2*m-1 by A1,Lm8,XXREAL_0:2;
A19: 2*m-'2+1-2 = 2*m-3 by A1,Lm14;
A20: 1 <= 2*n-'2+1 by NAT_1:11;
A21: 2*m-'1 < len J by A2,Lm15;
A22: n <= n+1 by NAT_1:11;
A23: 2*n-'2+1 = 2*n-'1 by A3,Lm9,XXREAL_0:2;
A24: 2*(m+1)-'2-2 = 2*m+2*1-'2-2 .= 2*m-2 by NAT_D:34;
A25: m < len I by A2,NAT_1:13;
then m < 2|^i + 3 by JORDAN8:def 1;
then 2*m-'2 < 2|^(i+1) + 3 by Lm13;
then
A26: 2*m-'2 < len J by JORDAN8:def 1;
then 2*m-'2+1 <= len J by NAT_1:13;
then [2*m-'2+1,1] in Indices J by A5,A11,A10,MATRIX_0:30;
then
A27: J*(2*m-'2+1,1)`1 = |[w+(e-w)/(2|^(i+1))*(2*m-'2+1-2),s+(z-s)/(2|^(i+1))
*(1-2)]|`1 by JORDAN8:def 1
.= w+(e-w)/(2|^(i+1))*(2*m-'2+1-2) by EUCLID:52;
A28: 1 <= m by A1,XXREAL_0:2;
then
A29: 1 < len I by A25,XXREAL_0:2;
then
A30: I*(m,1)`1 = J*(2*m-'2,1)`1 by A1,A25,A11,Th3;
A31: len I = width I by JORDAN8:def 1;
then
A32: n < width I by A4,NAT_1:13;
then
A33: I*(1,n)`2 = J*(1,2*n-'2)`2 by A3,A31,A29,A11,Th4;
A34: 1 <= 2*m-'2 by A1,Lm11;
then
A35: cell(J,2*m-'2,2*n-'1) = { |[r,q]| where r, q is Real:
J*(2*m-'2,1)`1 <=
r & r <= J* (2*m-'2+1,1)`1 & J*(1,2*n-'1)`2 <= q & q <= J*(1,2*n-'1+1)`2 }
by A5,A13,A26,A16,GOBRD11:32;
2*m-'2 = 2*m-2 by A1,Lm7;
then 2*m-'2 < 2*m-'1 by A18,XREAL_1:15;
then
A36: J*(2*m-'2,1)`1 < J*(2*m-'1,1)`1 by A5,A11,A34,A21,GOBOARD5:3;
A37: 2*n-'1 = 2*n-1 by A3,Lm8,XXREAL_0:2;
A38: 2*n-'2+1-2 = 2*n-3 by A3,Lm14;
n < 2|^i + 3 by A31,A32,JORDAN8:def 1;
then 2*n-'2 < 2|^(i+1) + 3 by Lm13;
then
A39: 2*n-'2 < width J by A5,JORDAN8:def 1;
then 2*n-'2+1 <= len J by A5,NAT_1:13;
then [1,2*n-'2+1] in Indices J by A5,A11,A20,MATRIX_0:30;
then
A40: J*(1,2*n-'2+1)`2 = |[w+(e-w)/(2|^(i+1))*(1-2),s+(z-s)/(2|^(i+1))*(2*n-'
2+1-2)]|`2 by JORDAN8:def 1
.= s+(z-s)/(2|^(i+1))*(2*n-'2+1-2) by EUCLID:52;
A41: 1 <= 2*n-'2 by A3,Lm11;
then
A42: cell(J,2*m-'2,2*n-'2) = { |[r,q]| where r, q is Real:
J*(2*m-'2,1)`1 <=
r & r <= J* (2*m-'2+1,1)`1 & J*(1,2*n-'2)`2 <= q & q <= J*(1,2*n-'2+1)`2 }
by A34,A26,A39,GOBRD11:32;
A43: 1 <= 2*m-'1 by A28,Lm12;
then
A44: cell(J,2*m-'1,2*n-'2) = { |[r,q]| where r, q is Real:
J*(2*m-'1,1)`1 <=
r & r <= J* (2*m-'1+1,1)`1 & J*(1,2*n-'2)`2 <= q & q <= J* (1,2*n-'2+1)`2 } by
A41,A39,A21,GOBRD11:32;
A45: cell(J,2*m-'1,2*n-'1) = { |[r,q]| where r, q is Real:
J*(2*m-'1,1)`1 <=
r & r <= J* (2*m-'1+1,1)`1 & J*(1,2*n-'1)`2 <= q & q <= J*(1,2*n-'1+1)`2 }
by A5,A13,A43,A16,A21,GOBRD11:32;
A46: cell(I,m,n) = { |[r,q]| where r, q is Real:
I*(m,1)`1 <= r & r <= I*(m+
1,1)`1 & I*(1,n)`2 <= q & q <= I*(1,n+1)`2 } by A28,A12,A25,A32,GOBRD11:32;
1 <= n+1 by NAT_1:11;
then [1,n+1] in Indices I by A4,A31,A29,MATRIX_0:30;
then
A47: I*(1,n+1)`2 = |[w+(e-w)/(2|^i)*(1-2),s+(z-s)/(2|^i)*(n+1-2)]|`2 by
JORDAN8:def 1
.= s+(z-s)/(2|^i)*(n+1-2) by EUCLID:52
.= s+(z-s)/(2|^(i+1))*(2*(n+1)-'2-2) by A3,A22,Lm10,XXREAL_0:2;
1 <= m+1 by NAT_1:11;
then [m+1,1] in Indices I by A2,A31,A29,MATRIX_0:30;
then
A48: I*(m+1,1)`1 = |[w+(e-w)/(2|^i)*(m+1-2),s+(z-s)/(2|^i)*(1-2)]|`1 by
JORDAN8:def 1
.= w+(e-w)/(2|^i)*(m+1-2) by EUCLID:52
.= w+(e-w)/(2|^(i+1))*(2*(m+1)-'2-2) by A1,A8,Lm10,XXREAL_0:2;
2*n-'2 = 2*n-2 by A3,Lm7;
then 2*n-'2 < 2*n-'1 by A37,XREAL_1:15;
then
A49: J*(1,2*n-'2)`2 < J*(1,2*n-'1)`2 by A5,A11,A41,A16,GOBOARD5:4;
A50: 2*m-'1+1 = 2*m by A28,Lm12,NAT_D:43;
2*m-'1 <= 2*m by NAT_D:35;
then
A51: 1 <= 2*m by A43,XXREAL_0:2;
2*m-'1+1 <= len J by A21,NAT_1:13;
then [2*m,1] in Indices J by A5,A50,A11,A51,MATRIX_0:30;
then
A52: J*(2*m,1)`1 = |[w+(e-w)/(2|^(i+1))*(2*m-2),s+(z-s)/(2|^(i+1))*(1-2) ]|
`1 by JORDAN8:def 1
.= w+(e-w)/(2|^(i+1))*(2*m-2) by EUCLID:52;
A53: 2*m-'2+1 = 2*m-'1 by A1,Lm9,XXREAL_0:2;
thus cell(Gauge(D,i),m,n) c= cell(Gauge(D,i+1),2*m-'2,2*n-'2) \/ cell(Gauge(
D,i+1),2*m-'1,2*n-'2) \/ cell(Gauge(D,i+1),2*m-'2,2*n-'1) \/ cell(Gauge(D,i+1),
2*m-'1,2*n-'1)
proof
let x be object;
assume x in cell(I,m,n);
then consider r, q being Real such that
A54: x = |[r,q]| and
A55: I*(m,1)`1 <= r and
A56: r <= I*(m+1,1)`1 and
A57: I*(1,n)`2 <= q and
A58: q <= I* (1,n+1)`2 by A46;
r <= J*(2*m-'1,1)`1 & q <= J*(1,2*n-'1)`2 or r >= J*(2*m-'1,1)`1 & q
<= J*(1,2*n-'1)`2 or r <= J*(2*m-'1,1)`1 & q >= J*(1,2*n-'1)`2 or r >= J*(2*m-'
1,1)`1 & q >= J*(1,2*n-'1)`2;
then |[r,q]| in cell(J,2*m-'2,2*n-'2) or |[r,q]| in cell(J,2*m-'1,2*n-'2)
or |[r,q]| in cell(J,2*m-'2,2*n-'1) or |[r,q]| in cell(J,2*m-'1,2*n-'1) by A53
,A23,A24,A9,A50,A15,A42,A44,A35,A45,A52,A17,A48,A47,A30,A33,A55,A56,A57,A58;
hence thesis by A54,Lm3;
end;
let x be object;
A59: 2*m-3 < 2*m-2 by XREAL_1:15;
e-w >= 0 by SPRECT_1:21,XREAL_1:48;
then (e-w)/(2|^(i+1))*(2*m-3) <= (e-w)/(2|^(i+1))*(2*m-2) by A59,XREAL_1:64;
then
A60: w+(e-w)/(2|^(i+1))*(2*m-3) <= w+(e-w)/(2|^(i+1))*(2*m-2) by XREAL_1:6;
assume
A61: x in cell(Gauge(D,i+1),2*m-'2,2*n-'2) \/ cell(Gauge(D,i+1),2*m-'1,2
*n-'2) \/ cell(Gauge(D,i+1),2*m-'2,2*n-'1) \/ cell(Gauge(D,i+1),2*m-'1,2*n-'1);
per cases by A61,Lm3;
suppose
x in cell(Gauge(D,i+1),2*m-'2,2*n-'2);
then consider r, q being Real such that
A62: x = |[r,q]| and
A63: J*(2*m-'2,1)`1 <= r and
A64: r <= J*(2*m-'2+1,1)`1 and
A65: J*(1,2*n-'2)`2 <= q and
A66: q <= J*(1,2*n-'2+1)`2 by A42;
A67: q <= I*(1,n+1)`2 by A38,A9,A7,A40,A47,A66,XXREAL_0:2;
r <= I*(m+1,1)`1 by A19,A24,A60,A27,A48,A64,XXREAL_0:2;
hence thesis by A46,A30,A33,A62,A63,A65,A67;
end;
suppose
x in cell(Gauge(D,i+1),2*m-'1,2*n-'2);
then consider r, q being Real such that
A68: x = |[r,q]| and
A69: J*(2*m-'1,1)`1 <= r and
A70: r <= J*(2*m-'1+1,1)`1 and
A71: J*(1,2*n-'2)`2 <= q and
A72: q <= J*(1,2*n-'2+1)`2 by A44;
A73: I*(m,1)`1 <= r by A30,A36,A69,XXREAL_0:2;
q <= I*(1,n+1)`2 by A38,A9,A7,A40,A47,A72,XXREAL_0:2;
hence thesis by A24,A50,A46,A52,A48,A33,A68,A70,A71,A73;
end;
suppose
x in cell(Gauge(D,i+1),2*m-'2,2*n-'1);
then consider r, q being Real such that
A74: x = |[r,q]| and
A75: J*(2*m-'2,1)`1 <= r and
A76: r <= J*(2*m-'2+1,1)`1 and
A77: J*(1,2*n-'1)`2 <= q and
A78: q <= J*(1,2*n-'1+1)`2 by A35;
A79: I*(1,n)`2 <= q by A33,A49,A77,XXREAL_0:2;
r <= I*(m+1,1)`1 by A19,A24,A60,A27,A48,A76,XXREAL_0:2;
hence thesis by A9,A15,A46,A17,A47,A30,A74,A75,A78,A79;
end;
suppose
x in cell(Gauge(D,i+1),2*m-'1,2*n-'1);
then consider r, q being Real such that
A80: x = |[r,q]| and
A81: J*(2*m-'1,1)`1 <= r and
A82: r <= J*(2*m-'1+1,1)`1 and
A83: J*(1,2*n-'1)`2 <= q and
A84: q <= J*(1,2*n-'1+1)`2 by A45;
A85: I*(1,n)`2 <= q by A33,A49,A83,XXREAL_0:2;
I*(m,1)`1 <= r by A30,A36,A81,XXREAL_0:2;
hence thesis by A24,A9,A50,A15,A46,A52,A17,A48,A47,A80,A82,A84,A85;
end;
end;
theorem
for D being compact non vertical non horizontal Subset of TOP-REAL 2,
k being Nat holds 2 <= m & m+1 < len Gauge(D,i) & 2 <= n & n+1 < len
Gauge(D,i) implies cell(Gauge(D,i),m,n) = union { cell(Gauge(D,i+k),a,b) where
a, b is Nat: 2|^k*m - 2|^(k+1) + 2 <= a & a <= 2|^k*m - 2|^k + 1 & 2
|^k*n - 2|^(k+1) + 2 <= b & b <= 2|^k*n - 2|^k + 1 }
proof
let D be compact non vertical non horizontal Subset of TOP-REAL 2;
let k be Nat;
assume that
A1: 2 <= m and
A2: m+1 < len Gauge(D,i) and
A3: 2 <= n and
A4: n+1 < len Gauge(D,i);
deffunc F(Nat) = { cell(Gauge(D,i+$1),a,b) where a, b is Nat:
2|^$1*m - 2|^($1+1) + 2 <= a & a <= 2|^$1*m - 2|^$1 + 1 & 2|^$1*n - 2|^
($1+1) + 2 <= b & b <= 2|^$1*n - 2|^$1 + 1 };
defpred P[Nat] means cell(Gauge(D,i),m,n) = union F($1);
A5: for w being Nat st P[w] holds P[w+1]
proof
let w be Nat such that
A6: P[w];
A7: len Gauge(D,i+w) = 2|^(i+w) + 3 by JORDAN8:def 1;
A8: i+w+1 = i+(w+1);
F(w+1) is_finer_than F(w)
proof
A9: now
let a be odd Nat;
consider e being Nat such that
A10: a = 2*e+1 by ABIAN:9;
A11: 2*e mod 2 = 0;
thus 2*(a div 2 + 1) = 2*(a div 2) + 2*1
.= 2*(2*e div 2 + (1 div 2)) + 2 by A10,A11,NAT_D:19
.= 2*(e + 0) + (1+1) by Lm1
.= a + 1 by A10;
end;
A12: now
let m;
thus 2 * (2|^w*m - 2|^w + 1) = 2*(2|^w*m) - 2*2|^w + (1+1)
.= 2*2|^w*m - 2|^(w+1) + (1+1) by NEWTON:6
.= 2|^(w+1)*m - 2|^(w+1) + (1+1) by NEWTON:6
.= 2|^(w+1)*m - 2|^(w+1) + 1+1;
end;
A13: now
let m;
let a be odd Nat;
assume a <= 2|^(w+1)*m - 2|^(w+1) + 1;
then
A14: a + 1 <= 2|^(w+1)*m - 2|^(w+1) + 1 + 1 by XREAL_1:6;
2 * (2|^w*m - 2|^w + 1) = 2|^(w+1)*m - 2|^(w+1) + 1+1 by A12;
then 2*(a div 2 + 1) <= 2*(2|^w*m - 2|^w + 1) by A9,A14;
hence a div 2 + 1 <= 2|^w*m - 2|^w + 1 by XREAL_1:68;
end;
A15: now
let a be even Nat;
A16: ex e being Nat st a = 2*e by ABIAN:def 2;
thus 2*(a div 2 + 1) = 2*(a div 2) + 2*1 .= a + 2 by A16;
end;
A17: now
let m;
let a be even Nat;
assume a <= 2|^(w+1)*m - 2|^(w+1) + 1;
then a < 2|^(w+1)*m - 2|^(w+1) + 1 by XXREAL_0:1;
then a + 1 <= 2|^(w+1)*m - 2|^(w+1) + 1 by INT_1:7;
then a + 1 + 1 <= 2|^(w+1)*m - 2|^(w+1) + 1 + 1 by XREAL_1:6;
then
A18: a + (1+1) <= 2|^(w+1)*m - 2|^(w+1) + 1 + 1;
2 * (2|^w*m - 2|^w + 1) = 2|^(w+1)*m - 2|^(w+1) + 1+1 by A12;
then 2*(a div 2 + 1) <= 2*(2|^w*m - 2|^w + 1) by A15,A18;
hence a div 2 + 1 <= 2|^w*m - 2|^w + 1 by XREAL_1:68;
end;
let X be set;
assume X in F(w+1);
then consider a, b being Nat such that
A19: X = cell(Gauge(D,i+(w+1)),a,b) and
A20: 2|^(w+1)*m - 2|^(w+1+1) + 2 <= a and
A21: a <= 2|^(w+1)*m - 2|^(w+1) + 1 and
A22: 2|^(w+1)*n - 2|^(w+1+1) + 2 <= b and
A23: b <= 2|^(w+1)*n - 2|^(w+1) + 1;
take Y = cell(Gauge(D,i+w),a div 2 + 1,b div 2 + 1);
deffunc G(Nat,Nat)= cell(Gauge(D,i+w+1),2*(a div 2
+ 1)-'$1,2*(b div 2 + 1)-'$2);
A24: now
let a, m;
A25: 2|^(w+1+1) = 2|^(w+1) * 2|^1 by NEWTON:8
.= 2|^(w+1) * 2;
assume 2 <= m;
then 2|^(w+1)*m >= 2|^(w+1+1) by A25,XREAL_1:64;
then 0 <= 2|^(w+1)*m - 2|^(w+1+1) by XREAL_1:48;
hence 0 + 2 <= 2|^(w+1)*m - 2|^(w+1+1) + 2 by XREAL_1:6;
end;
then 2 <= 2|^(w+1)*m - 2|^(w+1+1) + 2 by A1;
then 2 <= a by A20,XXREAL_0:2;
then 2 div 2 <= a div 2 by NAT_2:24;
then
A26: 1 + 1 <= a div 2 + 1 by Lm2,XREAL_1:6;
A27: now
let a, m;
assume m+1 < len Gauge(D,i);
then m+1 < 2|^i + 3 by JORDAN8:def 1;
then 2*(m+1)-'2 < 2|^(i+1) + 3 by Lm13;
then 2*m+2*1-'2 < 2|^(i+1) + 3;
then 2*m < 2|^(i+1) + 3 by NAT_D:34;
then 1/2*(2*m) < 1/2*(2|^(i+1) + 3) by XREAL_1:68;
then m < 1/2*2|^(i+1) + 1/2*3;
then
A28: m < 2|^i + 1/2*3 by Th2;
2|^i + 3/2 < 2|^i + 2 by XREAL_1:6;
then m < 2|^i + 2 by A28,XXREAL_0:2;
then m+1 <= 2|^i + 2 by NAT_1:13;
then m+1-2 <= 2|^i + 2 - 2 by XREAL_1:9;
then 2|^(w+1)*(m-1) <= 2|^(w+1)*2|^i by XREAL_1:64;
then 2|^(w+1)*(m - 1) + 5 < 2|^(w+1) * 2|^i + 6 by XREAL_1:8;
then
A29: 2|^(w+1)*(m - 1) + 5 < 2|^(w+1+i) + 6 by NEWTON:8;
then
A30: 2|^(w+1)*(m - 1) + 1 + (3 + 1) < 2*2|^(i+w) + 6 by A8,NEWTON:6;
A31: 2|^(w+1)*(m - 1) + 1 + 3 + 1 < 2*2|^(i+w) + 2*3 by A8,A29,NEWTON:6;
assume a <= 2|^(w+1)*m - 2|^(w+1) + 1;
then a+3 <= 2|^(w+1)*m - 2|^(w+1) + 1 + 3 by XREAL_1:6;
then
A32: a+3+0 < 2|^(w+1)*m - 2|^(w+1) + 1 + 3 + 1 by XREAL_1:8;
then
A33: a+3+1 <= 2|^(w+1)*m - 2|^(w+1) + 1 + 3 + 1 by INT_1:7;
now
per cases;
suppose
A34: a is odd;
2 * (a div 2 + 1 + 1) = 2*(a div 2 + 1) + 2*1 .= a+1+2 by A9,A34
.= a+(1+2);
hence 2 * (a div 2 + 1 + 1) < 2 * (2|^(i+w) + 3) by A32,A30,
XXREAL_0:2;
end;
suppose
A35: a is even;
2 * (a div 2 + 1 + 1) = 2*(a div 2 + 1) + 2*1 .= a+2+2 by A15,A35
.= a+(2+2);
hence 2 * (a div 2 + 1 + 1) < 2 * (2|^(i+w) + 3) by A33,A31,
XXREAL_0:2;
end;
end;
hence a div 2 + 1 + 1 < len Gauge(D,i+w) by A7,XREAL_1:64;
end;
then
A36: b div 2 + 1+1 < len Gauge(D,i+w) by A4,A23;
2 <= 2|^(w+1)*n - 2|^(w+1+1) + 2 by A3,A24;
then 2 <= b by A22,XXREAL_0:2;
then 2 div 2 <= b div 2 by NAT_2:24;
then
A37: 1 + 1 <= b div 2 + 1 by Lm2,XREAL_1:6;
a div 2 + 1+1 < len Gauge(D,i+w) by A2,A21,A27;
then
A38: Y = G(2,2) \/ G(1,2) \/ G(2,1) \/ G(1,1) by A26,A37,A36,Th5;
A39: now
let m;
thus 2 * (2|^w*m - 2|^(w+1) + 2) = 2*(2|^w*m) - 2*2|^(w+1) + (2+2)
.= 2*2|^w*m - 2|^(w+1+1) + (2+2) by NEWTON:6
.= 2|^(w+1)*m - 2|^(w+1+1) + (2+2) by NEWTON:6
.= 2|^(w+1)*m - 2|^(w+1+1) + 2+2;
end;
A40: now
let m;
let a be even Nat;
assume 2|^(w+1)*m - 2|^(w+1+1) + 2 <= a;
then
A41: 2|^(w+1)*m - 2|^(w+1+1) + 2 + 2 <= a + 2 by XREAL_1:6;
2 * (2|^w*m - 2|^(w+1) + 2) = 2|^(w+1)*m - 2|^(w+1+1) + 2+2 by A39;
then 2 * (2|^w*m - 2|^(w+1) + 2) <= 2 * (a div 2 + 1) by A15,A41;
hence 2|^w*m - 2|^(w+1) + 2 <= a div 2 + 1 by XREAL_1:68;
end;
A42: now
let m;
let a be odd Nat;
assume 2|^(w+1)*m - 2|^(w+1+1) + 2 <= a;
then 2|^(w+1)*m - 2|^(w+1+1) + 2 < a by XXREAL_0:1;
then 2|^(w+1)*m - 2|^(w+1+1) + 2 + 1 < a + 1 by XREAL_1:6;
then
A43: 2|^(w+1)*m - 2|^(w+1+1) + 2 + 1 + 1 <= a + 1 by INT_1:7;
2 * (2|^w*m - 2|^(w+1) + 2) = 2|^(w+1)*m - 2|^(w+1+1) + 2+2 by A39;
then 2 * (2|^w*m - 2|^(w+1) + 2) <= 2 * (a div 2 + 1) by A9,A43;
hence 2|^w*m - 2|^(w+1) + 2 <= a div 2 + 1 by XREAL_1:68;
end;
per cases;
suppose
A44: a is odd & b is odd;
then
A45: 2|^w*n - 2|^(w+1) + 2 <= b div 2 + 1 by A22,A42;
A46: a div 2 + 1 <= 2|^w*m - 2|^w + 1 by A21,A13,A44;
A47: b div 2 + 1 <= 2|^w*n - 2|^w + 1 by A23,A13,A44;
2|^w*m - 2|^(w+1) + 2 <= a div 2 + 1 by A20,A42,A44;
hence Y in F(w) by A46,A45,A47;
A48: 2*(b div 2 + 1)-'1 = b+1-'1 by A9,A44
.= b by NAT_D:34;
2*(a div 2 + 1)-'1 = a+1-'1 by A9,A44
.= a by NAT_D:34;
hence thesis by A19,A38,A48,XBOOLE_1:7;
end;
suppose
A49: a is odd & b is even;
then
A50: 2|^w*n - 2|^(w+1) + 2 <= b div 2 + 1 by A22,A40;
A51: a div 2 + 1 <= 2|^w*m - 2|^w + 1 by A21,A13,A49;
A52: b div 2 + 1 <= 2|^w*n - 2|^w + 1 by A23,A17,A49;
2|^w*m - 2|^(w+1) + 2 <= a div 2 + 1 by A20,A42,A49;
hence Y in F(w) by A51,A50,A52;
A53: G(2,2) \/ G(1,2) c= G(2,2) \/ G(1,2) \/ G(2,1) by XBOOLE_1:7;
G(1,2) c= G(2,2) \/ G(1,2) by XBOOLE_1:7;
then
A54: G(1,2) c= G(2,2) \/ G(1,2) \/ G(2,1) by A53;
A55: G(2,2) \/ G(1,2) \/ G(2,1) c= Y by A38,XBOOLE_1:7;
A56: 2*(b div 2 + 1)-'2 = b+2-'2 by A15,A49
.= b by NAT_D:34;
2*(a div 2 + 1)-'1 = a+1-'1 by A9,A49
.= a by NAT_D:34;
hence thesis by A19,A56,A54,A55;
end;
suppose
A57: a is even & b is odd;
then
A58: 2|^w*n - 2|^(w+1) + 2 <= b div 2 + 1 by A22,A42;
A59: a div 2 + 1 <= 2|^w*m - 2|^w + 1 by A21,A17,A57;
A60: b div 2 + 1 <= 2|^w*n - 2|^w + 1 by A23,A13,A57;
2|^w*m - 2|^(w+1) + 2 <= a div 2 + 1 by A20,A40,A57;
hence Y in F(w) by A59,A58,A60;
A61: G(2,1) c= G(2,2) \/ G(1,2) \/ G(2,1) by XBOOLE_1:7;
A62: G(2,2) \/ G(1,2) \/ G(2,1) c= Y by A38,XBOOLE_1:7;
A63: 2*(b div 2 + 1)-'1 = b+1-'1 by A9,A57
.= b by NAT_D:34;
2*(a div 2 + 1)-'2 = a+2-'2 by A15,A57
.= a by NAT_D:34;
hence thesis by A19,A63,A61,A62;
end;
suppose
A64: a is even & b is even;
then
A65: 2|^w*n - 2|^(w+1) + 2 <= b div 2 + 1 by A22,A40;
A66: a div 2 + 1 <= 2|^w*m - 2|^w + 1 by A21,A17,A64;
A67: b div 2 + 1 <= 2|^w*n - 2|^w + 1 by A23,A17,A64;
2|^w*m - 2|^(w+1) + 2 <= a div 2 + 1 by A20,A40,A64;
hence Y in F(w) by A66,A65,A67;
A68: 2*(b div 2 + 1)-'2 = b+2-'2 by A15,A64
.= b by NAT_D:34;
2*(a div 2 + 1)-'2 = a+2-'2 by A15,A64
.= a by NAT_D:34;
then X c= G(2,2) \/ (G(1,2) \/ G(2,1) \/ G(1,1)) by A19,A68,XBOOLE_1:7;
then X c= G(2,2) \/ (G(1,2) \/ G(2,1)) \/ G(1,1) by XBOOLE_1:4;
hence thesis by A38,XBOOLE_1:4;
end;
end;
then
A69: union F(w+1) c= union F(w) by SETFAM_1:13;
A70: len Gauge(D,i) = 2|^i + 3 by JORDAN8:def 1;
for x being set st x in F(w) ex K being set st K c= F(w+1) & x c= union K
proof
let x be set;
assume x in F(w);
then consider a, b such that
A71: x = cell(Gauge(D,i+w),a,b) and
A72: 2|^w*m - 2|^(w+1) + 2 <= a and
A73: a <= 2|^w*m - 2|^w + 1 and
A74: 2|^w*n - 2|^(w+1) + 2 <= b and
A75: b <= 2|^w*n - 2|^w + 1;
take K = { cell(Gauge(D,i+w+1),2*a-'2,2*b-'2), cell(Gauge(D,i+w+1),2*a-'
1,2*b-'2), cell(Gauge(D,i+w+1),2*a-'2,2*b-'1), cell(Gauge(D,i+w+1),2*a-'1,2*b-'
1) };
A76: now
let m;
assume 2 <= m;
then 2|^w*m >= 2|^w*2 by XREAL_1:64;
then 2|^w*m >= 2|^(w+1) by NEWTON:6;
then 0 <= 2|^w*m - 2|^(w+1) by XREAL_1:48;
hence 0 + 2 <= 2|^w*m - 2|^(w+1) + 2 by XREAL_1:6;
end;
then
A77: 2 <= 2|^w*m - 2|^(w+1) + 2 by A1;
then
A78: 2 <= a by A72,XXREAL_0:2;
A79: 2*a-'2 = 2*a-2 by A72,A77,Lm7,XXREAL_0:2;
A80: 2 <= 2|^w*n - 2|^(w+1) + 2 by A3,A76;
then
A81: 2 <= b by A74,XXREAL_0:2;
A82: 2*b-'2 = 2*b-2 by A74,A80,Lm7,XXREAL_0:2;
2*b-'1 = 2*b-1 by A81,Lm8,XXREAL_0:2;
then
A83: 2*b-'2 < 2*b-'1 by A82,XREAL_1:15;
2*a-'1 = 2*a-1 by A78,Lm8,XXREAL_0:2;
then
A84: 2*a-'2 < 2*a-'1 by A79,XREAL_1:15;
hereby
A85: now
let a,m;
assume
A86: 2 <= a;
assume a <= 2|^w*m - 2|^w + 1;
then 2*a <= 2*(2|^w*m - 2|^w + 1) by XREAL_1:64;
then 2*a <= 2*2|^w*m - 2*(2|^w) + 2;
then 2*a <= 2|^(w+1)*m - 2*(2|^w) + 2 by NEWTON:6;
then 2*a <= 2|^(w+1)*m - 2|^(w+1) + 2 by NEWTON:6;
then 2*a-2 <= 2|^(w+1)*m - 2|^(w+1) + 2 - 2 by XREAL_1:9;
then
A87: 2*a-'2 <= 2|^(w+1)*m - 2|^(w+1) + 2 - 2 by A86,Lm7;
2|^(w+1)*m - 2|^(w+1) + 0 < 2|^(w+1)*m - 2|^(w+1) + 1 by XREAL_1:6;
hence 2*a-'2 < 2|^(w+1)*m - 2|^(w+1) + 1 by A87,XXREAL_0:2;
end;
then
A88: 2*a-'2 < 2|^(w+1)*m - 2|^(w+1) + 1 by A73,A78;
then 2*a-'2+1 <= 2|^(w+1)*m - 2|^(w+1) + 1 by INT_1:7;
then
A89: 2*a-'1 <= 2|^(w+1)*m - 2|^(w+1) + 1 by A78,Lm9,XXREAL_0:2;
A90: now
let a,m;
assume
A91: 2 <= a;
assume 2|^w*m - 2|^(w+1) + 2 <= a;
then 2 * (2|^w*m - 2|^(w+1) + 2) <= 2 * a by XREAL_1:64;
then 2*2|^w*m - 2 * (2|^(w+1)) + 4 <= 2 * a;
then 2|^(w+1)*m - 2 * (2|^(w+1)) + 4 <= 2 * a by NEWTON:6;
then 2|^(w+1)*m - 2|^(w+1+1) + 4 <= 2 * a by NEWTON:6;
then 2|^(w+1)*m - 2|^(w+1+1) + 4 - 2 <= 2 * a - 2 by XREAL_1:9;
hence 2|^(w+1)*m - 2|^(w+1+1) + (4 - 2) <= 2 * a -' 2 by A91,Lm7;
end;
then
A92: 2|^(w+1)*n - 2|^(w+1+1) + 2 <= 2*b-'2 by A74,A81;
then
A93: 2|^(w+1)*n - 2|^(w+1+1) + 2 <= 2*b-'1 by A83,XXREAL_0:2;
let q be object;
assume q in K;
then
A94: q = cell(Gauge(D,i+(w+1)),2*a-'2,2*b-'2) or q = cell(Gauge(D,i+(w
+1)),2*a-'1,2*b-'2) or q = cell(Gauge(D,i+(w+1)),2*a-'2,2*b-'1) or q = cell(
Gauge(D,i+(w+1)),2*a-'1,2*b-'1) by ENUMSET1:def 2;
A95: 2*b-'2 < 2|^(w+1)*n - 2|^(w+1) + 1 by A75,A81,A85;
then 2*b-'2+1 <= 2|^(w+1)*n - 2|^(w+1) + 1 by INT_1:7;
then
A96: 2*b-'1 <= 2|^(w+1)*n - 2|^(w+1) + 1 by A81,Lm9,XXREAL_0:2;
A97: 2|^(w+1)*m - 2|^(w+1+1) + 2 <= 2*a-'2 by A72,A78,A90;
then 2|^(w+1)*m - 2|^(w+1+1) + 2 <= 2*a-'1 by A84,XXREAL_0:2;
hence q in F(w+1) by A97,A88,A89,A92,A95,A96,A93,A94;
end;
A98: now
let a, m;
assume m+1 < len Gauge(D,i);
then m+1-2 < 2|^i + 3 - 2 by A70,XREAL_1:9;
then m-1 < 2|^i + (3 - 2);
then m-1 <= 2|^i + 0 by INT_1:7;
then 2|^w*(m-1) <= 2|^w*2|^i by XREAL_1:64;
then 2|^w*(m-1) <= 2|^(w+i) by NEWTON:8;
then
A99: 2|^w*(m-1)+3 <= 2|^(w+i)+3 by XREAL_1:6;
assume a <= 2|^w*m - 2|^w + 1;
then a+1 <= 2|^w*m - 2|^w + 1 + 1 by XREAL_1:6;
then a+1 < 2|^w*m - 2|^w + 1 + 1 + 1 by XREAL_1:145;
hence a+1 < len Gauge(D,i+w) by A7,A99,XXREAL_0:2;
end;
then
A100: b+1 < len Gauge(D,i+w) by A4,A75;
a+1 < len Gauge(D,i+w) by A2,A73,A98;
then cell(Gauge(D,i+w),a,b) = cell(Gauge(D,i+w+1),2*a-'2,2*b-'2) \/
cell(Gauge(D,i+w+1),2*a-'1,2*b-'2) \/ cell(Gauge(D,i+w+1),2*a-'2,2*b-'1) \/
cell(Gauge(D,i+w+1),2*a-'1,2*b-'1) by A78,A81,A100,Th5;
hence thesis by A71,Lm4;
end;
hence cell(Gauge(D,i),m,n) c= union F(w+1) by A6,Th1;
let d be object;
assume d in union F(w+1);
hence thesis by A6,A69;
end;
A101: now
let m;
A102: 2|^0 * m = 1*m by NEWTON:4;
hence 2|^0 * m - 2|^(0+1) + 2 = m - 2 + 2
.= m;
thus 2|^0 * m - 2|^0 + 1 = m - 1 + 1 by A102,NEWTON:4
.= m;
end;
F(0) = { cell(Gauge(D,i),m,n) }
proof
hereby
let x be object;
assume x in F(0);
then consider a, b such that
A103: x = cell(Gauge(D,i+0),a,b) and
A104: 2|^0 * m - 2|^(0+1) + 2 <= a and
A105: a <= 2|^0 * m - 2|^0 + 1 and
A106: 2|^0 * n - 2|^(0+1) + 2 <= b and
A107: b <= 2|^0 * n - 2|^0 + 1;
A108: now
let a, m;
assume that
A109: 2|^0 * m - 2|^(0+1) + 2 <= a and
A110: a <= 2|^0 * m - 2|^0 + 1;
A111: 2|^0 * m - 2|^0 + 1 = m by A101;
2|^0 * m - 2|^(0+1) + 2= m by A101;
hence a = m by A109,A110,A111,XXREAL_0:1;
end;
then
A112: b = n by A106,A107;
a = m by A104,A105,A108;
hence x in { cell(Gauge(D,i),m,n) } by A103,A112,TARSKI:def 1;
end;
let x be object;
assume x in { cell(Gauge(D,i),m,n) };
then
A113: x = cell(Gauge(D,i+0),m,n) by TARSKI:def 1;
A114: m <= 2|^0 * m - 2|^0 + 1 by A101;
A115: n <= 2|^0 * n - 2|^0 + 1 by A101;
A116: 2|^0 * n - 2|^(0+1) + 2 <= n by A101;
2|^0 * m - 2|^(0+1) + 2 <= m by A101;
hence thesis by A113,A114,A116,A115;
end;
then
A117: P[0] by ZFMISC_1:25;
for w being Nat holds P[w] from NAT_1:sch 2(A117,A5);
hence thesis;
end;
theorem Th7:
ex i being Nat st 1 <= i & i < len Cage(C,n) & N-max
C in right_cell(Cage(C,n),i,Gauge(C,n))
proof
consider p be Point of TOP-REAL 2 such that
A1: north_halfline N-max C /\ L~Cage(C,n) = {p} by JORDAN1A:86,PSCOMP_1:42;
A2: p in north_halfline N-max C /\ L~Cage(C,n) by A1,TARSKI:def 1;
then
A3: p in north_halfline N-max C by XBOOLE_0:def 4;
p in L~Cage(C,n) by A2,XBOOLE_0:def 4;
then consider i be Nat such that
A4: 1 <= i and
A5: i+1 <= len Cage(C,n) and
A6: p in LSeg(Cage(C,n),i) by SPPOL_2:13;
take i;
A7: LSeg(Cage(C,n),i) = LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A4,A5,
TOPREAL1:def 3;
A8: len Gauge(C,n) >= 4 by JORDAN8:10;
then
A9: 1 < len Gauge(C,n) by XXREAL_0:2;
A10: len Gauge(C,n)-'1+1 = len Gauge(C,n) by A8,XREAL_1:235,XXREAL_0:2;
then
A11: len Gauge(C,n)-'1 < len Gauge(C,n) by NAT_1:13;
A12: N-max C = |[(N-max C)`1,(N-max C)`2]| by EUCLID:53;
A13: len Gauge(C,n)-'1 <= len Gauge(C,n) by NAT_D:44;
A14: (N-max C)`2 = N-bound C by EUCLID:52
.= Gauge(C,n)*(1,len Gauge(C,n)-'1)`2 by A9,JORDAN8:14;
A15: N-max C in N-most C by PSCOMP_1:42;
A16: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
thus
A17: 1 <= i & i < len Cage(C,n) by A4,A5,NAT_1:13;
then
A18: (Cage(C,n)/.i)`2 = p`2 by A3,A6,A15,A7,JORDAN1A:78,SPPOL_1:40;
A19: (Cage(C,n)/.(i+1))`2 = p`2 by A3,A6,A17,A15,A7,JORDAN1A:78,SPPOL_1:40;
A20: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i1,j1,i2,j2 be Nat such that
A21: [i1,j1] in Indices Gauge(C,n) and
A22: Cage(C,n)/.i = Gauge(C,n)*(i1,j1) and
A23: [i2,j2] in Indices Gauge(C,n) and
A24: Cage(C,n)/.(i+1) = Gauge(C,n)*(i2,j2) and
A25: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A4,A5,JORDAN8:3;
A26: 1 <= i1 by A21,MATRIX_0:32;
A27: j2 <= width Gauge(C,n) by A23,MATRIX_0:32;
A28: i1 <= len Gauge(C,n) by A21,MATRIX_0:32;
A29: 1 <= j1 by A21,MATRIX_0:32;
p`2 = N-bound L~Cage(C,n) by A2,JORDAN1A:82,PSCOMP_1:42;
then (Gauge(C,n)*(i1,j1))`2 = Gauge(C,n)*(i1,len Gauge(C,n))`2 by A22,A18,A26
,A28,JORDAN1A:70;
then
A30: len Gauge(C,n) <= j1 by A16,A26,A28,A29,GOBOARD5:4;
A31: j1 <= width Gauge(C,n) by A21,MATRIX_0:32;
then
A32: j1 = len Gauge(C,n) by A16,A30,XXREAL_0:1;
A33: 1 <= j2 by A23,MATRIX_0:32;
A34: j1 = j2
proof
assume j1 <> j2;
then j1 < j2 or j2 < j1 by XXREAL_0:1;
hence contradiction by A22,A24,A25,A18,A19,A26,A28,A29,A27,A33,A31,
GOBOARD5:4;
end;
A35: 1 <= i2 by A23,MATRIX_0:32;
A36: i2 <= len Gauge(C,n) by A23,MATRIX_0:32;
i1 <= i1+1 by NAT_1:11;
then
A37: (Cage(C,n)/.i)`1 <= (Cage(C,n)/.(i+1))`1 by A4,A5,A21,A22,A23,A24,A25,A16
,A26,A36,A29,A27,A34,A30,JORDAN10:4,JORDAN1A:18;
then p`1 <= (Cage(C,n)/.(i+1))`1 by A6,A7,TOPREAL1:3;
then
(N-max C)`1 <= Gauge(C,n)*(i1+1,len Gauge(C,n))`1 by A3,A4,A5,A21,A22,A23,A24
,A25,A16,A34,A32,JORDAN10:4,TOPREAL1:def 10;
then
A38: (N-max C)`1 <= Gauge(C,n)*(i1+1,1)`1 by A4,A5,A21,A22,A23,A24,A25,A16,A35
,A36,A34,A30,A9,GOBOARD5:2,JORDAN10:4;
(Cage(C,n)/.i)`1 <= p`1 by A6,A7,A37,TOPREAL1:3;
then Gauge(C,n)*(i1,len Gauge(C,n))`1 <= (N-max C)`1 by A3,A22,A32,
TOPREAL1:def 10;
then
A39: Gauge(C,n)*(i1,1)`1 <= (N-max C)`1 by A16,A26,A28,A9,GOBOARD5:2;
len Gauge(C,n) >= 1+1 by A8,XXREAL_0:2;
then
A40: len Gauge(C,n)-1 >= 1 by XREAL_1:19;
then len Gauge(C,n)-'1 >= 1 by XREAL_0:def 2;
then Gauge(C,n)*(1,j1)`2 >= (N-max C)`2 by A16,A32,A9,A14,A13,SPRECT_3:12;
then
A41: N-max C in { |[r,s]| where r,s is Real:
Gauge(C,n)*(i1,1)`1 <= r & r
<= Gauge(C,n)*(i1+1,1)`1 & Gauge(C,n)*(1,j1-'1)`2 <= s & s <= Gauge(C,n)*(1,j1)
`2 } by A32,A14,A39,A38,A12;
A42: 1 <= i1 by A21,MATRIX_0:32;
i1 < len Gauge(C,n) by A4,A5,A21,A22,A23,A24,A25,A16,A36,A34,A30,JORDAN10:4
,NAT_1:13;
then N-max C in cell(Gauge(C,n),i1,j1-'1) by A16,A32,A42,A40,A10,A11,A41,
GOBRD11:32;
hence thesis by A4,A5,A20,A21,A22,A23,A24,A25,A16,A34,A30,GOBRD13:24
,JORDAN10:4;
end;
theorem
ex i being Nat st 1 <= i & i < len Cage(C,n) & N-max C in
right_cell(Cage(C,n),i)
proof
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
consider i be Nat such that
A2: 1 <= i and
A3: i < len Cage(C,n) and
A4: N-max C in right_cell(Cage(C,n),i,Gauge(C,n)) by Th7;
take i;
thus 1 <= i & i < len Cage(C,n) by A2,A3;
i+1 <= len Cage(C,n) by A3,NAT_1:13;
then right_cell(Cage(C,n),i,Gauge(C,n)) c= right_cell(Cage(C,n),i) by A2,A1,
GOBRD13:33;
hence thesis by A4;
end;
theorem Th9:
ex i being Nat st 1 <= i & i < len Cage(C,n) & E-min
C in right_cell(Cage(C,n),i,Gauge(C,n))
proof
consider p be Point of TOP-REAL 2 such that
A1: east_halfline E-min C /\ L~Cage(C,n) = {p} by JORDAN1A:87,PSCOMP_1:50;
A2: p in east_halfline E-min C /\ L~Cage(C,n) by A1,TARSKI:def 1;
then
A3: p in east_halfline E-min C by XBOOLE_0:def 4;
len Gauge(C,n) < len Gauge(C,n)+1 by NAT_1:13;
then
A4: len Gauge(C,n)-1 < len Gauge(C,n) by XREAL_1:19;
A5: len Gauge(C,n)-'1 <= len Gauge(C,n) by NAT_D:44;
A6: E-min C = |[(E-min C)`1,(E-min C)`2]| by EUCLID:53;
A7: len Gauge(C,n) >= 4 by JORDAN8:10;
then
A8: 1 < len Gauge(C,n) by XXREAL_0:2;
A9: len Gauge(C,n)-'1+1 = len Gauge(C,n) by A7,XREAL_1:235,XXREAL_0:2;
A10: (E-min C)`1 = E-bound C by EUCLID:52
.= Gauge(C,n)*(len Gauge(C,n)-'1,1)`1 by A8,JORDAN8:12;
A11: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A12: E-min C in E-most C by PSCOMP_1:50;
p in L~Cage(C,n) by A2,XBOOLE_0:def 4;
then consider i be Nat such that
A13: 1 <= i and
A14: i+1 <= len Cage(C,n) and
A15: p in LSeg(Cage(C,n),i) by SPPOL_2:13;
take i;
A16: LSeg(Cage(C,n),i) = LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A13,A14,
TOPREAL1:def 3;
thus
A17: 1 <= i & i < len Cage(C,n) by A13,A14,NAT_1:13;
then
A18: (Cage(C,n)/.i)`1 = p`1 by A3,A15,A12,A16,JORDAN1A:79,SPPOL_1:41;
A19: (Cage(C,n)/.(i+1))`1 = p`1 by A3,A15,A17,A12,A16,JORDAN1A:79,SPPOL_1:41;
A20: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i1,j1,i2,j2 be Nat such that
A21: [i1,j1] in Indices Gauge(C,n) and
A22: Cage(C,n)/.i = Gauge(C,n)*(i1,j1) and
A23: [i2,j2] in Indices Gauge(C,n) and
A24: Cage(C,n)/.(i+1) = Gauge(C,n)*(i2,j2) and
A25: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A13,A14,JORDAN8:3;
A26: 1 <= i1 by A21,MATRIX_0:32;
A27: j1 <= width Gauge(C,n) by A21,MATRIX_0:32;
A28: j2 <= width Gauge(C,n) by A23,MATRIX_0:32;
A29: 1 <= i2 by A23,MATRIX_0:32;
A30: 1 <= j1 by A21,MATRIX_0:32;
p`1 = E-bound L~Cage(C,n) by A2,JORDAN1A:83,PSCOMP_1:50;
then (Gauge(C,n)*(i1,j1))`1 = Gauge(C,n)*(len Gauge(C,n),j1)`1 by A22,A18,A11
,A30,A27,JORDAN1A:71;
then
A31: len Gauge(C,n) <= i1 by A26,A30,A27,GOBOARD5:3;
A32: i1 <= len Gauge(C,n) by A21,MATRIX_0:32;
then
A33: i1 = len Gauge(C,n) by A31,XXREAL_0:1;
A34: i2 <= len Gauge(C,n) by A23,MATRIX_0:32;
A35: i1 = i2
proof
assume i1 <> i2;
then i1 < i2 or i2 < i1 by XXREAL_0:1;
hence contradiction by A22,A24,A25,A18,A19,A26,A32,A29,A34,A30,A28,
GOBOARD5:3;
end;
then
A36: j2 < width Gauge(C,n) by A13,A14,A21,A22,A23,A24,A25,A27,A31,JORDAN10:1
,NAT_1:13;
A37: 1 <= j2 by A23,MATRIX_0:32;
j2 <= j2+1 by NAT_1:11;
then
A38: (Cage(C,n)/.i)`2 >= (Cage(C,n)/.(i+1))`2 by A13,A14,A21,A22,A23,A24,A25
,A26,A32,A37,A27,A35,A31,JORDAN10:1,JORDAN1A:19;
then p`2 <= (Cage(C,n)/.i)`2 by A15,A16,TOPREAL1:4;
then
(E-min C)`2 <= Gauge(C,n)*(len Gauge(C,n),j2+1)`2 by A3,A13,A14,A21,A22,A23
,A24,A25,A35,A33,JORDAN10:1,TOPREAL1:def 11;
then
A39: (E-min C)`2 <= Gauge(C,n)* (1,j2+1)`2 by A13,A14,A21,A22,A23,A24,A25,A29
,A30,A27,A35,A33,GOBOARD5:1,JORDAN10:1;
(Cage(C,n)/.(i+1))`2 <= p`2 by A15,A16,A38,TOPREAL1:4;
then Gauge(C,n)*(len Gauge(C,n),j2)`2 <= (E-min C)`2 by A3,A24,A35,A33,
TOPREAL1:def 11;
then
A40: Gauge(C,n)*(1,j2)`2 <= (E-min C)`2 by A29,A28,A37,A35,A33,GOBOARD5:1;
len Gauge(C,n) >= 1+1 by A7,XXREAL_0:2;
then
A41: len Gauge(C,n)-1 >= 1 by XREAL_1:19;
then len Gauge(C,n)-'1 >= 1 by XREAL_0:def 2;
then Gauge(C,n)*(i1,1)`1 >= (E-min C)`1 by A11,A33,A8,A10,A5,SPRECT_3:13;
then
E-min C in { |[r,s]| where r,s is Real:
Gauge(C,n)*(len Gauge(C,n)-'1,
1)`1 <= r & r <= Gauge(C,n)*(len Gauge(C,n),1)`1 & Gauge(C,n)*(1,j2)`2 <= s & s
<= Gauge(C,n)*(1,j2+1)`2 } by A33,A10,A40,A39,A6;
then E-min C in cell(Gauge(C,n),i2-'1,j2) by A37,A35,A33,A36,A41,A4,A9,
GOBRD11:32;
hence thesis by A13,A14,A20,A21,A22,A23,A24,A25,A35,A31,GOBRD13:28,JORDAN10:1
;
end;
theorem
ex i being Nat st 1 <= i & i < len Cage(C,n) & E-min C in
right_cell(Cage(C,n),i)
proof
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
consider i be Nat such that
A2: 1 <= i and
A3: i < len Cage(C,n) and
A4: E-min C in right_cell(Cage(C,n),i,Gauge(C,n)) by Th9;
take i;
thus 1 <= i & i < len Cage(C,n) by A2,A3;
i+1 <= len Cage(C,n) by A3,NAT_1:13;
then right_cell(Cage(C,n),i,Gauge(C,n)) c= right_cell(Cage(C,n),i) by A2,A1,
GOBRD13:33;
hence thesis by A4;
end;
theorem Th11:
ex i being Nat st 1 <= i & i < len Cage(C,n) & E-max
C in right_cell(Cage(C,n),i,Gauge(C,n))
proof
consider p be Point of TOP-REAL 2 such that
A1: east_halfline E-max C /\ L~Cage(C,n) = {p} by JORDAN1A:87,PSCOMP_1:50;
A2: p in east_halfline E-max C /\ L~Cage(C,n) by A1,TARSKI:def 1;
then
A3: p in east_halfline E-max C by XBOOLE_0:def 4;
len Gauge(C,n) < len Gauge(C,n)+1 by NAT_1:13;
then
A4: len Gauge(C,n)-1 < len Gauge(C,n) by XREAL_1:19;
A5: len Gauge(C,n)-'1 <= len Gauge(C,n) by NAT_D:44;
A6: len Gauge(C,n) >= 4 by JORDAN8:10;
then
A7: 1 < len Gauge(C,n) by XXREAL_0:2;
A8: len Gauge(C,n)-'1+1 = len Gauge(C,n) by A6,XREAL_1:235,XXREAL_0:2;
A9: (E-max C)`1 = E-bound C by EUCLID:52
.= Gauge(C,n)*(len Gauge(C,n)-'1,1)`1 by A7,JORDAN8:12;
A10: E-max C = |[(E-max C)`1,(E-max C)`2]| by EUCLID:53;
A11: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A12: E-max C in E-most C by PSCOMP_1:50;
p in L~Cage(C,n) by A2,XBOOLE_0:def 4;
then consider i be Nat such that
A13: 1 <= i and
A14: i+1 <= len Cage(C,n) and
A15: p in LSeg(Cage(C,n),i) by SPPOL_2:13;
take i;
A16: LSeg(Cage(C,n),i) = LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A13,A14,
TOPREAL1:def 3;
thus
A17: 1 <= i & i < len Cage(C,n) by A13,A14,NAT_1:13;
then
A18: (Cage(C,n)/.i)`1 = p`1 by A3,A15,A12,A16,JORDAN1A:79,SPPOL_1:41;
A19: (Cage(C,n)/.(i+1))`1 = p`1 by A3,A15,A17,A12,A16,JORDAN1A:79,SPPOL_1:41;
A20: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i1,j1,i2,j2 be Nat such that
A21: [i1,j1] in Indices Gauge(C,n) and
A22: Cage(C,n)/.i = Gauge(C,n)*(i1,j1) and
A23: [i2,j2] in Indices Gauge(C,n) and
A24: Cage(C,n)/.(i+1) = Gauge(C,n)*(i2,j2) and
A25: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A13,A14,JORDAN8:3;
A26: 1 <= i1 by A21,MATRIX_0:32;
A27: j1 <= width Gauge(C,n) by A21,MATRIX_0:32;
A28: i2 <= len Gauge(C,n) by A23,MATRIX_0:32;
A29: j2 <= width Gauge(C,n) by A23,MATRIX_0:32;
A30: 1 <= j1 by A21,MATRIX_0:32;
p`1 = E-bound L~Cage(C,n) by A2,JORDAN1A:83,PSCOMP_1:50;
then (Gauge(C,n)*(i1,j1))`1 = Gauge(C,n)*(len Gauge(C,n),j1)`1 by A22,A18,A11
,A30,A27,JORDAN1A:71;
then
A31: len Gauge(C,n) <= i1 by A26,A30,A27,GOBOARD5:3;
A32: i1 <= len Gauge(C,n) by A21,MATRIX_0:32;
then
A33: i1 = len Gauge(C,n) by A31,XXREAL_0:1;
A34: 1 <= i2 by A23,MATRIX_0:32;
A35: i1 = i2
proof
assume i1 <> i2;
then i1 < i2 or i2 < i1 by XXREAL_0:1;
hence contradiction by A22,A24,A25,A18,A19,A26,A32,A34,A28,A30,A29,
GOBOARD5:3;
end;
then
A36: j2 < width Gauge(C,n) by A13,A14,A21,A22,A23,A24,A25,A27,A31,JORDAN10:1
,NAT_1:13;
A37: 1 <= j2 by A23,MATRIX_0:32;
j2 <= j2+1 by NAT_1:11;
then
A38: (Cage(C,n)/.i)`2 >= (Cage(C,n)/.(i+1))`2 by A13,A14,A21,A22,A23,A24,A25
,A26,A32,A37,A27,A35,A31,JORDAN10:1,JORDAN1A:19;
then p`2 <= (Cage(C,n)/.i)`2 by A15,A16,TOPREAL1:4;
then
(E-max C)`2 <= Gauge(C,n)*(len Gauge(C,n),j2+1)`2 by A3,A13,A14,A21,A22,A23
,A24,A25,A35,A33,JORDAN10:1,TOPREAL1:def 11;
then
A39: (E-max C)`2 <= Gauge(C,n)* (1,j2+1)`2 by A13,A14,A21,A22,A23,A24,A25,A30
,A27,A35,A31,A7,GOBOARD5:1,JORDAN10:1;
(Cage(C,n)/.(i+1))`2 <= p`2 by A15,A16,A38,TOPREAL1:4;
then Gauge(C,n)*(len Gauge(C,n),j2)`2 <= (E-max C)`2 by A3,A24,A35,A33,
TOPREAL1:def 11;
then
A40: Gauge(C,n)*(1,j2)`2 <= (E-max C)`2 by A29,A37,A7,GOBOARD5:1;
len Gauge(C,n) >= 1+1 by A6,XXREAL_0:2;
then
A41: len Gauge(C,n)-1 >= 1 by XREAL_1:19;
then len Gauge(C,n)-'1 >= 1 by XREAL_0:def 2;
then Gauge(C,n)*(i1,1)`1 >= (E-max C)`1 by A11,A33,A7,A9,A5,SPRECT_3:13;
then
E-max C in { |[r,s]| where r,s is Real:
Gauge(C,n)*(len Gauge(C,n)-'1,
1)`1 <= r & r <= Gauge(C,n)*(len Gauge(C,n),1)`1 & Gauge(C,n)*(1,j2)`2 <= s & s
<= Gauge(C,n)*(1,j2+1)`2 } by A33,A9,A40,A39,A10;
then E-max C in cell(Gauge(C,n),i2-'1,j2) by A37,A35,A33,A36,A41,A4,A8,
GOBRD11:32;
hence thesis by A13,A14,A20,A21,A22,A23,A24,A25,A35,A31,GOBRD13:28,JORDAN10:1
;
end;
theorem
ex i being Nat st 1 <= i & i < len Cage(C,n) & E-max C in
right_cell(Cage(C,n),i)
proof
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
consider i be Nat such that
A2: 1 <= i and
A3: i < len Cage(C,n) and
A4: E-max C in right_cell(Cage(C,n),i,Gauge(C,n)) by Th11;
take i;
thus 1 <= i & i < len Cage(C,n) by A2,A3;
i+1 <= len Cage(C,n) by A3,NAT_1:13;
then right_cell(Cage(C,n),i,Gauge(C,n)) c= right_cell(Cage(C,n),i) by A2,A1,
GOBRD13:33;
hence thesis by A4;
end;
theorem Th13:
ex i being Nat st 1 <= i & i < len Cage(C,n) & S-min
C in right_cell(Cage(C,n),i,Gauge(C,n))
proof
consider p be Point of TOP-REAL 2 such that
A1: south_halfline S-min C /\ L~Cage(C,n) = {p} by JORDAN1A:88,PSCOMP_1:58;
A2: p in south_halfline S-min C /\ L~Cage(C,n) by A1,TARSKI:def 1;
then
A3: p in south_halfline S-min C by XBOOLE_0:def 4;
A4: S-min C = |[(S-min C)`1,(S-min C)`2]| by EUCLID:53;
A5: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A6: len Gauge(C,n) >= 4 by JORDAN8:10;
then
A7: 1 < len Gauge(C,n) by XXREAL_0:2;
p in L~Cage(C,n) by A2,XBOOLE_0:def 4;
then consider i be Nat such that
A8: 1 <= i and
A9: i+1 <= len Cage(C,n) and
A10: p in LSeg(Cage(C,n),i) by SPPOL_2:13;
take i;
A11: LSeg(Cage(C,n),i) = LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A8,A9,
TOPREAL1:def 3;
A12: (S-min C)`2 = S-bound C by EUCLID:52
.= Gauge(C,n)*(1,2)`2 by A7,JORDAN8:13;
A13: S-min C in S-most C by PSCOMP_1:58;
thus
A14: 1 <= i & i < len Cage(C,n) by A8,A9,NAT_1:13;
then
A15: (Cage(C,n)/.i)`2 = p`2 by A3,A10,A13,A11,JORDAN1A:80,SPPOL_1:40;
A16: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i1,j1,i2,j2 be Nat such that
A17: [i1,j1] in Indices Gauge(C,n) and
A18: Cage(C,n)/.i = Gauge(C,n)*(i1,j1) and
A19: [i2,j2] in Indices Gauge(C,n) and
A20: Cage(C,n)/.(i+1) = Gauge(C,n)*(i2,j2) and
A21: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A8,A9,JORDAN8:3;
A22: 1 <= i1 by A17,MATRIX_0:32;
A23: 1 <= j2 by A19,MATRIX_0:32;
A24: i2 <= i2+1 by NAT_1:11;
A25: j2 <= width Gauge(C,n) by A19,MATRIX_0:32;
A26: i1 <= len Gauge(C,n) by A17,MATRIX_0:32;
A27: j1 <= width Gauge(C,n) by A17,MATRIX_0:32;
p`2 = S-bound L~Cage(C,n) by A2,JORDAN1A:84,PSCOMP_1:58;
then (Gauge(C,n)*(i1,j1))`2 = Gauge(C,n)*(i1,1)`2 by A18,A15,A22,A26,
JORDAN1A:72;
then
A28: 1 >= j1 by A22,A26,A27,GOBOARD5:4;
A29: 1 <= j1 by A17,MATRIX_0:32;
then
A30: j1 = 1 by A28,XXREAL_0:1;
A31: (Cage(C,n)/.(i+1))`2 = p`2 by A3,A10,A14,A13,A11,JORDAN1A:80,SPPOL_1:40;
A32: j1 = j2
proof
assume j1 <> j2;
then j1 < j2 or j2 < j1 by XXREAL_0:1;
hence contradiction by A18,A20,A21,A15,A31,A22,A26,A29,A25,A23,A27,
GOBOARD5:4;
end;
then
A33: i2 < len Gauge(C,n) by A8,A9,A17,A18,A19,A20,A21,A26,A28,JORDAN10:3
,NAT_1:13;
1 <= i2 by A19,MATRIX_0:32;
then
A34: (Cage(C,n)/.i)`1 >= (Cage(C,n)/.(i+1))`1 by A8,A9,A17,A18,A19,A20,A21,A26
,A29,A25,A23,A27,A28,A24,JORDAN10:3,JORDAN1A:18;
then p`1 <= (Cage(C,n)/.i)`1 by A10,A11,TOPREAL1:3;
then
A35: (S-min C)`1 <= Gauge(C,n)*(i2+ 1,1)`1 by A3,A8,A9,A17,A18,A19,A20,A21,A32
,A30,JORDAN10:3,TOPREAL1:def 12;
(Cage(C,n)/.(i+1))`1 <= p`1 by A10,A11,A34,TOPREAL1:3;
then
A36: Gauge(C,n)*(i2,1)`1 <= (S-min C)`1 by A3,A20,A32,A30,TOPREAL1:def 12;
A37: 1 <= i2 by A19,MATRIX_0:32;
1+1 <= len Gauge(C,n) by A6,XXREAL_0:2;
then Gauge(C,n)* (1,j1)`2 <= (S-min C)`2 by A5,A30,A7,A12,SPRECT_3:12;
then S-min C in { |[r,s]| where r,s is Real:
Gauge(C,n)*(i2,1)`1 <= r & r
<= Gauge(C,n)*(i2+1,1)`1 & Gauge(C,n)*(1,j1)`2 <= s & s <= Gauge(C,n)*(1,j1+1)
`2 } by A30,A12,A36,A35,A4;
then S-min C in cell(Gauge(C,n),i2,j1) by A5,A30,A37,A33,A7,GOBRD11:32;
hence thesis by A8,A9,A16,A17,A18,A19,A20,A21,A32,A28,GOBRD13:26,JORDAN10:3;
end;
theorem
ex i being Nat st 1 <= i & i < len Cage(C,n) & S-min C in
right_cell(Cage(C,n),i)
proof
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
consider i be Nat such that
A2: 1 <= i and
A3: i < len Cage(C,n) and
A4: S-min C in right_cell(Cage(C,n),i,Gauge(C,n)) by Th13;
take i;
thus 1 <= i & i < len Cage(C,n) by A2,A3;
i+1 <= len Cage(C,n) by A3,NAT_1:13;
then right_cell(Cage(C,n),i,Gauge(C,n)) c= right_cell(Cage(C,n),i) by A2,A1,
GOBRD13:33;
hence thesis by A4;
end;
theorem Th15:
ex i being Nat st 1 <= i & i < len Cage(C,n) & S-max
C in right_cell(Cage(C,n),i,Gauge(C,n))
proof
consider p be Point of TOP-REAL 2 such that
A1: south_halfline S-max C /\ L~Cage(C,n) = {p} by JORDAN1A:88,PSCOMP_1:58;
A2: p in south_halfline S-max C /\ L~Cage(C,n) by A1,TARSKI:def 1;
then
A3: p in south_halfline S-max C by XBOOLE_0:def 4;
A4: S-max C = |[(S-max C)`1,(S-max C)`2]| by EUCLID:53;
A5: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A6: len Gauge(C,n) >= 4 by JORDAN8:10;
then
A7: 1 < len Gauge(C,n) by XXREAL_0:2;
p in L~Cage(C,n) by A2,XBOOLE_0:def 4;
then consider i be Nat such that
A8: 1 <= i and
A9: i+1 <= len Cage(C,n) and
A10: p in LSeg(Cage(C,n),i) by SPPOL_2:13;
take i;
A11: LSeg(Cage(C,n),i) = LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A8,A9,
TOPREAL1:def 3;
A12: (S-max C)`2 = S-bound C by EUCLID:52
.= Gauge(C,n)*(1,2)`2 by A7,JORDAN8:13;
A13: S-max C in S-most C by PSCOMP_1:58;
thus
A14: 1 <= i & i < len Cage(C,n) by A8,A9,NAT_1:13;
then
A15: (Cage(C,n)/.i)`2 = p`2 by A3,A10,A13,A11,JORDAN1A:80,SPPOL_1:40;
A16: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i1,j1,i2,j2 be Nat such that
A17: [i1,j1] in Indices Gauge(C,n) and
A18: Cage(C,n)/.i = Gauge(C,n)*(i1,j1) and
A19: [i2,j2] in Indices Gauge(C,n) and
A20: Cage(C,n)/.(i+1) = Gauge(C,n)*(i2,j2) and
A21: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A8,A9,JORDAN8:3;
A22: 1 <= i1 by A17,MATRIX_0:32;
A23: 1 <= j2 by A19,MATRIX_0:32;
A24: i2 <= i2+1 by NAT_1:11;
A25: j2 <= width Gauge(C,n) by A19,MATRIX_0:32;
A26: i1 <= len Gauge(C,n) by A17,MATRIX_0:32;
A27: j1 <= width Gauge(C,n) by A17,MATRIX_0:32;
p`2 = S-bound L~Cage(C,n) by A2,JORDAN1A:84,PSCOMP_1:58;
then (Gauge(C,n)*(i1,j1))`2 = Gauge(C,n)*(i1,1)`2 by A18,A15,A22,A26,
JORDAN1A:72;
then
A28: 1 >= j1 by A22,A26,A27,GOBOARD5:4;
A29: 1 <= j1 by A17,MATRIX_0:32;
then
A30: j1 = 1 by A28,XXREAL_0:1;
A31: (Cage(C,n)/.(i+1))`2 = p`2 by A3,A10,A14,A13,A11,JORDAN1A:80,SPPOL_1:40;
A32: j1 = j2
proof
assume j1 <> j2;
then j1 < j2 or j2 < j1 by XXREAL_0:1;
hence contradiction by A18,A20,A21,A15,A31,A22,A26,A29,A25,A23,A27,
GOBOARD5:4;
end;
then
A33: i2 < len Gauge(C,n) by A8,A9,A17,A18,A19,A20,A21,A26,A28,JORDAN10:3
,NAT_1:13;
1 <= i2 by A19,MATRIX_0:32;
then
A34: (Cage(C,n)/.i)`1 >= (Cage(C,n)/.(i+1))`1 by A8,A9,A17,A18,A19,A20,A21,A26
,A29,A25,A23,A27,A28,A24,JORDAN10:3,JORDAN1A:18;
then p`1 <= (Cage(C,n)/.i)`1 by A10,A11,TOPREAL1:3;
then
A35: (S-max C)`1 <= Gauge(C,n)*(i2+ 1,1)`1 by A3,A8,A9,A17,A18,A19,A20,A21,A32
,A30,JORDAN10:3,TOPREAL1:def 12;
(Cage(C,n)/.(i+1))`1 <= p`1 by A10,A11,A34,TOPREAL1:3;
then
A36: Gauge(C,n)*(i2,1)`1 <= (S-max C)`1 by A3,A20,A32,A30,TOPREAL1:def 12;
A37: 1 <= i2 by A19,MATRIX_0:32;
1+1 <= len Gauge(C,n) by A6,XXREAL_0:2;
then Gauge(C,n)* (1,j1)`2 <= (S-max C)`2 by A5,A30,A7,A12,SPRECT_3:12;
then S-max C in { |[r,s]| where r,s is Real:
Gauge(C,n)*(i2,1)`1 <= r & r
<= Gauge(C,n)*(i2+1,1)`1 & Gauge(C,n)*(1,j1)`2 <= s & s <= Gauge(C,n)*(1,j1+1)
`2 } by A30,A12,A36,A35,A4;
then S-max C in cell(Gauge(C,n),i2,j1) by A5,A30,A37,A33,A7,GOBRD11:32;
hence thesis by A8,A9,A16,A17,A18,A19,A20,A21,A32,A28,GOBRD13:26,JORDAN10:3;
end;
theorem
ex i being Nat st 1 <= i & i < len Cage(C,n) & S-max C in
right_cell(Cage(C,n),i)
proof
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
consider i be Nat such that
A2: 1 <= i and
A3: i < len Cage(C,n) and
A4: S-max C in right_cell(Cage(C,n),i,Gauge(C,n)) by Th15;
take i;
thus 1 <= i & i < len Cage(C,n) by A2,A3;
i+1 <= len Cage(C,n) by A3,NAT_1:13;
then right_cell(Cage(C,n),i,Gauge(C,n)) c= right_cell(Cage(C,n),i) by A2,A1,
GOBRD13:33;
hence thesis by A4;
end;
theorem Th17:
ex i being Nat st 1 <= i & i < len Cage(C,n) & W-min
C in right_cell(Cage(C,n),i,Gauge(C,n))
proof
consider p be Point of TOP-REAL 2 such that
A1: west_halfline W-min C /\ L~Cage(C,n) = {p} by JORDAN1A:89,PSCOMP_1:34;
A2: p in west_halfline W-min C /\ L~Cage(C,n) by A1,TARSKI:def 1;
then
A3: p in west_halfline W-min C by XBOOLE_0:def 4;
A4: W-min C = |[(W-min C)`1,(W-min C)`2]| by EUCLID:53;
A5: len Gauge(C,n) >= 4 by JORDAN8:10;
then
A6: 1 < len Gauge(C,n) by XXREAL_0:2;
A7: (W-min C)`1 = W-bound C by EUCLID:52
.= Gauge(C,n)*(2,1)`1 by A6,JORDAN8:11;
A8: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A9: W-min C in W-most C by PSCOMP_1:34;
p in L~Cage(C,n) by A2,XBOOLE_0:def 4;
then consider i be Nat such that
A10: 1 <= i and
A11: i+1 <= len Cage(C,n) and
A12: p in LSeg(Cage(C,n),i) by SPPOL_2:13;
take i;
A13: LSeg(Cage(C,n),i) = LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A10,A11,
TOPREAL1:def 3;
thus
A14: 1 <= i & i < len Cage(C,n) by A10,A11,NAT_1:13;
then
A15: (Cage(C,n)/.i)`1 = p`1 by A3,A12,A9,A13,JORDAN1A:81,SPPOL_1:41;
A16: (Cage(C,n)/.(i+1))`1 = p`1 by A3,A12,A14,A9,A13,JORDAN1A:81,SPPOL_1:41;
A17: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i1,j1,i2,j2 be Nat such that
A18: [i1,j1] in Indices Gauge(C,n) and
A19: Cage(C,n)/.i = Gauge(C,n)*(i1,j1) and
A20: [i2,j2] in Indices Gauge(C,n) and
A21: Cage(C,n)/.(i+1) = Gauge(C,n)*(i2,j2) and
A22: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A10,A11,JORDAN8:3;
A23: i1 <= len Gauge(C,n) by A18,MATRIX_0:32;
A24: i2 <= len Gauge(C,n) by A20,MATRIX_0:32;
A25: j2 <= width Gauge(C,n) by A20,MATRIX_0:32;
A26: j1 <= width Gauge(C,n) by A18,MATRIX_0:32;
A27: 1 <= j1 by A18,MATRIX_0:32;
p`1 = W-bound L~Cage(C,n) by A2,JORDAN1A:85,PSCOMP_1:34;
then (Gauge(C,n)*(i1,j1))`1 = Gauge(C,n)*(1,j1)`1 by A19,A15,A8,A27,A26,
JORDAN1A:73;
then
A28: 1 >= i1 by A23,A27,A26,GOBOARD5:3;
A29: 1 <= i1 by A18,MATRIX_0:32;
then
A30: i1 = 1 by A28,XXREAL_0:1;
A31: 1 <= i2 by A20,MATRIX_0:32;
A32: i1 = i2
proof
assume i1 <> i2;
then i1 < i2 or i2 < i1 by XXREAL_0:1;
hence contradiction by A19,A21,A22,A15,A16,A29,A23,A31,A24,A27,A25,
GOBOARD5:3;
end;
then
A33: j1 < width Gauge(C,n) by A10,A11,A18,A19,A20,A21,A22,A25,A28,JORDAN10:2
,NAT_1:13;
j1 <= j1+1 by NAT_1:11;
then
A34: (Cage(C,n)/.i)`2 <= (Cage(C,n)/.(i+1))`2 by A10,A11,A18,A19,A20,A21,A22
,A29,A23,A27,A25,A32,A28,JORDAN10:2,JORDAN1A:19;
then p`2 <= (Cage(C,n)/.(i+1))`2 by A12,A13,TOPREAL1:4;
then
A35: (W-min C)`2 <= Gauge(C,n)*(1, j1+1)`2 by A3,A10,A11,A18,A19,A20,A21,A22
,A32,A30,JORDAN10:2,TOPREAL1:def 13;
(Cage(C,n)/.i)`2 <= p`2 by A12,A13,A34,TOPREAL1:4;
then
A36: Gauge(C,n)*(1,j1)`2 <= (W-min C)`2 by A3,A19,A30,TOPREAL1:def 13;
1+1 <= len Gauge(C,n) by A5,XXREAL_0:2;
then Gauge(C,n)* (i1,1)`1 <= (W-min C)`1 by A8,A30,A6,A7,SPRECT_3:13;
then W-min C in { |[r,s]| where r,s is Real:
Gauge(C,n)*(i1,1)`1 <= r & r
<= Gauge(C,n)*(i1+1,1)`1 & Gauge(C,n)*(1,j1)`2 <= s & s <= Gauge(C,n)*(1,j1+1)
`2 } by A30,A7,A36,A35,A4;
then W-min C in cell(Gauge(C,n),i1,j1) by A27,A30,A33,A6,GOBRD11:32;
hence thesis by A10,A11,A17,A18,A19,A20,A21,A22,A32,A28,GOBRD13:22,JORDAN10:2
;
end;
theorem
ex i being Nat st 1 <= i & i < len Cage(C,n) & W-min C in
right_cell(Cage(C,n),i)
proof
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
consider i be Nat such that
A2: 1 <= i and
A3: i < len Cage(C,n) and
A4: W-min C in right_cell(Cage(C,n),i,Gauge(C,n)) by Th17;
take i;
thus 1 <= i & i < len Cage(C,n) by A2,A3;
i+1 <= len Cage(C,n) by A3,NAT_1:13;
then right_cell(Cage(C,n),i,Gauge(C,n)) c= right_cell(Cage(C,n),i) by A2,A1,
GOBRD13:33;
hence thesis by A4;
end;
theorem Th19:
ex i being Nat st 1 <= i & i < len Cage(C,n) & W-max
C in right_cell(Cage(C,n),i,Gauge(C,n))
proof
consider p be Point of TOP-REAL 2 such that
A1: west_halfline W-max C /\ L~Cage(C,n) = {p} by JORDAN1A:89,PSCOMP_1:34;
A2: p in west_halfline W-max C /\ L~Cage(C,n) by A1,TARSKI:def 1;
then
A3: p in west_halfline W-max C by XBOOLE_0:def 4;
A4: W-max C = |[(W-max C)`1,(W-max C)`2]| by EUCLID:53;
A5: len Gauge(C,n) >= 4 by JORDAN8:10;
then
A6: 1 < len Gauge(C,n) by XXREAL_0:2;
A7: (W-max C)`1 = W-bound C by EUCLID:52
.= Gauge(C,n)*(2,1)`1 by A6,JORDAN8:11;
A8: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
A9: W-max C in W-most C by PSCOMP_1:34;
p in L~Cage(C,n) by A2,XBOOLE_0:def 4;
then consider i be Nat such that
A10: 1 <= i and
A11: i+1 <= len Cage(C,n) and
A12: p in LSeg(Cage(C,n),i) by SPPOL_2:13;
take i;
A13: LSeg(Cage(C,n),i) = LSeg(Cage(C,n)/.i,Cage(C,n)/.(i+1)) by A10,A11,
TOPREAL1:def 3;
thus
A14: 1 <= i & i < len Cage(C,n) by A10,A11,NAT_1:13;
then
A15: (Cage(C,n)/.i)`1 = p`1 by A3,A12,A9,A13,JORDAN1A:81,SPPOL_1:41;
A16: (Cage(C,n)/.(i+1))`1 = p`1 by A3,A12,A14,A9,A13,JORDAN1A:81,SPPOL_1:41;
A17: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i1,j1,i2,j2 be Nat such that
A18: [i1,j1] in Indices Gauge(C,n) and
A19: Cage(C,n)/.i = Gauge(C,n)*(i1,j1) and
A20: [i2,j2] in Indices Gauge(C,n) and
A21: Cage(C,n)/.(i+1) = Gauge(C,n)*(i2,j2) and
A22: i1 = i2 & j1+1 = j2 or i1+1 = i2 & j1 = j2 or i1 = i2+1 & j1 = j2
or i1 = i2 & j1 = j2+1 by A10,A11,JORDAN8:3;
A23: i1 <= len Gauge(C,n) by A18,MATRIX_0:32;
A24: i2 <= len Gauge(C,n) by A20,MATRIX_0:32;
A25: j2 <= width Gauge(C,n) by A20,MATRIX_0:32;
A26: j1 <= width Gauge(C,n) by A18,MATRIX_0:32;
A27: 1 <= j1 by A18,MATRIX_0:32;
p`1 = W-bound L~Cage(C,n) by A2,JORDAN1A:85,PSCOMP_1:34;
then (Gauge(C,n)*(i1,j1))`1 = Gauge(C,n)*(1,j1)`1 by A19,A15,A8,A27,A26,
JORDAN1A:73;
then
A28: 1 >= i1 by A23,A27,A26,GOBOARD5:3;
A29: 1 <= i1 by A18,MATRIX_0:32;
then
A30: i1 = 1 by A28,XXREAL_0:1;
A31: 1 <= i2 by A20,MATRIX_0:32;
A32: i1 = i2
proof
assume i1 <> i2;
then i1 < i2 or i2 < i1 by XXREAL_0:1;
hence contradiction by A19,A21,A22,A15,A16,A29,A23,A31,A24,A27,A25,
GOBOARD5:3;
end;
then
A33: j1 < width Gauge(C,n) by A10,A11,A18,A19,A20,A21,A22,A25,A28,JORDAN10:2
,NAT_1:13;
j1 <= j1+1 by NAT_1:11;
then
A34: (Cage(C,n)/.i)`2 <= (Cage(C,n)/.(i+1))`2 by A10,A11,A18,A19,A20,A21,A22
,A29,A23,A27,A25,A32,A28,JORDAN10:2,JORDAN1A:19;
then p`2 <= (Cage(C,n)/.(i+1))`2 by A12,A13,TOPREAL1:4;
then
A35: (W-max C)`2 <= Gauge(C,n)*(1, j1+1)`2 by A3,A10,A11,A18,A19,A20,A21,A22
,A32,A30,JORDAN10:2,TOPREAL1:def 13;
(Cage(C,n)/.i)`2 <= p`2 by A12,A13,A34,TOPREAL1:4;
then
A36: Gauge(C,n)*(1,j1)`2 <= (W-max C)`2 by A3,A19,A30,TOPREAL1:def 13;
1+1 <= len Gauge(C,n) by A5,XXREAL_0:2;
then Gauge(C,n)* (i1,1)`1 <= (W-max C)`1 by A8,A30,A6,A7,SPRECT_3:13;
then W-max C in { |[r,s]| where r,s is Real:
Gauge(C,n)*(i1,1)`1 <= r & r
<= Gauge(C,n)*(i1+1,1)`1 & Gauge(C,n)*(1,j1)`2 <= s & s <= Gauge(C,n)*(1,j1+1)
`2 } by A30,A7,A36,A35,A4;
then W-max C in cell(Gauge(C,n),i1,j1) by A27,A30,A33,A6,GOBRD11:32;
hence thesis by A10,A11,A17,A18,A19,A20,A21,A22,A32,A28,GOBRD13:22,JORDAN10:2
;
end;
theorem
ex i being Nat st 1 <= i & i < len Cage(C,n) & W-max C in
right_cell(Cage(C,n),i)
proof
A1: Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
consider i be Nat such that
A2: 1 <= i and
A3: i < len Cage(C,n) and
A4: W-max C in right_cell(Cage(C,n),i,Gauge(C,n)) by Th19;
take i;
thus 1 <= i & i < len Cage(C,n) by A2,A3;
i+1 <= len Cage(C,n) by A3,NAT_1:13;
then right_cell(Cage(C,n),i,Gauge(C,n)) c= right_cell(Cage(C,n),i) by A2,A1,
GOBRD13:33;
hence thesis by A4;
end;
theorem Th21:
ex i being Nat st 1 <= i & i <= len Gauge(C,n) &
N-min L~Cage(C,n) = Gauge(C,n)*(i,width Gauge(C,n))
proof
A1: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
N-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:39;
then consider m be Nat such that
A2: m in dom Cage(C,n) and
A3: Cage(C,n).m = N-min L~Cage(C,n) by FINSEQ_2:10;
A4: Cage(C,n)/.m = N-min L~Cage(C,n) by A2,A3,PARTFUN1:def 6;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i,j be Nat such that
A5: [i,j] in Indices Gauge(C,n) and
A6: Cage(C,n)/.m = Gauge(C,n)*(i,j) by A2,GOBOARD1:def 9;
take i;
thus
A7: 1 <= i & i <= len Gauge(C,n) by A5,MATRIX_0:32;
A8: 1 <= j by A5,MATRIX_0:32;
A9: now
assume j < width Gauge(C,n);
then
(N-min L~Cage(C,n))`2 < Gauge(C,n)*(i,width Gauge(C,n))`2 by A4,A6,A7,A8,
GOBOARD5:4;
then N-bound L~Cage(C,n) < Gauge(C,n)*(i,width Gauge(C,n))`2 by EUCLID:52;
hence contradiction by A7,A1,JORDAN1A:70;
end;
j <= width Gauge(C,n) by A5,MATRIX_0:32;
hence thesis by A4,A6,A9,XXREAL_0:1;
end;
theorem
ex i being Nat st 1 <= i & i <= len Gauge(C,n) & N-max L~
Cage(C,n) = Gauge(C,n)*(i,width Gauge(C,n))
proof
A1: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
N-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:40;
then consider m be Nat such that
A2: m in dom Cage(C,n) and
A3: Cage(C,n).m = N-max L~Cage(C,n) by FINSEQ_2:10;
A4: Cage(C,n)/.m = N-max L~Cage(C,n) by A2,A3,PARTFUN1:def 6;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i,j be Nat such that
A5: [i,j] in Indices Gauge(C,n) and
A6: Cage(C,n)/.m = Gauge(C,n)*(i,j) by A2,GOBOARD1:def 9;
take i;
thus
A7: 1 <= i & i <= len Gauge(C,n) by A5,MATRIX_0:32;
A8: 1 <= j by A5,MATRIX_0:32;
A9: now
assume j < width Gauge(C,n);
then
(N-max L~Cage(C,n))`2 < Gauge(C,n)*(i,width Gauge(C,n))`2 by A4,A6,A7,A8,
GOBOARD5:4;
then N-bound L~Cage(C,n) < Gauge(C,n)*(i,width Gauge(C,n))`2 by EUCLID:52;
hence contradiction by A7,A1,JORDAN1A:70;
end;
j <= width Gauge(C,n) by A5,MATRIX_0:32;
hence thesis by A4,A6,A9,XXREAL_0:1;
end;
theorem
ex i being Nat st 1 <= i & i <= len Gauge(C,n) & Gauge(C,n)
*(i,width Gauge(C,n)) in rng Cage(C,n)
proof
consider i be Nat such that
A1: 1 <= i and
A2: i <= len Gauge(C,n) and
A3: N-min L~Cage(C,n) = Gauge(C,n)*(i,width Gauge(C,n)) by Th21;
take i;
thus thesis by A1,A2,A3,SPRECT_2:39;
end;
theorem Th24:
ex j being Nat st 1 <= j & j <= width Gauge(C,n) &
E-min L~Cage(C,n) = Gauge(C,n)*(len Gauge(C,n),j)
proof
A1: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
E-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:45;
then consider m be Nat such that
A2: m in dom Cage(C,n) and
A3: Cage(C,n).m = E-min L~Cage(C,n) by FINSEQ_2:10;
A4: Cage(C,n)/.m = E-min L~Cage(C,n) by A2,A3,PARTFUN1:def 6;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i,j be Nat such that
A5: [i,j] in Indices Gauge(C,n) and
A6: Cage(C,n)/.m = Gauge(C,n)*(i,j) by A2,GOBOARD1:def 9;
take j;
thus
A7: 1 <= j & j <= width Gauge(C,n) by A5,MATRIX_0:32;
A8: 1 <= i by A5,MATRIX_0:32;
A9: now
assume i < len Gauge(C,n);
then (E-min L~Cage(C,n))`1 < Gauge(C,n)*(len Gauge(C,n),j)`1 by A4,A6,A7,A8
,GOBOARD5:3;
then E-bound L~Cage(C,n) < Gauge(C,n)* (len Gauge(C,n),j)`1 by EUCLID:52;
hence contradiction by A7,A1,JORDAN1A:71;
end;
i <= len Gauge(C,n) by A5,MATRIX_0:32;
hence thesis by A4,A6,A9,XXREAL_0:1;
end;
theorem
ex j being Nat st 1 <= j & j <= width Gauge(C,n) & E-max L~
Cage(C,n) = Gauge(C,n)*(len Gauge(C,n),j)
proof
A1: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
E-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:46;
then consider m be Nat such that
A2: m in dom Cage(C,n) and
A3: Cage(C,n).m = E-max L~Cage(C,n) by FINSEQ_2:10;
A4: Cage(C,n)/.m = E-max L~Cage(C,n) by A2,A3,PARTFUN1:def 6;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i,j be Nat such that
A5: [i,j] in Indices Gauge(C,n) and
A6: Cage(C,n)/.m = Gauge(C,n)*(i,j) by A2,GOBOARD1:def 9;
take j;
thus
A7: 1 <= j & j <= width Gauge(C,n) by A5,MATRIX_0:32;
A8: 1 <= i by A5,MATRIX_0:32;
A9: now
assume i < len Gauge(C,n);
then (E-max L~Cage(C,n))`1 < Gauge(C,n)*(len Gauge(C,n),j)`1 by A4,A6,A7,A8
,GOBOARD5:3;
then E-bound L~Cage(C,n) < Gauge(C,n)* (len Gauge(C,n),j)`1 by EUCLID:52;
hence contradiction by A7,A1,JORDAN1A:71;
end;
i <= len Gauge(C,n) by A5,MATRIX_0:32;
hence thesis by A4,A6,A9,XXREAL_0:1;
end;
theorem
ex j being Nat st 1 <= j & j <= width Gauge(C,n) & Gauge(C,
n)*(len Gauge(C,n),j) in rng Cage(C,n)
proof
consider j be Nat such that
A1: 1 <= j and
A2: j <= width Gauge(C,n) and
A3: E-min L~Cage(C,n) = Gauge(C,n)*(len Gauge(C,n),j) by Th24;
take j;
thus thesis by A1,A2,A3,SPRECT_2:45;
end;
theorem Th27:
ex i being Nat st 1 <= i & i <= len Gauge(C,n) &
S-min L~Cage(C,n) = Gauge(C,n)*(i,1)
proof
S-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:41;
then consider m be Nat such that
A1: m in dom Cage(C,n) and
A2: Cage(C,n).m = S-min L~Cage(C,n) by FINSEQ_2:10;
A3: Cage(C,n)/.m = S-min L~Cage(C,n) by A1,A2,PARTFUN1:def 6;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i,j be Nat such that
A4: [i,j] in Indices Gauge(C,n) and
A5: Cage(C,n)/.m = Gauge(C,n)*(i,j) by A1,GOBOARD1:def 9;
take i;
thus
A6: 1 <= i & i <= len Gauge(C,n) by A4,MATRIX_0:32;
A7: j <= width Gauge(C,n) by A4,MATRIX_0:32;
A8: now
assume j > 1;
then (S-min L~Cage(C,n))`2 > Gauge(C,n)*(i,1)`2 by A3,A5,A6,A7,GOBOARD5:4;
then S-bound L~Cage(C,n) > Gauge(C,n)*(i,1)`2 by EUCLID:52;
hence contradiction by A6,JORDAN1A:72;
end;
1 <= j by A4,MATRIX_0:32;
hence thesis by A3,A5,A8,XXREAL_0:1;
end;
theorem
ex i being Nat st 1 <= i & i <= len Gauge(C,n) & S-max L~
Cage(C,n) = Gauge(C,n)*(i,1)
proof
S-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:42;
then consider m be Nat such that
A1: m in dom Cage(C,n) and
A2: Cage(C,n).m = S-max L~Cage(C,n) by FINSEQ_2:10;
A3: Cage(C,n)/.m = S-max L~Cage(C,n) by A1,A2,PARTFUN1:def 6;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i,j be Nat such that
A4: [i,j] in Indices Gauge(C,n) and
A5: Cage(C,n)/.m = Gauge(C,n)*(i,j) by A1,GOBOARD1:def 9;
take i;
thus
A6: 1 <= i & i <= len Gauge(C,n) by A4,MATRIX_0:32;
A7: j <= width Gauge(C,n) by A4,MATRIX_0:32;
A8: now
assume j > 1;
then (S-max L~Cage(C,n))`2 > Gauge(C,n)*(i,1)`2 by A3,A5,A6,A7,GOBOARD5:4;
then S-bound L~Cage(C,n) > Gauge(C,n)*(i,1)`2 by EUCLID:52;
hence contradiction by A6,JORDAN1A:72;
end;
1 <= j by A4,MATRIX_0:32;
hence thesis by A3,A5,A8,XXREAL_0:1;
end;
theorem
ex i being Nat st 1 <= i & i <= len Gauge(C,n) & Gauge(C,n)
*(i,1) in rng Cage(C,n)
proof
consider i be Nat such that
A1: 1 <= i and
A2: i <= len Gauge(C,n) and
A3: S-min L~Cage(C,n) = Gauge(C,n)*(i,1) by Th27;
take i;
thus thesis by A1,A2,A3,SPRECT_2:41;
end;
theorem Th30:
ex j being Nat st 1 <= j & j <= width Gauge(C,n) &
W-min L~Cage(C,n) = Gauge(C,n)*(1,j)
proof
A1: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
W-min L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:43;
then consider m be Nat such that
A2: m in dom Cage(C,n) and
A3: Cage(C,n).m = W-min L~Cage(C,n) by FINSEQ_2:10;
A4: Cage(C,n)/.m = W-min L~Cage(C,n) by A2,A3,PARTFUN1:def 6;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i,j be Nat such that
A5: [i,j] in Indices Gauge(C,n) and
A6: Cage(C,n)/.m = Gauge(C,n)*(i,j) by A2,GOBOARD1:def 9;
take j;
thus
A7: 1 <= j & j <= width Gauge(C,n) by A5,MATRIX_0:32;
A8: i <= len Gauge(C,n) by A5,MATRIX_0:32;
A9: now
assume i > 1;
then (W-min L~Cage(C,n))`1 > Gauge(C,n)*(1,j)`1 by A4,A6,A7,A8,GOBOARD5:3;
then W-bound L~Cage(C,n) > Gauge(C,n)*(1,j)`1 by EUCLID:52;
hence contradiction by A7,A1,JORDAN1A:73;
end;
1 <= i by A5,MATRIX_0:32;
hence thesis by A4,A6,A9,XXREAL_0:1;
end;
theorem
ex j being Nat st 1 <= j & j <= width Gauge(C,n) & W-max L~
Cage(C,n) = Gauge(C,n)*(1,j)
proof
A1: len Gauge(C,n) = width Gauge(C,n) by JORDAN8:def 1;
W-max L~Cage(C,n) in rng Cage(C,n) by SPRECT_2:44;
then consider m be Nat such that
A2: m in dom Cage(C,n) and
A3: Cage(C,n).m = W-max L~Cage(C,n) by FINSEQ_2:10;
A4: Cage(C,n)/.m = W-max L~Cage(C,n) by A2,A3,PARTFUN1:def 6;
Cage(C,n) is_sequence_on Gauge(C,n) by JORDAN9:def 1;
then consider i,j be Nat such that
A5: [i,j] in Indices Gauge(C,n) and
A6: Cage(C,n)/.m = Gauge(C,n)*(i,j) by A2,GOBOARD1:def 9;
take j;
thus
A7: 1 <= j & j <= width Gauge(C,n) by A5,MATRIX_0:32;
A8: i <= len Gauge(C,n) by A5,MATRIX_0:32;
A9: now
assume i > 1;
then (W-max L~Cage(C,n))`1 > Gauge(C,n)*(1,j)`1 by A4,A6,A7,A8,GOBOARD5:3;
then W-bound L~Cage(C,n) > Gauge(C,n)*(1,j)`1 by EUCLID:52;
hence contradiction by A7,A1,JORDAN1A:73;
end;
1 <= i by A5,MATRIX_0:32;
hence thesis by A4,A6,A9,XXREAL_0:1;
end;
theorem
ex j being Nat st 1 <= j & j <= width Gauge(C,n) & Gauge(C,
n)*(1,j) in rng Cage(C,n)
proof
consider j be Nat such that
A1: 1 <= j and
A2: j <= width Gauge(C,n) and
A3: W-min L~Cage(C,n) = Gauge(C,n)*(1,j) by Th30;
take j;
thus thesis by A1,A2,A3,SPRECT_2:43;
end;