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)),0,j) misses C
let j, n be Nat; ( j <= len (Gauge (C,n)) implies cell ((Gauge (C,n)),0,j) misses C )
set G = Gauge (C,n);
A1:
j in NAT
by ORDINAL1:def 12;
assume A2:
j <= len (Gauge (C,n))
; cell ((Gauge (C,n)),0,j) misses C
A3:
len (Gauge (C,n)) = width (Gauge (C,n))
by Def1;
assume
(cell ((Gauge (C,n)),0,j)) /\ C <> {}
; XBOOLE_0:def 7 contradiction
then consider p being Point of (TOP-REAL 2) such that
A4:
p in (cell ((Gauge (C,n)),0,j)) /\ C
by SUBSET_1:4;
A5:
p in cell ((Gauge (C,n)),0,j)
by A4, XBOOLE_0:def 4;
A6:
p in C
by A4, XBOOLE_0:def 4;
4 <= len (Gauge (C,n))
by Th13;
then A7:
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);
[1,1] in Indices (Gauge (C,n))
by A3, A7, MATRIX_1:36;
then
(Gauge (C,n)) * (1,1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (1 - 2)))]|
by Def1;
then A8:
((Gauge (C,n)) * (1,1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (- 1))
by EUCLID:52;
A9:
2 |^ n > 0
by NEWTON:83;
E-bound C > W-bound C
by Th11;
then
(E-bound C) - (W-bound C) > 0
by XREAL_1:50;
then
((E-bound C) - (W-bound C)) / (2 |^ n) > 0
by A9, XREAL_1:139;
then
(((E-bound C) - (W-bound C)) / (2 |^ n)) * (- 1) < 0 * (- 1)
by XREAL_1:69;
then A10:
((Gauge (C,n)) * (1,1)) `1 < (W-bound C) + 0
by A8, XREAL_1:6;
( j = 0 or j > 0 )
by NAT_1:3;
then A11:
( 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, A11, XXREAL_0:1;
suppose
j = 0
;
contradictionthen
cell (
(Gauge (C,n)),
0,
j)
= { |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & s <= ((Gauge (C,n)) * (1,1)) `2 ) }
by GOBRD11:24;
then consider r,
s being
Real such that A12:
p = |[r,s]|
and A13:
r <= ((Gauge (C,n)) * (1,1)) `1
and
s <= ((Gauge (C,n)) * (1,1)) `2
by A5;
p `1 = r
by A12, EUCLID:52;
then
W-bound C > p `1
by A10, A13, XXREAL_0:2;
hence
contradiction
by A6, PSCOMP_1:24;
verum end; suppose
j = len (Gauge (C,n))
;
contradictionthen
cell (
(Gauge (C,n)),
0,
j)
= { |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s ) }
by A3, GOBRD11:25;
then consider r,
s being
Real such that A14:
p = |[r,s]|
and A15:
r <= ((Gauge (C,n)) * (1,1)) `1
and
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s
by A5;
p `1 = r
by A14, EUCLID:52;
then
W-bound C > p `1
by A10, A15, XXREAL_0:2;
hence
contradiction
by A6, PSCOMP_1:24;
verum end; suppose
( 1
<= j &
j < len (Gauge (C,n)) )
;
contradictionthen
cell (
(Gauge (C,n)),
0,
j)
= { |[r,s]| where r, s is Real : ( r <= ((Gauge (C,n)) * (1,1)) `1 & ((Gauge (C,n)) * (1,j)) `2 <= s & s <= ((Gauge (C,n)) * (1,(j + 1))) `2 ) }
by A1, A3, GOBRD11:26;
then consider r,
s being
Real such that A16:
p = |[r,s]|
and A17:
r <= ((Gauge (C,n)) * (1,1)) `1
and
((Gauge (C,n)) * (1,j)) `2 <= s
and
s <= ((Gauge (C,n)) * (1,(j + 1))) `2
by A5;
p `1 = r
by A16, EUCLID:52;
then
W-bound C > p `1
by A10, A17, XXREAL_0:2;
hence
contradiction
by A6, PSCOMP_1:24;
verum end;