let m, n, i be Element of NAT ; :: thesis: for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge C,n) holds
( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge C,m) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); :: thesis: ( m <= n & 1 <= i & i + 1 <= len (Gauge C,n) implies ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge C,m) ) )
assume that
A1: m <= n and
A2: ( 1 <= i & i + 1 <= len (Gauge C,n) ) ; :: thesis: ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge C,m) )
set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A3: ((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/] by INT_1:def 4;
A4: (n -' m) + 1 >= 0 + 1 by XREAL_1:8;
A5: (n -' m) + 1 <= 2 |^ (n -' m) by NEWTON:104;
then A6: 0 + 1 <= 2 |^ (n -' m) by A4, XXREAL_0:2;
1 - 2 <= i - 2 by A2, XREAL_1:11;
then A7: (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:74;
(- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by A6, XREAL_1:122;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A7, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:8;
then [\(((i - 2) / (2 |^ (n -' m))) + 2)/] >= 1 + 0 by A3, INT_1:20;
hence 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] ; :: thesis: [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge C,m)
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] <= ((i - 2) / (2 |^ (n -' m))) + 2 by INT_1:def 4;
then A8: [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= (((i - 2) / (2 |^ (n -' m))) + 2) + 1 by XREAL_1:8;
i + 1 <= (2 |^ n) + (2 + 1) by A2, JORDAN8:def 1;
then i + 1 <= ((2 |^ n) + 2) + 1 ;
then i <= (2 |^ n) + 2 by XREAL_1:8;
then i - 2 <= 2 |^ n by XREAL_1:22;
then i - 2 <= 2 |^ (m + (n -' m)) by A1, XREAL_1:237;
then (i - 2) * 1 <= (2 |^ m) * (2 |^ (n -' m)) by NEWTON:13;
then (i - 2) / (2 |^ (n -' m)) <= (2 |^ m) / 1 by A5, XREAL_1:104;
then ((i - 2) / (2 |^ (n -' m))) + 3 <= (2 |^ m) + 3 by XREAL_1:8;
then ((i - 2) / (2 |^ (n -' m))) + 3 <= len (Gauge C,m) by JORDAN8:def 1;
hence [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge C,m) by A8, XXREAL_0:2; :: thesis: verum