let C be compact non horizontal non vertical Subset of (TOP-REAL 2); for n, m being Nat st n <= m & n is_sufficiently_large_for C holds
m is_sufficiently_large_for C
let n, m be Nat; ( n <= m & n is_sufficiently_large_for C implies m is_sufficiently_large_for C )
assume that
A1:
n <= m
and
A2:
n is_sufficiently_large_for C
; m is_sufficiently_large_for C
consider j being Nat such that
A3:
j < width (Gauge (C,n))
and
A4:
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C
by A2, JORDAN1H:def 3;
set iin = X-SpanStart (C,n);
set iim = X-SpanStart (C,m);
n >= 1
by A2, JORDAN1H:51;
then A5:
X-SpanStart (C,m) = ((2 |^ (m -' n)) * ((X-SpanStart (C,n)) - 2)) + 2
by A1, Th27;
A6:
j > 1
proof
A7:
(X-SpanStart (C,n)) -' 1
<= len (Gauge (C,n))
by JORDAN1H:50;
assume A8:
j <= 1
;
contradiction
per cases
( j = 0 or j = 1 )
by A8, NAT_1:25;
suppose A9:
j = 0
;
contradiction
width (Gauge (C,n)) >= 0
;
then A10:
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0) is
empty
by A7, JORDAN1A:24;
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
c= UBD C
by A7, JORDAN1A:49;
hence
contradiction
by A4, A9, A10, JORDAN2C:24, XBOOLE_1:68;
verum end; suppose A11:
j = 1
;
contradictionset i1 =
X-SpanStart (
C,
n);
A12:
(X-SpanStart (C,n)) -' 1
<= X-SpanStart (
C,
n)
by NAT_D:44;
X-SpanStart (
C,
n)
< len (Gauge (C,n))
by JORDAN1H:49;
then A13:
(X-SpanStart (C,n)) -' 1
< len (Gauge (C,n))
by A12, XXREAL_0:2;
BDD C c= C `
by JORDAN2C:25;
then A14:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1)
c= C `
by A4, A11;
UBD C is_outside_component_of C
by JORDAN2C:68;
then A15:
UBD C is_a_component_of C `
by JORDAN2C:def 3;
width (Gauge (C,n)) <> 0
by MATRIX_0:def 10;
then A16:
0 + 1
<= width (Gauge (C,n))
by NAT_1:14;
then A17:
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1) is
empty
by A7, JORDAN1A:24;
A18:
1
<= (X-SpanStart (C,n)) -' 1
by JORDAN1H:50;
0 < width (Gauge (C,n))
by A16;
then
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),0)) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(0 + 1))) = LSeg (
((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(0 + 1))),
((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(0 + 1))))
by A13, A18, GOBOARD5:26;
then A19:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
meets cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(0 + 1))
by XBOOLE_0:def 7;
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
c= UBD C
by A7, JORDAN1A:49;
then
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1)
c= UBD C
by A16, A13, A19, A15, A14, GOBOARD9:4, JORDAN1A:25;
hence
contradiction
by A4, A11, A17, JORDAN2C:24, XBOOLE_1:68;
verum end; end;
end;
then
((2 |^ (m -' n)) * (j - 2)) + 2 > 1
by A1, A3, JORDAN1A:32;
then reconsider j1 = ((2 |^ (m -' n)) * (j - 2)) + 2 as Element of NAT by INT_1:3;
X-SpanStart (C,n) > 2
by JORDAN1H:49;
then A20:
X-SpanStart (C,n) >= 2 + 1
by NAT_1:13;
A21:
j + 1 < width (Gauge (C,n))
proof
assume
j + 1
>= width (Gauge (C,n))
;
contradiction
then A22:
(
j + 1
> width (Gauge (C,n)) or
j + 1
= width (Gauge (C,n)) )
by XXREAL_0:1;
A23:
(X-SpanStart (C,n)) -' 1
<= len (Gauge (C,n))
by JORDAN1H:50;
per cases
( j = width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) )
by A3, A22, NAT_1:13;
suppose A24:
j = width (Gauge (C,n))
;
contradictionA25:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(width (Gauge (C,n))))
c= UBD C
by A23, JORDAN1A:50;
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
j) is
empty
by A23, A24, JORDAN1A:24;
hence
contradiction
by A4, A24, A25, JORDAN2C:24, XBOOLE_1:68;
verum end; suppose
j + 1
= width (Gauge (C,n))
;
contradictionthen A26:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((width (Gauge (C,n))) -' 1))
c= BDD C
by A4, NAT_D:34;
BDD C c= C `
by JORDAN2C:25;
then A27:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((width (Gauge (C,n))) -' 1))
c= C `
by A26;
A28:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(width (Gauge (C,n))))
c= UBD C
by A23, JORDAN1A:50;
set i1 =
X-SpanStart (
C,
n);
A29:
(X-SpanStart (C,n)) -' 1
<= X-SpanStart (
C,
n)
by NAT_D:44;
X-SpanStart (
C,
n)
< len (Gauge (C,n))
by JORDAN1H:49;
then A30:
(X-SpanStart (C,n)) -' 1
< len (Gauge (C,n))
by A29, XXREAL_0:2;
UBD C is_outside_component_of C
by JORDAN2C:68;
then A31:
UBD C is_a_component_of C `
by JORDAN2C:def 3;
(width (Gauge (C,n))) -' 1
<= width (Gauge (C,n))
by NAT_D:44;
then A32:
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((width (Gauge (C,n))) -' 1)) is
empty
by A23, JORDAN1A:24;
A33:
(width (Gauge (C,n))) - 1
< width (Gauge (C,n))
by XREAL_1:146;
A34:
1
<= (X-SpanStart (C,n)) -' 1
by JORDAN1H:50;
A35:
width (Gauge (C,n)) <> 0
by MATRIX_0:def 10;
then
((width (Gauge (C,n))) -' 1) + 1
= width (Gauge (C,n))
by NAT_1:14, XREAL_1:235;
then
(cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))) /\ (cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),((width (Gauge (C,n))) -' 1))) = LSeg (
((Gauge (C,n)) * (((X-SpanStart (C,n)) -' 1),(width (Gauge (C,n))))),
((Gauge (C,n)) * ((((X-SpanStart (C,n)) -' 1) + 1),(width (Gauge (C,n))))))
by A30, A33, A34, GOBOARD5:26;
then A36:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(width (Gauge (C,n))))
meets cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((width (Gauge (C,n))) -' 1))
by XBOOLE_0:def 7;
(width (Gauge (C,n))) -' 1
< width (Gauge (C,n))
by A35, A33, NAT_1:14, XREAL_1:233;
then
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((width (Gauge (C,n))) -' 1))
c= UBD C
by A28, A30, A36, A31, A27, GOBOARD9:4, JORDAN1A:25;
hence
contradiction
by A26, A32, JORDAN2C:24, XBOOLE_1:68;
verum end; end;
end;
X-SpanStart (C,n) < len (Gauge (C,n))
by JORDAN1H:49;
then
cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),j1) c= cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j)
by A1, A5, A20, A6, A21, JORDAN1A:48;
then A37:
cell ((Gauge (C,m)),((X-SpanStart (C,m)) -' 1),j1) c= BDD C
by A4;
j1 < width (Gauge (C,m))
by A1, A3, A6, JORDAN1A:32;
hence
m is_sufficiently_large_for C
by A37, JORDAN1H:def 3; verum