let m, i, n be Nat; for C being compact non horizontal non vertical Subset of (TOP-REAL 2) st m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) holds
( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) )
let C be compact non horizontal non vertical Subset of (TOP-REAL 2); ( m <= n & 1 <= i & i + 1 <= len (Gauge (C,n)) implies ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) ) )
assume that
A1:
m <= n
and
A2:
1 <= i
and
A3:
i + 1 <= len (Gauge (C,n))
; ( 1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/] & [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m)) )
A4:
(n -' m) + 1 <= 2 |^ (n -' m)
by NEWTON:85;
i + 1 <= (2 |^ n) + (2 + 1)
by A3, JORDAN8:def 1;
then
i + 1 <= ((2 |^ n) + 2) + 1
;
then
i <= (2 |^ n) + 2
by XREAL_1:6;
then
i - 2 <= 2 |^ n
by XREAL_1:20;
then
i - 2 <= 2 |^ (m + (n -' m))
by A1, XREAL_1:235;
then
(i - 2) * 1 <= (2 |^ m) * (2 |^ (n -' m))
by NEWTON:8;
then
(i - 2) / (2 |^ (n -' m)) <= (2 |^ m) / 1
by A4, XREAL_1:102;
then
((i - 2) / (2 |^ (n -' m))) + 3 <= (2 |^ m) + 3
by XREAL_1:6;
then A5:
((i - 2) / (2 |^ (n -' m))) + 3 <= len (Gauge (C,m))
by JORDAN8:def 1;
set i1 = [\(((i - 2) / (2 |^ (n -' m))) + 2)/];
(((i - 2) / (2 |^ (n -' m))) + 2) - 1 = ((i - 2) / (2 |^ (n -' m))) + (2 - 1)
;
then A6:
((i - 2) / (2 |^ (n -' m))) + 1 < [\(((i - 2) / (2 |^ (n -' m))) + 2)/]
by INT_1:def 6;
(n -' m) + 1 >= 0 + 1
by XREAL_1:6;
then
0 + 1 <= 2 |^ (n -' m)
by A4, XXREAL_0:2;
then A7:
(- 1) / 1 <= (- 1) / (2 |^ (n -' m))
by XREAL_1:120;
1 - 2 <= i - 2
by A2, XREAL_1:9;
then
(- 1) / (2 |^ (n -' m)) <= (i - 2) / (2 |^ (n -' m))
by XREAL_1:72;
then
- 1 <= (i - 2) / (2 |^ (n -' m))
by A7, XXREAL_0:2;
then
(- 1) + 1 <= ((i - 2) / (2 |^ (n -' m))) + 1
by XREAL_1:6;
then
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] >= 1 + 0
by A6, INT_1:7;
hence
1 <= [\(((i - 2) / (2 |^ (n -' m))) + 2)/]
; [\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m))
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] <= ((i - 2) / (2 |^ (n -' m))) + 2
by INT_1:def 6;
then
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= (((i - 2) / (2 |^ (n -' m))) + 2) + 1
by XREAL_1:6;
hence
[\(((i - 2) / (2 |^ (n -' m))) + 2)/] + 1 <= len (Gauge (C,m))
by A5, XXREAL_0:2; verum