let n be Nat; for p being Point of (TOP-REAL 2)
for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))
let p be Point of (TOP-REAL 2); for C being compact non vertical Subset of (TOP-REAL 2)
for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))
let C be compact non vertical Subset of (TOP-REAL 2); for I being Integer st p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] holds
I + 1 <= len (Gauge (C,n))
set W = W-bound C;
set E = E-bound C;
set EW = (E-bound C) - (W-bound C);
set pW = (p `1) - (W-bound C);
let I be Integer; ( p in BDD C & I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/] implies I + 1 <= len (Gauge (C,n)) )
assume that
A1:
p in BDD C
and
A2:
I = [\(((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2)/]
; I + 1 <= len (Gauge (C,n))
A3:
E-bound C >= E-bound (BDD C)
by A1, Th7;
BDD C is bounded
by JORDAN2C:106;
then
p `1 <= E-bound (BDD C)
by A1, Th5;
then
p `1 <= E-bound C
by A3, XXREAL_0:2;
then A4:
(p `1) - (W-bound C) <= (E-bound C) - (W-bound C)
by XREAL_1:9;
(E-bound C) - (W-bound C) > 0
by SPRECT_1:31, XREAL_1:50;
then
((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C)) <= 1
by A4, XREAL_1:185;
then
(((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n) <= 1 * (2 |^ n)
by XREAL_1:64;
then A5:
((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 3 <= (2 |^ n) + 3
by XREAL_1:7;
I <= ((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2
by A2, INT_1:def 6;
then A6:
I + 1 <= (((((p `1) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2) + 1
by XREAL_1:6;
len (Gauge (C,n)) = (2 |^ n) + 3
by JORDAN8:def 1;
hence
I + 1 <= len (Gauge (C,n))
by A5, A6, XXREAL_0:2; verum