let C be non empty compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: for n, i1, i2 being Nat st 1 <= i1 & i1 + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i1,((width (Gauge C,n)) -' 1) & 1 <= i2 & i2 + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i2,((width (Gauge C,n)) -' 1) holds
i1 = i2
let n, i1, i2 be Nat; :: thesis: ( 1 <= i1 & i1 + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i1,((width (Gauge C,n)) -' 1) & 1 <= i2 & i2 + 1 <= len (Gauge C,n) & N-min C in cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1) & N-min C <> (Gauge C,n) * i2,((width (Gauge C,n)) -' 1) implies i1 = i2 )
A1:
( i1 in NAT & i2 in NAT )
by ORDINAL1:def 13;
set G = Gauge C,n;
set j = (width (Gauge C,n)) -' 1;
assume that
A2:
( 1 <= i1 & i1 + 1 <= len (Gauge C,n) )
and
A3:
N-min C in cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1)
and
A4:
N-min C <> (Gauge C,n) * i1,((width (Gauge C,n)) -' 1)
and
A5:
( 1 <= i2 & i2 + 1 <= len (Gauge C,n) )
and
A6:
N-min C in cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1)
and
A7:
N-min C <> (Gauge C,n) * i2,((width (Gauge C,n)) -' 1)
and
A8:
i1 <> i2
; :: thesis: contradiction
A9:
( i1 < len (Gauge C,n) & i2 < len (Gauge C,n) & len (Gauge C,n) = width (Gauge C,n) )
by A2, A5, JORDAN8:def 1, NAT_1:13;
A10:
cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1) meets cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1)
by A3, A6, XBOOLE_0:3;
A11:
( len (Gauge C,n) = (2 |^ n) + 3 & len (Gauge C,n) = width (Gauge C,n) )
by JORDAN8:def 1;
A12:
2 |^ n >= n + 1
by NEWTON:104;
then
len (Gauge C,n) >= (n + 1) + 3
by A11, XREAL_1:8;
then A13:
( len (Gauge C,n) >= 1 + (n + 3) & 1 + (n + 3) > 1 + 0 )
by XREAL_1:8;
then
len (Gauge C,n) > 1
by XXREAL_0:2;
then A14:
len (Gauge C,n) >= 1 + 1
by NAT_1:13;
then A15:
1 <= (width (Gauge C,n)) -' 1
by A9, JORDAN5B:2;
A16:
((width (Gauge C,n)) -' 1) + 1 = len (Gauge C,n)
by A9, A13, XREAL_1:237, XXREAL_0:2;
then A17:
(width (Gauge C,n)) -' 1 < len (Gauge C,n)
by NAT_1:13;
per cases
( i1 < i2 or i2 < i1 )
by A8, XXREAL_0:1;
suppose A18:
i1 < i2
;
:: thesis: contradictionthen A19:
(i2 -' i1) + i1 = i2
by XREAL_1:237;
then
i2 -' i1 <= 1
by A1, A9, A10, A15, A17, JORDAN8:10;
then
(
i2 -' i1 < 1 or
i2 -' i1 = 1 )
by XXREAL_0:1;
then
(
i2 -' i1 = 0 or
i2 -' i1 = 1 )
by NAT_1:14;
then
(cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1)) /\ (cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1)) = LSeg ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)),
((Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1))
by A1, A9, A14, A17, A18, A19, GOBOARD5:26, JORDAN5B:2;
then A20:
N-min C in LSeg ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)),
((Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1))
by A3, A6, XBOOLE_0:def 4;
A21:
[i2,((width (Gauge C,n)) -' 1)] in Indices (Gauge C,n)
by A5, A9, A15, A17, MATRIX_1:37;
1
<= ((width (Gauge C,n)) -' 1) + 1
by NAT_1:12;
then A22:
[i2,(((width (Gauge C,n)) -' 1) + 1)] in Indices (Gauge C,n)
by A5, A9, A16, MATRIX_1:37;
set x =
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2));
set y1 =
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2));
set y2 =
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 1));
A23:
(((width (Gauge C,n)) -' 1) + 1) - (1 + 1) = ((width (Gauge C,n)) -' 1) - 1
;
A24:
(Gauge C,n) * i2,
((width (Gauge C,n)) -' 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2)))]|
by A21, JORDAN8:def 1;
(Gauge C,n) * i2,
(((width (Gauge C,n)) -' 1) + 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 1)))]|
by A22, A23, JORDAN8:def 1;
then A25:
(
((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2)) &
((Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i2 - 2)) )
by A24, EUCLID:56;
then
LSeg ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)),
((Gauge C,n) * i2,(((width (Gauge C,n)) -' 1) + 1)) is
vertical
by SPPOL_1:37;
then A26:
(N-min C) `1 = ((Gauge C,n) * i2,((width (Gauge C,n)) -' 1)) `1
by A20, SPPOL_1:64;
(width (Gauge C,n)) -' 1 =
(((2 |^ n) + 2) + 1) -' 1
by A11
.=
(2 |^ n) + 2
by NAT_D:34
;
then
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2) = (N-bound C) - (S-bound C)
by A12, XCMPLX_1:88;
hence
contradiction
by A7, A24, A25, A26, EUCLID:56;
:: thesis: verum end; suppose A27:
i2 < i1
;
:: thesis: contradictionthen A28:
(i1 -' i2) + i2 = i1
by XREAL_1:237;
then
i1 -' i2 <= 1
by A1, A9, A10, A15, A17, JORDAN8:10;
then
(
i1 -' i2 < 1 or
i1 -' i2 = 1 )
by XXREAL_0:1;
then
(
i1 -' i2 = 0 or
i1 -' i2 = 1 )
by NAT_1:14;
then
(cell (Gauge C,n),i2,((width (Gauge C,n)) -' 1)) /\ (cell (Gauge C,n),i1,((width (Gauge C,n)) -' 1)) = LSeg ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)),
((Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1))
by A1, A9, A14, A17, A27, A28, GOBOARD5:26, JORDAN5B:2;
then A29:
N-min C in LSeg ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)),
((Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1))
by A3, A6, XBOOLE_0:def 4;
A30:
[i1,((width (Gauge C,n)) -' 1)] in Indices (Gauge C,n)
by A2, A9, A15, A17, MATRIX_1:37;
1
<= ((width (Gauge C,n)) -' 1) + 1
by NAT_1:12;
then A31:
[i1,(((width (Gauge C,n)) -' 1) + 1)] in Indices (Gauge C,n)
by A2, A9, A16, MATRIX_1:37;
set x =
(W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2));
set y1 =
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2));
set y2 =
(S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 1));
A32:
(((width (Gauge C,n)) -' 1) + 1) - (1 + 1) = ((width (Gauge C,n)) -' 1) - 1
;
A33:
(Gauge C,n) * i1,
((width (Gauge C,n)) -' 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2)))]|
by A30, JORDAN8:def 1;
(Gauge C,n) * i1,
(((width (Gauge C,n)) -' 1) + 1) = |[((W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2))),((S-bound C) + ((((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 1)))]|
by A31, A32, JORDAN8:def 1;
then A34:
(
((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2)) &
((Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1)) `1 = (W-bound C) + ((((E-bound C) - (W-bound C)) / (2 |^ n)) * (i1 - 2)) )
by A33, EUCLID:56;
then
LSeg ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)),
((Gauge C,n) * i1,(((width (Gauge C,n)) -' 1) + 1)) is
vertical
by SPPOL_1:37;
then A35:
(N-min C) `1 = ((Gauge C,n) * i1,((width (Gauge C,n)) -' 1)) `1
by A29, SPPOL_1:64;
(width (Gauge C,n)) -' 1 =
(((2 |^ n) + 2) + 1) -' 1
by A11
.=
(2 |^ n) + 2
by NAT_D:34
;
then
(((N-bound C) - (S-bound C)) / (2 |^ n)) * (((width (Gauge C,n)) -' 1) - 2) = (N-bound C) - (S-bound C)
by A12, XCMPLX_1:88;
hence
contradiction
by A4, A33, A34, A35, EUCLID:56;
:: thesis: verum end;