jordan1d.miz
begin
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 by
NAT_D:def 1;
Lm3: for x,A,B,C,D be
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 be
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 be
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 ::
JORDAN1D:1
Th1: for A,B be
set st for x be
set st x
in A holds ex K be
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 be
set st x
in A holds ex K be
set st K
c= B & x
c= (
union K);
let a be
object;
assume a
in (
union A);
then
consider Z be
set such that
A2: a
in Z and
A3: Z
in A by
TARSKI:def 4;
consider K be
set such that
A4: K
c= B and
A5: Z
c= (
union K) by
A1,
A3;
ex S be
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 ::
JORDAN1D:2
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 be
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
theorem ::
JORDAN1D:3
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 ::
JORDAN1D:4
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 ::
JORDAN1D:5
Th5: for D be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 be
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 ::
JORDAN1D:6
for D be
compact non
vertical non
horizontal
Subset of (
TOP-REAL 2), k be
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 be
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 be
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 be
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(+)
is_finer_than
F(w)
proof
A9:
now
let a be
odd
Nat;
consider e be
Nat such that
A10: a
= ((2
* e)
+ 1) by
ABIAN: 9;
A11: ((2
* e)
mod 2)
=
0 by
NAT_D: 13;
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,
NAT_D: 18
.= (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 be
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,
NAT_D: 18;
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(+);
then
consider a,b be
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(,)
\/
G(,))
\/
G(,))
\/
G(,)) 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(,)
\/
G(,))
c= ((
G(,)
\/
G(,))
\/
G(,)) by
XBOOLE_1: 7;
G(,)
c= (
G(,)
\/
G(,)) by
XBOOLE_1: 7;
then
A54:
G(,)
c= ((
G(,)
\/
G(,))
\/
G(,)) by
A53;
A55: ((
G(,)
\/
G(,))
\/
G(,))
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(,)
c= ((
G(,)
\/
G(,))
\/
G(,)) by
XBOOLE_1: 7;
A62: ((
G(,)
\/
G(,))
\/
G(,))
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(,)
\/ ((
G(,)
\/
G(,))
\/
G(,))) by
A19,
A68,
XBOOLE_1: 7;
then X
c= ((
G(,)
\/ (
G(,)
\/
G(,)))
\/
G(,)) by
XBOOLE_1: 4;
hence thesis by
A38,
XBOOLE_1: 4;
end;
end;
then
A69: (
union
F(+))
c= (
union
F(w)) by
SETFAM_1: 13;
A70: (
len (
Gauge (D,i)))
= ((2
|^ i)
+ 3) by
JORDAN8:def 1;
for x be
set st x
in
F(w) holds ex K be
set st K
c=
F(+) & 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(+) 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(+)) by
A6,
Th1;
let d be
object;
assume d
in (
union
F(+));
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 be
Nat holds
P[w] from
NAT_1:sch 2(
A117,
A5);
hence thesis;
end;
theorem ::
JORDAN1D:7
Th7: ex i be
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 be
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 ::
JORDAN1D:8
ex i be
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 ::
JORDAN1D:9
Th9: ex i be
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 be
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 ::
JORDAN1D:10
ex i be
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 ::
JORDAN1D:11
Th11: ex i be
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 be
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 ::
JORDAN1D:12
ex i be
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 ::
JORDAN1D:13
Th13: ex i be
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 be
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 ::
JORDAN1D:14
ex i be
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 ::
JORDAN1D:15
Th15: ex i be
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 be
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 ::
JORDAN1D:16
ex i be
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 ::
JORDAN1D:17
Th17: ex i be
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 be
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 ::
JORDAN1D:18
ex i be
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 ::
JORDAN1D:19
Th19: ex i be
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 be
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 ::
JORDAN1D:20
ex i be
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 ::
JORDAN1D:21
Th21: ex i be
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 ::
JORDAN1D:22
ex i be
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 ::
JORDAN1D:23
ex i be
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 ::
JORDAN1D:24
Th24: ex j be
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 ::
JORDAN1D:25
ex j be
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 ::
JORDAN1D:26
ex j be
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 ::
JORDAN1D:27
Th27: ex i be
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 ::
JORDAN1D:28
ex i be
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 ::
JORDAN1D:29
ex i be
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 ::
JORDAN1D:30
Th30: ex j be
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 ::
JORDAN1D:31
ex j be
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 ::
JORDAN1D:32
ex j be
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;