let C be Subset of (TOP-REAL 2); :: thesis: for n, m, i being Element of 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 Element of 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:18;
A4: 2 |^ (n -' m) > 0 by NEWTON:102;
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:9;
then i2 < 2 |^ m by XREAL_1:21;
then (2 |^ (n -' m)) * i2 < (2 |^ (n -' m)) * (2 |^ m) by A4, XREAL_1:70;
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 < (2 |^ n) + 2 by XREAL_1:10;
then (((2 |^ (n -' m)) * (i - 2)) + 2) + 1 < ((2 |^ n) + 2) + 1 by XREAL_1:10;
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