let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); for i, n being Nat st i <= len (Gauge (C,n)) holds
cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C
let i, n be Nat; ( i <= len (Gauge (C,n)) implies cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C )
set G = Gauge (C,n);
assume A1:
i <= len (Gauge (C,n))
; cell ((Gauge (C,n)),i,(len (Gauge (C,n)))) misses C
A2:
len (Gauge (C,n)) = (2 |^ n) + (1 + 2)
by Def1;
A3:
len (Gauge (C,n)) = width (Gauge (C,n))
by Def1;
assume
(cell ((Gauge (C,n)),i,(len (Gauge (C,n))))) /\ C <> {}
; XBOOLE_0:def 7 contradiction
then consider p being Point of (TOP-REAL 2) such that
A4:
p in (cell ((Gauge (C,n)),i,(len (Gauge (C,n))))) /\ C
by SUBSET_1:4;
A5:
p in cell ((Gauge (C,n)),i,(len (Gauge (C,n))))
by A4, XBOOLE_0:def 4;
A6:
p in C
by A4, XBOOLE_0:def 4;
4 <= len (Gauge (C,n))
by Th10;
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 NS = ((N-bound C) - (S-bound C)) / (2 |^ n);
[1,(width (Gauge (C,n)))] in Indices (Gauge (C,n))
by A3, A7, MATRIX_0:30;
then A8:
(Gauge (C,n)) * (1,(width (Gauge (C,n)))) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * ((width (Gauge (C,n))) - 2)))]|
by Def1;
A9:
2 |^ n > 0
by NEWTON:83;
N-bound C > S-bound C
by Th9;
then A10:
(N-bound C) - (S-bound C) > 0
by XREAL_1:50;
(((N-bound C) - (S-bound C)) / (2 |^ n)) * ((width (Gauge (C,n))) - 2) =
((((N-bound C) - (S-bound C)) / (2 |^ n)) * (2 |^ n)) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * 1)
by A2, A3
.=
((N-bound C) - (S-bound C)) + (((N-bound C) - (S-bound C)) / (2 |^ n))
by A9, XCMPLX_1:87
;
then
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
by A8, EUCLID:52;
then A11:
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 > N-bound C
by A9, A10, XREAL_1:29, XREAL_1:139;
A12:
( i = 0 or i >= 1 + 0 )
by NAT_1:9;
per cases
( i = 0 or i = len (Gauge (C,n)) or ( 1 <= i & i < len (Gauge (C,n)) ) )
by A1, A12, XXREAL_0:1;
suppose
i = 0
;
contradictionthen
cell (
(Gauge (C,n)),
i,
(width (Gauge (C,n))))
= { |[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 GOBRD11:25;
then consider r,
s being
Real such that A13:
p = |[r,s]|
and
r <= ((Gauge (C,n)) * (1,1)) `1
and A14:
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s
by A3, A5;
p `2 = s
by A13, EUCLID:52;
then
N-bound C < p `2
by A11, A14, XXREAL_0:2;
hence
contradiction
by A6, PSCOMP_1:24;
verum end; suppose
i = len (Gauge (C,n))
;
contradictionthen
cell (
(Gauge (C,n)),
i,
(width (Gauge (C,n))))
= { |[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 GOBRD11:28;
then consider r,
s being
Real such that A15:
p = |[r,s]|
and
((Gauge (C,n)) * ((len (Gauge (C,n))),1)) `1 <= r
and A16:
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s
by A3, A5;
p `2 = s
by A15, EUCLID:52;
then
N-bound C < p `2
by A11, A16, XXREAL_0:2;
hence
contradiction
by A6, PSCOMP_1:24;
verum end; suppose
( 1
<= i &
i < len (Gauge (C,n)) )
;
contradictionthen
cell (
(Gauge (C,n)),
i,
(width (Gauge (C,n))))
= { |[r,s]| where r, s is Real : ( ((Gauge (C,n)) * (i,1)) `1 <= r & r <= ((Gauge (C,n)) * ((i + 1),1)) `1 & ((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s ) }
by GOBRD11:31;
then consider r,
s being
Real such that A17:
p = |[r,s]|
and
((Gauge (C,n)) * (i,1)) `1 <= r
and
r <= ((Gauge (C,n)) * ((i + 1),1)) `1
and A18:
((Gauge (C,n)) * (1,(width (Gauge (C,n))))) `2 <= s
by A3, A5;
p `2 = s
by A17, EUCLID:52;
then
N-bound C < p `2
by A11, A18, XXREAL_0:2;
hence
contradiction
by A6, PSCOMP_1:24;
verum end;