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