let n be Element of NAT ; :: thesis: 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); :: thesis: 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); :: thesis: 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; :: thesis: ( 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)/] ; :: thesis: I + 1 <= len (Gauge C,n)
A3: E-bound C >= E-bound (BDD C) by A1, Th19;
BDD C is Bounded by JORDAN2C:114;
then p `1 <= E-bound (BDD C) by A1, Th6;
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:11;
(E-bound C) - (W-bound C) > 0 by SPRECT_1:33, XREAL_1:52;
then ((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C)) <= 1 by A4, XREAL_1:187;
then (((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n) <= 1 * (2 |^ n) by XREAL_1:66;
then A5: ((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 3 <= (2 |^ n) + 3 by XREAL_1:9;
I <= ((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2 by A2, INT_1:def 4;
then A6: I + 1 <= (((((p `1 ) - (W-bound C)) / ((E-bound C) - (W-bound C))) * (2 |^ n)) + 2) + 1 by XREAL_1:8;
len (Gauge C,n) = (2 |^ n) + 3 by JORDAN8:def 1;
hence I + 1 <= len (Gauge C,n) by A5, A6, XXREAL_0:2; :: thesis: verum