let n be Nat; :: thesis: 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); :: thesis: ( n is_sufficiently_large_for C implies n >= 1 )
A1: 2 |^ 0 = 1 by NEWTON:4;
assume n is_sufficiently_large_for C ; :: thesis: 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 ; :: thesis: 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 ; :: thesis: contradiction
per cases ( j = 0 or j = 1 ) by A7, NAT_1:25;
suppose A10: j = 1 ; :: thesis: contradiction
set 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; :: thesis: 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)) ; :: thesis: 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)) ; :: thesis: 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; :: thesis: verum
end;
suppose j + 1 = width (Gauge (C,n)) ; :: thesis: contradiction
then 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; :: thesis: 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 ) ; :: thesis: contradiction
hence contradiction by A5; :: thesis: verum
end;
suppose A34: j = 2 ; :: thesis: contradiction
A35: X-SpanStart (C,0) = 1 + 2 by A1, NAT_2:8;
then (X-SpanStart (C,0)) -' 1 = (X-SpanStart (C,0)) - 1 by NAT_D:39
.= 2 by A35 ;
hence contradiction by A3, A4, A34, JORDAN1B:18; :: thesis: verum
end;
suppose ( j = 3 or j = 4 ) ; :: thesis: contradiction
hence contradiction by A18, A20, A1, A4; :: thesis: verum
end;
end;