let m, n, i be Element of NAT ; :: thesis: for D being non empty Subset of (TOP-REAL 2) st m <= n & 1 < i & i < len (Gauge D,m) holds
( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < len (Gauge D,n) )
let D be non empty Subset of (TOP-REAL 2); :: thesis: ( m <= n & 1 < i & i < len (Gauge D,m) implies ( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < len (Gauge D,n) ) )
assume that
A1: m <= n and
A2: 1 < i and
A3: i < len (Gauge D,m) ; :: thesis: ( 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 & ((2 |^ (n -' m)) * (i - 2)) + 2 < len (Gauge D,n) )
1 + 1 <= i by A2, NAT_1:13;
then reconsider i2 = i - 2 as Element of NAT by INT_1:18;
0 < ((2 |^ (n -' m)) * i2) + 1 ;
then 0 + 1 < (((2 |^ (n -' m)) * (i - 2)) + 1) + 1 by XREAL_1:8;
hence 1 < ((2 |^ (n -' m)) * (i - 2)) + 2 ; :: thesis: ((2 |^ (n -' m)) * (i - 2)) + 2 < len (Gauge D,n)
len (Gauge D,m) = (2 |^ m) + (2 + 1) by JORDAN8:def 1
.= ((2 |^ m) + 2) + 1 ;
then i <= (2 |^ m) + 2 by A3, NAT_1:13;
then i2 <= 2 |^ m by XREAL_1:22;
then (2 |^ (n -' m)) * i2 <= (2 |^ (n -' m)) * (2 |^ m) by XREAL_1:66;
then (2 |^ (n -' m)) * i2 <= 2 |^ ((n -' m) + m) by NEWTON:13;
then (2 |^ (n -' m)) * i2 <= 2 |^ n by A1, XREAL_1:237;
then (2 |^ (n -' m)) * i2 < (2 |^ n) + 1 by NAT_1:13;
then ((2 |^ (n -' m)) * (i - 2)) + 2 < ((2 |^ n) + 1) + 2 by XREAL_1:8;
then ((2 |^ (n -' m)) * (i - 2)) + 2 < (2 |^ n) + (1 + 2) ;
hence ((2 |^ (n -' m)) * (i - 2)) + 2 < len (Gauge D,n) by JORDAN8:def 1; :: thesis: verum