let i, m, n be Nat; 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); ( 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))
; ( 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
; ((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; verum