let m, i, n be 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 and
A3: 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)) )
A4: (n -' m) + 1 <= 2 |^ (n -' m) by NEWTON:85;
i + 1 <= (2 |^ n) + (2 + 1) by A3, JORDAN8:def 1;
then i + 1 <= ((2 |^ n) + 2) + 1 ;
then i <= (2 |^ n) + 2 by XREAL_1:6;
then i - 2 <= 2 |^ n by XREAL_1:20;
then i - 2 <= 2 |^ (m + (n -' m)) by A1, XREAL_1:235;
then (i - 2) * 1 <= (2 |^ m) * (2 |^ (n -' m)) by NEWTON:8;
then (i - 2) / (2 |^ (n -' m)) <= (2 |^ m) / 1 by A4, XREAL_1:102;
then ((i - 2) / (2 |^ (n -' m))) + 3 <= (2 |^ m) + 3 by XREAL_1:6;
then A5: ((i - 2) / (2 |^ (n -' m))) + 3 <= len (Gauge (C,m)) by JORDAN8:def 1;
set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A6: ((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/] by INT_1:def 6;
(n -' m) + 1 >= 0 + 1 by XREAL_1:6;
then 0 + 1 <= 2 |^ (n -' m) by A4, XXREAL_0:2;
then A7: (- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by XREAL_1:120;
1 - 2 <= i - 2 by A2, XREAL_1:9;
then (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:72;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A7, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:6;
then [\(((i - 2) / (2 |^ (n -' m))) + 2)/] >= 1 + 0 by A6, INT_1:7;
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 6;
then [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= (((i - 2) / (2 |^ (n -' m))) + 2) + 1 by XREAL_1:6;
hence [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) by A5, XXREAL_0:2; :: thesis: verum