let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); for j, n being Nat st j <= len (Gauge C,n) holds
cell (Gauge C,n),(len (Gauge C,n)),j misses C
let j, n be Nat; ( j <= len (Gauge C,n) implies cell (Gauge C,n),(len (Gauge C,n)),j misses C )
set G = Gauge C,n;
A1:
j in NAT
by ORDINAL1:def 13;
assume A2:
j <= len (Gauge C,n)
; cell (Gauge C,n),(len (Gauge C,n)),j misses C
A3:
len (Gauge C,n) = (2 |^ n) + (1 + 2)
by Def1;
A4:
len (Gauge C,n) = width (Gauge C,n)
by Def1;
assume
(cell (Gauge C,n),(len (Gauge C,n)),j) /\ C <> {}
; XBOOLE_0:def 7 contradiction
then consider p being Point of (TOP-REAL 2) such that
A5:
p in (cell (Gauge C,n),(len (Gauge C,n)),j) /\ C
by SUBSET_1:10;
A6:
p in cell (Gauge C,n),(len (Gauge C,n)),j
by A5, XBOOLE_0:def 4;
A7:
p in C
by A5, XBOOLE_0:def 4;
4 <= len (Gauge C,n)
by Th13;
then A8:
1 <= len (Gauge C,n)
by XXREAL_0:2;
set W = W-bound C;
set S = S-bound C;
set E = E-bound C;
set N = N-bound C;
set EW = ((E-bound C) - (W-bound C)) / (2 |^ n);
[(len (Gauge C,n)),1] in Indices (Gauge C,n)
by A4, A8, MATRIX_1:37;
then A9:
(Gauge C,n) * (len (Gauge C,n)),1 = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (Gauge C,n)) - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]|
by Def1;
A10:
2 |^ n > 0
by NEWTON:102;
E-bound C > W-bound C
by Th11;
then A11:
(E-bound C) - (W-bound C) > 0
by XREAL_1:52;
(((E-bound C) - (W-bound C)) / (2 |^ n)) * ((len (Gauge C,n)) - 2) =
((((E-bound C) - (W-bound C)) / (2 |^ n)) * (2 |^ n)) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * 1)
by A3
.=
((E-bound C) - (W-bound C)) + (((E-bound C) - (W-bound C)) / (2 |^ n))
by A10, XCMPLX_1:88
;
then
((Gauge C,n) * (len (Gauge C,n)),1) `1 = (E-bound C) + (((E-bound C) - (W-bound C)) / (2 |^ n))
by A9, EUCLID:56;
then A12:
((Gauge C,n) * (len (Gauge C,n)),1) `1 > E-bound C
by A10, A11, XREAL_1:31, XREAL_1:141;
( j = 0 or j > 0 )
by NAT_1:3;
then A13:
( j = 0 or j >= 1 + 0 )
by NAT_1:9;
per cases
( j = 0 or j = len (Gauge C,n) or ( 1 <= j & j < len (Gauge C,n) ) )
by A2, A13, XXREAL_0:1;
suppose
j = 0
;
contradictionthen
cell (Gauge C,n),
(len (Gauge C,n)),
j = { |[r,s]| where r, s is Real : ( ((Gauge C,n) * (len (Gauge C,n)),1) `1 <= r & s <= ((Gauge C,n) * 1,1) `2 ) }
by GOBRD11:27;
then consider r,
s being
Real such that A14:
p = |[r,s]|
and A15:
((Gauge C,n) * (len (Gauge C,n)),1) `1 <= r
and
s <= ((Gauge C,n) * 1,1) `2
by A6;
p `1 = r
by A14, EUCLID:56;
then
E-bound C < p `1
by A12, A15, XXREAL_0:2;
hence
contradiction
by A7, PSCOMP_1:71;
verum end; suppose
j = len (Gauge C,n)
;
contradictionthen
cell (Gauge C,n),
(len (Gauge C,n)),
j = { |[r,s]| where r, s is Real : ( ((Gauge C,n) * (len (Gauge C,n)),1) `1 <= r & ((Gauge C,n) * 1,(width (Gauge C,n))) `2 <= s ) }
by A4, GOBRD11:28;
then consider r,
s being
Real such that A16:
p = |[r,s]|
and A17:
((Gauge C,n) * (len (Gauge C,n)),1) `1 <= r
and
((Gauge C,n) * 1,(width (Gauge C,n))) `2 <= s
by A6;
p `1 = r
by A16, EUCLID:56;
then
E-bound C < p `1
by A12, A17, XXREAL_0:2;
hence
contradiction
by A7, PSCOMP_1:71;
verum end; suppose
( 1
<= j &
j < len (Gauge C,n) )
;
contradictionthen
cell (Gauge C,n),
(len (Gauge C,n)),
j = { |[r,s]| where r, s is Real : ( ((Gauge C,n) * (len (Gauge C,n)),1) `1 <= r & ((Gauge C,n) * 1,j) `2 <= s & s <= ((Gauge C,n) * 1,(j + 1)) `2 ) }
by A1, A4, GOBRD11:29;
then consider r,
s being
Real such that A18:
p = |[r,s]|
and A19:
((Gauge C,n) * (len (Gauge C,n)),1) `1 <= r
and
((Gauge C,n) * 1,j) `2 <= s
and
s <= ((Gauge C,n) * 1,(j + 1)) `2
by A6;
p `1 = r
by A18, EUCLID:56;
then
E-bound C < p `1
by A12, A19, XXREAL_0:2;
hence
contradiction
by A7, PSCOMP_1:71;
verum end;