let C be compact non horizontal non vertical Subset of (TOP-REAL 2); for r, t being Real st r > 0 & t > 0 holds
ex n being Nat st
( 1 < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
let r, t be Real; ( r > 0 & t > 0 implies ex n being Nat st
( 1 < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t ) )
assume that
A1:
r > 0
and
A2:
t > 0
; ex n being Nat st
( 1 < n & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (1,2))) < r & dist (((Gauge (C,n)) * (1,1)),((Gauge (C,n)) * (2,1))) < t )
set n = N-bound C;
set e = E-bound C;
set s = S-bound C;
set w = W-bound C;
set a = |.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1;
set b = |.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1;
take i = (max ((|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1),(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1))) + 1; ( 1 < i & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t )
A3:
2 to_power i > 0
by POWER:34;
then A4:
2 |^ i > 0
by POWER:41;
[\(log (2,(((N-bound C) - (S-bound C)) / r)))/] <= |.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].|
by ABSVALUE:4;
then A5:
[\(log (2,(((N-bound C) - (S-bound C)) / r)))/] + 1 <= |.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1
by XREAL_1:6;
[\(log (2,(((N-bound C) - (S-bound C)) / r)))/] > (log (2,(((N-bound C) - (S-bound C)) / r))) - 1
by INT_1:def 6;
then
[\(log (2,(((N-bound C) - (S-bound C)) / r)))/] + 1 > ((log (2,(((N-bound C) - (S-bound C)) / r))) - 1) + 1
by XREAL_1:6;
then A6:
|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1 > ((log (2,(((N-bound C) - (S-bound C)) / r))) - 1) + 1
by A5, XXREAL_0:2;
|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1 <= max ((|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1),(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1))
by XXREAL_0:25;
then A7:
(|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1) + 1 <= (max ((|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1),(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1))) + 1
by XREAL_1:6;
|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1 < (|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1) + 1
by XREAL_1:29;
then
i > |.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1
by A7, XXREAL_0:2;
then
i > log (2,(((N-bound C) - (S-bound C)) / r))
by A6, XXREAL_0:2;
then
log (2,(2 to_power i)) > log (2,(((N-bound C) - (S-bound C)) / r))
by A3, POWER:def 3;
then
2 to_power i > ((N-bound C) - (S-bound C)) / r
by A3, PRE_FF:10;
then
2 |^ i > ((N-bound C) - (S-bound C)) / r
by POWER:41;
then
(2 |^ i) * r > (((N-bound C) - (S-bound C)) / r) * r
by A1, XREAL_1:68;
then
(2 |^ i) * r > (N-bound C) - (S-bound C)
by A1, XCMPLX_1:87;
then
((2 |^ i) * r) / (2 |^ i) > ((N-bound C) - (S-bound C)) / (2 |^ i)
by A4, XREAL_1:74;
then A8:
((N-bound C) - (S-bound C)) / (2 |^ i) < r
by A4, XCMPLX_1:89;
( |.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1 >= 0 + 1 & max ((|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1),(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1)) >= |.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1 )
by XREAL_1:7, XXREAL_0:25;
then
max ((|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1),(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1)) >= 1
by XXREAL_0:2;
then
(max ((|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1),(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1))) + 1 >= 1 + 1
by XREAL_1:7;
hence
1 < i
by XXREAL_0:2; ( dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t )
A9:
len (Gauge (C,i)) >= 4
by JORDAN8:10;
then A10:
1 <= len (Gauge (C,i))
by XXREAL_0:2;
[\(log (2,(((E-bound C) - (W-bound C)) / t)))/] <= |.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].|
by ABSVALUE:4;
then A11:
[\(log (2,(((E-bound C) - (W-bound C)) / t)))/] + 1 <= |.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1
by XREAL_1:6;
[\(log (2,(((E-bound C) - (W-bound C)) / t)))/] > (log (2,(((E-bound C) - (W-bound C)) / t))) - 1
by INT_1:def 6;
then
[\(log (2,(((E-bound C) - (W-bound C)) / t)))/] + 1 > ((log (2,(((E-bound C) - (W-bound C)) / t))) - 1) + 1
by XREAL_1:6;
then A12:
|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1 > ((log (2,(((E-bound C) - (W-bound C)) / t))) - 1) + 1
by A11, XXREAL_0:2;
|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1 <= max ((|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1),(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1))
by XXREAL_0:25;
then A13:
(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1) + 1 <= (max ((|.[\(log (2,(((N-bound C) - (S-bound C)) / r)))/].| + 1),(|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1))) + 1
by XREAL_1:6;
|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1 < (|.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1) + 1
by XREAL_1:29;
then
i > |.[\(log (2,(((E-bound C) - (W-bound C)) / t)))/].| + 1
by A13, XXREAL_0:2;
then
i > log (2,(((E-bound C) - (W-bound C)) / t))
by A12, XXREAL_0:2;
then
log (2,(2 to_power i)) > log (2,(((E-bound C) - (W-bound C)) / t))
by A3, POWER:def 3;
then
2 to_power i > ((E-bound C) - (W-bound C)) / t
by A3, PRE_FF:10;
then
2 |^ i > ((E-bound C) - (W-bound C)) / t
by POWER:41;
then
(2 |^ i) * t > (((E-bound C) - (W-bound C)) / t) * t
by A2, XREAL_1:68;
then
(2 |^ i) * t > (E-bound C) - (W-bound C)
by A2, XCMPLX_1:87;
then
((2 |^ i) * t) / (2 |^ i) > ((E-bound C) - (W-bound C)) / (2 |^ i)
by A4, XREAL_1:74;
then A14:
((E-bound C) - (W-bound C)) / (2 |^ i) < t
by A4, XCMPLX_1:89;
A15:
len (Gauge (C,i)) = width (Gauge (C,i))
by JORDAN8:def 1;
then A16:
[1,1] in Indices (Gauge (C,i))
by A10, MATRIX_0:30;
A17:
1 + 1 <= width (Gauge (C,i))
by A15, A9, XXREAL_0:2;
then A18:
[1,(1 + 1)] in Indices (Gauge (C,i))
by A10, MATRIX_0:30;
[(1 + 1),1] in Indices (Gauge (C,i))
by A15, A10, A17, MATRIX_0:30;
hence
( dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (1,2))) < r & dist (((Gauge (C,i)) * (1,1)),((Gauge (C,i)) * (2,1))) < t )
by A8, A14, A16, A18, Th9, Th10; verum