let i, m, n be 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:5;
0 < ((2 |^ (n -' m)) * i2) + 1 ;
then 0 + 1 < (((2 |^ (n -' m)) * (i - 2)) + 1) + 1 by XREAL_1:6;
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:20;
then (2 |^ (n -' m)) * i2 <= (2 |^ (n -' m)) * (2 |^ m) by XREAL_1:64;
then (2 |^ (n -' m)) * i2 <= 2 |^ ((n -' m) + m) by NEWTON:8;
then (2 |^ (n -' m)) * i2 <= 2 |^ n by A1, XREAL_1:235;
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:6;
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