let n be Nat; for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st n is_sufficiently_large_for C holds
n >= 1
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ( n is_sufficiently_large_for C implies n >= 1 )
A1:
2 |^ 0 = 1
by NEWTON:4;
assume
n is_sufficiently_large_for C
; n >= 1
then consider j being Nat such that
A2:
j < width (Gauge (C,n))
and
A3:
cell ((Gauge (C,n)),((X-SpanStart (C,n)) -' 1),j) c= BDD C
;
assume
n < 1
; contradiction
then A4:
n = 0
by NAT_1:14;
A5:
j > 1
proof
A6:
(X-SpanStart (C,n)) -' 1
<= len (Gauge (C,n))
by Th50;
assume A7:
j <= 1
;
contradiction
per cases
( j = 0 or j = 1 )
by A7, NAT_1:25;
suppose A8:
j = 0
;
contradiction
0 <= width (Gauge (C,n))
;
then A9:
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0) is
empty
by A6, JORDAN1A:24;
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
c= UBD C
by A6, JORDAN1A:49;
hence
contradiction
by A3, A8, A9, JORDAN2C:24, XBOOLE_1:68;
verum end; suppose A10:
j = 1
;
contradictionset i1 =
X-SpanStart (
C,
n);
UBD C is_outside_component_of C
by JORDAN2C:68;
then A11:
UBD C is_a_component_of C `
by JORDAN2C:def 3;
(
X-SpanStart (
C,
n)
< len (Gauge (C,n)) &
(X-SpanStart (C,n)) -' 1
<= X-SpanStart (
C,
n) )
by Th49, NAT_D:44;
then A12:
(X-SpanStart (C,n)) -' 1
< len (Gauge (C,n))
by XXREAL_0:2;
BDD C c= C `
by JORDAN2C:25;
then A13:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1)
c= C `
by A3, A10;
A14:
width (Gauge (C,n)) <> 0
by MATRIX_0:def 10;
then A15:
0 + 1
<= width (Gauge (C,n))
by NAT_1:14;
then A16:
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1) is
empty
by A6, JORDAN1A:24;
1
<= (X-SpanStart (C,n)) -' 1
by Th50;
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 A14, A12, GOBOARD5:26;
then A17:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
meets cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(0 + 1))
;
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
0)
c= UBD C
by A6, JORDAN1A:49;
then
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),1)
c= UBD C
by A15, A12, A17, A11, A13, GOBOARD9:4, JORDAN1A:25;
hence
contradiction
by A3, A10, A16, JORDAN2C:24, XBOOLE_1:68;
verum end; end;
end;
A18:
width (Gauge (C,n)) = (2 |^ n) + 3
by JORDAN1A:28;
then A19:
j <= 3 + 1
by A2, A4, NEWTON:4;
A20:
j + 1 < width (Gauge (C,n))
proof
assume
j + 1
>= width (Gauge (C,n))
;
contradiction
then A21:
(
j + 1
> width (Gauge (C,n)) or
j + 1
= width (Gauge (C,n)) )
by XXREAL_0:1;
A22:
(X-SpanStart (C,n)) -' 1
<= len (Gauge (C,n))
by Th50;
per cases
( j = width (Gauge (C,n)) or j + 1 = width (Gauge (C,n)) )
by A2, A21, NAT_1:13;
suppose A23:
j = width (Gauge (C,n))
;
contradiction
( not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(width (Gauge (C,n)))) is
empty &
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(width (Gauge (C,n))))
c= UBD C )
by A22, JORDAN1A:24, JORDAN1A:50;
hence
contradiction
by A3, A23, JORDAN2C:24, XBOOLE_1:68;
verum end; suppose
j + 1
= width (Gauge (C,n))
;
contradictionthen A24:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((width (Gauge (C,n))) -' 1))
c= BDD C
by A3, NAT_D:34;
BDD C c= C `
by JORDAN2C:25;
then A25:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((width (Gauge (C,n))) -' 1))
c= C `
by A24;
set i1 =
X-SpanStart (
C,
n);
A26:
(width (Gauge (C,n))) - 1
< width (Gauge (C,n))
by XREAL_1:146;
UBD C is_outside_component_of C
by JORDAN2C:68;
then A27:
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 A28:
not
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
((width (Gauge (C,n))) -' 1)) is
empty
by A22, JORDAN1A:24;
A29:
cell (
(Gauge (C,n)),
((X-SpanStart (C,n)) -' 1),
(width (Gauge (C,n))))
c= UBD C
by A22, JORDAN1A:50;
A30:
1
<= (X-SpanStart (C,n)) -' 1
by Th50;
(
X-SpanStart (
C,
n)
< len (Gauge (C,n)) &
(X-SpanStart (C,n)) -' 1
<= X-SpanStart (
C,
n) )
by Th49, NAT_D:44;
then A31:
(X-SpanStart (C,n)) -' 1
< len (Gauge (C,n))
by XXREAL_0:2;
A32:
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 A31, A26, A30, GOBOARD5:26;
then A33:
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))
;
(width (Gauge (C,n))) -' 1
< width (Gauge (C,n))
by A32, A26, 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 A29, A31, A33, A27, A25, GOBOARD9:4, JORDAN1A:25;
hence
contradiction
by A24, A28, JORDAN2C:24, XBOOLE_1:68;
verum end; end;
end;
not not j = 0 & ... & not j = 4
by A19;
per cases then
( j = 0 or j = 1 or j = 2 or j = 3 or j = 4 )
;
suppose
(
j = 0 or
j = 1 )
;
contradictionhence
contradiction
by A5;
verum end; suppose
(
j = 3 or
j = 4 )
;
contradictionend; end;