let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: 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; :: thesis: ( i <= len (Gauge C,n) implies cell (Gauge C,n),i,(len (Gauge C,n)) misses C )
set G = Gauge C,n;
A1:
i in NAT
by ORDINAL1:def 13;
assume A2:
i <= len (Gauge C,n)
; :: thesis: cell (Gauge C,n),i,(len (Gauge C,n)) misses C
A3:
( len (Gauge C,n) = (2 |^ n) + (1 + 2) & len (Gauge C,n) = width (Gauge C,n) )
by Def1;
assume
(cell (Gauge C,n),i,(len (Gauge C,n))) /\ C <> {}
; :: according to XBOOLE_0:def 7 :: thesis: 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:10;
A5:
( p in cell (Gauge C,n),i,(len (Gauge C,n)) & p in C )
by A4, XBOOLE_0:def 4;
4 <= len (Gauge C,n)
by Th13;
then A6:
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, A6, MATRIX_1:37;
then A7:
(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;
A8:
2 |^ n > 0
by NEWTON:102;
N-bound C > S-bound C
by Th12;
then
(N-bound C) - (S-bound C) > 0
by XREAL_1:52;
then A9:
((N-bound C) - (S-bound C)) / (2 |^ n) > 0
by A8, XREAL_1:141;
(((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 A3
.=
((N-bound C) - (S-bound C)) + (((N-bound C) - (S-bound C)) / (2 |^ n))
by A8, XCMPLX_1:88
;
then
((Gauge C,n) * 1,(width (Gauge C,n))) `2 = (N-bound C) + (((N-bound C) - (S-bound C)) / (2 |^ n))
by A7, EUCLID:56;
then A10:
((Gauge C,n) * 1,(width (Gauge C,n))) `2 > N-bound C
by A9, XREAL_1:31;
( i = 0 or i > 0 )
by NAT_1:3;
then A11:
( 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 A2, A11, XXREAL_0:1;
suppose
i = 0
;
:: thesis: 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 A12:
p = |[r,s]|
and A13:
(
r <= ((Gauge C,n) * 1,1) `1 &
((Gauge C,n) * 1,(width (Gauge C,n))) `2 <= s )
by A3, A5;
p `2 = s
by A12, EUCLID:56;
then
(
N-bound C < p `2 &
p `2 <= N-bound C )
by A5, A10, A13, PSCOMP_1:71, XXREAL_0:2;
hence
contradiction
;
:: thesis: verum end; suppose
i = len (Gauge C,n)
;
:: thesis: 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 A14:
p = |[r,s]|
and A15:
(
((Gauge C,n) * (len (Gauge C,n)),1) `1 <= r &
((Gauge C,n) * 1,(width (Gauge C,n))) `2 <= s )
by A3, A5;
p `2 = s
by A14, EUCLID:56;
then
(
N-bound C < p `2 &
p `2 <= N-bound C )
by A5, A10, A15, PSCOMP_1:71, XXREAL_0:2;
hence
contradiction
;
:: thesis: verum end; suppose
( 1
<= i &
i < len (Gauge C,n) )
;
:: thesis: 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 A1, GOBRD11:31;
then consider r,
s being
Real such that A16:
p = |[r,s]|
and A17:
(
((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 A3, A5;
p `2 = s
by A16, EUCLID:56;
then
(
N-bound C < p `2 &
p `2 <= N-bound C )
by A5, A10, A17, PSCOMP_1:71, XXREAL_0:2;
hence
contradiction
;
:: thesis: verum end;