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
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT
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 [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT )
assume that
m <= n and
A1: ( 1 <= i & i + 1 <= len (Gauge C,n) ) ; :: thesis: [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT
set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1) ;
then A2: ((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/] by INT_1:def 4;
A3: (n -' m) + 1 >= 0 + 1 by XREAL_1:8;
(n -' m) + 1 <= 2 |^ (n -' m) by NEWTON:104;
then A5: 0 + 1 <= 2 |^ (n -' m) by A3, XXREAL_0:2;
1 - 2 <= i - 2 by A1, XREAL_1:11;
then A6: (- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m)) by XREAL_1:74;
(- 1) / 1 <= (- 1) / (2 |^ (n -' m)) by A5, XREAL_1:122;
then - 1 <= (i - 2) / (2 |^ (n -' m)) by A6, XXREAL_0:2;
then (- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1 by XREAL_1:8;
hence [\(((i - 2) / (2 |^ (n -' m))) + 2)/] is Element of NAT by A2, INT_1:16; :: thesis: verum