let C be Subset of (TOP-REAL 2); :: thesis: for n, m, i being Nat st m <= n & 1 < i & i + 1 < len (Gauge (C,m)) holds
(((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))
let n, m, i be Nat; :: thesis: ( m <= n & 1 < i & i + 1 < len (Gauge (C,m)) implies (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) )
assume that
A1: m <= n and
A2: 1 < i and
A3: i + 1 < len (Gauge (C,m)) ; :: thesis: (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n))
1 + 1 <= i by A2, NAT_1:13;
then reconsider i2 = i - 2 as Element of NAT by INT_1:5;
A4: 2 |^ (n -' m) > 0 by NEWTON:83;
len (Gauge (C,m)) = (2 |^ m) + (2 + 1) by JORDAN8:def 1
.= ((2 |^ m) + 2) + 1 ;
then i < (2 |^ m) + 2 by A3, XREAL_1:7;
then i2 < 2 |^ m by XREAL_1:19;
then (2 |^ (n -' m)) * i2 < (2 |^ (n -' m)) * (2 |^ m) by A4, XREAL_1:68;
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 < (2 |^ n) + 2 by XREAL_1:8;
then (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < ((2 |^ n) + 2) + 1 by XREAL_1:8;
then (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < (2 |^ n) + (1 + 2) ;
hence (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < len (Gauge (C,n)) by JORDAN8:def 1; :: thesis: verum