let i, m, k, j be Element of NAT ; for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m > k & [i,j] in Indices (Gauge C,k) & [i,(j + 1)] in Indices (Gauge C,k) holds
dist ((Gauge C,m) * i,j),((Gauge C,m) * i,(j + 1)) < dist ((Gauge C,k) * i,j),((Gauge C,k) * i,(j + 1))
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ( m > k & [i,j] in Indices (Gauge C,k) & [i,(j + 1)] in Indices (Gauge C,k) implies dist ((Gauge C,m) * i,j),((Gauge C,m) * i,(j + 1)) < dist ((Gauge C,k) * i,j),((Gauge C,k) * i,(j + 1)) )
assume that
A1:
m > k
and
A2:
[i,j] in Indices (Gauge C,k)
and
A3:
[i,(j + 1)] in Indices (Gauge C,k)
; dist ((Gauge C,m) * i,j),((Gauge C,m) * i,(j + 1)) < dist ((Gauge C,k) * i,j),((Gauge C,k) * i,(j + 1))
A4:
len (Gauge C,k) < len (Gauge C,m)
by A1, JORDAN1A:50;
A5:
len (Gauge C,m) = width (Gauge C,m)
by JORDAN8:def 1;
A6:
len (Gauge C,k) = width (Gauge C,k)
by JORDAN8:def 1;
j <= width (Gauge C,k)
by A2, MATRIX_1:39;
then A7:
j <= width (Gauge C,m)
by A6, A5, A4, XXREAL_0:2;
A8:
(N-bound C) - (S-bound C) > 0
by SPRECT_1:34, XREAL_1:52;
i <= len (Gauge C,k)
by A2, MATRIX_1:39;
then A9:
i <= len (Gauge C,m)
by A4, XXREAL_0:2;
j + 1 <= width (Gauge C,k)
by A3, MATRIX_1:39;
then A10:
j + 1 <= width (Gauge C,m)
by A6, A5, A4, XXREAL_0:2;
A11:
1 <= i
by A2, MATRIX_1:39;
1 <= j + 1
by NAT_1:11;
then A12:
[i,(j + 1)] in Indices (Gauge C,m)
by A11, A9, A10, MATRIX_1:37;
1 <= j
by A2, MATRIX_1:39;
then
[i,j] in Indices (Gauge C,m)
by A11, A9, A7, MATRIX_1:37;
then A13:
dist ((Gauge C,m) * i,j),((Gauge C,m) * i,(j + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ m)
by A12, GOBRD14:19;
A14:
2 |^ k > 0
by NEWTON:102;
dist ((Gauge C,k) * i,j),((Gauge C,k) * i,(j + 1)) = ((N-bound C) - (S-bound C)) / (2 |^ k)
by A2, A3, GOBRD14:19;
hence
dist ((Gauge C,m) * i,j),((Gauge C,m) * i,(j + 1)) < dist ((Gauge C,k) * i,j),((Gauge C,k) * i,(j + 1))
by A1, A13, A14, A8, PEPIN:71, XREAL_1:78; verum